Introduced a generic "induct_tac" which picks up the right induction scheme
automatically. Also changed nat_ind_tac, which does no longer append a "1" to
the name of the induction variable. This caused some changes...

--- a/src/HOL/Hoare/Arith2.ML	Thu Apr 24 18:03:23 1997 +0200
+++ b/src/HOL/Hoare/Arith2.ML	Thu Apr 24 18:06:46 1997 +0200
@@ -189,7 +189,7 @@
 by (nat_ind_tac "m" 1);
 by (Simp_tac 1);
 by (etac mod_less 1);
-by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1);
+by (dres_inst_tac [("m","m*n")] mod_eq_add 1);
 by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1);
 qed "mod_prod_nn_is_0";
 

--- a/src/HOL/IOA/meta_theory/IOA.ML	Thu Apr 24 18:03:23 1997 +0200
+++ b/src/HOL/IOA/meta_theory/IOA.ML	Thu Apr 24 18:06:46 1997 +0200
@@ -81,8 +81,8 @@
   by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1);
   by (nat_ind_tac "n" 1);
   by (fast_tac (!claset addIs [p1,reachable_0]) 1);
-  by (eres_inst_tac[("x","n1")]allE 1);
-  by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n1")] optionE 1);
+  by (eres_inst_tac[("x","n")]allE 1);
+  by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n")] optionE 1);
   by (Asm_simp_tac 1);
   by (safe_tac (!claset));
   by (etac (p2 RS mp) 1);

--- a/src/HOL/List.ML	Thu Apr 24 18:03:23 1997 +0200
+++ b/src/HOL/List.ML	Thu Apr 24 18:06:46 1997 +0200
@@ -7,13 +7,13 @@
 *)
 
 goal thy "!x. xs ~= x#xs";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "not_Cons_self";
 Addsimps [not_Cons_self];
 
 goal thy "(xs ~= []) = (? y ys. xs = y#ys)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "neq_Nil_conv";
