src/HOL/Library/Quotient_Sum.thy
changeset 47634 091bcd569441
parent 47624 16d433895d2e
child 47635 ebb79474262c
equal deleted inserted replaced
47627:2b1d3eda59eb 47634:091bcd569441
   100   using assms unfolding Quotient_alt_def
   100   using assms unfolding Quotient_alt_def
   101   by (simp add: split_sum_all)
   101   by (simp add: split_sum_all)
   102 
   102 
   103 declare [[map sum = (sum_rel, Quotient_sum)]]
   103 declare [[map sum = (sum_rel, Quotient_sum)]]
   104 
   104 
       
   105 fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
       
   106 where
       
   107   "sum_pred R1 R2 (Inl a) = R1 a"
       
   108 | "sum_pred R1 R2 (Inr a) = R2 a"
       
   109 
       
   110 lemma sum_invariant_commute [invariant_commute]: 
       
   111   "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
       
   112   apply (simp add: fun_eq_iff Lifting.invariant_def)
       
   113   apply (intro allI) 
       
   114   apply (case_tac x rule: sum.exhaust)
       
   115   apply (case_tac xa rule: sum.exhaust)
       
   116   apply auto[2]
       
   117   apply (case_tac xa rule: sum.exhaust)
       
   118   apply auto
       
   119 done
       
   120 
   105 subsection {* Rules for quotient package *}
   121 subsection {* Rules for quotient package *}
   106 
   122 
   107 lemma sum_quotient [quot_thm]:
   123 lemma sum_quotient [quot_thm]:
   108   assumes q1: "Quotient3 R1 Abs1 Rep1"
   124   assumes q1: "Quotient3 R1 Abs1 Rep1"
   109   assumes q2: "Quotient3 R2 Abs2 Rep2"
   125   assumes q2: "Quotient3 R2 Abs2 Rep2"