1open HolKernel boolLib bossLib OpenTheoryMap OpenTheoryBoolTheory 2 3val Thy = "HOL4bool" 4val _ = new_theory Thy 5 6val n = ref 0; 7fun export (tm,tac) = 8 store_thm(("th"^Int.toString(!n)),tm,tac) 9 before n := !n+1 10 11val res0 = export(``!t. F ==> t``, 12 gen_tac >> 13 qspec_then`t`(ACCEPT_TAC o C MATCH_MP th136 o snd o EQ_IMP_RULE) th98) 14 (* DB.match["OpenTheoryBool"]``F ==> t`` *) 15 16val res = export(``~~p ==> p``, 17 qspec_then`p`(ACCEPT_TAC o fst o EQ_IMP_RULE) th110) 18 (* DB.match["OpenTheoryBool"]``~~p`` *) 19 20val res2 = export(``~(p ==> q) ==> p``, 21 strip_tac >> 22 qspecl_then[`p`,`q`](ACCEPT_TAC o CONJUNCT1 o UNDISCH o fst o EQ_IMP_RULE) th52) 23 (* DB.match["OpenTheoryBool"]``~(p ==> q)`` *) 24 25val res3 = export(``!x. x = (x = T)``, 26 ACCEPT_TAC(GSYM th106)) 27 (* DB.match["OpenTheoryBool"]``x = T`` *) 28 29val res = export(``~(p ==> q) ==> ~q``, 30 strip_tac >> 31 qspecl_then[`p`,`q`](ACCEPT_TAC o CONJUNCT2 o UNDISCH o fst o EQ_IMP_RULE) th52) 32 (* DB.match["OpenTheoryBool"]``~(p ==> q)`` *) 33 34val res = export(``~(p \/ q) ==> ~p``, 35 strip_tac >> 36 qspecl_then[`p`,`q`](ACCEPT_TAC o CONJUNCT1 o UNDISCH o fst o EQ_IMP_RULE) th50) 37 (* DB.match["OpenTheoryBool"]``~(p \/ q)`` *) 38 39val res = export(``~(p \/ q) ==> ~q``, 40 strip_tac >> 41 qspecl_then[`p`,`q`](ACCEPT_TAC o CONJUNCT2 o UNDISCH o fst o EQ_IMP_RULE) th50) 42 (* DB.match["OpenTheoryBool"]``~(p \/ q)`` *) 43 44val res7 = export(``!A. A ==> ~A ==> F``, 45 gen_tac >> strip_tac >> 46 disch_then(fn th => qspec_then`A`(mp_tac o C EQ_MP th o SYM)th104) >> 47 disch_then(fn th => pop_assum(ACCEPT_TAC o EQ_MP (SYM th)))) 48 (* DB.match["OpenTheoryBool"]``(F <=> t) <=> ~t`` *) 49 50val res8 = export(``!t1 t2. (t1 ==> t2) ==> (t2 ==> t1) ==> (t1 <=> t2)``, 51 deductAntisym 52 (MP (ASSUME``t2 ==> t1``) (ASSUME``t2:bool``)) 53 (MP (ASSUME``t1 ==> t2``) (ASSUME``t1:bool``)) 54 |> DISCH``t2 ==> t1`` |> DISCH_ALL 55 |> Q.GEN`t2` |> GEN_ALL 56 |> ACCEPT_TAC) 57 58val res9 = export(``!t. t ==> F <=> (t = F)``, 59 res8 60 |> Q.SPECL[`t==>F`,`t <=> F`] 61 |> C MP (DISCH_ALL(SYM(UNDISCH(MATCH_MP res8 (SPEC_ALL res0))))) 62 |> CONV_RULE(PATH_CONV"lrlr"(REWR_CONV (SPEC_ALL th105) THENC 63 RATOR_CONV(REWR_CONV th132) THENC 64 BETA_CONV)) 65 |> C MP (DISCH_ALL(ASSUME``t ==> F``)) 66 |> GEN_ALL 67 |> ACCEPT_TAC) 68 (* DB.match["OpenTheoryBool"]``(t <=> F) = ~t`` *) 69 (* DB.match["OpenTheoryBool"]``$~ = x`` *) 70 71val res = export(``!x. (x = x) <=> T``, 72 EQ_MP(SYM(Q.SPEC`x = x`th106))(REFL``x:'a``) 73 |> GEN_ALL |> ACCEPT_TAC) 74 (* DB.match["OpenTheoryBool"]``(x = T)`` *) 75 76val _ = OpenTheory_const_name{ 77 const={Thy=Thy,Name="literal_case"}, 78 name=(["HOL4"],"literal_case")} 79val def = new_definition("literal_case_def",concl boolTheory.literal_case_DEF) 80val res = export(``!f x. literal_case f x = f x``, 81 rpt gen_tac >> CONV_TAC(PATH_CONV"lrll"(REWR_CONV def)) >> 82 CONV_TAC(RATOR_CONV(RAND_CONV (RATOR_CONV BETA_CONV THENC BETA_CONV))) >> 83 REFL_TAC); 84 85val _ = OpenTheory_const_name{ 86 const={Thy=Thy,Name="LET"}, 87 name=(["Data","Bool"],"let")} 88val def = new_definition("LET",concl boolTheory.LET_DEF) 89val res = export(``!f x. LET f x = f x``, 90 rpt gen_tac >> CONV_TAC(PATH_CONV"lrll"(REWR_CONV def)) >> 91 CONV_TAC(RATOR_CONV(RAND_CONV (RATOR_CONV BETA_CONV THENC BETA_CONV))) >> 92 REFL_TAC); 93 94val _ = OpenTheory_const_name{ 95 const={Thy=Thy,Name="TYPE_DEFINITION"}, 96 name=(["HOL4"],"TYPE_DEFINITION")} 97val def = new_definition("TYPE_DEFINITION",concl boolTheory.TYPE_DEFINITION) 98val res13 = export(``!P rep. TYPE_DEFINITION P rep <=> ^(rhs(concl(SPEC_ALL boolTheory.TYPE_DEFINITION_THM)))``, 99 rpt gen_tac >> CONV_TAC(PATH_CONV"lrll"(REWR_CONV def)) >> 100 CONV_TAC(RATOR_CONV(RAND_CONV (RATOR_CONV BETA_CONV THENC BETA_CONV))) >> 101 REFL_TAC); 102 103val res = export(``(~A ==> F) ==> (A ==> F) ==> F``, 104 CONV_TAC(PATH_CONV"lr"(REWR_CONV res9)) >> 105 disch_then(fn th => CONV_TAC(RAND_CONV(REWR_CONV(SYM th)))) >> 106 CONV_TAC(PATH_CONV"rl" (REWR_CONV th132)) >> 107 CONV_TAC(RAND_CONV BETA_CONV) >> 108 disch_then ACCEPT_TAC) 109 110val res = export(``!f g. (f = g) <=> !x. (f x = g x)``, 111 ACCEPT_TAC(GSYM th49)) 112 (* DB.match["OpenTheoryBool"]``!x. f x = g x`` *) 113 114val res = export(``!t1 t2. ((if T then t1 else t2) = t1) /\ ((if F then t1 else t2) = t2)``, 115 rpt gen_tac >> ACCEPT_TAC (CONJ (SPEC_ALL th75) (SPEC_ALL th76))) 116 (* DB.match["OpenTheoryBool"]``if a then b else c`` *) 117 118val res = export(``(!t. ~~t <=> t) /\ (~T <=> F) /\ (~F <=> T)``, 119 ACCEPT_TAC (LIST_CONJ[th110,th134,th135])) 120 (* DB.match["OpenTheoryBool"]``~~ t <=> t`` *) 121 (* DB.match["OpenTheoryBool"]``~T <=> F`` *) 122 (* DB.match["OpenTheoryBool"]``~F <=> T`` *) 123 124val res = export(``!t. 125 ((T <=> t) <=> t) /\ ((t <=> T) <=> t) /\ ((F <=> t) <=> ~t) /\ 126 ((t <=> F) <=> ~t)``, 127 ACCEPT_TAC (GEN_ALL(LIST_CONJ(map SPEC_ALL [th107,th106,th104,th105])))) 128 (* DB.match["OpenTheoryBool"]``T = t`` *) 129 (* DB.match["OpenTheoryBool"]``t = T`` *) 130 (* DB.match["OpenTheoryBool"]``F = t`` *) 131 (* DB.match["OpenTheoryBool"]``t = F`` *) 132 133val res = export(``!t. 134 (T /\ t <=> t) /\ (t /\ T <=> t) /\ (F /\ t <=> F) /\ 135 (t /\ F <=> F) /\ (t /\ t <=> t)``, 136 ACCEPT_TAC (GEN_ALL(LIST_CONJ(map SPEC_ALL [th102,th100,th103,th101,th99])))) 137 (* DB.match["OpenTheoryBool"]``T /\ t`` *) 138 (* DB.match["OpenTheoryBool"]``t /\ T`` *) 139 (* DB.match["OpenTheoryBool"]``F /\ t`` *) 140 (* DB.match["OpenTheoryBool"]``t /\ F`` *) 141 (* DB.match["OpenTheoryBool"]``t /\ t = t`` *) 142 143val res = export(``!t. 144 (T \/ t <=> T) /\ (t \/ T <=> T) /\ (F \/ t <=> t) /\ 145 (t \/ F <=> t) /\ (t \/ t <=> t)``, 146 ACCEPT_TAC (GEN_ALL(LIST_CONJ(map SPEC_ALL [th93,th91,th94,th92,th90])))) 147 (* DB.match["OpenTheoryBool"]``T \/ t`` *) 148 (* DB.match["OpenTheoryBool"]``t \/ T`` *) 149 (* DB.match["OpenTheoryBool"]``F \/ t`` *) 150 (* DB.match["OpenTheoryBool"]``t \/ F`` *) 151 (* DB.match["OpenTheoryBool"]``t \/ t = t`` *) 152 153val res = export(``!t. 154 (T ==> t <=> t) /\ (t ==> T <=> T) /\ (F ==> t <=> T) /\ 155 (t ==> t <=> T) /\ (t ==> F <=> ~t)``, 156 ACCEPT_TAC (GEN_ALL(LIST_CONJ(map SPEC_ALL [th97,th96,th98, 157 EQ_MP (Q.SPEC`t ==> t`res3) (SPEC_ALL th84), th95])))) 158 (* DB.match["OpenTheoryBool"]``T ==> t`` *) 159 (* DB.match["OpenTheoryBool"]``t ==> T`` *) 160 (* DB.match["OpenTheoryBool"]``F ==> t`` *) 161 (* DB.match["OpenTheoryBool"]``t ==> t`` *) 162 (* DB.match["OpenTheoryBool"]``t ==> F`` *) 163 164val res = export(``~(t /\ ~t)``, 165 CONV_TAC(REWR_CONV th51) >> 166 MATCH_ACCEPT_TAC th82) 167 (* DB.match["OpenTheoryBool"]``~(t /\ q)`` *) 168 (* DB.match["OpenTheoryBool"]``t \/ ~t`` *) 169 170val res = export(``!t. ~t ==> t ==> F``, 171 gen_tac >> 172 CONV_TAC(LAND_CONV(REWR_CONV(GSYM th95))) >> 173 MATCH_ACCEPT_TAC th84) 174 (* DB.match["OpenTheoryBool"]``t ==> F`` *) 175 (* DB.match["OpenTheoryBool"]``t ==> t`` *) 176 177val res = export(``!t. (t ==> F) ==> ~t``, 178 gen_tac >> 179 CONV_TAC(RAND_CONV(REWR_CONV(GSYM th95))) >> 180 MATCH_ACCEPT_TAC th84) 181 182val res = export(``!f b x y. f (if b then x else y) = if b then f x else f y``, 183 rpt gen_tac >> 184 MATCH_ACCEPT_TAC th6); 185 (* DB.match["OpenTheoryBool"]``if x then y else z`` *) 186 187val res = export(``(!(t1:'a) t2. (if T then t1 else t2) = t1) /\ 188 !(t1:'a) t2. (if F then t1 else t2) = t2``, 189 ACCEPT_TAC(CONJ th75 th76)); 190 (* DB.match["OpenTheoryBool"]``if x then y else z`` *) 191 192val res = export(``!A B. A ==> B <=> ~A \/ B``, 193 rpt gen_tac >> 194 qspec_then`A`strip_assume_tac th81 >> 195 first_assum(fn th => PURE_REWRITE_TAC [th]) >> 196 PURE_REWRITE_TAC[th134,th135,th93,th94,th97,th98] >> 197 REFL_TAC ) 198 (* DB.match["OpenTheoryBool"]``A <=> T`` *) 199 (* DB.match["OpenTheoryBool"]``T ==> t`` *) 200 (* DB.match["OpenTheoryBool"]``F ==> t`` *) 201 (* DB.match["OpenTheoryBool"]``~T`` *) 202 (* DB.match["OpenTheoryBool"]``~F`` *) 203 (* DB.match["OpenTheoryBool"]``F \/ b`` *) 204 (* DB.match["OpenTheoryBool"]``T \/ b`` *) 205 206val res = export(``(x ==> y) /\ (z ==> w) ==> x /\ z ==> y /\ w``, 207 MATCH_ACCEPT_TAC th3) 208 209val res = export(``(x ==> y) /\ (z ==> w) ==> x \/ z ==> y \/ w``, 210 MATCH_ACCEPT_TAC th2) 211 212val res = export(``!t1 t2 t3. t1 /\ t2 /\ t3 <=> (t1 /\ t2) /\ t3``, 213 MATCH_ACCEPT_TAC(GSYM th14)) 214 (* DB.match["OpenTheoryBool"]``a /\ b /\ c`` *) 215 216val res = export(``!A B C. A \/ B \/ C <=> (A \/ B) \/ C``, 217 MATCH_ACCEPT_TAC(GSYM th11)) 218 (* DB.match["OpenTheoryBool"]``a \/ b \/ c`` *) 219 220val res = export(``!Q P. (!e. P e \/ Q) <=> (!x. P x) \/ Q``, 221 MATCH_ACCEPT_TAC th40) 222 (* DB.match["OpenTheoryBool"]``P e \/ Q`` *) 223 224val res = export(``!t1 t2. (t1 <=> t2) <=> t1 /\ t2 \/ ~t1 /\ ~t2``, 225 rpt gen_tac >> 226 qspec_then`t1`strip_assume_tac th81 >> 227 first_assum(fn th => PURE_REWRITE_TAC[th]) >> 228 PURE_REWRITE_TAC[th107,th102,th104,th103,th134,th135,th94,th92] >> 229 REFL_TAC) 230 (* DB.match["OpenTheoryBool"]``T <=> t`` *) 231 (* DB.match["OpenTheoryBool"]``F <=> t`` *) 232 (* DB.match["OpenTheoryBool"]``T /\ t`` *) 233 (* DB.match["OpenTheoryBool"]``F /\ t`` *) 234 (* DB.match["OpenTheoryBool"]``~T`` *) 235 (* DB.match["OpenTheoryBool"]``F \/ t`` *) 236 (* DB.match["OpenTheoryBool"]``t \/ F`` *) 237 238val res = export(``!A B C. B /\ C \/ A <=> (B \/ A) /\ (C \/ A)``, 239 MATCH_ACCEPT_TAC th10) 240 (* DB.match["OpenTheoryBool"]``b /\ c \/ a`` *) 241 242val res = export(``(?!x. P x) <=> ((?x. P x) /\ !x y. P x /\ P y ==> (x = y))``, 243 Q.ISPEC_THEN`P`MATCH_ACCEPT_TAC th86) 244 (* DB.match["OpenTheoryBool"]``?!x. P x`` *) 245 246val res = export(``(!x. P x ==> Q x) ==> (?x. P x) ==> ?x. Q x``, 247 MATCH_ACCEPT_TAC th21) 248 249val res = export(`` 250 !P Q. 251 ((?x. P x) ==> Q <=> !x. P x ==> Q) /\ 252 ((?x. P x) /\ Q <=> ?x. P x /\ Q) /\ 253 (Q /\ (?x. P x) <=> ?x. Q /\ P x)``, 254 rpt gen_tac >> 255 conj_tac >- MATCH_ACCEPT_TAC th55 >> 256 conj_tac >- MATCH_ACCEPT_TAC (GSYM th36) >> 257 MATCH_ACCEPT_TAC th69) 258 (* DB.match["OpenTheoryBool"]``(?x. P x) ==> Q`` *) 259 (* DB.match["OpenTheoryBool"]``(?x. P x) /\ Q`` *) 260 (* DB.match["OpenTheoryBool"]``Q /\ (?x. P x)`` *) 261 262val res = export( 263 ``!x x' y y'. 264 (x <=> x') /\ (x' ==> (y <=> y')) ==> (x ==> y <=> x' ==> y')``, 265 rpt gen_tac >> 266 PURE_REWRITE_TAC[GSYM th17] >> 267 disch_then(fn th => PURE_REWRITE_TAC[th]) >> 268 qspec_then`x'`strip_assume_tac th81 >> 269 pop_assum(fn th => PURE_REWRITE_TAC[th]) >> 270 PURE_REWRITE_TAC[th97,th98] >> 271 TRY(disch_then ACCEPT_TAC) >> REFL_TAC) 272 (* DB.match["OpenTheoryBool"]``(p1 ==> p2) <=> p3`` *) 273 (* DB.match["OpenTheoryBool"]``T ==> t`` *) 274 (* DB.match["OpenTheoryBool"]``F ==> t`` *) 275 276val res = export(``!A B. (~(A /\ B) <=> ~A \/ ~B) /\ (~(A \/ B) <=> ~A /\ ~B)``, 277 rpt gen_tac >> 278 conj_tac >- MATCH_ACCEPT_TAC th51 >> 279 MATCH_ACCEPT_TAC th50) 280 (* DB.match["OpenTheoryBool"]``~(a /\ b)`` *) 281 (* DB.match["OpenTheoryBool"]``~(a \/ b)`` *) 282 283val res8' = CONV_RULE(STRIP_QUANT_CONV(REWR_CONV th17))res8 284 285val res = export(``!t1 t2. (t1 <=> t2) <=> (t1 ==> t2) /\ (t2 ==> t1)``, 286 rpt gen_tac >> 287 match_mp_tac res8' >> 288 reverse conj_tac >- MATCH_ACCEPT_TAC res8' >> 289 disch_then(fn th => ACCEPT_TAC(CONJ 290 (MATCH_MP th27 th) 291 (MATCH_MP th27 (SYM th) )))) 292 (* DB.match["OpenTheoryBool"]``(t1 <=> t2) ==> t3`` *) 293 294val res = export(`` 295 !P. 296 (?(rep:'b -> 'a). TYPE_DEFINITION P rep) ==> 297 ?(rep:'b -> 'a) abs. (!a. (abs (rep a) = a)) /\ !r. (P r <=> (rep (abs r) = r))``, 298 gen_tac >> 299 ho_match_mp_tac th21 >> 300 gen_tac >> 301 CONV_TAC(LAND_CONV(REWR_CONV res13)) >> 302 strip_tac >> 303 qexists_tac`\ra. @a. rep a = ra` >> 304 conj_tac >- ( 305 CONV_TAC (QUANT_CONV(LAND_CONV BETA_CONV)) >> 306 gen_tac >> 307 ho_match_mp_tac th23 >> 308 gen_tac >> 309 match_mp_tac res8' >> 310 conj_tac >- first_assum MATCH_ACCEPT_TAC >> 311 disch_then(fn th => PURE_REWRITE_TAC[th]) >> 312 REFL_TAC ) >> 313 gen_tac >> 314 CONV_TAC(PATH_CONV"rlrr"BETA_CONV) >> 315 match_mp_tac res8' >> 316 pop_assum(fn th => PURE_REWRITE_TAC[th]) >> 317 conj_tac >- ( 318 CONV_TAC(HO_REWR_CONV th55) >> 319 CONV_TAC(QUANT_CONV(LAND_CONV SYM_CONV)) >> 320 Q.ISPEC_THEN`\a. rep a = r`(MATCH_ACCEPT_TAC o BETA_RULE) th29 ) >> 321 disch_then(fn th => CONV_TAC(QUANT_CONV(LAND_CONV(REWR_CONV(SYM th))))) >> 322 qexists_tac`@a. rep a = r` >> 323 REFL_TAC) 324 (* DB.match["OpenTheoryBool"]``$@`` *) 325 (* DB.match["OpenTheoryBool"]``p ==> q ==> r`` *) 326 327val res = export(`` 328 !P Q x x' y y'. 329 (P <=> Q) /\ (Q ==> (x = x')) /\ (~Q ==> (y = y')) ==> 330 ((if P then x else y) = if Q then x' else y')``, 331 rpt gen_tac >> 332 qspec_then`P`strip_assume_tac th81 >> 333 first_assum(fn th => PURE_REWRITE_TAC [th]) >> 334 qspec_then`Q`strip_assume_tac th81 >> 335 first_assum(fn th => PURE_REWRITE_TAC [th]) >> 336 PURE_REWRITE_TAC[th107,th104,th75,th76,th134,th135,th102,th103,th97,th98,th100] >> 337 disch_then ACCEPT_TAC ) 338 (* DB.match["OpenTheoryBool"]``F <=> t`` *) 339 (* DB.match["OpenTheoryBool"]``T <=> t`` *) 340 (* DB.match["OpenTheoryBool"]``T ==> t`` *) 341 (* DB.match["OpenTheoryBool"]``F ==> t`` *) 342 (* DB.match["OpenTheoryBool"]``T /\ t`` *) 343 (* DB.match["OpenTheoryBool"]``t /\ T`` *) 344 (* DB.match["OpenTheoryBool"]``F /\ t`` *) 345 (* DB.match["OpenTheoryBool"]``~T`` *) 346 (* DB.match["OpenTheoryBool"]``~F`` *) 347 (* DB.match["OpenTheoryBool"]``if T then x else y`` *) 348 (* DB.match["OpenTheoryBool"]``if F then x else y`` *) 349 350val _ = export_theory() 351