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 term_tactic 12 13local open TypeBase Ho_Rewrite Psyntax Rsyntax in end 14 15val parse_from_grammars = Parse.parse_from_grammars; 16 17(*--------------------------------------------------------------------------- 18 Stock the rewriter in Ho_Rewrite with some rules not yet 19 proved in boolTheory. 20 ---------------------------------------------------------------------------*) 21 22local open HolKernel Ho_Rewrite (* signature control *) 23 structure Parse = 24 struct 25 open Parse 26 val (Type,Term) = parse_from_grammars bool_grammars 27 end 28 open Parse 29in 30(*---------------------------------------------------------------------------*) 31(* The first conjunct is useful when rewriting assumptions, but not when *) 32(* rewriting conclusion, since it prevents stripping. Better rewrite on *) 33(* conclusions is IF_THEN_T_IMP. *) 34(*---------------------------------------------------------------------------*) 35 36val COND_BOOL_CLAUSES = 37 prove(``(!b e. (if b then T else e) = (b \/ e)) /\ 38 (!b t. (if b then t else T) = (b ==> t)) /\ 39 (!b e. (if b then F else e) = (~b /\ e)) /\ 40 (!b t. (if b then t else F) = (b /\ t))``, 41REPEAT (STRIP_TAC ORELSE COND_CASES_TAC ORELSE EQ_TAC) 42 THEN RULE_ASSUM_TAC (REWRITE_RULE[F_DEF]) 43 THEN (ACCEPT_TAC TRUTH ORELSE TRY(FIRST_ASSUM MATCH_ACCEPT_TAC)) 44 THEN ASM_REWRITE_TAC[]); 45 46val _ = Ho_Rewrite.add_implicit_rewrites [COND_BOOL_CLAUSES]; 47 48val IF_THEN_T_IMP = (* better rewrite for RW_TAC *) 49 prove(``!b e. (if b then T else e) = (~b ==> e)``, 50REPEAT (STRIP_TAC ORELSE COND_CASES_TAC ORELSE EQ_TAC) 51 THEN RULE_ASSUM_TAC (REWRITE_RULE[F_DEF]) 52 THEN (ACCEPT_TAC TRUTH ORELSE TRY(FIRST_ASSUM MATCH_ACCEPT_TAC)) 53 THEN ASM_REWRITE_TAC[]); 54 55(* ------------------------------------------------------------------------- *) 56(* Alternative version of unique existence, slated for boolTheory. *) 57(* ------------------------------------------------------------------------- *) 58 59val EXISTS_UNIQUE_ALT = prove( 60(* store_thm( "EXISTS_UNIQUE_ALT", *) 61 ``!P:'a->bool. (?!x. P x) = ?x. !y. P y = (x = y)``, 62 GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_THM] THEN EQ_TAC THENL 63 [DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC ``x:'a``) ASSUME_TAC) THEN 64 EXISTS_TAC ``x:'a`` THEN GEN_TAC THEN EQ_TAC THENL 65 [DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[], 66 DISCH_THEN(SUBST1_TAC o SYM) THEN FIRST_ASSUM MATCH_ACCEPT_TAC], 67 DISCH_THEN(X_CHOOSE_TAC ``x:'a``) THEN 68 ASM_REWRITE_TAC[GSYM EXISTS_REFL] THEN REPEAT GEN_TAC THEN 69 DISCH_THEN(CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN REFL_TAC]);; 70 71 72(* ------------------------------------------------------------------------- *) 73(* NB: this one is true intuitionistically and intensionally. *) 74(* ------------------------------------------------------------------------- *) 75 76val UNIQUE_SKOLEM_ALT = prove 77(* "UNIQUE_SKOLEM_ALT", *) 78 (``!P:'a->'b->bool. (!x. ?!y. P x y) = ?f. !x y. P x y = (f x = y)``, 79 GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_ALT, SKOLEM_THM]); 80 81 82(* ------------------------------------------------------------------------- *) 83(* and this one intuitionistically and extensionally. *) 84(* ------------------------------------------------------------------------- *) 85 86val UNIQUE_SKOLEM_THM = prove 87(* store_thm("UNIQUE_SKOLEM_THM", *) 88(``!P. (!x:'a. ?!y:'b. P x y) = ?!f. !x. P x (f x)``, 89 GEN_TAC 90 THEN REWRITE_TAC[EXISTS_UNIQUE_THM, SKOLEM_THM, FORALL_AND_THM] 91 THEN EQ_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) 92 THEN ASM_REWRITE_TAC[] THENL 93 [REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 94 X_GEN_TAC ``x:'a`` THEN FIRST_ASSUM MATCH_MP_TAC THEN 95 EXISTS_TAC ``x:'a`` THEN ASM_REWRITE_TAC[], 96 MAP_EVERY X_GEN_TAC [``x:'a``, ``y1:'b``, ``y2:'b``] 97 THEN STRIP_TAC THEN 98 FIRST_ASSUM(X_CHOOSE_TAC ``f:'a->'b``) THEN 99 SUBGOAL_THEN ``(\z. if z=x then y1 else (f:'a->'b) z) 100 = (\z. if z=x then y2 else (f:'a->'b) z)`` MP_TAC THENL 101 [FIRST_ASSUM MATCH_MP_TAC THEN 102 REPEAT STRIP_TAC THEN BETA_TAC THEN COND_CASES_TAC THEN 103 ASM_REWRITE_TAC[], 104 DISCH_THEN(MP_TAC o C AP_THM ``x:'a``) THEN REWRITE_TAC[BETA_THM]]]) 105 106 107 108end (* local open *) 109 110val def_suffix = ref "_def" 111 112local 113open Feedback Theory 114fun prove_local (n,th) = 115 (if not (!Globals.interactive) then 116 print ("Proved triviality _ \"" ^ String.toString n ^ "\"\n") 117 else (); 118 DB.store_local n th; 119 th) 120in 121fun save_thm_attrs fname (n, attrs, th) = let 122 val (save, attrf, attrs) = let 123 val nonlocal = List.filter (not o Lib.equal "local") attrs 124 in 125 if length nonlocal = length attrs then 126 (Theory.save_thm, ThmAttribute.store_at_attribute, attrs) 127 else 128 (prove_local, ThmAttribute.local_attribute, nonlocal) 129 end 130 fun do_attr a = attrf {thm = th, name = n, attrname = a} 131in 132 save(n,th) before app do_attr attrs 133end 134fun store_thm(n0,t,tac) = let 135 val (n, attrs) = ThmAttribute.extract_attributes n0 136 val th = Tactical.prove(t,tac) 137 handle e => (print ("Failed to prove theorem " ^ n ^ ".\n"); 138 Raise e) 139in 140 save_thm_attrs "store_thm" (n,attrs,th) 141end 142fun save_thm(n0,th) = let 143 val (n,attrs) = ThmAttribute.extract_attributes n0 144in 145 save_thm_attrs "save_thm" (n,attrs,th) 146end 147 148 149(* ---------------------------------------------------------------------- 150 Gets a variant of an arbitrary term instead of a single variable. 151 Besides the resulting term, it returns also the substitution used to 152 get it. 153 ---------------------------------------------------------------------- *) 154 155fun variant_of_term vs t = 156 let 157 open HolKernel 158 val check_vars = free_vars t 159 val (_,sub) = 160 foldl (fn (v, (vs,sub)) => 161 let 162 val v' = variant vs v 163 val vs' = v'::vs 164 val sub' = if (aconv v v') then sub else 165 (v |-> v')::sub 166 in 167 (vs',sub') 168 end) (vs,[]) check_vars 169 val t' = subst sub t 170 in 171 (t', sub) 172 end 173 174end (* local *) 175 176datatype pel = pLeft | pRight | pAbs 177fun term_diff t1 t2 = 178 let 179 open Term HolKernel 180 fun recurse p t1 t2 = 181 if aconv t1 t2 then [] 182 else 183 case (dest_term t1, dest_term t2) of 184 (COMB(f1,x1), COMB (f2,x2)) => 185 if aconv f1 f2 then recurse (pRight :: p) x1 x2 186 else if aconv x1 x2 then recurse (pLeft :: p) f1 f2 187 else recurse (pLeft :: p) f1 f2 @ recurse (pRight :: p) x1 x2 188 | (LAMB(v1,b1), LAMB(v2,b2)) => 189 if aconv v1 v2 then recurse (pAbs :: p) b1 b2 190 else if Type.compare(type_of v1,type_of v2) = EQUAL then 191 let val v1' = variant (free_vars b2) v1 192 in 193 recurse (pAbs :: p) b1 (subst [v2 |-> v1'] b2) 194 end 195 else recurse (pAbs :: p) b1 b2 196 | (CONST _, CONST _) => if same_const t1 t2 then [] 197 else [(List.rev p,t1,t2)] 198 | _ => [(List.rev p,t1,t2)] 199 in 200 recurse [] t1 t2 201 end 202 203 204end; 205