src/HOL/List.thy

--- a/src/HOL/List.thy	Mon May 21 19:11:38 2007 +0200
+++ b/src/HOL/List.thy	Mon May 21 19:11:39 2007 +0200
@@ -2728,7 +2728,6 @@
   list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
   list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
-  itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
   map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
 
@@ -2764,10 +2763,6 @@
   "map_filter f P (x#xs) =
      (if P x then f x # map_filter f P xs else map_filter f P xs)"
 
-primrec
-  "itrev [] ys = ys"
-  "itrev (x#xs) ys = itrev xs (x#ys)"
-
 text {*
   Only use @{text mem} for generating executable code.  Otherwise use
   @{prop "x : set xs"} instead --- it is much easier to reason about.
@@ -2780,11 +2775,27 @@
 
   Efficient emptyness check is implemented by @{const null}.
 
-  The functions @{const itrev}, @{const filtermap} and @{const
-  map_filter} are just there to generate efficient code. Do not use
+  The functions @{const filtermap} and @{const map_filter} are just
+  there to generate efficient code. Do not use
   them for modelling and proving.
 *}
 
+lemma rev_foldl_cons [code]:
+  "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
+proof (induct xs)
+  case Nil then show ?case by simp
+next
+  case Cons
+  {
+    fix x xs ys
+    have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
+      = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
+    by (induct xs arbitrary: ys) auto
+  }
+  note aux = this
+  show ?case by (induct xs) (auto simp add: Cons aux)
+qed
+
 lemma mem_iff [normal post]:
   "x mem xs \<longleftrightarrow> x \<in> set xs"
   by (induct xs) auto
@@ -2831,10 +2842,6 @@
   "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
   unfolding list_ex_iff set_conv_nth by auto
 
-lemma itrev [simp]:
-  "itrev xs ys = rev xs @ ys"
-  by (induct xs arbitrary: ys) simp_all
-
 lemma filtermap_conv:
    "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
   by (induct xs) (simp_all split: option.split) 
@@ -2843,10 +2850,6 @@
   "map_filter f P xs = map f (filter P xs)"
   by (induct xs) auto
 
-lemma rev_code [code func]:
-  "rev xs = itrev xs []"
-  by simp
-
 
 text {* code for bounded quantification over nats *}