src/HOL/Lifting.thy
changeset 55731 66df76dd2640
parent 55610 9066b603dff6
child 55737 84f6ac9f6e41
--- a/src/HOL/Lifting.thy	Mon Feb 24 23:17:55 2014 +0000
+++ b/src/HOL/Lifting.thy	Tue Feb 25 15:02:19 2014 +0100
@@ -591,6 +591,21 @@
 
 subsection {* Domains *}
 
+lemma composed_equiv_rel_invariant:
+  assumes "left_unique R"
+  assumes "(R ===> op=) P P'"
+  assumes "Domainp R = P''"
+  shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) = Lifting.invariant (inf P'' P)"
+using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def fun_rel_def invariant_def
+fun_eq_iff by blast
+
+lemma composed_equiv_rel_eq_invariant:
+  assumes "left_unique R"
+  assumes "Domainp R = P"
+  shows "(R OO op= OO R\<inverse>\<inverse>) = Lifting.invariant P"
+using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def invariant_def
+fun_eq_iff is_equality_def by metis
+
 lemma pcr_Domainp_par_left_total:
   assumes "Domainp B = P"
   assumes "left_total A"