src/HOL/Library/Quotient_Sum.thy
changeset 47634 091bcd569441
parent 47624 16d433895d2e
child 47635 ebb79474262c
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 15:49:45 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 18:29:21 2012 +0200
     1.3 @@ -102,6 +102,22 @@
     1.4  
     1.5  declare [[map sum = (sum_rel, Quotient_sum)]]
     1.6  
     1.7 +fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
     1.8 +where
     1.9 +  "sum_pred R1 R2 (Inl a) = R1 a"
    1.10 +| "sum_pred R1 R2 (Inr a) = R2 a"
    1.11 +
    1.12 +lemma sum_invariant_commute [invariant_commute]: 
    1.13 +  "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
    1.14 +  apply (simp add: fun_eq_iff Lifting.invariant_def)
    1.15 +  apply (intro allI) 
    1.16 +  apply (case_tac x rule: sum.exhaust)
    1.17 +  apply (case_tac xa rule: sum.exhaust)
    1.18 +  apply auto[2]
    1.19 +  apply (case_tac xa rule: sum.exhaust)
    1.20 +  apply auto
    1.21 +done
    1.22 +
    1.23  subsection {* Rules for quotient package *}
    1.24  
    1.25  lemma sum_quotient [quot_thm]: