1(* non-interactive mode 2*) 3open HolKernel Parse boolLib; 4val _ = new_theory "subtype"; 5val _ = ParseExtras.temp_loose_equality() 6 7(* interactive mode 8show_assums := true; 9loadPath := union ["../ho_prover"] (!loadPath); 10app load 11 ["bossLib", "combinTheory", "pred_setTheory", "seqTheory", "HurdUseful", 12 "res_quanTheory", "ho_proverTools", "pairTheory"]; 13*) 14 15open bossLib combinTheory pred_setTheory seqTheory hurdUtils 16 res_quanTheory ho_proverTools pairTheory; 17 18infixr 0 ++ << || THENC ORELSEC ORELSER ##; 19infix 1 >>; 20 21val op++ = op THEN; 22val op<< = op THENL; 23val op|| = op ORELSE; 24val op>> = op THEN1; 25 26(* ------------------------------------------------------------------------- *) 27(* Auxiliary theorems. *) 28(* ------------------------------------------------------------------------- *) 29 30val EQ_T_IMP = store_thm 31 ("EQ_T_IMP", 32 ``!x. x = T ==> x``, 33 PROVE_TAC []); 34 35val EQ_SUBSET_SUBSET = store_thm 36 ("EQ_SUBSET_SUBSET", 37 ``!(s : 'a -> bool) t. (s = t) ==> s SUBSET t /\ t SUBSET s``, 38 RW_TAC std_ss [SUBSET_DEF, EXTENSION]); 39 40val IN_EQ_UNIV_IMP = store_thm 41 ("IN_EQ_UNIV_IMP", 42 ``!s. (s = UNIV) ==> !v. (v : 'a) IN s``, 43 RW_TAC std_ss [IN_UNIV]); 44 45(* ------------------------------------------------------------------------- *) 46(* bool theory subtypes. *) 47(* ------------------------------------------------------------------------- *) 48 49(* Subtype definitions *) 50 51val _ = add_infix("->", 250, HOLgrammars.RIGHT); 52 53val _ = overload_on 54 ("->", ``FUNSET:('a->bool) -> ('b->bool) -> (('a->'b)->bool)``); 55val _ = overload_on 56 ("-->", ``DFUNSET : ('a->bool) -> ('a->'b->bool) -> (('a->'b)->bool)``); 57 58val pair_def = Define 59 `pair (X : 'a -> bool) (Y : 'b -> bool) = \ (x, y). x IN X /\ y IN Y`; 60 61val IN_PAIR = store_thm 62 ("IN_PAIR", 63 ``!(x : 'a # 'b) X Y. x IN pair X Y = FST x IN X /\ SND x IN Y``, 64 Cases 65 ++ RW_TAC std_ss [pair_def, SPECIFICATION]); 66 67(* Simplifications *) 68 69val PAIR_UNIV = store_thm 70 ("PAIR_UNIV", 71 ``pair UNIV UNIV = (UNIV : 'a # 'b -> bool)``, 72 RW_TAC std_ss [SET_EQ, IN_PAIR, IN_UNIV]); 73 74(* Subtypes *) 75 76val DEFAULT_SUBTYPE = store_thm 77 ("DEFAULT_SUBTYPE", 78 ``!x. x IN UNIV``, 79 RW_TAC std_ss [IN_UNIV]); 80 81val COMB_SUBTYPE = store_thm 82 ("COMB_SUBTYPE", 83 ``!(f : 'a -> 'b) a x y. f IN (x --> y) /\ a IN x ==> f a IN y a``, 84 RW_TAC std_ss [IN_DFUNSET] 85 ++ PROVE_TAC []); 86 87val ABS_SUBTYPE = store_thm 88 ("ABS_SUBTYPE", 89 ``!(f : 'a -> 'b) p. (!x. f x IN p x) ==> (\x. f x) IN (UNIV --> p)``, 90 CONV_TAC (DEPTH_CONV FUN_EQ_CONV) 91 ++ RW_TAC std_ss [IN_DFUNSET]); 92 93val COND_SUBTYPE = store_thm 94 ("COND_SUBTYPE", 95 ``!c (a:'a) b x. 96 (c ==> a IN x) /\ 97 (~c ==> b IN x) ==> 98 COND c a b IN x``, 99 RW_TAC std_ss []); 100 101val RES_ABSTRACT_SUBTYPE = store_thm 102 ("RES_ABSTRACT_SUBTYPE", 103 ``!p (f : 'a -> 'b) q. 104 (!x. x IN p ==> (f x IN q x)) ==> 105 RES_ABSTRACT p f IN (p --> q)``, 106 RW_TAC std_ss [RES_FORALL, RES_ABSTRACT, IN_DFUNSET]); 107 108val UNCURRY_SUBTYPE = store_thm 109 ("UNCURRY_SUBTYPE", 110 ``!(f : 'a -> 'b -> 'c) p. 111 (!x y. f x y IN p x y) ==> 112 (UNCURRY f IN (UNIV --> UNCURRY p))``, 113 RW_TAC std_ss [IN_DFUNSET] 114 ++ Cases_on `x` 115 ++ RW_TAC std_ss []); 116 117(* ------------------------------------------------------------------------- *) 118(* The bool theory simplifier module. *) 119(* ------------------------------------------------------------------------- *) 120 121(* Congruences *) 122 123val comb_cong = store_thm 124 ("comb_cong", 125 ``!(f : 'a -> 'b) f' a a'. (f = f') /\ (a = a') ==> (f a = f' a')``, 126 RW_TAC std_ss []); 127 128val abs_cong = store_thm 129 ("abs_cong", 130 ``!(f : 'a -> 'b) f'. (!x. f x = f' x) ==> ((\x. f x) = f')``, 131 CONV_TAC (DEPTH_CONV FUN_EQ_CONV) 132 ++ RW_TAC std_ss []); 133 134val conj_cong = store_thm 135 ("conj_cong", 136 ``!a a' b b'. 137 (b ==> (a = a')) /\ 138 (a' ==> (b = b')) ==> 139 (a /\ b = a' /\ b')``, 140 RW_TAC std_ss [] 141 ++ ho_PROVE_TAC []); 142 143val disj_cong = store_thm 144 ("disj_cong", 145 ``!a a' b b'. 146 (~b ==> (a = a')) /\ 147 (~a' ==> (b = b')) ==> 148 (a \/ b = a' \/ b')``, 149 RW_TAC std_ss [] 150 ++ ho_PROVE_TAC []); 151 152val imp_cong = store_thm 153 ("imp_cong", 154 ``!a a' b b'. 155 (a = a') /\ 156 (a' ==> (b = b')) ==> 157 (a ==> b = a' ==> b')``, 158 RW_TAC std_ss [] 159 ++ ho_PROVE_TAC []); 160 161val cond_cong = store_thm 162 ("cond_cong", 163 ``!c c' (a:'a) a' b b'. 164 (c = c') /\ 165 (c' ==> (a = a')) /\ 166 (~c' ==> (b = b')) ==> 167 (COND c a b = COND c' a' b')``, 168 RW_TAC std_ss []); 169 170val res_forall_cong = store_thm 171 ("res_forall_cong", 172 ``!(p : 'a -> bool) p' f f'. 173 (p = p') /\ 174 (!x. x IN p' ==> (f x = f' x)) ==> 175 (RES_FORALL p f = RES_FORALL p' f')``, 176 RW_TAC std_ss [RES_FORALL]); 177 178val res_exists_cong = store_thm 179 ("res_exists_cong", 180 ``!(p : 'a -> bool) p' f f'. 181 (p = p') /\ 182 (!x. x IN p' ==> (f x = f' x)) ==> 183 (RES_EXISTS p f = RES_EXISTS p' f')``, 184 RW_TAC std_ss [RES_EXISTS] 185 ++ ho_PROVE_TAC []); 186 187val res_select_cong = store_thm 188 ("res_select_cong", 189 ``!(p : 'a -> bool) p' f f'. 190 (p = p') /\ 191 (!x. x IN p' ==> (f x = f' x)) ==> 192 (RES_SELECT p f = RES_SELECT p' f')``, 193 RW_TAC std_ss [RES_SELECT] 194 ++ Q_TAC SUFF_TAC `!x. x IN p /\ f x = x IN p /\ f' x` >> RW_TAC std_ss [] 195 ++ ho_PROVE_TAC []); 196 197val res_abstract_cong = store_thm 198 ("res_abstract_cong", 199 ``!(p : 'a -> bool) p' f f'. 200 (p = p') /\ 201 (!x. x IN p' ==> (f x = f' x)) ==> 202 (RES_ABSTRACT p f = RES_ABSTRACT p' f')``, 203 RW_TAC std_ss [RES_ABSTRACT_EQUAL]); 204 205val uncurry_cong = store_thm 206 ("uncurry_cong", 207 ``!(f : 'a -> 'b -> 'c) f'. 208 (!x y. f x y = f' x y) ==> 209 (UNCURRY f = UNCURRY f')``, 210 FUN_EQ_TAC 211 ++ RW_TAC std_ss [] 212 ++ Cases_on `x` 213 ++ RW_TAC std_ss [UNCURRY_DEF]); 214 215(* Rewrites *) 216 217val PAIRED_BETA_THM = store_thm 218 ("PAIRED_BETA_THM", 219 ``!f z. UNCURRY f z = f (FST z) (SND z)``, 220 STRIP_TAC 221 ++ Cases 222 ++ RW_TAC std_ss []); 223 224(* non-interactive mode 225*) 226val _ = export_theory (); 227