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
```