nipkow@30246: (* Title: HOL/Option.thy nipkow@30246: Author: Folklore nipkow@30246: *) nipkow@30246: nipkow@30246: header {* Datatype option *} nipkow@30246: nipkow@30246: theory Option haftmann@35719: imports Datatype nipkow@30246: begin nipkow@30246: nipkow@30246: datatype 'a option = None | Some 'a nipkow@30246: nipkow@30246: lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" nipkow@30246: by (induct x) auto nipkow@30246: nipkow@30246: lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)" nipkow@30246: by (induct x) auto nipkow@30246: nipkow@30246: text{*Although it may appear that both of these equalities are helpful nipkow@30246: only when applied to assumptions, in practice it seems better to give nipkow@30246: them the uniform iff attribute. *} nipkow@30246: nipkow@31080: lemma inj_Some [simp]: "inj_on Some A" nipkow@31080: by (rule inj_onI) simp nipkow@31080: nipkow@30246: lemma option_caseE: nipkow@30246: assumes c: "(case x of None => P | Some y => Q y)" nipkow@30246: obtains nipkow@30246: (None) "x = None" and P nipkow@30246: | (Some) y where "x = Some y" and "Q y" nipkow@30246: using c by (cases x) simp_all nipkow@30246: nipkow@31080: lemma UNIV_option_conv: "UNIV = insert None (range Some)" nipkow@31080: by(auto intro: classical) nipkow@31080: nipkow@30246: nipkow@30246: subsubsection {* Operations *} nipkow@30246: nipkow@30246: primrec the :: "'a option => 'a" where nipkow@30246: "the (Some x) = x" nipkow@30246: nipkow@30246: primrec set :: "'a option => 'a set" where nipkow@30246: "set None = {}" | nipkow@30246: "set (Some x) = {x}" nipkow@30246: nipkow@30246: lemma ospec [dest]: "(ALL x:set A. P x) ==> A = Some x ==> P x" nipkow@30246: by simp nipkow@30246: nipkow@30246: declaration {* fn _ => wenzelm@39159: Classical.map_cs (fn cs => cs addSD2 ("ospec", @{thm ospec})) nipkow@30246: *} nipkow@30246: nipkow@30246: lemma elem_set [iff]: "(x : set xo) = (xo = Some x)" nipkow@30246: by (cases xo) auto nipkow@30246: nipkow@30246: lemma set_empty_eq [simp]: "(set xo = {}) = (xo = None)" nipkow@30246: by (cases xo) auto nipkow@30246: haftmann@31154: definition map :: "('a \ 'b) \ 'a option \ 'b option" where haftmann@31154: "map = (%f y. case y of None => None | Some x => Some (f x))" nipkow@30246: nipkow@30246: lemma option_map_None [simp, code]: "map f None = None" nipkow@30246: by (simp add: map_def) nipkow@30246: nipkow@30246: lemma option_map_Some [simp, code]: "map f (Some x) = Some (f x)" nipkow@30246: by (simp add: map_def) nipkow@30246: nipkow@30246: lemma option_map_is_None [iff]: nipkow@30246: "(map f opt = None) = (opt = None)" nipkow@30246: by (simp add: map_def split add: option.split) nipkow@30246: nipkow@30246: lemma option_map_eq_Some [iff]: nipkow@30246: "(map f xo = Some y) = (EX z. xo = Some z & f z = y)" nipkow@30246: by (simp add: map_def split add: option.split) nipkow@30246: nipkow@30246: lemma option_map_comp: nipkow@30246: "map f (map g opt) = map (f o g) opt" nipkow@30246: by (simp add: map_def split add: option.split) nipkow@30246: nipkow@30246: lemma option_map_o_sum_case [simp]: nipkow@30246: "map f o sum_case g h = sum_case (map f o g) (map f o h)" nipkow@30246: by (rule ext) (simp split: sum.split) nipkow@30246: haftmann@41372: type_lifting map: Option.map proof - haftmann@41372: fix f g haftmann@41372: show "Option.map f \ Option.map g = Option.map (f \ g)" haftmann@41372: proof haftmann@41372: fix x haftmann@41372: show "(Option.map f \ Option.map g) x= Option.map (f \ g) x" haftmann@41372: by (cases x) simp_all haftmann@41372: qed haftmann@40609: next haftmann@41372: show "Option.map id = id" haftmann@41372: proof haftmann@41372: fix x haftmann@41372: show "Option.map id x = id x" haftmann@41372: by (cases x) simp_all haftmann@41372: qed haftmann@40609: qed haftmann@40609: krauss@39149: primrec bind :: "'a option \ ('a \ 'b option) \ 'b option" where krauss@39149: bind_lzero: "bind None f = None" | krauss@39149: bind_lunit: "bind (Some x) f = f x" nipkow@30246: krauss@39149: lemma bind_runit[simp]: "bind x Some = x" krauss@39149: by (cases x) auto krauss@39149: krauss@39149: lemma bind_assoc[simp]: "bind (bind x f) g = bind x (\y. bind (f y) g)" krauss@39149: by (cases x) auto krauss@39149: krauss@39149: lemma bind_rzero[simp]: "bind x (\x. None) = None" krauss@39149: by (cases x) auto krauss@39149: krauss@39149: hide_const (open) set map bind nipkow@30246: nipkow@30246: subsubsection {* Code generator setup *} nipkow@30246: haftmann@31154: definition is_none :: "'a option \ bool" where haftmann@31998: [code_post]: "is_none x \ x = None" nipkow@30246: nipkow@30246: lemma is_none_code [code]: nipkow@30246: shows "is_none None \ True" nipkow@30246: and "is_none (Some x) \ False" haftmann@31154: unfolding is_none_def by simp_all haftmann@31154: haftmann@32069: lemma [code_unfold]: haftmann@38857: "HOL.equal x None \ is_none x" krauss@39150: by (simp add: equal is_none_def) nipkow@30246: wenzelm@36176: hide_const (open) is_none nipkow@30246: nipkow@30246: code_type option nipkow@30246: (SML "_ option") nipkow@30246: (OCaml "_ option") nipkow@30246: (Haskell "Maybe _") haftmann@34886: (Scala "!Option[(_)]") nipkow@30246: nipkow@30246: code_const None and Some nipkow@30246: (SML "NONE" and "SOME") nipkow@30246: (OCaml "None" and "Some _") nipkow@30246: (Haskell "Nothing" and "Just") haftmann@37880: (Scala "!None" and "Some") nipkow@30246: haftmann@38857: code_instance option :: equal nipkow@30246: (Haskell -) nipkow@30246: haftmann@38857: code_const "HOL.equal \ 'a option \ 'a option \ bool" haftmann@39272: (Haskell infix 4 "==") nipkow@30246: nipkow@30246: code_reserved SML nipkow@30246: option NONE SOME nipkow@30246: nipkow@30246: code_reserved OCaml nipkow@30246: option None Some nipkow@30246: haftmann@34886: code_reserved Scala haftmann@34886: Option None Some haftmann@34886: nipkow@30246: end