src/HOL/Option.thy
author haftmann
Tue Jul 14 10:54:04 2009 +0200 (2009-07-14)
changeset 31998 2c7a24f74db9
parent 31154 f919b8e67413
child 32069 6d28bbd33e2c
permissions -rw-r--r--
code attributes use common underscore convention
     1 (*  Title:      HOL/Option.thy
     2     Author:     Folklore
     3 *)
     4 
     5 header {* Datatype option *}
     6 
     7 theory Option
     8 imports Datatype Finite_Set
     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 inj_Some [simp]: "inj_on Some A"
    24 by (rule inj_onI) simp
    25 
    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 
    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)
    39 
    40 instance option :: (finite) finite proof
    41 qed (simp add: UNIV_option_conv)
    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 
    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))"
    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 
    96 definition is_none :: "'a option \<Rightarrow> bool" where
    97   [code_post]: "is_none x \<longleftrightarrow> x = None"
    98 
    99 lemma is_none_code [code]:
   100   shows "is_none None \<longleftrightarrow> True"
   101     and "is_none (Some x) \<longleftrightarrow> False"
   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 
   108 lemma [code_inline]:
   109   "eq_class.eq x None \<longleftrightarrow> is_none x"
   110   by (simp add: eq is_none_none)
   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