src/HOL/List.ML
changeset 9747 043098ba5098
parent 9700 71364b487232
child 9763 252c690690b0
     1.1 --- a/src/HOL/List.ML	Wed Aug 30 16:24:29 2000 +0200
     1.2 +++ b/src/HOL/List.ML	Wed Aug 30 16:29:21 2000 +0200
     1.3 @@ -414,10 +414,10 @@
     1.4  by (eresolve_tac prems 1);
     1.5  qed "rev_induct";
     1.6  
     1.7 -fun rev_induct_tac xs = res_inst_tac [("xs",xs)] rev_induct;
     1.8 +val rev_induct_tac = induct_thm_tac rev_induct;
     1.9  
    1.10  Goal  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
    1.11 -by (res_inst_tac [("xs","xs")] rev_induct 1);
    1.12 +by (rev_induct_tac "xs" 1);
    1.13  by Auto_tac;
    1.14  bind_thm ("rev_exhaust",
    1.15    impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
    1.16 @@ -752,7 +752,7 @@
    1.17  Addsimps [butlast_snoc];
    1.18  
    1.19  Goal "length(butlast xs) = length xs - 1";
    1.20 -by (res_inst_tac [("xs","xs")] rev_induct 1);
    1.21 +by (rev_induct_tac "xs" 1);
    1.22  by Auto_tac;
    1.23  qed "length_butlast";
    1.24  Addsimps [length_butlast];
    1.25 @@ -1217,7 +1217,7 @@
    1.26  qed "map_Suc_upt";
    1.27  
    1.28  Goal "ALL i. i < n-m --> (map f [m..n(]) ! i = f(m+i)";
    1.29 -by (res_inst_tac [("m","n"),("n","m")] diff_induct 1);
    1.30 +by (induct_thm_tac diff_induct "n m" 1);
    1.31  by (stac (map_Suc_upt RS sym) 3);
    1.32  by (auto_tac (claset(), simpset() addsimps [less_diff_conv, nth_upt]));
    1.33  qed_spec_mp "nth_map_upt";
    1.34 @@ -1453,14 +1453,14 @@
    1.35  
    1.36  Goal "map fst [p:zip xs [i..i + length xs(] . snd p : A] =     \
    1.37  \     map fst [p:zip xs [0..length xs(] . snd p + i : A]";
    1.38 -by (res_inst_tac [("xs","xs")] rev_induct 1);
    1.39 +by (rev_induct_tac "xs" 1);
    1.40   by (asm_simp_tac (simpset() addsimps [add_commute]) 2);
    1.41  by (Simp_tac 1);
    1.42  qed "sublist_shift_lemma";
    1.43  
    1.44  Goalw [sublist_def]
    1.45       "sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}";
    1.46 -by (res_inst_tac [("xs","l'")] rev_induct 1);
    1.47 +by (rev_induct_tac "l'" 1);
    1.48  by (Simp_tac 1);
    1.49  by (asm_simp_tac (simpset() addsimps [inst "i" "0" upt_add_eq_append, 
    1.50  	                              zip_append, sublist_shift_lemma]) 1);
    1.51 @@ -1470,7 +1470,7 @@
    1.52  Addsimps [sublist_empty, sublist_nil];
    1.53  
    1.54  Goal "sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}";
    1.55 -by (res_inst_tac [("xs","l")] rev_induct 1);
    1.56 +by (rev_induct_tac "l" 1);
    1.57   by (asm_simp_tac (simpset() delsimps [append_Cons]
    1.58  	 		     addsimps [append_Cons RS sym, sublist_append]) 2);
    1.59  by (simp_tac (simpset() addsimps [sublist_def]) 1);
    1.60 @@ -1482,7 +1482,7 @@
    1.61  Addsimps [sublist_singleton];
    1.62  
    1.63  Goal "sublist l {..n(} = take n l";
    1.64 -by (res_inst_tac [("xs","l")] rev_induct 1);
    1.65 +by (rev_induct_tac "l" 1);
    1.66   by (asm_simp_tac (simpset() addsplits [nat_diff_split]
    1.67                               addsimps [sublist_append]) 2);
    1.68  by (Simp_tac 1);