summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 20 Feb 2004 01:32:59 +0100 | |

changeset 14402 | 4201e1916482 |

parent 14401 | 477380c74c1d |

child 14403 | 32d1526d3237 |

moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy

src/HOL/List.thy | file | annotate | diff | comparison | revisions | |

src/HOL/MicroJava/Comp/AuxLemmas.thy | file | annotate | diff | comparison | revisions |

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

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