# HG changeset patch
# User nipkow
# Date 867665299 -7200
# Node ID a0797ba03dfe7f662db3514881558afaf9bf6e07
# Parent  30791e5a69c4c15033cfd9557d4c6f78e2cadc0d
More concat lemmas.

diff -r 30791e5a69c4 -r a0797ba03dfe src/HOL/List.ML
--- 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);