src/HOL/Lifting.thy
changeset 47536 8474a865a4e5
parent 47535 0f94b02fda1c
child 47537 b06be48923a4
     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 +  "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
    1.42 +  using a unfolding Quotient_def
    1.43    by blast
    1.44  
    1.45 -lemma Quotient_refl1: 
    1.46 -  assumes a: "Quotient R Abs Rep T" 
    1.47 -  shows "R r s \<Longrightarrow> R r r"
    1.48 -  using a unfolding Quotient_def 
    1.49 -  by fast
    1.50 -
    1.51 -lemma Quotient_refl2: 
    1.52 -  assumes a: "Quotient R Abs Rep T" 
    1.53 -  shows "R r s \<Longrightarrow> R s s"
    1.54 -  using a unfolding Quotient_def 
    1.55 -  by fast
    1.56 -
    1.57 -lemma Quotient_rel_rep:
    1.58 -  assumes a: "Quotient R Abs Rep T"
    1.59 -  shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
    1.60 -  using a
    1.61 -  unfolding Quotient_def
    1.62 -  by metis
    1.63 -
    1.64 -lemma Quotient_rep_abs:
    1.65 -  assumes a: "Quotient R Abs Rep T"
    1.66 -  shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
    1.67 +lemma Quotient_cr_rel: "T = (\<lambda>x y. R x x \<and> Abs x = y)"
    1.68    using a unfolding Quotient_def
    1.69    by blast
    1.70  
    1.71 -lemma Quotient_rel_abs:
    1.72 -  assumes a: "Quotient R Abs Rep T"
    1.73 -  shows "R r s \<Longrightarrow> Abs r = Abs s"
    1.74 +lemma Quotient_refl1: "R r s \<Longrightarrow> R r r"
    1.75 +  using a unfolding Quotient_def
    1.76 +  by fast
    1.77 +
    1.78 +lemma Quotient_refl2: "R r s \<Longrightarrow> R s s"
    1.79 +  using a unfolding Quotient_def
    1.80 +  by fast
    1.81 +
    1.82 +lemma Quotient_rel_rep: "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
    1.83 +  using a unfolding Quotient_def
    1.84 +  by metis
    1.85 +
    1.86 +lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r"
    1.87    using a unfolding Quotient_def
    1.88    by blast
    1.89  
    1.90 -lemma Quotient_symp:
    1.91 -  assumes a: "Quotient R Abs Rep T"
    1.92 -  shows "symp R"
    1.93 +lemma Quotient_rel_abs: "R r s \<Longrightarrow> Abs r = Abs s"
    1.94 +  using a unfolding Quotient_def
    1.95 +  by blast
    1.96 +
    1.97 +lemma Quotient_symp: "symp R"
    1.98    using a unfolding Quotient_def using sympI by (metis (full_types))
    1.99  
   1.100 -lemma Quotient_transp:
   1.101 -  assumes a: "Quotient R Abs Rep T"
   1.102 -  shows "transp R"
   1.103 +lemma Quotient_transp: "transp R"
   1.104    using a unfolding Quotient_def using transpI by (metis (full_types))
   1.105  
   1.106 -lemma Quotient_part_equivp:
   1.107 -  assumes a: "Quotient R Abs Rep T"
   1.108 -  shows "part_equivp R"
   1.109 -by (metis Quotient_rep_reflp Quotient_symp Quotient_transp a part_equivpI)
   1.110 +lemma Quotient_part_equivp: "part_equivp R"
   1.111 +by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI)
   1.112 +
   1.113 +end
   1.114  
   1.115  lemma identity_quotient: "Quotient (op =) id id (op =)"
   1.116  unfolding Quotient_def by simp