1open HolKernel boolLib Opentheory bossLib BasicProvers 2 3val Thy = "prove_base_assums"; 4 5val _ = new_theory Thy; 6 7val _ = new_constant("base-1.203",alpha); 8 9fun fix_tyop {abs={Name="_",Thy=athy},rep={Name="_",Thy=rthy},args,ax,name={Thy=tthy,Tyop=tyop}} = 10 {abs={Name=(tyop^"_abs"),Thy=athy}, 11 rep={Name=(tyop^"_rep"),Thy=rthy}, 12 name={Thy=tthy,Tyop=tyop}, 13 args=args, 14 ax=ax} 15| fix_tyop x = x 16 17fun const_name ([],"=") = {Thy="min",Name="="} 18 | const_name ([],"select") = {Thy="min",Name="@"} 19 | const_name (["Data","Bool"],"==>") = {Thy="min",Name="==>"} 20 | const_name (["Data","Bool"],"~") = {Thy="bool",Name="~"} 21 | const_name (["Data","Bool"],"!") = {Thy="bool",Name="!"} 22 | const_name (["Data","Bool"],"?") = {Thy="bool",Name="?"} 23 | const_name (["Data","Bool"],"?!") = {Thy="bool",Name="?!"} 24 | const_name (["Data","Bool"],"\\/") = {Thy="bool",Name="\\/"} 25 | const_name (["Data","Bool"],"/\\") = {Thy="bool",Name="/\\"} 26 | const_name (["Data","Bool"],"T") = {Thy="bool",Name="T"} 27 | const_name (["Data","Bool"],"F") = {Thy="bool",Name="F"} 28 | const_name (["Data","Bool"],"cond") = {Thy="bool",Name="COND"} 29 | const_name (["HOL4","bool"],"LET") = {Thy="bool",Name="LET"} 30 | const_name (["HOL4","bool"],"IN") = {Thy="bool",Name="IN"} 31 | const_name (["HOL4","bool"],"literal_case") = {Thy="bool",Name="literal_case"} 32 | const_name (["HOL4","bool"],"TYPE_DEFINITION") = {Thy="bool",Name="TYPE_DEFINITION"} 33 | const_name (["HOL4","bool"],"ARB") = {Thy="bool",Name="ARB"} 34 | const_name (["Data","Unit"],"()") = {Thy=Thy,Name="Data_Unit_unit"} 35 | const_name (["Data","Pair"],",") = {Thy=Thy,Name="Data_Pair_comma"} 36 | const_name (["Data","List"],"[]") = {Thy=Thy,Name="Data_List_nil"} 37 | const_name (["Data","List"],"::") = {Thy=Thy,Name="Data_List_cons"} 38 | const_name (["Data","List"],"@") = {Thy=Thy,Name="Data_List_append"} 39 | const_name (["Data","List","case","[]"],"::") = {Thy=Thy,Name="Data_List_case"} 40 | const_name (["Number","Natural"],"<") = {Thy=Thy,Name="Number_Natural_less"} 41 | const_name (["Number","Natural"],">") = {Thy=Thy,Name="Number_Natural_greater"} 42 | const_name (["Number","Natural"],"<=") = {Thy=Thy,Name="Number_Natural_lesseq"} 43 | const_name (["Number","Natural"],">=") = {Thy=Thy,Name="Number_Natural_greatereq"} 44 | const_name (["Number","Natural"],"*") = {Thy=Thy,Name="Number_Natural_times"} 45 | const_name (["Number","Natural"],"+") = {Thy=Thy,Name="Number_Natural_plus"} 46 | const_name (["Number","Natural"],"-") = {Thy=Thy,Name="Number_Natural_minus"} 47 | const_name (["Number","Natural"],"^") = {Thy=Thy,Name="Number_Natural_power"} 48 | const_name (["Number","Real"],"<=") = {Thy=Thy,Name="Number_Real_lesseq"} 49 | const_name (["Number","Real"],"<") = {Thy=Thy,Name="Number_Real_less"} 50 | const_name (["Number","Real"],">") = {Thy=Thy,Name="Number_Real_greater"} 51 | const_name (["Number","Real"],">=") = {Thy=Thy,Name="Number_Real_greatereq"} 52 | const_name (["Number","Real"],"+") = {Thy=Thy,Name="Number_Real_plus"} 53 | const_name (["Number","Real"],"*") = {Thy=Thy,Name="Number_Real_times"} 54 | const_name (["Number","Real"],"^") = {Thy=Thy,Name="Number_Real_power"} 55 | const_name (["Number","Real"],"~") = {Thy=Thy,Name="Number_Real_negate"} 56 | const_name (["Number","Real"],"-") = {Thy=Thy,Name="Number_Real_minus"} 57 | const_name (["Number","Real"],"/") = {Thy=Thy,Name="Number_Real_divide"} 58 | const_name (["Set"],"{}") = {Thy=Thy,Name="Set_empty"} 59 | const_name (["Function"],"^") = {Thy=Thy,Name="Function_pow"} 60 | const_name (ns,n) = {Thy=Thy,Name=String.concatWith "_"(ns@[n])} 61fun tyop_name ([],"bool") = {Thy="min",Tyop="bool"} 62 | tyop_name ([],"->") = {Thy="min",Tyop="fun"} 63 | tyop_name ([],"ind") = {Thy="min",Tyop="ind"} 64 | tyop_name (["Data","Pair"],"*") = {Thy=Thy,Tyop="Data_Pair_prod"} 65 | tyop_name (["Data","Sum"],"+") = {Thy=Thy,Tyop="Data_Sum_sum"} 66 | tyop_name (ns,n) = {Thy=Thy,Tyop=String.concatWith "_"(ns@[n])} 67 68val defs = ref ([]:thm list) 69fun add_def tm = 70 let 71 val th = mk_oracle_thm"def" ([],tm) 72 val _ = defs := th::(!defs) 73 in th end 74 75fun define_const {Thy="bool",Name="~"} tm = add_def(``$~ = ^tm``) 76 | define_const {Thy="bool",Name="!"} tm = add_def(``$! = ^tm``) 77 | define_const {Thy="bool",Name="?"} tm = add_def(``$? = ^tm``) 78 | define_const {Thy="bool",Name="?!"} tm = add_def(``$?! = ^tm``) 79 | define_const {Thy="bool",Name="\\/"} tm = add_def(``$\/ = ^tm``) 80 | define_const {Thy="bool",Name="/\\"} tm = add_def(``$/\ = ^tm``) 81 | define_const {Thy="bool",Name="T"} tm = add_def(``T = ^tm``) 82 | define_const {Thy="bool",Name="F"} tm = add_def(``F = ^tm``) 83 | define_const {Thy="bool",Name="COND"} tm = add_def(``COND = ^tm``) 84 | define_const {Thy="min",Name="==>"} tm = add_def(``$==> = ^tm``) 85 | define_const x tm = define_const_in_thy (fn x => x) x tm 86 87val (reader:reader) = { 88 define_tyop = define_tyop_in_thy o fix_tyop, 89 define_const = define_const, 90 axiom = fn _ => mk_thm, 91 const_name = const_name, 92 tyop_name = tyop_name} 93 94val base_thms = read_article "base-theorems.art" reader; 95 96val _ = Net.itnet (fn th => (Thm.delete_proof th; K ())) base_thms () 97 98fun itpred P th acc = if P th then th::acc else acc 99fun amatch tm = Net.itnet (itpred (DB.matches tm)) base_thms [] 100 101val _ = new_constant("hol-base-assums-1.0",alpha); 102 103local 104 fun find_tyop {name={Tyop,...},...} = 105 let 106 val (ar,ra) = definition(Tyop^"_bij") |> CONJ_PAIR 107 in 108 {rep_abs = uneta_type_bijection ra, 109 abs_rep = uneta_type_bijection ar} 110 end 111 fun find_const {Name,...} = definition(Name^"_def") 112 handle HOL_ERR _ => first (equal Name o #1 o dest_const o lhs o concl) (!defs) 113 handle HOL_ERR _ => raise(Fail Name) 114in 115 val (reader:reader) = { 116 define_tyop = fn x => find_tyop (fix_tyop x), 117 define_const = fn x => fn _ => find_const x, 118 axiom = fn _ => mk_thm, 119 const_name = const_name, 120 tyop_name = tyop_name} 121end 122 123val LET_DEF = add_def(concl LET_DEF) 124val IN_DEF = add_def(concl IN_DEF) 125val literal_case_DEF = add_def(concl literal_case_DEF) 126val TYPE_DEFINITION = add_def(concl TYPE_DEFINITION) 127val ARB_DEF = add_def(concl (REFL``ARB``)) 128 129val goalsNet = read_article "hol4-assums.art" reader; 130 131val goals = Net.listItems goalsNet 132 133val _ = Parse.hide"_" 134 135val bool_cases = hd (amatch ``t \/ ~t``) 136val or_def = hd(amatch``$\/ = _``) 137 138val imp_T = hd(amatch``t ==> T``) 139val T_imp = hd(amatch``T ==> t``) 140val F_imp = hd(amatch``F ==> t``) 141val imp_F = hd(amatch``t ==> F <=> _``) 142val imp_i = hd(amatch``t ==> t``) 143 144val T_iff = hd(amatch``(T <=> t) <=> _``) 145val iff_T = hd(amatch``(t <=> T) <=> _``) 146val F_iff = hd(amatch``(F <=> t) <=> _``) 147val iff_F = hd(amatch``(t <=> F) <=> _``) 148 149val and_imp_intro = hd(amatch``(a ==> b ==> c) <=> _``) 150 151val eq_T = hd(amatch``(t <=> T) <=> _``) 152fun EQT_INTRO th = EQ_MP (SPEC (concl th) (GSYM eq_T)) th 153 154val EQF_INTRO = SYM o (CONV_RULE(REWR_CONV(GSYM F_iff))) 155 156val not_and = hd (amatch ``~(t1 /\ t2) <=> _``) 157val not_not = hd (amatch ``~(~ _)``) 158val disj_comm = hd (amatch ``_ \/ _ <=> _ \/ _``) 159 160val T_or = hd(amatch``T \/ t``) 161val or_T = hd(amatch``t \/ T``) 162val F_or = hd(amatch``F \/ t``) 163val or_F = hd(amatch``t \/ F``) 164val or_i = hd(amatch``t \/ t``) 165 166val truth = hd(amatch``T``); 167val not_F = hd(amatch``~F``) 168 169val bool_cases = hd(amatch``(x = T) \/ _``) 170 171val th1 = store_thm("th1", el 1 goals |> concl, 172 PURE_REWRITE_TAC[not_and,not_not] 173 \\ Q.SPEC_THEN`t`FULL_STRUCT_CASES_TAC bool_cases 174 \\ PURE_REWRITE_TAC[or_T,or_F,not_F]) 175 176val ex_unique_thm = hd (amatch``(?!x. p x) <=> _ /\ _``) 177val list_rec = hd(amatch``fn (Data_List_cons h t) = f h t (fn t)``) 178val list_ind = hd(amatch``_ ==> !l:'a Data_List_list. P l``) 179val fun_eq_thm = hd(amatch``(!x. f x = g x) <=> (f = g)``) 180val th2 = store_thm("th2", el 2 goals |> concl, 181 rpt gen_tac 182 \\ CONV_TAC(HO_REWR_CONV ex_unique_thm) 183 \\ conj_tac >- ( 184 Q.ISPECL_THEN[`x`,`\h t a. f a h t`]strip_assume_tac list_rec 185 \\ qexists_tac`fn` 186 \\ first_x_assum (fn th => conj_tac >- MATCH_ACCEPT_TAC th) 187 \\ first_x_assum (MATCH_ACCEPT_TAC o BETA_RULE) ) 188 \\ rpt gen_tac \\ strip_tac 189 \\ PURE_REWRITE_TAC[GSYM fun_eq_thm] 190 \\ ho_match_mp_tac list_ind 191 \\ rpt VAR_EQ_TAC 192 \\ conj_tac >- (first_assum MATCH_ACCEPT_TAC) 193 \\ rpt strip_tac 194 \\ rpt (last_x_assum(qspecl_then[`h`,`x`]mp_tac)) 195 \\ pop_assum SUBST_ALL_TAC 196 \\ disch_then(SUBST_ALL_TAC o SYM) 197 \\ disch_then (MATCH_ACCEPT_TAC)); 198 199val o_def = hd(amatch``Function_o = _``) 200 201val sum_cases = hd(amatch``(?a. x = Data_Sum_left a) \/ _``) 202val sum_ind = hd(amatch``_ ==> !l:('a,'b) Data_Sum_sum. P l``) 203 204val sum_case_thms = amatch``Data_Sum_case_left_right f g (_ _) = _`` 205 206val th3 = store_thm("th3", el 3 goals |> concl, 207 rpt gen_tac 208 \\ CONV_TAC(HO_REWR_CONV ex_unique_thm) 209 \\ PURE_REWRITE_TAC[o_def] 210 \\ PURE_REWRITE_TAC[GSYM fun_eq_thm] 211 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 212 \\ rpt strip_tac 213 >- ( 214 qexists_tac`Data_Sum_case_left_right f g` 215 \\ PURE_REWRITE_TAC sum_case_thms 216 \\ PURE_REWRITE_TAC[fun_eq_thm] 217 \\ conj_tac \\ REFL_TAC ) 218 \\ Q.ISPEC_THEN`x`FULL_STRUCT_CASES_TAC sum_cases 219 >- ( 220 rpt(first_x_assum(qspec_then`a`SUBST_ALL_TAC)) 221 \\ REFL_TAC) 222 \\ rpt(first_x_assum(qspec_then`b`SUBST_ALL_TAC)) 223 \\ REFL_TAC) 224 225val if_T = hd(amatch``(if T then _ else _) = _``) 226val if_F = hd(amatch``(if F then _ else _) = _``) 227 228val th4 = store_thm("th4", el 4 goals |> concl, 229 rpt gen_tac 230 \\ rpt strip_tac 231 \\ last_x_assum SUBST_ALL_TAC 232 \\ Q.ISPEC_THEN`Q`FULL_STRUCT_CASES_TAC bool_cases 233 \\ PURE_REWRITE_TAC[if_T,if_F] 234 \\ first_x_assum match_mp_tac 235 \\ PURE_REWRITE_TAC[truth,not_F]); 236 237val T_and = hd(amatch``T /\ t``) 238val and_T = hd(amatch``t /\ T <=> _``) 239val F_and = hd(amatch``F /\ t``) 240val and_F = hd(amatch``t /\ F <=> _``) 241val and_i = hd(amatch``t /\ t``) 242 243val th5 = store_thm("th5", el 5 goals |> concl, 244 rpt strip_tac 245 \\ Q.ISPEC_THEN`Q`FULL_STRUCT_CASES_TAC bool_cases 246 \\ Q.ISPEC_THEN`P'`FULL_STRUCT_CASES_TAC bool_cases 247 \\ rpt (pop_assum mp_tac) 248 \\ PURE_REWRITE_TAC[and_T,T_and,and_F,F_and,T_imp,F_imp,T_iff,iff_T,F_iff,iff_F,not_F] 249 \\ TRY(disch_then MATCH_ACCEPT_TAC) 250 \\ disch_then(SUBST_ALL_TAC o EQT_INTRO) 251 \\ disch_then(SUBST_ALL_TAC o EQT_INTRO) 252 \\ REFL_TAC); 253 254val th6 = store_thm("th6", el 6 goals |> concl, 255 rpt strip_tac 256 \\ last_x_assum SUBST_ALL_TAC 257 \\ Q.ISPEC_THEN`x'`FULL_STRUCT_CASES_TAC bool_cases 258 \\ pop_assum mp_tac 259 \\ PURE_REWRITE_TAC[T_imp,F_imp] 260 \\ TRY REFL_TAC 261 \\ disch_then ACCEPT_TAC); 262 263val cons_11 = hd (amatch ``Data_List_cons _ _ = Data_List_cons _ _``) 264val th7 = store_thm("th7", el 7 goals |> concl, MATCH_ACCEPT_TAC cons_11) 265 266val app_if = hd (amatch ``f (if b then x else y) = if b then f x else f y``) 267val th8 = store_thm("th8", el 8 goals |> concl, MATCH_ACCEPT_TAC app_if) 268 269val demorgan = hd (amatch``(b \/ a) /\ (c \/ a)``) 270val th9 = store_thm("th9", el 9 goals |> concl, MATCH_ACCEPT_TAC demorgan) 271 272val or_assoc = hd (amatch``(a \/ b) \/ c``) 273val th10 = store_thm("th10", el 10 goals |> concl, MATCH_ACCEPT_TAC (GSYM or_assoc)) 274 275val or_distrib_and = hd (amatch``(b \/ c) /\ a <=> _``) 276val th11 = store_thm("th11", el 11 goals |> concl, MATCH_ACCEPT_TAC or_distrib_and) 277 278val and_assoc = hd (amatch``(a /\ b) /\ c``) 279val th12 = store_thm("th12", el 12 goals |> concl, MATCH_ACCEPT_TAC (GSYM and_assoc)) 280 281val if_T = hd (amatch ``if T then t1 else t2``) 282val if_F = hd (amatch ``if F then t1 else t2``) 283 284val th13 = store_thm("th13", el 13 goals |> concl, 285 rpt gen_tac 286 \\ qexists_tac`\b. if b then t1 else t2` 287 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 288 \\ PURE_REWRITE_TAC[if_T,if_F] 289 \\ conj_tac \\ REFL_TAC); 290 291val not_or = hd(amatch``~(_ \/ _)``) 292 293val th14 = store_thm("th14", el 14 goals |> concl, 294 rpt gen_tac 295 \\ PURE_REWRITE_TAC[not_and,not_or] 296 \\ conj_tac \\ REFL_TAC); 297 298val and_ex = hd(amatch``p /\ (?x. _) <=> ?x. p /\ _``) 299val ex_and = hd(amatch``(?x. _) /\ p <=> ?x. _ /\ p``) 300val ex_imp = hd(amatch``((?x. _) ==> _) <=> _``) 301 302val th15 = store_thm("th15", el 15 goals |> concl, 303 rpt gen_tac 304 \\ PURE_REWRITE_TAC[and_ex,ex_and,ex_imp] 305 \\ rpt conj_tac \\ REFL_TAC); 306 307val and_all = hd(amatch``p /\ (!x. _) <=> !x. p /\ _``) 308val all_and = hd(amatch``(!x. _) /\ p <=> !x. _ /\ p``) 309val all_imp = hd(amatch``((!x. _) ==> _) <=> _``) 310val imp_all = hd(amatch``(_ ==> (!x. _)) <=> _``) 311 312val th16 = store_thm("th16", el 16 goals |> concl, 313 rpt gen_tac 314 \\ PURE_REWRITE_TAC[and_all,all_and,all_imp,imp_all] 315 \\ rpt conj_tac \\ REFL_TAC); 316 317val th17 = store_thm("th17", el 17 goals |> concl, 318 rpt gen_tac \\ MATCH_ACCEPT_TAC (CONJ (SPEC_ALL if_T) (SPEC_ALL if_F))) 319 320val forall_eq = hd(amatch``!x. (x = t) ==> _``) 321val forall_eq2 = hd(amatch``!x. (t = x) ==> _``) 322 323val ex_def = hd(amatch``$? = _``) 324val select_ax = hd(amatch ``p t ==> p ($@ p)``) 325 326val th18 = store_thm("th18", el 18 goals |> concl, 327 PURE_REWRITE_TAC[forall_eq,ex_def] 328 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 329 \\ MATCH_ACCEPT_TAC select_ax); 330 331val eta_ax = hd(amatch``!f. (\x. f x) = f``) 332 333val th19 = store_thm("th19", el 19 goals |> concl, 334 PURE_REWRITE_TAC[ex_def] 335 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 336 \\ rpt strip_tac 337 \\ first_x_assum match_mp_tac 338 \\ CONV_TAC(RAND_CONV(RAND_CONV(REWR_CONV (GSYM eta_ax)))) 339 \\ first_x_assum ACCEPT_TAC); 340 341val th20 = store_thm("th20", el 20 goals |> concl, 342 rpt strip_tac 343 \\ Q.ISPEC_THEN`t1`mp_tac bool_cases 344 \\ PURE_REWRITE_TAC[or_def] 345 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 346 \\ disch_then(qspec_then`t1 = t2`mp_tac) 347 \\ PURE_REWRITE_TAC[iff_T,iff_F,and_imp_intro] 348 \\ disch_then match_mp_tac 349 \\ conj_tac 350 \\ TRY (disch_then(SUBST_ALL_TAC o EQF_INTRO)) 351 \\ TRY (disch_then(SUBST_ALL_TAC o EQT_INTRO)) 352 \\ rpt (pop_assum mp_tac) 353 \\ PURE_REWRITE_TAC[T_imp,T_iff,imp_T,F_imp,F_iff,imp_F] 354 \\ disch_then ACCEPT_TAC); 355 356val suc_11 =hd(amatch``Number_Natural_suc _ = Number_Natural_suc _``) 357val th21 = store_thm("th21", el 21 goals |> concl, 358 rpt gen_tac \\ MATCH_ACCEPT_TAC (#1 (EQ_IMP_RULE (SPEC_ALL suc_11)))) 359 360val forall_or = el 2 (amatch``_ <=> (!x. P x) \/ Q``) 361val th22 = store_thm("th22", el 22 goals |> concl, MATCH_ACCEPT_TAC forall_or) 362 363val null_eq = hd(amatch``Data_List_null t <=> (_ = Data_List_nil)``) 364val last_cons = hd(amatch``Data_List_last (Data_List_cons h t) = COND _ _ _``) 365 366val th23 = store_thm("th23", el 23 goals |> concl, 367 MATCH_ACCEPT_TAC(PURE_REWRITE_RULE[null_eq]last_cons)) 368 369val not_T = hd(amatch``~T``) 370 371val th24 = store_thm("th24", el 24 goals |> concl, 372 rpt gen_tac 373 \\ Q.ISPEC_THEN`t1`FULL_STRUCT_CASES_TAC bool_cases 374 \\ PURE_REWRITE_TAC[T_iff,T_and,not_T,F_and,or_F,not_F,F_or,F_iff] 375 \\ REFL_TAC); 376 377val th25 = store_thm("th25", el 25 goals |> concl, 378 rpt gen_tac 379 \\ Q.ISPEC_THEN`t1`FULL_STRUCT_CASES_TAC bool_cases 380 \\ PURE_REWRITE_TAC[T_iff,F_iff,T_imp,F_imp,imp_T,imp_F,and_T,T_and] 381 \\ REFL_TAC); 382 383val ext = hd(amatch``(!x. f x = g x) <=> _``) 384val th26 = store_thm("th26", el 26 goals |> concl, 385 MATCH_ACCEPT_TAC (GSYM ext)) 386 387val th27 = store_thm("th27", el 27 goals |> concl, 388 rpt gen_tac 389 \\ Q.ISPEC_THEN`A`FULL_STRUCT_CASES_TAC bool_cases 390 \\ PURE_REWRITE_TAC[T_iff,or_T,F_iff,or_F,imp_T,imp_F] 391 \\ REFL_TAC); 392 393val cons_neq_nil = hd(amatch``_ <> Data_List_nil``) 394val th28 = store_thm("th28", el 28 goals |> concl, MATCH_ACCEPT_TAC (GSYM cons_neq_nil)) 395 396val some_neq_none = hd(amatch``_ <> Data_Option_none``) 397val th29 = store_thm("th29", el 29 goals |> concl, MATCH_ACCEPT_TAC (GSYM some_neq_none)) 398 399val th30 = store_thm("th30", el 30 goals |> concl, 400 gen_tac 401 \\ conj_tac >- MATCH_ACCEPT_TAC T_imp 402 \\ conj_tac >- MATCH_ACCEPT_TAC imp_T 403 \\ conj_tac >- MATCH_ACCEPT_TAC F_imp 404 \\ conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO (SPEC_ALL imp_i)) 405 \\ MATCH_ACCEPT_TAC imp_F); 406 407val th31 = store_thm("th31", el 31 goals |> concl, 408 gen_tac 409 \\ conj_tac >- MATCH_ACCEPT_TAC T_or 410 \\ conj_tac >- MATCH_ACCEPT_TAC or_T 411 \\ conj_tac >- MATCH_ACCEPT_TAC F_or 412 \\ conj_tac >- MATCH_ACCEPT_TAC or_F 413 \\ MATCH_ACCEPT_TAC or_i); 414 415val th32 = store_thm("th32", el 32 goals |> concl, 416 gen_tac 417 \\ conj_tac >- MATCH_ACCEPT_TAC T_and 418 \\ conj_tac >- MATCH_ACCEPT_TAC and_T 419 \\ conj_tac >- MATCH_ACCEPT_TAC F_and 420 \\ conj_tac >- MATCH_ACCEPT_TAC and_F 421 \\ MATCH_ACCEPT_TAC and_i); 422 423val th33 = store_thm("th33", el 33 goals |> concl, 424 gen_tac 425 \\ conj_tac >- MATCH_ACCEPT_TAC T_iff 426 \\ conj_tac >- MATCH_ACCEPT_TAC iff_T 427 \\ conj_tac >- MATCH_ACCEPT_TAC F_iff 428 \\ MATCH_ACCEPT_TAC iff_F); 429 430val select_eq = hd(amatch``@y. y = x``) 431val th34 = store_thm("th34", el 34 goals |> concl, 432 CONV_TAC(QUANT_CONV(LAND_CONV(RAND_CONV(ABS_CONV SYM_CONV)))) 433 \\ MATCH_ACCEPT_TAC select_eq); 434 435val th35 = store_thm("th35", el 35 goals |> concl, 436 PURE_REWRITE_TAC[imp_F, iff_F] 437 \\ gen_tac \\ REFL_TAC) 438 439val refl = hd(amatch``!x. x = x``) 440val th36 = store_thm("th36", el 36 goals |> concl, 441 gen_tac \\ MATCH_ACCEPT_TAC(EQT_INTRO(SPEC_ALL refl))) 442 443val eq_trans = hd(amatch``(x = y) /\ (y = z) ==> _``) 444 445val th37 = store_thm("th37", el 37 goals |> concl, 446 rpt strip_tac 447 \\ first_assum(qspecl_then[`x`,`y`,`z`]SUBST_ALL_TAC) 448 \\ last_assum(qspecl_then[`f x y`,`z`]SUBST_ALL_TAC) 449 \\ first_assum(qspecl_then[`z`,`x`,`y`]SUBST_ALL_TAC) 450 \\ last_assum(qspecl_then[`f z x`,`y`]SUBST_ALL_TAC) 451 \\ AP_TERM_TAC 452 \\ last_assum(qspecl_then[`z`,`x`]ACCEPT_TAC)); 453 454val less_zero = hd(amatch``Number_Natural_less Number_Natural_zero n <=> _ <> _``) 455val div_mod = hd(amatch``Number_Natural_times (Number_Natural_div k n) n``) 456 457val less_mod = hd(amatch``Number_Natural_less (Number_Natural_mod _ _)``) 458 459val th38 = store_thm("th38", el 38 goals |> concl, 460 PURE_REWRITE_TAC[less_zero] 461 \\ gen_tac 462 \\ disch_then(fn th => (strip_assume_tac (MATCH_MP less_mod th) >> 463 (strip_assume_tac (MATCH_MP div_mod th)))) 464 \\ gen_tac 465 \\ first_x_assum(qspec_then`k`SUBST_ALL_TAC) 466 \\ conj_tac >- REFL_TAC 467 \\ first_x_assum(qspec_then`k`ACCEPT_TAC)); 468 469val list_ind = hd(amatch``_ ==> !(l:'a Data_List_list). P l``) 470val th39 = store_thm("th39", el 39 goals |> concl, 471 rpt strip_tac 472 \\ match_mp_tac list_ind 473 \\ conj_tac >- first_assum ACCEPT_TAC 474 \\ rpt strip_tac \\ res_tac 475 \\ first_assum MATCH_ACCEPT_TAC); 476 477val th40 = store_thm("th40", el 40 goals |> concl, 478 imp_F |> SPEC_ALL |> EQ_IMP_RULE |> #1 |> MATCH_ACCEPT_TAC) 479 480val th41 = store_thm("th41", el 41 goals |> concl, 481 imp_F |> SPEC_ALL |> EQ_IMP_RULE |> #2 |> MATCH_ACCEPT_TAC) 482 483val th42 = store_thm("th42", el 42 goals |> concl, 484 PURE_REWRITE_TAC[GSYM imp_F] 485 \\ gen_tac 486 \\ disch_then(fn th => disch_then(ACCEPT_TAC o C MP th))); 487 488val th43 = store_thm("th43", el 43 goals |> concl, 489 MATCH_ACCEPT_TAC(EQT_ELIM(SPEC_ALL F_imp))) 490 491val unpair = hd(amatch``Data_Pair_comma (Data_Pair_fst _) _``) 492 493val unzip_nil = hd(amatch``Data_List_unzip Data_List_nil``) 494val unzip_cons = hd(amatch``Data_List_unzip (Data_List_cons _ _)``) 495val th44 = store_thm("th44", el 44 goals |> concl, 496 conj_tac >- MATCH_ACCEPT_TAC unzip_nil 497 \\ PURE_REWRITE_TAC[unzip_cons] 498 \\ rpt gen_tac 499 \\ conj_tac 500 \\ MATCH_ACCEPT_TAC(GSYM unpair)); 501 502val reverse_nil = hd(amatch``Data_List_reverse Data_List_nil``) 503val reverse_cons = hd(amatch``Data_List_reverse (Data_List_cons _ _)``) 504val th45 = store_thm("th45", el 45 goals |> concl, 505 conj_tac >- MATCH_ACCEPT_TAC reverse_nil 506 \\ MATCH_ACCEPT_TAC reverse_cons); 507 508val concat_nil = hd(amatch``Data_List_concat Data_List_nil``) 509val concat_cons = hd(amatch``Data_List_concat (Data_List_cons _ _)``) 510val th46 = store_thm("th46", el 46 goals |> concl, 511 conj_tac >- MATCH_ACCEPT_TAC concat_nil 512 \\ MATCH_ACCEPT_TAC concat_cons); 513 514val fact_zero = hd(amatch``Number_Natural_factorial Number_Natural_zero``) 515val fact_suc = hd(amatch``Number_Natural_factorial (Number_Natural_suc _)``) 516 517val th47 = store_thm("th47", el 47 goals |> concl, 518 conj_tac >- MATCH_ACCEPT_TAC fact_zero 519 \\ MATCH_ACCEPT_TAC fact_suc); 520 521val length_nil = hd(amatch``Data_List_length Data_List_nil``) 522val length_cons = hd(amatch``Data_List_length (Data_List_cons _ _)``) 523val th48 = store_thm("th48", el 48 goals |> concl, 524 conj_tac >- MATCH_ACCEPT_TAC length_nil 525 \\ MATCH_ACCEPT_TAC length_cons); 526 527fun EQT_ELIM th = EQ_MP (SYM th) truth 528 529fun EQF_ELIM th = 530 let 531 val (lhs, rhs) = dest_eq (concl th) 532 val _ = assert (equal boolSyntax.F) rhs 533 in 534 NOT_INTRO (DISCH lhs (EQ_MP th (ASSUME lhs))) 535 end 536 537val null_nil = hd(amatch``Data_List_null Data_List_nil``) 538val null_cons = hd(amatch``Data_List_null (Data_List_cons _ _)``) 539 540val th49 = store_thm("th49", el 49 goals |> concl, 541 conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO null_nil) 542 \\ MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL null_cons))); 543 544val odd_nil = hd(amatch``Number_Natural_odd Number_Natural_zero``) 545val odd_cons = hd(amatch``Number_Natural_odd (Number_Natural_suc _)``) 546 547val th50 = store_thm("th50", el 50 goals |> concl, 548 conj_tac >- MATCH_ACCEPT_TAC (EQF_INTRO odd_nil) 549 \\ MATCH_ACCEPT_TAC odd_cons); 550 551val even_nil = hd(amatch``Number_Natural_even Number_Natural_zero``) 552val even_cons = hd(amatch``Number_Natural_even (Number_Natural_suc _)``) 553 554val th51 = store_thm("th51", el 51 goals |> concl, 555 conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO even_nil) 556 \\ MATCH_ACCEPT_TAC even_cons); 557 558val map_none = hd(amatch``Data_Option_map _ Data_Option_none = _``) 559val map_some = hd(amatch``Data_Option_map _ (Data_Option_some _) = _``) 560 561val th52 = store_thm("th52", el 52 goals |> concl, 562 conj_tac >- MATCH_ACCEPT_TAC map_some 563 \\ MATCH_ACCEPT_TAC map_none); 564 565val filter_nil = hd(amatch``Data_List_filter _ Data_List_nil``) 566val filter_cons = hd(amatch``Data_List_filter _ (Data_List_cons _ _)``) 567 568val th53 = store_thm("th53", el 53 goals |> concl, 569 conj_tac >- MATCH_ACCEPT_TAC filter_nil 570 \\ MATCH_ACCEPT_TAC filter_cons); 571 572val any_nil = hd(amatch``Data_List_any _ Data_List_nil``) 573val any_cons = hd(amatch``Data_List_any _ (Data_List_cons _ _)``) 574 575val th54 = store_thm("th54", el 54 goals |> concl, 576 conj_tac >- MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL any_nil)) 577 \\ MATCH_ACCEPT_TAC any_cons) 578 579val all_nil = hd(amatch``Data_List_all _ Data_List_nil``) 580val all_cons = hd(amatch``Data_List_all _ (Data_List_cons _ _)``) 581 582val th55 = store_thm("th55", el 55 goals |> concl, 583 conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO (SPEC_ALL all_nil)) 584 \\ MATCH_ACCEPT_TAC all_cons) 585 586val map_nil = hd(amatch``Data_List_map _ Data_List_nil``) 587val map_cons = hd(amatch``Data_List_map _ (Data_List_cons _ _)``) 588 589val th56 = store_thm("th56", el 56 goals |> concl, 590 conj_tac >- MATCH_ACCEPT_TAC map_nil 591 \\ MATCH_ACCEPT_TAC map_cons) 592 593val append_nil = hd(amatch``Data_List_append Data_List_nil``) 594val append_cons = hd(amatch``Data_List_append (Data_List_cons _ _) _ = Data_List_cons _ (_ _ _)``) 595 596val th57 = store_thm("th57", el 57 goals |> concl, 597 conj_tac >- MATCH_ACCEPT_TAC append_nil 598 \\ MATCH_ACCEPT_TAC append_cons) 599 600val power_zero = hd(amatch``Number_Natural_power _ Number_Natural_zero``) 601val power_suc = hd(amatch``Number_Natural_power _ (Number_Natural_suc _)``) 602 603val th58 = store_thm("th58", el 58 goals |> concl, 604 conj_tac >- MATCH_ACCEPT_TAC power_zero 605 \\ MATCH_ACCEPT_TAC power_suc) 606 607val times_comm = hd(amatch``Number_Natural_times x y = Number_Natural_times y x``) 608val plus_comm = hd(amatch``Number_Natural_plus x y = Number_Natural_plus y x``) 609val times_zero = hd(amatch``Number_Natural_times _ Number_Natural_zero``) 610val times_suc = hd(amatch``Number_Natural_times _ (Number_Natural_suc _)``) 611val times_zero_comm = PURE_ONCE_REWRITE_RULE[times_comm]times_zero 612 613val th59 = store_thm("th59", el 59 goals |> concl, 614 conj_tac >- MATCH_ACCEPT_TAC times_zero_comm 615 \\ MATCH_ACCEPT_TAC 616 (PURE_ONCE_REWRITE_RULE[plus_comm](PURE_ONCE_REWRITE_RULE[times_comm]times_suc))) 617 618val plus_zero = hd(amatch``Number_Natural_plus _ Number_Natural_zero``) 619val plus_suc = hd(amatch``Number_Natural_plus _ (Number_Natural_suc _)``) 620 621val th60 = store_thm("th60", el 60 goals |> concl, 622 conj_tac >- MATCH_ACCEPT_TAC (PURE_ONCE_REWRITE_RULE[plus_comm]plus_zero) 623 \\ MATCH_ACCEPT_TAC (PURE_ONCE_REWRITE_RULE[plus_comm]plus_suc)) 624 625val th61 = store_thm("th61", el 61 goals |> concl, 626 PURE_REWRITE_TAC[not_not,iff_F,iff_T,truth,not_F,and_T] 627 \\ gen_tac \\ REFL_TAC) 628 629val isSome_some = hd(amatch``Data_Option_isSome (Data_Option_some _)``) 630val isSome_none = hd(amatch``Data_Option_isSome (Data_Option_none)``) 631 632val th62 = store_thm("th62", el 62 goals |> concl, 633 conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO (SPEC_ALL isSome_some)) 634 \\ MATCH_ACCEPT_TAC (EQF_INTRO isSome_none)) 635 636val isNone_some = hd(amatch``Data_Option_isNone (Data_Option_some _)``) 637val isNone_none = hd(amatch``Data_Option_isNone (Data_Option_none)``) 638 639val th63 = store_thm("th63", el 63 goals |> concl, 640 conj_tac >- MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL isNone_some)) 641 \\ MATCH_ACCEPT_TAC (EQT_INTRO isNone_none)) 642 643val isRight_right = hd(amatch``Data_Sum_isRight (Data_Sum_right _)``) 644val isRight_left = hd(amatch``Data_Sum_isRight (Data_Sum_left _)``) 645 646val th64 = store_thm("th64", el 64 goals |> concl, 647 conj_tac >- MATCH_ACCEPT_TAC isRight_right 648 \\ MATCH_ACCEPT_TAC isRight_left) 649 650val isLeft_right = hd(amatch``Data_Sum_isLeft (Data_Sum_right _)``) 651val isLeft_left = hd(amatch``Data_Sum_isLeft (Data_Sum_left _)``) 652 653val th65 = store_thm("th65", el 65 goals |> concl, 654 conj_tac >- MATCH_ACCEPT_TAC isLeft_left 655 \\ MATCH_ACCEPT_TAC isLeft_right) 656 657val th66 = store_thm("th66", el 66 goals |> concl, 658 rpt strip_tac 659 \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th)) 660 \\ qexists_tac`x` 661 \\ first_assum ACCEPT_TAC); 662 663val th67 = store_thm("th67", el 67 goals |> concl, 664 rpt strip_tac 665 \\ first_x_assum match_mp_tac 666 \\ first_x_assum(qspec_then`x`ACCEPT_TAC)); 667 668val th68 = store_thm("th68", el 68 goals |> concl, 669 rpt strip_tac 670 \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th)) 671 \\ TRY (disj1_tac >> first_assum ACCEPT_TAC) 672 \\ TRY (disj2_tac >> first_assum ACCEPT_TAC)) 673 674val th69 = store_thm("th69", el 69 goals |> concl, 675 rpt strip_tac 676 \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th)) 677 \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th)) 678 \\ first_assum ACCEPT_TAC); 679 680val th70 = store_thm("th70", el 70 goals |> concl, 681 PURE_REWRITE_TAC[imp_F] 682 \\ disch_then ACCEPT_TAC) 683 684val th71 = store_thm("th71", el 71 goals |> concl, 685 PURE_REWRITE_TAC[not_or] 686 \\ strip_tac) 687 688val th72 = store_thm("th72", el 72 goals |> concl, 689 PURE_REWRITE_TAC[not_or] 690 \\ strip_tac) 691 692val not_imp = hd(amatch``~(_ ==> _)``) 693 694val th73 = store_thm("th73", el 73 goals |> concl, 695 PURE_REWRITE_TAC[not_imp] 696 \\ strip_tac) 697 698val th74 = store_thm("th74", el 74 goals |> concl, 699 PURE_REWRITE_TAC[not_imp] 700 \\ strip_tac) 701 702val th75 = store_thm("th75", el 75 goals |> concl, 703 PURE_REWRITE_TAC[not_not] 704 \\ strip_tac) 705 706val tc_def = hd(amatch``!x. Relation_transitiveClosure x = _``) 707 708val bigIntersect_thm = hd(amatch``Relation_bigIntersect a b c <=> _``) 709 710val mem_fromPred = hd(amatch``Set_member r (Set_fromPredicate _)``) 711 712val subrelation_thm = hd(amatch``Relation_subrelation x s <=> !x y. _``) 713 714val transitive_thm = hd(amatch``Relation_transitive s <=> _``) 715 716val th76 = store_thm("th76", el 76 goals |> concl, 717 PURE_REWRITE_TAC[GSYM fun_eq_thm] 718 \\ PURE_REWRITE_TAC[tc_def,bigIntersect_thm,mem_fromPred] 719 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 720 \\ Ho_Rewrite.PURE_REWRITE_TAC[ex_imp] 721 \\ PURE_REWRITE_TAC[subrelation_thm,transitive_thm] 722 \\ PURE_ONCE_REWRITE_TAC[GSYM and_imp_intro] 723 \\ Ho_Rewrite.PURE_REWRITE_TAC[forall_eq2] 724 \\ rpt gen_tac 725 \\ PURE_REWRITE_TAC[GSYM and_imp_intro] 726 \\ REFL_TAC) 727 728val wellFounded_thm = hd(amatch``Relation_wellFounded r <=> !p. (?x. _) ==> _``) 729 730val th77 = store_thm("th77", el 77 goals |> concl, 731 PURE_REWRITE_TAC[GSYM fun_eq_thm] 732 \\ PURE_REWRITE_TAC[wellFounded_thm] 733 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 734 \\ gen_tac \\ REFL_TAC) 735 736val less_thm = hd(amatch``Number_Natural_less _ _ <=> ?x. _``) 737val less_refl = hd(amatch``Number_Natural_less x x``) 738val less_zero = hd(amatch``~(Number_Natural_less _ (Number_Natural_zero))``) 739val less_suc_suc = hd(amatch``Number_Natural_less (Number_Natural_suc _) b``) 740 741val less_suc = hd(amatch``Number_Natural_less n (Number_Natural_suc n)``) 742val less_trans = hd(amatch``Number_Natural_less x y /\ Number_Natural_less y z ==> _``) 743 744val num_cases = hd(amatch``(n = Number_Natural_zero) \/ ?n. _``) 745 746val num_ind = hd(amatch``_ ==> !n. P (n:Number_Natural_natural)``) 747 748val num_less_ind = hd(amatch``(!x. _ ==> _) ==> !n. P (n:Number_Natural_natural)``) 749 750val not_less = hd(amatch``~(Number_Natural_less _ _) <=> _``) 751 752val less_lesseq = hd(amatch``Number_Natural_less m (Number_Natural_suc n) <=> Number_Natural_lesseq m n``) 753 754val less_or_eq = hd(amatch``Number_Natural_lesseq _ _ <=> (Number_Natural_less _ _) \/ _``) 755 756val trichotomy = hd(amatch``_ \/ _ \/ (_ = _)``) 757 758val th78 = store_thm("th78", el 78 goals |> concl, 759 PURE_REWRITE_TAC[GSYM fun_eq_thm] 760 \\ qx_genl_tac[`a`,`b`] 761 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 762 \\ match_mp_tac (PURE_REWRITE_RULE[and_imp_intro]th20) 763 \\ conj_tac \\ strip_tac 764 >- ( 765 qexists_tac`\x. Number_Natural_less x b` 766 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 767 \\ reverse conj_tac 768 >- ( 769 conj_tac >- (first_assum ACCEPT_TAC) 770 \\ MATCH_ACCEPT_TAC less_refl ) 771 \\ gen_tac 772 \\ Q.ISPEC_THEN`b`FULL_STRUCT_CASES_TAC num_cases 773 >- ( 774 PURE_REWRITE_TAC[EQF_INTRO (SPEC_ALL less_zero)] 775 \\ disch_then ACCEPT_TAC) 776 \\ PURE_REWRITE_TAC[less_suc_suc] 777 \\ strip_tac 778 \\ match_mp_tac less_trans 779 \\ qexists_tac`n'` 780 \\ conj_tac >- (first_assum ACCEPT_TAC) 781 \\ MATCH_ACCEPT_TAC less_suc ) 782 \\ `!n. Number_Natural_less n a ==> P n` 783 by ( 784 qpat_x_assum`P a`mp_tac 785 \\ qid_spec_tac`a` 786 \\ ho_match_mp_tac num_ind 787 \\ conj_tac 788 >- ( 789 PURE_REWRITE_TAC[EQF_INTRO (SPEC_ALL less_zero)] 790 \\ ntac 2 strip_tac 791 \\ CONV_TAC(REWR_CONV F_imp)) 792 \\ rpt strip_tac 793 \\ `P a` by (first_x_assum(fn th => (first_x_assum match_mp_tac \\ first_assum ACCEPT_TAC))) 794 \\ `!n. Number_Natural_less n a ==> P n` by (first_x_assum match_mp_tac \\ first_assum ACCEPT_TAC) 795 \\ first_x_assum(assume_tac o CONV_RULE(REWR_CONV less_lesseq)) 796 \\ first_x_assum(strip_assume_tac o CONV_RULE(REWR_CONV less_or_eq)) 797 >- ( 798 first_x_assum match_mp_tac 799 \\ first_assum ACCEPT_TAC) 800 \\ VAR_EQ_TAC 801 \\ first_assum ACCEPT_TAC ) 802 \\ qspecl_then[`a`,`b`]strip_assume_tac trichotomy 803 >- ( 804 qspec_then`Number_Natural_less a b`(match_mp_tac o EQT_ELIM) F_imp 805 \\ qspec_then`~(P b)`(match_mp_tac o UNDISCH) th42 806 \\ PURE_REWRITE_TAC[not_not] 807 \\ first_x_assum match_mp_tac 808 \\ first_assum ACCEPT_TAC ) 809 \\ VAR_EQ_TAC 810 \\ first_x_assum(assume_tac o EQF_INTRO) 811 \\ first_x_assum(fn th => (first_x_assum(mp_tac o EQ_MP th))) 812 \\ PURE_REWRITE_TAC[F_imp]) 813 814val th79 = store_thm("th79", el 79 goals |> concl, 815 PURE_REWRITE_TAC[GSYM fun_eq_thm,transitive_thm] 816 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 817 \\ gen_tac \\ REFL_TAC) 818 819val th80 = store_thm("th80", el 80 goals |> concl, 820 PURE_REWRITE_TAC[GSYM fun_eq_thm,subrelation_thm] 821 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 822 \\ rpt gen_tac \\ REFL_TAC) 823 824val union_thm = hd(amatch``Relation_union r s = _``) 825val fromSet_thm = hd(amatch``Relation_fromSet _ _ _``) 826val mem_union = hd(amatch``Set_member _ (Set_union _ _) <=> _``) 827val mem_toSet = hd(amatch``Set_member _ (Relation_toSet _)``) 828 829val th81 = store_thm("th81", el 81 goals |> concl, 830 PURE_REWRITE_TAC[GSYM fun_eq_thm,union_thm,fromSet_thm,mem_union,mem_toSet] 831 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 832 \\ rpt gen_tac \\ REFL_TAC) 833 834val intersect_thm = hd(amatch``Relation_intersect x y = _``) 835 836val mem_inter = hd(amatch``Set_member _ (Set_intersect _ _)``) 837 838val th82 = store_thm("th82", el 82 goals |> concl, 839 PURE_REWRITE_TAC[GSYM fun_eq_thm,intersect_thm,fromSet_thm,mem_inter,mem_toSet] 840 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 841 \\ rpt gen_tac \\ REFL_TAC) 842 843val greatereq_thm = hd(amatch``Number_Natural_greatereq _ _``) 844val greater_thm = hd(amatch``Number_Natural_greater _ _ = _``) 845 846val th83 = store_thm("th83", el 83 goals |> concl, 847 PURE_REWRITE_TAC[GSYM fun_eq_thm,greatereq_thm,less_or_eq,greater_thm] 848 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 849 \\ rpt gen_tac 850 \\ CONV_TAC(RAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) 851 \\ REFL_TAC) 852 853val th84 = store_thm("th84", el 84 goals |> concl, 854 PURE_REWRITE_TAC[GSYM fun_eq_thm,less_or_eq] 855 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 856 \\ rpt gen_tac \\ REFL_TAC) 857 858val th85 = store_thm("th85", el 85 goals |> concl, 859 MATCH_ACCEPT_TAC ex_unique_thm) 860 861val th86 = store_thm("th86", el 86 goals |> concl, 862 Q.ISPEC_THEN`A`FULL_STRUCT_CASES_TAC bool_cases 863 \\ PURE_REWRITE_TAC[not_or,imp_F,not_and,not_not,T_or,not_T,F_imp,F_or,T_imp] 864 \\ REFL_TAC) 865 866val th87 = store_thm("th87", el 87 goals |> concl, 867 Q.ISPEC_THEN`A`FULL_STRUCT_CASES_TAC bool_cases 868 \\ PURE_REWRITE_TAC[not_or,imp_F,not_and,not_not,T_or,not_T,F_imp,F_or,T_imp,not_F] 869 \\ REFL_TAC) 870 871val th88 = store_thm("th88", el 88 goals |> concl, 872 Q.ISPEC_THEN`q`FULL_STRUCT_CASES_TAC bool_cases 873 \\ PURE_REWRITE_TAC[if_T,T_or,not_T,or_T,or_F,T_and,F_or,and_T] 874 \\ Q.ISPEC_THEN`p`FULL_STRUCT_CASES_TAC bool_cases 875 \\ PURE_REWRITE_TAC[T_iff,T_or,not_T,or_F,T_and,F_iff,F_or,not_F,if_F,or_T,and_T] 876 \\ TRY REFL_TAC 877 \\ Q.ISPEC_THEN`r`FULL_STRUCT_CASES_TAC bool_cases 878 \\ PURE_REWRITE_TAC[not_T,F_or,F_and,not_F,T_or,T_and,and_T,and_i] 879 \\ REFL_TAC) 880 881val th89 = store_thm("th89", el 89 goals |> concl, 882 Q.ISPEC_THEN`p`FULL_STRUCT_CASES_TAC bool_cases 883 \\ PURE_REWRITE_TAC[T_iff,T_or,not_T,or_F,T_and,F_iff,F_or,not_F,or_T,and_T] 884 \\ Q.ISPEC_THEN`q`FULL_STRUCT_CASES_TAC bool_cases 885 \\ PURE_REWRITE_TAC[T_iff,T_or,not_T,or_F,T_and,F_iff,F_or,not_F,or_T,and_T,not_not] 886 \\ REFL_TAC) 887 888val th90 = store_thm("th90", el 90 goals |> concl, 889 Q.ISPEC_THEN`p`FULL_STRUCT_CASES_TAC bool_cases 890 \\ PURE_REWRITE_TAC[T_iff,T_or,not_T,or_F,T_and,F_iff,F_or,not_F,or_T,and_T,not_and] 891 \\ REFL_TAC) 892 893val th91 = store_thm("th91", el 91 goals |> concl, 894 Q.ISPEC_THEN`p`FULL_STRUCT_CASES_TAC bool_cases 895 \\ PURE_REWRITE_TAC[T_iff,T_or,not_T,or_F,T_and,F_iff,F_or,not_F,or_T,and_T,not_and,not_or] 896 \\ REFL_TAC) 897 898val th92 = store_thm("th92", el 92 goals |> concl, 899 Q.ISPEC_THEN`p`FULL_STRUCT_CASES_TAC bool_cases 900 \\ PURE_REWRITE_TAC[T_iff,T_or,not_T,or_F,T_and,F_iff,F_or,not_F,or_T,and_T,not_imp] 901 \\ TRY REFL_TAC 902 \\ Q.ISPEC_THEN`q`FULL_STRUCT_CASES_TAC bool_cases 903 \\ PURE_REWRITE_TAC[T_imp,not_T,F_imp,not_F,F_or,T_or] 904 \\ REFL_TAC) 905 906val th93 = store_thm("th93", el 93 goals |> concl, 907 Q.ISPEC_THEN`p`FULL_STRUCT_CASES_TAC bool_cases 908 \\ PURE_REWRITE_TAC[T_iff,T_or,not_T,or_F,T_and,F_iff,F_or,not_F,or_T,and_T,not_not] 909 \\ REFL_TAC) 910 911val comma_11 = hd(amatch``Data_Pair_comma _ _ = Data_Pair_comma _ _``) 912 913val th94 = store_thm("th94", el 94 goals |> concl, 914 MATCH_ACCEPT_TAC comma_11) 915 916val right_11 = hd(amatch``Data_Sum_right _ = Data_Sum_right _``) 917 918val th95 = store_thm("th95", el 95 goals |> concl, 919 MATCH_ACCEPT_TAC right_11) 920 921val left_11 = hd(amatch``Data_Sum_left _ = Data_Sum_left _``) 922 923val th96 = store_thm("th96", el 96 goals |> concl, 924 MATCH_ACCEPT_TAC left_11) 925 926val min_thm = hd(amatch``Number_Natural_min _ _ = COND _ _ _``) 927 928val if_id = hd(amatch``if _ then x else x``) 929 930val th97 = store_thm("th97", el 97 goals |> concl, 931 PURE_REWRITE_TAC[GSYM fun_eq_thm,min_thm,less_or_eq] 932 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 933 \\ rpt gen_tac 934 \\ qspec_then`x = x'`strip_assume_tac bool_cases 935 \\ first_assum SUBST1_TAC 936 \\ PURE_REWRITE_TAC[or_F,or_T,if_T] 937 \\ TRY REFL_TAC 938 \\ pop_assum(SUBST1_TAC o EQT_ELIM) 939 \\ PURE_REWRITE_TAC[if_id] 940 \\ REFL_TAC) 941 942val max_thm = hd(amatch``Number_Natural_max _ _ = COND _ _ _``) 943 944val th98 = store_thm("th98", el 98 goals |> concl, 945 PURE_REWRITE_TAC[GSYM fun_eq_thm,max_thm,less_or_eq] 946 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 947 \\ rpt gen_tac 948 \\ qspec_then`x = x'`strip_assume_tac bool_cases 949 \\ first_assum SUBST1_TAC 950 \\ PURE_REWRITE_TAC[or_F,or_T,if_T] 951 \\ TRY REFL_TAC 952 \\ pop_assum(SUBST1_TAC o EQT_ELIM) 953 \\ PURE_REWRITE_TAC[if_id] 954 \\ REFL_TAC) 955 956val bit1_thm = hd(amatch``Number_Natural_bit1 _ = _``) 957val bit0_suc = hd(amatch``Number_Natural_bit0 _ = _ _``) 958val bit0_zero = hd(amatch``Number_Natural_bit0 Number_Natural_zero``) 959val plus_zero = hd(amatch``Number_Natural_plus Number_Natural_zero _``) 960val plus_suc = hd(amatch``Number_Natural_plus _ (Number_Natural_suc _)``) 961val plus_suc1 = hd(amatch``Number_Natural_plus (Number_Natural_suc _) _``) 962 963val th99 = store_thm("th99", el 99 goals |> concl, 964 PURE_REWRITE_TAC[GSYM fun_eq_thm,bit1_thm,plus_suc] 965 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 966 \\ gen_tac 967 \\ AP_TERM_TAC 968 \\ qid_spec_tac`x` 969 \\ ho_match_mp_tac num_ind 970 \\ PURE_REWRITE_TAC[bit0_zero,bit0_suc,plus_zero,plus_suc1] 971 \\ conj_tac >- REFL_TAC 972 \\ gen_tac 973 \\ disch_then SUBST_ALL_TAC 974 \\ PURE_REWRITE_TAC[plus_suc] 975 \\ REFL_TAC) 976 977val irreflexive_thm = hd(amatch``Relation_irreflexive _ = _``) 978 979val th100 = store_thm("th100", el 100 goals |> concl, 980 PURE_REWRITE_TAC[GSYM fun_eq_thm, irreflexive_thm] 981 \\ CONV_TAC (DEPTH_CONV BETA_CONV) 982 \\ rpt gen_tac 983 \\ REFL_TAC) 984 985val reflexive_thm = hd(amatch``Relation_reflexive _ = _``) 986 987val th101 = store_thm("th101", el 101 goals |> concl, 988 PURE_REWRITE_TAC[GSYM fun_eq_thm, reflexive_thm] 989 \\ CONV_TAC (DEPTH_CONV BETA_CONV) 990 \\ rpt gen_tac \\ REFL_TAC) 991 992val o_thm = hd(amatch``(Function_o _ _) _ = _``) 993 994val th102 = store_thm("th102", el 102 goals |> concl, 995 PURE_REWRITE_TAC[GSYM fun_eq_thm,o_thm] 996 \\ CONV_TAC (DEPTH_CONV BETA_CONV) 997 \\ rpt gen_tac \\ REFL_TAC) 998 999val th103 = store_thm("th103", el 103 goals |> concl, 1000 PURE_REWRITE_TAC[GSYM fun_eq_thm,greater_thm] 1001 \\ CONV_TAC (DEPTH_CONV BETA_CONV) 1002 \\ rpt gen_tac \\ REFL_TAC) 1003 1004val skk = hd(amatch``Function_Combinator_s _ _ = Function_id``) 1005 1006val th104 = store_thm("th104", el 104 goals |> concl, 1007 PURE_REWRITE_TAC[skk] \\ REFL_TAC) 1008 1009val one_thm = hd(amatch``_ = Data_Unit_unit``) 1010 1011val th105 = store_thm("th105", el 105 goals |> concl, 1012 PURE_ONCE_REWRITE_TAC[one_thm] \\ REFL_TAC) 1013 1014val universe_thm = hd(amatch``Relation_universe _ _``) 1015 1016val th106 = store_thm("th106", el 106 goals |> concl, 1017 PURE_REWRITE_TAC[GSYM fun_eq_thm,EQT_INTRO(SPEC_ALL universe_thm)] 1018 \\ CONV_TAC (DEPTH_CONV BETA_CONV) 1019 \\ rpt gen_tac \\ REFL_TAC) 1020 1021val empty_thm = hd(amatch``Relation_empty _ _``) 1022 1023val th107 = store_thm("th107", el 107 goals |> concl, 1024 PURE_REWRITE_TAC[GSYM fun_eq_thm,EQF_INTRO (SPEC_ALL empty_thm)] 1025 \\ CONV_TAC (DEPTH_CONV BETA_CONV) 1026 \\ rpt gen_tac \\ REFL_TAC) 1027 1028val th108 = store_thm("th108", el 108 goals |> concl, 1029 REFL_TAC) 1030 1031(* other theorems from boolTheory *) 1032 1033val MONO_IMP = store_thm("MONO_IMP", concl boolTheory.MONO_IMP, 1034 rpt strip_tac 1035 \\ rpt(first_x_assum match_mp_tac) 1036 \\ first_x_assum ACCEPT_TAC); 1037 1038val IMP_DISJ_THM = store_thm("IMP_DISJ_THM", concl boolTheory.IMP_DISJ_THM, 1039 rpt gen_tac 1040 \\ qspec_then`A`FULL_STRUCT_CASES_TAC bool_cases 1041 \\ PURE_REWRITE_TAC[T_imp,not_T,F_imp,not_F,F_or,T_or] 1042 \\ REFL_TAC) 1043 1044val LET_CONG = store_thm("LET_CONG", concl boolTheory.LET_CONG, 1045 rpt strip_tac 1046 \\ VAR_EQ_TAC 1047 \\ PURE_REWRITE_TAC[LET_DEF] 1048 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 1049 \\ first_x_assum match_mp_tac 1050 \\ REFL_TAC) 1051 1052val LET_RAND = store_thm("LET_RAND", concl boolTheory.LET_RAND, 1053 PURE_REWRITE_TAC[LET_DEF] 1054 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 1055 \\ REFL_TAC) 1056 1057val BOOL_EQ_DISTINCT = store_thm("BOOL_EQ_DISTINCT", concl boolTheory.BOOL_EQ_DISTINCT, 1058 PURE_REWRITE_TAC[iff_F,not_not,iff_T,not_F,and_T]); 1059 1060val bool_case_thm = store_thm("bool_case_thm", concl boolTheory.bool_case_thm, 1061 PURE_REWRITE_TAC[th17] 1062 \\ conj_tac \\ rpt gen_tac \\ REFL_TAC); 1063 1064val forall_bool = hd(amatch``(!b:bool. P b) <=> _``) 1065val FORALL_BOOL = store_thm("FORALL_BOOL", concl boolTheory.FORALL_BOOL, 1066 MATCH_ACCEPT_TAC forall_bool); 1067 1068val exists_refl = hd(amatch ``?x. x = a``) 1069 1070val itself_tydef = prim_type_definition({Thy="prove_base_assums",Tyop="itself"}, 1071 SPEC boolSyntax.arb exists_refl |> CONV_RULE(QUANT_CONV SYM_CONV)) 1072 1073val _ = Parse.hide"the_value" 1074val the_value_def = new_definition("the_value_def",``the_value = (ARB:'a itself)``) 1075 1076val itself_unique = Q.store_thm("itself_unique", 1077 `!i. i = the_value`, 1078 CHOOSE_TAC itself_tydef 1079 \\ pop_assum mp_tac 1080 \\ PURE_REWRITE_TAC[TYPE_DEFINITION] 1081 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 1082 \\ strip_tac 1083 \\ gen_tac 1084 \\ first_assum(qspec_then`rep the_value`(mp_tac o #2 o EQ_IMP_RULE)) 1085 \\ impl_tac >- (qexists_tac`the_value` \\ REFL_TAC) 1086 \\ first_assum(qspec_then`rep i`(mp_tac o #2 o EQ_IMP_RULE)) 1087 \\ impl_tac >- (qexists_tac`i` \\ REFL_TAC) 1088 \\ disch_then(fn th => PURE_REWRITE_TAC[th]) 1089 \\ first_x_assum MATCH_ACCEPT_TAC); 1090 1091val itself_induction = store_thm("itself_induction", 1092 ``!P. P the_value ==> !i. P i``, 1093 rpt strip_tac 1094 \\ PURE_ONCE_REWRITE_TAC[itself_unique] 1095 \\ first_assum ACCEPT_TAC); 1096 1097val itself_Axiom = store_thm("itself_Axiom", ``!e. ?f. f the_value = e``, 1098 gen_tac 1099 \\ qexists_tac`\x. e` 1100 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 1101 \\ REFL_TAC); 1102 1103val RES_FORALL_DEF = new_definition("RES_FORALL_DEF",concl boolTheory.RES_FORALL_DEF); 1104val RES_EXISTS_DEF = new_definition("RES_EXISTS_DEF",concl boolTheory.RES_EXISTS_DEF); 1105val RES_EXISTS_UNIQUE_DEF = new_definition("RES_EXISTS_UNIQUE_DEF", 1106 concl boolTheory.RES_EXISTS_UNIQUE_DEF 1107 |> Term.subst [boolSyntax.res_exists_tm |-> lhs(concl RES_EXISTS_DEF), 1108 boolSyntax.res_forall_tm |-> lhs(concl RES_FORALL_DEF)]); 1109val RES_SELECT_DEF = new_definition("RES_SELECT_DEF",concl boolTheory.RES_SELECT_DEF); 1110 1111val RES_FORALL_THM = store_thm("RES_FORALL_THM", 1112 Term.subst [boolSyntax.res_forall_tm |-> lhs(concl RES_FORALL_DEF)] 1113 (concl RES_FORALL_THM), 1114 PURE_REWRITE_TAC[RES_FORALL_DEF] 1115 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 1116 \\ rpt gen_tac \\ REFL_TAC); 1117 1118val RES_EXISTS_THM = store_thm("RES_EXISTS_THM", 1119 Term.subst [boolSyntax.res_exists_tm |-> lhs(concl RES_EXISTS_DEF)] 1120 (concl RES_EXISTS_THM), 1121 PURE_REWRITE_TAC[RES_EXISTS_DEF] 1122 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 1123 \\ rpt gen_tac \\ REFL_TAC); 1124 1125val RES_SELECT_THM = store_thm("RES_SELECT_THM", 1126 Term.subst [boolSyntax.res_select_tm |-> lhs(concl RES_SELECT_DEF)] 1127 (concl RES_SELECT_THM), 1128 PURE_REWRITE_TAC[RES_SELECT_DEF] 1129 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 1130 \\ rpt gen_tac \\ REFL_TAC); 1131 1132val RES_FORALL_CONG = store_thm("RES_FORALL_CONG", 1133 Term.subst [boolSyntax.res_forall_tm |-> lhs(concl RES_FORALL_DEF)] 1134 (concl RES_FORALL_CONG), 1135 disch_then SUBST_ALL_TAC 1136 \\ PURE_REWRITE_TAC[RES_FORALL_THM] 1137 \\ strip_tac 1138 \\ PURE_REWRITE_TAC[th25] 1139 \\ conj_tac \\ rpt strip_tac 1140 \\ rpt (first_x_assum(qspec_then`x`mp_tac)) 1141 \\ PURE_ASM_REWRITE_TAC[T_imp] 1142 \\ disch_then SUBST_ALL_TAC 1143 \\ disch_then ACCEPT_TAC); 1144 1145val RES_EXISTS_CONG = store_thm("RES_EXISTS_CONG", 1146 Term.subst [boolSyntax.res_exists_tm |-> lhs(concl RES_EXISTS_DEF)] 1147 (concl RES_EXISTS_CONG), 1148 disch_then SUBST_ALL_TAC 1149 \\ PURE_REWRITE_TAC[RES_EXISTS_THM] 1150 \\ strip_tac 1151 \\ PURE_REWRITE_TAC[th25] 1152 \\ conj_tac \\ rpt strip_tac 1153 \\ qexists_tac`x` 1154 \\ rpt (first_x_assum(qspec_then`x`mp_tac)) 1155 \\ PURE_ASM_REWRITE_TAC[T_imp,T_and,iff_T,T_iff] 1156 \\ disch_then ACCEPT_TAC); 1157 1158val RES_EXISTS_UNIQUE_THM = store_thm("RES_EXISTS_UNIQUE_THM", 1159 Term.subst [boolSyntax.res_exists1_tm |-> lhs(concl RES_EXISTS_UNIQUE_DEF), 1160 boolSyntax.res_exists_tm |-> lhs(concl RES_EXISTS_DEF), 1161 boolSyntax.res_forall_tm |-> lhs(concl RES_FORALL_DEF)] 1162 (concl RES_EXISTS_UNIQUE_THM), 1163 PURE_REWRITE_TAC[RES_EXISTS_UNIQUE_DEF] 1164 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 1165 \\ rpt gen_tac \\ REFL_TAC); 1166 1167val RES_ABSTRACT_EXISTS = prove( 1168 let 1169 val fvar = mk_var("f",type_of boolSyntax.res_abstract_tm) 1170 in 1171 mk_exists(fvar, Term.subst [boolSyntax.res_abstract_tm|->fvar] (concl RES_ABSTRACT_DEF)) 1172 end, 1173 qexists_tac`\p m x. if x IN p then m x else ARB x` 1174 \\ PURE_REWRITE_TAC[GSYM fun_eq_thm] 1175 \\ CONV_TAC(DEPTH_CONV BETA_CONV) 1176 \\ conj_tac 1177 >- ( 1178 rpt gen_tac 1179 \\ disch_then (SUBST_ALL_TAC o EQT_INTRO) 1180 \\ PURE_REWRITE_TAC[if_T] 1181 \\ REFL_TAC) 1182 \\ rpt gen_tac \\ strip_tac \\ gen_tac 1183 \\ first_x_assum(qspec_then`x`mp_tac) 1184 \\ Q.SPEC_THEN`x IN p`FULL_STRUCT_CASES_TAC bool_cases 1185 \\ PURE_REWRITE_TAC[if_T,if_F,T_imp] 1186 >- disch_then ACCEPT_TAC 1187 \\ disch_then kall_tac 1188 \\ REFL_TAC); 1189 1190val _ = List.app (Theory.delete_binding o #1) (axioms"-"); 1191val _ = List.app (Theory.delete_binding o #1) (definitions"-"); 1192 1193val RES_ABSTRACT_DEF = new_specification("RES_ABSTRACT_DEF",["RES_ABSTRACT"],RES_ABSTRACT_EXISTS) 1194 1195val _ = export_theory() 1196