equal
deleted
inserted
replaced
9 begin |
9 begin |
10 |
10 |
11 subsection {* Rules for the Quotient package *} |
11 subsection {* Rules for the Quotient package *} |
12 |
12 |
13 lemma option_rel_map1: |
13 lemma option_rel_map1: |
14 "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y" |
14 "option_rel R (map_option f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y" |
15 by (simp add: option_rel_def split: option.split) |
15 by (simp add: option_rel_def split: option.split) |
16 |
16 |
17 lemma option_rel_map2: |
17 lemma option_rel_map2: |
18 "option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y" |
18 "option_rel R x (map_option f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y" |
19 by (simp add: option_rel_def split: option.split) |
19 by (simp add: option_rel_def split: option.split) |
20 |
20 |
21 lemma option_map_id [id_simps]: |
21 declare |
22 "Option.map id = id" |
22 map_option.id [id_simps] |
23 by (simp add: id_def Option.map.identity fun_eq_iff) |
23 option_rel_eq [id_simps] |
24 |
|
25 lemma option_rel_eq [id_simps]: |
|
26 "option_rel (op =) = (op =)" |
|
27 by (simp add: option_rel_def fun_eq_iff split: option.split) |
|
28 |
24 |
29 lemma option_symp: |
25 lemma option_symp: |
30 "symp R \<Longrightarrow> symp (option_rel R)" |
26 "symp R \<Longrightarrow> symp (option_rel R)" |
31 unfolding symp_def split_option_all option_rel_simps by fast |
27 unfolding symp_def split_option_all option_rel_simps by fast |
32 |
28 |
38 "equivp R \<Longrightarrow> equivp (option_rel R)" |
34 "equivp R \<Longrightarrow> equivp (option_rel R)" |
39 by (blast intro: equivpI reflp_option_rel option_symp option_transp elim: equivpE) |
35 by (blast intro: equivpI reflp_option_rel option_symp option_transp elim: equivpE) |
40 |
36 |
41 lemma option_quotient [quot_thm]: |
37 lemma option_quotient [quot_thm]: |
42 assumes "Quotient3 R Abs Rep" |
38 assumes "Quotient3 R Abs Rep" |
43 shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)" |
39 shows "Quotient3 (option_rel R) (map_option Abs) (map_option Rep)" |
44 apply (rule Quotient3I) |
40 apply (rule Quotient3I) |
45 apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms]) |
41 apply (simp_all add: option.map_comp comp_def option.map_id[unfolded id_def] option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms]) |
46 using Quotient3_rel [OF assms] |
42 using Quotient3_rel [OF assms] |
47 apply (simp add: option_rel_def split: option.split) |
43 apply (simp add: option_rel_def split: option.split) |
48 done |
44 done |
49 |
45 |
50 declare [[mapQ3 option = (option_rel, option_quotient)]] |
46 declare [[mapQ3 option = (option_rel, option_quotient)]] |
59 shows "(R ===> option_rel R) Some Some" |
55 shows "(R ===> option_rel R) Some Some" |
60 by (rule Some_transfer) |
56 by (rule Some_transfer) |
61 |
57 |
62 lemma option_None_prs [quot_preserve]: |
58 lemma option_None_prs [quot_preserve]: |
63 assumes q: "Quotient3 R Abs Rep" |
59 assumes q: "Quotient3 R Abs Rep" |
64 shows "Option.map Abs None = None" |
60 shows "map_option Abs None = None" |
65 by simp |
61 by simp |
66 |
62 |
67 lemma option_Some_prs [quot_preserve]: |
63 lemma option_Some_prs [quot_preserve]: |
68 assumes q: "Quotient3 R Abs Rep" |
64 assumes q: "Quotient3 R Abs Rep" |
69 shows "(Rep ---> Option.map Abs) Some = Some" |
65 shows "(Rep ---> map_option Abs) Some = Some" |
70 apply(simp add: fun_eq_iff) |
66 apply(simp add: fun_eq_iff) |
71 apply(simp add: Quotient3_abs_rep[OF q]) |
67 apply(simp add: Quotient3_abs_rep[OF q]) |
72 done |
68 done |
73 |
69 |
74 end |
70 end |