154 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs); |
156 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs); |
155 |
157 |
156 |
158 |
157 val imp_cong = impI RSN |
159 val imp_cong = impI RSN |
158 (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" |
160 (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" |
159 (fn _=> [Blast_tac 1]) RS mp RS mp); |
161 (fn _=> [(Blast_tac 1)]) RS mp RS mp); |
160 |
162 |
161 (*Miniscoping: pushing in existential quantifiers*) |
163 (*Miniscoping: pushing in existential quantifiers*) |
162 val ex_simps = map prover |
164 val ex_simps = map prover |
163 ["(EX x. P x & Q) = ((EX x. P x) & Q)", |
165 ["(EX x. P x & Q) = ((EX x. P x) & Q)", |
164 "(EX x. P & Q x) = (P & (EX x. Q x))", |
166 "(EX x. P & Q x) = (P & (EX x. Q x))", |
183 let val lemma1 = prove_goal HOL.thy |
185 let val lemma1 = prove_goal HOL.thy |
184 "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)" |
186 "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)" |
185 (fn prems => [resolve_tac prems 1, etac exI 1]); |
187 (fn prems => [resolve_tac prems 1, etac exI 1]); |
186 val lemma2 = prove_goalw HOL.thy [Ex_def] |
188 val lemma2 = prove_goalw HOL.thy [Ex_def] |
187 "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)" |
189 "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)" |
188 (fn prems => [REPEAT(resolve_tac prems 1)]) |
190 (fn prems => [(REPEAT(resolve_tac prems 1))]) |
189 in equal_intr lemma1 lemma2 end; |
191 in equal_intr lemma1 lemma2 end; |
190 |
192 |
191 end; |
193 end; |
192 |
194 |
193 (* Elimination of True from asumptions: *) |
195 (* Elimination of True from asumptions: *) |
194 |
196 |
195 val True_implies_equals = prove_goal HOL.thy |
197 val True_implies_equals = prove_goal HOL.thy |
196 "(True ==> PROP P) == PROP P" |
198 "(True ==> PROP P) == PROP P" |
197 (K [rtac equal_intr_rule 1, atac 2, |
199 (fn _ => [rtac equal_intr_rule 1, atac 2, |
198 METAHYPS (fn prems => resolve_tac prems 1) 1, |
200 METAHYPS (fn prems => resolve_tac prems 1) 1, |
199 rtac TrueI 1]); |
201 rtac TrueI 1]); |
200 |
202 |
201 fun prove nm thm = qed_goal nm HOL.thy thm (K [Blast_tac 1]); |
203 fun prove nm thm = qed_goal nm HOL.thy thm (fn _ => [(Blast_tac 1)]); |
202 |
204 |
203 prove "conj_commute" "(P&Q) = (Q&P)"; |
205 prove "conj_commute" "(P&Q) = (Q&P)"; |
204 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
206 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
205 val conj_comms = [conj_commute, conj_left_commute]; |
207 val conj_comms = [conj_commute, conj_left_commute]; |
206 prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))"; |
208 prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))"; |
253 (* '&' congruence rule: not included by default! |
255 (* '&' congruence rule: not included by default! |
254 May slow rewrite proofs down by as much as 50% *) |
256 May slow rewrite proofs down by as much as 50% *) |
255 |
257 |
256 let val th = prove_goal HOL.thy |
258 let val th = prove_goal HOL.thy |
257 "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" |
259 "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" |
258 (fn _=> [Blast_tac 1]) |
260 (fn _=> [(Blast_tac 1)]) |
259 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; |
260 |
262 |
261 let val th = prove_goal HOL.thy |
263 let val th = prove_goal HOL.thy |
262 "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" |
264 "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" |
263 (fn _=> [Blast_tac 1]) |
265 (fn _=> [(Blast_tac 1)]) |
264 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; |
265 |
267 |
266 (* '|' congruence rule: not included by default! *) |
268 (* '|' congruence rule: not included by default! *) |
267 |
269 |
268 let val th = prove_goal HOL.thy |
270 let val th = prove_goal HOL.thy |
269 "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" |
271 "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" |
270 (fn _=> [Blast_tac 1]) |
272 (fn _=> [(Blast_tac 1)]) |
271 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; |
272 |
274 |
273 prove "eq_sym_conv" "(x=y) = (y=x)"; |
275 prove "eq_sym_conv" "(x=y) = (y=x)"; |
274 |
276 |
275 |
277 |
276 (** if-then-else rules **) |
278 (** if-then-else rules **) |
277 |
279 |
278 qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x" |
280 Goalw [if_def] "(if True then x else y) = x"; |
279 (K [Blast_tac 1]); |
281 by (Blast_tac 1); |
280 |
282 qed "if_True"; |
281 qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y" |
283 |
282 (K [Blast_tac 1]); |
284 Goalw [if_def] "(if False then x else y) = y"; |
283 |
285 by (Blast_tac 1); |
284 qed_goalw "if_P" HOL.thy [if_def] "!!P. P ==> (if P then x else y) = x" |
286 qed "if_False"; |
285 (K [Blast_tac 1]); |
287 |
286 |
288 Goalw [if_def] "!!P. P ==> (if P then x else y) = x"; |
287 qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y" |
289 by (Blast_tac 1); |
288 (K [Blast_tac 1]); |
290 qed "if_P"; |
289 |
291 |
290 qed_goal "split_if" HOL.thy |
292 Goalw [if_def] "!!P. ~P ==> (if P then x else y) = y"; |
291 "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [ |
293 by (Blast_tac 1); |
292 res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1, |
294 qed "if_not_P"; |
293 stac if_P 2, |
295 |
294 stac if_not_P 1, |
296 Goal "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"; |
295 ALLGOALS (Blast_tac)]); |
297 by (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1); |
|
298 by (stac if_P 2); |
|
299 by (stac if_not_P 1); |
|
300 by (ALLGOALS (Blast_tac)); |
|
301 qed "split_if"; |
|
302 |
296 (* for backwards compatibility: *) |
303 (* for backwards compatibility: *) |
297 val expand_if = split_if; |
304 val expand_if = split_if; |
298 |
305 |
299 qed_goal "split_if_asm" HOL.thy |
306 Goal "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"; |
300 "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))" |
307 by (stac split_if 1); |
301 (K [stac split_if 1, |
308 by (Blast_tac 1); |
302 Blast_tac 1]); |
309 qed "split_if_asm"; |
303 |
310 |
304 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x" |
311 Goal "(if c then x else x) = x"; |
305 (K [stac split_if 1, Blast_tac 1]); |
312 by (stac split_if 1); |
306 |
313 by (Blast_tac 1); |
307 qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x" |
314 qed "if_cancel"; |
308 (K [stac split_if 1, Blast_tac 1]); |
315 |
|
316 Goal "(if x = y then y else x) = x"; |
|
317 by (stac split_if 1); |
|
318 by (Blast_tac 1); |
|
319 qed "if_eq_cancel"; |
309 |
320 |
310 (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*) |
321 (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*) |
311 qed_goal "if_bool_eq_conj" HOL.thy |
322 Goal |
312 "(if P then Q else R) = ((P-->Q) & (~P-->R))" |
323 "(if P then Q else R) = ((P-->Q) & (~P-->R))"; |
313 (K [rtac split_if 1]); |
324 by (rtac split_if 1); |
|
325 qed "if_bool_eq_conj"; |
314 |
326 |
315 (*And this form is useful for expanding IFs on the LEFT*) |
327 (*And this form is useful for expanding IFs on the LEFT*) |
316 qed_goal "if_bool_eq_disj" HOL.thy |
328 Goal "(if P then Q else R) = ((P&Q) | (~P&R))"; |
317 "(if P then Q else R) = ((P&Q) | (~P&R))" |
329 by (stac split_if 1); |
318 (K [stac split_if 1, |
330 by (Blast_tac 1); |
319 Blast_tac 1]); |
331 qed "if_bool_eq_disj"; |
320 |
332 |
321 |
333 |
322 (*** make simplification procedures for quantifier elimination ***) |
334 (*** make simplification procedures for quantifier elimination ***) |
323 |
335 |
324 structure Quantifier1 = Quantifier1Fun( |
336 structure Quantifier1 = Quantifier1Fun( |
451 \ (if b then x else y) = (if c then u else v)"; |
463 \ (if b then x else y) = (if c then u else v)"; |
452 by (asm_simp_tac (HOL_ss addsimps prems) 1); |
464 by (asm_simp_tac (HOL_ss addsimps prems) 1); |
453 qed "if_cong"; |
465 qed "if_cong"; |
454 |
466 |
455 (*Prevents simplification of x and y: much faster*) |
467 (*Prevents simplification of x and y: much faster*) |
456 qed_goal "if_weak_cong" HOL.thy |
468 Goal "b=c ==> (if b then x else y) = (if c then x else y)"; |
457 "b=c ==> (if b then x else y) = (if c then x else y)" |
469 by (etac arg_cong 1); |
458 (fn [prem] => [rtac (prem RS arg_cong) 1]); |
470 qed "if_weak_cong"; |
459 |
471 |
460 (*Prevents simplification of t: much faster*) |
472 (*Prevents simplification of t: much faster*) |
461 qed_goal "let_weak_cong" HOL.thy |
473 Goal "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"; |
462 "a = b ==> (let x=a in t(x)) = (let x=b in t(x))" |
474 by (etac arg_cong 1); |
463 (fn [prem] => [rtac (prem RS arg_cong) 1]); |
475 qed "let_weak_cong"; |
464 |
476 |
465 qed_goal "if_distrib" HOL.thy |
477 Goal "f(if c then x else y) = (if c then f x else f y)"; |
466 "f(if c then x else y) = (if c then f x else f y)" |
478 by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1); |
467 (K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]); |
479 qed "if_distrib"; |
468 |
480 |
469 |
481 |
470 (*For expand_case_tac*) |
482 (*For expand_case_tac*) |
471 val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; |
483 val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; |
472 by (case_tac "P" 1); |
484 by (case_tac "P" 1); |