1128
|
1 |
(* Title: Quotient_Option.thy
|
932
|
2 |
Author: Cezary Kaliszyk and Christian Urban
|
|
3 |
*)
|
1128
|
4 |
theory Quotient_Option
|
1129
|
5 |
imports Quotient Quotient_Syntax
|
698
|
6 |
begin
|
|
7 |
|
937
|
8 |
section {* Quotient infrastructure for the option type. *}
|
932
|
9 |
|
698
|
10 |
fun
|
|
11 |
option_rel
|
|
12 |
where
|
|
13 |
"option_rel R None None = True"
|
|
14 |
| "option_rel R (Some x) None = False"
|
|
15 |
| "option_rel R None (Some x) = False"
|
|
16 |
| "option_rel R (Some x) (Some y) = R x y"
|
|
17 |
|
932
|
18 |
declare [[map option = (Option.map, option_rel)]]
|
698
|
19 |
|
933
|
20 |
text {* should probably be in Option.thy *}
|
1128
|
21 |
lemma split_option_all:
|
933
|
22 |
shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"
|
937
|
23 |
apply(auto)
|
|
24 |
apply(case_tac x)
|
|
25 |
apply(simp_all)
|
|
26 |
done
|
698
|
27 |
|
|
28 |
lemma option_quotient[quot_thm]:
|
|
29 |
assumes q: "Quotient R Abs Rep"
|
932
|
30 |
shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
|
|
31 |
unfolding Quotient_def
|
933
|
32 |
apply(simp add: split_option_all)
|
|
33 |
apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
|
698
|
34 |
using q
|
|
35 |
unfolding Quotient_def
|
933
|
36 |
apply(blast)
|
923
|
37 |
done
|
1128
|
38 |
|
698
|
39 |
lemma option_equivp[quot_equiv]:
|
|
40 |
assumes a: "equivp R"
|
|
41 |
shows "equivp (option_rel R)"
|
923
|
42 |
apply(rule equivpI)
|
|
43 |
unfolding reflp_def symp_def transp_def
|
933
|
44 |
apply(simp_all add: split_option_all)
|
|
45 |
apply(blast intro: equivp_reflp[OF a])
|
|
46 |
apply(blast intro: equivp_symp[OF a])
|
|
47 |
apply(blast intro: equivp_transp[OF a])
|
698
|
48 |
done
|
|
49 |
|
923
|
50 |
lemma option_None_rsp[quot_respect]:
|
|
51 |
assumes q: "Quotient R Abs Rep"
|
|
52 |
shows "option_rel R None None"
|
|
53 |
by simp
|
|
54 |
|
|
55 |
lemma option_Some_rsp[quot_respect]:
|
|
56 |
assumes q: "Quotient R Abs Rep"
|
|
57 |
shows "(R ===> option_rel R) Some Some"
|
|
58 |
by simp
|
|
59 |
|
|
60 |
lemma option_None_prs[quot_preserve]:
|
|
61 |
assumes q: "Quotient R Abs Rep"
|
932
|
62 |
shows "Option.map Abs None = None"
|
923
|
63 |
by simp
|
|
64 |
|
1122
|
65 |
lemma option_Some_prs[quot_preserve]:
|
923
|
66 |
assumes q: "Quotient R Abs Rep"
|
932
|
67 |
shows "(Rep ---> Option.map Abs) Some = Some"
|
923
|
68 |
apply(simp add: expand_fun_eq)
|
|
69 |
apply(simp add: Quotient_abs_rep[OF q])
|
|
70 |
done
|
|
71 |
|
1128
|
72 |
lemma option_map_id[id_simps]:
|
936
|
73 |
shows "Option.map id = id"
|
933
|
74 |
by (simp add: expand_fun_eq split_option_all)
|
829
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
75 |
|
1128
|
76 |
lemma option_rel_eq[id_simps]:
|
927
|
77 |
shows "option_rel (op =) = (op =)"
|
933
|
78 |
by (simp add: expand_fun_eq split_option_all)
|
829
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
79 |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
80 |
end
|