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 *) |
9 (* legacy ML bindings - FIXME get rid of this *) |
10 |
10 |
11 val Eq_FalseI = thm "Eq_FalseI"; |
11 val Eq_FalseI = thm "Eq_FalseI"; |
12 val Eq_TrueI = thm "Eq_TrueI"; |
12 val Eq_TrueI = thm "Eq_TrueI"; |
13 val all_conj_distrib = thm "all_conj_distrib"; |
|
14 val all_simps = thms "all_simps"; |
|
15 val cases_simp = thm "cases_simp"; |
|
16 val conj_assoc = thm "conj_assoc"; |
|
17 val conj_comms = thms "conj_comms"; |
|
18 val conj_commute = thm "conj_commute"; |
|
19 val conj_cong = thm "conj_cong"; |
|
20 val conj_disj_distribL = thm "conj_disj_distribL"; |
|
21 val conj_disj_distribR = thm "conj_disj_distribR"; |
|
22 val conj_left_commute = thm "conj_left_commute"; |
|
23 val de_Morgan_conj = thm "de_Morgan_conj"; |
13 val de_Morgan_conj = thm "de_Morgan_conj"; |
24 val de_Morgan_disj = thm "de_Morgan_disj"; |
14 val de_Morgan_disj = thm "de_Morgan_disj"; |
25 val disj_assoc = thm "disj_assoc"; |
|
26 val disj_comms = thms "disj_comms"; |
|
27 val disj_commute = thm "disj_commute"; |
|
28 val disj_cong = thm "disj_cong"; |
|
29 val disj_conj_distribL = thm "disj_conj_distribL"; |
|
30 val disj_conj_distribR = thm "disj_conj_distribR"; |
|
31 val disj_left_commute = thm "disj_left_commute"; |
|
32 val disj_not1 = thm "disj_not1"; |
|
33 val disj_not2 = thm "disj_not2"; |
|
34 val eq_ac = thms "eq_ac"; |
|
35 val eq_assoc = thm "eq_assoc"; |
|
36 val eq_commute = thm "eq_commute"; |
|
37 val eq_left_commute = thm "eq_left_commute"; |
|
38 val eq_sym_conv = thm "eq_sym_conv"; |
|
39 val eta_contract_eq = thm "eta_contract_eq"; |
|
40 val ex_disj_distrib = thm "ex_disj_distrib"; |
|
41 val ex_simps = thms "ex_simps"; |
|
42 val if_False = thm "if_False"; |
|
43 val if_P = thm "if_P"; |
|
44 val if_True = thm "if_True"; |
|
45 val if_bool_eq_conj = thm "if_bool_eq_conj"; |
|
46 val if_bool_eq_disj = thm "if_bool_eq_disj"; |
|
47 val if_cancel = thm "if_cancel"; |
|
48 val if_def2 = thm "if_def2"; |
|
49 val if_eq_cancel = thm "if_eq_cancel"; |
|
50 val if_not_P = thm "if_not_P"; |
|
51 val if_splits = thms "if_splits"; |
|
52 val iff_conv_conj_imp = thm "iff_conv_conj_imp"; |
15 val iff_conv_conj_imp = thm "iff_conv_conj_imp"; |
53 val imp_all = thm "imp_all"; |
|
54 val imp_cong = thm "imp_cong"; |
16 val imp_cong = thm "imp_cong"; |
55 val imp_conjL = thm "imp_conjL"; |
|
56 val imp_conjR = thm "imp_conjR"; |
|
57 val imp_conv_disj = thm "imp_conv_disj"; |
17 val imp_conv_disj = thm "imp_conv_disj"; |
58 val imp_disj1 = thm "imp_disj1"; |
18 val imp_disj1 = thm "imp_disj1"; |
59 val imp_disj2 = thm "imp_disj2"; |
19 val imp_disj2 = thm "imp_disj2"; |
60 val imp_disjL = thm "imp_disjL"; |
20 val imp_disjL = thm "imp_disjL"; |
61 val imp_disj_not1 = thm "imp_disj_not1"; |
|
62 val imp_disj_not2 = thm "imp_disj_not2"; |
|
63 val imp_ex = thm "imp_ex"; |
|
64 val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; |
|
65 val neq_commute = thm "neq_commute"; |
|
66 val not_all = thm "not_all"; |
|
67 val not_ex = thm "not_ex"; |
|
68 val not_iff = thm "not_iff"; |
|
69 val not_imp = thm "not_imp"; |
|
70 val not_not = thm "not_not"; |
|
71 val rev_conj_cong = thm "rev_conj_cong"; |
|
72 val simp_impliesE = thm "simp_impliesI"; |
|
73 val simp_impliesI = thm "simp_impliesI"; |
21 val simp_impliesI = thm "simp_impliesI"; |
74 val simp_implies_cong = thm "simp_implies_cong"; |
22 val simp_implies_cong = thm "simp_implies_cong"; |
75 val simp_implies_def = thm "simp_implies_def"; |
23 val simp_implies_def = thm "simp_implies_def"; |
76 val simp_thms = thms "simp_thms"; |
24 |
77 val split_if = thm "split_if"; |
25 local |
78 val split_if_asm = thm "split_if_asm"; |
26 val uncurry = thm "uncurry" |
79 val atomize_not = thm"atomize_not"; |
27 val iff_allI = thm "iff_allI" |
80 |
28 val iff_exI = thm "iff_exI" |
81 local |
29 val all_comm = thm "all_comm" |
82 val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R" |
30 val ex_comm = thm "ex_comm" |
83 (fn prems => [cut_facts_tac prems 1, Blast_tac 1]); |
|
84 |
|
85 val iff_allI = allI RS |
|
86 prove_goal (the_context()) "!x. P x = Q x ==> (!x. P x) = (!x. Q x)" |
|
87 (fn prems => [cut_facts_tac prems 1, Blast_tac 1]) |
|
88 val iff_exI = allI RS |
|
89 prove_goal (the_context()) "!x. P x = Q x ==> (? x. P x) = (? x. Q x)" |
|
90 (fn prems => [cut_facts_tac prems 1, Blast_tac 1]) |
|
91 |
|
92 val all_comm = prove_goal (the_context()) "(!x y. P x y) = (!y x. P x y)" |
|
93 (fn _ => [Blast_tac 1]) |
|
94 val ex_comm = prove_goal (the_context()) "(? x y. P x y) = (? y x. P x y)" |
|
95 (fn _ => [Blast_tac 1]) |
|
96 in |
31 in |
97 |
32 |
98 (*** make simplification procedures for quantifier elimination ***) |
33 (*** make simplification procedures for quantifier elimination ***) |
99 |
34 |
100 structure Quantifier1 = Quantifier1Fun |
35 structure Quantifier1 = Quantifier1Fun |
107 fun dest_imp((c as Const("op -->",_)) $ s $ t) = SOME(c,s,t) |
42 fun dest_imp((c as Const("op -->",_)) $ s $ t) = SOME(c,s,t) |
108 | dest_imp _ = NONE; |
43 | dest_imp _ = NONE; |
109 val conj = HOLogic.conj |
44 val conj = HOLogic.conj |
110 val imp = HOLogic.imp |
45 val imp = HOLogic.imp |
111 (*rules*) |
46 (*rules*) |
112 val iff_reflection = eq_reflection |
47 val iff_reflection = HOL.eq_reflection |
113 val iffI = iffI |
48 val iffI = HOL.iffI |
114 val iff_trans = trans |
49 val iff_trans = HOL.trans |
115 val conjI= conjI |
50 val conjI= HOL.conjI |
116 val conjE= conjE |
51 val conjE= HOL.conjE |
117 val impI = impI |
52 val impI = HOL.impI |
118 val mp = mp |
53 val mp = HOL.mp |
119 val uncurry = uncurry |
54 val uncurry = uncurry |
120 val exI = exI |
55 val exI = HOL.exI |
121 val exE = exE |
56 val exE = HOL.exE |
122 val iff_allI = iff_allI |
57 val iff_allI = iff_allI |
123 val iff_exI = iff_exI |
58 val iff_exI = iff_exI |
124 val all_comm = all_comm |
59 val all_comm = all_comm |
125 val ex_comm = ex_comm |
60 val ex_comm = ex_comm |
126 end); |
61 end); |
127 |
62 |
128 end; |
63 end; |
129 |
64 |
130 val defEX_regroup = |
65 val defEX_regroup = |
131 Simplifier.simproc (Theory.sign_of (the_context ())) |
66 Simplifier.simproc (the_context ()) |
132 "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; |
67 "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; |
133 |
68 |
134 val defALL_regroup = |
69 val defALL_regroup = |
135 Simplifier.simproc (Theory.sign_of (the_context ())) |
70 Simplifier.simproc (the_context ()) |
136 "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; |
71 "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; |
137 |
72 |
138 |
73 |
139 (*** simproc for proving "(y = x) == False" from prmise "~(x = y)" ***) |
74 (* simproc for proving "(y = x) == False" from premise "~(x = y)" *) |
140 |
75 |
141 val use_neq_simproc = ref true; |
76 val use_neq_simproc = ref true; |
142 |
77 |
143 local |
78 local |
144 |
79 val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI; |
145 val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI; |
80 fun neq_prover sg ss (eq $ lhs $ rhs) = |
146 |
81 let |
147 fun neq_prover sg ss (eq $ lhs $ rhs) = |
82 fun test thm = (case #prop (rep_thm thm) of |
148 let |
|
149 fun test thm = (case #prop(rep_thm thm) of |
|
150 _ $ (Not $ (eq' $ l' $ r')) => |
83 _ $ (Not $ (eq' $ l' $ r')) => |
151 Not = HOLogic.Not andalso eq' = eq andalso |
84 Not = HOLogic.Not andalso eq' = eq andalso |
152 r' aconv lhs andalso l' aconv rhs |
85 r' aconv lhs andalso l' aconv rhs |
153 | _ => false) |
86 | _ => false) |
154 in |
87 in if !use_neq_simproc then case find_first test (prems_of_ss ss) |
155 if !use_neq_simproc then |
88 of NONE => NONE |
156 case Library.find_first test (prems_of_ss ss) of NONE => NONE |
89 | SOME thm => SOME (thm RS neq_to_EQ_False) |
157 | SOME thm => SOME (thm RS neq_to_EQ_False) |
90 else NONE |
158 else NONE |
91 end |
159 end |
92 in |
160 |
93 |
161 in |
94 val neq_simproc = Simplifier.simproc (the_context ()) |
162 |
95 "neq_simproc" ["x = y"] neq_prover; |
163 val neq_simproc = |
96 |
164 Simplifier.simproc (the_context ()) "neq_simproc" ["x = y"] neq_prover; |
97 end; |
165 |
98 |
166 end; |
99 |
167 |
100 (* Simproc for Let *) |
168 |
|
169 (*** Simproc for Let ***) |
|
170 |
101 |
171 val use_let_simproc = ref true; |
102 val use_let_simproc = ref true; |
172 |
103 |
173 local |
104 local |
174 val Let_folded = thm "Let_folded"; |
105 val Let_folded = thm "Let_folded"; |
175 val Let_unfold = thm "Let_unfold"; |
106 val Let_unfold = thm "Let_unfold"; |
176 |
107 val (f_Let_unfold,x_Let_unfold) = |
177 val (f_Let_unfold,x_Let_unfold) = |
|
178 let val [(_$(f$x)$_)] = prems_of Let_unfold |
108 let val [(_$(f$x)$_)] = prems_of Let_unfold |
179 in (cterm_of (sign_of (the_context ())) f,cterm_of (sign_of (the_context ())) x) end |
109 in (cterm_of (the_context ()) f,cterm_of (the_context ()) x) end |
180 val (f_Let_folded,x_Let_folded) = |
110 val (f_Let_folded,x_Let_folded) = |
181 let val [(_$(f$x)$_)] = prems_of Let_folded |
111 let val [(_$(f$x)$_)] = prems_of Let_folded |
182 in (cterm_of (sign_of (the_context ())) f, cterm_of (sign_of (the_context ())) x) end; |
112 in (cterm_of (the_context ()) f, cterm_of (the_context ()) x) end; |
183 val g_Let_folded = |
113 val g_Let_folded = |
184 let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (sign_of (the_context ())) g end; |
114 let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (the_context ()) g end; |
185 in |
115 in |
|
116 |
186 val let_simproc = |
117 val let_simproc = |
187 Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"] |
118 Simplifier.simproc (the_context ()) "let_simp" ["Let x f"] |
188 (fn sg => fn ss => fn t => |
119 (fn sg => fn ss => fn t => |
189 let val ctxt = Simplifier.the_context ss; |
120 let val ctxt = Simplifier.the_context ss; |
190 val ([t'],ctxt') = Variable.import_terms false [t] ctxt; |
121 val ([t'],ctxt') = Variable.import_terms false [t] ctxt; |
191 in Option.map (hd o Variable.export ctxt' ctxt o single) |
122 in Option.map (hd o Variable.export ctxt' ctxt o single) |
192 (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *) |
123 (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *) |
193 if not (!use_let_simproc) then NONE |
124 if not (!use_let_simproc) then NONE |
194 else if is_Free x orelse is_Bound x orelse is_Const x |
125 else if is_Free x orelse is_Bound x orelse is_Const x |
195 then SOME Let_def |
126 then SOME (thm "Let_def") |
196 else |
127 else |
197 let |
128 let |
198 val n = case f of (Abs (x,_,_)) => x | _ => "x"; |
129 val n = case f of (Abs (x,_,_)) => x | _ => "x"; |
199 val cx = cterm_of sg x; |
130 val cx = cterm_of sg x; |
200 val {T=xT,...} = rep_cterm cx; |
131 val {T=xT,...} = rep_cterm cx; |
219 in SOME (rl OF [transitive fx_g g_g'x]) |
150 in SOME (rl OF [transitive fx_g g_g'x]) |
220 end) |
151 end) |
221 end |
152 end |
222 | _ => NONE) |
153 | _ => NONE) |
223 end) |
154 end) |
|
155 |
224 end |
156 end |
225 |
157 |
226 (*** Case splitting ***) |
158 (*** Case splitting ***) |
227 |
159 |
228 (*Make meta-equalities. The operator below is Trueprop*) |
160 (*Make meta-equalities. The operator below is Trueprop*) |
229 |
161 |
230 fun mk_meta_eq r = r RS eq_reflection; |
162 fun mk_meta_eq r = r RS HOL.eq_reflection; |
231 fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; |
163 fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; |
232 |
164 |
233 fun mk_eq th = case concl_of th of |
165 fun mk_eq th = case concl_of th of |
234 Const("==",_)$_$_ => th |
166 Const("==",_)$_$_ => th |
235 | _$(Const("op =",_)$_$_) => mk_meta_eq th |
167 | _$(Const("op =",_)$_$_) => mk_meta_eq th |
236 | _$(Const("Not",_)$_) => th RS Eq_FalseI |
168 | _$(Const("Not",_)$_) => th RS Eq_FalseI |
237 | _ => th RS Eq_TrueI; |
169 | _ => th RS Eq_TrueI; |
238 (* Expects Trueprop(.) if not == *) |
170 (* Expects Trueprop(.) if not == *) |
239 |
171 |
240 fun mk_eq_True r = |
172 fun mk_eq_True r = |
241 SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE; |
173 SOME (r RS HOL.meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE; |
242 |
174 |
243 (* Produce theorems of the form |
175 (* Produce theorems of the form |
244 (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) |
176 (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) |
245 *) |
177 *) |
246 fun lift_meta_eq_to_obj_eq i st = |
178 fun lift_meta_eq_to_obj_eq i st = |
247 let |
179 let |
248 val {sign, ...} = rep_thm st; |
180 val {sign, ...} = rep_thm st; |
249 fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q |
181 fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q |
250 | count_imp _ = 0; |
182 | count_imp _ = 0; |
251 val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1))) |
183 val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1))) |
252 in if j = 0 then meta_eq_to_obj_eq |
184 in if j = 0 then HOL.meta_eq_to_obj_eq |
253 else |
185 else |
254 let |
186 let |
255 val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); |
187 val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); |
256 fun mk_simp_implies Q = foldr (fn (R, S) => |
188 fun mk_simp_implies Q = foldr (fn (R, S) => |
257 Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps |
189 Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps |
274 in mk_meta_eq rl' handle THM _ => |
206 in mk_meta_eq rl' handle THM _ => |
275 if can Logic.dest_equals (concl_of rl') then rl' |
207 if can Logic.dest_equals (concl_of rl') then rl' |
276 else error "Conclusion of congruence rules must be =-equality" |
208 else error "Conclusion of congruence rules must be =-equality" |
277 end); |
209 end); |
278 |
210 |
279 (* Elimination of True from assumptions: *) |
|
280 |
|
281 local fun rd s = read_cterm (the_context()) (s, propT); |
|
282 in val True_implies_equals = standard' (equal_intr |
|
283 (implies_intr_hyps (implies_elim (assume (rd "True ==> PROP P")) TrueI)) |
|
284 (implies_intr_hyps (implies_intr (rd "True") (assume (rd "PROP P"))))); |
|
285 end; |
|
286 |
|
287 |
|
288 structure SplitterData = |
211 structure SplitterData = |
289 struct |
212 struct |
290 structure Simplifier = Simplifier |
213 structure Simplifier = Simplifier |
291 val mk_eq = mk_eq |
214 val mk_eq = mk_eq |
292 val meta_eq_to_iff = meta_eq_to_obj_eq |
215 val meta_eq_to_iff = HOL.meta_eq_to_obj_eq |
293 val iffD = iffD2 |
216 val iffD = HOL.iffD2 |
294 val disjE = disjE |
217 val disjE = HOL.disjE |
295 val conjE = conjE |
218 val conjE = HOL.conjE |
296 val exE = exE |
219 val exE = HOL.exE |
297 val contrapos = contrapos_nn |
220 val contrapos = HOL.contrapos_nn |
298 val contrapos2 = contrapos_pp |
221 val contrapos2 = HOL.contrapos_pp |
299 val notnotD = notnotD |
222 val notnotD = HOL.notnotD |
300 end; |
223 end; |
301 |
224 |
302 structure Splitter = SplitterFun(SplitterData); |
225 structure Splitter = SplitterFun(SplitterData); |
303 |
226 |
304 val split_tac = Splitter.split_tac; |
227 val split_tac = Splitter.split_tac; |
305 val split_inside_tac = Splitter.split_inside_tac; |
228 val split_inside_tac = Splitter.split_inside_tac; |
308 val op delsplits = Splitter.delsplits; |
231 val op delsplits = Splitter.delsplits; |
309 val Addsplits = Splitter.Addsplits; |
232 val Addsplits = Splitter.Addsplits; |
310 val Delsplits = Splitter.Delsplits; |
233 val Delsplits = Splitter.Delsplits; |
311 |
234 |
312 val mksimps_pairs = |
235 val mksimps_pairs = |
313 [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
236 [("op -->", [HOL.mp]), ("op &", [thm "conjunct1", thm "conjunct2"]), |
314 ("All", [spec]), ("True", []), ("False", []), |
237 ("All", [HOL.spec]), ("True", []), ("False", []), |
315 ("HOL.If", [if_bool_eq_conj RS iffD1])]; |
238 ("HOL.If", [thm "if_bool_eq_conj" RS HOL.iffD1])]; |
316 |
239 |
317 (* |
240 (* |
318 val mk_atomize: (string * thm list) list -> thm -> thm list |
241 val mk_atomize: (string * thm list) list -> thm -> thm list |
319 looks too specific to move it somewhere else |
242 looks too specific to move it somewhere else |
320 *) |
243 *) |
334 fun mksimps pairs = |
257 fun mksimps pairs = |
335 (List.mapPartial (try mk_eq) o mk_atomize pairs o gen_all); |
258 (List.mapPartial (try mk_eq) o mk_atomize pairs o gen_all); |
336 |
259 |
337 fun unsafe_solver_tac prems = |
260 fun unsafe_solver_tac prems = |
338 (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' |
261 (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' |
339 FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE]; |
262 FIRST'[resolve_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems), atac, etac HOL.FalseE]; |
340 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; |
263 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; |
341 |
264 |
342 (*No premature instantiation of variables during simplification*) |
265 (*No premature instantiation of variables during simplification*) |
343 fun safe_solver_tac prems = |
266 fun safe_solver_tac prems = |
344 (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' |
267 (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' |
345 FIRST'[match_tac(reflexive_thm::TrueI::refl::prems), |
268 FIRST'[match_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems), |
346 eq_assume_tac, ematch_tac [FalseE]]; |
269 eq_assume_tac, ematch_tac [HOL.FalseE]]; |
347 val safe_solver = mk_solver "HOL safe" safe_solver_tac; |
270 val safe_solver = mk_solver "HOL safe" safe_solver_tac; |
348 |
271 |
349 val HOL_basic_ss = |
272 val HOL_basic_ss = |
350 Simplifier.theory_context (the_context ()) empty_ss |
273 Simplifier.theory_context (the_context ()) empty_ss |
351 setsubgoaler asm_simp_tac |
274 setsubgoaler asm_simp_tac |
363 might cause exponential blow-up. But imp_disjL has been in for a while |
286 might cause exponential blow-up. But imp_disjL has been in for a while |
364 and cannot be removed without affecting existing proofs. Moreover, |
287 and cannot be removed without affecting existing proofs. Moreover, |
365 rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the |
288 rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the |
366 grounds that it allows simplification of R in the two cases.*) |
289 grounds that it allows simplification of R in the two cases.*) |
367 |
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 |
368 val HOL_ss = |
306 val HOL_ss = |
369 HOL_basic_ss addsimps |
307 HOL_basic_ss addsimps |
370 ([triv_forall_equality, (* prunes params *) |
308 ([triv_forall_equality, (* prunes params *) |
371 True_implies_equals, (* prune asms `True' *) |
309 True_implies_equals, (* prune asms `True' *) |
372 if_True, if_False, if_cancel, if_eq_cancel, |
310 if_True, if_False, if_cancel, if_eq_cancel, |
373 imp_disjL, conj_assoc, disj_assoc, |
311 imp_disjL, conj_assoc, disj_assoc, |
374 de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp, |
312 de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, thm "not_imp", |
375 disj_not1, not_all, not_ex, cases_simp, |
313 disj_not1, thm "not_all", thm "not_ex", cases_simp, |
376 thm "the_eq_trivial", the_sym_eq_trivial] |
314 thm "the_eq_trivial", HOL.the_sym_eq_trivial] |
377 @ ex_simps @ all_simps @ simp_thms) |
315 @ ex_simps @ all_simps @ simp_thms) |
378 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc] |
316 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc] |
379 addcongs [imp_cong, simp_implies_cong] |
317 addcongs [imp_cong, simp_implies_cong] |
380 addsplits [split_if]; |
318 addsplits [thm "split_if"]; |
|
319 |
|
320 end; |
381 |
321 |
382 fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); |
322 fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); |
383 |
|
384 |
|
385 (*Simplifies x assuming c and y assuming ~c*) |
|
386 val prems = Goalw [if_def] |
|
387 "[| b=c; c ==> x=u; ~c ==> y=v |] ==> \ |
|
388 \ (if b then x else y) = (if c then u else v)"; |
|
389 by (asm_simp_tac (HOL_ss addsimps prems) 1); |
|
390 qed "if_cong"; |
|
391 |
|
392 (*Prevents simplification of x and y: faster and allows the execution |
|
393 of functional programs. NOW THE DEFAULT.*) |
|
394 Goal "b=c ==> (if b then x else y) = (if c then x else y)"; |
|
395 by (etac arg_cong 1); |
|
396 qed "if_weak_cong"; |
|
397 |
|
398 (*Prevents simplification of t: much faster*) |
|
399 Goal "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"; |
|
400 by (etac arg_cong 1); |
|
401 qed "let_weak_cong"; |
|
402 |
|
403 (*To tidy up the result of a simproc. Only the RHS will be simplified.*) |
|
404 Goal "u = u' ==> (t==u) == (t==u')"; |
|
405 by (asm_simp_tac HOL_ss 1); |
|
406 qed "eq_cong2"; |
|
407 |
|
408 Goal "f(if c then x else y) = (if c then f x else f y)"; |
|
409 by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1); |
|
410 qed "if_distrib"; |
|
411 |
|
412 (*For expand_case_tac*) |
|
413 val prems = Goal "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; |
|
414 by (case_tac "P" 1); |
|
415 by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems))); |
|
416 qed "expand_case"; |
|
417 |
|
418 (*This lemma restricts the effect of the rewrite rule u=v to the left-hand |
|
419 side of an equality. Used in {Integ,Real}/simproc.ML*) |
|
420 Goal "x=y ==> (x=z) = (y=z)"; |
|
421 by (asm_simp_tac HOL_ss 1); |
|
422 qed "restrict_to_left"; |
|
423 |
323 |
424 (* default simpset *) |
324 (* default simpset *) |
425 val simpsetup = |
325 val simpsetup = |
426 (fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy)); |
326 (fn thy => (change_simpset_of thy (fn _ => HOL_ss); thy)); |
427 |
327 |
428 |
328 |
429 (*** integration of simplifier with classical reasoner ***) |
329 (*** integration of simplifier with classical reasoner ***) |
430 |
330 |
431 structure Clasimp = ClasimpFun |
331 structure Clasimp = ClasimpFun |
432 (structure Simplifier = Simplifier and Splitter = Splitter |
332 (structure Simplifier = Simplifier and Splitter = Splitter |
433 and Classical = Classical and Blast = Blast |
333 and Classical = Classical and Blast = Blast |
434 val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE); |
334 val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE); |
435 open Clasimp; |
335 open Clasimp; |
436 |
336 |
437 val HOL_css = (HOL_cs, HOL_ss); |
337 val HOL_css = (HOL_cs, HOL_ss); |
438 |
338 |
439 |
339 |
460 local |
360 local |
461 val nnf_simpset = |
361 val nnf_simpset = |
462 empty_ss setmkeqTrue mk_eq_True |
362 empty_ss setmkeqTrue mk_eq_True |
463 setmksimps (mksimps mksimps_pairs) |
363 setmksimps (mksimps mksimps_pairs) |
464 addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj, |
364 addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj, |
465 not_all,not_ex,not_not]; |
365 thm "not_all", thm "not_ex", thm "not_not"]; |
466 fun prem_nnf_tac i st = |
366 fun prem_nnf_tac i st = |
467 full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st; |
367 full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st; |
468 in |
368 in |
469 fun refute_tac test prep_tac ref_tac = |
369 fun refute_tac test prep_tac ref_tac = |
470 let val refute_prems_tac = |
370 let val refute_prems_tac = |
471 REPEAT_DETERM |
371 REPEAT_DETERM |
472 (eresolve_tac [conjE, exE] 1 ORELSE |
372 (eresolve_tac [HOL.conjE, HOL.exE] 1 ORELSE |
473 filter_prems_tac test 1 ORELSE |
373 filter_prems_tac test 1 ORELSE |
474 etac disjE 1) THEN |
374 etac HOL.disjE 1) THEN |
475 ((etac notE 1 THEN eq_assume_tac 1) ORELSE |
375 ((etac HOL.notE 1 THEN eq_assume_tac 1) ORELSE |
476 ref_tac 1); |
376 ref_tac 1); |
477 in EVERY'[TRY o filter_prems_tac test, |
377 in EVERY'[TRY o filter_prems_tac test, |
478 REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, |
378 REPEAT_DETERM o etac HOL.rev_mp, prep_tac, rtac HOL.ccontr, prem_nnf_tac, |
479 SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] |
379 SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] |
480 end; |
380 end; |
481 end; |
381 end; |