src/HOL/Quotient.thy
 changeset 44204 3cdc4176638c parent 42814 5af15f1e2ef6 child 44242 a5cb6aa77ffc
```     1.1 --- a/src/HOL/Quotient.thy	Mon Aug 15 22:31:17 2011 +0200
1.2 +++ b/src/HOL/Quotient.thy	Tue Aug 16 07:17:15 2011 +0900
1.3 @@ -603,66 +603,52 @@
1.4
1.5  locale quot_type =
1.6    fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1.7 -  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
1.8 -  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
1.9 +  and   Abs :: "'a set \<Rightarrow> 'b"
1.10 +  and   Rep :: "'b \<Rightarrow> 'a set"
1.11    assumes equivp: "part_equivp R"
1.12 -  and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = R x"
1.13 +  and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = Collect (R x)"
1.14    and     rep_inverse: "\<And>x. Abs (Rep x) = x"
1.15 -  and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = R x))) \<Longrightarrow> (Rep (Abs c)) = c"
1.16 +  and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = Collect (R x)))) \<Longrightarrow> (Rep (Abs c)) = c"
1.17    and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
1.18  begin
1.19
1.20  definition
1.21    abs :: "'a \<Rightarrow> 'b"
1.22  where
1.23 -  "abs x = Abs (R x)"
1.24 +  "abs x = Abs (Collect (R x))"
1.25
1.26  definition
1.27    rep :: "'b \<Rightarrow> 'a"
1.28  where
1.29 -  "rep a = Eps (Rep a)"
1.30 -
1.31 -lemma homeier5:
1.32 -  assumes a: "R r r"
1.33 -  shows "Rep (Abs (R r)) = R r"
1.34 -  apply (subst abs_inverse)
1.35 -  using a by auto
1.36 +  "rep a = (SOME x. x \<in> Rep a)"
1.37
1.38 -theorem homeier6:
1.39 -  assumes a: "R r r"
1.40 -  and b: "R s s"
1.41 -  shows "Abs (R r) = Abs (R s) \<longleftrightarrow> R r = R s"
1.42 -  by (metis a b homeier5)
1.43 -
1.44 -theorem homeier8:
1.45 +lemma some_collect:
1.46    assumes "R r r"
1.47 -  shows "R (Eps (R r)) = R r"
1.48 -  using assms equivp[simplified part_equivp_def]
1.49 -  apply clarify
1.50 -  by (metis assms exE_some)
1.51 +  shows "R (SOME x. x \<in> Collect (R r)) = R r"
1.52 +  apply simp
1.53 +  by (metis assms exE_some equivp[simplified part_equivp_def])
1.54
1.55  lemma Quotient:
1.56    shows "Quotient R abs rep"
1.57    unfolding Quotient_def abs_def rep_def
1.58    proof (intro conjI allI)
1.59      fix a r s
1.60 -    show "Abs (R (Eps (Rep a))) = a"
1.61 -      using [[metis_new_skolemizer = false]]
1.62 -      by (metis equivp exE_some part_equivp_def rep_inverse rep_prop)
1.63 -    show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (R r) = Abs (R s))"
1.64 -      by (metis homeier6 equivp[simplified part_equivp_def])
1.65 -    show "R (Eps (Rep a)) (Eps (Rep a))" proof -
1.66 -      obtain x where r: "R x x" and rep: "Rep a = R x" using rep_prop[of a] by auto
1.67 -      have "R (Eps (R x)) x" using homeier8 r by simp
1.68 -      then have "R x (Eps (R x))" using part_equivp_symp[OF equivp] by fast
1.69 -      then have "R (Eps (R x)) (Eps (R x))" using homeier8[OF r] by simp
1.70 -      then show "R (Eps (Rep a)) (Eps (Rep a))" using rep by simp
1.71 +    show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof -
1.72 +      obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto
1.73 +      have "R (SOME x. x \<in> Rep a) x"  using r rep some_collect by metis
1.74 +      then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast
1.75 +      then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)"
1.76 +        using part_equivp_transp[OF equivp] by (metis `R (SOME x. x \<in> Rep a) x`)
1.77      qed
1.78 -  qed
1.79 -
1.80 +    have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
1.81 +    then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
1.82 +    have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s"
1.83 +      by (metis Collect_def abs_inverse)
1.84 +    then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
1.85 +      using equivp[simplified part_equivp_def] by metis
1.86 +    qed
1.87  end
1.88
1.89 -
1.90  subsection {* ML setup *}
1.91
1.92  text {* Auxiliary data for the quotient package *}
```