src/HOL/List.ML
changeset 11336 fedccaeb5267
parent 11289 65782388cf40
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/List.ML	Thu May 31 16:17:28 2001 +0200
     1.2 +++ b/src/HOL/List.ML	Thu May 31 16:50:04 2001 +0200
     1.3 @@ -1125,7 +1125,19 @@
     1.4  by (force_tac (claset(), simpset() addsimps [set_zip]) 1);
     1.5  qed "list_all2_conv_all_nth";
     1.6  
     1.7 -(** foldl **)
     1.8 +Goal "ALL a b c. P1 a b --> P2 b c --> P3 a c ==> \
     1.9 +\ ALL bs cs. list_all2 P1 as bs --> list_all2 P2 bs cs --> list_all2 P3 as cs";
    1.10 +by (induct_tac "as" 1);
    1.11 +by  (Simp_tac 1);
    1.12 +by (rtac allI 1);
    1.13 +by (induct_tac "bs" 1);
    1.14 +by  (Simp_tac 1);
    1.15 +by (rtac allI 1);
    1.16 +by (induct_tac "cs" 1);
    1.17 +by Auto_tac;
    1.18 +qed_spec_mp "list_all2_trans";
    1.19 +
    1.20 +
    1.21  section "foldl";
    1.22  
    1.23  Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";