1.1 --- a/src/HOL/Quotient.thy Wed Aug 17 18:05:31 2011 +0200
1.2 +++ b/src/HOL/Quotient.thy Wed Aug 17 18:52:21 2011 +0200
1.3 @@ -643,10 +643,18 @@
1.4 have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
1.5 then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
1.6 have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s"
1.7 - by (metis Collect_def abs_inverse)
1.8 + proof -
1.9 + assume "R r r" and "R s s"
1.10 + then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)"
1.11 + by (metis abs_inverse)
1.12 + 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))"
1.13 + by rule simp_all
1.14 + finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp
1.15 + qed
1.16 then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
1.17 using equivp[simplified part_equivp_def] by metis
1.18 qed
1.19 +
1.20 end
1.21
1.22 subsection {* ML setup *}