src/HOL/List.ML
changeset 6794 ac367328b875
parent 6451 bc943acc5fda
child 6813 bf90f86502b2
     1.1 --- a/src/HOL/List.ML	Sat Jun 05 21:43:02 1999 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Jun 07 19:25:12 1999 +0200
     1.3 @@ -1026,6 +1026,55 @@
     1.4  (** replicate **)
     1.5  section "replicate";
     1.6  
     1.7 +Goal "length(replicate n x) = n";
     1.8 +by(induct_tac "n" 1);
     1.9 +by(Auto_tac);
    1.10 +qed "length_replicate";
    1.11 +Addsimps [length_replicate];
    1.12 +
    1.13 +Goal "map f (replicate n x) = replicate n (f x)";
    1.14 +by (induct_tac "n" 1);
    1.15 +by(Auto_tac);
    1.16 +qed "map_replicate";
    1.17 +Addsimps [map_replicate];
    1.18 +
    1.19 +Goal "(replicate n x) @ (x#xs) = x # replicate n x @ xs";
    1.20 +by (induct_tac "n" 1);
    1.21 +by(Auto_tac);
    1.22 +qed "replicate_app_Cons_same";
    1.23 +
    1.24 +Goal "rev(replicate n x) = replicate n x";
    1.25 +by (induct_tac "n" 1);
    1.26 + by(Simp_tac 1);
    1.27 +by (asm_simp_tac (simpset() addsimps [replicate_app_Cons_same]) 1);
    1.28 +qed "rev_replicate";
    1.29 +Addsimps [rev_replicate];
    1.30 +
    1.31 +Goal"n ~= 0 --> hd(replicate n x) = x";
    1.32 +by (induct_tac "n" 1);
    1.33 +by(Auto_tac);
    1.34 +qed_spec_mp "hd_replicate";
    1.35 +Addsimps [hd_replicate];
    1.36 +
    1.37 +Goal "n ~= 0 --> tl(replicate n x) = replicate (n-1) x";
    1.38 +by (induct_tac "n" 1);
    1.39 +by(Auto_tac);
    1.40 +qed_spec_mp "tl_replicate";
    1.41 +Addsimps [tl_replicate];
    1.42 +
    1.43 +Goal "n ~= 0 --> last(replicate n x) = x";
    1.44 +by (induct_tac "n" 1);
    1.45 +by(Auto_tac);
    1.46 +qed_spec_mp "last_replicate";
    1.47 +Addsimps [last_replicate];
    1.48 +
    1.49 +Goal "!i. i<n --> (replicate n x)!i = x";
    1.50 +by(induct_tac "n" 1);
    1.51 + by(Simp_tac 1);
    1.52 +by(asm_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
    1.53 +qed_spec_mp "nth_replicate";
    1.54 +Addsimps [nth_replicate];
    1.55 +
    1.56  Goal "set(replicate (Suc n) x) = {x}";
    1.57  by (induct_tac "n" 1);
    1.58  by Auto_tac;
    1.59 @@ -1036,6 +1085,10 @@
    1.60  qed "set_replicate";
    1.61  Addsimps [set_replicate];
    1.62  
    1.63 +Goal "replicate (n+m) x = replicate n x @ replicate m x";
    1.64 +by (induct_tac "n" 1);
    1.65 +by Auto_tac;
    1.66 +qed "replicate_add";
    1.67  
    1.68  (*** Lexcicographic orderings on lists ***)
    1.69  section"Lexcicographic orderings on lists";