# HG changeset patch
# User haftmann
# Date 1291029314 -3600
# Node ID fa64f627856824ef83d3f2c0b258e8cd15b056c9
# Parent  f1fc2a1547eb27f15bbab0d374d962c1edb5244c
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

diff -r f1fc2a1547eb -r fa64f6278568 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Mon Nov 29 12:14:46 2010 +0100
+++ b/src/HOL/Quotient.thy	Mon Nov 29 12:15:14 2010 +0100
@@ -14,127 +14,11 @@
   ("Tools/Quotient/quotient_tacs.ML")
 begin
 
-
 text {*
   Basic definition for equivalence relations
   that are represented by predicates.
 *}
 
-definition
-  "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
-
-lemma refl_reflp:
-  "refl A \<longleftrightarrow> reflp (\<lambda>x y. (x, y) \<in> A)"
-  by (simp add: refl_on_def reflp_def)
-
-definition
-  "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
-
-lemma sym_symp:
-  "sym A \<longleftrightarrow> symp (\<lambda>x y. (x, y) \<in> A)"
-  by (simp add: sym_def symp_def)
-
-definition
-  "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
-
-lemma trans_transp:
-  "trans A \<longleftrightarrow> transp (\<lambda>x y. (x, y) \<in> A)"
-  by (auto simp add: trans_def transp_def)
-
-definition
-  "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
-
-lemma equivp_reflp_symp_transp:
-  shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
-  unfolding equivp_def reflp_def symp_def transp_def fun_eq_iff
-  by blast
-
-lemma equiv_equivp:
-  "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
-  by (simp add: equiv_def equivp_reflp_symp_transp refl_reflp sym_symp trans_transp)
-
-lemma equivp_reflp:
-  shows "equivp E \<Longrightarrow> E x x"
-  by (simp only: equivp_reflp_symp_transp reflp_def)
-
-lemma equivp_symp:
-  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
-  by (simp add: equivp_def)
-
-lemma equivp_transp:
-  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
-  by (simp add: equivp_def)
-
-lemma equivpI:
-  assumes "reflp R" "symp R" "transp R"
-  shows "equivp R"
-  using assms by (simp add: equivp_reflp_symp_transp)
-
-lemma identity_equivp:
-  shows "equivp (op =)"
-  unfolding equivp_def
-  by auto
-
-text {* Partial equivalences *}
-
-definition
-  "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)))"
-
-lemma equivp_implies_part_equivp:
-  assumes a: "equivp E"
-  shows "part_equivp E"
-  using a
-  unfolding equivp_def part_equivp_def
-  by auto
-
-lemma part_equivp_symp:
-  assumes e: "part_equivp R"
-  and a: "R x y"
-  shows "R y x"
-  using e[simplified part_equivp_def] a
-  by (metis)
-
-lemma part_equivp_typedef:
-  shows "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
-  unfolding part_equivp_def mem_def
-  apply clarify
-  apply (intro exI)
-  apply (rule conjI)
-  apply assumption
-  apply (rule refl)
-  done
-
-lemma part_equivp_refl_symp_transp:
-  shows "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> symp E \<and> transp E)"
-proof
-  assume "part_equivp E"
-  then show "(\<exists>x. E x x) \<and> symp E \<and> transp E"
-  unfolding part_equivp_def symp_def transp_def
-  by metis
-next
-  assume a: "(\<exists>x. E x x) \<and> symp E \<and> transp E"
-  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)"
-    unfolding symp_def transp_def by (metis, metis)
-  have "(\<forall>x y. E x y = (E x x \<and> E y y \<and> E x = E y))"
-  proof (intro allI iffI conjI)
-    fix x y
-    assume d: "E x y"
-    then show "E x x" using b c by metis
-    show "E y y" using b c d by metis
-    show "E x = E y" unfolding fun_eq_iff using b c d by metis
-  next
-    fix x y
-    assume "E x x \<and> E y y \<and> E x = E y"
-    then show "E x y" using b c by metis
-  qed
-  then show "part_equivp E" unfolding part_equivp_def using a by metis
-qed
-
-lemma part_equivpI:
-  assumes "\<exists>x. R x x" "symp R" "transp R"
-  shows "part_equivp R"
-  using assms by (simp add: part_equivp_refl_symp_transp)
-
 text {* Composition of Relations *}
 
 abbreviation
