author | wenzelm |
Thu, 22 Dec 2005 00:28:36 +0100 | |
changeset 18457 | 356a9f711899 |
parent 18407 | fa075b606571 |
child 18529 | 540da2415751 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/simpdata.ML |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
923 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
5304 | 6 |
Instantiation of the generic simplifier for HOL. |
923 | 7 |
*) |
8 |
||
12281 | 9 |
(* legacy ML bindings *) |
3904 | 10 |
|
12281 | 11 |
val Eq_FalseI = thm "Eq_FalseI"; |
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"; |
|
24 |
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"; |
|
53 |
val imp_all = thm "imp_all"; |
|
54 |
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"; |
|
58 |
val imp_disj1 = thm "imp_disj1"; |
|
59 |
val imp_disj2 = thm "imp_disj2"; |
|
60 |
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"; |
|
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
72 |
val simp_impliesE = thm "simp_impliesI"; |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
73 |
val simp_impliesI = thm "simp_impliesI"; |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
74 |
val simp_implies_cong = thm "simp_implies_cong"; |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
75 |
val simp_implies_def = thm "simp_implies_def"; |
12281 | 76 |
val simp_thms = thms "simp_thms"; |
77 |
val split_if = thm "split_if"; |
|
78 |
val split_if_asm = thm "split_if_asm"; |
|
14749 | 79 |
val atomize_not = thm"atomize_not"; |
2134 | 80 |
|
11232 | 81 |
local |
82 |
val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R" |
|
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]) |
|
12524
66eb843b1d35
mods due to mor powerful simprocs for 1-point rules (quantifier1).
nipkow
parents:
12475
diff
changeset
|
88 |
val iff_exI = allI RS |
66eb843b1d35
mods due to mor powerful simprocs for 1-point rules (quantifier1).
nipkow
parents:
12475
diff
changeset
|
89 |
prove_goal (the_context()) "!x. P x = Q x ==> (? x. P x) = (? x. Q x)" |
66eb843b1d35
mods due to mor powerful simprocs for 1-point rules (quantifier1).
nipkow
parents:
12475
diff
changeset
|
90 |
(fn prems => [cut_facts_tac prems 1, Blast_tac 1]) |
66eb843b1d35
mods due to mor powerful simprocs for 1-point rules (quantifier1).
nipkow
parents:
12475
diff
changeset
|
91 |
|
66eb843b1d35
mods due to mor powerful simprocs for 1-point rules (quantifier1).
nipkow
parents:
12475
diff
changeset
|
92 |
val all_comm = prove_goal (the_context()) "(!x y. P x y) = (!y x. P x y)" |
66eb843b1d35
mods due to mor powerful simprocs for 1-point rules (quantifier1).
nipkow
parents:
12475
diff
changeset
|
93 |
(fn _ => [Blast_tac 1]) |
66eb843b1d35
mods due to mor powerful simprocs for 1-point rules (quantifier1).
nipkow
parents:
12475
diff
changeset
|
94 |
val ex_comm = prove_goal (the_context()) "(? x y. P x y) = (? y x. P x y)" |
66eb843b1d35
mods due to mor powerful simprocs for 1-point rules (quantifier1).
nipkow
parents:
12475
diff
changeset
|
95 |
(fn _ => [Blast_tac 1]) |
11232 | 96 |
in |
4351 | 97 |
|
98 |
(*** make simplification procedures for quantifier elimination ***) |
|
99 |
||
9851 | 100 |
structure Quantifier1 = Quantifier1Fun |
101 |
(struct |
|
4351 | 102 |
(*abstract syntax*) |
15531 | 103 |
fun dest_eq((c as Const("op =",_)) $ s $ t) = SOME(c,s,t) |
104 |
| dest_eq _ = NONE; |
|
105 |
fun dest_conj((c as Const("op &",_)) $ s $ t) = SOME(c,s,t) |
|
106 |
| dest_conj _ = NONE; |
|
107 |
fun dest_imp((c as Const("op -->",_)) $ s $ t) = SOME(c,s,t) |
|
108 |
| dest_imp _ = NONE; |
|
4351 | 109 |
val conj = HOLogic.conj |
110 |
val imp = HOLogic.imp |
|
111 |
(*rules*) |
|
112 |
val iff_reflection = eq_reflection |
|
113 |
val iffI = iffI |
|
12524
66eb843b1d35
mods due to mor powerful simprocs for 1-point rules (quantifier1).
nipkow
parents:
12475
diff
changeset
|
114 |
val iff_trans = trans |
4351 | 115 |
val conjI= conjI |
116 |
val conjE= conjE |
|
117 |
val impI = impI |
|
118 |
val mp = mp |
|
11232 | 119 |
val uncurry = uncurry |
4351 | 120 |
val exI = exI |
121 |
val exE = exE |
|
11232 | 122 |
val iff_allI = iff_allI |
12524
66eb843b1d35
mods due to mor powerful simprocs for 1-point rules (quantifier1).
nipkow
parents:
12475
diff
changeset
|
123 |
val iff_exI = iff_exI |
66eb843b1d35
mods due to mor powerful simprocs for 1-point rules (quantifier1).
nipkow
parents:
12475
diff
changeset
|
124 |
val all_comm = all_comm |
66eb843b1d35
mods due to mor powerful simprocs for 1-point rules (quantifier1).
nipkow
parents:
12475
diff
changeset
|
125 |
val ex_comm = ex_comm |
4351 | 126 |
end); |
127 |
||
11232 | 128 |
end; |
129 |
||
13462 | 130 |
val defEX_regroup = |
131 |
Simplifier.simproc (Theory.sign_of (the_context ())) |
|
132 |
"defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; |
|
133 |
||
134 |
val defALL_regroup = |
|
135 |
Simplifier.simproc (Theory.sign_of (the_context ())) |
|
136 |
"defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; |
|
3913 | 137 |
|
17778 | 138 |
|
139 |
(*** simproc for proving "(y = x) == False" from prmise "~(x = y)" ***) |
|
140 |
||
141 |
val use_neq_simproc = ref true; |
|
142 |
||
143 |
local |
|
144 |
||
145 |
val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI; |
|
146 |
||
147 |
fun neq_prover sg ss (eq $ lhs $ rhs) = |
|
148 |
let |
|
149 |
fun test thm = (case #prop(rep_thm thm) of |
|
150 |
_ $ (Not $ (eq' $ l' $ r')) => |
|
151 |
Not = HOLogic.Not andalso eq' = eq andalso |
|
152 |
r' aconv lhs andalso l' aconv rhs |
|
153 |
| _ => false) |
|
154 |
in |
|
155 |
if !use_neq_simproc then |
|
156 |
case Library.find_first test (prems_of_ss ss) of NONE => NONE |
|
157 |
| SOME thm => SOME (thm RS neq_to_EQ_False) |
|
158 |
else NONE |
|
159 |
end |
|
160 |
||
161 |
in |
|
162 |
||
163 |
val neq_simproc = |
|
164 |
Simplifier.simproc (the_context ()) "neq_simproc" ["x = y"] neq_prover; |
|
165 |
||
166 |
end; |
|
167 |
||
168 |
||
169 |
||
170 |
||
15423 | 171 |
(*** Simproc for Let ***) |
172 |
||
173 |
val use_let_simproc = ref true; |
|
174 |
||
175 |
local |
|
176 |
val Let_folded = thm "Let_folded"; |
|
177 |
val Let_unfold = thm "Let_unfold"; |
|
178 |
||
179 |
val f_Let_unfold = |
|
180 |
let val [(_$(f$_)$_)] = prems_of Let_unfold in cterm_of (sign_of (the_context ())) f end |
|
181 |
val f_Let_folded = |
|
182 |
let val [(_$(f$_)$_)] = prems_of Let_folded in cterm_of (sign_of (the_context ())) f end; |
|
183 |
val g_Let_folded = |
|
184 |
let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (sign_of (the_context ())) g end; |
|
185 |
in |
|
186 |
val let_simproc = |
|
187 |
Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"] |
|
188 |
(fn sg => fn ss => fn t => |
|
189 |
(case t of (Const ("Let",_)$x$f) => (* x and f are already in normal form *) |
|
15531 | 190 |
if not (!use_let_simproc) then NONE |
15423 | 191 |
else if is_Free x orelse is_Bound x orelse is_Const x |
15531 | 192 |
then SOME Let_def |
15423 | 193 |
else |
194 |
let |
|
195 |
val n = case f of (Abs (x,_,_)) => x | _ => "x"; |
|
196 |
val cx = cterm_of sg x; |
|
197 |
val {T=xT,...} = rep_cterm cx; |
|
198 |
val cf = cterm_of sg f; |
|
199 |
val fx_g = Simplifier.rewrite ss (Thm.capply cf cx); |
|
200 |
val (_$_$g) = prop_of fx_g; |
|
201 |
val g' = abstract_over (x,g); |
|
202 |
in (if (g aconv g') |
|
203 |
then |
|
204 |
let |
|
205 |
val rl = cterm_instantiate [(f_Let_unfold,cf)] Let_unfold; |
|
15531 | 206 |
in SOME (rl OF [fx_g]) end |
18176 | 207 |
else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*) |
15423 | 208 |
else let |
209 |
val abs_g'= Abs (n,xT,g'); |
|
210 |
val g'x = abs_g'$x; |
|
211 |
val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x)); |
|
212 |
val rl = cterm_instantiate |
|
213 |
[(f_Let_folded,cterm_of sg f), |
|
214 |
(g_Let_folded,cterm_of sg abs_g')] |
|
215 |
Let_folded; |
|
15531 | 216 |
in SOME (rl OF [transitive fx_g g_g'x]) end) |
15423 | 217 |
end |
15531 | 218 |
| _ => NONE)) |
15423 | 219 |
end |
4351 | 220 |
|
221 |
(*** Case splitting ***) |
|
3913 | 222 |
|
12278 | 223 |
(*Make meta-equalities. The operator below is Trueprop*) |
224 |
||
13600
9702c8636a7b
Removed nRS again because extract_rews now takes care of preserving names.
berghofe
parents:
13568
diff
changeset
|
225 |
fun mk_meta_eq r = r RS eq_reflection; |
12278 | 226 |
fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; |
227 |
||
228 |
fun mk_eq th = case concl_of th of |
|
229 |
Const("==",_)$_$_ => th |
|
230 |
| _$(Const("op =",_)$_$_) => mk_meta_eq th |
|
13600
9702c8636a7b
Removed nRS again because extract_rews now takes care of preserving names.
berghofe
parents:
13568
diff
changeset
|
231 |
| _$(Const("Not",_)$_) => th RS Eq_FalseI |
9702c8636a7b
Removed nRS again because extract_rews now takes care of preserving names.
berghofe
parents:
13568
diff
changeset
|
232 |
| _ => th RS Eq_TrueI; |
13568
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset
|
233 |
(* Expects Trueprop(.) if not == *) |
12278 | 234 |
|
235 |
fun mk_eq_True r = |
|
15531 | 236 |
SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE; |
12278 | 237 |
|
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
238 |
(* Produce theorems of the form |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
239 |
(P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
240 |
*) |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
241 |
fun lift_meta_eq_to_obj_eq i st = |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
242 |
let |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
243 |
val {sign, ...} = rep_thm st; |
17197 | 244 |
fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
245 |
| count_imp _ = 0; |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
246 |
val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1))) |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
247 |
in if j = 0 then meta_eq_to_obj_eq |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
248 |
else |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
249 |
let |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
250 |
val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
251 |
fun mk_simp_implies Q = foldr (fn (R, S) => |
17197 | 252 |
Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
253 |
val aT = TFree ("'a", HOLogic.typeS); |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
254 |
val x = Free ("x", aT); |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
255 |
val y = Free ("y", aT) |
17985 | 256 |
in standard (Goal.prove (Thm.theory_of_thm st) [] |
257 |
[mk_simp_implies (Logic.mk_equals (x, y))] |
|
258 |
(mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))) |
|
259 |
(fn prems => EVERY |
|
260 |
[rewrite_goals_tac [simp_implies_def], |
|
261 |
REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])) |
|
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
262 |
end |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
263 |
end; |
17985 | 264 |
|
12278 | 265 |
(*Congruence rules for = (instead of ==)*) |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
266 |
fun mk_meta_cong rl = zero_var_indexes |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
267 |
(let val rl' = Seq.hd (TRYALL (fn i => fn st => |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
268 |
rtac (lift_meta_eq_to_obj_eq i st) i st) rl) |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
269 |
in mk_meta_eq rl' handle THM _ => |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
270 |
if Logic.is_equals (concl_of rl') then rl' |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
271 |
else error "Conclusion of congruence rules must be =-equality" |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
272 |
end); |
12278 | 273 |
|
274 |
(* Elimination of True from asumptions: *) |
|
275 |
||
276 |
local fun rd s = read_cterm (sign_of (the_context())) (s, propT); |
|
277 |
in val True_implies_equals = standard' (equal_intr |
|
278 |
(implies_intr_hyps (implies_elim (assume (rd "True ==> PROP P")) TrueI)) |
|
279 |
(implies_intr_hyps (implies_intr (rd "True") (assume (rd "PROP P"))))); |
|
280 |
end; |
|
281 |
||
282 |
||
5304 | 283 |
structure SplitterData = |
284 |
struct |
|
285 |
structure Simplifier = Simplifier |
|
5552 | 286 |
val mk_eq = mk_eq |
5304 | 287 |
val meta_eq_to_iff = meta_eq_to_obj_eq |
288 |
val iffD = iffD2 |
|
289 |
val disjE = disjE |
|
290 |
val conjE = conjE |
|
291 |
val exE = exE |
|
10231 | 292 |
val contrapos = contrapos_nn |
293 |
val contrapos2 = contrapos_pp |
|
5304 | 294 |
val notnotD = notnotD |
295 |
end; |
|
4681 | 296 |
|
5304 | 297 |
structure Splitter = SplitterFun(SplitterData); |
2263 | 298 |
|
5304 | 299 |
val split_tac = Splitter.split_tac; |
300 |
val split_inside_tac = Splitter.split_inside_tac; |
|
301 |
val split_asm_tac = Splitter.split_asm_tac; |
|
5307 | 302 |
val op addsplits = Splitter.addsplits; |
303 |
val op delsplits = Splitter.delsplits; |
|
5304 | 304 |
val Addsplits = Splitter.Addsplits; |
305 |
val Delsplits = Splitter.Delsplits; |
|
4718
fc2ba9fb2135
new rewrite rules not1_or, not2_or, and if_eq_cancel
oheimb
parents:
4681
diff
changeset
|
306 |
|
2134 | 307 |
val mksimps_pairs = |
308 |
[("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
|
309 |
("All", [spec]), ("True", []), ("False", []), |
|
16587 | 310 |
("HOL.If", [if_bool_eq_conj RS iffD1])]; |
1758 | 311 |
|
13568
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset
|
312 |
(* |
5304 | 313 |
val mk_atomize: (string * thm list) list -> thm -> thm list |
13568
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset
|
314 |
looks too specific to move it somewhere else |
5304 | 315 |
*) |
316 |
fun mk_atomize pairs = |
|
317 |
let fun atoms th = |
|
318 |
(case concl_of th of |
|
319 |
Const("Trueprop",_) $ p => |
|
320 |
(case head_of p of |
|
321 |
Const(a,_) => |
|
17325 | 322 |
(case AList.lookup (op =) pairs a of |
15570 | 323 |
SOME(rls) => List.concat (map atoms ([th] RL rls)) |
15531 | 324 |
| NONE => [th]) |
5304 | 325 |
| _ => [th]) |
326 |
| _ => [th]) |
|
327 |
in atoms end; |
|
328 |
||
11624
8a45c7abef04
mksimps and mk_eq_True no longer raise THM exception.
berghofe
parents:
11534
diff
changeset
|
329 |
fun mksimps pairs = |
15570 | 330 |
(List.mapPartial (try mk_eq) o mk_atomize pairs o gen_all); |
5304 | 331 |
|
7570 | 332 |
fun unsafe_solver_tac prems = |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
333 |
(fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' |
7570 | 334 |
FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE]; |
335 |
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; |
|
336 |
||
2636
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset
|
337 |
(*No premature instantiation of variables during simplification*) |
7570 | 338 |
fun safe_solver_tac prems = |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
339 |
(fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' |
7570 | 340 |
FIRST'[match_tac(reflexive_thm::TrueI::refl::prems), |
341 |
eq_assume_tac, ematch_tac [FalseE]]; |
|
342 |
val safe_solver = mk_solver "HOL safe" safe_solver_tac; |
|
2443
a81d4c219c3c
factored out HOL_base_ss and val HOL_min_ss, added HOL_safe_min_ss
oheimb
parents:
2263
diff
changeset
|
343 |
|
9713 | 344 |
val HOL_basic_ss = |
17892 | 345 |
Simplifier.theory_context (the_context ()) empty_ss |
346 |
setsubgoaler asm_simp_tac |
|
9713 | 347 |
setSSolver safe_solver |
348 |
setSolver unsafe_solver |
|
349 |
setmksimps (mksimps mksimps_pairs) |
|
350 |
setmkeqTrue mk_eq_True |
|
351 |
setmkcong mk_meta_cong; |
|
2443
a81d4c219c3c
factored out HOL_base_ss and val HOL_min_ss, added HOL_safe_min_ss
oheimb
parents:
2263
diff
changeset
|
352 |
|
18324 | 353 |
fun unfold_tac ths = |
354 |
let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths |
|
355 |
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end; |
|
17003 | 356 |
|
13568
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset
|
357 |
(*In general it seems wrong to add distributive laws by default: they |
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset
|
358 |
might cause exponential blow-up. But imp_disjL has been in for a while |
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset
|
359 |
and cannot be removed without affecting existing proofs. Moreover, |
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset
|
360 |
rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the |
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset
|
361 |
grounds that it allows simplification of R in the two cases.*) |
6b12df05f358
preserve names of rewrite rules when transforming them
nipkow
parents:
13462
diff
changeset
|
362 |
|
9713 | 363 |
val HOL_ss = |
364 |
HOL_basic_ss addsimps |
|
3446
a14e5451f613
Addition of not_imp (which pushes negation into implication) as a default
paulson
parents:
3282
diff
changeset
|
365 |
([triv_forall_equality, (* prunes params *) |
3654 | 366 |
True_implies_equals, (* prune asms `True' *) |
4718
fc2ba9fb2135
new rewrite rules not1_or, not2_or, and if_eq_cancel
oheimb
parents:
4681
diff
changeset
|
367 |
if_True, if_False, if_cancel, if_eq_cancel, |
5304 | 368 |
imp_disjL, conj_assoc, disj_assoc, |
3904 | 369 |
de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp, |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11434
diff
changeset
|
370 |
disj_not1, not_all, not_ex, cases_simp, |
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
13743
diff
changeset
|
371 |
thm "the_eq_trivial", the_sym_eq_trivial] |
3446
a14e5451f613
Addition of not_imp (which pushes negation into implication) as a default
paulson
parents:
3282
diff
changeset
|
372 |
@ ex_simps @ all_simps @ simp_thms) |
17778 | 373 |
addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc] |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
374 |
addcongs [imp_cong, simp_implies_cong] |
4830 | 375 |
addsplits [split_if]; |
2082 | 376 |
|
11034 | 377 |
fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); |
378 |
||
379 |
||
6293 | 380 |
(*Simplifies x assuming c and y assuming ~c*) |
381 |
val prems = Goalw [if_def] |
|
382 |
"[| b=c; c ==> x=u; ~c ==> y=v |] ==> \ |
|
383 |
\ (if b then x else y) = (if c then u else v)"; |
|
384 |
by (asm_simp_tac (HOL_ss addsimps prems) 1); |
|
385 |
qed "if_cong"; |
|
386 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7031
diff
changeset
|
387 |
(*Prevents simplification of x and y: faster and allows the execution |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7031
diff
changeset
|
388 |
of functional programs. NOW THE DEFAULT.*) |
7031 | 389 |
Goal "b=c ==> (if b then x else y) = (if c then x else y)"; |
390 |
by (etac arg_cong 1); |
|
391 |
qed "if_weak_cong"; |
|
6293 | 392 |
|
393 |
(*Prevents simplification of t: much faster*) |
|
7031 | 394 |
Goal "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"; |
395 |
by (etac arg_cong 1); |
|
396 |
qed "let_weak_cong"; |
|
6293 | 397 |
|
12975 | 398 |
(*To tidy up the result of a simproc. Only the RHS will be simplified.*) |
399 |
Goal "u = u' ==> (t==u) == (t==u')"; |
|
400 |
by (asm_simp_tac HOL_ss 1); |
|
401 |
qed "eq_cong2"; |
|
402 |
||
7031 | 403 |
Goal "f(if c then x else y) = (if c then f x else f y)"; |
404 |
by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1); |
|
405 |
qed "if_distrib"; |
|
1655 | 406 |
|
4327 | 407 |
(*For expand_case_tac*) |
7584 | 408 |
val prems = Goal "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; |
2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
409 |
by (case_tac "P" 1); |
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
410 |
by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems))); |
7584 | 411 |
qed "expand_case"; |
2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
412 |
|
4327 | 413 |
(*Used in Auth proofs. Typically P contains Vars that become instantiated |
414 |
during unification.*) |
|
2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
415 |
fun expand_case_tac P i = |
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
416 |
res_inst_tac [("P",P)] expand_case i THEN |
9713 | 417 |
Simp_tac (i+1) THEN |
2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
418 |
Simp_tac i; |
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
419 |
|
7584 | 420 |
(*This lemma restricts the effect of the rewrite rule u=v to the left-hand |
421 |
side of an equality. Used in {Integ,Real}/simproc.ML*) |
|
422 |
Goal "x=y ==> (x=z) = (y=z)"; |
|
423 |
by (asm_simp_tac HOL_ss 1); |
|
424 |
qed "restrict_to_left"; |
|
2948
f18035b1d531
Moved expand_case_tac from Auth/Message.ML to simpdata.ML
paulson
parents:
2935
diff
changeset
|
425 |
|
7357 | 426 |
(* default simpset *) |
9713 | 427 |
val simpsetup = |
17875 | 428 |
[fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy)]; |
3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3577
diff
changeset
|
429 |
|
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4651
diff
changeset
|
430 |
|
5219 | 431 |
(*** integration of simplifier with classical reasoner ***) |
2636
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset
|
432 |
|
5219 | 433 |
structure Clasimp = ClasimpFun |
8473 | 434 |
(structure Simplifier = Simplifier and Splitter = Splitter |
9851 | 435 |
and Classical = Classical and Blast = Blast |
11344 | 436 |
val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE |
9851 | 437 |
val cla_make_elim = cla_make_elim); |
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
4651
diff
changeset
|
438 |
open Clasimp; |
2636
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset
|
439 |
|
4b30dbe4a020
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb
parents:
2595
diff
changeset
|
440 |
val HOL_css = (HOL_cs, HOL_ss); |
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
441 |
|
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
442 |
|
8641
978db2870862
change_global/local_css move to Provers/clasimp.ML;
wenzelm
parents:
8473
diff
changeset
|
443 |
|
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
444 |
(*** A general refutation procedure ***) |
9713 | 445 |
|
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
446 |
(* Parameters: |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
447 |
|
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
448 |
test: term -> bool |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
449 |
tests if a term is at all relevant to the refutation proof; |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
450 |
if not, then it can be discarded. Can improve performance, |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
451 |
esp. if disjunctions can be discarded (no case distinction needed!). |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
452 |
|
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
453 |
prep_tac: int -> tactic |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
454 |
A preparation tactic to be applied to the goal once all relevant premises |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
455 |
have been moved to the conclusion. |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
456 |
|
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
457 |
ref_tac: int -> tactic |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
458 |
the actual refutation tactic. Should be able to deal with goals |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
459 |
[| A1; ...; An |] ==> False |
9876 | 460 |
where the Ai are atomic, i.e. no top-level &, | or EX |
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
461 |
*) |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
462 |
|
15184 | 463 |
local |
464 |
val nnf_simpset = |
|
17892 | 465 |
empty_ss setmkeqTrue mk_eq_True |
466 |
setmksimps (mksimps mksimps_pairs) |
|
467 |
addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj, |
|
468 |
not_all,not_ex,not_not]; |
|
469 |
fun prem_nnf_tac i st = |
|
470 |
full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st; |
|
15184 | 471 |
in |
472 |
fun refute_tac test prep_tac ref_tac = |
|
473 |
let val refute_prems_tac = |
|
12475 | 474 |
REPEAT_DETERM |
475 |
(eresolve_tac [conjE, exE] 1 ORELSE |
|
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
476 |
filter_prems_tac test 1 ORELSE |
6301 | 477 |
etac disjE 1) THEN |
11200
f43fa07536c0
arith_tac now copes with propositional reasoning as well.
nipkow
parents:
11162
diff
changeset
|
478 |
((etac notE 1 THEN eq_assume_tac 1) ORELSE |
f43fa07536c0
arith_tac now copes with propositional reasoning as well.
nipkow
parents:
11162
diff
changeset
|
479 |
ref_tac 1); |
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
480 |
in EVERY'[TRY o filter_prems_tac test, |
12475 | 481 |
REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, |
5975
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
482 |
SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] |
cd19eaa90f45
Added a general refutation tactic which works by putting things into nnf first.
nipkow
parents:
5552
diff
changeset
|
483 |
end; |
17003 | 484 |
end; |