# HG changeset patch
# User nipkow
# Date 1077237179 -3600
# Node ID 4201e19164820e38c6af810f4eb4710978b1e079
# Parent  477380c74c1d2b8f8e5db4e9793147170b29d593
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy

diff -r 477380c74c1d -r 4201e1916482 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Feb 19 18:24:08 2004 +0100
+++ b/src/HOL/List.thy	Fri Feb 20 01:32:59 2004 +0100
@@ -510,6 +510,9 @@
 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
 by (induct xs, auto)
 
+lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
+by (induct xs) auto
+
 subsection {* @{text rev} *}
 
 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
@@ -681,6 +684,12 @@
 apply (case_tac n, auto)
 done
 
+lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
+by (induct "xs") auto
+
+lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
+by (induct "xs") auto
+
 lemma nth_map [simp]: "!!n. n < length xs ==> (map f xs)!n = f(xs!n)"
 apply (induct xs, simp)
 apply (case_tac n, auto)
@@ -730,7 +739,7 @@
 "!!i. i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]"
 by (induct xs) (auto split: nat.split)
 
-lemma list_update_id[simp]: "!!i. i < length xs \<Longrightarrow> xs[i := xs!i] = xs"
+lemma list_update_id[simp]: "!!i. i < length xs ==> xs[i := xs!i] = xs"
 apply (induct xs, simp)
 apply(simp split:nat.splits)
 done
@@ -745,6 +754,10 @@
 apply(simp split:nat.split)
 done
 
+lemma list_update_length [simp]:
+ "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
+by (induct xs, auto)
+
 lemma update_zip:
 "!!i xy xs. length xs = length ys ==>
 (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
@@ -1187,12 +1200,21 @@
   done
 
 
-subsection {* @{text foldl} *}
+subsection {* @{text foldl} and @{text foldr} *}
 
 lemma foldl_append [simp]:
 "!!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
 by (induct xs) auto
 
+lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
+by (induct xs) auto
+
+lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
+by (induct xs) auto
+
+lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
+by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
+
 text {*
 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
 difficult to use because it requires an additional transitivity step.
diff -r 477380c74c1d -r 4201e1916482 src/HOL/MicroJava/Comp/AuxLemmas.thy
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Thu Feb 19 18:24:08 2004 +0100
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Fri Feb 20 01:32:59 2004 +0100
@@ -15,21 +15,6 @@
 
 
 
-lemma foldr_foldl: "foldr f xs a = foldl (\<lambda> x y. (f y x)) a (rev xs)"
-by (induct xs, simp, simp)
-
-lemma foldl_foldr: "foldl f a xs = foldr (\<lambda> x y. (f y x)) (rev xs) a"
-by (simp add: foldr_foldl [of "(\<lambda> x y. (f y x))" "(rev xs)"])
-
-lemma foldr_append: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
-by (induct xs, auto)
-
-lemma app_nth_len [simp]: "(pre @ a # post) ! length pre = a"
-by (induct "pre") auto
-
-lemma app_nth_len_plus [simp]: "(pre @ post) ! ((length pre) + n) = post ! n"
-by (induct "pre") auto
-
 lemma app_nth_greater_len [rule_format (no_asm), simp]:
  "\<forall> ind. length pre \<le> ind \<longrightarrow> (pre @ a # post) ! (Suc ind) = (pre @ post) ! ind"
 apply (induct "pre")
@@ -38,10 +23,6 @@
 apply auto
 done
 
-lemma list_update_length [simp]: "(xs @ a# ys)[length xs := b] = (xs @ b# ys)"
-by (induct xs, auto)
-
-
 lemma length_takeWhile: "v \<in> set xs \<Longrightarrow> length (takeWhile (%z. z~=v) xs) < length xs"
 by (induct xs, auto)
 
@@ -50,9 +31,6 @@
 by (induct xs, auto)
 
 
-lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
-by (induct xs, auto)
-
 lemma map_list_update [simp]:
   "\<lbrakk> x \<in> set xs; distinct xs\<rbrakk> \<Longrightarrow> 
   (map f xs) [length (takeWhile (\<lambda>z. z \<noteq> x) xs) := v] =