src/HOL/Lifting.thy
changeset 47652 1b722b100301
parent 47651 8e4f50afd21a
child 47698 18202d3d5832
     1.1 --- a/src/HOL/Lifting.thy	Sat Apr 21 13:06:22 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Sat Apr 21 13:12:27 2012 +0200
     1.3 @@ -99,6 +99,8 @@
     1.4  lemma identity_quotient: "Quotient (op =) id id (op =)"
     1.5  unfolding Quotient_def by simp 
     1.6  
     1.7 +text {* TODO: Use one of these alternatives as the real definition. *}
     1.8 +
     1.9  lemma Quotient_alt_def:
    1.10    "Quotient R Abs Rep T \<longleftrightarrow>
    1.11      (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
    1.12 @@ -125,6 +127,17 @@
    1.13      (\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))"
    1.14    unfolding Quotient_alt_def by (safe, metis+)
    1.15  
    1.16 +lemma Quotient_alt_def3:
    1.17 +  "Quotient R Abs Rep T \<longleftrightarrow>
    1.18 +    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and>
    1.19 +    (\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))"
    1.20 +  unfolding Quotient_alt_def2 by (safe, metis+)
    1.21 +
    1.22 +lemma Quotient_alt_def4:
    1.23 +  "Quotient R Abs Rep T \<longleftrightarrow>
    1.24 +    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
    1.25 +  unfolding Quotient_alt_def3 fun_eq_iff by auto
    1.26 +
    1.27  lemma fun_quotient:
    1.28    assumes 1: "Quotient R1 abs1 rep1 T1"
    1.29    assumes 2: "Quotient R2 abs2 rep2 T2"
    1.30 @@ -160,42 +173,7 @@
    1.31    assumes 1: "Quotient R1 Abs1 Rep1 T1"
    1.32    assumes 2: "Quotient R2 Abs2 Rep2 T2"
    1.33    shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
    1.34 -proof -
    1.35 -  from 1 have Abs1: "\<And>a b. T1 a b \<Longrightarrow> Abs1 a = b"
    1.36 -    unfolding Quotient_alt_def by simp
    1.37 -  from 1 have Rep1: "\<And>b. T1 (Rep1 b) b"
    1.38 -    unfolding Quotient_alt_def by simp
    1.39 -  from 2 have Abs2: "\<And>a b. T2 a b \<Longrightarrow> Abs2 a = b"
    1.40 -    unfolding Quotient_alt_def by simp
    1.41 -  from 2 have Rep2: "\<And>b. T2 (Rep2 b) b"
    1.42 -    unfolding Quotient_alt_def by simp
    1.43 -  from 2 have R2:
    1.44 -    "\<And>x y. R2 x y \<longleftrightarrow> T2 x (Abs2 x) \<and> T2 y (Abs2 y) \<and> Abs2 x = Abs2 y"
    1.45 -    unfolding Quotient_alt_def by simp
    1.46 -  show ?thesis
    1.47 -    unfolding Quotient_alt_def
    1.48 -    apply simp
    1.49 -    apply safe
    1.50 -    apply (drule Abs1, simp)
    1.51 -    apply (erule Abs2)
    1.52 -    apply (rule relcomppI)
    1.53 -    apply (rule Rep1)
    1.54 -    apply (rule Rep2)
    1.55 -    apply (rule relcomppI, assumption)
    1.56 -    apply (drule Abs1, simp)
    1.57 -    apply (clarsimp simp add: R2)
    1.58 -    apply (rule relcomppI, assumption)
    1.59 -    apply (drule Abs1, simp)+
    1.60 -    apply (clarsimp simp add: R2)
    1.61 -    apply (drule Abs1, simp)+
    1.62 -    apply (clarsimp simp add: R2)
    1.63 -    apply (rule relcomppI, assumption)
    1.64 -    apply (rule relcomppI [rotated])
    1.65 -    apply (erule conversepI)
    1.66 -    apply (drule Abs1, simp)+
    1.67 -    apply (simp add: R2)
    1.68 -    done
    1.69 -qed
    1.70 +  using assms unfolding Quotient_alt_def4 by (auto intro!: ext)
    1.71  
    1.72  lemma equivp_reflp2:
    1.73    "equivp R \<Longrightarrow> reflp R"