equal
deleted
inserted
replaced
641 using part_equivp_transp[OF equivp] by (metis `R (SOME x. x \<in> Rep a) x`) |
641 using part_equivp_transp[OF equivp] by (metis `R (SOME x. x \<in> Rep a) x`) |
642 qed |
642 qed |
643 have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop) |
643 have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop) |
644 then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto |
644 then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto |
645 have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" |
645 have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" |
646 by (metis Collect_def abs_inverse) |
646 proof - |
|
647 assume "R r r" and "R s s" |
|
648 then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)" |
|
649 by (metis abs_inverse) |
|
650 also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))" |
|
651 by rule simp_all |
|
652 finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp |
|
653 qed |
647 then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))" |
654 then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))" |
648 using equivp[simplified part_equivp_def] by metis |
655 using equivp[simplified part_equivp_def] by metis |
649 qed |
656 qed |
|
657 |
650 end |
658 end |
651 |
659 |
652 subsection {* ML setup *} |
660 subsection {* ML setup *} |
653 |
661 |
654 text {* Auxiliary data for the quotient package *} |
662 text {* Auxiliary data for the quotient package *} |