@@ -169,16 +53,16 @@
 definition
   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)
 where
-  "fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+  "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
 
 lemma fun_relI [intro]:
-  assumes "\<And>x y. E1 x y \<Longrightarrow> E2 (f x) (g y)"
-  shows "(E1 ===> E2) f g"
+  assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+  shows "(R1 ===> R2) f g"
   using assms by (simp add: fun_rel_def)
 
 lemma fun_relE:
-  assumes "(E1 ===> E2) f g" and "E1 x y"
-  obtains "E2 (f x) (g y)"
+  assumes "(R1 ===> R2) f g" and "R1 x y"
+  obtains "R2 (f x) (g y)"
   using assms by (simp add: fun_rel_def)
 
 lemma fun_rel_eq:
@@ -189,27 +73,27 @@
 subsection {* Quotient Predicate *}
 
 definition
-  "Quotient E Abs Rep \<longleftrightarrow>
-     (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
-     (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
+  "Quotient R Abs Rep \<longleftrightarrow>
+     (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
+     (\<forall>r s. R r s = (R r r \<and> R s s \<and> (Abs r = Abs s)))"
 
 lemma Quotient_abs_rep:
-  assumes a: "Quotient E Abs Rep"
+  assumes a: "Quotient R Abs Rep"
   shows "Abs (Rep a) = a"
   using a
   unfolding Quotient_def
   by simp
 
 lemma Quotient_rep_reflp:
-  assumes a: "Quotient E Abs Rep"
-  shows "E (Rep a) (Rep a)"
+  assumes a: "Quotient R Abs Rep"
+  shows "R (Rep a) (Rep a)"
   using a
   unfolding Quotient_def
   by blast
 
 lemma Quotient_rel:
-  assumes a: "Quotient E Abs Rep"
-  shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
+  assumes a: "Quotient R Abs Rep"
+  shows " R r s = (R r r \<and> R s s \<and> (Abs r = Abs s))"
   using a
   unfolding Quotient_def
   by blast
@@ -228,22 +112,20 @@
   by blast
 
 lemma Quotient_rel_abs:
-  assumes a: "Quotient E Abs Rep"
-  shows "E r s \<Longrightarrow> Abs r = Abs s"
+  assumes a: "Quotient R Abs Rep"
+  shows "R r s \<Longrightarrow> Abs r = Abs s"
   using a unfolding Quotient_def
   by blast
 
 lemma Quotient_symp:
-  assumes a: "Quotient E Abs Rep"
-  shows "symp E"
-  using a unfolding Quotient_def symp_def
-  by metis
+  assumes a: "Quotient R Abs Rep"
+  shows "symp R"
+  using a unfolding Quotient_def using sympI by metis
 
 lemma Quotient_transp:
-  assumes a: "Quotient E Abs Rep"
-  shows "transp E"
-  using a unfolding Quotient_def transp_def
-  by metis
+  assumes a: "Quotient R Abs Rep"
+  shows "transp R"
+  using a unfolding Quotient_def using transpI by metis
 
 lemma identity_quotient:
   shows "Quotient (op =) id id"
@@ -291,8 +173,7 @@
   and     a: "R xa xb" "R ya yb"
   shows "R xa ya = R xb yb"
   using a Quotient_symp[OF q] Quotient_transp[OF q]
-  unfolding symp_def transp_def
-  by blast
+  by (blast elim: sympE transpE)
 
 lemma lambda_prs:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -300,7 +181,7 @@
   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
   unfolding fun_eq_iff
   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
-  by (simp add:)
+  by simp
 
 lemma lambda_prs1:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -308,7 +189,7 @@
   shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
   unfolding fun_eq_iff
   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
-  by (simp add:)
+  by simp
 
 lemma rep_abs_rsp:
   assumes q: "Quotient R Abs Rep"
@@ -392,9 +273,7 @@
   apply(simp add: in_respects fun_rel_def)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
-  apply(simp add: reflp_def)
-  apply(simp)
-  apply(simp)
+  apply (auto elim: equivpE reflpE)
   done
 
 lemma bex_reg_eqv_range:
@@ -406,7 +285,7 @@
   apply(simp add: Respects_def in_respects fun_rel_def)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
-  apply(simp add: reflp_def)
+  apply (auto elim: equivpE reflpE)
   done
 
 (* Next four lemmas are unused *)