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