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