1 (* Title: HOL/simpdata.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Instantiation of the generic simplifier for HOL. |
|
7 *) |
|
8 |
|
9 (** tools setup **) |
|
10 |
|
11 structure Quantifier1 = Quantifier1Fun |
|
12 (struct |
|
13 (*abstract syntax*) |
|
14 fun dest_eq ((c as Const("op =",_)) $ s $ t) = SOME (c, s, t) |
|
15 | dest_eq _ = NONE; |
|
16 fun dest_conj ((c as Const("op &",_)) $ s $ t) = SOME (c, s, t) |
|
17 | dest_conj _ = NONE; |
|
18 fun dest_imp ((c as Const("op -->",_)) $ s $ t) = SOME (c, s, t) |
|
19 | dest_imp _ = NONE; |
|
20 val conj = HOLogic.conj |
|
21 val imp = HOLogic.imp |
|
22 (*rules*) |
|
23 val iff_reflection = @{thm eq_reflection} |
|
24 val iffI = @{thm iffI} |
|
25 val iff_trans = @{thm trans} |
|
26 val conjI= @{thm conjI} |
|
27 val conjE= @{thm conjE} |
|
28 val impI = @{thm impI} |
|
29 val mp = @{thm mp} |
|
30 val uncurry = @{thm uncurry} |
|
31 val exI = @{thm exI} |
|
32 val exE = @{thm exE} |
|
33 val iff_allI = @{thm iff_allI} |
|
34 val iff_exI = @{thm iff_exI} |
|
35 val all_comm = @{thm all_comm} |
|
36 val ex_comm = @{thm ex_comm} |
|
37 end); |
|
38 |
|
39 structure Simpdata = |
|
40 struct |
|
41 |
|
42 fun mk_meta_eq r = r RS @{thm eq_reflection}; |
|
43 fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; |
|
44 |
|
45 fun mk_eq th = case concl_of th |
|
46 (*expects Trueprop if not == *) |
|
47 of Const ("==",_) $ _ $ _ => th |
|
48 | _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq th |
|
49 | _ $ (Const ("Not", _) $ _) => th RS @{thm Eq_FalseI} |
|
50 | _ => th RS @{thm Eq_TrueI} |
|
51 |
|
52 fun mk_eq_True r = |
|
53 SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE; |
|
54 |
|
55 (* Produce theorems of the form |
|
56 (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) |
|
57 *) |
|
58 |
|
59 fun lift_meta_eq_to_obj_eq i st = |
|
60 let |
|
61 fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q |
|
62 | count_imp _ = 0; |
|
63 val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1))) |
|
64 in if j = 0 then @{thm meta_eq_to_obj_eq} |
|
65 else |
|
66 let |
|
67 val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); |
|
68 fun mk_simp_implies Q = foldr (fn (R, S) => |
|
69 Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps |
|
70 val aT = TFree ("'a", HOLogic.typeS); |
|
71 val x = Free ("x", aT); |
|
72 val y = Free ("y", aT) |
|
73 in Goal.prove_global (Thm.theory_of_thm st) [] |
|
74 [mk_simp_implies (Logic.mk_equals (x, y))] |
|
75 (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))) |
|
76 (fn {prems, ...} => EVERY |
|
77 [rewrite_goals_tac @{thms simp_implies_def}, |
|
78 REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} :: |
|
79 map (rewrite_rule @{thms simp_implies_def}) prems) 1)]) |
|
80 end |
|
81 end; |
|
82 |
|
83 (*Congruence rules for = (instead of ==)*) |
|
84 fun mk_meta_cong rl = zero_var_indexes |
|
85 (let val rl' = Seq.hd (TRYALL (fn i => fn st => |
|
86 rtac (lift_meta_eq_to_obj_eq i st) i st) rl) |
|
87 in mk_meta_eq rl' handle THM _ => |
|
88 if can Logic.dest_equals (concl_of rl') then rl' |
|
89 else error "Conclusion of congruence rules must be =-equality" |
|
90 end); |
|
91 |
|
92 fun mk_atomize pairs = |
|
93 let |
|
94 fun atoms thm = |
|
95 let |
|
96 fun res th = map (fn rl => th RS rl); (*exception THM*) |
|
97 fun res_fixed rls = |
|
98 if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls |
|
99 else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.thm_context thm) [thm]; |
|
100 in |
|
101 case concl_of thm |
|
102 of Const ("Trueprop", _) $ p => (case head_of p |
|
103 of Const (a, _) => (case AList.lookup (op =) pairs a |
|
104 of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm]) |
|
105 | NONE => [thm]) |
|
106 | _ => [thm]) |
|
107 | _ => [thm] |
|
108 end; |
|
109 in atoms end; |
|
110 |
|
111 fun mksimps pairs = |
|
112 map_filter (try mk_eq) o mk_atomize pairs o gen_all; |
|
113 |
|
114 fun unsafe_solver_tac prems = |
|
115 (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' |
|
116 FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems), atac, |
|
117 etac @{thm FalseE}]; |
|
118 |
|
119 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; |
|
120 |
|
121 |
|
122 (*No premature instantiation of variables during simplification*) |
|
123 fun safe_solver_tac prems = |
|
124 (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' |
|
125 FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems), |
|
126 eq_assume_tac, ematch_tac @{thms FalseE}]; |
|
127 |
|
128 val safe_solver = mk_solver "HOL safe" safe_solver_tac; |
|
129 |
|
130 structure SplitterData = |
|
131 struct |
|
132 structure Simplifier = Simplifier |
|
133 val mk_eq = mk_eq |
|
134 val meta_eq_to_iff = @{thm meta_eq_to_obj_eq} |
|
135 val iffD = @{thm iffD2} |
|
136 val disjE = @{thm disjE} |
|
137 val conjE = @{thm conjE} |
|
138 val exE = @{thm exE} |
|
139 val contrapos = @{thm contrapos_nn} |
|
140 val contrapos2 = @{thm contrapos_pp} |
|
141 val notnotD = @{thm notnotD} |
|
142 end; |
|
143 |
|
144 structure Splitter = SplitterFun(SplitterData); |
|
145 |
|
146 val split_tac = Splitter.split_tac; |
|
147 val split_inside_tac = Splitter.split_inside_tac; |
|
148 |
|
149 val op addsplits = Splitter.addsplits; |
|
150 val op delsplits = Splitter.delsplits; |
|
151 val Addsplits = Splitter.Addsplits; |
|
152 val Delsplits = Splitter.Delsplits; |
|
153 |
|
154 |
|
155 (* integration of simplifier with classical reasoner *) |
|
156 |
|
157 structure Clasimp = ClasimpFun |
|
158 (structure Simplifier = Simplifier and Splitter = Splitter |
|
159 and Classical = Classical and Blast = Blast |
|
160 val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val notE = @{thm notE}); |
|
161 open Clasimp; |
|
162 |
|
163 val _ = ML_Antiquote.value "clasimpset" |
|
164 (Scan.succeed "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"); |
|
165 |
|
166 val mksimps_pairs = |
|
167 [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]), |
|
168 ("All", [@{thm spec}]), ("True", []), ("False", []), |
|
169 ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])]; |
|
170 |
|
171 val HOL_basic_ss = |
|
172 Simplifier.theory_context (the_context ()) empty_ss |
|
173 setsubgoaler asm_simp_tac |
|
174 setSSolver safe_solver |
|
175 setSolver unsafe_solver |
|
176 setmksimps (mksimps mksimps_pairs) |
|
177 setmkeqTrue mk_eq_True |
|
178 setmkcong mk_meta_cong; |
|
179 |
|
180 fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); |
|
181 |
|
182 fun unfold_tac ths = |
|
183 let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths |
|
184 in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end; |
|
185 |
|
186 val defALL_regroup = |
|
187 Simplifier.simproc (the_context ()) |
|
188 "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; |
|
189 |
|
190 val defEX_regroup = |
|
191 Simplifier.simproc (the_context ()) |
|
192 "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; |
|
193 |
|
194 |
|
195 val simpset_simprocs = HOL_basic_ss addsimprocs [defALL_regroup, defEX_regroup] |
|
196 |
|
197 end; |
|
198 |
|
199 structure Splitter = Simpdata.Splitter; |
|
200 structure Clasimp = Simpdata.Clasimp; |
|