# HG changeset patch
# User huffman
# Date 1335006747 -7200
# Node ID 1b722b10030104f550328f3e144f78c838f51a7e
# Parent  8e4f50afd21a89f2b23b44419a3b3890981ed9bb
move alternative definition lemmas into Lifting.thy;
simplify proof of Quotient_compose

diff -r 8e4f50afd21a -r 1b722b100301 src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 13:06:22 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 13:12:27 2012 +0200
@@ -174,17 +174,6 @@
 
 subsection {* Setup for lifting package *}
 
-lemma Quotient_alt_def3:
-  "Quotient R Abs Rep T \<longleftrightarrow>
-    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and>
-    (\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))"
-  unfolding Quotient_alt_def2 by (safe, metis+)
-
-lemma Quotient_alt_def4:
-  "Quotient R Abs Rep T \<longleftrightarrow>
-    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
-  unfolding Quotient_alt_def3 fun_eq_iff by auto
-
 lemma Quotient_set:
   assumes "Quotient R Abs Rep T"
   shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
diff -r 8e4f50afd21a -r 1b722b100301 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Sat Apr 21 13:06:22 2012 +0200
+++ b/src/HOL/Lifting.thy	Sat Apr 21 13:12:27 2012 +0200
@@ -99,6 +99,8 @@
 lemma identity_quotient: "Quotient (op =) id id (op =)"
 unfolding Quotient_def by simp 
 
+text {* TODO: Use one of these alternatives as the real definition. *}
+
 lemma Quotient_alt_def:
   "Quotient R Abs Rep T \<longleftrightarrow>
     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
@@ -125,6 +127,17 @@
     (\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))"
   unfolding Quotient_alt_def by (safe, metis+)
 
+lemma Quotient_alt_def3:
+  "Quotient R Abs Rep T \<longleftrightarrow>
+    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and>
+    (\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))"
+  unfolding Quotient_alt_def2 by (safe, metis+)
+
+lemma Quotient_alt_def4:
+  "Quotient R Abs Rep T \<longleftrightarrow>
+    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
+  unfolding Quotient_alt_def3 fun_eq_iff by auto
+
 lemma fun_quotient:
   assumes 1: "Quotient R1 abs1 rep1 T1"
   assumes 2: "Quotient R2 abs2 rep2 T2"
@@ -160,42 +173,7 @@
   assumes 1: "Quotient R1 Abs1 Rep1 T1"
   assumes 2: "Quotient R2 Abs2 Rep2 T2"
   shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
-proof -
-  from 1 have Abs1: "\<And>a b. T1 a b \<Longrightarrow> Abs1 a = b"
-    unfolding Quotient_alt_def by simp
-  from 1 have Rep1: "\<And>b. T1 (Rep1 b) b"
-    unfolding Quotient_alt_def by simp
-  from 2 have Abs2: "\<And>a b. T2 a b \<Longrightarrow> Abs2 a = b"
-    unfolding Quotient_alt_def by simp
-  from 2 have Rep2: "\<And>b. T2 (Rep2 b) b"
-    unfolding Quotient_alt_def by simp
-  from 2 have R2:
-    "\<And>x y. R2 x y \<longleftrightarrow> T2 x (Abs2 x) \<and> T2 y (Abs2 y) \<and> Abs2 x = Abs2 y"
-    unfolding Quotient_alt_def by simp
-  show ?thesis
-    unfolding Quotient_alt_def
-    apply simp
-    apply safe
-    apply (drule Abs1, simp)
-    apply (erule Abs2)
-    apply (rule relcomppI)
-    apply (rule Rep1)
-    apply (rule Rep2)
-    apply (rule relcomppI, assumption)
-    apply (drule Abs1, simp)
-    apply (clarsimp simp add: R2)
-    apply (rule relcomppI, assumption)
-    apply (drule Abs1, simp)+
-    apply (clarsimp simp add: R2)
-    apply (drule Abs1, simp)+
-    apply (clarsimp simp add: R2)
-    apply (rule relcomppI, assumption)
-    apply (rule relcomppI [rotated])
-    apply (erule conversepI)
-    apply (drule Abs1, simp)+
-    apply (simp add: R2)
-    done
-qed
+  using assms unfolding Quotient_alt_def4 by (auto intro!: ext)
 
 lemma equivp_reflp2:
   "equivp R \<Longrightarrow> reflp R"