87 "add rules to simpset and claset simultaneously")]]; |
87 "add rules to simpset and claset simultaneously")]]; |
88 |
88 |
89 end; |
89 end; |
90 |
90 |
91 |
91 |
92 val [prem] = goal HOL.thy "x==y ==> x=y"; |
92 val [prem] = goal (the_context ()) "x==y ==> x=y"; |
93 by (rewtac prem); |
93 by (rewtac prem); |
94 by (rtac refl 1); |
94 by (rtac refl 1); |
95 qed "meta_eq_to_obj_eq"; |
95 qed "meta_eq_to_obj_eq"; |
96 |
96 |
97 local |
97 local |
98 |
98 |
99 fun prover s = prove_goal HOL.thy s (fn _ => [(Blast_tac 1)]); |
99 fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]); |
100 |
100 |
101 in |
101 in |
102 |
102 |
103 (*Make meta-equalities. The operator below is Trueprop*) |
103 (*Make meta-equalities. The operator below is Trueprop*) |
104 |
104 |
155 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs); |
155 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs); |
156 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs); |
156 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs); |
157 |
157 |
158 |
158 |
159 val imp_cong = impI RSN |
159 val imp_cong = impI RSN |
160 (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" |
160 (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" |
161 (fn _=> [(Blast_tac 1)]) RS mp RS mp); |
161 (fn _=> [(Blast_tac 1)]) RS mp RS mp); |
162 |
162 |
163 (*Miniscoping: pushing in existential quantifiers*) |
163 (*Miniscoping: pushing in existential quantifiers*) |
164 val ex_simps = map prover |
164 val ex_simps = map prover |
165 ["(EX x. P x & Q) = ((EX x. P x) & Q)", |
165 ["(EX x. P x & Q) = ((EX x. P x) & Q)", |
180 |
180 |
181 |
181 |
182 (* elimination of existential quantifiers in assumptions *) |
182 (* elimination of existential quantifiers in assumptions *) |
183 |
183 |
184 val ex_all_equiv = |
184 val ex_all_equiv = |
185 let val lemma1 = prove_goal HOL.thy |
185 let val lemma1 = prove_goal (the_context ()) |
186 "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)" |
186 "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)" |
187 (fn prems => [resolve_tac prems 1, etac exI 1]); |
187 (fn prems => [resolve_tac prems 1, etac exI 1]); |
188 val lemma2 = prove_goalw HOL.thy [Ex_def] |
188 val lemma2 = prove_goalw (the_context ()) [Ex_def] |
189 "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)" |
189 "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)" |
190 (fn prems => [(REPEAT(resolve_tac prems 1))]) |
190 (fn prems => [(REPEAT(resolve_tac prems 1))]) |
191 in equal_intr lemma1 lemma2 end; |
191 in equal_intr lemma1 lemma2 end; |
192 |
192 |
193 end; |
193 end; |
194 |
194 |
195 (* Elimination of True from asumptions: *) |
195 (* Elimination of True from asumptions: *) |
196 |
196 |
197 val True_implies_equals = prove_goal HOL.thy |
197 val True_implies_equals = prove_goal (the_context ()) |
198 "(True ==> PROP P) == PROP P" |
198 "(True ==> PROP P) == PROP P" |
199 (fn _ => [rtac equal_intr_rule 1, atac 2, |
199 (fn _ => [rtac equal_intr_rule 1, atac 2, |
200 METAHYPS (fn prems => resolve_tac prems 1) 1, |
200 METAHYPS (fn prems => resolve_tac prems 1) 1, |
201 rtac TrueI 1]); |
201 rtac TrueI 1]); |
202 |
202 |
203 fun prove nm thm = qed_goal nm HOL.thy thm (fn _ => [(Blast_tac 1)]); |
203 fun prove nm thm = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]); |
204 |
204 |
205 prove "conj_commute" "(P&Q) = (Q&P)"; |
205 prove "conj_commute" "(P&Q) = (Q&P)"; |
206 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
206 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
207 val conj_comms = [conj_commute, conj_left_commute]; |
207 val conj_comms = [conj_commute, conj_left_commute]; |
208 prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))"; |
208 prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))"; |
253 prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; |
253 prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; |
254 |
254 |
255 (* '&' congruence rule: not included by default! |
255 (* '&' congruence rule: not included by default! |
256 May slow rewrite proofs down by as much as 50% *) |
256 May slow rewrite proofs down by as much as 50% *) |
257 |
257 |
258 let val th = prove_goal HOL.thy |
258 let val th = prove_goal (the_context ()) |
259 "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" |
259 "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" |
260 (fn _=> [(Blast_tac 1)]) |
260 (fn _=> [(Blast_tac 1)]) |
261 in bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
261 in bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
262 |
262 |
263 let val th = prove_goal HOL.thy |
263 let val th = prove_goal (the_context ()) |
264 "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" |
264 "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" |
265 (fn _=> [(Blast_tac 1)]) |
265 (fn _=> [(Blast_tac 1)]) |
266 in bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
266 in bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
267 |
267 |
268 (* '|' congruence rule: not included by default! *) |
268 (* '|' congruence rule: not included by default! *) |
269 |
269 |
270 let val th = prove_goal HOL.thy |
270 let val th = prove_goal (the_context ()) |
271 "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" |
271 "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" |
272 (fn _=> [(Blast_tac 1)]) |
272 (fn _=> [(Blast_tac 1)]) |
273 in bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
273 in bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp))) end; |
274 |
274 |
275 prove "eq_sym_conv" "(x=y) = (y=x)"; |
275 prove "eq_sym_conv" "(x=y) = (y=x)"; |
476 by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1); |
476 by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1); |
477 qed "if_distrib"; |
477 qed "if_distrib"; |
478 |
478 |
479 |
479 |
480 (*For expand_case_tac*) |
480 (*For expand_case_tac*) |
481 val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; |
481 val prems = goal (the_context ()) "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; |
482 by (case_tac "P" 1); |
482 by (case_tac "P" 1); |
483 by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems))); |
483 by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems))); |
484 val expand_case = result(); |
484 val expand_case = result(); |
485 |
485 |
486 (*Used in Auth proofs. Typically P contains Vars that become instantiated |
486 (*Used in Auth proofs. Typically P contains Vars that become instantiated |
489 res_inst_tac [("P",P)] expand_case i THEN |
489 res_inst_tac [("P",P)] expand_case i THEN |
490 Simp_tac (i+1) THEN |
490 Simp_tac (i+1) THEN |
491 Simp_tac i; |
491 Simp_tac i; |
492 |
492 |
493 |
493 |
494 (* install implicit simpset *) |
494 (* default simpset *) |
495 |
495 val simpsetup = [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)]; |
496 simpset_ref() := HOL_ss addcongs [if_weak_cong]; |
|
497 |
496 |
498 |
497 |
499 (*** integration of simplifier with classical reasoner ***) |
498 (*** integration of simplifier with classical reasoner ***) |
500 |
499 |
501 structure Clasimp = ClasimpFun |
500 structure Clasimp = ClasimpFun |