1.1 --- a/src/HOL/Lifting.thy	Wed Apr 18 12:15:20 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 18 14:34:25 2012 +0200
     1.3 @@ -43,79 +43,58 @@
     1.4    shows "Quotient R Abs Rep T"
     1.5    using assms unfolding Quotient_def by blast
     1.6  
     1.7 -lemma Quotient_abs_rep:
     1.8 +context
     1.9 +  fixes R Abs Rep T
    1.10    assumes a: "Quotient R Abs Rep T"
    1.11 -  shows "Abs (Rep a) = a"
    1.12 -  using a
    1.13 -  unfolding Quotient_def
    1.14 +begin
    1.15 +
    1.16 +lemma Quotient_abs_rep: "Abs (Rep a) = a"
    1.17 +  using a unfolding Quotient_def
    1.18    by simp
    1.19  
    1.20 -lemma Quotient_rep_reflp:
    1.21 -  assumes a: "Quotient R Abs Rep T"
    1.22 -  shows "R (Rep a) (Rep a)"
    1.23 -  using a
    1.24 -  unfolding Quotient_def
    1.25 +lemma Quotient_rep_reflp: "R (Rep a) (Rep a)"
    1.26 +  using a unfolding Quotient_def
    1.27    by blast
    1.28  
    1.29  lemma Quotient_rel:
    1.30 -  assumes a: "Quotient R Abs Rep T"
    1.31 -  shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
    1.32 -  using a
    1.33 -  unfolding Quotient_def
    1.34 -  by blast
    1.35 -
    1.36 -lemma Quotient_cr_rel:
    1.37 -  assumes a: "Quotient R Abs Rep T"
    1.38 -  shows "T = (\<lambda>x y. R x x \<and> Abs x = y)"
    1.39 -  using a
    1.40 -  unfolding Quotient_def
    1.41 -  by blast
    1.42 -
    1.43 -lemma Quotient_refl1: 
    1.44 -  assumes a: "Quotient R Abs Rep T" 
    1.45 -  shows "R r s \<Longrightarrow> R r r"
    1.46 -  using a unfolding Quotient_def 
    1.47 -  by fast
    1.48 -
    1.49 -lemma Quotient_refl2: 
    1.50 -  assumes a: "Quotient R Abs Rep T" 
    1.51 -  shows "R r s \<Longrightarrow> R s s"
    1.52 -  using a unfolding Quotient_def 
    1.53 -  by fast
    1.54 -
    1.55 -lemma Quotient_rel_rep:
    1.56 -  assumes a: "Quotient R Abs Rep T"
    1.57 -  shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
    1.58 -  using a
    1.59 -  unfolding Quotient_def
    1.60 -  by metis
    1.61 -
    1.62 -lemma Quotient_rep_abs:
    1.63 -  assumes a: "Quotient R Abs Rep T"
    1.64 -  shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
    1.65 +  "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
    1.66    using a unfolding Quotient_def
    1.67    by blast
    1.68  
    1.69 -lemma Quotient_rel_abs:
    1.70 -  assumes a: "Quotient R Abs Rep T"
    1.71 -  shows "R r s \<Longrightarrow> Abs r = Abs s"
    1.72 +lemma Quotient_cr_rel: "T = (\<lambda>x y. R x x \<and> Abs x = y)"
    1.73    using a unfolding Quotient_def
    1.74    by blast
    1.75  
    1.76 -lemma Quotient_symp:
    1.77 -  assumes a: "Quotient R Abs Rep T"
    1.78 -  shows "symp R"
    1.79 +lemma Quotient_refl1: "R r s \<Longrightarrow> R r r"
    1.80 +  using a unfolding Quotient_def
    1.81 +  by fast
    1.82 +
    1.83 +lemma Quotient_refl2: "R r s \<Longrightarrow> R s s"
    1.84 +  using a unfolding Quotient_def
    1.85 +  by fast
    1.86 +
    1.87 +lemma Quotient_rel_rep: "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
    1.88 +  using a unfolding Quotient_def
    1.89 +  by metis
    1.90 +
    1.91 +lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r"
    1.92 +  using a unfolding Quotient_def
    1.93 +  by blast
    1.94 +
    1.95 +lemma Quotient_rel_abs: "R r s \<Longrightarrow> Abs r = Abs s"
    1.96 +  using a unfolding Quotient_def
    1.97 +  by blast
    1.98 +
    1.99 +lemma Quotient_symp: "symp R"
   1.100    using a unfolding Quotient_def using sympI by (metis (full_types))
   1.101  
   1.102 -lemma Quotient_transp:
   1.103 -  assumes a: "Quotient R Abs Rep T"
   1.104 -  shows "transp R"
   1.105 +lemma Quotient_transp: "transp R"
   1.106    using a unfolding Quotient_def using transpI by (metis (full_types))
   1.107  
   1.108 -lemma Quotient_part_equivp:
   1.109 -  assumes a: "Quotient R Abs Rep T"
   1.110 -  shows "part_equivp R"
   1.111 -by (metis Quotient_rep_reflp Quotient_symp Quotient_transp a part_equivpI)
   1.112 +lemma Quotient_part_equivp: "part_equivp R"
   1.113 +by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI)
   1.114 +
   1.115 +end
   1.116  
   1.117  lemma identity_quotient: "Quotient (op =) id id (op =)"
   1.118  unfolding Quotient_def by simp