1(* Title: HOL/Option.thy 2 Author: Folklore 3*) 4 5section \<open>Datatype option\<close> 6 7theory Option 8 imports Lifting 9begin 10 11datatype 'a option = 12 None 13 | Some (the: 'a) 14 15datatype_compat option 16 17lemma [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 22lemma [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 27text \<open>Compatibility:\<close> 28setup \<open>Sign.mandatory_path "option"\<close> 29lemmas inducts = option.induct 30lemmas cases = option.case 31setup \<open>Sign.parent_path\<close> 32 33lemma not_None_eq [iff]: "x \<noteq> None \<longleftrightarrow> (\<exists>y. x = Some y)" 34 by (induct x) auto 35 36lemma not_Some_eq [iff]: "(\<forall>y. x \<noteq> Some y) \<longleftrightarrow> x = None" 37 by (induct x) auto 38 39lemma comp_the_Some[simp]: "the o Some = id" 40by auto 41 42text \<open>Although it may appear that both of these equalities are helpful 43only when applied to assumptions, in practice it seems better to give 44them the uniform iff attribute.\<close> 45 46lemma inj_Some [simp]: "inj_on Some A" 47 by (rule inj_onI) simp 48 49lemma case_optionE: 50 assumes c: "(case x of None \<Rightarrow> P | Some y \<Rightarrow> Q y)" 51 obtains 52 (None) "x = None" and P 53 | (Some) y where "x = Some y" and "Q y" 54 using c by (cases x) simp_all 55 56lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))" 57 by (auto intro: option.induct) 58 59lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))" 60 using split_option_all[of "\<lambda>x. \<not> P x"] by blast 61 62lemma UNIV_option_conv: "UNIV = insert None (range Some)" 63 by (auto intro: classical) 64 65lemma rel_option_None1 [simp]: "rel_option P None x \<longleftrightarrow> x = None" 66 by (cases x) simp_all 67 68lemma rel_option_None2 [simp]: "rel_option P x None \<longleftrightarrow> x = None" 69 by (cases x) simp_all 70 71lemma option_rel_Some1: "rel_option A (Some x) y \<longleftrightarrow> (\<exists>y'. y = Some y' \<and> A x y')" (* Option *) 72by(cases y) simp_all 73 74lemma option_rel_Some2: "rel_option A x (Some y) \<longleftrightarrow> (\<exists>x'. x = Some x' \<and> A x' y)" (* Option *) 75by(cases x) simp_all 76 77lemma rel_option_inf: "inf (rel_option A) (rel_option B) = rel_option (inf A B)" 78 (is "?lhs = ?rhs") 79proof (rule antisym) 80 show "?lhs \<le> ?rhs" by (auto elim: option.rel_cases) 81 show "?rhs \<le> ?lhs" by (auto elim: option.rel_mono_strong) 82qed 83 84lemma rel_option_reflI: 85 "(\<And>x. x \<in> set_option y \<Longrightarrow> P x x) \<Longrightarrow> rel_option P y y" 86 by (cases y) auto 87 88 89subsubsection \<open>Operations\<close> 90 91lemma ospec [dest]: "(\<forall>x\<in>set_option A. P x) \<Longrightarrow> A = Some x \<Longrightarrow> P x" 92 by simp 93 94setup \<open>map_theory_claset (fn ctxt => ctxt addSD2 ("ospec", @{thm ospec}))\<close> 95 96lemma elem_set [iff]: "(x \<in> set_option xo) = (xo = Some x)" 97 by (cases xo) auto 98 99lemma set_empty_eq [simp]: "(set_option xo = {}) = (xo = None)" 100 by (cases xo) auto 101 102lemma map_option_case: "map_option f y = (case y of None \<Rightarrow> None | Some x \<Rightarrow> Some (f x))" 103 by (auto split: option.split) 104 105lemma map_option_is_None [iff]: "(map_option f opt = None) = (opt = None)" 106 by (simp add: map_option_case split: option.split) 107 108lemma None_eq_map_option_iff [iff]: "None = map_option f x \<longleftrightarrow> x = None" 109by(cases x) simp_all 110 111lemma map_option_eq_Some [iff]: "(map_option f xo = Some y) = (\<exists>z. xo = Some z \<and> f z = y)" 112 by (simp add: map_option_case split: option.split) 113 114lemma map_option_o_case_sum [simp]: 115 "map_option f \<circ> case_sum g h = case_sum (map_option f \<circ> g) (map_option f \<circ> h)" 116 by (rule o_case_sum) 117 118lemma 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" 119 by (cases x) auto 120 121lemma map_option_idI: "(\<And>y. y \<in> set_option x \<Longrightarrow> f y = y) \<Longrightarrow> map_option f x = x" 122by(cases x)(simp_all) 123 124functor map_option: map_option 125 by (simp_all add: option.map_comp fun_eq_iff option.map_id) 126 127lemma case_map_option [simp]: "case_option g h (map_option f x) = case_option g (h \<circ> f) x" 128 by (cases x) simp_all 129 130lemma None_notin_image_Some [simp]: "None \<notin> Some ` A" 131by auto 132 133lemma notin_range_Some: "x \<notin> range Some \<longleftrightarrow> x = None" 134by(cases x) auto 135 136lemma rel_option_iff: 137 "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True 138 | (Some x, Some y) \<Rightarrow> R x y 139 | _ \<Rightarrow> False)" 140 by (auto split: prod.split option.split) 141 142 143definition combine_options :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" 144 where "combine_options f x y = 145 (case x of None \<Rightarrow> y | Some x \<Rightarrow> (case y of None \<Rightarrow> Some x | Some y \<Rightarrow> Some (f x y)))" 146 147lemma combine_options_simps [simp]: 148 "combine_options f None y = y" 149 "combine_options f x None = x" 150 "combine_options f (Some a) (Some b) = Some (f a b)" 151 by (simp_all add: combine_options_def split: option.splits) 152 153lemma combine_options_cases [case_names None1 None2 Some]: 154 "(x = None \<Longrightarrow> P x y) \<Longrightarrow> (y = None \<Longrightarrow> P x y) \<Longrightarrow> 155 (\<And>a b. x = Some a \<Longrightarrow> y = Some b \<Longrightarrow> P x y) \<Longrightarrow> P x y" 156 by (cases x; cases y) simp_all 157 158lemma combine_options_commute: 159 "(\<And>x y. f x y = f y x) \<Longrightarrow> combine_options f x y = combine_options f y x" 160 using combine_options_cases[of x ] 161 by (induction x y rule: combine_options_cases) simp_all 162 163lemma combine_options_assoc: 164 "(\<And>x y z. f (f x y) z = f x (f y z)) \<Longrightarrow> 165 combine_options f (combine_options f x y) z = 166 combine_options f x (combine_options f y z)" 167 by (auto simp: combine_options_def split: option.splits) 168 169lemma combine_options_left_commute: 170 "(\<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> 171 combine_options f y (combine_options f x z) = 172 combine_options f x (combine_options f y z)" 173 by (auto simp: combine_options_def split: option.splits) 174 175lemmas combine_options_ac = 176 combine_options_commute combine_options_assoc combine_options_left_commute 177 178 179context 180begin 181 182qualified definition is_none :: "'a option \<Rightarrow> bool" 183 where [code_post]: "is_none x \<longleftrightarrow> x = None" 184 185lemma is_none_simps [simp]: 186 "is_none None" 187 "\<not> is_none (Some x)" 188 by (simp_all add: is_none_def) 189 190lemma is_none_code [code]: 191 "is_none None = True" 192 "is_none (Some x) = False" 193 by simp_all 194 195lemma rel_option_unfold: 196 "rel_option R x y \<longleftrightarrow> 197 (is_none x \<longleftrightarrow> is_none y) \<and> (\<not> is_none x \<longrightarrow> \<not> is_none y \<longrightarrow> R (the x) (the y))" 198 by (simp add: rel_option_iff split: option.split) 199 200lemma rel_optionI: 201 "\<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> 202 \<Longrightarrow> rel_option P x y" 203 by (simp add: rel_option_unfold) 204 205lemma is_none_map_option [simp]: "is_none (map_option f x) \<longleftrightarrow> is_none x" 206 by (simp add: is_none_def) 207 208lemma the_map_option: "\<not> is_none x \<Longrightarrow> the (map_option f x) = f (the x)" 209 by (auto simp add: is_none_def) 210 211 212qualified primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" 213where 214 bind_lzero: "bind None f = None" 215| bind_lunit: "bind (Some x) f = f x" 216 217lemma is_none_bind: "is_none (bind f g) \<longleftrightarrow> is_none f \<or> is_none (g (the f))" 218 by (cases f) simp_all 219 220lemma bind_runit[simp]: "bind x Some = x" 221 by (cases x) auto 222 223lemma bind_assoc[simp]: "bind (bind x f) g = bind x (\<lambda>y. bind (f y) g)" 224 by (cases x) auto 225 226lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None" 227 by (cases x) auto 228 229qualified lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g" 230 by (cases x) auto 231 232lemma bind_split: "P (bind m f) \<longleftrightarrow> (m = None \<longrightarrow> P None) \<and> (\<forall>v. m = Some v \<longrightarrow> P (f v))" 233 by (cases m) auto 234 235lemma 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)))" 236 by (cases m) auto 237 238lemmas bind_splits = bind_split bind_split_asm 239 240lemma bind_eq_Some_conv: "bind f g = Some x \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)" 241 by (cases f) simp_all 242 243lemma bind_eq_None_conv: "Option.bind a f = None \<longleftrightarrow> a = None \<or> f (the a) = None" 244by(cases a) simp_all 245 246lemma map_option_bind: "map_option f (bind x g) = bind x (map_option f \<circ> g)" 247 by (cases x) simp_all 248 249lemma bind_option_cong: 250 "\<lbrakk> x = y; \<And>z. z \<in> set_option y \<Longrightarrow> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g" 251 by (cases y) simp_all 252 253lemma bind_option_cong_simp: 254 "\<lbrakk> x = y; \<And>z. z \<in> set_option y =simp=> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g" 255 unfolding simp_implies_def by (rule bind_option_cong) 256 257lemma bind_option_cong_code: "x = y \<Longrightarrow> bind x f = bind y f" 258 by simp 259 260lemma bind_map_option: "bind (map_option f x) g = bind x (g \<circ> f)" 261by(cases x) simp_all 262 263lemma set_bind_option [simp]: "set_option (bind x f) = UNION (set_option x) (set_option \<circ> f)" 264by(cases x) auto 265 266lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \<circ> f)" 267by(cases x) simp_all 268 269end 270 271setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})\<close> 272 273 274context 275begin 276 277qualified definition these :: "'a option set \<Rightarrow> 'a set" 278 where "these A = the ` {x \<in> A. x \<noteq> None}" 279 280lemma these_empty [simp]: "these {} = {}" 281 by (simp add: these_def) 282 283lemma these_insert_None [simp]: "these (insert None A) = these A" 284 by (auto simp add: these_def) 285 286lemma these_insert_Some [simp]: "these (insert (Some x) A) = insert x (these A)" 287proof - 288 have "{y \<in> insert (Some x) A. y \<noteq> None} = insert (Some x) {y \<in> A. y \<noteq> None}" 289 by auto 290 then show ?thesis by (simp add: these_def) 291qed 292 293lemma in_these_eq: "x \<in> these A \<longleftrightarrow> Some x \<in> A" 294proof 295 assume "Some x \<in> A" 296 then obtain B where "A = insert (Some x) B" by auto 297 then show "x \<in> these A" by (auto simp add: these_def intro!: image_eqI) 298next 299 assume "x \<in> these A" 300 then show "Some x \<in> A" by (auto simp add: these_def) 301qed 302 303lemma these_image_Some_eq [simp]: "these (Some ` A) = A" 304 by (auto simp add: these_def intro!: image_eqI) 305 306lemma Some_image_these_eq: "Some ` these A = {x\<in>A. x \<noteq> None}" 307 by (auto simp add: these_def image_image intro!: image_eqI) 308 309lemma these_empty_eq: "these B = {} \<longleftrightarrow> B = {} \<or> B = {None}" 310 by (auto simp add: these_def) 311 312lemma these_not_empty_eq: "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}" 313 by (auto simp add: these_empty_eq) 314 315end 316 317lemma finite_range_Some: "finite (range (Some :: 'a \<Rightarrow> 'a option)) = finite (UNIV :: 'a set)" 318 by (auto dest: finite_imageD intro: inj_Some) 319 320 321subsection \<open>Transfer rules for the Transfer package\<close> 322 323context includes lifting_syntax 324begin 325 326lemma option_bind_transfer [transfer_rule]: 327 "(rel_option A ===> (A ===> rel_option B) ===> rel_option B) 328 Option.bind Option.bind" 329 unfolding rel_fun_def split_option_all by simp 330 331lemma pred_option_parametric [transfer_rule]: 332 "((A ===> (=)) ===> rel_option A ===> (=)) pred_option pred_option" 333 by (rule rel_funI)+ (auto simp add: rel_option_unfold Option.is_none_def dest: rel_funD) 334 335end 336 337 338subsubsection \<open>Interaction with finite sets\<close> 339 340lemma finite_option_UNIV [simp]: 341 "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)" 342 by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some) 343 344instance option :: (finite) finite 345 by standard (simp add: UNIV_option_conv) 346 347 348subsubsection \<open>Code generator setup\<close> 349 350lemma equal_None_code_unfold [code_unfold]: 351 "HOL.equal x None \<longleftrightarrow> Option.is_none x" 352 "HOL.equal None = Option.is_none" 353 by (auto simp add: equal Option.is_none_def) 354 355code_printing 356 type_constructor option \<rightharpoonup> 357 (SML) "_ option" 358 and (OCaml) "_ option" 359 and (Haskell) "Maybe _" 360 and (Scala) "!Option[(_)]" 361| constant None \<rightharpoonup> 362 (SML) "NONE" 363 and (OCaml) "None" 364 and (Haskell) "Nothing" 365 and (Scala) "!None" 366| constant Some \<rightharpoonup> 367 (SML) "SOME" 368 and (OCaml) "Some _" 369 and (Haskell) "Just" 370 and (Scala) "Some" 371| class_instance option :: equal \<rightharpoonup> 372 (Haskell) - 373| constant "HOL.equal :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" \<rightharpoonup> 374 (Haskell) infix 4 "==" 375 376code_reserved SML 377 option NONE SOME 378 379code_reserved OCaml 380 option None Some 381 382code_reserved Scala 383 Option None Some 384 385end 386