--- 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