src/HOL/List.ML
changeset 3467 a0797ba03dfe
parent 3465 e85c24717cad
child 3468 1f972dc8eafb
     1.1 --- a/src/HOL/List.ML	Fri Jun 27 10:47:13 1997 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Jun 30 12:08:19 1997 +0200
     1.3 @@ -52,6 +52,8 @@
     1.4  
     1.5  (** @ - append **)
     1.6  
     1.7 +section "@ - append";
     1.8 +
     1.9  goal thy "(xs@ys)@zs = xs@(ys@zs)";
    1.10  by (induct_tac "xs" 1);
    1.11  by (ALLGOALS Asm_simp_tac);
    1.12 @@ -111,6 +113,8 @@
    1.13  
    1.14  (** map **)
    1.15  
    1.16 +section "map";
    1.17 +
    1.18  goal thy
    1.19    "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
    1.20  by (induct_tac "xs" 1);
    1.21 @@ -143,6 +147,8 @@
    1.22  
    1.23  (** rev **)
    1.24  
    1.25 +section "rev";
    1.26 +
    1.27  goal thy "rev(xs@ys) = rev(ys) @ rev(xs)";
    1.28  by (induct_tac "xs" 1);
    1.29  by (ALLGOALS Asm_simp_tac);
    1.30 @@ -158,6 +164,8 @@
    1.31  
    1.32  (** mem **)
    1.33  
    1.34 +section "mem";
    1.35 +
    1.36  goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
    1.37  by (induct_tac "xs" 1);
    1.38  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    1.39 @@ -172,6 +180,8 @@
    1.40  
    1.41  (** set **)
    1.42  
    1.43 +section "set";
    1.44 +
    1.45  goal thy "set (xs@ys) = (set xs Un set ys)";
    1.46  by (induct_tac "xs" 1);
    1.47  by (ALLGOALS Asm_simp_tac);
    1.48 @@ -210,6 +220,8 @@
    1.49  
    1.50  (** list_all **)
    1.51  
    1.52 +section "list_all";
    1.53 +
    1.54  goal thy "list_all (%x.True) xs = True";
    1.55  by (induct_tac "xs" 1);
    1.56  by (ALLGOALS Asm_simp_tac);
    1.57 @@ -231,6 +243,8 @@
    1.58  
    1.59  (** filter **)
    1.60  
    1.61 +section "filter";
    1.62 +
    1.63  goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
    1.64  by (induct_tac "xs" 1);
    1.65   by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    1.66 @@ -245,19 +259,39 @@
    1.67  
    1.68  (** concat **)
    1.69  
    1.70 +section "concat";
    1.71 +
    1.72  goal thy  "concat(xs@ys) = concat(xs)@concat(ys)";
    1.73  by (induct_tac "xs" 1);
    1.74  by (ALLGOALS Asm_simp_tac);
    1.75  qed"concat_append";
    1.76  Addsimps [concat_append];
    1.77  
    1.78 -goal thy "rev(concat ls) = concat (map rev (rev ls))";
    1.79 -by (induct_tac "ls" 1);
    1.80 +goal thy  "set(concat xs) = Union(set `` set xs)";
    1.81 +by (induct_tac "xs" 1);
    1.82 +by (ALLGOALS Asm_simp_tac);
    1.83 +qed"set_of_list_concat";
    1.84 +Addsimps [set_of_list_concat];
    1.85 +
    1.86 +goal thy "map f (concat xs) = concat (map (map f) xs)"; 
    1.87 +by (induct_tac "xs" 1);
    1.88 +by (ALLGOALS Asm_simp_tac);
    1.89 +qed "map_concat";
    1.90 +
    1.91 +goal thy "filter p (concat xs) = concat (map (filter p) xs)"; 
    1.92 +by (induct_tac "xs" 1);
    1.93 +by (ALLGOALS Asm_simp_tac);
    1.94 +qed"filter_concat"; 
    1.95 +
    1.96 +goal thy "rev(concat xs) = concat (map rev (rev xs))";
    1.97 +by (induct_tac "xs" 1);
    1.98  by (ALLGOALS Asm_simp_tac);
    1.99  qed "rev_concat";
   1.100  
   1.101  (** length **)
   1.102  
   1.103 +section "length";
   1.104 +
   1.105  goal thy "length(xs@ys) = length(xs)+length(ys)";
   1.106  by (induct_tac "xs" 1);
   1.107  by (ALLGOALS Asm_simp_tac);
   1.108 @@ -291,6 +325,8 @@
   1.109  
   1.110  (** nth **)
   1.111  
   1.112 +section "nth";
   1.113 +
   1.114  goal thy
   1.115    "!xs. nth n (xs@ys) = \
   1.116  \          (if n < length xs then nth n xs else nth (n - length xs) ys)";
   1.117 @@ -482,6 +518,8 @@
   1.118  
   1.119  (** takeWhile & dropWhile **)
   1.120  
   1.121 +section "takeWhile & dropWhile";
   1.122 +
   1.123  goal thy
   1.124    "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
   1.125  by (induct_tac "xs" 1);