src/HOL/Lifting.thy
 changeset 47937 70375fa2679d parent 47936 756f30eac792 child 47982 7aa35601ff65
```     1.1 --- a/src/HOL/Lifting.thy	Wed May 16 19:15:45 2012 +0200
1.2 +++ b/src/HOL/Lifting.thy	Wed May 16 19:17:20 2012 +0200
1.3 @@ -82,10 +82,31 @@
1.4    using a unfolding Quotient_def
1.5    by blast
1.6
1.7 +lemma Quotient_rep_abs_fold_unmap:
1.8 +  assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'"
1.9 +  shows "R (Rep' x') x"
1.10 +proof -
1.11 +  have "R (Rep x') x" using assms(1-2) Quotient_rep_abs by auto
1.12 +  then show ?thesis using assms(3) by simp
1.13 +qed
1.14 +
1.15 +lemma Quotient_Rep_eq:
1.16 +  assumes "x' \<equiv> Abs x"
1.17 +  shows "Rep x' \<equiv> Rep x'"
1.18 +by simp
1.19 +
1.20  lemma Quotient_rel_abs: "R r s \<Longrightarrow> Abs r = Abs s"
1.21    using a unfolding Quotient_def
1.22    by blast
1.23
1.24 +lemma Quotient_rel_abs2:
1.25 +  assumes "R (Rep x) y"
1.26 +  shows "x = Abs y"
1.27 +proof -
1.28 +  from assms have "Abs (Rep x) = Abs y" by (auto intro: Quotient_rel_abs)
1.29 +  then show ?thesis using assms(1) by (simp add: Quotient_abs_rep)
1.30 +qed
1.31 +
1.32  lemma Quotient_symp: "symp R"
1.33    using a unfolding Quotient_def using sympI by (metis (full_types))
1.34
```