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