src/HOL/Option.thy
changeset 31154 f919b8e67413
parent 31080 21ffc770ebc0
child 31998 2c7a24f74db9
     1.1 --- a/src/HOL/Option.thy	Thu May 14 15:09:46 2009 +0200
     1.2 +++ b/src/HOL/Option.thy	Thu May 14 15:09:47 2009 +0200
     1.3 @@ -63,10 +63,8 @@
     1.4  lemma set_empty_eq [simp]: "(set xo = {}) = (xo = None)"
     1.5    by (cases xo) auto
     1.6  
     1.7 -definition
     1.8 -  map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
     1.9 -where
    1.10 -  [code del]: "map = (%f y. case y of None => None | Some x => Some (f x))"
    1.11 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option" where
    1.12 +  "map = (%f y. case y of None => None | Some x => Some (f x))"
    1.13  
    1.14  lemma option_map_None [simp, code]: "map f None = None"
    1.15    by (simp add: map_def)
    1.16 @@ -95,14 +93,21 @@
    1.17  
    1.18  subsubsection {* Code generator setup *}
    1.19  
    1.20 -definition
    1.21 -  is_none :: "'a option \<Rightarrow> bool" where
    1.22 -  is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
    1.23 +definition is_none :: "'a option \<Rightarrow> bool" where
    1.24 +  [code post]: "is_none x \<longleftrightarrow> x = None"
    1.25  
    1.26  lemma is_none_code [code]:
    1.27    shows "is_none None \<longleftrightarrow> True"
    1.28      and "is_none (Some x) \<longleftrightarrow> False"
    1.29 -  unfolding is_none_none [symmetric] by simp_all
    1.30 +  unfolding is_none_def by simp_all
    1.31 +
    1.32 +lemma is_none_none:
    1.33 +  "is_none x \<longleftrightarrow> x = None"
    1.34 +  by (simp add: is_none_def)
    1.35 +
    1.36 +lemma [code inline]:
    1.37 +  "eq_class.eq x None \<longleftrightarrow> is_none x"
    1.38 +  by (simp add: eq is_none_none)
    1.39  
    1.40  hide (open) const is_none
    1.41