53 lemma option_equivp [quot_equiv]: |
53 lemma option_equivp [quot_equiv]: |
54 "equivp R \<Longrightarrow> equivp (option_rel R)" |
54 "equivp R \<Longrightarrow> equivp (option_rel R)" |
55 by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE) |
55 by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE) |
56 |
56 |
57 lemma option_quotient [quot_thm]: |
57 lemma option_quotient [quot_thm]: |
58 assumes "Quotient R Abs Rep" |
58 assumes "Quotient3 R Abs Rep" |
59 shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" |
59 shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)" |
60 apply (rule QuotientI) |
60 apply (rule Quotient3I) |
61 apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms]) |
61 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]) |
62 using Quotient_rel [OF assms] |
62 using Quotient3_rel [OF assms] |
63 apply (simp add: option_rel_unfold split: option.split) |
63 apply (simp add: option_rel_unfold split: option.split) |
64 done |
64 done |
65 |
65 |
66 declare [[map option = (option_rel, option_quotient)]] |
66 declare [[mapQ3 option = (option_rel, option_quotient)]] |
67 |
67 |
68 lemma option_None_rsp [quot_respect]: |
68 lemma option_None_rsp [quot_respect]: |
69 assumes q: "Quotient R Abs Rep" |
69 assumes q: "Quotient3 R Abs Rep" |
70 shows "option_rel R None None" |
70 shows "option_rel R None None" |
71 by simp |
71 by simp |
72 |
72 |
73 lemma option_Some_rsp [quot_respect]: |
73 lemma option_Some_rsp [quot_respect]: |
74 assumes q: "Quotient R Abs Rep" |
74 assumes q: "Quotient3 R Abs Rep" |
75 shows "(R ===> option_rel R) Some Some" |
75 shows "(R ===> option_rel R) Some Some" |
76 by auto |
76 by auto |
77 |
77 |
78 lemma option_None_prs [quot_preserve]: |
78 lemma option_None_prs [quot_preserve]: |
79 assumes q: "Quotient R Abs Rep" |
79 assumes q: "Quotient3 R Abs Rep" |
80 shows "Option.map Abs None = None" |
80 shows "Option.map Abs None = None" |
81 by simp |
81 by simp |
82 |
82 |
83 lemma option_Some_prs [quot_preserve]: |
83 lemma option_Some_prs [quot_preserve]: |
84 assumes q: "Quotient R Abs Rep" |
84 assumes q: "Quotient3 R Abs Rep" |
85 shows "(Rep ---> Option.map Abs) Some = Some" |
85 shows "(Rep ---> Option.map Abs) Some = Some" |
86 apply(simp add: fun_eq_iff) |
86 apply(simp add: fun_eq_iff) |
87 apply(simp add: Quotient_abs_rep[OF q]) |
87 apply(simp add: Quotient3_abs_rep[OF q]) |
88 done |
88 done |
89 |
89 |
90 end |
90 end |