1open HolKernel Parse Drule Tactical Tactic Conv Rewrite boolTheory; 2 3val _ = new_theory "ConseqConv"; 4 5 6val forall_eq_thm = store_thm ("forall_eq_thm", 7 ``(!s:'a. (P s = Q s)) ==> ((!s. P s) = (!s. Q s))``, 8 STRIP_TAC THEN ASM_REWRITE_TAC[]); 9 10val exists_eq_thm = store_thm ("exists_eq_thm", 11 ``(!s:'a. (P s = Q s)) ==> ((?s. P s) = (?s. Q s))``, 12 STRIP_TAC THEN ASM_REWRITE_TAC[]); 13 14 15val true_imp = store_thm ("true_imp", ``!t. t ==> T``, REWRITE_TAC[]); 16val false_imp = store_thm ("false_imp", ``!t. F ==> t``, REWRITE_TAC[]); 17 18 19val NOT_CLAUSES_THML = CONJUNCTS NOT_CLAUSES 20Theorem NOT_CLAUSES_X = el 1 NOT_CLAUSES_THML 21Theorem NOT_CLAUSES_T = el 2 NOT_CLAUSES_THML 22Theorem NOT_CLAUSES_F = el 3 NOT_CLAUSES_THML 23 24val IMP_CONG_conj_strengthen = store_thm ("IMP_CONG_conj_strengthen", 25``!x x' y y'. 26 ((y ==> (x' ==> x)) /\ (x' ==> (y' ==> y))) ==> 27 ((x' /\ y') ==> (x /\ y))``, 28Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]); 29 30val IMP_CONG_conj_weaken = store_thm("IMP_CONG_conj_weaken", 31``!x x' y y'. 32 ((y ==> (x ==> x')) /\ (x' ==> (y ==> y'))) ==> 33 ((x /\ y) ==> (x' /\ y'))``, 34Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]); 35 36 37val AND_CLAUSES_THML = 38 (CONJUNCTS (Ho_Rewrite.PURE_REWRITE_RULE [FORALL_AND_THM] AND_CLAUSES)) 39 40Theorem AND_CLAUSES_TX = el 1 AND_CLAUSES_THML; 41Theorem AND_CLAUSES_XT = el 2 AND_CLAUSES_THML; 42Theorem AND_CLAUSES_FX = el 3 AND_CLAUSES_THML; 43Theorem AND_CLAUSES_XF = el 4 AND_CLAUSES_THML; 44Theorem AND_CLAUSES_XX = el 5 AND_CLAUSES_THML; 45 46 47val IMP_CONG_disj_strengthen = store_thm ("IMP_CONG_disj_strengthen", 48``!x x' y y'. 49 ((~y ==> (x' ==> x)) /\ (~x' ==> (y' ==> y))) ==> 50 ((x' \/ y') ==> (x \/ y))``, 51Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]); 52 53 54val IMP_CONG_disj_weaken = store_thm ("IMP_CONG_disj_weaken", 55``!x x' y y'. 56 ((~y ==> (x ==> x')) /\ (~x' ==> (y ==> y'))) ==> 57 ((x \/ y) ==> (x' \/ y'))``, 58Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]); 59 60 61val OR_CLAUSES_THML = 62 (CONJUNCTS (Ho_Rewrite.PURE_REWRITE_RULE [FORALL_AND_THM] OR_CLAUSES)) 63 64val OR_CLAUSES_TX = save_thm ("OR_CLAUSES_TX", el 1 OR_CLAUSES_THML) 65val OR_CLAUSES_XT = save_thm ("OR_CLAUSES_XT", el 2 OR_CLAUSES_THML) 66val OR_CLAUSES_FX = save_thm ("OR_CLAUSES_FX", el 3 OR_CLAUSES_THML) 67val OR_CLAUSES_XF = save_thm ("OR_CLAUSES_XF", el 4 OR_CLAUSES_THML) 68val OR_CLAUSES_XX = save_thm ("OR_CLAUSES_XX", el 5 OR_CLAUSES_THML) 69 70 71 72 73val IMP_CONG_imp_strengthen = store_thm ("IMP_CONG_imp_strengthen", 74``!x x' y y'. 75 ((x ==> (y' ==> y)) /\ (~y' ==> (x ==> x'))) ==> 76 ((x' ==> y') ==> (x ==> y))``, 77 Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]); 78 79val IMP_CONG_imp_weaken = store_thm ("IMP_CONG_imp_weaken", 80``!x x' y y'. 81 ((x ==> (y ==> y')) /\ (~y' ==> (x' ==> x))) ==> 82 ((x ==> y) ==> (x' ==> y'))``, 83 Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]); 84 85 86val IMP_CONG_simple_imp_strengthen = store_thm ("IMP_CONG_simple_imp_strengthen", 87``!x x' y y'. 88 ((x ==> x') /\ (x' ==> (y' ==> y))) ==> 89 ((x' ==> y') ==> (x ==> y))``, 90 Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]); 91 92val IMP_CONG_simple_imp_weaken = store_thm ("IMP_CONG_simple_imp_weaken", 93``!x x' y y'. 94 ((x' ==> x) /\ (x' ==> (y ==> y'))) ==> 95 ((x ==> y) ==> (x' ==> y'))``, 96 Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]); 97 98 99val IMP_CLAUSES_THML = 100 (CONJUNCTS (Ho_Rewrite.PURE_REWRITE_RULE [FORALL_AND_THM] IMP_CLAUSES)) 101 102val IMP_CLAUSES_TX = save_thm ("IMP_CLAUSES_TX", el 1 IMP_CLAUSES_THML) 103val IMP_CLAUSES_XT = save_thm ("IMP_CLAUSES_XT", el 2 IMP_CLAUSES_THML) 104val IMP_CLAUSES_FX = save_thm ("IMP_CLAUSES_FX", el 3 IMP_CLAUSES_THML) 105val IMP_CLAUSES_XX = save_thm ("IMP_CLAUSES_XX", el 4 IMP_CLAUSES_THML) 106val IMP_CLAUSES_XF = save_thm ("IMP_CLAUSES_XF", el 5 IMP_CLAUSES_THML) 107 108 109 110val IMP_CONG_cond_simple = store_thm ("IMP_CONG_cond_simple", 111``!c x x' y y'. 112 ((x' ==> x) /\ (y' ==> y)) ==> 113 ((if c then x' else y') ==> (if c then x else y))``, 114Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]); 115 116val IMP_CONG_cond = store_thm ("IMP_CONG_cond", 117``!c x x' y y'. 118 ((c ==> (x' ==> x)) /\ (~c ==> (y' ==> y))) ==> 119 ((if c then x' else y') ==> (if c then x else y))``, 120Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]); 121 122 123 124val COND_CLAUSES_THML = 125 (CONJUNCTS (Ho_Rewrite.PURE_REWRITE_RULE [FORALL_AND_THM] COND_CLAUSES)) 126fun bool_save_thm (s,t) = store_thm (s, t, Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]) 127 128val COND_CLAUSES_CT = save_thm ("COND_CLAUSES_CT", el 1 COND_CLAUSES_THML) 129val COND_CLAUSES_CF = save_thm ("COND_CLAUSES_CF", el 2 COND_CLAUSES_THML) 130val COND_CLAUSES_ID = save_thm ("COND_CLAUSES_ID", COND_ID) 131val COND_CLAUSES_TT = bool_save_thm ("COND_CLAUSES_TT", 132 ``!c x. (if c then T else x) = (~c ==> x)``) 133val COND_CLAUSES_FT = bool_save_thm ("COND_CLAUSES_FT", 134 ``!c x. (if c then x else T) = (c ==> x)``) 135val COND_CLAUSES_TF = bool_save_thm ("COND_CLAUSES_TF", 136 ``!c x. (if c then F else x) = (~c /\ x)``) 137val COND_CLAUSES_FF = bool_save_thm ("COND_CLAUSES_FF", 138 ``!c x. (if c then x else F) = (c /\ x)``) 139 140 141val ASM_MARKER_DEF = 142 Definition.new_definition 143 ("ASM_MARKER_DEF", Term `ASM_MARKER = (\ (y:bool) x:bool. x)`); 144 145val ASM_MARKER_THM = store_thm ("ASM_MARKER_THM", 146``!y x. ASM_MARKER y x = x``, 147REWRITE_TAC[ASM_MARKER_DEF] THEN 148BETA_TAC THEN REWRITE_TAC []) 149 150 151val _ = export_theory(); 152