author  haftmann 
Tue, 14 Jul 2009 10:54:04 +0200  
changeset 31998  2c7a24f74db9 
parent 31154  f919b8e67413 
child 32069  6d28bbd33e2c 
permissions  rwrr 
30246  1 
(* Title: HOL/Option.thy 
2 
Author: Folklore 

3 
*) 

4 

5 
header {* Datatype option *} 

6 

7 
theory Option 

30327  8 
imports Datatype Finite_Set 
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 

36 
lemma finite_option_UNIV[simp]: 

37 
"finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)" 

38 
by(auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some) 

30246  39 

30327  40 
instance option :: (finite) finite proof 
31080  41 
qed (simp add: UNIV_option_conv) 
30246  42 

43 

44 
subsubsection {* Operations *} 

45 

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

47 
"the (Some x) = x" 

48 

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

50 
"set None = {}"  

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

52 

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

54 
by simp 

55 

56 
declaration {* fn _ => 

57 
Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec")) 

58 
*} 

59 

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

61 
by (cases xo) auto 

62 

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

64 
by (cases xo) auto 

65 

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

30246  68 

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

70 
by (simp add: map_def) 

71 

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

73 
by (simp add: map_def) 

74 

75 
lemma option_map_is_None [iff]: 

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

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

78 

79 
lemma option_map_eq_Some [iff]: 

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

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

82 

83 
lemma option_map_comp: 

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

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

86 

87 
lemma option_map_o_sum_case [simp]: 

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

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

90 

91 

92 
hide (open) const set map 

93 

94 
subsubsection {* Code generator setup *} 

95 

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

97 
[code_post]: "is_none x \<longleftrightarrow> x = None" 
30246  98 

99 
lemma is_none_code [code]: 

100 
shows "is_none None \<longleftrightarrow> True" 

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

31154  102 
unfolding is_none_def by simp_all 
103 

104 
lemma is_none_none: 

105 
"is_none x \<longleftrightarrow> x = None" 

106 
by (simp add: is_none_def) 

107 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31154
diff
changeset

108 
lemma [code_inline]: 
31154  109 
"eq_class.eq x None \<longleftrightarrow> is_none x" 
110 
by (simp add: eq is_none_none) 

30246  111 

112 
hide (open) const is_none 

113 

114 
code_type option 

115 
(SML "_ option") 

116 
(OCaml "_ option") 

117 
(Haskell "Maybe _") 

118 

119 
code_const None and Some 

120 
(SML "NONE" and "SOME") 

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

122 
(Haskell "Nothing" and "Just") 

123 

124 
code_instance option :: eq 

125 
(Haskell ) 

126 

127 
code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool" 

128 
(Haskell infixl 4 "==") 

129 

130 
code_reserved SML 

131 
option NONE SOME 

132 

133 
code_reserved OCaml 

134 
option None Some 

135 

136 
end 