1(* non-interactive mode 2*) 3open HolKernel Parse boolLib; 4val _ = new_theory "extra_bool"; 5 6(* interactive mode 7show_assums := true; 8loadPath := union ["../finished"] (!loadPath); 9app load 10 ["bossLib", "arithmeticTheory", "dividesTheory", "gcdTheory", 11 "primeTheory", "res_quan2Theory", "pred_setTheory", "subtypeTheory", 12 "res_quanTools", "subtypeTools", "ho_proverTools", "numContext", 13 "millerTools", "extra_numTheory", "ho_basicTools", 14 "prob_extraTheory"]; 15installPP subtypeTools.pp_precontext; 16installPP subtypeTools.pp_context; 17*) 18 19open bossLib res_quanTheory pred_setTheory subtypeTheory 20 res_quanTools subtypeTools ho_proverTools HurdUseful 21 ho_basicTools boolContext combinTheory; 22 23infixr 0 ++ << || THENC ORELSEC ORELSER ##; 24infix 1 >>; 25 26val !! = REPEAT; 27val op++ = op THEN; 28val op<< = op THENL; 29val op|| = op ORELSE; 30val op>> = op THEN1; 31 32(* ------------------------------------------------------------------------- *) 33(* Tools. *) 34(* ------------------------------------------------------------------------- *) 35 36val S_TAC = !! (POP_ASSUM MP_TAC) ++ !! RESQ_STRIP_TAC; 37 38val (R_TAC, AR_TAC, R_TAC', AR_TAC') = SIMPLIFY_TACS bool_c; 39 40val Strip = S_TAC; 41val Simplify = R_TAC; 42val Suff = SUFF_TAC; 43val Know = KNOW_TAC; 44 45(* ------------------------------------------------------------------------- *) 46(* Definitions. *) 47(* ------------------------------------------------------------------------- *) 48 49(* ------------------------------------------------------------------------- *) 50(* Theorems. *) 51(* ------------------------------------------------------------------------- *) 52 53val RAND_THM = store_thm 54 ("RAND_THM", 55 ``!f x y. (x = y) ==> (f x = f y)``, 56 RW_TAC std_ss []); 57 58val K_PARTIAL = store_thm 59 ("K_PARTIAL", 60 ``!x. K x = \z. x``, 61 RW_TAC std_ss [K_DEF]); 62 63val SELECT_EXISTS_UNIQUE = store_thm 64 ("SELECT_EXISTS_UNIQUE", 65 ``!P n. $? P /\ (!m. P m ==> (m = n)) ==> ($@ P = n)``, 66 RW_TAC std_ss [boolTheory.EXISTS_DEF]); 67 68val CONJ_EQ_IMP = store_thm 69 ("CONJ_EQ_IMP", 70 ``!a b c. (a ==> (b = c)) ==> (a /\ b = a /\ c)``, 71 PROVE_TAC []); 72 73(* non-interactive mode 74*) 75val _ = export_theory (); 76