# HG changeset patch
# User haftmann
# Date 1242306587 -7200
# Node ID f919b8e67413d5dc9060e17830c00f1285b99f0b
# Parent  6b31b143f18b3bd6c44326d7ea68fcd100a24800
preprocessing must consider eq

diff -r 6b31b143f18b -r f919b8e67413 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 14 15:09:46 2009 +0200
+++ b/src/HOL/List.thy	Thu May 14 15:09:47 2009 +0200
@@ -3646,10 +3646,14 @@
 
 lemmas in_set_code [code unfold] = mem_iff [symmetric]
 
-lemma empty_null [code inline]:
+lemma empty_null:
   "xs = [] \<longleftrightarrow> null xs"
 by (cases xs) simp_all
 
+lemma [code inline]:
+  "eq_class.eq xs [] \<longleftrightarrow> null xs"
+by (simp add: eq empty_null)
+
 lemmas null_empty [code post] =
   empty_null [symmetric]
 
diff -r 6b31b143f18b -r f919b8e67413 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Thu May 14 15:09:46 2009 +0200
+++ b/src/HOL/Option.thy	Thu May 14 15:09:47 2009 +0200
@@ -63,10 +63,8 @@
 lemma set_empty_eq [simp]: "(set xo = {}) = (xo = None)"
   by (cases xo) auto
 
-definition
-  map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
-where
-  [code del]: "map = (%f y. case y of None => None | Some x => Some (f x))"
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option" where
+  "map = (%f y. case y of None => None | Some x => Some (f x))"
 
 lemma option_map_None [simp, code]: "map f None = None"
   by (simp add: map_def)
@@ -95,14 +93,21 @@
 
 subsubsection {* Code generator setup *}
 
-definition
-  is_none :: "'a option \<Rightarrow> bool" where
-  is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
+definition is_none :: "'a option \<Rightarrow> bool" where
+  [code post]: "is_none x \<longleftrightarrow> x = None"
 
 lemma is_none_code [code]:
   shows "is_none None \<longleftrightarrow> True"
     and "is_none (Some x) \<longleftrightarrow> False"
-  unfolding is_none_none [symmetric] by simp_all
+  unfolding is_none_def by simp_all
+
+lemma is_none_none:
+  "is_none x \<longleftrightarrow> x = None"
+  by (simp add: is_none_def)
+
+lemma [code inline]:
+  "eq_class.eq x None \<longleftrightarrow> is_none x"
+  by (simp add: eq is_none_none)
 
 hide (open) const is_none