4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Instantiation of the generic simplifier for HOL. |
6 Instantiation of the generic simplifier for HOL. |
7 *) |
7 *) |
8 |
8 |
9 (* legacy ML bindings - FIXME get rid of this *) |
9 (** tools setup **) |
10 |
|
11 val Eq_FalseI = thm "Eq_FalseI"; |
|
12 val Eq_TrueI = thm "Eq_TrueI"; |
|
13 val de_Morgan_conj = thm "de_Morgan_conj"; |
|
14 val de_Morgan_disj = thm "de_Morgan_disj"; |
|
15 val iff_conv_conj_imp = thm "iff_conv_conj_imp"; |
|
16 val imp_cong = thm "imp_cong"; |
|
17 val imp_conv_disj = thm "imp_conv_disj"; |
|
18 val imp_disj1 = thm "imp_disj1"; |
|
19 val imp_disj2 = thm "imp_disj2"; |
|
20 val imp_disjL = thm "imp_disjL"; |
|
21 val simp_impliesI = thm "simp_impliesI"; |
|
22 val simp_implies_cong = thm "simp_implies_cong"; |
|
23 val simp_implies_def = thm "simp_implies_def"; |
|
24 |
|
25 local |
|
26 val uncurry = thm "uncurry" |
|
27 val iff_allI = thm "iff_allI" |
|
28 val iff_exI = thm "iff_exI" |
|
29 val all_comm = thm "all_comm" |
|
30 val ex_comm = thm "ex_comm" |
|
31 in |
|
32 |
|
33 (*** make simplification procedures for quantifier elimination ***) |
|
34 |
10 |
35 structure Quantifier1 = Quantifier1Fun |
11 structure Quantifier1 = Quantifier1Fun |
36 (struct |
12 (struct |
37 (*abstract syntax*) |
13 (*abstract syntax*) |
38 fun dest_eq((c as Const("op =",_)) $ s $ t) = SOME(c,s,t) |
14 fun dest_eq ((c as Const("op =",_)) $ s $ t) = SOME (c, s, t) |
39 | dest_eq _ = NONE; |
15 | dest_eq _ = NONE; |
40 fun dest_conj((c as Const("op &",_)) $ s $ t) = SOME(c,s,t) |
16 fun dest_conj ((c as Const("op &",_)) $ s $ t) = SOME (c, s, t) |
41 | dest_conj _ = NONE; |
17 | dest_conj _ = NONE; |
42 fun dest_imp((c as Const("op -->",_)) $ s $ t) = SOME(c,s,t) |
18 fun dest_imp ((c as Const("op -->",_)) $ s $ t) = SOME (c, s, t) |
43 | dest_imp _ = NONE; |
19 | dest_imp _ = NONE; |
44 val conj = HOLogic.conj |
20 val conj = HOLogic.conj |
45 val imp = HOLogic.imp |
21 val imp = HOLogic.imp |
46 (*rules*) |
22 (*rules*) |
47 val iff_reflection = HOL.eq_reflection |
23 val iff_reflection = HOL.eq_reflection |
49 val iff_trans = HOL.trans |
25 val iff_trans = HOL.trans |
50 val conjI= HOL.conjI |
26 val conjI= HOL.conjI |
51 val conjE= HOL.conjE |
27 val conjE= HOL.conjE |
52 val impI = HOL.impI |
28 val impI = HOL.impI |
53 val mp = HOL.mp |
29 val mp = HOL.mp |
54 val uncurry = uncurry |
30 val uncurry = thm "uncurry" |
55 val exI = HOL.exI |
31 val exI = HOL.exI |
56 val exE = HOL.exE |
32 val exE = HOL.exE |
57 val iff_allI = iff_allI |
33 val iff_allI = thm "iff_allI" |
58 val iff_exI = iff_exI |
34 val iff_exI = thm "iff_exI" |
59 val all_comm = all_comm |
35 val all_comm = thm "all_comm" |
60 val ex_comm = ex_comm |
36 val ex_comm = thm "ex_comm" |
61 end); |
37 end); |
62 |
38 |
|
39 structure HOL = |
|
40 struct |
|
41 |
|
42 open HOL; |
|
43 |
|
44 val Eq_FalseI = thm "Eq_FalseI"; |
|
45 val Eq_TrueI = thm "Eq_TrueI"; |
|
46 val simp_implies_def = thm "simp_implies_def"; |
|
47 val simp_impliesI = thm "simp_impliesI"; |
|
48 |
|
49 fun mk_meta_eq r = r RS eq_reflection; |
|
50 fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; |
|
51 |
|
52 fun mk_eq thm = case concl_of thm |
|
53 (*expects Trueprop if not == *) |
|
54 of Const ("==",_) $ _ $ _ => thm |
|
55 | _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq thm |
|
56 | _ $ (Const ("Not", _) $ _) => thm RS Eq_FalseI |
|
57 | _ => thm RS Eq_TrueI; |
|
58 |
|
59 fun mk_eq_True r = |
|
60 SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE; |
|
61 |
|
62 (* Produce theorems of the form |
|
63 (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) |
|
64 *) |
|
65 fun lift_meta_eq_to_obj_eq i st = |
|
66 let |
|
67 fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q |
|
68 | count_imp _ = 0; |
|
69 val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1))) |
|
70 in if j = 0 then meta_eq_to_obj_eq |
|
71 else |
|
72 let |
|
73 val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); |
|
74 fun mk_simp_implies Q = foldr (fn (R, S) => |
|
75 Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps |
|
76 val aT = TFree ("'a", HOLogic.typeS); |
|
77 val x = Free ("x", aT); |
|
78 val y = Free ("y", aT) |
|
79 in Goal.prove_global (Thm.theory_of_thm st) [] |
|
80 [mk_simp_implies (Logic.mk_equals (x, y))] |
|
81 (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))) |
|
82 (fn prems => EVERY |
|
83 [rewrite_goals_tac [simp_implies_def], |
|
84 REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)]) |
|
85 end |
|
86 end; |
|
87 |
|
88 (*Congruence rules for = (instead of ==)*) |
|
89 fun mk_meta_cong rl = zero_var_indexes |
|
90 (let val rl' = Seq.hd (TRYALL (fn i => fn st => |
|
91 rtac (lift_meta_eq_to_obj_eq i st) i st) rl) |
|
92 in mk_meta_eq rl' handle THM _ => |
|
93 if can Logic.dest_equals (concl_of rl') then rl' |
|
94 else error "Conclusion of congruence rules must be =-equality" |
|
95 end); |
|
96 |
|
97 (* |
|
98 val mk_atomize: (string * thm list) list -> thm -> thm list |
|
99 looks too specific to move it somewhere else |
|
100 *) |
|
101 fun mk_atomize pairs = |
|
102 let |
|
103 fun atoms thm = case concl_of thm |
|
104 of Const("Trueprop", _) $ p => (case head_of p |
|
105 of Const(a, _) => (case AList.lookup (op =) pairs a |
|
106 of SOME rls => maps atoms ([thm] RL rls) |
|
107 | NONE => [thm]) |
|
108 | _ => [thm]) |
|
109 | _ => [thm] |
|
110 in atoms end; |
|
111 |
|
112 fun mksimps pairs = |
|
113 (map_filter (try mk_eq) o mk_atomize pairs o gen_all); |
|
114 |
|
115 fun unsafe_solver_tac prems = |
|
116 (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' |
|
117 FIRST'[resolve_tac(reflexive_thm :: TrueI :: refl :: prems), atac, etac FalseE]; |
|
118 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; |
|
119 |
|
120 (*No premature instantiation of variables during simplification*) |
|
121 fun safe_solver_tac prems = |
|
122 (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' |
|
123 FIRST'[match_tac(reflexive_thm :: TrueI :: refl :: prems), |
|
124 eq_assume_tac, ematch_tac [FalseE]]; |
|
125 val safe_solver = mk_solver "HOL safe" safe_solver_tac; |
|
126 |
63 end; |
127 end; |
64 |
128 |
65 val defEX_regroup = |
129 structure SplitterData = |
66 Simplifier.simproc (the_context ()) |
130 struct |
67 "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; |
131 structure Simplifier = Simplifier |
68 |
132 val mk_eq = HOL.mk_eq |
69 val defALL_regroup = |
133 val meta_eq_to_iff = HOL.meta_eq_to_obj_eq |
70 Simplifier.simproc (the_context ()) |
134 val iffD = HOL.iffD2 |
71 "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; |
135 val disjE = HOL.disjE |
72 |
136 val conjE = HOL.conjE |
|
137 val exE = HOL.exE |
|
138 val contrapos = HOL.contrapos_nn |
|
139 val contrapos2 = HOL.contrapos_pp |
|
140 val notnotD = HOL.notnotD |
|
141 end; |
|
142 |
|
143 structure Splitter = SplitterFun(SplitterData); |
|
144 |
|
145 (* integration of simplifier with classical reasoner *) |
|
146 |
|
147 structure Clasimp = ClasimpFun |
|
148 (structure Simplifier = Simplifier and Splitter = Splitter |
|
149 and Classical = Classical and Blast = Blast |
|
150 val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE); |
|
151 |
|
152 structure HOL = |
|
153 struct |
|
154 |
|
155 open HOL; |
|
156 |
|
157 val mksimps_pairs = |
|
158 [("op -->", [mp]), ("op &", [thm "conjunct1", thm "conjunct2"]), |
|
159 ("All", [spec]), ("True", []), ("False", []), |
|
160 ("HOL.If", [thm "if_bool_eq_conj" RS iffD1])]; |
|
161 |
|
162 val simpset_basic = |
|
163 Simplifier.theory_context (the_context ()) empty_ss |
|
164 setsubgoaler asm_simp_tac |
|
165 setSSolver safe_solver |
|
166 setSolver unsafe_solver |
|
167 setmksimps (mksimps mksimps_pairs) |
|
168 setmkeqTrue mk_eq_True |
|
169 setmkcong mk_meta_cong; |
|
170 |
|
171 fun simplify rews = Simplifier.full_simplify (simpset_basic addsimps rews); |
|
172 |
|
173 fun unfold_tac ths = |
|
174 let val ss0 = Simplifier.clear_ss simpset_basic addsimps ths |
|
175 in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end; |
|
176 |
|
177 (** simprocs **) |
73 |
178 |
74 (* simproc for proving "(y = x) == False" from premise "~(x = y)" *) |
179 (* simproc for proving "(y = x) == False" from premise "~(x = y)" *) |
75 |
180 |
76 val use_neq_simproc = ref true; |
181 val use_neq_simproc = ref true; |
77 |
182 |
78 local |
183 local |
79 val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI; |
184 val thy = the_context (); |
|
185 val neq_to_EQ_False = thm "not_sym" RS HOL.Eq_FalseI; |
80 fun neq_prover sg ss (eq $ lhs $ rhs) = |
186 fun neq_prover sg ss (eq $ lhs $ rhs) = |
81 let |
187 let |
82 fun test thm = (case #prop (rep_thm thm) of |
188 fun test thm = (case #prop (rep_thm thm) of |
83 _ $ (Not $ (eq' $ l' $ r')) => |
189 _ $ (Not $ (eq' $ l' $ r')) => |
84 Not = HOLogic.Not andalso eq' = eq andalso |
190 Not = HOLogic.Not andalso eq' = eq andalso |
89 | SOME thm => SOME (thm RS neq_to_EQ_False) |
195 | SOME thm => SOME (thm RS neq_to_EQ_False) |
90 else NONE |
196 else NONE |
91 end |
197 end |
92 in |
198 in |
93 |
199 |
94 val neq_simproc = Simplifier.simproc (the_context ()) |
200 val neq_simproc = Simplifier.simproc thy "neq_simproc" ["x = y"] neq_prover; |
95 "neq_simproc" ["x = y"] neq_prover; |
201 |
96 |
202 end; (*local*) |
97 end; |
|
98 |
203 |
99 |
204 |
100 (* Simproc for Let *) |
205 (* Simproc for Let *) |
101 |
206 |
102 val use_let_simproc = ref true; |
207 val use_let_simproc = ref true; |
103 |
208 |
104 local |
209 local |
|
210 val thy = the_context (); |
105 val Let_folded = thm "Let_folded"; |
211 val Let_folded = thm "Let_folded"; |
106 val Let_unfold = thm "Let_unfold"; |
212 val Let_unfold = thm "Let_unfold"; |
107 val (f_Let_unfold,x_Let_unfold) = |
213 val (f_Let_unfold, x_Let_unfold) = |
108 let val [(_$(f$x)$_)] = prems_of Let_unfold |
214 let val [(_$(f$x)$_)] = prems_of Let_unfold |
109 in (cterm_of (the_context ()) f,cterm_of (the_context ()) x) end |
215 in (cterm_of thy f, cterm_of thy x) end |
110 val (f_Let_folded,x_Let_folded) = |
216 val (f_Let_folded, x_Let_folded) = |
111 let val [(_$(f$x)$_)] = prems_of Let_folded |
217 let val [(_$(f$x)$_)] = prems_of Let_folded |
112 in (cterm_of (the_context ()) f, cterm_of (the_context ()) x) end; |
218 in (cterm_of thy f, cterm_of thy x) end; |
113 val g_Let_folded = |
219 val g_Let_folded = |
114 let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (the_context ()) g end; |
220 let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of thy g end; |
115 in |
221 in |
116 |
222 |
117 val let_simproc = |
223 val let_simproc = |
118 Simplifier.simproc (the_context ()) "let_simp" ["Let x f"] |
224 Simplifier.simproc thy "let_simp" ["Let x f"] |
119 (fn sg => fn ss => fn t => |
225 (fn sg => fn ss => fn t => |
120 let val ctxt = Simplifier.the_context ss; |
226 let val ctxt = Simplifier.the_context ss; |
121 val ([t'],ctxt') = Variable.import_terms false [t] ctxt; |
227 val ([t'], ctxt') = Variable.import_terms false [t] ctxt; |
122 in Option.map (hd o Variable.export ctxt' ctxt o single) |
228 in Option.map (hd o Variable.export ctxt' ctxt o single) |
123 (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *) |
229 (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *) |
124 if not (!use_let_simproc) then NONE |
230 if not (!use_let_simproc) then NONE |
125 else if is_Free x orelse is_Bound x orelse is_Const x |
231 else if is_Free x orelse is_Bound x orelse is_Const x |
126 then SOME (thm "Let_def") |
232 then SOME (thm "Let_def") |
151 end) |
257 end) |
152 end |
258 end |
153 | _ => NONE) |
259 | _ => NONE) |
154 end) |
260 end) |
155 |
261 |
156 end |
262 end; (*local*) |
157 |
263 |
158 (*** Case splitting ***) |
264 (* A general refutation procedure *) |
159 |
|
160 (*Make meta-equalities. The operator below is Trueprop*) |
|
161 |
|
162 fun mk_meta_eq r = r RS HOL.eq_reflection; |
|
163 fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; |
|
164 |
|
165 fun mk_eq th = case concl_of th of |
|
166 Const("==",_)$_$_ => th |
|
167 | _$(Const("op =",_)$_$_) => mk_meta_eq th |
|
168 | _$(Const("Not",_)$_) => th RS Eq_FalseI |
|
169 | _ => th RS Eq_TrueI; |
|
170 (* Expects Trueprop(.) if not == *) |
|
171 |
|
172 fun mk_eq_True r = |
|
173 SOME (r RS HOL.meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE; |
|
174 |
|
175 (* Produce theorems of the form |
|
176 (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) |
|
177 *) |
|
178 fun lift_meta_eq_to_obj_eq i st = |
|
179 let |
|
180 val {sign, ...} = rep_thm st; |
|
181 fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q |
|
182 | count_imp _ = 0; |
|
183 val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1))) |
|
184 in if j = 0 then HOL.meta_eq_to_obj_eq |
|
185 else |
|
186 let |
|
187 val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); |
|
188 fun mk_simp_implies Q = foldr (fn (R, S) => |
|
189 Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps |
|
190 val aT = TFree ("'a", HOLogic.typeS); |
|
191 val x = Free ("x", aT); |
|
192 val y = Free ("y", aT) |
|
193 in Goal.prove_global (Thm.theory_of_thm st) [] |
|
194 [mk_simp_implies (Logic.mk_equals (x, y))] |
|
195 (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))) |
|
196 (fn prems => EVERY |
|
197 [rewrite_goals_tac [simp_implies_def], |
|
198 REPEAT (ares_tac (HOL.meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)]) |
|
199 end |
|
200 end; |
|
201 |
|
202 (*Congruence rules for = (instead of ==)*) |
|
203 fun mk_meta_cong rl = zero_var_indexes |
|
204 (let val rl' = Seq.hd (TRYALL (fn i => fn st => |
|
205 rtac (lift_meta_eq_to_obj_eq i st) i st) rl) |
|
206 in mk_meta_eq rl' handle THM _ => |
|
207 if can Logic.dest_equals (concl_of rl') then rl' |
|
208 else error "Conclusion of congruence rules must be =-equality" |
|
209 end); |
|
210 |
|
211 structure SplitterData = |
|
212 struct |
|
213 structure Simplifier = Simplifier |
|
214 val mk_eq = mk_eq |
|
215 val meta_eq_to_iff = HOL.meta_eq_to_obj_eq |
|
216 val iffD = HOL.iffD2 |
|
217 val disjE = HOL.disjE |
|
218 val conjE = HOL.conjE |
|
219 val exE = HOL.exE |
|
220 val contrapos = HOL.contrapos_nn |
|
221 val contrapos2 = HOL.contrapos_pp |
|
222 val notnotD = HOL.notnotD |
|
223 end; |
|
224 |
|
225 structure Splitter = SplitterFun(SplitterData); |
|
226 |
|
227 val split_tac = Splitter.split_tac; |
|
228 val split_inside_tac = Splitter.split_inside_tac; |
|
229 val split_asm_tac = Splitter.split_asm_tac; |
|
230 val op addsplits = Splitter.addsplits; |
|
231 val op delsplits = Splitter.delsplits; |
|
232 val Addsplits = Splitter.Addsplits; |
|
233 val Delsplits = Splitter.Delsplits; |
|
234 |
|
235 val mksimps_pairs = |
|
236 [("op -->", [HOL.mp]), ("op &", [thm "conjunct1", thm "conjunct2"]), |
|
237 ("All", [HOL.spec]), ("True", []), ("False", []), |
|
238 ("HOL.If", [thm "if_bool_eq_conj" RS HOL.iffD1])]; |
|
239 |
|
240 (* |
|
241 val mk_atomize: (string * thm list) list -> thm -> thm list |
|
242 looks too specific to move it somewhere else |
|
243 *) |
|
244 fun mk_atomize pairs = |
|
245 let fun atoms th = |
|
246 (case concl_of th of |
|
247 Const("Trueprop",_) $ p => |
|
248 (case head_of p of |
|
249 Const(a,_) => |
|
250 (case AList.lookup (op =) pairs a of |
|
251 SOME(rls) => List.concat (map atoms ([th] RL rls)) |
|
252 | NONE => [th]) |
|
253 | _ => [th]) |
|
254 | _ => [th]) |
|
255 in atoms end; |
|
256 |
|
257 fun mksimps pairs = |
|
258 (List.mapPartial (try mk_eq) o mk_atomize pairs o gen_all); |
|
259 |
|
260 fun unsafe_solver_tac prems = |
|
261 (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' |
|
262 FIRST'[resolve_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems), atac, etac HOL.FalseE]; |
|
263 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; |
|
264 |
|
265 (*No premature instantiation of variables during simplification*) |
|
266 fun safe_solver_tac prems = |
|
267 (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' |
|
268 FIRST'[match_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems), |
|
269 eq_assume_tac, ematch_tac [HOL.FalseE]]; |
|
270 val safe_solver = mk_solver "HOL safe" safe_solver_tac; |
|
271 |
|
272 val HOL_basic_ss = |
|
273 Simplifier.theory_context (the_context ()) empty_ss |
|
274 setsubgoaler asm_simp_tac |
|
275 setSSolver safe_solver |
|
276 setSolver unsafe_solver |
|
277 setmksimps (mksimps mksimps_pairs) |
|
278 setmkeqTrue mk_eq_True |
|
279 setmkcong mk_meta_cong; |
|
280 |
|
281 fun unfold_tac ths = |
|
282 let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths |
|
283 in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end; |
|
284 |
|
285 (*In general it seems wrong to add distributive laws by default: they |
|
286 might cause exponential blow-up. But imp_disjL has been in for a while |
|
287 and cannot be removed without affecting existing proofs. Moreover, |
|
288 rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the |
|
289 grounds that it allows simplification of R in the two cases.*) |
|
290 |
|
291 local |
|
292 val ex_simps = thms "ex_simps"; |
|
293 val all_simps = thms "all_simps"; |
|
294 val simp_thms = thms "simp_thms"; |
|
295 val cases_simp = thm "cases_simp"; |
|
296 val conj_assoc = thm "conj_assoc"; |
|
297 val if_False = thm "if_False"; |
|
298 val if_True = thm "if_True"; |
|
299 val disj_assoc = thm "disj_assoc"; |
|
300 val disj_not1 = thm "disj_not1"; |
|
301 val if_cancel = thm "if_cancel"; |
|
302 val if_eq_cancel = thm "if_eq_cancel"; |
|
303 val True_implies_equals = thm "True_implies_equals"; |
|
304 in |
|
305 |
|
306 val HOL_ss = |
|
307 HOL_basic_ss addsimps |
|
308 ([triv_forall_equality, (* prunes params *) |
|
309 True_implies_equals, (* prune asms `True' *) |
|
310 if_True, if_False, if_cancel, if_eq_cancel, |
|
311 imp_disjL, conj_assoc, disj_assoc, |
|
312 de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, thm "not_imp", |
|
313 disj_not1, thm "not_all", thm "not_ex", cases_simp, |
|
314 thm "the_eq_trivial", HOL.the_sym_eq_trivial] |
|
315 @ ex_simps @ all_simps @ simp_thms) |
|
316 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc] |
|
317 addcongs [imp_cong, simp_implies_cong] |
|
318 addsplits [thm "split_if"]; |
|
319 |
|
320 end; |
|
321 |
|
322 fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); |
|
323 |
|
324 (* default simpset *) |
|
325 val simpsetup = |
|
326 (fn thy => (change_simpset_of thy (fn _ => HOL_ss); thy)); |
|
327 |
|
328 |
|
329 (*** integration of simplifier with classical reasoner ***) |
|
330 |
|
331 structure Clasimp = ClasimpFun |
|
332 (structure Simplifier = Simplifier and Splitter = Splitter |
|
333 and Classical = Classical and Blast = Blast |
|
334 val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE); |
|
335 open Clasimp; |
|
336 |
|
337 val HOL_css = (HOL_cs, HOL_ss); |
|
338 |
|
339 |
|
340 |
|
341 (*** A general refutation procedure ***) |
|
342 |
265 |
343 (* Parameters: |
266 (* Parameters: |
344 |
267 |
345 test: term -> bool |
268 test: term -> bool |
346 tests if a term is at all relevant to the refutation proof; |
269 tests if a term is at all relevant to the refutation proof; |
359 |
282 |
360 local |
283 local |
361 val nnf_simpset = |
284 val nnf_simpset = |
362 empty_ss setmkeqTrue mk_eq_True |
285 empty_ss setmkeqTrue mk_eq_True |
363 setmksimps (mksimps mksimps_pairs) |
286 setmksimps (mksimps mksimps_pairs) |
364 addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj, |
287 addsimps [thm "imp_conv_disj", thm "iff_conv_conj_imp", thm "de_Morgan_disj", thm "de_Morgan_conj", |
365 thm "not_all", thm "not_ex", thm "not_not"]; |
288 thm "not_all", thm "not_ex", thm "not_not"]; |
366 fun prem_nnf_tac i st = |
289 fun prem_nnf_tac i st = |
367 full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st; |
290 full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st; |
368 in |
291 in |
369 fun refute_tac test prep_tac ref_tac = |
292 fun refute_tac test prep_tac ref_tac = |
370 let val refute_prems_tac = |
293 let val refute_prems_tac = |
371 REPEAT_DETERM |
294 REPEAT_DETERM |
372 (eresolve_tac [HOL.conjE, HOL.exE] 1 ORELSE |
295 (eresolve_tac [conjE, exE] 1 ORELSE |
373 filter_prems_tac test 1 ORELSE |
296 filter_prems_tac test 1 ORELSE |
374 etac HOL.disjE 1) THEN |
297 etac disjE 1) THEN |
375 ((etac HOL.notE 1 THEN eq_assume_tac 1) ORELSE |
298 ((etac notE 1 THEN eq_assume_tac 1) ORELSE |
376 ref_tac 1); |
299 ref_tac 1); |
377 in EVERY'[TRY o filter_prems_tac test, |
300 in EVERY'[TRY o filter_prems_tac test, |
378 REPEAT_DETERM o etac HOL.rev_mp, prep_tac, rtac HOL.ccontr, prem_nnf_tac, |
301 REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, |
379 SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] |
302 SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] |
380 end; |
303 end; |
381 end; |
304 end; (*local*) |
|
305 |
|
306 val defALL_regroup = |
|
307 Simplifier.simproc (the_context ()) |
|
308 "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; |
|
309 |
|
310 val defEX_regroup = |
|
311 Simplifier.simproc (the_context ()) |
|
312 "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; |
|
313 |
|
314 |
|
315 val simpset_simprocs = simpset_basic |
|
316 addsimprocs [defALL_regroup, defEX_regroup, neq_simproc, let_simproc] |
|
317 |
|
318 end; (*struct*) |