1(* ===================================================================== *) 2(* FILE : boolLib.sml *) 3(* DESCRIPTION : boolTheory and related support. *) 4(* ===================================================================== *) 5 6structure boolLib = 7struct 8 9open boolTheory boolSyntax Hol_pp ParseExtras 10 Drule Tactical Tactic Thm_cont Conv Rewrite Prim_rec Abbrev DB 11 BoundedRewrites TexTokenMap ThmSetData 12 13local open DefnBase TypeBase Ho_Rewrite Psyntax Rsyntax in end 14 15val parse_from_grammars = Parse.parse_from_grammars; 16 17(* ---------------------------------------------------------------------- 18 Update DefnBase with some extra congruence rules 19 ---------------------------------------------------------------------- *) 20 21val _ = DefnBase.write_congs (DefnBase.read_congs() @ 22 map (REWRITE_RULE [AND_IMP_INTRO]) 23 [RES_FORALL_CONG, RES_EXISTS_CONG]) 24 25(*--------------------------------------------------------------------------- 26 Stock the rewriter in Ho_Rewrite with some rules not yet 27 proved in boolTheory. 28 ---------------------------------------------------------------------------*) 29 30local open HolKernel Ho_Rewrite (* signature control *) 31 structure Parse = 32 struct 33 open Parse 34 val (Type,Term) = parse_from_grammars bool_grammars 35 end 36 open Parse 37in 38(*---------------------------------------------------------------------------*) 39(* The first canjunct is useful when rewriting assumptions, but not when *) 40(* rewriting conclusion, since it prevents stripping. Better rewrite on *) 41(* conclusions is IF_THEN_T_IMP. *) 42(*---------------------------------------------------------------------------*) 43 44val COND_BOOL_CLAUSES = 45 prove(``(!b e. (if b then T else e) = (b \/ e)) /\ 46 (!b t. (if b then t else T) = (b ==> t)) /\ 47 (!b e. (if b then F else e) = (~b /\ e)) /\ 48 (!b t. (if b then t else F) = (b /\ t))``, 49REPEAT (STRIP_TAC ORELSE COND_CASES_TAC ORELSE EQ_TAC) 50 THEN RULE_ASSUM_TAC (REWRITE_RULE[F_DEF]) 51 THEN (ACCEPT_TAC TRUTH ORELSE TRY(FIRST_ASSUM MATCH_ACCEPT_TAC)) 52 THEN ASM_REWRITE_TAC[]); 53 54val _ = Ho_Rewrite.add_implicit_rewrites [COND_BOOL_CLAUSES]; 55 56val IF_THEN_T_IMP = (* better rewrite for RW_TAC *) 57 prove(``!b e. (if b then T else e) = (~b ==> e)``, 58REPEAT (STRIP_TAC ORELSE COND_CASES_TAC ORELSE EQ_TAC) 59 THEN RULE_ASSUM_TAC (REWRITE_RULE[F_DEF]) 60 THEN (ACCEPT_TAC TRUTH ORELSE TRY(FIRST_ASSUM MATCH_ACCEPT_TAC)) 61 THEN ASM_REWRITE_TAC[]); 62 63(* ------------------------------------------------------------------------- *) 64(* Alternative version of unique existence, slated for boolTheory. *) 65(* ------------------------------------------------------------------------- *) 66 67val EXISTS_UNIQUE_ALT = prove( 68(* store_thm( "EXISTS_UNIQUE_ALT", *) 69 ``!P:'a->bool. (?!x. P x) = ?x. !y. P y = (x = y)``, 70 GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_THM] THEN EQ_TAC THENL 71 [DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC ``x:'a``) ASSUME_TAC) THEN 72 EXISTS_TAC ``x:'a`` THEN GEN_TAC THEN EQ_TAC THENL 73 [DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[], 74 DISCH_THEN(SUBST1_TAC o SYM) THEN FIRST_ASSUM MATCH_ACCEPT_TAC], 75 DISCH_THEN(X_CHOOSE_TAC ``x:'a``) THEN 76 ASM_REWRITE_TAC[GSYM EXISTS_REFL] THEN REPEAT GEN_TAC THEN 77 DISCH_THEN(CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN REFL_TAC]);; 78 79 80(* ------------------------------------------------------------------------- *) 81(* NB: this one is true intuitionistically and intensionally. *) 82(* ------------------------------------------------------------------------- *) 83 84val UNIQUE_SKOLEM_ALT = prove 85(* "UNIQUE_SKOLEM_ALT", *) 86 (``!P:'a->'b->bool. (!x. ?!y. P x y) = ?f. !x y. P x y = (f x = y)``, 87 GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_ALT, SKOLEM_THM]); 88 89 90(* ------------------------------------------------------------------------- *) 91(* and this one intuitionistically and extensionally. *) 92(* ------------------------------------------------------------------------- *) 93 94val UNIQUE_SKOLEM_THM = prove 95(* store_thm("UNIQUE_SKOLEM_THM", *) 96(``!P. (!x:'a. ?!y:'b. P x y) = ?!f. !x. P x (f x)``, 97 GEN_TAC 98 THEN REWRITE_TAC[EXISTS_UNIQUE_THM, SKOLEM_THM, FORALL_AND_THM] 99 THEN EQ_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) 100 THEN ASM_REWRITE_TAC[] THENL 101 [REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 102 X_GEN_TAC ``x:'a`` THEN FIRST_ASSUM MATCH_MP_TAC THEN 103 EXISTS_TAC ``x:'a`` THEN ASM_REWRITE_TAC[], 104 MAP_EVERY X_GEN_TAC [``x:'a``, ``y1:'b``, ``y2:'b``] 105 THEN STRIP_TAC THEN 106 FIRST_ASSUM(X_CHOOSE_TAC ``f:'a->'b``) THEN 107 SUBGOAL_THEN ``(\z. if z=x then y1 else (f:'a->'b) z) 108 = (\z. if z=x then y2 else (f:'a->'b) z)`` MP_TAC THENL 109 [FIRST_ASSUM MATCH_MP_TAC THEN 110 REPEAT STRIP_TAC THEN BETA_TAC THEN COND_CASES_TAC THEN 111 ASM_REWRITE_TAC[], 112 DISCH_THEN(MP_TAC o C AP_THM ``x:'a``) THEN REWRITE_TAC[BETA_THM]]]) 113 114 115 116end (* local open *) 117 118val def_suffix = ref "_def" 119 120local 121open Feedback Theory 122fun resolve_storename s = let 123 open Substring 124 val (bracketl,rest) = position "[" (full s) 125in 126 if isEmpty rest then (s,[]) 127 else let 128 val (names,bracketr) = position "]" (slice(rest,1,NONE)) 129 in 130 if size bracketr <> 1 then 131 raise mk_HOL_ERR "boolLib" "resolve_storename" 132 ("Malformed theorem-binding specifier: "^s) 133 else 134 (string bracketl, String.fields (fn c => c = #",") (string names)) 135 end 136end 137in 138fun save_thm_attrs fname (n, attrs, th) = let 139 fun do_attr a = let 140 val storefn = valOf (ThmSetData.data_storefn a) 141 handle Option => raise mk_HOL_ERR "boolLib" fname 142 ("No attribute with name "^a) 143 val exportfn = ThmSetData.data_exportfn a 144 in 145 storefn n; 146 case exportfn of 147 NONE => () 148 | SOME ef => ef (current_theory()) [(n,th)] 149 end 150in 151 Theory.save_thm(n,th) before app do_attr attrs 152end 153fun store_thm(n0,t,tac) = let 154 val (n, attrs) = resolve_storename n0 155 val th = Tactical.prove(t,tac) 156 handle e => (print ("Failed to prove theorem " ^ n ^ ".\n"); 157 Raise e) 158in 159 save_thm_attrs "store_thm" (n,attrs,th) 160end 161fun save_thm(n0,th) = let 162 val (n,attrs) = resolve_storename n0 163in 164 save_thm_attrs "save_thm" (n,attrs,th) 165end 166 167 168(* ---------------------------------------------------------------------- 169 Gets a variant of an arbitrary term instead of a single variable. 170 Besides the resulting term, it returns also the substitution used to 171 get it. 172 ---------------------------------------------------------------------- *) 173 174fun variant_of_term vs t = 175 let 176 open HolKernel 177 val check_vars = free_vars t 178 val (_,sub) = 179 foldl (fn (v, (vs,sub)) => 180 let 181 val v' = variant vs v 182 val vs' = v'::vs 183 val sub' = if (aconv v v') then sub else 184 (v |-> v')::sub 185 in 186 (vs',sub') 187 end) (vs,[]) check_vars 188 val t' = subst sub t 189 in 190 (t', sub) 191 end 192 193end (* local *) 194 195datatype pel = pLeft | pRight | pAbs 196fun term_diff t1 t2 = 197 let 198 open Term HolKernel 199 fun recurse p t1 t2 = 200 if aconv t1 t2 then [] 201 else 202 case (dest_term t1, dest_term t2) of 203 (COMB(f1,x1), COMB (f2,x2)) => 204 if aconv f1 f2 then recurse (pRight :: p) x1 x2 205 else if aconv x1 x2 then recurse (pLeft :: p) f1 f2 206 else recurse (pLeft :: p) f1 f2 @ recurse (pRight :: p) x1 x2 207 | (LAMB(v1,b1), LAMB(v2,b2)) => 208 if aconv v1 v2 then recurse (pAbs :: p) b1 b2 209 else if Type.compare(type_of v1,type_of v2) = EQUAL then 210 let val v1' = variant (free_vars b2) v1 211 in 212 recurse (pAbs :: p) b1 (subst [v2 |-> v1'] b2) 213 end 214 else recurse (pAbs :: p) b1 b2 215 | (CONST _, CONST _) => if same_const t1 t2 then [] 216 else [(List.rev p,t1,t2)] 217 | _ => [(List.rev p,t1,t2)] 218 in 219 recurse [] t1 t2 220 end 221 222fun Teq tm = Term.same_const boolSyntax.T tm 223fun Feq tm = Term.same_const boolSyntax.F tm 224fun tmleq tl1 tl2 = ListPair.allEq op~~ (tl1,tl2) 225fun goaleq (tl1,t1) (tl2,t2) = tmleq tl1 tl2 andalso t1 ~~ t2 226fun goals_eq gl1 gl2 = ListPair.allEq (fn (g1,g2) => goaleq g1 g2) (gl1,gl2) 227val tmem = Lib.op_mem Term.aconv 228val tunion = Lib.op_union Term.aconv 229fun tassoc t l = Lib.op_assoc Term.aconv t l 230 231fun tmx_eq (tm1,x1) (tm2,x2) = x1 = x2 andalso Term.aconv tm1 tm2 232fun xtm_eq (x1,tm1) (x2,tm2) = x1 = x2 andalso Term.aconv tm1 tm2 233fun tmp_eq (tm1,tm2) (tma,tmb) = tm1 ~~ tma andalso tm2 ~~ tmb 234 235 236end; 237