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 *}