improved code lemmas

--- a/src/HOL/Datatype.thy	Tue Jun 06 14:55:56 2006 +0200
+++ b/src/HOL/Datatype.thy	Tue Jun 06 14:56:42 2006 +0200
@@ -218,6 +218,17 @@
   apply (simp split add: sum.split)
   done
 
+
+consts
+  is_none :: "'a option \<Rightarrow> bool"
+primrec
+  "is_none None = True"
+  "is_none (Some x) = False"
+
+(* lemma is_none_none [code unfolt]:
+  "(x = None) = (is_none x)" 
+by (cases "x") simp_all *)
+
 lemmas [code] = imp_conv_disj
 
 subsubsection {* Codegenerator setup *}

--- a/src/HOL/List.thy	Tue Jun 06 14:55:56 2006 +0200
+++ b/src/HOL/List.thy	Tue Jun 06 14:56:42 2006 +0200
@@ -270,6 +270,9 @@
 lemma null_empty: "null xs = (xs = [])"
   by (cases xs) simp_all
 
+(*lemma empty_null [code unfolt]:
+  "(xs = []) = null xs"
+using null_empty [symmetric] .*)
 
 subsubsection {* @{text length} *}
 
@@ -1086,19 +1089,6 @@
 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
 by(induct xs)(auto simp:neq_Nil_conv)
 
-lemma last_code [code]:
-  "last (x # xs) = (if null xs then x else last xs)"
-by (cases xs) simp_all
-
-declare last.simps [code del]
-
-lemma butlast_code [code]:
-  "butlast [] = []"
-  "butlast (x # xs) = (if null xs then [] else x # butlast xs)"
-by (simp, cases xs) simp_all
-
-declare butlast.simps [code del]
-
 subsubsection {* @{text take} and @{text drop} *}
 
 lemma take_0 [simp]: "take 0 xs = []"
@@ -1461,17 +1451,11 @@
   "list_all2 P xs ys ==> length xs = length ys"
   by (simp add: list_all2_def)
 
-lemma list_all2_Nil [iff]: "list_all2 P [] ys = (ys = [])"
-  by (simp add: list_all2_def)
-
-lemma list_all2_Nil2 [iff]: "list_all2 P xs [] = (xs = [])"
+lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
   by (simp add: list_all2_def)
 
-lemma list_all2_Nil_code [code]: "list_all2 P [] ys = null ys"
-  unfolding null_empty by simp
-
-lemma list_all2_Nil2_code [code]: "list_all2 P xs [] = null xs"
-  unfolding null_empty by simp
+lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
+  by (simp add: list_all2_def)
 
 lemma list_all2_Cons [iff, code]:
   "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
@@ -2750,7 +2734,7 @@
 
 code_alias
   "List.op @" "List.append"
-  "List.op mem" "List.member"
+  "List.op mem" "List.mem"
 
 code_generate Nil Cons