src/HOL/Library/Quotient_Sum.thy
changeset 47634 091bcd569441
parent 47624 16d433895d2e
child 47635 ebb79474262c
--- a/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 15:49:45 2012 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 18:29:21 2012 +0200
@@ -102,6 +102,22 @@
 
 declare [[map sum = (sum_rel, Quotient_sum)]]
 
+fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
+where
+  "sum_pred R1 R2 (Inl a) = R1 a"
+| "sum_pred R1 R2 (Inr a) = R2 a"
+
+lemma sum_invariant_commute [invariant_commute]: 
+  "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
+  apply (simp add: fun_eq_iff Lifting.invariant_def)
+  apply (intro allI) 
+  apply (case_tac x rule: sum.exhaust)
+  apply (case_tac xa rule: sum.exhaust)
+  apply auto[2]
+  apply (case_tac xa rule: sum.exhaust)
+  apply auto
+done
+
 subsection {* Rules for quotient package *}
 
 lemma sum_quotient [quot_thm]: