equal
deleted
inserted
replaced
498 lemma pred3_cong: "[| p:a=a'; q:b=b'; r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')" |
498 lemma pred3_cong: "[| p:a=a'; q:b=b'; r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')" |
499 apply (rule iffI) |
499 apply (rule iffI) |
500 apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *}) |
500 apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *}) |
501 done |
501 done |
502 |
502 |
503 (*special cases for free variables P, Q, R, S -- up to 3 arguments*) |
503 lemmas pred_congs = pred1_cong pred2_cong pred3_cong |
504 |
|
505 ML {* |
|
506 bind_thms ("pred_congs", |
|
507 flat (map (fn c => |
|
508 map (fn th => read_instantiate [("P",c)] th) |
|
509 [@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}]) |
|
510 (explode"PQRS"))) |
|
511 *} |
|
512 |
504 |
513 (*special case for the equality predicate!*) |
505 (*special case for the equality predicate!*) |
514 lemmas eq_cong = pred2_cong [where P = "op =", standard] |
506 lemmas eq_cong = pred2_cong [where P = "op =", standard] |
515 |
507 |
516 |
508 |