src/HOL/Quotient.thy
changeset 40814 fa64f6278568
parent 40615 ab551d108feb
child 40818 b117df72e56b
     1.1 --- a/src/HOL/Quotient.thy	Mon Nov 29 12:14:46 2010 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Mon Nov 29 12:15:14 2010 +0100
     1.3 @@ -14,127 +14,11 @@
     1.4    ("Tools/Quotient/quotient_tacs.ML")
     1.5  begin
     1.6  
     1.7 -
     1.8  text {*
     1.9    Basic definition for equivalence relations
    1.10    that are represented by predicates.
    1.11  *}
    1.12  
    1.13 -definition
    1.14 -  "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
    1.15 -
    1.16 -lemma refl_reflp:
    1.17 -  "refl A \<longleftrightarrow> reflp (\<lambda>x y. (x, y) \<in> A)"
    1.18 -  by (simp add: refl_on_def reflp_def)
    1.19 -
    1.20 -definition
    1.21 -  "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
    1.22 -
    1.23 -lemma sym_symp:
    1.24 -  "sym A \<longleftrightarrow> symp (\<lambda>x y. (x, y) \<in> A)"
    1.25 -  by (simp add: sym_def symp_def)
    1.26 -
    1.27 -definition
    1.28 -  "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
    1.29 -
    1.30 -lemma trans_transp:
    1.31 -  "trans A \<longleftrightarrow> transp (\<lambda>x y. (x, y) \<in> A)"
    1.32 -  by (auto simp add: trans_def transp_def)
    1.33 -
    1.34 -definition
    1.35 -  "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
    1.36 -
    1.37 -lemma equivp_reflp_symp_transp:
    1.38 -  shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
    1.39 -  unfolding equivp_def reflp_def symp_def transp_def fun_eq_iff
    1.40 -  by blast
    1.41 -
    1.42 -lemma equiv_equivp:
    1.43 -  "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
    1.44 -  by (simp add: equiv_def equivp_reflp_symp_transp refl_reflp sym_symp trans_transp)
    1.45 -
    1.46 -lemma equivp_reflp:
    1.47 -  shows "equivp E \<Longrightarrow> E x x"
    1.48 -  by (simp only: equivp_reflp_symp_transp reflp_def)
    1.49 -
    1.50 -lemma equivp_symp:
    1.51 -  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
    1.52 -  by (simp add: equivp_def)
    1.53 -
    1.54 -lemma equivp_transp:
    1.55 -  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
    1.56 -  by (simp add: equivp_def)
    1.57 -
    1.58 -lemma equivpI:
    1.59 -  assumes "reflp R" "symp R" "transp R"
    1.60 -  shows "equivp R"
    1.61 -  using assms by (simp add: equivp_reflp_symp_transp)
    1.62 -
    1.63 -lemma identity_equivp:
    1.64 -  shows "equivp (op =)"
    1.65 -  unfolding equivp_def
    1.66 -  by auto
    1.67 -
    1.68 -text {* Partial equivalences *}
    1.69 -
    1.70 -definition
    1.71 -  "part_equivp E \<longleftrightarrow> (\<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.72 -
    1.73 -lemma equivp_implies_part_equivp:
    1.74 -  assumes a: "equivp E"
    1.75 -  shows "part_equivp E"
    1.76 -  using a
    1.77 -  unfolding equivp_def part_equivp_def
    1.78 -  by auto
    1.79 -
    1.80 -lemma part_equivp_symp:
    1.81 -  assumes e: "part_equivp R"
    1.82 -  and a: "R x y"
    1.83 -  shows "R y x"
    1.84 -  using e[simplified part_equivp_def] a
    1.85 -  by (metis)
    1.86 -
    1.87 -lemma part_equivp_typedef:
    1.88 -  shows "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
    1.89 -  unfolding part_equivp_def mem_def
    1.90 -  apply clarify
    1.91 -  apply (intro exI)
    1.92 -  apply (rule conjI)
    1.93 -  apply assumption
    1.94 -  apply (rule refl)
    1.95 -  done
    1.96 -
    1.97 -lemma part_equivp_refl_symp_transp:
    1.98 -  shows "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> symp E \<and> transp E)"
    1.99 -proof
   1.100 -  assume "part_equivp E"
   1.101 -  then show "(\<exists>x. E x x) \<and> symp E \<and> transp E"
   1.102 -  unfolding part_equivp_def symp_def transp_def
   1.103 -  by metis
   1.104 -next
   1.105 -  assume a: "(\<exists>x. E x x) \<and> symp E \<and> transp E"
   1.106 -  then have b: "(\<forall>x y. E x y \<longrightarrow> E y x)" and c: "(\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
   1.107 -    unfolding symp_def transp_def by (metis, metis)
   1.108 -  have "(\<forall>x y. E x y = (E x x \<and> E y y \<and> E x = E y))"
   1.109 -  proof (intro allI iffI conjI)
   1.110 -    fix x y
   1.111 -    assume d: "E x y"
   1.112 -    then show "E x x" using b c by metis
   1.113 -    show "E y y" using b c d by metis
   1.114 -    show "E x = E y" unfolding fun_eq_iff using b c d by metis
   1.115 -  next
   1.116 -    fix x y
   1.117 -    assume "E x x \<and> E y y \<and> E x = E y"
   1.118 -    then show "E x y" using b c by metis
   1.119 -  qed
   1.120 -  then show "part_equivp E" unfolding part_equivp_def using a by metis
   1.121 -qed
   1.122 -
   1.123 -lemma part_equivpI:
   1.124 -  assumes "\<exists>x. R x x" "symp R" "transp R"
   1.125 -  shows "part_equivp R"
   1.126 -  using assms by (simp add: part_equivp_refl_symp_transp)
   1.127 -
   1.128  text {* Composition of Relations *}
   1.129  
   1.130  abbreviation
   1.131 @@ -169,16 +53,16 @@
   1.132  definition
   1.133    fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
   1.134  where
   1.135 -  "fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
   1.136 +  "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
   1.137  
   1.138  lemma fun_relI [intro]:
   1.139 -  assumes "\<And>x y. E1 x y \<Longrightarrow> E2 (f x) (g y)"
   1.140 -  shows "(E1 ===> E2) f g"
   1.141 +  assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
   1.142 +  shows "(R1 ===> R2) f g"
   1.143    using assms by (simp add: fun_rel_def)
   1.144  
   1.145  lemma fun_relE:
   1.146 -  assumes "(E1 ===> E2) f g" and "E1 x y"
   1.147 -  obtains "E2 (f x) (g y)"
   1.148 +  assumes "(R1 ===> R2) f g" and "R1 x y"
   1.149 +  obtains "R2 (f x) (g y)"
   1.150    using assms by (simp add: fun_rel_def)
   1.151  
   1.152  lemma fun_rel_eq:
   1.153 @@ -189,27 +73,27 @@
   1.154  subsection {* Quotient Predicate *}
   1.155  
   1.156  definition
   1.157 -  "Quotient E Abs Rep \<longleftrightarrow>
   1.158 -     (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
   1.159 -     (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
   1.160 +  "Quotient R Abs Rep \<longleftrightarrow>
   1.161 +     (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
   1.162 +     (\<forall>r s. R r s = (R r r \<and> R s s \<and> (Abs r = Abs s)))"
   1.163  
   1.164  lemma Quotient_abs_rep:
   1.165 -  assumes a: "Quotient E Abs Rep"
   1.166 +  assumes a: "Quotient R Abs Rep"
   1.167    shows "Abs (Rep a) = a"
   1.168    using a
   1.169    unfolding Quotient_def
   1.170    by simp
   1.171  
   1.172  lemma Quotient_rep_reflp:
   1.173 -  assumes a: "Quotient E Abs Rep"
   1.174 -  shows "E (Rep a) (Rep a)"
   1.175 +  assumes a: "Quotient R Abs Rep"
   1.176 +  shows "R (Rep a) (Rep a)"
   1.177    using a
   1.178    unfolding Quotient_def
   1.179    by blast
   1.180  
   1.181  lemma Quotient_rel:
   1.182 -  assumes a: "Quotient E Abs Rep"
   1.183 -  shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
   1.184 +  assumes a: "Quotient R Abs Rep"
   1.185 +  shows " R r s = (R r r \<and> R s s \<and> (Abs r = Abs s))"
   1.186    using a
   1.187    unfolding Quotient_def
   1.188    by blast
   1.189 @@ -228,22 +112,20 @@
   1.190    by blast
   1.191  
   1.192  lemma Quotient_rel_abs:
   1.193 -  assumes a: "Quotient E Abs Rep"
   1.194 -  shows "E r s \<Longrightarrow> Abs r = Abs s"
   1.195 +  assumes a: "Quotient R Abs Rep"
   1.196 +  shows "R r s \<Longrightarrow> Abs r = Abs s"
   1.197    using a unfolding Quotient_def
   1.198    by blast
   1.199  
   1.200  lemma Quotient_symp:
   1.201 -  assumes a: "Quotient E Abs Rep"
   1.202 -  shows "symp E"
   1.203 -  using a unfolding Quotient_def symp_def
   1.204 -  by metis
   1.205 +  assumes a: "Quotient R Abs Rep"
   1.206 +  shows "symp R"
   1.207 +  using a unfolding Quotient_def using sympI by metis
   1.208  
   1.209  lemma Quotient_transp:
   1.210 -  assumes a: "Quotient E Abs Rep"
   1.211 -  shows "transp E"
   1.212 -  using a unfolding Quotient_def transp_def
   1.213 -  by metis
   1.214 +  assumes a: "Quotient R Abs Rep"
   1.215 +  shows "transp R"
   1.216 +  using a unfolding Quotient_def using transpI by metis
   1.217  
   1.218  lemma identity_quotient:
   1.219    shows "Quotient (op =) id id"
   1.220 @@ -291,8 +173,7 @@
   1.221    and     a: "R xa xb" "R ya yb"
   1.222    shows "R xa ya = R xb yb"
   1.223    using a Quotient_symp[OF q] Quotient_transp[OF q]
   1.224 -  unfolding symp_def transp_def
   1.225 -  by blast
   1.226 +  by (blast elim: sympE transpE)
   1.227  
   1.228  lemma lambda_prs:
   1.229    assumes q1: "Quotient R1 Abs1 Rep1"
   1.230 @@ -300,7 +181,7 @@
   1.231    shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
   1.232    unfolding fun_eq_iff
   1.233    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   1.234 -  by (simp add:)
   1.235 +  by simp
   1.236  
   1.237  lemma lambda_prs1:
   1.238    assumes q1: "Quotient R1 Abs1 Rep1"
   1.239 @@ -308,7 +189,7 @@
   1.240    shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
   1.241    unfolding fun_eq_iff
   1.242    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   1.243 -  by (simp add:)
   1.244 +  by simp
   1.245  
   1.246  lemma rep_abs_rsp:
   1.247    assumes q: "Quotient R Abs Rep"
   1.248 @@ -392,9 +273,7 @@
   1.249    apply(simp add: in_respects fun_rel_def)
   1.250    apply(rule impI)
   1.251    using a equivp_reflp_symp_transp[of "R2"]
   1.252 -  apply(simp add: reflp_def)
   1.253 -  apply(simp)
   1.254 -  apply(simp)
   1.255 +  apply (auto elim: equivpE reflpE)
   1.256    done
   1.257  
   1.258  lemma bex_reg_eqv_range:
   1.259 @@ -406,7 +285,7 @@
   1.260    apply(simp add: Respects_def in_respects fun_rel_def)
   1.261    apply(rule impI)
   1.262    using a equivp_reflp_symp_transp[of "R2"]
   1.263 -  apply(simp add: reflp_def)
   1.264 +  apply (auto elim: equivpE reflpE)
   1.265    done
   1.266  
   1.267  (* Next four lemmas are unused *)