src/HOL/Library/Quotient_Sum.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (7 months ago) changeset 69946 494934c30f38 parent 67399 eab6ce8368fa permissions -rw-r--r--
improved code equations taken over from AFP
1 (*  Title:      HOL/Library/Quotient_Sum.thy
2     Author:     Cezary Kaliszyk and Christian Urban
3 *)
5 section \<open>Quotient infrastructure for the sum type\<close>
7 theory Quotient_Sum
8 imports Quotient_Syntax
9 begin
11 subsection \<open>Rules for the Quotient package\<close>
13 lemma rel_sum_map1:
14   "rel_sum R1 R2 (map_sum f1 f2 x) y \<longleftrightarrow> rel_sum (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
15   by (rule sum.rel_map(1))
17 lemma rel_sum_map2:
18   "rel_sum R1 R2 x (map_sum f1 f2 y) \<longleftrightarrow> rel_sum (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
19   by (rule sum.rel_map(2))
21 lemma map_sum_id [id_simps]:
22   "map_sum id id = id"
23   by (simp add: id_def map_sum.identity fun_eq_iff)
25 lemma rel_sum_eq [id_simps]:
26   "rel_sum (=) (=) = (=)"
27   by (rule sum.rel_eq)
29 lemma reflp_rel_sum:
30   "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (rel_sum R1 R2)"
31   unfolding reflp_def split_sum_all rel_sum_simps by fast
33 lemma sum_symp:
34   "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (rel_sum R1 R2)"
35   unfolding symp_def split_sum_all rel_sum_simps by fast
37 lemma sum_transp:
38   "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (rel_sum R1 R2)"
39   unfolding transp_def split_sum_all rel_sum_simps by fast
41 lemma sum_equivp [quot_equiv]:
42   "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (rel_sum R1 R2)"
43   by (blast intro: equivpI reflp_rel_sum sum_symp sum_transp elim: equivpE)
45 lemma sum_quotient [quot_thm]:
46   assumes q1: "Quotient3 R1 Abs1 Rep1"
47   assumes q2: "Quotient3 R2 Abs2 Rep2"
48   shows "Quotient3 (rel_sum R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2)"
49   apply (rule Quotient3I)
50   apply (simp_all add: map_sum.compositionality comp_def map_sum.identity rel_sum_eq rel_sum_map1 rel_sum_map2
51     Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
52   using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
53   apply (fastforce elim!: rel_sum.cases simp add: comp_def split: sum.split)
54   done
56 declare [[mapQ3 sum = (rel_sum, sum_quotient)]]
58 lemma sum_Inl_rsp [quot_respect]:
59   assumes q1: "Quotient3 R1 Abs1 Rep1"
60   assumes q2: "Quotient3 R2 Abs2 Rep2"
61   shows "(R1 ===> rel_sum R1 R2) Inl Inl"
62   by auto
64 lemma sum_Inr_rsp [quot_respect]:
65   assumes q1: "Quotient3 R1 Abs1 Rep1"
66   assumes q2: "Quotient3 R2 Abs2 Rep2"
67   shows "(R2 ===> rel_sum R1 R2) Inr Inr"
68   by auto
70 lemma sum_Inl_prs [quot_preserve]:
71   assumes q1: "Quotient3 R1 Abs1 Rep1"
72   assumes q2: "Quotient3 R2 Abs2 Rep2"
73   shows "(Rep1 ---> map_sum Abs1 Abs2) Inl = Inl"