src/HOL/Library/Quotient_Sum.thy
 changeset 47634 091bcd569441 parent 47624 16d433895d2e child 47635 ebb79474262c
equal 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"`