author | paulson |
Thu, 05 Sep 1996 10:23:55 +0200 | |
changeset 1948 | 78e5bfcbc1e9 |
parent 1922 | ce495557ac33 |
child 1968 | daa97cc96feb |
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 |
||
6 |
Instantiation of the generic simplifier |
|
7 |
*) |
|
8 |
||
9 |
open Simplifier; |
|
10 |
||
1922 | 11 |
(*** Integration of simplifier with classical reasoner ***) |
12 |
||
13 |
(*Add a simpset to a classical set!*) |
|
14 |
infix 4 addss; |
|
15 |
fun cs addss ss = cs addbefore asm_full_simp_tac ss 1; |
|
16 |
||
17 |
fun Addss ss = (claset := !claset addbefore asm_full_simp_tac ss 1); |
|
18 |
||
19 |
(*Maybe swap the safe_tac and simp_tac lines?**) |
|
20 |
fun auto_tac (cs,ss) = |
|
21 |
TRY (safe_tac cs) THEN |
|
22 |
ALLGOALS (asm_full_simp_tac ss) THEN |
|
23 |
REPEAT (FIRSTGOAL (best_tac (cs addss ss))); |
|
24 |
||
25 |
fun Auto_tac() = auto_tac (!claset, !simpset); |
|
26 |
||
27 |
fun auto() = by (Auto_tac()); |
|
28 |
||
29 |
||
923 | 30 |
local |
31 |
||
1922 | 32 |
fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); |
923 | 33 |
|
1922 | 34 |
val P_imp_P_iff_True = prover "P --> (P = True)" RS mp; |
35 |
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; |
|
923 | 36 |
|
1922 | 37 |
val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp; |
38 |
val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection; |
|
923 | 39 |
|
1922 | 40 |
fun atomize pairs = |
41 |
let fun atoms th = |
|
42 |
(case concl_of th of |
|
43 |
Const("Trueprop",_) $ p => |
|
44 |
(case head_of p of |
|
45 |
Const(a,_) => |
|
46 |
(case assoc(pairs,a) of |
|
47 |
Some(rls) => flat (map atoms ([th] RL rls)) |
|
48 |
| None => [th]) |
|
49 |
| _ => [th]) |
|
50 |
| _ => [th]) |
|
51 |
in atoms end; |
|
923 | 52 |
|
1922 | 53 |
fun mk_meta_eq r = case concl_of r of |
54 |
Const("==",_)$_$_ => r |
|
55 |
| _$(Const("op =",_)$_$_) => r RS eq_reflection |
|
56 |
| _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False |
|
57 |
| _ => r RS P_imp_P_eq_True; |
|
58 |
(* last 2 lines requires all formulae to be of the from Trueprop(.) *) |
|
923 | 59 |
|
1922 | 60 |
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
923 | 61 |
|
1922 | 62 |
val simp_thms = map prover |
63 |
[ "(x=x) = True", |
|
64 |
"(~True) = False", "(~False) = True", "(~ ~ P) = P", |
|
65 |
"(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))", |
|
66 |
"(True=P) = P", "(P=True) = P", |
|
67 |
"(True --> P) = P", "(False --> P) = True", |
|
68 |
"(P --> True) = True", "(P --> P) = True", |
|
69 |
"(P --> False) = (~P)", "(P --> ~P) = (~P)", |
|
70 |
"(P & True) = P", "(True & P) = P", |
|
71 |
"(P & False) = False", "(False & P) = False", "(P & P) = P", |
|
72 |
"(P | True) = True", "(True | P) = True", |
|
73 |
"(P | False) = P", "(False | P) = P", "(P | P) = P", |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
74 |
"((~P) = (~Q)) = (P=Q)", |
1922 | 75 |
"(!x.P) = P", "(? x.P) = P", "? x. x=t", |
76 |
"(? x. x=t & P(x)) = P(t)", "(! x. x=t --> P(x)) = P(t)" ]; |
|
923 | 77 |
|
78 |
in |
|
79 |
||
80 |
val meta_eq_to_obj_eq = prove_goal HOL.thy "x==y ==> x=y" |
|
81 |
(fn [prem] => [rewtac prem, rtac refl 1]); |
|
82 |
||
83 |
val eq_sym_conv = prover "(x=y) = (y=x)"; |
|
84 |
||
85 |
val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))"; |
|
86 |
||
1922 | 87 |
val disj_assoc = prover "((P|Q)|R) = (P|(Q|R))"; |
88 |
||
89 |
val imp_disj = prover "(P|Q --> R) = ((P-->R)&(Q-->R))"; |
|
90 |
||
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
91 |
(*Avoids duplication of subgoals after expand_if, when the true and false |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
92 |
cases boil down to the same thing.*) |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
93 |
val cases_simp = prover "((P --> Q) & (~P --> Q)) = Q"; |
1922 | 94 |
|
965 | 95 |
val if_True = prove_goalw HOL.thy [if_def] "(if True then x else y) = x" |
923 | 96 |
(fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]); |
97 |
||
965 | 98 |
val if_False = prove_goalw HOL.thy [if_def] "(if False then x else y) = y" |
923 | 99 |
(fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]); |
100 |
||
965 | 101 |
val if_P = prove_goal HOL.thy "P ==> (if P then x else y) = x" |
923 | 102 |
(fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]); |
103 |
||
965 | 104 |
val if_not_P = prove_goal HOL.thy "~P ==> (if P then x else y) = y" |
923 | 105 |
(fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]); |
106 |
||
107 |
val expand_if = prove_goal HOL.thy |
|
965 | 108 |
"P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" |
923 | 109 |
(fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1), |
1465 | 110 |
rtac (if_P RS ssubst) 2, |
111 |
rtac (if_not_P RS ssubst) 1, |
|
112 |
REPEAT(fast_tac HOL_cs 1) ]); |
|
923 | 113 |
|
965 | 114 |
val if_bool_eq = prove_goal HOL.thy |
115 |
"(if P then Q else R) = ((P-->Q) & (~P-->R))" |
|
116 |
(fn _ => [rtac expand_if 1]); |
|
923 | 117 |
|
988 | 118 |
(*Add congruence rules for = (instead of ==) *) |
119 |
infix 4 addcongs; |
|
923 | 120 |
fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); |
121 |
||
1264 | 122 |
fun Addcongs congs = (simpset := !simpset addcongs congs); |
123 |
||
923 | 124 |
val mksimps_pairs = |
125 |
[("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
|
126 |
("All", [spec]), ("True", []), ("False", []), |
|
965 | 127 |
("If", [if_bool_eq RS iffD1])]; |
923 | 128 |
|
129 |
fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all; |
|
130 |
||
1922 | 131 |
val imp_cong = impI RSN |
132 |
(2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" |
|
133 |
(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp); |
|
134 |
||
135 |
val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))" |
|
136 |
(fn _ => [rtac refl 1]); |
|
137 |
||
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
138 |
(*Miniscoping: pushing in existential quantifiers*) |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
139 |
val ex_simps = map prover |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
140 |
["(EX x. P x & Q) = ((EX x.P x) & Q)", |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
141 |
"(EX x. P & Q x) = (P & (EX x.Q x))", |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
142 |
"(EX x. P x | Q) = ((EX x.P x) | Q)", |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
143 |
"(EX x. P | Q x) = (P | (EX x.Q x))", |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
144 |
"(EX x. P x --> Q) = ((ALL x.P x) --> Q)", |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
145 |
"(EX x. P --> Q x) = (P --> (EX x.Q x))"]; |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
146 |
|
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
147 |
(*Miniscoping: pushing in universal quantifiers*) |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
148 |
val all_simps = map prover |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
149 |
["(ALL x. P x & Q) = ((ALL x.P x) & Q)", |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
150 |
"(ALL x. P & Q x) = (P & (ALL x.Q x))", |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
151 |
"(ALL x. P x | Q) = ((ALL x.P x) | Q)", |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
152 |
"(ALL x. P | Q x) = (P | (ALL x.Q x))", |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
153 |
"(ALL x. P x --> Q) = ((EX x.P x) --> Q)", |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
154 |
"(ALL x. P --> Q x) = (P --> (ALL x.Q x))"]; |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
155 |
|
923 | 156 |
val HOL_ss = empty_ss |
157 |
setmksimps (mksimps mksimps_pairs) |
|
158 |
setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac |
|
159 |
ORELSE' etac FalseE) |
|
160 |
setsubgoaler asm_simp_tac |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
161 |
addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc, |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
162 |
cases_simp] |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
163 |
@ ex_simps @ all_simps @ simp_thms) |
923 | 164 |
addcongs [imp_cong]; |
165 |
||
1922 | 166 |
|
167 |
(*In general it seems wrong to add distributive laws by default: they |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
168 |
might cause exponential blow-up. But imp_disj has been in for a while |
1922 | 169 |
and cannot be removed without affecting existing proofs. Moreover, |
170 |
rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the |
|
171 |
grounds that it allows simplification of R in the two cases.*) |
|
172 |
||
173 |
||
941 | 174 |
local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) |
175 |
in |
|
176 |
fun split_tac splits = mktac (map mk_meta_eq splits) |
|
177 |
end; |
|
178 |
||
1722 | 179 |
local val mktac = mk_case_split_inside_tac (meta_eq_to_obj_eq RS iffD2) |
180 |
in |
|
181 |
fun split_inside_tac splits = mktac (map mk_meta_eq splits) |
|
182 |
end; |
|
183 |
||
923 | 184 |
|
185 |
(* eliminiation of existential quantifiers in assumptions *) |
|
186 |
||
187 |
val ex_all_equiv = |
|
188 |
let val lemma1 = prove_goal HOL.thy |
|
189 |
"(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)" |
|
190 |
(fn prems => [resolve_tac prems 1, etac exI 1]); |
|
191 |
val lemma2 = prove_goalw HOL.thy [Ex_def] |
|
192 |
"(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)" |
|
193 |
(fn prems => [REPEAT(resolve_tac prems 1)]) |
|
194 |
in equal_intr lemma1 lemma2 end; |
|
195 |
||
196 |
(* '&' congruence rule: not included by default! |
|
197 |
May slow rewrite proofs down by as much as 50% *) |
|
198 |
||
199 |
val conj_cong = impI RSN |
|
200 |
(2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" |
|
1465 | 201 |
(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp); |
923 | 202 |
|
1548 | 203 |
val rev_conj_cong = impI RSN |
204 |
(2, prove_goal HOL.thy "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" |
|
205 |
(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp); |
|
206 |
||
923 | 207 |
(** 'if' congruence rules: neither included by default! *) |
208 |
||
209 |
(*Simplifies x assuming c and y assuming ~c*) |
|
210 |
val if_cong = prove_goal HOL.thy |
|
965 | 211 |
"[| b=c; c ==> x=u; ~c ==> y=v |] ==>\ |
212 |
\ (if b then x else y) = (if c then u else v)" |
|
923 | 213 |
(fn rew::prems => |
214 |
[stac rew 1, stac expand_if 1, stac expand_if 1, |
|
215 |
fast_tac (HOL_cs addDs prems) 1]); |
|
216 |
||
217 |
(*Prevents simplification of x and y: much faster*) |
|
218 |
val if_weak_cong = prove_goal HOL.thy |
|
965 | 219 |
"b=c ==> (if b then x else y) = (if c then x else y)" |
923 | 220 |
(fn [prem] => [rtac (prem RS arg_cong) 1]); |
221 |
||
222 |
(*Prevents simplification of t: much faster*) |
|
223 |
val let_weak_cong = prove_goal HOL.thy |
|
224 |
"a = b ==> (let x=a in t(x)) = (let x=b in t(x))" |
|
225 |
(fn [prem] => [rtac (prem RS arg_cong) 1]); |
|
226 |
||
227 |
end; |
|
228 |
||
229 |
fun prove nm thm = qed_goal nm HOL.thy thm (fn _ => [fast_tac HOL_cs 1]); |
|
230 |
||
231 |
prove "conj_commute" "(P&Q) = (Q&P)"; |
|
232 |
prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
|
233 |
val conj_comms = [conj_commute, conj_left_commute]; |
|
234 |
||
1922 | 235 |
prove "disj_commute" "(P|Q) = (Q|P)"; |
236 |
prove "disj_left_commute" "(P|(Q|R)) = (Q|(P|R))"; |
|
237 |
val disj_comms = [disj_commute, disj_left_commute]; |
|
238 |
||
923 | 239 |
prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)"; |
240 |
prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)"; |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
241 |
|
1892 | 242 |
prove "disj_conj_distribL" "(P|(Q&R)) = ((P|Q) & (P|R))"; |
243 |
prove "disj_conj_distribR" "((P&Q)|R) = ((P|R) & (Q|R))"; |
|
244 |
||
245 |
prove "imp_conj_distrib" "(P --> (Q&R)) = ((P-->Q) & (P-->R))"; |
|
1922 | 246 |
prove "imp_conj" "((P&Q)-->R) = (P --> (Q --> R))"; |
1892 | 247 |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
248 |
prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)"; |
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
249 |
prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)"; |
1922 | 250 |
prove "not_iff" "(P~=Q) = (P = (~Q))"; |
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
251 |
|
1660 | 252 |
prove "not_all" "(~ (! x.P(x))) = (? x.~P(x))"; |
1922 | 253 |
prove "imp_all" "((! x. P x) --> Q) = (? x. P x --> Q)"; |
1660 | 254 |
prove "not_ex" "(~ (? x.P(x))) = (! x.~P(x))"; |
1922 | 255 |
prove "imp_ex" "((? x. P x) --> Q) = (! x. P x --> Q)"; |
1660 | 256 |
|
1655 | 257 |
prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))"; |
258 |
prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; |
|
259 |
||
1758 | 260 |
|
1655 | 261 |
qed_goal "if_cancel" HOL.thy "(if c then x else x) = x" |
262 |
(fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); |
|
263 |
||
264 |
qed_goal "if_distrib" HOL.thy |
|
265 |
"f(if c then x else y) = (if c then f x else f y)" |
|
266 |
(fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); |
|
267 |
||
1874 | 268 |
qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = (f o g o h)" |
1655 | 269 |
(fn _=>[rtac ext 1, rtac refl 1]); |