src/HOL/List.ML
changeset 9003 3747ec2aeb86
parent 8982 4cb682fc083d
child 9014 4382883421ec
     1.1 --- a/src/HOL/List.ML	Wed May 31 11:55:21 2000 +0200
     1.2 +++ b/src/HOL/List.ML	Wed May 31 11:55:51 2000 +0200
     1.3 @@ -181,10 +181,7 @@
     1.4  by (Simp_tac 1);
     1.5  qed "append_same_eq";
     1.6  
     1.7 -AddSIs
     1.8 - [same_append_eq RS iffD2, append1_eq_conv RS iffD2, append_same_eq RS iffD2];
     1.9 -AddSDs
    1.10 - [same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1];
    1.11 +AddIffs [same_append_eq, append1_eq_conv, append_same_eq];
    1.12  
    1.13  Goal "(xs @ ys = ys) = (xs=[])";
    1.14  by (cut_inst_tac [("zs","[]")] append_same_eq 1);
    1.15 @@ -1188,6 +1185,12 @@
    1.16  by (Asm_simp_tac 1);
    1.17  qed "upt_conv_Cons";
    1.18  
    1.19 +(*LOOPS as a simprule, since j<=j*)
    1.20 +Goal "i<=j ==> [i..j+k(] = [i..j(]@[j..j+k(]";
    1.21 +by (induct_tac "k" 1);
    1.22 +by Auto_tac;
    1.23 +qed "upt_add_eq_append";
    1.24 +
    1.25  Goal "length [i..j(] = j-i";
    1.26  by (induct_tac "j" 1);
    1.27   by (Simp_tac 1);
    1.28 @@ -1217,30 +1220,15 @@
    1.29  qed_spec_mp "take_upt";
    1.30  Addsimps [take_upt];
    1.31  
    1.32 -Goal "!m i. i < n-m --> (map f [m..n(]) ! i = f(m+i)";
    1.33 +Goal "map Suc [m..n(] = [Suc m..n]";
    1.34  by (induct_tac "n" 1);
    1.35 - by (Simp_tac 1);
    1.36 -by (Clarify_tac 1);
    1.37 -by (subgoal_tac "m < Suc n" 1);
    1.38 - by (arith_tac 2);
    1.39 -by (stac upt_rec 1);
    1.40 -by (asm_simp_tac (simpset() delsplits [split_if]) 1);
    1.41 -by (split_tac [split_if] 1);
    1.42 -by (rtac conjI 1);
    1.43 - by (simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
    1.44 - by (simp_tac (simpset() addsimps [nth_append] addsplits [nat.split]) 1);
    1.45 - by (Clarify_tac 1);
    1.46 - by (rtac conjI 1);
    1.47 -  by (Clarify_tac 1);
    1.48 -  by (subgoal_tac "Suc(m+nat) < n" 1);
    1.49 -   by (arith_tac 2);
    1.50 -  by (Asm_simp_tac 1);
    1.51 - by (Clarify_tac 1);
    1.52 - by (subgoal_tac "n = Suc(m+nat)" 1);
    1.53 -  by (arith_tac 2);
    1.54 - by (Asm_simp_tac 1);
    1.55 -by (simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
    1.56 -by (arith_tac 1);
    1.57 +by Auto_tac;
    1.58 +qed "map_Suc_upt";
    1.59 +
    1.60 +Goal "ALL i. i < n-m --> (map f [m..n(]) ! i = f(m+i)";
    1.61 +by (res_inst_tac [("m","n"),("n","m")] diff_induct 1);
    1.62 +by (stac (map_Suc_upt RS sym) 3);
    1.63 +by (auto_tac (claset(), simpset() addsimps [less_diff_conv, nth_upt]));
    1.64  qed_spec_mp "nth_map_upt";
    1.65  
    1.66  Goal "ALL xs ys. k <= length xs --> k <= length ys -->  \