src/HOL/Lifting.thy
changeset 55731 66df76dd2640
parent 55610 9066b603dff6
child 55737 84f6ac9f6e41
     1.1 --- a/src/HOL/Lifting.thy	Mon Feb 24 23:17:55 2014 +0000
     1.2 +++ b/src/HOL/Lifting.thy	Tue Feb 25 15:02:19 2014 +0100
     1.3 @@ -591,6 +591,21 @@
     1.4  
     1.5  subsection {* Domains *}
     1.6  
     1.7 +lemma composed_equiv_rel_invariant:
     1.8 +  assumes "left_unique R"
     1.9 +  assumes "(R ===> op=) P P'"
    1.10 +  assumes "Domainp R = P''"
    1.11 +  shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) = Lifting.invariant (inf P'' P)"
    1.12 +using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def fun_rel_def invariant_def
    1.13 +fun_eq_iff by blast
    1.14 +
    1.15 +lemma composed_equiv_rel_eq_invariant:
    1.16 +  assumes "left_unique R"
    1.17 +  assumes "Domainp R = P"
    1.18 +  shows "(R OO op= OO R\<inverse>\<inverse>) = Lifting.invariant P"
    1.19 +using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def invariant_def
    1.20 +fun_eq_iff is_equality_def by metis
    1.21 +
    1.22  lemma pcr_Domainp_par_left_total:
    1.23    assumes "Domainp B = P"
    1.24    assumes "left_total A"