13 (* List.thy *) |
13 (* List.thy *) |
14 (**********************************************************************) |
14 (**********************************************************************) |
15 |
15 |
16 |
16 |
17 |
17 |
18 lemma foldr_foldl: "foldr f xs a = foldl (\<lambda> x y. (f y x)) a (rev xs)" |
|
19 by (induct xs, simp, simp) |
|
20 |
|
21 lemma foldl_foldr: "foldl f a xs = foldr (\<lambda> x y. (f y x)) (rev xs) a" |
|
22 by (simp add: foldr_foldl [of "(\<lambda> x y. (f y x))" "(rev xs)"]) |
|
23 |
|
24 lemma foldr_append: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)" |
|
25 by (induct xs, auto) |
|
26 |
|
27 lemma app_nth_len [simp]: "(pre @ a # post) ! length pre = a" |
|
28 by (induct "pre") auto |
|
29 |
|
30 lemma app_nth_len_plus [simp]: "(pre @ post) ! ((length pre) + n) = post ! n" |
|
31 by (induct "pre") auto |
|
32 |
|
33 lemma app_nth_greater_len [rule_format (no_asm), simp]: |
18 lemma app_nth_greater_len [rule_format (no_asm), simp]: |
34 "\<forall> ind. length pre \<le> ind \<longrightarrow> (pre @ a # post) ! (Suc ind) = (pre @ post) ! ind" |
19 "\<forall> ind. length pre \<le> ind \<longrightarrow> (pre @ a # post) ! (Suc ind) = (pre @ post) ! ind" |
35 apply (induct "pre") |
20 apply (induct "pre") |
36 apply auto |
21 apply auto |
37 apply (case_tac ind) |
22 apply (case_tac ind) |
38 apply auto |
23 apply auto |
39 done |
24 done |
40 |
25 |
41 lemma list_update_length [simp]: "(xs @ a# ys)[length xs := b] = (xs @ b# ys)" |
|
42 by (induct xs, auto) |
|
43 |
|
44 |
|
45 lemma length_takeWhile: "v \<in> set xs \<Longrightarrow> length (takeWhile (%z. z~=v) xs) < length xs" |
26 lemma length_takeWhile: "v \<in> set xs \<Longrightarrow> length (takeWhile (%z. z~=v) xs) < length xs" |
46 by (induct xs, auto) |
27 by (induct xs, auto) |
47 |
28 |
48 lemma nth_length_takeWhile [simp]: |
29 lemma nth_length_takeWhile [simp]: |
49 "v \<in> set xs \<Longrightarrow> xs ! (length (takeWhile (%z. z~=v) xs)) = v" |
30 "v \<in> set xs \<Longrightarrow> xs ! (length (takeWhile (%z. z~=v) xs)) = v" |
50 by (induct xs, auto) |
31 by (induct xs, auto) |
51 |
32 |
52 |
|
53 lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs" |
|
54 by (induct xs, auto) |
|
55 |
33 |
56 lemma map_list_update [simp]: |
34 lemma map_list_update [simp]: |
57 "\<lbrakk> x \<in> set xs; distinct xs\<rbrakk> \<Longrightarrow> |
35 "\<lbrakk> x \<in> set xs; distinct xs\<rbrakk> \<Longrightarrow> |
58 (map f xs) [length (takeWhile (\<lambda>z. z \<noteq> x) xs) := v] = |
36 (map f xs) [length (takeWhile (\<lambda>z. z \<noteq> x) xs) := v] = |
59 map (f(x:=v)) xs" |
37 map (f(x:=v)) xs" |