|
1 (* Title: HOL/Datatype.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
|
5 Author: Florian Haftmann, TU Muenchen |
|
6 *) |
|
7 |
|
8 header {* The option datatype *} |
|
9 |
|
10 theory Option |
|
11 imports Datatype |
|
12 begin |
|
13 |
|
14 subsection {* Type declaration *} |
|
15 |
|
16 datatype 'a option = None | Some 'a |
|
17 |
|
18 lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" |
|
19 by (induct x) auto |
|
20 |
|
21 lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)" |
|
22 by (induct x) auto |
|
23 |
|
24 text{*Although it may appear that both of these equalities are helpful |
|
25 only when applied to assumptions, in practice it seems better to give |
|
26 them the uniform iff attribute. *} |
|
27 |
|
28 lemma option_caseE: |
|
29 assumes c: "(case x of None => P | Some y => Q y)" |
|
30 obtains |
|
31 (None) "x = None" and P |
|
32 | (Some) y where "x = Some y" and "Q y" |
|
33 using c by (cases x) simp_all |
|
34 |
|
35 |
|
36 subsection {* Operations *} |
|
37 |
|
38 consts |
|
39 the :: "'a option => 'a" |
|
40 primrec |
|
41 "the (Some x) = x" |
|
42 |
|
43 consts |
|
44 o2s :: "'a option => 'a set" |
|
45 primrec |
|
46 "o2s None = {}" |
|
47 "o2s (Some x) = {x}" |
|
48 |
|
49 lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x" |
|
50 by simp |
|
51 |
|
52 ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *} |
|
53 |
|
54 lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)" |
|
55 by (cases xo) auto |
|
56 |
|
57 lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)" |
|
58 by (cases xo) auto |
|
59 |
|
60 |
|
61 constdefs |
|
62 option_map :: "('a => 'b) => ('a option => 'b option)" |
|
63 [code func del]: "option_map == %f y. case y of None => None | Some x => Some (f x)" |
|
64 |
|
65 lemma option_map_None [simp, code]: "option_map f None = None" |
|
66 by (simp add: option_map_def) |
|
67 |
|
68 lemma option_map_Some [simp, code]: "option_map f (Some x) = Some (f x)" |
|
69 by (simp add: option_map_def) |
|
70 |
|
71 lemma option_map_is_None [iff]: |
|
72 "(option_map f opt = None) = (opt = None)" |
|
73 by (simp add: option_map_def split add: option.split) |
|
74 |
|
75 lemma option_map_eq_Some [iff]: |
|
76 "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)" |
|
77 by (simp add: option_map_def split add: option.split) |
|
78 |
|
79 lemma option_map_comp: |
|
80 "option_map f (option_map g opt) = option_map (f o g) opt" |
|
81 by (simp add: option_map_def split add: option.split) |
|
82 |
|
83 lemma option_map_o_sum_case [simp]: |
|
84 "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)" |
|
85 by (rule ext) (simp split: sum.split) |
|
86 |
|
87 |
|
88 subsection {* Code generator setup *} |
|
89 |
|
90 definition |
|
91 is_none :: "'a option \<Rightarrow> bool" where |
|
92 is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None" |
|
93 |
|
94 lemma is_none_code [code]: |
|
95 shows "is_none None \<longleftrightarrow> True" |
|
96 and "is_none (Some x) \<longleftrightarrow> False" |
|
97 unfolding is_none_none [symmetric] by simp_all |
|
98 |
|
99 hide (open) const is_none |
|
100 |
|
101 code_type option |
|
102 (SML "_ option") |
|
103 (OCaml "_ option") |
|
104 (Haskell "Maybe _") |
|
105 |
|
106 code_const None and Some |
|
107 (SML "NONE" and "SOME") |
|
108 (OCaml "None" and "Some _") |
|
109 (Haskell "Nothing" and "Just") |
|
110 |
|
111 code_instance option :: eq |
|
112 (Haskell -) |
|
113 |
|
114 code_const "op = \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool" |
|
115 (Haskell infixl 4 "==") |
|
116 |
|
117 code_reserved SML |
|
118 option NONE SOME |
|
119 |
|
120 code_reserved OCaml |
|
121 option None Some |
|
122 |
|
123 end |