author haftmann Mon Nov 29 12:15:14 2010 +0100 (2010-11-29) changeset 40814 fa64f6278568 parent 40813 f1fc2a1547eb child 40815 6e2d17cc0d1d
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
moved generic definitions about relations from Quotient.thy to Predicate;
consistent use of R rather than E for relations;
more natural deduction rules
 src/HOL/Quotient.thy file | annotate | diff | revisions
```     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.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.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.250    apply(rule impI)
1.251    using a equivp_reflp_symp_transp[of "R2"]
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"]