preprocessing must consider eq
authorhaftmann
Thu May 14 15:09:47 2009 +0200 (2009-05-14)
changeset 31154f919b8e67413
parent 31153 6b31b143f18b
child 31155 92d8ff6af82c
preprocessing must consider eq
src/HOL/List.thy
src/HOL/Option.thy
     1.1 --- a/src/HOL/List.thy	Thu May 14 15:09:46 2009 +0200
     1.2 +++ b/src/HOL/List.thy	Thu May 14 15:09:47 2009 +0200
     1.3 @@ -3646,10 +3646,14 @@
     1.4  
     1.5  lemmas in_set_code [code unfold] = mem_iff [symmetric]
     1.6  
     1.7 -lemma empty_null [code inline]:
     1.8 +lemma empty_null:
     1.9    "xs = [] \<longleftrightarrow> null xs"
    1.10  by (cases xs) simp_all
    1.11  
    1.12 +lemma [code inline]:
    1.13 +  "eq_class.eq xs [] \<longleftrightarrow> null xs"
    1.14 +by (simp add: eq empty_null)
    1.15 +
    1.16  lemmas null_empty [code post] =
    1.17    empty_null [symmetric]
    1.18  
     2.1 --- a/src/HOL/Option.thy	Thu May 14 15:09:46 2009 +0200
     2.2 +++ b/src/HOL/Option.thy	Thu May 14 15:09:47 2009 +0200
     2.3 @@ -63,10 +63,8 @@
     2.4  lemma set_empty_eq [simp]: "(set xo = {}) = (xo = None)"
     2.5    by (cases xo) auto
     2.6  
     2.7 -definition
     2.8 -  map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
     2.9 -where
    2.10 -  [code del]: "map = (%f y. case y of None => None | Some x => Some (f x))"
    2.11 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option" where
    2.12 +  "map = (%f y. case y of None => None | Some x => Some (f x))"
    2.13  
    2.14  lemma option_map_None [simp, code]: "map f None = None"
    2.15    by (simp add: map_def)
    2.16 @@ -95,14 +93,21 @@
    2.17  
    2.18  subsubsection {* Code generator setup *}
    2.19  
    2.20 -definition
    2.21 -  is_none :: "'a option \<Rightarrow> bool" where
    2.22 -  is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
    2.23 +definition is_none :: "'a option \<Rightarrow> bool" where
    2.24 +  [code post]: "is_none x \<longleftrightarrow> x = None"
    2.25  
    2.26  lemma is_none_code [code]:
    2.27    shows "is_none None \<longleftrightarrow> True"
    2.28      and "is_none (Some x) \<longleftrightarrow> False"
    2.29 -  unfolding is_none_none [symmetric] by simp_all
    2.30 +  unfolding is_none_def by simp_all
    2.31 +
    2.32 +lemma is_none_none:
    2.33 +  "is_none x \<longleftrightarrow> x = None"
    2.34 +  by (simp add: is_none_def)
    2.35 +
    2.36 +lemma [code inline]:
    2.37 +  "eq_class.eq x None \<longleftrightarrow> is_none x"
    2.38 +  by (simp add: eq is_none_none)
    2.39  
    2.40  hide (open) const is_none
    2.41