17 | "sum_map f1 f2 (Inr a) = Inr (f2 a)" |
20 | "sum_map f1 f2 (Inr a) = Inr (f2 a)" |
18 |
21 |
19 declare [[map "+" = (sum_map, sum_rel)]] |
22 declare [[map "+" = (sum_map, sum_rel)]] |
20 |
23 |
21 |
24 |
|
25 text {* should probably be in Sum_Type.thy *} |
|
26 lemma split_sum_all: |
|
27 shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))" |
|
28 apply(auto) |
|
29 apply(case_tac x) |
|
30 apply(simp_all) |
|
31 done |
|
32 |
22 lemma sum_equivp[quot_equiv]: |
33 lemma sum_equivp[quot_equiv]: |
23 assumes a: "equivp R1" |
34 assumes a: "equivp R1" |
24 assumes b: "equivp R2" |
35 assumes b: "equivp R2" |
25 shows "equivp (sum_rel R1 R2)" |
36 shows "equivp (sum_rel R1 R2)" |
26 apply(rule equivpI) |
37 apply(rule equivpI) |
27 unfolding reflp_def symp_def transp_def |
38 unfolding reflp_def symp_def transp_def |
28 apply(auto) |
39 apply(simp_all add: split_sum_all) |
29 apply(case_tac [!] x) |
40 apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b]) |
30 apply(simp_all add: equivp_reflp[OF a] equivp_reflp[OF b]) |
41 apply(blast intro: equivp_symp[OF a] equivp_symp[OF b]) |
31 apply(case_tac [!] y) |
42 apply(blast intro: equivp_transp[OF a] equivp_transp[OF b]) |
32 apply(simp_all add: equivp_symp[OF a] equivp_symp[OF b]) |
|
33 apply(case_tac [!] z) |
|
34 apply(simp_all) |
|
35 apply(rule equivp_transp[OF a]) |
|
36 apply(assumption)+ |
|
37 apply(rule equivp_transp[OF b]) |
|
38 apply(assumption)+ |
|
39 done |
43 done |
40 |
|
41 (* |
|
42 lemma sum_fun_fun: |
|
43 assumes q1: "Quotient R1 Abs1 Rep1" |
|
44 assumes q2: "Quotient R2 Abs2 Rep2" |
|
45 shows "sum_rel R1 R2 r s = |
|
46 (sum_rel R1 R2 r r \<and> sum_rel R1 R2 s s \<and> sum_map Abs1 Abs2 r = sum_map Abs1 Abs2 s)" |
|
47 using q1 q2 |
|
48 apply(case_tac r) |
|
49 apply(case_tac s) |
|
50 apply(simp_all) |
|
51 prefer 2 |
|
52 apply(case_tac s) |
|
53 apply(auto) |
|
54 unfolding Quotient_def |
|
55 apply metis+ |
|
56 done |
|
57 *) |
|
58 |
44 |
59 lemma sum_quotient[quot_thm]: |
45 lemma sum_quotient[quot_thm]: |
60 assumes q1: "Quotient R1 Abs1 Rep1" |
46 assumes q1: "Quotient R1 Abs1 Rep1" |
61 assumes q2: "Quotient R2 Abs2 Rep2" |
47 assumes q2: "Quotient R2 Abs2 Rep2" |
62 shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" |
48 shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" |
63 unfolding Quotient_def |
49 unfolding Quotient_def |
64 apply(auto) |
50 apply(simp add: split_sum_all) |
65 apply(case_tac a) |
51 apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1]) |
66 apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1] |
52 apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) |
67 Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) |
|
68 apply(case_tac a) |
|
69 apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1] |
|
70 Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) |
|
71 apply(case_tac [!] r) |
|
72 apply(case_tac [!] s) |
|
73 apply(simp_all) |
|
74 using q1 q2 |
53 using q1 q2 |
75 unfolding Quotient_def |
54 unfolding Quotient_def |
76 apply(blast)+ |
55 apply(blast)+ |
77 done |
56 done |
78 |
57 |
|
58 lemma sum_Inl_rsp[quot_respect]: |
|
59 assumes q1: "Quotient R1 Abs1 Rep1" |
|
60 assumes q2: "Quotient R2 Abs2 Rep2" |
|
61 shows "(R1 ===> sum_rel R1 R2) Inl Inl" |
|
62 by simp |
|
63 |
|
64 lemma sum_Inr_rsp[quot_respect]: |
|
65 assumes q1: "Quotient R1 Abs1 Rep1" |
|
66 assumes q2: "Quotient R2 Abs2 Rep2" |
|
67 shows "(R2 ===> sum_rel R1 R2) Inr Inr" |
|
68 by simp |
|
69 |
|
70 lemma sum_Inl_prs[quot_respect]: |
|
71 assumes q1: "Quotient R1 Abs1 Rep1" |
|
72 assumes q2: "Quotient R2 Abs2 Rep2" |
|
73 shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" |
|
74 apply(simp add: expand_fun_eq) |
|
75 apply(simp add: Quotient_abs_rep[OF q1]) |
|
76 done |
|
77 |
|
78 lemma sum_Inr_prs[quot_respect]: |
|
79 assumes q1: "Quotient R1 Abs1 Rep1" |
|
80 assumes q2: "Quotient R2 Abs2 Rep2" |
|
81 shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" |
|
82 apply(simp add: expand_fun_eq) |
|
83 apply(simp add: Quotient_abs_rep[OF q2]) |
|
84 done |
|
85 |
79 lemma sum_map_id[id_simps]: |
86 lemma sum_map_id[id_simps]: |
80 shows "sum_map id id \<equiv> id" |
87 shows "sum_map id id \<equiv> id" |
81 apply (rule eq_reflection) |
88 apply (rule eq_reflection) |
82 apply (rule ext) |
89 apply (simp add: expand_fun_eq split_sum_all) |
83 apply (case_tac x) |
|
84 apply (auto) |
|
85 done |
90 done |
86 |
91 |
87 lemma sum_rel_eq[id_simps]: |
92 lemma sum_rel_eq[id_simps]: |
88 "sum_rel op = op = \<equiv> op =" |
93 shows "sum_rel (op =) (op =) \<equiv> (op =)" |
89 apply (rule eq_reflection) |
94 apply (rule eq_reflection) |
90 apply (rule ext)+ |
95 apply(simp add: expand_fun_eq split_sum_all) |
91 apply (case_tac x) |
|
92 apply auto |
|
93 apply (case_tac xa) |
|
94 apply auto |
|
95 apply (case_tac xa) |
|
96 apply auto |
|
97 done |
96 done |
98 |
97 |
99 end |
98 end |