add lemmas about functions on option
authorAndreas Lochbihler
Wed Feb 11 14:45:10 2015 +0100 (2015-02-11)
changeset 595220c5c5ad5d2e0
parent 59521 ef8ac8d2315e
child 59523 860fb1c65553
add lemmas about functions on option
src/HOL/Option.thy
     1.1 --- a/src/HOL/Option.thy	Wed Feb 11 14:19:46 2015 +0100
     1.2 +++ b/src/HOL/Option.thy	Wed Feb 11 14:45:10 2015 +0100
     1.3 @@ -62,6 +62,21 @@
     1.4  lemma UNIV_option_conv: "UNIV = insert None (range Some)"
     1.5  by(auto intro: classical)
     1.6  
     1.7 +lemma rel_option_None1 [simp]: "rel_option P None x \<longleftrightarrow> x = None"
     1.8 +by(cases x) simp_all
     1.9 +
    1.10 +lemma rel_option_None2 [simp]: "rel_option P x None \<longleftrightarrow> x = None"
    1.11 +by(cases x) simp_all
    1.12 +
    1.13 +lemma rel_option_inf: "inf (rel_option A) (rel_option B) = rel_option (inf A B)" (is "?lhs = ?rhs")
    1.14 +proof(rule antisym)
    1.15 +  show "?lhs \<le> ?rhs" by(auto elim!: option.rel_cases)
    1.16 +qed(auto elim: option.rel_mono_strong)
    1.17 +
    1.18 +lemma rel_option_reflI:
    1.19 +  "(\<And>x. x \<in> set_option y \<Longrightarrow> P x x) \<Longrightarrow> rel_option P y y"
    1.20 +by(cases y) auto
    1.21 +
    1.22  subsubsection {* Operations *}
    1.23  
    1.24  lemma ospec [dest]: "(ALL x:set_option A. P x) ==> A = Some x ==> P x"
    1.25 @@ -106,10 +121,43 @@
    1.26      | _ \<Rightarrow> False)"
    1.27  by (auto split: prod.split option.split)
    1.28  
    1.29 +definition is_none :: "'a option \<Rightarrow> bool"
    1.30 +where [code_post]: "is_none x \<longleftrightarrow> x = None"
    1.31 +
    1.32 +lemma is_none_simps [simp]:
    1.33 +  "is_none None"
    1.34 +  "\<not> is_none (Some x)"
    1.35 +by(simp_all add: is_none_def)
    1.36 +
    1.37 +lemma is_none_code [code]:
    1.38 +  "is_none None = True"
    1.39 +  "is_none (Some x) = False"
    1.40 +by simp_all
    1.41 +
    1.42 +lemma rel_option_unfold:
    1.43 +  "rel_option R x y \<longleftrightarrow>
    1.44 +   (is_none x \<longleftrightarrow> is_none y) \<and> (\<not> is_none x \<longrightarrow> \<not> is_none y \<longrightarrow> R (the x) (the y))"
    1.45 +by(simp add: rel_option_iff split: option.split)
    1.46 +
    1.47 +lemma rel_optionI:
    1.48 +  "\<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>
    1.49 +  \<Longrightarrow> rel_option P x y"
    1.50 +by(simp add: rel_option_unfold)
    1.51 +
    1.52 +lemma is_none_map_option [simp]: "is_none (map_option f x) \<longleftrightarrow> is_none x"
    1.53 +by(simp add: is_none_def)
    1.54 +
    1.55 +lemma the_map_option: "\<not> is_none x \<Longrightarrow> the (map_option f x) = f (the x)"
    1.56 +by(clarsimp simp add: is_none_def)
    1.57 +
    1.58 +
    1.59  primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
    1.60  bind_lzero: "bind None f = None" |
    1.61  bind_lunit: "bind (Some x) f = f x"
    1.62  
    1.63 +lemma is_none_bind: "is_none (bind f g) \<longleftrightarrow> is_none f \<or> is_none (g (the f))"
    1.64 +by(cases f) simp_all
    1.65 +
    1.66  lemma bind_runit[simp]: "bind x Some = x"
    1.67  by (cases x) auto
    1.68  
    1.69 @@ -133,6 +181,24 @@
    1.70  
    1.71  lemmas bind_splits = bind_split bind_split_asm
    1.72  
    1.73 +lemma bind_eq_Some_conv: "bind f g = Some x \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
    1.74 +by(cases f) simp_all
    1.75 +
    1.76 +lemma map_option_bind: "map_option f (bind x g) = bind x (map_option f \<circ> g)"
    1.77 +by(cases x) simp_all
    1.78 +
    1.79 +lemma bind_option_cong:
    1.80 +  "\<lbrakk> x = y; \<And>z. z \<in> set_option y \<Longrightarrow> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g"
    1.81 +by(cases y) simp_all
    1.82 +
    1.83 +lemma bind_option_cong_simp:
    1.84 +  "\<lbrakk> x = y; \<And>z. z \<in> set_option y =simp=> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g"
    1.85 +unfolding simp_implies_def by(rule bind_option_cong)
    1.86 +
    1.87 +lemma bind_option_cong_code: "x = y \<Longrightarrow> bind x f = bind y f" by simp
    1.88 +setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})\<close>
    1.89 +
    1.90 +
    1.91  definition these :: "'a option set \<Rightarrow> 'a set"
    1.92  where
    1.93    "these A = the ` {x \<in> A. x \<noteq> None}"
    1.94 @@ -210,15 +276,7 @@
    1.95  
    1.96  subsubsection {* Code generator setup *}
    1.97  
    1.98 -definition is_none :: "'a option \<Rightarrow> bool" where
    1.99 -  [code_post]: "is_none x \<longleftrightarrow> x = None"
   1.100 -
   1.101 -lemma is_none_code [code]:
   1.102 -  shows "is_none None \<longleftrightarrow> True"
   1.103 -    and "is_none (Some x) \<longleftrightarrow> False"
   1.104 -  unfolding is_none_def by simp_all
   1.105 -
   1.106 -lemma [code_unfold]:
   1.107 +lemma equal_None_code_unfold [code_unfold]:
   1.108    "HOL.equal x None \<longleftrightarrow> is_none x"
   1.109    "HOL.equal None = is_none"
   1.110    by (auto simp add: equal is_none_def)