author  wenzelm 
Mon, 06 Sep 2010 19:13:10 +0200  
changeset 39159  0dec18004e75 
parent 39150  c4ff5fd8db99 
child 39272  0b61951d2682 
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 

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

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

30246  87 

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

90 

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

92 
by (cases x) auto 

93 

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

95 
by (cases x) auto 

96 

97 
hide_const (open) set map bind 

30246  98 

99 
subsubsection {* Code generator setup *} 

100 

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

102 
[code_post]: "is_none x \<longleftrightarrow> x = None" 
30246  103 

104 
lemma is_none_code [code]: 

105 
shows "is_none None \<longleftrightarrow> True" 

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

31154  107 
unfolding is_none_def by simp_all 
108 

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

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

110 
"HOL.equal x None \<longleftrightarrow> is_none x" 
39150  111 
by (simp add: equal is_none_def) 
30246  112 

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

113 
hide_const (open) is_none 
30246  114 

115 
code_type option 

116 
(SML "_ option") 

117 
(OCaml "_ option") 

118 
(Haskell "Maybe _") 

34886  119 
(Scala "!Option[(_)]") 
30246  120 

121 
code_const None and Some 

122 
(SML "NONE" and "SOME") 

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

124 
(Haskell "Nothing" and "Just") 

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

125 
(Scala "!None" and "Some") 
30246  126 

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

127 
code_instance option :: equal 
30246  128 
(Haskell ) 
129 

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

130 
code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool" 
30246  131 
(Haskell infixl 4 "==") 
132 

133 
code_reserved SML 

134 
option NONE SOME 

135 

136 
code_reserved OCaml 

137 
option None Some 

138 

34886  139 
code_reserved Scala 
140 
Option None Some 

141 

30246  142 
end 