author  haftmann 
Tue, 11 Jan 2011 14:12:37 +0100  
changeset 41505  6d19301074cf 
parent 41372  551eb49a6e91 
child 46526  c4cf9d03c352 
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 

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

84 
enriched_type map: Option.map proof  
41372  85 
fix f g 
86 
show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)" 

87 
proof 

88 
fix x 

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

90 
by (cases x) simp_all 

91 
qed 

40609  92 
next 
41372  93 
show "Option.map id = id" 
94 
proof 

95 
fix x 

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

97 
by (cases x) simp_all 

98 
qed 

40609  99 
qed 
100 

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

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

30246  104 

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

107 

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

109 
by (cases x) auto 

110 

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

112 
by (cases x) auto 

113 

114 
hide_const (open) set map bind 

30246  115 

116 
subsubsection {* Code generator setup *} 

117 

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

119 
[code_post]: "is_none x \<longleftrightarrow> x = None" 
30246  120 

121 
lemma is_none_code [code]: 

122 
shows "is_none None \<longleftrightarrow> True" 

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

31154  124 
unfolding is_none_def by simp_all 
125 

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

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

127 
"HOL.equal x None \<longleftrightarrow> is_none x" 
39150  128 
by (simp add: equal is_none_def) 
30246  129 

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

130 
hide_const (open) is_none 
30246  131 

132 
code_type option 

133 
(SML "_ option") 

134 
(OCaml "_ option") 

135 
(Haskell "Maybe _") 

34886  136 
(Scala "!Option[(_)]") 
30246  137 

138 
code_const None and Some 

139 
(SML "NONE" and "SOME") 

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

141 
(Haskell "Nothing" and "Just") 

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

142 
(Scala "!None" and "Some") 
30246  143 

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

144 
code_instance option :: equal 
30246  145 
(Haskell ) 
146 

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

147 
code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool" 
39272  148 
(Haskell infix 4 "==") 
30246  149 

150 
code_reserved SML 

151 
option NONE SOME 

152 

153 
code_reserved OCaml 

154 
option None Some 

155 

34886  156 
code_reserved Scala 
157 
Option None Some 

158 

30246  159 
end 