src/HOL/Library/Quotient_Sum.thy
 changeset 47094 1a7ad2601cb5 parent 45802 b16f976db515 child 47308 9caab698dbe4
equal inserted replaced
`    13 where`
`    13 where`
`    14   "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"`
`    14   "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"`
`    15 | "sum_rel R1 R2 (Inl a1) (Inr b2) = False"`
`    15 | "sum_rel R1 R2 (Inl a1) (Inr b2) = False"`
`    16 | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"`
`    16 | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"`
`    17 | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"`
`    17 | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"`
`    20 `
`    18 `
`    21 lemma sum_rel_unfold:`
`    19 lemma sum_rel_unfold:`
`    22   "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y`
`    20   "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y`
`    23     | (Inr x, Inr y) \<Rightarrow> R2 x y`
`    21     | (Inr x, Inr y) \<Rightarrow> R2 x y`
`    24     | _ \<Rightarrow> False)"`
`    22     | _ \<Rightarrow> False)"`
`    65     Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])`
`    63     Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])`
`    66   using Quotient_rel [OF q1] Quotient_rel [OF q2]`
`    64   using Quotient_rel [OF q1] Quotient_rel [OF q2]`
`    67   apply (simp add: sum_rel_unfold comp_def split: sum.split)`
`    65   apply (simp add: sum_rel_unfold comp_def split: sum.split)`
`    68   done`
`    66   done`
`    69 `
`    67 `
`       `
`    68 declare [[map sum = (sum_rel, sum_quotient)]]`
`       `
`    69 `
`    70 lemma sum_Inl_rsp [quot_respect]:`
`    70 lemma sum_Inl_rsp [quot_respect]:`
`    71   assumes q1: "Quotient R1 Abs1 Rep1"`
`    71   assumes q1: "Quotient R1 Abs1 Rep1"`
`    72   assumes q2: "Quotient R2 Abs2 Rep2"`
`    72   assumes q2: "Quotient R2 Abs2 Rep2"`
`    73   shows "(R1 ===> sum_rel R1 R2) Inl Inl"`
`    73   shows "(R1 ===> sum_rel R1 R2) Inl Inl"`
`    74   by auto`
`    74   by auto`