src/HOL/Option.thy
author wenzelm
Mon Aug 31 19:34:26 2015 +0200 (2015-08-31)
changeset 61066 00a169fe5de4
parent 60758 d8d85a8172b5
child 61068 6cb92c2a5ece
permissions -rw-r--r--
misc tuning and modernization;
     1 (*  Title:      HOL/Option.thy
     2     Author:     Folklore
     3 *)
     4 
     5 section \<open>Datatype option\<close>
     6 
     7 theory Option
     8 imports Lifting Finite_Set
     9 begin
    10 
    11 datatype 'a option =
    12     None
    13   | Some (the: 'a)
    14 
    15 datatype_compat option
    16 
    17 lemma [case_names None Some, cases type: option]:
    18   -- \<open>for backward compatibility -- names of variables differ\<close>
    19   "(y = None \<Longrightarrow> P) \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> P) \<Longrightarrow> P"
    20   by (rule option.exhaust)
    21 
    22 lemma [case_names None Some, induct type: option]:
    23   -- \<open>for backward compatibility -- names of variables differ\<close>
    24   "P None \<Longrightarrow> (\<And>option. P (Some option)) \<Longrightarrow> P option"
    25   by (rule option.induct)
    26 
    27 text \<open>Compatibility:\<close>
    28 setup \<open>Sign.mandatory_path "option"\<close>
    29 lemmas inducts = option.induct
    30 lemmas cases = option.case
    31 setup \<open>Sign.parent_path\<close>
    32 
    33 lemma not_None_eq [iff]: "x \<noteq> None \<longleftrightarrow> (\<exists>y. x = Some y)"
    34   by (induct x) auto
    35 
    36 lemma not_Some_eq [iff]: "(\<forall>y. x \<noteq> Some y) \<longleftrightarrow> x = None"
    37   by (induct x) auto
    38 
    39 text \<open>Although it may appear that both of these equalities are helpful
    40 only when applied to assumptions, in practice it seems better to give
    41 them the uniform iff attribute.\<close>
    42 
    43 lemma inj_Some [simp]: "inj_on Some A"
    44   by (rule inj_onI) simp
    45 
    46 lemma case_optionE:
    47   assumes c: "(case x of None \<Rightarrow> P | Some y \<Rightarrow> Q y)"
    48   obtains
    49     (None) "x = None" and P
    50   | (Some) y where "x = Some y" and "Q y"
    51   using c by (cases x) simp_all
    52 
    53 lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))"
    54   by (auto intro: option.induct)
    55 
    56 lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
    57   using split_option_all[of "\<lambda>x. \<not> P x"] by blast
    58 
    59 lemma UNIV_option_conv: "UNIV = insert None (range Some)"
    60   by (auto intro: classical)
    61 
    62 lemma rel_option_None1 [simp]: "rel_option P None x \<longleftrightarrow> x = None"
    63   by (cases x) simp_all
    64 
    65 lemma rel_option_None2 [simp]: "rel_option P x None \<longleftrightarrow> x = None"
    66   by (cases x) simp_all
    67 
    68 lemma rel_option_inf: "inf (rel_option A) (rel_option B) = rel_option (inf A B)"
    69   (is "?lhs = ?rhs")
    70 proof (rule antisym)
    71   show "?lhs \<le> ?rhs" by (auto elim: option.rel_cases)
    72   show "?rhs \<le> ?lhs" by (auto elim: option.rel_mono_strong)
    73 qed
    74 
    75 lemma rel_option_reflI:
    76   "(\<And>x. x \<in> set_option y \<Longrightarrow> P x x) \<Longrightarrow> rel_option P y y"
    77   by (cases y) auto
    78 
    79 
    80 subsubsection \<open>Operations\<close>
    81 
    82 lemma ospec [dest]: "(\<forall>x\<in>set_option A. P x) \<Longrightarrow> A = Some x \<Longrightarrow> P x"
    83   by simp
    84 
    85 setup \<open>map_theory_claset (fn ctxt => ctxt addSD2 ("ospec", @{thm ospec}))\<close>
    86 
    87 lemma elem_set [iff]: "(x \<in> set_option xo) = (xo = Some x)"
    88   by (cases xo) auto
    89 
    90 lemma set_empty_eq [simp]: "(set_option xo = {}) = (xo = None)"
    91   by (cases xo) auto
    92 
    93 lemma map_option_case: "map_option f y = (case y of None \<Rightarrow> None | Some x \<Rightarrow> Some (f x))"
    94   by (auto split: option.split)
    95 
    96 lemma map_option_is_None [iff]: "(map_option f opt = None) = (opt = None)"
    97   by (simp add: map_option_case split add: option.split)
    98 
    99 lemma map_option_eq_Some [iff]: "(map_option f xo = Some y) = (\<exists>z. xo = Some z \<and> f z = y)"
   100   by (simp add: map_option_case split add: option.split)
   101 
   102 lemma map_option_o_case_sum [simp]:
   103     "map_option f o case_sum g h = case_sum (map_option f o g) (map_option f o h)"
   104   by (rule o_case_sum)
   105 
   106 lemma map_option_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map_option f x = map_option g y"
   107   by (cases x) auto
   108 
   109 functor map_option: map_option
   110   by (simp_all add: option.map_comp fun_eq_iff option.map_id)
   111 
   112 lemma case_map_option [simp]: "case_option g h (map_option f x) = case_option g (h \<circ> f) x"
   113   by (cases x) simp_all
   114 
   115 lemma rel_option_iff:
   116   "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
   117     | (Some x, Some y) \<Rightarrow> R x y
   118     | _ \<Rightarrow> False)"
   119   by (auto split: prod.split option.split)
   120 
   121 definition is_none :: "'a option \<Rightarrow> bool"
   122   where [code_post]: "is_none x \<longleftrightarrow> x = None"
   123 
   124 lemma is_none_simps [simp]:
   125   "is_none None"
   126   "\<not> is_none (Some x)"
   127   by (simp_all add: is_none_def)
   128 
   129 lemma is_none_code [code]:
   130   "is_none None = True"
   131   "is_none (Some x) = False"
   132   by simp_all
   133 
   134 lemma rel_option_unfold:
   135   "rel_option R x y \<longleftrightarrow>
   136    (is_none x \<longleftrightarrow> is_none y) \<and> (\<not> is_none x \<longrightarrow> \<not> is_none y \<longrightarrow> R (the x) (the y))"
   137   by (simp add: rel_option_iff split: option.split)
   138 
   139 lemma rel_optionI:
   140   "\<lbrakk> is_none x \<longleftrightarrow> is_none y; \<lbrakk> \<not> is_none x; \<not> is_none y \<rbrakk> \<Longrightarrow> P (the x) (the y) \<rbrakk>
   141   \<Longrightarrow> rel_option P x y"
   142   by (simp add: rel_option_unfold)
   143 
   144 lemma is_none_map_option [simp]: "is_none (map_option f x) \<longleftrightarrow> is_none x"
   145   by (simp add: is_none_def)
   146 
   147 lemma the_map_option: "\<not> is_none x \<Longrightarrow> the (map_option f x) = f (the x)"
   148   by (auto simp add: is_none_def)
   149 
   150 
   151 primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"
   152 where
   153   bind_lzero: "bind None f = None"
   154 | bind_lunit: "bind (Some x) f = f x"
   155 
   156 lemma is_none_bind: "is_none (bind f g) \<longleftrightarrow> is_none f \<or> is_none (g (the f))"
   157   by (cases f) simp_all
   158 
   159 lemma bind_runit[simp]: "bind x Some = x"
   160   by (cases x) auto
   161 
   162 lemma bind_assoc[simp]: "bind (bind x f) g = bind x (\<lambda>y. bind (f y) g)"
   163   by (cases x) auto
   164 
   165 lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None"
   166   by (cases x) auto
   167 
   168 lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
   169   by (cases x) auto
   170 
   171 lemma bind_split: "P (bind m f) \<longleftrightarrow> (m = None \<longrightarrow> P None) \<and> (\<forall>v. m = Some v \<longrightarrow> P (f v))"
   172   by (cases m) auto
   173 
   174 lemma bind_split_asm: "P (bind m f) \<longleftrightarrow> \<not> (m = None \<and> \<not> P None \<or> (\<exists>x. m = Some x \<and> \<not> P (f x)))"
   175   by (cases m) auto
   176 
   177 lemmas bind_splits = bind_split bind_split_asm
   178 
   179 lemma bind_eq_Some_conv: "bind f g = Some x \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
   180   by (cases f) simp_all
   181 
   182 lemma map_option_bind: "map_option f (bind x g) = bind x (map_option f \<circ> g)"
   183   by (cases x) simp_all
   184 
   185 lemma bind_option_cong:
   186   "\<lbrakk> x = y; \<And>z. z \<in> set_option y \<Longrightarrow> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g"
   187   by (cases y) simp_all
   188 
   189 lemma bind_option_cong_simp:
   190   "\<lbrakk> x = y; \<And>z. z \<in> set_option y =simp=> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g"
   191   unfolding simp_implies_def by (rule bind_option_cong)
   192 
   193 lemma bind_option_cong_code: "x = y \<Longrightarrow> bind x f = bind y f"
   194   by simp
   195 setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})\<close>
   196 
   197 
   198 definition these :: "'a option set \<Rightarrow> 'a set"
   199   where "these A = the ` {x \<in> A. x \<noteq> None}"
   200 
   201 lemma these_empty [simp]: "these {} = {}"
   202   by (simp add: these_def)
   203 
   204 lemma these_insert_None [simp]: "these (insert None A) = these A"
   205   by (auto simp add: these_def)
   206 
   207 lemma these_insert_Some [simp]: "these (insert (Some x) A) = insert x (these A)"
   208 proof -
   209   have "{y \<in> insert (Some x) A. y \<noteq> None} = insert (Some x) {y \<in> A. y \<noteq> None}"
   210     by auto
   211   then show ?thesis by (simp add: these_def)
   212 qed
   213 
   214 lemma in_these_eq: "x \<in> these A \<longleftrightarrow> Some x \<in> A"
   215 proof
   216   assume "Some x \<in> A"
   217   then obtain B where "A = insert (Some x) B" by auto
   218   then show "x \<in> these A" by (auto simp add: these_def intro!: image_eqI)
   219 next
   220   assume "x \<in> these A"
   221   then show "Some x \<in> A" by (auto simp add: these_def)
   222 qed
   223 
   224 lemma these_image_Some_eq [simp]: "these (Some ` A) = A"
   225   by (auto simp add: these_def intro!: image_eqI)
   226 
   227 lemma Some_image_these_eq: "Some ` these A = {x\<in>A. x \<noteq> None}"
   228   by (auto simp add: these_def image_image intro!: image_eqI)
   229 
   230 lemma these_empty_eq: "these B = {} \<longleftrightarrow> B = {} \<or> B = {None}"
   231   by (auto simp add: these_def)
   232 
   233 lemma these_not_empty_eq: "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
   234   by (auto simp add: these_empty_eq)
   235 
   236 hide_const (open) bind these
   237 hide_fact (open) bind_cong
   238 
   239 
   240 subsection \<open>Transfer rules for the Transfer package\<close>
   241 
   242 context
   243 begin
   244 
   245 interpretation lifting_syntax .
   246 
   247 lemma option_bind_transfer [transfer_rule]:
   248   "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
   249     Option.bind Option.bind"
   250   unfolding rel_fun_def split_option_all by simp
   251 
   252 lemma pred_option_parametric [transfer_rule]:
   253   "((A ===> op =) ===> rel_option A ===> op =) pred_option pred_option"
   254   by (rule rel_funI)+ (auto simp add: rel_option_unfold is_none_def dest: rel_funD)
   255 
   256 end
   257 
   258 
   259 subsubsection \<open>Interaction with finite sets\<close>
   260 
   261 lemma finite_option_UNIV [simp]:
   262   "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
   263   by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
   264 
   265 instance option :: (finite) finite
   266   by standard (simp add: UNIV_option_conv)
   267 
   268 
   269 subsubsection \<open>Code generator setup\<close>
   270 
   271 lemma equal_None_code_unfold [code_unfold]:
   272   "HOL.equal x None \<longleftrightarrow> is_none x"
   273   "HOL.equal None = is_none"
   274   by (auto simp add: equal is_none_def)
   275 
   276 hide_const (open) is_none
   277 
   278 code_printing
   279   type_constructor option \<rightharpoonup>
   280     (SML) "_ option"
   281     and (OCaml) "_ option"
   282     and (Haskell) "Maybe _"
   283     and (Scala) "!Option[(_)]"
   284 | constant None \<rightharpoonup>
   285     (SML) "NONE"
   286     and (OCaml) "None"
   287     and (Haskell) "Nothing"
   288     and (Scala) "!None"
   289 | constant Some \<rightharpoonup>
   290     (SML) "SOME"
   291     and (OCaml) "Some _"
   292     and (Haskell) "Just"
   293     and (Scala) "Some"
   294 | class_instance option :: equal \<rightharpoonup>
   295     (Haskell) -
   296 | constant "HOL.equal :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" \<rightharpoonup>
   297     (Haskell) infix 4 "=="
   298 
   299 code_reserved SML
   300   option NONE SOME
   301 
   302 code_reserved OCaml
   303   option None Some
   304 
   305 code_reserved Scala
   306   Option None Some
   307 
   308 end