src/HOL/Quotient.thy
 changeset 37493 2377d246a631 parent 37049 ca1c293e521e child 37564 a47bb386b238
```     1.1 --- a/src/HOL/Quotient.thy	Wed Jun 23 08:42:41 2010 +0200
1.2 +++ b/src/HOL/Quotient.thy	Wed Jun 23 08:44:44 2010 +0200
1.3 @@ -59,7 +59,7 @@
1.4    unfolding equivp_def
1.5    by auto
1.6
1.7 -text {* Partial equivalences: not yet used anywhere *}
1.8 +text {* Partial equivalences *}
1.9
1.10  definition
1.11    "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
1.12 @@ -71,6 +71,23 @@
1.13    unfolding equivp_def part_equivp_def
1.14    by auto
1.15
1.16 +lemma part_equivp_symp:
1.17 +  assumes e: "part_equivp R"
1.18 +  and a: "R x y"
1.19 +  shows "R y x"
1.20 +  using e[simplified part_equivp_def] a
1.21 +  by (metis)
1.22 +
1.23 +lemma part_equivp_typedef:
1.24 +  shows "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
1.25 +  unfolding part_equivp_def mem_def
1.26 +  apply clarify
1.27 +  apply (intro exI)
1.28 +  apply (rule conjI)
1.29 +  apply assumption
1.30 +  apply (rule refl)
1.31 +  done
1.32 +
1.33  text {* Composition of Relations *}
1.34
1.35  abbreviation
1.36 @@ -630,10 +647,10 @@
1.37    fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1.38    and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
1.39    and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
1.40 -  assumes equivp: "equivp R"
1.41 -  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
1.42 +  assumes equivp: "part_equivp R"
1.43 +  and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = R x"
1.44    and     rep_inverse: "\<And>x. Abs (Rep x) = x"
1.45 -  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
1.46 +  and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = R x))) \<Longrightarrow> (Rep (Abs c)) = c"
1.47    and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
1.48  begin
1.49
1.50 @@ -647,64 +664,46 @@
1.51  where
1.52    "rep a = Eps (Rep a)"
1.53
1.54 -lemma homeier_lem9:
1.55 -  shows "R (Eps (R x)) = R x"
1.56 -proof -
1.57 -  have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
1.58 -  then have "R x (Eps (R x))" by (rule someI)
1.59 -  then show "R (Eps (R x)) = R x"
1.60 -    using equivp unfolding equivp_def by simp
1.61 -qed
1.62 -
1.63 -theorem homeier_thm10:
1.64 -  shows "abs (rep a) = a"
1.65 -  unfolding abs_def rep_def
1.66 -proof -
1.67 -  from rep_prop
1.68 -  obtain x where eq: "Rep a = R x" by auto
1.69 -  have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
1.70 -  also have "\<dots> = Abs (R x)" using homeier_lem9 by simp
1.71 -  also have "\<dots> = Abs (Rep a)" using eq by simp
1.72 -  also have "\<dots> = a" using rep_inverse by simp
1.73 -  finally
1.74 -  show "Abs (R (Eps (Rep a))) = a" by simp
1.75 -qed
1.76 +lemma homeier5:
1.77 +  assumes a: "R r r"
1.78 +  shows "Rep (Abs (R r)) = R r"
1.79 +  apply (subst abs_inverse)
1.80 +  using a by auto
1.81
1.82 -lemma homeier_lem7:
1.83 -  shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
1.84 -proof -
1.85 -  have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
1.86 -  also have "\<dots> = ?LHS" by (simp add: abs_inverse)
1.87 -  finally show "?LHS = ?RHS" by simp
1.88 -qed
1.89 +theorem homeier6:
1.90 +  assumes a: "R r r"
1.91 +  and b: "R s s"
1.92 +  shows "Abs (R r) = Abs (R s) \<longleftrightarrow> R r = R s"
1.93 +  by (metis a b homeier5)
1.94
1.95 -theorem homeier_thm11:
1.96 -  shows "R r r' = (abs r = abs r')"
1.97 -  unfolding abs_def
1.98 -  by (simp only: equivp[simplified equivp_def] homeier_lem7)
1.99 -
1.100 -lemma rep_refl:
1.101 -  shows "R (rep a) (rep a)"
1.102 -  unfolding rep_def
1.103 -  by (simp add: equivp[simplified equivp_def])
1.104 -
1.105 -
1.106 -lemma rep_abs_rsp:
1.107 -  shows "R f (rep (abs g)) = R f g"
1.108 -  and   "R (rep (abs g)) f = R g f"
1.109 -  by (simp_all add: homeier_thm10 homeier_thm11)
1.110 +theorem homeier8:
1.111 +  assumes "R r r"
1.112 +  shows "R (Eps (R r)) = R r"
1.113 +  using assms equivp[simplified part_equivp_def]
1.114 +  apply clarify
1.115 +  by (metis assms exE_some)
1.116
1.117  lemma Quotient:
1.118    shows "Quotient R abs rep"
1.119 -  unfolding Quotient_def
1.122 -  apply(subst homeier_thm11[symmetric])
1.123 -  apply(simp add: equivp[simplified equivp_def])
1.124 -  done
1.125 +  unfolding Quotient_def abs_def rep_def
1.126 +  proof (intro conjI allI)
1.127 +    fix a r s
1.128 +    show "Abs (R (Eps (Rep a))) = a"
1.129 +      by (metis equivp exE_some part_equivp_def rep_inverse rep_prop)
1.130 +    show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (R r) = Abs (R s))"
1.131 +      by (metis homeier6 equivp[simplified part_equivp_def])
1.132 +    show "R (Eps (Rep a)) (Eps (Rep a))" proof -
1.133 +      obtain x where r: "R x x" and rep: "Rep a = R x" using rep_prop[of a] by auto
1.134 +      have "R (Eps (R x)) x" using homeier8 r by simp
1.135 +      then have "R x (Eps (R x))" using part_equivp_symp[OF equivp] by fast
1.136 +      then have "R (Eps (R x)) (Eps (R x))" using homeier8[OF r] by simp
1.137 +      then show "R (Eps (Rep a)) (Eps (Rep a))" using rep by simp
1.138 +    qed
1.139 +  qed
1.140
1.141  end
1.142
1.143 +
1.144  subsection {* ML setup *}
1.145
1.146  text {* Auxiliary data for the quotient package *}
```