move alternative definition lemmas into Lifting.thy;
authorhuffman
Sat Apr 21 13:12:27 2012 +0200 (2012-04-21)
changeset 476521b722b100301
parent 47651 8e4f50afd21a
child 47653 4605d4341b8b
child 47654 f7df7104d13e
move alternative definition lemmas into Lifting.thy;
simplify proof of Quotient_compose
src/HOL/Library/Quotient_Set.thy
src/HOL/Lifting.thy
     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 13:06:22 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 13:12:27 2012 +0200
     1.3 @@ -174,17 +174,6 @@
     1.4  
     1.5  subsection {* Setup for lifting package *}
     1.6  
     1.7 -lemma Quotient_alt_def3:
     1.8 -  "Quotient R Abs Rep T \<longleftrightarrow>
     1.9 -    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and>
    1.10 -    (\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))"
    1.11 -  unfolding Quotient_alt_def2 by (safe, metis+)
    1.12 -
    1.13 -lemma Quotient_alt_def4:
    1.14 -  "Quotient R Abs Rep T \<longleftrightarrow>
    1.15 -    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
    1.16 -  unfolding Quotient_alt_def3 fun_eq_iff by auto
    1.17 -
    1.18  lemma Quotient_set:
    1.19    assumes "Quotient R Abs Rep T"
    1.20    shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
     2.1 --- a/src/HOL/Lifting.thy	Sat Apr 21 13:06:22 2012 +0200
     2.2 +++ b/src/HOL/Lifting.thy	Sat Apr 21 13:12:27 2012 +0200
     2.3 @@ -99,6 +99,8 @@
     2.4  lemma identity_quotient: "Quotient (op =) id id (op =)"
     2.5  unfolding Quotient_def by simp 
     2.6  
     2.7 +text {* TODO: Use one of these alternatives as the real definition. *}
     2.8 +
     2.9  lemma Quotient_alt_def:
    2.10    "Quotient R Abs Rep T \<longleftrightarrow>
    2.11      (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
    2.12 @@ -125,6 +127,17 @@
    2.13      (\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))"
    2.14    unfolding Quotient_alt_def by (safe, metis+)
    2.15  
    2.16 +lemma Quotient_alt_def3:
    2.17 +  "Quotient R Abs Rep T \<longleftrightarrow>
    2.18 +    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and>
    2.19 +    (\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))"
    2.20 +  unfolding Quotient_alt_def2 by (safe, metis+)
    2.21 +
    2.22 +lemma Quotient_alt_def4:
    2.23 +  "Quotient R Abs Rep T \<longleftrightarrow>
    2.24 +    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
    2.25 +  unfolding Quotient_alt_def3 fun_eq_iff by auto
    2.26 +
    2.27  lemma fun_quotient:
    2.28    assumes 1: "Quotient R1 abs1 rep1 T1"
    2.29    assumes 2: "Quotient R2 abs2 rep2 T2"
    2.30 @@ -160,42 +173,7 @@
    2.31    assumes 1: "Quotient R1 Abs1 Rep1 T1"
    2.32    assumes 2: "Quotient R2 Abs2 Rep2 T2"
    2.33    shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
    2.34 -proof -
    2.35 -  from 1 have Abs1: "\<And>a b. T1 a b \<Longrightarrow> Abs1 a = b"
    2.36 -    unfolding Quotient_alt_def by simp
    2.37 -  from 1 have Rep1: "\<And>b. T1 (Rep1 b) b"
    2.38 -    unfolding Quotient_alt_def by simp
    2.39 -  from 2 have Abs2: "\<And>a b. T2 a b \<Longrightarrow> Abs2 a = b"
    2.40 -    unfolding Quotient_alt_def by simp
    2.41 -  from 2 have Rep2: "\<And>b. T2 (Rep2 b) b"
    2.42 -    unfolding Quotient_alt_def by simp
    2.43 -  from 2 have R2:
    2.44 -    "\<And>x y. R2 x y \<longleftrightarrow> T2 x (Abs2 x) \<and> T2 y (Abs2 y) \<and> Abs2 x = Abs2 y"
    2.45 -    unfolding Quotient_alt_def by simp
    2.46 -  show ?thesis
    2.47 -    unfolding Quotient_alt_def
    2.48 -    apply simp
    2.49 -    apply safe
    2.50 -    apply (drule Abs1, simp)
    2.51 -    apply (erule Abs2)
    2.52 -    apply (rule relcomppI)
    2.53 -    apply (rule Rep1)
    2.54 -    apply (rule Rep2)
    2.55 -    apply (rule relcomppI, assumption)
    2.56 -    apply (drule Abs1, simp)
    2.57 -    apply (clarsimp simp add: R2)
    2.58 -    apply (rule relcomppI, assumption)
    2.59 -    apply (drule Abs1, simp)+
    2.60 -    apply (clarsimp simp add: R2)
    2.61 -    apply (drule Abs1, simp)+
    2.62 -    apply (clarsimp simp add: R2)
    2.63 -    apply (rule relcomppI, assumption)
    2.64 -    apply (rule relcomppI [rotated])
    2.65 -    apply (erule conversepI)
    2.66 -    apply (drule Abs1, simp)+
    2.67 -    apply (simp add: R2)
    2.68 -    done
    2.69 -qed
    2.70 +  using assms unfolding Quotient_alt_def4 by (auto intro!: ext)
    2.71  
    2.72  lemma equivp_reflp2:
    2.73    "equivp R \<Longrightarrow> reflp R"