15 | "option_rel R None (Some x) = False" |
15 | "option_rel R None (Some x) = False" |
16 | "option_rel R (Some x) (Some y) = R x y" |
16 | "option_rel R (Some x) (Some y) = R x y" |
17 |
17 |
18 declare [[map option = (Option.map, option_rel)]] |
18 declare [[map option = (Option.map, option_rel)]] |
19 |
19 |
|
20 text {* should probably be in Option.thy *} |
|
21 lemma split_option_all: |
|
22 shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))" |
|
23 apply(auto) |
|
24 apply(case_tac x) |
|
25 apply(simp_all) |
|
26 done |
|
27 |
20 lemma option_quotient[quot_thm]: |
28 lemma option_quotient[quot_thm]: |
21 assumes q: "Quotient R Abs Rep" |
29 assumes q: "Quotient R Abs Rep" |
22 shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" |
30 shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" |
23 unfolding Quotient_def |
31 unfolding Quotient_def |
24 apply(auto) |
32 apply(simp add: split_option_all) |
25 apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
33 apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
26 apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
|
27 apply(case_tac [!] r) |
|
28 apply(case_tac [!] s) |
|
29 apply(simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q] ) |
|
30 using q |
34 using q |
31 unfolding Quotient_def |
35 unfolding Quotient_def |
32 apply(blast)+ |
36 apply(blast) |
33 done |
37 done |
34 |
38 |
35 lemma option_equivp[quot_equiv]: |
39 lemma option_equivp[quot_equiv]: |
36 assumes a: "equivp R" |
40 assumes a: "equivp R" |
37 shows "equivp (option_rel R)" |
41 shows "equivp (option_rel R)" |
38 apply(rule equivpI) |
42 apply(rule equivpI) |
39 unfolding reflp_def symp_def transp_def |
43 unfolding reflp_def symp_def transp_def |
40 apply(auto) |
44 apply(simp_all add: split_option_all) |
41 apply(case_tac [!] x) |
45 apply(blast intro: equivp_reflp[OF a]) |
42 apply(simp_all add: equivp_reflp[OF a]) |
46 apply(blast intro: equivp_symp[OF a]) |
43 apply(case_tac [!] y) |
47 apply(blast intro: equivp_transp[OF a]) |
44 apply(simp_all add: equivp_symp[OF a]) |
|
45 apply(case_tac [!] z) |
|
46 apply(simp_all) |
|
47 apply(clarify) |
|
48 apply(rule equivp_transp[OF a]) |
|
49 apply(assumption)+ |
|
50 done |
48 done |
51 |
49 |
52 lemma option_None_rsp[quot_respect]: |
50 lemma option_None_rsp[quot_respect]: |
53 assumes q: "Quotient R Abs Rep" |
51 assumes q: "Quotient R Abs Rep" |
54 shows "option_rel R None None" |
52 shows "option_rel R None None" |
72 done |
70 done |
73 |
71 |
74 lemma option_map_id[id_simps]: |
72 lemma option_map_id[id_simps]: |
75 shows "Option.map id \<equiv> id" |
73 shows "Option.map id \<equiv> id" |
76 apply (rule eq_reflection) |
74 apply (rule eq_reflection) |
77 apply (auto simp add: expand_fun_eq) |
75 by (simp add: expand_fun_eq split_option_all) |
78 apply (case_tac x) |
|
79 apply (auto) |
|
80 done |
|
81 |
76 |
82 lemma option_rel_eq[id_simps]: |
77 lemma option_rel_eq[id_simps]: |
83 shows "option_rel (op =) \<equiv> (op =)" |
78 shows "option_rel (op =) \<equiv> (op =)" |
84 apply(rule eq_reflection) |
79 apply(rule eq_reflection) |
85 apply(auto simp add: expand_fun_eq) |
80 by (simp add: expand_fun_eq split_option_all) |
86 apply(case_tac x) |
|
87 apply(case_tac [!] xa) |
|
88 apply(auto) |
|
89 done |
|
90 |
81 |
91 end |
82 end |