author  haftmann 
Fri, 07 Sep 2012 08:20:18 +0200  
changeset 49189  3f85cd15a0cc 
parent 46526  c4cf9d03c352 
child 51096  60e4b75fefe1 
permissions  rwrr 
30246  1 
(* Title: HOL/Option.thy 
2 
Author: Folklore 

3 
*) 

4 

5 
header {* Datatype option *} 

6 

7 
theory Option 

35719
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
34886
diff
changeset

8 
imports Datatype 
30246  9 
begin 
10 

11 
datatype 'a option = None  Some 'a 

12 

13 
lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" 

14 
by (induct x) auto 

15 

16 
lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)" 

17 
by (induct x) auto 

18 

19 
text{*Although it may appear that both of these equalities are helpful 

20 
only when applied to assumptions, in practice it seems better to give 

21 
them the uniform iff attribute. *} 

22 

31080  23 
lemma inj_Some [simp]: "inj_on Some A" 
24 
by (rule inj_onI) simp 

25 

30246  26 
lemma option_caseE: 
27 
assumes c: "(case x of None => P  Some y => Q y)" 

28 
obtains 

29 
(None) "x = None" and P 

30 
 (Some) y where "x = Some y" and "Q y" 

31 
using c by (cases x) simp_all 

32 

31080  33 
lemma UNIV_option_conv: "UNIV = insert None (range Some)" 
34 
by(auto intro: classical) 

35 

30246  36 

37 
subsubsection {* Operations *} 

38 

39 
primrec the :: "'a option => 'a" where 

40 
"the (Some x) = x" 

41 

42 
primrec set :: "'a option => 'a set" where 

43 
"set None = {}"  

44 
"set (Some x) = {x}" 

45 

46 
lemma ospec [dest]: "(ALL x:set A. P x) ==> A = Some x ==> P x" 

47 
by simp 

48 

49 
declaration {* fn _ => 

39159  50 
Classical.map_cs (fn cs => cs addSD2 ("ospec", @{thm ospec})) 
30246  51 
*} 
52 

53 
lemma elem_set [iff]: "(x : set xo) = (xo = Some x)" 

54 
by (cases xo) auto 

55 

56 
lemma set_empty_eq [simp]: "(set xo = {}) = (xo = None)" 

57 
by (cases xo) auto 

58 

31154  59 
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option" where 
60 
"map = (%f y. case y of None => None  Some x => Some (f x))" 

30246  61 

62 
lemma option_map_None [simp, code]: "map f None = None" 

63 
by (simp add: map_def) 

64 

65 
lemma option_map_Some [simp, code]: "map f (Some x) = Some (f x)" 

66 
by (simp add: map_def) 

67 

68 
lemma option_map_is_None [iff]: 

69 
"(map f opt = None) = (opt = None)" 

70 
by (simp add: map_def split add: option.split) 

71 

72 
lemma option_map_eq_Some [iff]: 

73 
"(map f xo = Some y) = (EX z. xo = Some z & f z = y)" 

74 
by (simp add: map_def split add: option.split) 

75 

76 
lemma option_map_comp: 

77 
"map f (map g opt) = map (f o g) opt" 

78 
by (simp add: map_def split add: option.split) 

79 

80 
lemma option_map_o_sum_case [simp]: 

81 
"map f o sum_case g h = sum_case (map f o g) (map f o h)" 

82 
by (rule ext) (simp split: sum.split) 

83 

46526  84 
lemma map_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map f x = map g y" 
85 
by (cases x) auto 

86 

41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41372
diff
changeset

87 
enriched_type map: Option.map proof  
41372  88 
fix f g 
89 
show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)" 

90 
proof 

91 
fix x 

92 
show "(Option.map f \<circ> Option.map g) x= Option.map (f \<circ> g) x" 

93 
by (cases x) simp_all 

94 
qed 

40609  95 
next 
41372  96 
show "Option.map id = id" 
97 
proof 

98 
fix x 

99 
show "Option.map id x = id x" 

100 
by (cases x) simp_all 

101 
qed 

40609  102 
qed 
103 

39149  104 
primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where 
105 
bind_lzero: "bind None f = None"  

106 
bind_lunit: "bind (Some x) f = f x" 

30246  107 

39149  108 
lemma bind_runit[simp]: "bind x Some = x" 
109 
by (cases x) auto 

