10 |
10 |
11 subsection {* Rules for the Quotient package *} |
11 subsection {* Rules for the Quotient package *} |
12 |
12 |
13 lemma sum_rel_map1: |
13 lemma sum_rel_map1: |
14 "sum_rel R1 R2 (sum_map f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y" |
14 "sum_rel R1 R2 (sum_map f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y" |
15 by (simp add: sum_rel_unfold split: sum.split) |
15 by (simp add: sum_rel_def split: sum.split) |
16 |
16 |
17 lemma sum_rel_map2: |
17 lemma sum_rel_map2: |
18 "sum_rel R1 R2 x (sum_map f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y" |
18 "sum_rel R1 R2 x (sum_map f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y" |
19 by (simp add: sum_rel_unfold split: sum.split) |
19 by (simp add: sum_rel_def split: sum.split) |
20 |
20 |
21 lemma sum_map_id [id_simps]: |
21 lemma sum_map_id [id_simps]: |
22 "sum_map id id = id" |
22 "sum_map id id = id" |
23 by (simp add: id_def sum_map.identity fun_eq_iff) |
23 by (simp add: id_def sum_map.identity fun_eq_iff) |
24 |
24 |
25 lemma sum_rel_eq [id_simps]: |
25 lemma sum_rel_eq [id_simps]: |
26 "sum_rel (op =) (op =) = (op =)" |
26 "sum_rel (op =) (op =) = (op =)" |
27 by (simp add: sum_rel_unfold fun_eq_iff split: sum.split) |
27 by (simp add: sum_rel_def fun_eq_iff split: sum.split) |
28 |
28 |
29 lemma sum_symp: |
29 lemma sum_symp: |
30 "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)" |
30 "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)" |
31 unfolding symp_def split_sum_all sum_rel.simps by fast |
31 unfolding symp_def split_sum_all sum_rel_simps by fast |
32 |
32 |
33 lemma sum_transp: |
33 lemma sum_transp: |
34 "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)" |
34 "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)" |
35 unfolding transp_def split_sum_all sum_rel.simps by fast |
35 unfolding transp_def split_sum_all sum_rel_simps by fast |
36 |
36 |
37 lemma sum_equivp [quot_equiv]: |
37 lemma sum_equivp [quot_equiv]: |
38 "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)" |
38 "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)" |
39 by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE) |
39 by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE) |
40 |
40 |
44 shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" |
44 shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" |
45 apply (rule Quotient3I) |
45 apply (rule Quotient3I) |
46 apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2 |
46 apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2 |
47 Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2]) |
47 Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2]) |
48 using Quotient3_rel [OF q1] Quotient3_rel [OF q2] |
48 using Quotient3_rel [OF q1] Quotient3_rel [OF q2] |
49 apply (simp add: sum_rel_unfold comp_def split: sum.split) |
49 apply (simp add: sum_rel_def comp_def split: sum.split) |
50 done |
50 done |
51 |
51 |
52 declare [[mapQ3 sum = (sum_rel, sum_quotient)]] |
52 declare [[mapQ3 sum = (sum_rel, sum_quotient)]] |
53 |
53 |
54 lemma sum_Inl_rsp [quot_respect]: |
54 lemma sum_Inl_rsp [quot_respect]: |