equal
deleted
inserted
replaced
591 end |
591 end |
592 |
592 |
593 |
593 |
594 (** proves the equivp predicate for all alphas **) |
594 (** proves the equivp predicate for all alphas **) |
595 |
595 |
|
596 val reflp_def' = |
|
597 @{lemma "reflp R == !x. R x x" by (simp add: reflp_def refl_on_def)} |
|
598 |
|
599 val symp_def' = |
|
600 @{lemma "symp R == !x y . R x y --> R y x" by (simp add: symp_def sym_def)} |
|
601 |
596 val transp_def' = |
602 val transp_def' = |
597 @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" |
603 @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" |
598 by (rule eq_reflection, auto simp add: transp_def)} |
604 by (rule eq_reflection, auto simp add: trans_def transp_def)} |
599 |
605 |
600 fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = |
606 fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = |
601 let |
607 let |
602 val refl' = map (fold_rule @{thms reflp_def[THEN eq_reflection]} o atomize) refl |
608 val refl' = map (fold_rule [reflp_def'] o atomize) refl |
603 val symm' = map (fold_rule @{thms symp_def[THEN eq_reflection]} o atomize) symm |
609 val symm' = map (fold_rule [symp_def'] o atomize) symm |
604 val trans' = map (fold_rule [transp_def'] o atomize) trans |
610 val trans' = map (fold_rule [transp_def'] o atomize) trans |
605 |
611 |
606 fun prep_goal t = |
612 fun prep_goal t = |
607 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
613 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
608 in |
614 in |