src/HOL/Option.thy
author wenzelm
Mon Dec 07 10:38:04 2015 +0100 (2015-12-07)
changeset 61799 4cf66f21b764
parent 61630 608520e0e8e2
child 63194 0b7bdb75f451
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     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   \<comment> \<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   \<comment> \<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 option_rel_Some1: "rel_option A (Some x) y \<longleftrightarrow> (\<exists>y'. y = Some y' \<and> A x y')" (* Option *)
    69 by(cases y) simp_all
    70 
    71 lemma option_rel_Some2: "rel_option A x (Some y) \<longleftrightarrow> (\<exists>x'. x = Some x' \<and> A x' y)" (* Option *)
    72 by(cases x) simp_all
    73 
    74 lemma rel_option_inf: "inf (rel_option A) (rel_option B) = rel_option (inf A B)"
    75   (is "?lhs = ?rhs")
    76 proof (rule antisym)
    77   show "?lhs \<le> ?rhs" by (auto elim: option.rel_cases)
    78   show "?rhs \<le> ?lhs" by (auto elim: option.rel_mono_strong)
    79 qed
    80 
    81 lemma rel_option_reflI:
    82   "(\<And>x. x \<in> set_option y \<Longrightarrow> P x x) \<Longrightarrow> rel_option P y y"
    83   by (cases y) auto
    84 
    85 
    86 subsubsection \<open>Operations\<close>
    87 
    88 lemma ospec [dest]: "(\<forall>x\<in>set_option A. P x) \<Longrightarrow> A = Some x \<Longrightarrow> P x"
    89   by simp
    90 
    91 setup \<open>map_theory_claset (fn ctxt => ctxt addSD2 ("ospec", @{thm ospec}))\<close>
    92 
    93 lemma elem_set [iff]: "(x \<in> set_option xo) = (xo = Some x)"
    94   by (cases xo) auto
    95 
    96 lemma set_empty_eq [simp]: "(set_option xo = {}) = (xo = None)"
    97   by (cases xo) auto
    98 
    99 lemma map_option_case: "map_option f y = (case y of None \<Rightarrow> None | Some x \<Rightarrow> Some (f x))"
   100   by (auto split: option.split)
   101 
   102 lemma map_option_is_None [iff]: "(map_option f opt = None) = (opt = None)"
   103   by (simp add: map_option_case split add: option.split)
   104 
   105 lemma None_eq_map_option_iff [iff]: "None = map_option f x \<longleftrightarrow> x = None"
   106 by(cases x) simp_all
   107 
   108 lemma map_option_eq_Some [iff]: "(map_option f xo = Some y) = (\<exists>z. xo = Some z \<and> f z = y)"
   109   by (simp add: map_option_case split add: option.split)
   110 
   111 lemma map_option_o_case_sum [simp]:
   112     "map_option f o case_sum g h = case_sum (map_option f o g) (map_option f o h)"
   113   by (rule o_case_sum)
   114 
   115 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"
   116   by (cases x) auto
   117 
   118 lemma map_option_idI: "(\<And>y. y \<in> set_option x \<Longrightarrow> f y = y) \<Longrightarrow> map_option f x = x"
   119 by(cases x)(simp_all)
   120 
   121 functor map_option: map_option
   122   by (simp_all add: option.map_comp fun_eq_iff option.map_id)
   123 
   124 lemma case_map_option [simp]: "case_option g h (map_option f x) = case_option g (h \<circ> f) x"
   125   by (cases x) simp_all
   126 
   127 lemma None_notin_image_Some [simp]: "None \<notin> Some ` A"
   128 by auto
   129 
   130 lemma notin_range_Some: "x \<notin> range Some \<longleftrightarrow> x = None"
   131 by(cases x) auto
   132 
   133 lemma rel_option_iff:
   134   "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
   135     | (Some x, Some y) \<Rightarrow> R x y
   136     | _ \<Rightarrow> False)"
   137   by (auto split: prod.split option.split)
   138 
   139 context
   140 begin
   141 
   142 qualified definition is_none :: "'a option \<Rightarrow> bool"
   143   where [code_post]: "is_none x \<longleftrightarrow> x = None"
   144 
   145 lemma is_none_simps [simp]:
   146   "is_none None"
   147   "\<not> is_none (Some x)"
   148   by (simp_all add: is_none_def)
   149 
   150 lemma is_none_code [code]:
   151   "is_none None = True"
   152   "is_none (Some x) = False"
   153   by simp_all
   154 
   155 lemma rel_option_unfold:
   156   "rel_option R x y \<longleftrightarrow>
   157    (is_none x \<longleftrightarrow> is_none y) \<and> (\<not> is_none x \<longrightarrow> \<not> is_none y \<longrightarrow> R (the x) (the y))"
   158   by (simp add: rel_option_iff split: option.split)
   159 
   160 lemma rel_optionI:
   161   "\<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>
   162   \<Longrightarrow> rel_option P x y"
   163   by (simp add: rel_option_unfold)
   164 
   165 lemma is_none_map_option [simp]: "is_none (map_option f x) \<longleftrightarrow> is_none x"
   166   by (simp add: is_none_def)
   167 
   168 lemma the_map_option: "\<not> is_none x \<Longrightarrow> the (map_option f x) = f (the x)"
   169   by (auto simp add: is_none_def)
   170 
   171 
   172 qualified primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"
   173 where
   174   bind_lzero: "bind None f = None"
   175 | bind_lunit: "bind (Some x) f = f x"
   176 
   177 lemma is_none_bind: "is_none (bind f g) \<longleftrightarrow> is_none f \<or> is_none (g (the f))"
   178   by (cases f) simp_all
   179 
   180 lemma bind_runit[simp]: "bind x Some = x"
   181   by (cases x) auto
   182 
   183 lemma bind_assoc[simp]: "bind (bind x f) g = bind x (\<lambda>y. bind (f y) g)"
   184   by (cases x) auto
   185 
   186 lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None"
   187   by (cases x) auto
   188 
   189 qualified lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
   190   by (cases x) auto
   191 
   192 lemma bind_split: "P (bind m f) \<longleftrightarrow> (m = None \<longrightarrow> P None) \<and> (\<forall>v. m = Some v \<longrightarrow> P (f v))"
   193   by (cases m) auto
   194 
   195 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)))"
   196   by (cases m) auto
   197 
   198 lemmas bind_splits = bind_split bind_split_asm
   199 
   200 lemma bind_eq_Some_conv: "bind f g = Some x \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
   201   by (cases f) simp_all
   202 
   203 lemma bind_eq_None_conv: "Option.bind a f = None \<longleftrightarrow> a = None \<or> f (the a) = None"
   204 by(cases a) simp_all
   205 
   206 lemma map_option_bind: "map_option f (bind x g) = bind x (map_option f \<circ> g)"
   207   by (cases x) simp_all
   208 
   209 lemma bind_option_cong:
   210   "\<lbrakk> x = y; \<And>z. z \<in> set_option y \<Longrightarrow> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g"
   211   by (cases y) simp_all
   212 
   213 lemma bind_option_cong_simp:
   214   "\<lbrakk> x = y; \<And>z. z \<in> set_option y =simp=> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g"
   215   unfolding simp_implies_def by (rule bind_option_cong)
   216 
   217 lemma bind_option_cong_code: "x = y \<Longrightarrow> bind x f = bind y f"
   218   by simp
   219 
   220 lemma bind_map_option: "bind (map_option f x) g = bind x (g \<circ> f)"
   221 by(cases x) simp_all
   222 
   223 lemma set_bind_option [simp]: "set_option (bind x f) = UNION (set_option x) (set_option \<circ> f)"
   224 by(cases x) auto
   225 
   226 lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \<circ> f)"
   227 by(cases x) simp_all
   228 
   229 end
   230 
   231 setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})\<close>
   232 
   233 
   234 context
   235 begin
   236 
   237 qualified definition these :: "'a option set \<Rightarrow> 'a set"
   238   where "these A = the ` {x \<in> A. x \<noteq> None}"
   239 
   240 lemma these_empty [simp]: "these {} = {}"
   241   by (simp add: these_def)
   242 
   243 lemma these_insert_None [simp]: "these (insert None A) = these A"
   244   by (auto simp add: these_def)
   245 
   246 lemma these_insert_Some [simp]: "these (insert (Some x) A) = insert x (these A)"
   247 proof -
   248   have "{y \<in> insert (Some x) A. y \<noteq> None} = insert (Some x) {y \<in> A. y \<noteq> None}"
   249     by auto
   250   then show ?thesis by (simp add: these_def)
   251 qed
   252 
   253 lemma in_these_eq: "x \<in> these A \<longleftrightarrow> Some x \<in> A"
   254 proof
   255   assume "Some x \<in> A"
   256   then obtain B where "A = insert (Some x) B" by auto
   257   then show "x \<in> these A" by (auto simp add: these_def intro!: image_eqI)
   258 next
   259   assume "x \<in> these A"
   260   then show "Some x \<in> A" by (auto simp add: these_def)
   261 qed
   262 
   263 lemma these_image_Some_eq [simp]: "these (Some ` A) = A"
   264   by (auto simp add: these_def intro!: image_eqI)
   265 
   266 lemma Some_image_these_eq: "Some ` these A = {x\<in>A. x \<noteq> None}"
   267   by (auto simp add: these_def image_image intro!: image_eqI)
   268 
   269 lemma these_empty_eq: "these B = {} \<longleftrightarrow> B = {} \<or> B = {None}"
   270   by (auto simp add: these_def)
   271 
   272 lemma these_not_empty_eq: "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
   273   by (auto simp add: these_empty_eq)
   274 
   275 end
   276 
   277 
   278 subsection \<open>Transfer rules for the Transfer package\<close>
   279 
   280 context
   281 begin
   282 
   283 interpretation lifting_syntax .
   284 
   285 lemma option_bind_transfer [transfer_rule]:
   286   "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
   287     Option.bind Option.bind"
   288   unfolding rel_fun_def split_option_all by simp
   289 
   290 lemma pred_option_parametric [transfer_rule]:
   291   "((A ===> op =) ===> rel_option A ===> op =) pred_option pred_option"
   292   by (rule rel_funI)+ (auto simp add: rel_option_unfold Option.is_none_def dest: rel_funD)
   293 
   294 end
   295 
   296 
   297 subsubsection \<open>Interaction with finite sets\<close>
   298 
   299 lemma finite_option_UNIV [simp]:
   300   "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
   301   by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
   302 
   303 instance option :: (finite) finite
   304   by standard (simp add: UNIV_option_conv)
   305 
   306 
   307 subsubsection \<open>Code generator setup\<close>
   308 
   309 lemma equal_None_code_unfold [code_unfold]:
   310   "HOL.equal x None \<longleftrightarrow> Option.is_none x"
   311   "HOL.equal None = Option.is_none"
   312   by (auto simp add: equal Option.is_none_def)
   313 
   314 code_printing
   315   type_constructor option \<rightharpoonup>
   316     (SML) "_ option"
   317     and (OCaml) "_ option"
   318     and (Haskell) "Maybe _"
   319     and (Scala) "!Option[(_)]"
   320 | constant None \<rightharpoonup>
   321     (SML) "NONE"
   322     and (OCaml) "None"
   323     and (Haskell) "Nothing"
   324     and (Scala) "!None"
   325 | constant Some \<rightharpoonup>
   326     (SML) "SOME"
   327     and (OCaml) "Some _"
   328     and (Haskell) "Just"
   329     and (Scala) "Some"
   330 | class_instance option :: equal \<rightharpoonup>
   331     (Haskell) -
   332 | constant "HOL.equal :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" \<rightharpoonup>
   333     (Haskell) infix 4 "=="
   334 
   335 code_reserved SML
   336   option NONE SOME
   337 
   338 code_reserved OCaml
   339   option None Some
   340 
   341 code_reserved Scala
   342   Option None Some
   343 
   344 end