src/HOL/Option.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 63194 0b7bdb75f451
child 63648 f9f3006a5579
permissions -rw-r--r--
bundle lifting_syntax;
     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 
   140 definition combine_options :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> 'a option"
   141   where "combine_options f x y = 
   142            (case x of None \<Rightarrow> y | Some x \<Rightarrow> (case y of None \<Rightarrow> Some x | Some y \<Rightarrow> Some (f x y)))"
   143 
   144 lemma combine_options_simps [simp]:
   145   "combine_options f None y = y"
   146   "combine_options f x None = x"
   147   "combine_options f (Some a) (Some b) = Some (f a b)"
   148   by (simp_all add: combine_options_def split: option.splits)
   149   
   150 lemma combine_options_cases [case_names None1 None2 Some]:
   151   "(x = None \<Longrightarrow> P x y) \<Longrightarrow> (y = None \<Longrightarrow> P x y) \<Longrightarrow> 
   152      (\<And>a b. x = Some a \<Longrightarrow> y = Some b \<Longrightarrow> P x y) \<Longrightarrow> P x y"
   153   by (cases x; cases y) simp_all
   154 
   155 lemma combine_options_commute: 
   156   "(\<And>x y. f x y = f y x) \<Longrightarrow> combine_options f x y = combine_options f y x"
   157   using combine_options_cases[of x ]
   158   by (induction x y rule: combine_options_cases) simp_all
   159 
   160 lemma combine_options_assoc:
   161   "(\<And>x y z. f (f x y) z = f x (f y z)) \<Longrightarrow> 
   162      combine_options f (combine_options f x y) z =
   163      combine_options f x (combine_options f y z)"
   164   by (auto simp: combine_options_def split: option.splits)
   165 
   166 lemma combine_options_left_commute:
   167   "(\<And>x y. f x y = f y x) \<Longrightarrow> (\<And>x y z. f (f x y) z = f x (f y z)) \<Longrightarrow> 
   168      combine_options f y (combine_options f x z) =
   169      combine_options f x (combine_options f y z)"
   170   by (auto simp: combine_options_def split: option.splits)
   171 
   172 lemmas combine_options_ac = 
   173   combine_options_commute combine_options_assoc combine_options_left_commute
   174 
   175 
   176 context
   177 begin
   178 
   179 qualified definition is_none :: "'a option \<Rightarrow> bool"
   180   where [code_post]: "is_none x \<longleftrightarrow> x = None"
   181 
   182 lemma is_none_simps [simp]:
   183   "is_none None"
   184   "\<not> is_none (Some x)"
   185   by (simp_all add: is_none_def)
   186 
   187 lemma is_none_code [code]:
   188   "is_none None = True"
   189   "is_none (Some x) = False"
   190   by simp_all
   191 
   192 lemma rel_option_unfold:
   193   "rel_option R x y \<longleftrightarrow>
   194    (is_none x \<longleftrightarrow> is_none y) \<and> (\<not> is_none x \<longrightarrow> \<not> is_none y \<longrightarrow> R (the x) (the y))"
   195   by (simp add: rel_option_iff split: option.split)
   196 
   197 lemma rel_optionI:
   198   "\<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>
   199   \<Longrightarrow> rel_option P x y"
   200   by (simp add: rel_option_unfold)
   201 
   202 lemma is_none_map_option [simp]: "is_none (map_option f x) \<longleftrightarrow> is_none x"
   203   by (simp add: is_none_def)
   204 
   205 lemma the_map_option: "\<not> is_none x \<Longrightarrow> the (map_option f x) = f (the x)"
   206   by (auto simp add: is_none_def)
   207 
   208 
   209 qualified primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"
   210 where
   211   bind_lzero: "bind None f = None"
   212 | bind_lunit: "bind (Some x) f = f x"
   213 
   214 lemma is_none_bind: "is_none (bind f g) \<longleftrightarrow> is_none f \<or> is_none (g (the f))"
   215   by (cases f) simp_all
   216 
   217 lemma bind_runit[simp]: "bind x Some = x"
   218   by (cases x) auto
   219 
   220 lemma bind_assoc[simp]: "bind (bind x f) g = bind x (\<lambda>y. bind (f y) g)"
   221   by (cases x) auto
   222 
   223 lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None"
   224   by (cases x) auto
   225 
   226 qualified lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
   227   by (cases x) auto
   228 
   229 lemma bind_split: "P (bind m f) \<longleftrightarrow> (m = None \<longrightarrow> P None) \<and> (\<forall>v. m = Some v \<longrightarrow> P (f v))"
   230   by (cases m) auto
   231 
   232 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)))"
   233   by (cases m) auto
   234 
   235 lemmas bind_splits = bind_split bind_split_asm
   236 
   237 lemma bind_eq_Some_conv: "bind f g = Some x \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
   238   by (cases f) simp_all
   239 
   240 lemma bind_eq_None_conv: "Option.bind a f = None \<longleftrightarrow> a = None \<or> f (the a) = None"
   241 by(cases a) simp_all
   242 
   243 lemma map_option_bind: "map_option f (bind x g) = bind x (map_option f \<circ> g)"
   244   by (cases x) simp_all
   245 
   246 lemma bind_option_cong:
   247   "\<lbrakk> x = y; \<And>z. z \<in> set_option y \<Longrightarrow> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g"
   248   by (cases y) simp_all
   249 
   250 lemma bind_option_cong_simp:
   251   "\<lbrakk> x = y; \<And>z. z \<in> set_option y =simp=> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g"
   252   unfolding simp_implies_def by (rule bind_option_cong)
   253 
   254 lemma bind_option_cong_code: "x = y \<Longrightarrow> bind x f = bind y f"
   255   by simp
   256 
   257 lemma bind_map_option: "bind (map_option f x) g = bind x (g \<circ> f)"
   258 by(cases x) simp_all
   259 
   260 lemma set_bind_option [simp]: "set_option (bind x f) = UNION (set_option x) (set_option \<circ> f)"
   261 by(cases x) auto
   262 
   263 lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \<circ> f)"
   264 by(cases x) simp_all
   265 
   266 end
   267 
   268 setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})\<close>
   269 
   270 
   271 context
   272 begin
   273 
   274 qualified definition these :: "'a option set \<Rightarrow> 'a set"
   275   where "these A = the ` {x \<in> A. x \<noteq> None}"
   276 
   277 lemma these_empty [simp]: "these {} = {}"
   278   by (simp add: these_def)
   279 
   280 lemma these_insert_None [simp]: "these (insert None A) = these A"
   281   by (auto simp add: these_def)
   282 
   283 lemma these_insert_Some [simp]: "these (insert (Some x) A) = insert x (these A)"
   284 proof -
   285   have "{y \<in> insert (Some x) A. y \<noteq> None} = insert (Some x) {y \<in> A. y \<noteq> None}"
   286     by auto
   287   then show ?thesis by (simp add: these_def)
   288 qed
   289 
   290 lemma in_these_eq: "x \<in> these A \<longleftrightarrow> Some x \<in> A"
   291 proof
   292   assume "Some x \<in> A"
   293   then obtain B where "A = insert (Some x) B" by auto
   294   then show "x \<in> these A" by (auto simp add: these_def intro!: image_eqI)
   295 next
   296   assume "x \<in> these A"
   297   then show "Some x \<in> A" by (auto simp add: these_def)
   298 qed
   299 
   300 lemma these_image_Some_eq [simp]: "these (Some ` A) = A"
   301   by (auto simp add: these_def intro!: image_eqI)
   302 
   303 lemma Some_image_these_eq: "Some ` these A = {x\<in>A. x \<noteq> None}"
   304   by (auto simp add: these_def image_image intro!: image_eqI)
   305 
   306 lemma these_empty_eq: "these B = {} \<longleftrightarrow> B = {} \<or> B = {None}"
   307   by (auto simp add: these_def)
   308 
   309 lemma these_not_empty_eq: "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
   310   by (auto simp add: these_empty_eq)
   311 
   312 end
   313 
   314 
   315 subsection \<open>Transfer rules for the Transfer package\<close>
   316 
   317 context includes lifting_syntax
   318 begin
   319 
   320 lemma option_bind_transfer [transfer_rule]:
   321   "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
   322     Option.bind Option.bind"
   323   unfolding rel_fun_def split_option_all by simp
   324 
   325 lemma pred_option_parametric [transfer_rule]:
   326   "((A ===> op =) ===> rel_option A ===> op =) pred_option pred_option"
   327   by (rule rel_funI)+ (auto simp add: rel_option_unfold Option.is_none_def dest: rel_funD)
   328 
   329 end
   330 
   331 
   332 subsubsection \<open>Interaction with finite sets\<close>
   333 
   334 lemma finite_option_UNIV [simp]:
   335   "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
   336   by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
   337 
   338 instance option :: (finite) finite
   339   by standard (simp add: UNIV_option_conv)
   340 
   341 
   342 subsubsection \<open>Code generator setup\<close>
   343 
   344 lemma equal_None_code_unfold [code_unfold]:
   345   "HOL.equal x None \<longleftrightarrow> Option.is_none x"
   346   "HOL.equal None = Option.is_none"
   347   by (auto simp add: equal Option.is_none_def)
   348 
   349 code_printing
   350   type_constructor option \<rightharpoonup>
   351     (SML) "_ option"
   352     and (OCaml) "_ option"
   353     and (Haskell) "Maybe _"
   354     and (Scala) "!Option[(_)]"
   355 | constant None \<rightharpoonup>
   356     (SML) "NONE"
   357     and (OCaml) "None"
   358     and (Haskell) "Nothing"
   359     and (Scala) "!None"
   360 | constant Some \<rightharpoonup>
   361     (SML) "SOME"
   362     and (OCaml) "Some _"
   363     and (Haskell) "Just"
   364     and (Scala) "Some"
   365 | class_instance option :: equal \<rightharpoonup>
   366     (Haskell) -
   367 | constant "HOL.equal :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" \<rightharpoonup>
   368     (Haskell) infix 4 "=="
   369 
   370 code_reserved SML
   371   option NONE SOME
   372 
   373 code_reserved OCaml
   374   option None Some
   375 
   376 code_reserved Scala
   377   Option None Some
   378 
   379 end