110 

111 
lemma bind_assoc[simp]: "bind (bind x f) g = bind x (\<lambda>y. bind (f y) g)" 

112 
by (cases x) auto 

113 

114 
lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None" 

115 
by (cases x) auto 

116 

46526  117 
lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g" 
118 
by (cases x) auto 

119 

49189  120 
definition these :: "'a option set \<Rightarrow> 'a set" 
121 
where 

122 
"these A = the ` {x \<in> A. x \<noteq> None}" 

123 

124 
lemma these_empty [simp]: 

125 
"these {} = {}" 

126 
by (simp add: these_def) 

127 

128 
lemma these_insert_None [simp]: 

129 
"these (insert None A) = these A" 

130 
by (auto simp add: these_def) 

131 

132 
lemma these_insert_Some [simp]: 

133 
"these (insert (Some x) A) = insert x (these A)" 

134 
proof  

135 
have "{y \<in> insert (Some x) A. y \<noteq> None} = insert (Some x) {y \<in> A. y \<noteq> None}" 

136 
by auto 

137 
then show ?thesis by (simp add: these_def) 

138 
qed 

139 

140 
lemma in_these_eq: 

141 
"x \<in> these A \<longleftrightarrow> Some x \<in> A" 

142 
proof 

143 
assume "Some x \<in> A" 

144 
then obtain B where "A = insert (Some x) B" by auto 

145 
then show "x \<in> these A" by (auto simp add: these_def intro!: image_eqI) 

146 
next 

147 
assume "x \<in> these A" 

148 
then show "Some x \<in> A" by (auto simp add: these_def) 

149 
qed 

150 

151 
lemma these_image_Some_eq [simp]: 

152 
"these (Some ` A) = A" 

153 
by (auto simp add: these_def intro!: image_eqI) 

154 

155 
lemma Some_image_these_eq: 

156 
"Some ` these A = {x\<in>A. x \<noteq> None}" 

157 
by (auto simp add: these_def image_image intro!: image_eqI) 

158 

159 
lemma these_empty_eq: 

160 
"these B = {} \<longleftrightarrow> B = {} \<or> B = {None}" 

161 
by (auto simp add: these_def) 

162 

163 
lemma these_not_empty_eq: 

164 
"these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}" 

165 
by (auto simp add: these_empty_eq) 

166 

167 
hide_const (open) set map bind these 

46526  168 
hide_fact (open) map_cong bind_cong 
30246  169 

49189  170 

30246  171 
subsubsection {* Code generator setup *} 
172 

31154  173 
definition is_none :: "'a option \<Rightarrow> bool" where 
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31154
diff
changeset

174 
[code_post]: "is_none x \<longleftrightarrow> x = None" 
30246  175 

176 
lemma is_none_code [code]: 

177 
shows "is_none None \<longleftrightarrow> True" 

178 
and "is_none (Some x) \<longleftrightarrow> False" 

31154  179 
unfolding is_none_def by simp_all 
180 

32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

181 
lemma [code_unfold]: 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37880
diff
changeset

182 
"HOL.equal x None \<longleftrightarrow> is_none x" 
39150  183 
by (simp add: equal is_none_def) 
30246  184 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35719
diff
changeset

185 
hide_const (open) is_none 
30246  186 

187 
code_type option 

188 
(SML "_ option") 

189 
(OCaml "_ option") 

190 
(Haskell "Maybe _") 

34886  191 
(Scala "!Option[(_)]") 
30246  192 

193 
code_const None and Some 

194 
(SML "NONE" and "SOME") 

195 
(OCaml "None" and "Some _") 

196 
(Haskell "Nothing" and "Just") 

37880
3b9ca8d2c5fb
Scala: subtle difference in printing strings vs. complex mixfix syntax
haftmann
parents:
36176
diff
changeset

197 
(Scala "!None" and "Some") 
30246  198 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37880
diff
changeset

199 
code_instance option :: equal 
30246  200 
(Haskell ) 
201 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37880
diff
changeset

202 
code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool" 
39272  203 
(Haskell infix 4 "==") 
30246  204 

205 
code_reserved SML 

206 
option NONE SOME 

207 

208 
code_reserved OCaml 

209 
option None Some 

210 

34886  211 
code_reserved Scala 
212 
Option None Some 

213 

30246  214 
end 
49189  215 