492 - Ball (Respects ?E) ?P = All ?P |
492 - Ball (Respects ?E) ?P = All ?P |
493 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
493 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
494 |
494 |
495 *) |
495 *) |
496 |
496 |
497 (* FIXME: they should be in in the new Isabelle *) |
|
498 lemma [mono]: |
|
499 "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)" |
|
500 by blast |
|
501 |
|
502 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
|
503 by auto |
|
504 |
|
505 (* FIXME: OPTION_equivp, PAIR_equivp, ... *) |
497 (* FIXME: OPTION_equivp, PAIR_equivp, ... *) |
506 ML {* |
498 ML {* |
507 fun equiv_tac rel_eqvs = |
499 fun equiv_tac rel_eqvs = |
508 REPEAT_ALL_NEW (FIRST' |
500 REPEAT_ALL_NEW (FIRST' |
509 [resolve_tac rel_eqvs, |
501 [resolve_tac rel_eqvs, |
510 rtac @{thm identity_equivp}, |
502 rtac @{thm identity_equivp}, |
511 rtac @{thm list_equivp}]) |
503 rtac @{thm list_equivp}]) |
512 *} |
504 *} |
|
505 |
|
506 thm ball_reg_eqv |
513 |
507 |
514 ML {* |
508 ML {* |
515 fun ball_reg_eqv_simproc rel_eqvs ss redex = |
509 fun ball_reg_eqv_simproc rel_eqvs ss redex = |
516 let |
510 let |
517 val ctxt = Simplifier.the_context ss |
511 val ctxt = Simplifier.the_context ss |