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.120 -  apply(simp add: homeier_thm10)
   1.121 -  apply(simp add: rep_refl)
   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 *}