30246

1 
(* Title: HOL/Option.thy


2 
Author: Folklore


3 
*)


4 


5 
header {* Datatype option *}


6 


7 
theory Option


8 
imports Datatype


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 


23 
lemma option_caseE:


24 
assumes c: "(case x of None => P  Some y => Q y)"


25 
obtains


26 
(None) "x = None" and P


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


28 
using c by (cases x) simp_all


29 


30 
lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"


31 
by (rule set_ext, case_tac x) auto


32 


33 
lemma inj_Some [simp]: "inj_on Some A"


34 
by (rule inj_onI) simp


35 


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 _ =>


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


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 


59 
definition


60 
map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"


61 
where


62 
[code del]: "map = (%f y. case y of None => None  Some x => Some (f x))"


63 


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


65 
by (simp add: map_def)


66 


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


68 
by (simp add: map_def)


69 


70 
lemma option_map_is_None [iff]:


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


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


73 


74 
lemma option_map_eq_Some [iff]:


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


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


77 


78 
lemma option_map_comp:


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


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


81 


82 
lemma option_map_o_sum_case [simp]:


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


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


85 


86 


87 
hide (open) const set map


88 


89 
subsubsection {* Code generator setup *}


90 


91 
definition


92 
is_none :: "'a option \<Rightarrow> bool" where


93 
is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"


94 


95 
lemma is_none_code [code]:


96 
shows "is_none None \<longleftrightarrow> True"


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


98 
unfolding is_none_none [symmetric] by simp_all


99 


100 
hide (open) const is_none


101 


102 
code_type option


103 
(SML "_ option")


104 
(OCaml "_ option")


105 
(Haskell "Maybe _")


106 


107 
code_const None and Some


108 
(SML "NONE" and "SOME")


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


110 
(Haskell "Nothing" and "Just")


111 


112 
code_instance option :: eq


113 
(Haskell )


114 


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


116 
(Haskell infixl 4 "==")


117 


118 
code_reserved SML


119 
option NONE SOME


120 


121 
code_reserved OCaml


122 
option None Some


123 


124 
end
