More concat lemmas.
--- a/src/HOL/List.ML Fri Jun 27 10:47:13 1997 +0200
+++ b/src/HOL/List.ML Mon Jun 30 12:08:19 1997 +0200
@@ -52,6 +52,8 @@
(** @ - append **)
+section "@ - append";
+
goal thy "(xs@ys)@zs = xs@(ys@zs)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
@@ -111,6 +113,8 @@
(** map **)
+section "map";
+
goal thy
"(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
by (induct_tac "xs" 1);
@@ -143,6 +147,8 @@
(** rev **)
+section "rev";
+
goal thy "rev(xs@ys) = rev(ys) @ rev(xs)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
@@ -158,6 +164,8 @@
(** mem **)
+section "mem";
+
goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
by (induct_tac "xs" 1);
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
@@ -172,6 +180,8 @@
(** set **)
+section "set";
+
goal thy "set (xs@ys) = (set xs Un set ys)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
@@ -210,6 +220,8 @@
(** list_all **)
+section "list_all";
+
goal thy "list_all (%x.True) xs = True";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
@@ -231,6 +243,8 @@
(** filter **)
+section "filter";
+
goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
by (induct_tac "xs" 1);
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
@@ -245,19 +259,39 @@
(** concat **)
+section "concat";
+
goal thy "concat(xs@ys) = concat(xs)@concat(ys)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed"concat_append";
Addsimps [concat_append];
-goal thy "rev(concat ls) = concat (map rev (rev ls))";
-by (induct_tac "ls" 1);
+goal thy "set(concat xs) = Union(set `` set xs)";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed"set_of_list_concat";
+Addsimps [set_of_list_concat];
+
+goal thy "map f (concat xs) = concat (map (map f) xs)";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "map_concat";
+
+goal thy "filter p (concat xs) = concat (map (filter p) xs)";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed"filter_concat";
+
+goal thy "rev(concat xs) = concat (map rev (rev xs))";
+by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "rev_concat";
(** length **)
+section "length";
+
goal thy "length(xs@ys) = length(xs)+length(ys)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
@@ -291,6 +325,8 @@
(** nth **)
+section "nth";
+
goal thy
"!xs. nth n (xs@ys) = \
\ (if n < length xs then nth n xs else nth (n - length xs) ys)";
@@ -482,6 +518,8 @@
(** takeWhile & dropWhile **)
+section "takeWhile & dropWhile";
+
goal thy
"x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
by (induct_tac "xs" 1);