20 |
20 |
21 |
21 |
22 lemma option_quotient[quot_thm]: |
22 lemma option_quotient[quot_thm]: |
23 assumes q: "Quotient R Abs Rep" |
23 assumes q: "Quotient R Abs Rep" |
24 shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)" |
24 shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)" |
25 apply (unfold Quotient_def) |
25 apply(unfold Quotient_def) |
26 apply (rule conjI) |
26 apply(auto) |
27 apply (rule allI) |
27 apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
28 apply (case_tac a) |
28 apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
29 apply (simp_all add: Quotient_abs_rep[OF q]) |
29 apply(case_tac [!] r) |
30 apply (rule conjI) |
30 apply(case_tac [!] s) |
31 apply (rule allI) |
31 apply(simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q] ) |
32 apply (case_tac a) |
|
33 apply (simp_all add: Quotient_rel_rep[OF q]) |
|
34 apply (rule allI)+ |
|
35 apply (case_tac r) |
|
36 apply (case_tac s) |
|
37 apply (simp_all add: Quotient_abs_rep[OF q] add: Quotient_rel_rep[OF q]) |
|
38 apply (case_tac s) |
|
39 apply (simp_all add: Quotient_abs_rep[OF q] add: Quotient_rel_rep[OF q]) |
|
40 using q |
32 using q |
41 unfolding Quotient_def |
33 unfolding Quotient_def |
42 apply metis |
34 apply(blast)+ |
43 done |
35 done |
44 |
36 |
45 lemma option_rel_some: |
|
46 assumes e: "equivp R" |
|
47 and a: "option_rel R (Some a) = option_rel R (Some aa)" |
|
48 shows "R a aa" |
|
49 using a apply(drule_tac x="Some aa" in fun_cong) |
|
50 apply(simp add: equivp_reflp[OF e]) |
|
51 done |
|
52 |
|
53 lemma option_equivp[quot_equiv]: |
37 lemma option_equivp[quot_equiv]: |
54 assumes a: "equivp R" |
38 assumes a: "equivp R" |
55 shows "equivp (option_rel R)" |
39 shows "equivp (option_rel R)" |
56 unfolding equivp_def |
40 apply(rule equivpI) |
57 apply(rule allI)+ |
41 unfolding reflp_def symp_def transp_def |
58 apply(case_tac x) |
42 apply(auto) |
59 apply(case_tac y) |
43 apply(case_tac [!] x) |
|
44 apply(simp_all add: equivp_reflp[OF a]) |
|
45 apply(case_tac [!] y) |
|
46 apply(simp_all add: equivp_symp[OF a]) |
|
47 apply(case_tac [!] z) |
60 apply(simp_all) |
48 apply(simp_all) |
61 apply(unfold not_def) |
49 apply(clarify) |
62 apply(rule impI) |
|
63 apply(drule_tac x="None" in fun_cong) |
|
64 apply simp |
|
65 apply(case_tac y) |
|
66 apply(simp_all) |
|
67 apply(unfold not_def) |
|
68 apply(rule impI) |
|
69 apply(drule_tac x="None" in fun_cong) |
|
70 apply simp |
|
71 apply(rule iffI) |
|
72 apply(rule ext) |
|
73 apply(case_tac xa) |
|
74 apply(auto) |
|
75 apply(rule equivp_transp[OF a]) |
|
76 apply(rule equivp_symp[OF a]) |
|
77 apply(assumption)+ |
|
78 apply(rule equivp_transp[OF a]) |
50 apply(rule equivp_transp[OF a]) |
79 apply(assumption)+ |
51 apply(assumption)+ |
80 apply(simp only: option_rel_some[OF a]) |
|
81 done |
52 done |
82 |
53 |
83 lemma option_map_id[id_simps]: "option_map id \<equiv> id" |
54 lemma option_None_rsp[quot_respect]: |
|
55 assumes q: "Quotient R Abs Rep" |
|
56 shows "option_rel R None None" |
|
57 by simp |
|
58 |
|
59 lemma option_Some_rsp[quot_respect]: |
|
60 assumes q: "Quotient R Abs Rep" |
|
61 shows "(R ===> option_rel R) Some Some" |
|
62 by simp |
|
63 |
|
64 lemma option_None_prs[quot_preserve]: |
|
65 assumes q: "Quotient R Abs Rep" |
|
66 shows "option_map Abs None = None" |
|
67 by simp |
|
68 |
|
69 lemma option_Some_prs[quot_respect]: |
|
70 assumes q: "Quotient R Abs Rep" |
|
71 shows "(Rep ---> option_map Abs) Some = Some" |
|
72 apply(simp add: expand_fun_eq) |
|
73 apply(simp add: Quotient_abs_rep[OF q]) |
|
74 done |
|
75 |
|
76 lemma option_map_id[id_simps]: |
|
77 shows "option_map id \<equiv> id" |
84 apply (rule eq_reflection) |
78 apply (rule eq_reflection) |
85 apply (rule ext) |
79 apply (auto simp add: expand_fun_eq) |
86 apply (case_tac x) |
80 apply (case_tac x) |
87 apply (auto) |
81 apply (auto) |
88 done |
82 done |
89 |
83 |
90 lemma option_rel_eq[id_simps]: "option_rel op = \<equiv> op =" |
84 lemma option_rel_eq[id_simps]: |
91 apply (rule eq_reflection) |
85 shows "option_rel op = \<equiv> op =" |
92 apply (rule ext)+ |
86 apply(rule eq_reflection) |
93 apply (case_tac x) |
87 apply(auto simp add: expand_fun_eq) |
94 apply auto |
88 apply(case_tac x) |
95 apply (case_tac xa) |
89 apply(case_tac [!] xa) |
96 apply auto |
90 apply(auto) |
97 apply (case_tac xa) |
|
98 apply auto |
|
99 done |
91 done |
100 |
92 |
101 end |
93 end |