16 | "option_rel R None (Some x) = False" |
16 | "option_rel R None (Some x) = False" |
17 | "option_rel R (Some x) (Some y) = R x y" |
17 | "option_rel R (Some x) (Some y) = R x y" |
18 |
18 |
19 declare [[map option = (Option.map, option_rel)]] |
19 declare [[map option = (Option.map, option_rel)]] |
20 |
20 |
21 text {* should probably be in Option.thy *} |
21 lemma option_rel_unfold: |
22 lemma split_option_all: |
22 "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True |
23 shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))" |
23 | (Some x, Some y) \<Rightarrow> R x y |
24 apply(auto) |
24 | _ \<Rightarrow> False)" |
25 apply(case_tac x) |
25 by (cases x) (cases y, simp_all)+ |
26 apply(simp_all) |
26 |
|
27 lemma option_rel_map1: |
|
28 "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y" |
|
29 by (simp add: option_rel_unfold split: option.split) |
|
30 |
|
31 lemma option_rel_map2: |
|
32 "option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y" |
|
33 by (simp add: option_rel_unfold split: option.split) |
|
34 |
|
35 lemma option_map_id [id_simps]: |
|
36 "Option.map id = id" |
|
37 by (simp add: id_def Option.map.identity fun_eq_iff) |
|
38 |
|
39 lemma option_rel_eq [id_simps]: |
|
40 "option_rel (op =) = (op =)" |
|
41 by (simp add: option_rel_unfold fun_eq_iff split: option.split) |
|
42 |
|
43 lemma option_reflp: |
|
44 "reflp R \<Longrightarrow> reflp (option_rel R)" |
|
45 by (auto simp add: option_rel_unfold split: option.splits intro!: reflpI elim: reflpE) |
|
46 |
|
47 lemma option_symp: |
|
48 "symp R \<Longrightarrow> symp (option_rel R)" |
|
49 by (auto simp add: option_rel_unfold split: option.splits intro!: sympI elim: sympE) |
|
50 |
|
51 lemma option_transp: |
|
52 "transp R \<Longrightarrow> transp (option_rel R)" |
|
53 by (auto simp add: option_rel_unfold split: option.splits intro!: transpI elim: transpE) |
|
54 |
|
55 lemma option_equivp [quot_equiv]: |
|
56 "equivp R \<Longrightarrow> equivp (option_rel R)" |
|
57 by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE) |
|
58 |
|
59 lemma option_quotient [quot_thm]: |
|
60 assumes "Quotient R Abs Rep" |
|
61 shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" |
|
62 apply (rule QuotientI) |
|
63 apply (simp_all add: Option.map.compositionality Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms]) |
|
64 using Quotient_rel [OF assms] |
|
65 apply (simp add: option_rel_unfold split: option.split) |
27 done |
66 done |
28 |
67 |
29 lemma option_quotient[quot_thm]: |
68 lemma option_None_rsp [quot_respect]: |
30 assumes q: "Quotient R Abs Rep" |
|
31 shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" |
|
32 unfolding Quotient_def |
|
33 apply(simp add: split_option_all) |
|
34 apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
|
35 using q |
|
36 unfolding Quotient_def |
|
37 apply(blast) |
|
38 done |
|
39 |
|
40 lemma option_equivp[quot_equiv]: |
|
41 assumes a: "equivp R" |
|
42 shows "equivp (option_rel R)" |
|
43 apply(rule equivpI) |
|
44 unfolding reflp_def symp_def transp_def |
|
45 apply(simp_all add: split_option_all) |
|
46 apply(blast intro: equivp_reflp[OF a]) |
|
47 apply(blast intro: equivp_symp[OF a]) |
|
48 apply(blast intro: equivp_transp[OF a]) |
|
49 done |
|
50 |
|
51 lemma option_None_rsp[quot_respect]: |
|
52 assumes q: "Quotient R Abs Rep" |
69 assumes q: "Quotient R Abs Rep" |
53 shows "option_rel R None None" |
70 shows "option_rel R None None" |
54 by simp |
71 by simp |
55 |
72 |
56 lemma option_Some_rsp[quot_respect]: |
73 lemma option_Some_rsp [quot_respect]: |
57 assumes q: "Quotient R Abs Rep" |
74 assumes q: "Quotient R Abs Rep" |
58 shows "(R ===> option_rel R) Some Some" |
75 shows "(R ===> option_rel R) Some Some" |
59 by auto |
76 by auto |
60 |
77 |
61 lemma option_None_prs[quot_preserve]: |
78 lemma option_None_prs [quot_preserve]: |
62 assumes q: "Quotient R Abs Rep" |
79 assumes q: "Quotient R Abs Rep" |
63 shows "Option.map Abs None = None" |
80 shows "Option.map Abs None = None" |
64 by simp |
81 by simp |
65 |
82 |
66 lemma option_Some_prs[quot_preserve]: |
83 lemma option_Some_prs [quot_preserve]: |
67 assumes q: "Quotient R Abs Rep" |
84 assumes q: "Quotient R Abs Rep" |
68 shows "(Rep ---> Option.map Abs) Some = Some" |
85 shows "(Rep ---> Option.map Abs) Some = Some" |
69 apply(simp add: fun_eq_iff) |
86 apply(simp add: fun_eq_iff) |
70 apply(simp add: Quotient_abs_rep[OF q]) |
87 apply(simp add: Quotient_abs_rep[OF q]) |
71 done |
88 done |
72 |
89 |
73 lemma option_map_id[id_simps]: |
|
74 shows "Option.map id = id" |
|
75 by (simp add: fun_eq_iff split_option_all) |
|
76 |
|
77 lemma option_rel_eq[id_simps]: |
|
78 shows "option_rel (op =) = (op =)" |
|
79 by (simp add: fun_eq_iff split_option_all) |
|
80 |
|
81 end |
90 end |