@@ -24,18 +24,18 @@
 goal thy
  "P(list_case a f xs) = ((xs=[] --> P(a)) & \
 \                        (!y ys. xs=y#ys --> P(f y ys)))";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
 qed "expand_list_case";
 
 val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
 by(REPEAT(resolve_tac prems 1));
 qed "list_cases";
 
 goal thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (Blast_tac 1);
 by (Blast_tac 1);
 bind_thm("list_eq_cases",
@@ -45,55 +45,55 @@
 (** @ - append **)
 
 goal thy "(xs@ys)@zs = xs@(ys@zs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "append_assoc";
 Addsimps [append_assoc];
 
 goal thy "xs @ [] = xs";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "append_Nil2";
 Addsimps [append_Nil2];
 
 goal thy "(xs@ys = []) = (xs=[] & ys=[])";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "append_is_Nil_conv";
 AddIffs [append_is_Nil_conv];
 
 goal thy "([] = xs@ys) = (xs=[] & ys=[])";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 by(Blast_tac 1);
 qed "Nil_is_append_conv";
 AddIffs [Nil_is_append_conv];
 
 goal thy "(xs @ ys = xs @ zs) = (ys=zs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "same_append_eq";
 AddIffs [same_append_eq];
 
 goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
  br allI 1;
- by(list.induct_tac "ys" 1);
+ by(induct_tac "ys" 1);
   by(ALLGOALS Asm_simp_tac);
 br allI 1;
-by(list.induct_tac "ys" 1);
+by(induct_tac "ys" 1);
  by(ALLGOALS Asm_simp_tac);
 qed_spec_mp "append1_eq_conv";
 AddIffs [append1_eq_conv];
 
 goal thy "xs ~= [] --> hd xs # tl xs = xs";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
 by(ALLGOALS Asm_simp_tac);
 qed_spec_mp "hd_Cons_tl";
 Addsimps [hd_Cons_tl];
 
 goal thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "hd_append";
 
@@ -105,44 +105,44 @@
 
 goal thy
   "(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
 by(ALLGOALS Asm_simp_tac);
 bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
 
 goal thy "map (%x.x) = (%xs.xs)";
 by (rtac ext 1);
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_ident";
 Addsimps[map_ident];
 
 goal thy "map f (xs@ys) = map f xs @ map f ys";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_append";
 Addsimps[map_append];
 
 goalw thy [o_def] "map (f o g) xs = map f (map g xs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_compose";
 Addsimps[map_compose];
 
 goal thy "rev(map f xs) = map f (rev xs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "rev_map";
 
 (** rev **)
 
 goal thy "rev(xs@ys) = rev(ys) @ rev(xs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "rev_append";
 Addsimps[rev_append];
 
 goal thy "rev(rev l) = l";
-by (list.induct_tac "l" 1);
+by (induct_tac "l" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "rev_rev_ident";
 Addsimps[rev_rev_ident];
@@ -151,13 +151,13 @@
 (** mem **)
 
 goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mem_append";
 Addsimps[mem_append];
 
 goal thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mem_filter";
 Addsimps[mem_filter];
@@ -165,14 +165,14 @@
 (** set_of_list **)
 
 goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
 qed "set_of_list_append";
 Addsimps[set_of_list_append];
 
 goal thy "(x mem xs) = (x: set_of_list xs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 by (Blast_tac 1);
 qed "set_of_list_mem_eq";
@@ -183,20 +183,20 @@
 qed "set_of_list_subset_Cons";
 
 goal thy "(set_of_list xs = {}) = (xs = [])";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
 by(ALLGOALS Asm_simp_tac);
 qed "set_of_list_empty";
 Addsimps [set_of_list_empty];
 
 goal thy "set_of_list(rev xs) = set_of_list(xs)";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
 by(ALLGOALS Asm_simp_tac);
 by(Blast_tac 1);
 qed "set_of_list_rev";
 Addsimps [set_of_list_rev];
 
 goal thy "set_of_list(map f xs) = f``(set_of_list xs)";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
 by(ALLGOALS Asm_simp_tac);
 qed "set_of_list_map";
 Addsimps [set_of_list_map];
@@ -205,19 +205,19 @@
 (** list_all **)
 
 goal thy "list_all (%x.True) xs = True";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "list_all_True";
 Addsimps [list_all_True];
 
 goal thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "list_all_append";
 Addsimps [list_all_append];
 
 goal thy "list_all P xs = (!x. x mem xs --> P(x))";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 by (Blast_tac 1);
 qed "list_all_mem_conv";
@@ -226,7 +226,7 @@
 (** filter **)
 
 goal thy "[x:xs@ys . P] = [x:xs . P] @ [y:ys . P]";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
  by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "filter_append";
 Addsimps [filter_append];
@@ -235,44 +235,44 @@
 (** concat **)
 
 goal thy  "concat(xs@ys) = concat(xs)@concat(ys)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed"concat_append";
 Addsimps [concat_append];
 
 goal thy "rev(concat ls) = concat (map rev (rev ls))";
-by (list.induct_tac "ls" 1);
+by (induct_tac "ls" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "rev_concat";
 
 (** length **)
 
 goal thy "length(xs@ys) = length(xs)+length(ys)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed"length_append";
 Addsimps [length_append];
 
 goal thy "length (map f l) = length l";
-by (list.induct_tac "l" 1);
+by (induct_tac "l" 1);
 by (ALLGOALS Simp_tac);
 qed "length_map";
 Addsimps [length_map];
 
 goal thy "length(rev xs) = length(xs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "length_rev";
 Addsimps [length_rev];
 
 goal thy "(length xs = 0) = (xs = [])";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
 by(ALLGOALS Asm_simp_tac);
 qed "length_0_conv";
 AddIffs [length_0_conv];
 
 goal thy "(0 < length xs) = (xs ~= [])";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
 by(ALLGOALS Asm_simp_tac);
 qed "length_greater_0_conv";
 AddIffs [length_greater_0_conv];
@@ -294,7 +294,7 @@
 qed_spec_mp "nth_append";
 
 goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 (* case [] *)
 by (Asm_full_simp_tac 1);
 (* case x#xl *)
@@ -305,7 +305,7 @@
 Addsimps [nth_map];
 
 goal thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case x#xl *)
@@ -315,7 +315,7 @@
 qed_spec_mp "list_all_nth";
 
 goal thy "!n. n < length xs --> (nth n xs) mem xs";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case x#xl *)
@@ -333,12 +333,12 @@
 section "take & drop";
 
 goal thy "take 0 xs = []";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "take_0";
 
 goal thy "drop 0 xs = xs";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "drop_0";
 
@@ -451,7 +451,7 @@
 
 goal thy
   "!n i. i < n --> nth i (take n xs) = nth i xs";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
  by(ALLGOALS Asm_simp_tac);
 by(strip_tac 1);
 by(res_inst_tac [("n","n")] natE 1);
@@ -475,7 +475,7 @@
 
 goal thy
   "x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
  by(Simp_tac 1);
 by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 by(Blast_tac 1);
@@ -484,7 +484,7 @@
 
 goal thy
   "(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
  by(Simp_tac 1);
 by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 bind_thm("takeWhile_append2", ballI RS (result() RS mp));
@@ -492,7 +492,7 @@
 
 goal thy
   "x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
  by(Simp_tac 1);
 by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 by(Blast_tac 1);
@@ -501,14 +501,14 @@
 
 goal thy
   "(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
  by(Simp_tac 1);
 by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 bind_thm("dropWhile_append2", ballI RS (result() RS mp));
 Addsimps [dropWhile_append2];
 
 goal thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x";
-by(list.induct_tac "xs" 1);
+by(induct_tac "xs" 1);
  by(Simp_tac 1);
 by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 qed_spec_mp"set_of_list_take_whileD";

--- a/src/HOL/NatDef.ML	Thu Apr 24 18:03:23 1997 +0200
+++ b/src/HOL/NatDef.ML	Thu Apr 24 18:06:46 1997 +0200
@@ -33,7 +33,7 @@
 
 val prems = goalw thy [Zero_def,Suc_def]
     "[| P(0);   \
-\       !!k. P(k) ==> P(Suc(k)) |]  ==> P(n)";
+\       !!n. P(n) ==> P(Suc(n)) |]  ==> P(n)";
 by (rtac (Rep_Nat_inverse RS subst) 1);   (*types force good instantiation*)
 by (rtac (Rep_Nat RS Nat_induct) 1);
 by (REPEAT (ares_tac prems 1
@@ -42,8 +42,16 @@
 
 (*Perform induction on n. *)
 fun nat_ind_tac a i = 
-    EVERY [res_inst_tac [("n",a)] nat_induct i,
-           rename_last_tac a ["1"] (i+1)];
+    EVERY[res_inst_tac [("n",a)] nat_induct i,
+          COND (Datatype.occs_in_prems a (i+1)) all_tac
+               (rename_last_tac a [""] (i+1))];
+
+(*Install 'automatic' induction tactic, pretending nat is a datatype *)
+(*except for induct_tac, everything is dummy*)
+datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
+  constructors = [], induct_tac = nat_ind_tac,
+  nchotomy = flexpair_def, case_cong = flexpair_def})];
+
 
 (*A special form of induction for reasoning about m<n and m-n*)
 val prems = goal thy

--- a/src/HOL/datatype.ML	Thu Apr 24 18:03:23 1997 +0200
+++ b/src/HOL/datatype.ML	Thu Apr 24 18:06:46 1997 +0200
@@ -410,8 +410,17 @@
            |> add_trrules xrules
            |> add_axioms rules, add_primrec)
     end
-end
-end
+
+(*Check if the (induction) variable occurs among the premises, which
+  usually signals a mistake *)
+fun occs_in_prems a i state =
+  let val (_, _, Bi, _) = dest_state(state,i)
+      val prems = Logic.strip_assums_hyp Bi
+  in a  mem  map (#1 o dest_Free) (foldr add_term_frees (prems,[])) end;
+
+end;
+
+end;
 
 (*
 Informal description of functions used in datatype.ML for the Isabelle/HOL
@@ -492,8 +501,7 @@
 (* The following has been written by Konrad Slind. *)
 
 
-type dtype_info = {case_const:term, case_rewrites:thm list,
-                   constructors:term list, nchotomy:thm, case_cong:thm};
+(* type dtype_info is defined in simpdata.ML *)
 
 signature Dtype_sig =
 sig
@@ -832,10 +840,15 @@
      fun const s = Const(s, the(Sign.const_type sign s))
      val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
      val {nchotomy,case_cong} = case_thms sign case_rewrites itac
+     fun induct_tac a i = itac a i THEN
+           COND (Datatype.occs_in_prems a i)
+             (warning "Induction variable occurs also among premises!";
+              all_tac) all_tac
  in
   (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,
         case_const = const (ty^"_case"),
         case_rewrites = map mk_rw case_rewrites,
+        induct_tac = induct_tac,
         nchotomy = nchotomy,
         case_cong = case_cong})
  end

--- a/src/HOL/ex/Mutil.ML	Thu Apr 24 18:03:23 1997 +0200
+++ b/src/HOL/ex/Mutil.ML	Thu Apr 24 18:06:46 1997 +0200
@@ -53,8 +53,8 @@
 by (resolve_tac tiling.intrs 1);
 by (assume_tac 2);
 by (subgoal_tac    (*seems the easiest way of turning one to the other*)
-    "({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \
-\    {(i, n1+n1), (i, Suc(n1+n1))}" 1);
+    "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
+\    {(i, n+n), (i, Suc(n+n))}" 1);
 by (Blast_tac 2);
 by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
 by (blast_tac (!claset addEs  [less_irrefl, less_asym]

--- a/src/HOL/simpdata.ML	Thu Apr 24 18:03:23 1997 +0200
+++ b/src/HOL/simpdata.ML	Thu Apr 24 18:06:46 1997 +0200
@@ -347,8 +347,12 @@
      ("simpset", ThyMethods {merge = merge, put = put, get = get})
 end;
 
-type dtype_info = {case_const:term, case_rewrites:thm list,
-                   constructors:term list, nchotomy:thm, case_cong:thm};
+type dtype_info = {case_const:term,
+                   case_rewrites:thm list,
+                   constructors:term list,
+                   induct_tac: string -> int -> tactic,
+                   nchotomy:thm,
+                   case_cong:thm};
 
 exception DT_DATA of (string * dtype_info) list;
 val datatypes = ref [] : (string * dtype_info) list ref;

--- a/src/HOL/thy_data.ML	Thu Apr 24 18:03:23 1997 +0200
+++ b/src/HOL/thy_data.ML	Thu Apr 24 18:06:46 1997 +0200
@@ -49,6 +49,27 @@
               in (map #case_cong info, flat (map #case_rewrites info)) end;
   in {case_congs = congs, case_rewrites = rewrites} end;
 
+(* generic induction tactic for datatypes *)
+fun induct_tac var i =
+  let fun find_tname Bi =
+        let val frees = map (fn Free x => x) (term_frees Bi)
+            val params = Logic.strip_params Bi;
+        in case assoc (frees@params, var) of
+             None => error("No such variable in subgoal: " ^ quote var)
+           | Some(Type(tn,_)) => tn
+           | _ => error("Cannot induct on type of " ^ quote var)
+        end;
+      fun get_ind_tac sign tn =
+        (case get_thydata (thyname_of_sign sign) "datatypes" of
+           None => error ("No such datatype: " ^ quote tn)
+         | Some (DT_DATA ds) =>
+             (case assoc (ds, tn) of
+                Some {induct_tac, ...} => induct_tac
+              | None => error ("Not a datatype: " ^ quote tn)));
+      fun induct state =
+        let val (_, _, Bi, _) = dest_state (state, i) 
+        in get_ind_tac (#sign(rep_thm state)) (find_tname Bi) var i end
+  in STATE induct end;
 
 (*Must be redefined in order to refer to the new instance of bind_thm
   created by init_thy_reader.*)
@@ -62,4 +83,3 @@
 
 fun qed_goalw_spec_mp name thy defs s p = 
 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
-