31 |
31 |
32 |
32 |
33 (*** Addition of rules to simpsets and clasets simultaneously ***) |
33 (*** Addition of rules to simpsets and clasets simultaneously ***) |
34 |
34 |
35 (*Takes UNCONDITIONAL theorems of the form A<->B to |
35 (*Takes UNCONDITIONAL theorems of the form A<->B to |
36 the Safe Intr rule B==>A and |
36 the Safe Intr rule B==>A and |
37 the Safe Destruct rule A==>B. |
37 the Safe Destruct rule A==>B. |
38 Also ~A goes to the Safe Elim rule A ==> ?R |
38 Also ~A goes to the Safe Elim rule A ==> ?R |
39 Failing other cases, A is added as a Safe Intr rule*) |
39 Failing other cases, A is added as a Safe Intr rule*) |
40 local |
40 local |
41 val iff_const = HOLogic.eq_const HOLogic.boolT; |
41 val iff_const = HOLogic.eq_const HOLogic.boolT; |
42 |
42 |
43 fun addIff th = |
43 fun addIff th = |
44 (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of |
44 (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of |
45 (Const("not",_) $ A) => |
45 (Const("not",_) $ A) => |
46 AddSEs [zero_var_indexes (th RS notE)] |
46 AddSEs [zero_var_indexes (th RS notE)] |
47 | (con $ _ $ _) => |
47 | (con $ _ $ _) => |
48 if con=iff_const |
48 if con=iff_const |
49 then (AddSIs [zero_var_indexes (th RS iffD2)]; |
49 then (AddSIs [zero_var_indexes (th RS iffD2)]; |
50 AddSDs [zero_var_indexes (th RS iffD1)]) |
50 AddSDs [zero_var_indexes (th RS iffD1)]) |
51 else AddSIs [th] |
51 else AddSIs [th] |
52 | _ => AddSIs [th]; |
52 | _ => AddSIs [th]; |
53 Addsimps [th]) |
53 Addsimps [th]) |
54 handle _ => error ("AddIffs: theorem must be unconditional\n" ^ |
54 handle _ => error ("AddIffs: theorem must be unconditional\n" ^ |
55 string_of_thm th) |
55 string_of_thm th) |
56 |
56 |
57 fun delIff th = |
57 fun delIff th = |
58 (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of |
58 (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of |
59 (Const("not",_) $ A) => |
59 (Const("not",_) $ A) => |
60 Delrules [zero_var_indexes (th RS notE)] |
60 Delrules [zero_var_indexes (th RS notE)] |
61 | (con $ _ $ _) => |
61 | (con $ _ $ _) => |
62 if con=iff_const |
62 if con=iff_const |
63 then Delrules [zero_var_indexes (th RS iffD2), |
63 then Delrules [zero_var_indexes (th RS iffD2), |
64 zero_var_indexes (th RS iffD1)] |
64 zero_var_indexes (th RS iffD1)] |
65 else Delrules [th] |
65 else Delrules [th] |
66 | _ => Delrules [th]; |
66 | _ => Delrules [th]; |
67 Delsimps [th]) |
67 Delsimps [th]) |
68 handle _ => warning("DelIffs: ignoring conditional theorem\n" ^ |
68 handle _ => warning("DelIffs: ignoring conditional theorem\n" ^ |
69 string_of_thm th) |
69 string_of_thm th) |
70 in |
70 in |
71 val AddIffs = seq addIff |
71 val AddIffs = seq addIff |
72 val DelIffs = seq delIff |
72 val DelIffs = seq delIff |
73 end; |
73 end; |
74 |
74 |
83 val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp; |
83 val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp; |
84 val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection; |
84 val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection; |
85 |
85 |
86 fun atomize pairs = |
86 fun atomize pairs = |
87 let fun atoms th = |
87 let fun atoms th = |
88 (case concl_of th of |
88 (case concl_of th of |
89 Const("Trueprop",_) $ p => |
89 Const("Trueprop",_) $ p => |
90 (case head_of p of |
90 (case head_of p of |
91 Const(a,_) => |
91 Const(a,_) => |
92 (case assoc(pairs,a) of |
92 (case assoc(pairs,a) of |
93 Some(rls) => flat (map atoms ([th] RL rls)) |
93 Some(rls) => flat (map atoms ([th] RL rls)) |
94 | None => [th]) |
94 | None => [th]) |
95 | _ => [th]) |
95 | _ => [th]) |
96 | _ => [th]) |
96 | _ => [th]) |
97 in atoms end; |
97 in atoms end; |
98 |
98 |
99 fun mk_meta_eq r = case concl_of r of |
99 fun mk_meta_eq r = case concl_of r of |
100 Const("==",_)$_$_ => r |
100 Const("==",_)$_$_ => r |
101 | _$(Const("op =",_)$_$_) => r RS eq_reflection |
101 | _$(Const("op =",_)$_$_) => r RS eq_reflection |
102 | _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False |
102 | _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False |
103 | _ => r RS P_imp_P_eq_True; |
103 | _ => r RS P_imp_P_eq_True; |
104 (* last 2 lines requires all formulae to be of the from Trueprop(.) *) |
104 (* last 2 lines requires all formulae to be of the from Trueprop(.) *) |
105 |
105 |
151 (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]); |
151 (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]); |
152 |
152 |
153 val expand_if = prove_goal HOL.thy |
153 val expand_if = prove_goal HOL.thy |
154 "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" |
154 "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" |
155 (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1), |
155 (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1), |
156 rtac (if_P RS ssubst) 2, |
156 stac if_P 2, |
157 rtac (if_not_P RS ssubst) 1, |
157 stac if_not_P 1, |
158 REPEAT(fast_tac HOL_cs 1) ]); |
158 REPEAT(fast_tac HOL_cs 1) ]); |
159 |
159 |
160 val if_bool_eq = prove_goal HOL.thy |
160 val if_bool_eq = prove_goal HOL.thy |
161 "(if P then Q else R) = ((P-->Q) & (~P-->R))" |
161 "(if P then Q else R) = ((P-->Q) & (~P-->R))" |
162 (fn _ => [rtac expand_if 1]); |
162 (fn _ => [rtac expand_if 1]); |
181 val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))" |
181 val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))" |
182 (fn _ => [rtac refl 1]); |
182 (fn _ => [rtac refl 1]); |
183 |
183 |
184 (*Miniscoping: pushing in existential quantifiers*) |
184 (*Miniscoping: pushing in existential quantifiers*) |
185 val ex_simps = map prover |
185 val ex_simps = map prover |
186 ["(EX x. P x & Q) = ((EX x.P x) & Q)", |
186 ["(EX x. P x & Q) = ((EX x.P x) & Q)", |
187 "(EX x. P & Q x) = (P & (EX x.Q x))", |
187 "(EX x. P & Q x) = (P & (EX x.Q x))", |
188 "(EX x. P x | Q) = ((EX x.P x) | Q)", |
188 "(EX x. P x | Q) = ((EX x.P x) | Q)", |
189 "(EX x. P | Q x) = (P | (EX x.Q x))", |
189 "(EX x. P | Q x) = (P | (EX x.Q x))", |
190 "(EX x. P x --> Q) = ((ALL x.P x) --> Q)", |
190 "(EX x. P x --> Q) = ((ALL x.P x) --> Q)", |
191 "(EX x. P --> Q x) = (P --> (EX x.Q x))"]; |
191 "(EX x. P --> Q x) = (P --> (EX x.Q x))"]; |
192 |
192 |
193 (*Miniscoping: pushing in universal quantifiers*) |
193 (*Miniscoping: pushing in universal quantifiers*) |
194 val all_simps = map prover |
194 val all_simps = map prover |
195 ["(ALL x. P x & Q) = ((ALL x.P x) & Q)", |
195 ["(ALL x. P x & Q) = ((ALL x.P x) & Q)", |
196 "(ALL x. P & Q x) = (P & (ALL x.Q x))", |
196 "(ALL x. P & Q x) = (P & (ALL x.Q x))", |
197 "(ALL x. P x | Q) = ((ALL x.P x) | Q)", |
197 "(ALL x. P x | Q) = ((ALL x.P x) | Q)", |
198 "(ALL x. P | Q x) = (P | (ALL x.Q x))", |
198 "(ALL x. P | Q x) = (P | (ALL x.Q x))", |
199 "(ALL x. P x --> Q) = ((EX x.P x) --> Q)", |
199 "(ALL x. P x --> Q) = ((EX x.P x) --> Q)", |
200 "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"]; |
200 "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"]; |
201 |
201 |
202 val HOL_ss = empty_ss |
202 val HOL_ss = empty_ss |
203 setmksimps (mksimps mksimps_pairs) |
203 setmksimps (mksimps mksimps_pairs) |
204 setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac |
204 setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac |
205 ORELSE' etac FalseE) |
205 ORELSE' etac FalseE) |
206 setsubgoaler asm_simp_tac |
206 setsubgoaler asm_simp_tac |
207 addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc, |
207 addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc, |
208 cases_simp] |
208 cases_simp] |
209 @ ex_simps @ all_simps @ simp_thms) |
209 @ ex_simps @ all_simps @ simp_thms) |
210 addcongs [imp_cong]; |
210 addcongs [imp_cong]; |
211 |
211 |
212 |
212 |
213 (*In general it seems wrong to add distributive laws by default: they |
213 (*In general it seems wrong to add distributive laws by default: they |
243 May slow rewrite proofs down by as much as 50% *) |
243 May slow rewrite proofs down by as much as 50% *) |
244 |
244 |
245 val conj_cong = |
245 val conj_cong = |
246 let val th = prove_goal HOL.thy |
246 let val th = prove_goal HOL.thy |
247 "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" |
247 "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" |
248 (fn _=> [fast_tac HOL_cs 1]) |
248 (fn _=> [fast_tac HOL_cs 1]) |
249 in standard (impI RSN (2, th RS mp RS mp)) end; |
249 in standard (impI RSN (2, th RS mp RS mp)) end; |
250 |
250 |
251 val rev_conj_cong = |
251 val rev_conj_cong = |
252 let val th = prove_goal HOL.thy |
252 let val th = prove_goal HOL.thy |
253 "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" |
253 "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" |
254 (fn _=> [fast_tac HOL_cs 1]) |
254 (fn _=> [fast_tac HOL_cs 1]) |
255 in standard (impI RSN (2, th RS mp RS mp)) end; |
255 in standard (impI RSN (2, th RS mp RS mp)) end; |
256 |
256 |
257 (* '|' congruence rule: not included by default! *) |
257 (* '|' congruence rule: not included by default! *) |
258 |
258 |
259 val disj_cong = |
259 val disj_cong = |
260 let val th = prove_goal HOL.thy |
260 let val th = prove_goal HOL.thy |
261 "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" |
261 "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" |
262 (fn _=> [fast_tac HOL_cs 1]) |
262 (fn _=> [fast_tac HOL_cs 1]) |
263 in standard (impI RSN (2, th RS mp RS mp)) end; |
263 in standard (impI RSN (2, th RS mp RS mp)) end; |
264 |
264 |
265 (** 'if' congruence rules: neither included by default! *) |
265 (** 'if' congruence rules: neither included by default! *) |
266 |
266 |
267 (*Simplifies x assuming c and y assuming ~c*) |
267 (*Simplifies x assuming c and y assuming ~c*) |