Introduced a generic "induct_tac" which picks up the right induction scheme
authornipkow
Thu Apr 24 18:06:46 1997 +0200 (1997-04-24)
changeset 30407d48671753da
parent 3039 bbf4e3738ef0
child 3041 bdd21deed6ea
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...
src/HOL/Hoare/Arith2.ML
src/HOL/IOA/meta_theory/IOA.ML
src/HOL/List.ML
src/HOL/NatDef.ML
src/HOL/datatype.ML
src/HOL/ex/Mutil.ML
src/HOL/simpdata.ML
src/HOL/thy_data.ML
     1.1 --- a/src/HOL/Hoare/Arith2.ML	Thu Apr 24 18:03:23 1997 +0200
     1.2 +++ b/src/HOL/Hoare/Arith2.ML	Thu Apr 24 18:06:46 1997 +0200
     1.3 @@ -189,7 +189,7 @@
     1.4  by (nat_ind_tac "m" 1);
     1.5  by (Simp_tac 1);
     1.6  by (etac mod_less 1);
     1.7 -by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1);
     1.8 +by (dres_inst_tac [("m","m*n")] mod_eq_add 1);
     1.9  by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1);
    1.10  qed "mod_prod_nn_is_0";
    1.11  
     2.1 --- a/src/HOL/IOA/meta_theory/IOA.ML	Thu Apr 24 18:03:23 1997 +0200
     2.2 +++ b/src/HOL/IOA/meta_theory/IOA.ML	Thu Apr 24 18:06:46 1997 +0200
     2.3 @@ -81,8 +81,8 @@
     2.4    by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1);
     2.5    by (nat_ind_tac "n" 1);
     2.6    by (fast_tac (!claset addIs [p1,reachable_0]) 1);
     2.7 -  by (eres_inst_tac[("x","n1")]allE 1);
     2.8 -  by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n1")] optionE 1);
     2.9 +  by (eres_inst_tac[("x","n")]allE 1);
    2.10 +  by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n")] optionE 1);
    2.11    by (Asm_simp_tac 1);
    2.12    by (safe_tac (!claset));
    2.13    by (etac (p2 RS mp) 1);
     3.1 --- a/src/HOL/List.ML	Thu Apr 24 18:03:23 1997 +0200
     3.2 +++ b/src/HOL/List.ML	Thu Apr 24 18:06:46 1997 +0200
     3.3 @@ -7,13 +7,13 @@
     3.4  *)
     3.5  
     3.6  goal thy "!x. xs ~= x#xs";
     3.7 -by (list.induct_tac "xs" 1);
     3.8 +by (induct_tac "xs" 1);
     3.9  by (ALLGOALS Asm_simp_tac);
    3.10  qed_spec_mp "not_Cons_self";
    3.11  Addsimps [not_Cons_self];
    3.12  
    3.13  goal thy "(xs ~= []) = (? y ys. xs = y#ys)";
    3.14 -by (list.induct_tac "xs" 1);
    3.15 +by (induct_tac "xs" 1);
    3.16  by (Simp_tac 1);
    3.17  by (Asm_simp_tac 1);
    3.18  qed "neq_Nil_conv";
    3.19 @@ -24,18 +24,18 @@
    3.20  goal thy
    3.21   "P(list_case a f xs) = ((xs=[] --> P(a)) & \
    3.22  \                        (!y ys. xs=y#ys --> P(f y ys)))";
    3.23 -by (list.induct_tac "xs" 1);
    3.24 +by (induct_tac "xs" 1);
    3.25  by (ALLGOALS Asm_simp_tac);
    3.26  by (Blast_tac 1);
    3.27  qed "expand_list_case";
    3.28  
    3.29  val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
    3.30 -by(list.induct_tac "xs" 1);
    3.31 +by(induct_tac "xs" 1);
    3.32  by(REPEAT(resolve_tac prems 1));
    3.33  qed "list_cases";
    3.34  
    3.35  goal thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
    3.36 -by (list.induct_tac "xs" 1);
    3.37 +by (induct_tac "xs" 1);
    3.38  by (Blast_tac 1);
    3.39  by (Blast_tac 1);
    3.40  bind_thm("list_eq_cases",
    3.41 @@ -45,55 +45,55 @@
    3.42  (** @ - append **)
    3.43  
    3.44  goal thy "(xs@ys)@zs = xs@(ys@zs)";
    3.45 -by (list.induct_tac "xs" 1);
    3.46 +by (induct_tac "xs" 1);
    3.47  by (ALLGOALS Asm_simp_tac);
    3.48  qed "append_assoc";
    3.49  Addsimps [append_assoc];
    3.50  
    3.51  goal thy "xs @ [] = xs";
    3.52 -by (list.induct_tac "xs" 1);
    3.53 +by (induct_tac "xs" 1);
    3.54  by (ALLGOALS Asm_simp_tac);
    3.55  qed "append_Nil2";
    3.56  Addsimps [append_Nil2];
    3.57  
    3.58  goal thy "(xs@ys = []) = (xs=[] & ys=[])";
    3.59 -by (list.induct_tac "xs" 1);
    3.60 +by (induct_tac "xs" 1);
    3.61  by (ALLGOALS Asm_simp_tac);
    3.62  qed "append_is_Nil_conv";
    3.63  AddIffs [append_is_Nil_conv];
    3.64  
    3.65  goal thy "([] = xs@ys) = (xs=[] & ys=[])";
    3.66 -by (list.induct_tac "xs" 1);
    3.67 +by (induct_tac "xs" 1);
    3.68  by (ALLGOALS Asm_simp_tac);
    3.69  by(Blast_tac 1);
    3.70  qed "Nil_is_append_conv";
    3.71  AddIffs [Nil_is_append_conv];
    3.72  
    3.73  goal thy "(xs @ ys = xs @ zs) = (ys=zs)";
    3.74 -by (list.induct_tac "xs" 1);
    3.75 +by (induct_tac "xs" 1);
    3.76  by (ALLGOALS Asm_simp_tac);
    3.77  qed "same_append_eq";
    3.78  AddIffs [same_append_eq];
    3.79  
    3.80  goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
    3.81 -by(list.induct_tac "xs" 1);
    3.82 +by(induct_tac "xs" 1);
    3.83   br allI 1;
    3.84 - by(list.induct_tac "ys" 1);
    3.85 + by(induct_tac "ys" 1);
    3.86    by(ALLGOALS Asm_simp_tac);
    3.87  br allI 1;
    3.88 -by(list.induct_tac "ys" 1);
    3.89 +by(induct_tac "ys" 1);
    3.90   by(ALLGOALS Asm_simp_tac);
    3.91  qed_spec_mp "append1_eq_conv";
    3.92  AddIffs [append1_eq_conv];
    3.93  
    3.94  goal thy "xs ~= [] --> hd xs # tl xs = xs";
    3.95 -by(list.induct_tac "xs" 1);
    3.96 +by(induct_tac "xs" 1);
    3.97  by(ALLGOALS Asm_simp_tac);
    3.98  qed_spec_mp "hd_Cons_tl";
    3.99  Addsimps [hd_Cons_tl];
   3.100  
   3.101  goal thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
   3.102 -by (list.induct_tac "xs" 1);
   3.103 +by (induct_tac "xs" 1);
   3.104  by (ALLGOALS Asm_simp_tac);
   3.105  qed "hd_append";
   3.106  
   3.107 @@ -105,44 +105,44 @@
   3.108  
   3.109  goal thy
   3.110    "(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs";
   3.111 -by(list.induct_tac "xs" 1);
   3.112 +by(induct_tac "xs" 1);
   3.113  by(ALLGOALS Asm_simp_tac);
   3.114  bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
   3.115  
   3.116  goal thy "map (%x.x) = (%xs.xs)";
   3.117  by (rtac ext 1);
   3.118 -by (list.induct_tac "xs" 1);
   3.119 +by (induct_tac "xs" 1);
   3.120  by (ALLGOALS Asm_simp_tac);
   3.121  qed "map_ident";
   3.122  Addsimps[map_ident];
   3.123  
   3.124  goal thy "map f (xs@ys) = map f xs @ map f ys";
   3.125 -by (list.induct_tac "xs" 1);
   3.126 +by (induct_tac "xs" 1);
   3.127  by (ALLGOALS Asm_simp_tac);
   3.128  qed "map_append";
   3.129  Addsimps[map_append];
   3.130  
   3.131  goalw thy [o_def] "map (f o g) xs = map f (map g xs)";
   3.132 -by (list.induct_tac "xs" 1);
   3.133 +by (induct_tac "xs" 1);
   3.134  by (ALLGOALS Asm_simp_tac);
   3.135  qed "map_compose";
   3.136  Addsimps[map_compose];
   3.137  
   3.138  goal thy "rev(map f xs) = map f (rev xs)";
   3.139 -by (list.induct_tac "xs" 1);
   3.140 +by (induct_tac "xs" 1);
   3.141  by (ALLGOALS Asm_simp_tac);
   3.142  qed "rev_map";
   3.143  
   3.144  (** rev **)
   3.145  
   3.146  goal thy "rev(xs@ys) = rev(ys) @ rev(xs)";
   3.147 -by (list.induct_tac "xs" 1);
   3.148 +by (induct_tac "xs" 1);
   3.149  by (ALLGOALS Asm_simp_tac);
   3.150  qed "rev_append";
   3.151  Addsimps[rev_append];
   3.152  
   3.153  goal thy "rev(rev l) = l";
   3.154 -by (list.induct_tac "l" 1);
   3.155 +by (induct_tac "l" 1);
   3.156  by (ALLGOALS Asm_simp_tac);
   3.157  qed "rev_rev_ident";
   3.158  Addsimps[rev_rev_ident];
   3.159 @@ -151,13 +151,13 @@
   3.160  (** mem **)
   3.161  
   3.162  goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
   3.163 -by (list.induct_tac "xs" 1);
   3.164 +by (induct_tac "xs" 1);
   3.165  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   3.166  qed "mem_append";
   3.167  Addsimps[mem_append];
   3.168  
   3.169  goal thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
   3.170 -by (list.induct_tac "xs" 1);
   3.171 +by (induct_tac "xs" 1);
   3.172  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   3.173  qed "mem_filter";
   3.174  Addsimps[mem_filter];
   3.175 @@ -165,14 +165,14 @@
   3.176  (** set_of_list **)
   3.177  
   3.178  goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
   3.179 -by (list.induct_tac "xs" 1);
   3.180 +by (induct_tac "xs" 1);
   3.181  by (ALLGOALS Asm_simp_tac);
   3.182  by (Blast_tac 1);
   3.183  qed "set_of_list_append";
   3.184  Addsimps[set_of_list_append];
   3.185  
   3.186  goal thy "(x mem xs) = (x: set_of_list xs)";
   3.187 -by (list.induct_tac "xs" 1);
   3.188 +by (induct_tac "xs" 1);
   3.189  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   3.190  by (Blast_tac 1);
   3.191  qed "set_of_list_mem_eq";
   3.192 @@ -183,20 +183,20 @@
   3.193  qed "set_of_list_subset_Cons";
   3.194  
   3.195  goal thy "(set_of_list xs = {}) = (xs = [])";
   3.196 -by(list.induct_tac "xs" 1);
   3.197 +by(induct_tac "xs" 1);
   3.198  by(ALLGOALS Asm_simp_tac);
   3.199  qed "set_of_list_empty";
   3.200  Addsimps [set_of_list_empty];
   3.201  
   3.202  goal thy "set_of_list(rev xs) = set_of_list(xs)";
   3.203 -by(list.induct_tac "xs" 1);
   3.204 +by(induct_tac "xs" 1);
   3.205  by(ALLGOALS Asm_simp_tac);
   3.206  by(Blast_tac 1);
   3.207  qed "set_of_list_rev";
   3.208  Addsimps [set_of_list_rev];
   3.209  
   3.210  goal thy "set_of_list(map f xs) = f``(set_of_list xs)";
   3.211 -by(list.induct_tac "xs" 1);
   3.212 +by(induct_tac "xs" 1);
   3.213  by(ALLGOALS Asm_simp_tac);
   3.214  qed "set_of_list_map";
   3.215  Addsimps [set_of_list_map];
   3.216 @@ -205,19 +205,19 @@
   3.217  (** list_all **)
   3.218  
   3.219  goal thy "list_all (%x.True) xs = True";
   3.220 -by (list.induct_tac "xs" 1);
   3.221 +by (induct_tac "xs" 1);
   3.222  by (ALLGOALS Asm_simp_tac);
   3.223  qed "list_all_True";
   3.224  Addsimps [list_all_True];
   3.225  
   3.226  goal thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
   3.227 -by (list.induct_tac "xs" 1);
   3.228 +by (induct_tac "xs" 1);
   3.229  by (ALLGOALS Asm_simp_tac);
   3.230  qed "list_all_append";
   3.231  Addsimps [list_all_append];
   3.232  
   3.233  goal thy "list_all P xs = (!x. x mem xs --> P(x))";
   3.234 -by (list.induct_tac "xs" 1);
   3.235 +by (induct_tac "xs" 1);
   3.236  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   3.237  by (Blast_tac 1);
   3.238  qed "list_all_mem_conv";
   3.239 @@ -226,7 +226,7 @@
   3.240  (** filter **)
   3.241  
   3.242  goal thy "[x:xs@ys . P] = [x:xs . P] @ [y:ys . P]";
   3.243 -by(list.induct_tac "xs" 1);
   3.244 +by(induct_tac "xs" 1);
   3.245   by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   3.246  qed "filter_append";
   3.247  Addsimps [filter_append];
   3.248 @@ -235,44 +235,44 @@
   3.249  (** concat **)
   3.250  
   3.251  goal thy  "concat(xs@ys) = concat(xs)@concat(ys)";
   3.252 -by (list.induct_tac "xs" 1);
   3.253 +by (induct_tac "xs" 1);
   3.254  by (ALLGOALS Asm_simp_tac);
   3.255  qed"concat_append";
   3.256  Addsimps [concat_append];
   3.257  
   3.258  goal thy "rev(concat ls) = concat (map rev (rev ls))";
   3.259 -by (list.induct_tac "ls" 1);
   3.260 +by (induct_tac "ls" 1);
   3.261  by (ALLGOALS Asm_simp_tac);
   3.262  qed "rev_concat";
   3.263  
   3.264  (** length **)
   3.265  
   3.266  goal thy "length(xs@ys) = length(xs)+length(ys)";
   3.267 -by (list.induct_tac "xs" 1);
   3.268 +by (induct_tac "xs" 1);
   3.269  by (ALLGOALS Asm_simp_tac);
   3.270  qed"length_append";
   3.271  Addsimps [length_append];
   3.272  
   3.273  goal thy "length (map f l) = length l";
   3.274 -by (list.induct_tac "l" 1);
   3.275 +by (induct_tac "l" 1);
   3.276  by (ALLGOALS Simp_tac);
   3.277  qed "length_map";
   3.278  Addsimps [length_map];
   3.279  
   3.280  goal thy "length(rev xs) = length(xs)";
   3.281 -by (list.induct_tac "xs" 1);
   3.282 +by (induct_tac "xs" 1);
   3.283  by (ALLGOALS Asm_simp_tac);
   3.284  qed "length_rev";
   3.285  Addsimps [length_rev];
   3.286  
   3.287  goal thy "(length xs = 0) = (xs = [])";
   3.288 -by(list.induct_tac "xs" 1);
   3.289 +by(induct_tac "xs" 1);
   3.290  by(ALLGOALS Asm_simp_tac);
   3.291  qed "length_0_conv";
   3.292  AddIffs [length_0_conv];
   3.293  
   3.294  goal thy "(0 < length xs) = (xs ~= [])";
   3.295 -by(list.induct_tac "xs" 1);
   3.296 +by(induct_tac "xs" 1);
   3.297  by(ALLGOALS Asm_simp_tac);
   3.298  qed "length_greater_0_conv";
   3.299  AddIffs [length_greater_0_conv];
   3.300 @@ -294,7 +294,7 @@
   3.301  qed_spec_mp "nth_append";
   3.302  
   3.303  goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
   3.304 -by (list.induct_tac "xs" 1);
   3.305 +by (induct_tac "xs" 1);
   3.306  (* case [] *)
   3.307  by (Asm_full_simp_tac 1);
   3.308  (* case x#xl *)
   3.309 @@ -305,7 +305,7 @@
   3.310  Addsimps [nth_map];
   3.311  
   3.312  goal thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
   3.313 -by (list.induct_tac "xs" 1);
   3.314 +by (induct_tac "xs" 1);
   3.315  (* case [] *)
   3.316  by (Simp_tac 1);
   3.317  (* case x#xl *)
   3.318 @@ -315,7 +315,7 @@
   3.319  qed_spec_mp "list_all_nth";
   3.320  
   3.321  goal thy "!n. n < length xs --> (nth n xs) mem xs";
   3.322 -by (list.induct_tac "xs" 1);
   3.323 +by (induct_tac "xs" 1);
   3.324  (* case [] *)
   3.325  by (Simp_tac 1);
   3.326  (* case x#xl *)
   3.327 @@ -333,12 +333,12 @@
   3.328  section "take & drop";
   3.329  
   3.330  goal thy "take 0 xs = []";
   3.331 -by (list.induct_tac "xs" 1);
   3.332 +by (induct_tac "xs" 1);
   3.333  by (ALLGOALS Asm_simp_tac);
   3.334  qed "take_0";
   3.335  
   3.336  goal thy "drop 0 xs = xs";
   3.337 -by (list.induct_tac "xs" 1);
   3.338 +by (induct_tac "xs" 1);
   3.339  by (ALLGOALS Asm_simp_tac);
   3.340  qed "drop_0";
   3.341  
   3.342 @@ -451,7 +451,7 @@
   3.343  
   3.344  goal thy
   3.345    "!n i. i < n --> nth i (take n xs) = nth i xs";
   3.346 -by(list.induct_tac "xs" 1);
   3.347 +by(induct_tac "xs" 1);
   3.348   by(ALLGOALS Asm_simp_tac);
   3.349  by(strip_tac 1);
   3.350  by(res_inst_tac [("n","n")] natE 1);
   3.351 @@ -475,7 +475,7 @@
   3.352  
   3.353  goal thy
   3.354    "x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
   3.355 -by(list.induct_tac "xs" 1);
   3.356 +by(induct_tac "xs" 1);
   3.357   by(Simp_tac 1);
   3.358  by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   3.359  by(Blast_tac 1);
   3.360 @@ -484,7 +484,7 @@
   3.361  
   3.362  goal thy
   3.363    "(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
   3.364 -by(list.induct_tac "xs" 1);
   3.365 +by(induct_tac "xs" 1);
   3.366   by(Simp_tac 1);
   3.367  by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   3.368  bind_thm("takeWhile_append2", ballI RS (result() RS mp));
   3.369 @@ -492,7 +492,7 @@
   3.370  
   3.371  goal thy
   3.372    "x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
   3.373 -by(list.induct_tac "xs" 1);
   3.374 +by(induct_tac "xs" 1);
   3.375   by(Simp_tac 1);
   3.376  by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   3.377  by(Blast_tac 1);
   3.378 @@ -501,14 +501,14 @@
   3.379  
   3.380  goal thy
   3.381    "(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
   3.382 -by(list.induct_tac "xs" 1);
   3.383 +by(induct_tac "xs" 1);
   3.384   by(Simp_tac 1);
   3.385  by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   3.386  bind_thm("dropWhile_append2", ballI RS (result() RS mp));
   3.387  Addsimps [dropWhile_append2];
   3.388  
   3.389  goal thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x";
   3.390 -by(list.induct_tac "xs" 1);
   3.391 +by(induct_tac "xs" 1);
   3.392   by(Simp_tac 1);
   3.393  by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   3.394  qed_spec_mp"set_of_list_take_whileD";
     4.1 --- a/src/HOL/NatDef.ML	Thu Apr 24 18:03:23 1997 +0200
     4.2 +++ b/src/HOL/NatDef.ML	Thu Apr 24 18:06:46 1997 +0200
     4.3 @@ -33,7 +33,7 @@
     4.4  
     4.5  val prems = goalw thy [Zero_def,Suc_def]
     4.6      "[| P(0);   \
     4.7 -\       !!k. P(k) ==> P(Suc(k)) |]  ==> P(n)";
     4.8 +\       !!n. P(n) ==> P(Suc(n)) |]  ==> P(n)";
     4.9  by (rtac (Rep_Nat_inverse RS subst) 1);   (*types force good instantiation*)
    4.10  by (rtac (Rep_Nat RS Nat_induct) 1);
    4.11  by (REPEAT (ares_tac prems 1
    4.12 @@ -42,8 +42,16 @@
    4.13  
    4.14  (*Perform induction on n. *)
    4.15  fun nat_ind_tac a i = 
    4.16 -    EVERY [res_inst_tac [("n",a)] nat_induct i,
    4.17 -           rename_last_tac a ["1"] (i+1)];
    4.18 +    EVERY[res_inst_tac [("n",a)] nat_induct i,
    4.19 +          COND (Datatype.occs_in_prems a (i+1)) all_tac
    4.20 +               (rename_last_tac a [""] (i+1))];
    4.21 +
    4.22 +(*Install 'automatic' induction tactic, pretending nat is a datatype *)
    4.23 +(*except for induct_tac, everything is dummy*)
    4.24 +datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
    4.25 +  constructors = [], induct_tac = nat_ind_tac,
    4.26 +  nchotomy = flexpair_def, case_cong = flexpair_def})];
    4.27 +
    4.28  
    4.29  (*A special form of induction for reasoning about m<n and m-n*)
    4.30  val prems = goal thy
     5.1 --- a/src/HOL/datatype.ML	Thu Apr 24 18:03:23 1997 +0200
     5.2 +++ b/src/HOL/datatype.ML	Thu Apr 24 18:06:46 1997 +0200
     5.3 @@ -410,8 +410,17 @@
     5.4             |> add_trrules xrules
     5.5             |> add_axioms rules, add_primrec)
     5.6      end
     5.7 -end
     5.8 -end
     5.9 +
    5.10 +(*Check if the (induction) variable occurs among the premises, which
    5.11 +  usually signals a mistake *)
    5.12 +fun occs_in_prems a i state =
    5.13 +  let val (_, _, Bi, _) = dest_state(state,i)
    5.14 +      val prems = Logic.strip_assums_hyp Bi
    5.15 +  in a  mem  map (#1 o dest_Free) (foldr add_term_frees (prems,[])) end;
    5.16 +
    5.17 +end;
    5.18 +
    5.19 +end;
    5.20  
    5.21  (*
    5.22  Informal description of functions used in datatype.ML for the Isabelle/HOL
    5.23 @@ -492,8 +501,7 @@
    5.24  (* The following has been written by Konrad Slind. *)
    5.25  
    5.26  
    5.27 -type dtype_info = {case_const:term, case_rewrites:thm list,
    5.28 -                   constructors:term list, nchotomy:thm, case_cong:thm};
    5.29 +(* type dtype_info is defined in simpdata.ML *)
    5.30  
    5.31  signature Dtype_sig =
    5.32  sig
    5.33 @@ -832,10 +840,15 @@
    5.34       fun const s = Const(s, the(Sign.const_type sign s))
    5.35       val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
    5.36       val {nchotomy,case_cong} = case_thms sign case_rewrites itac
    5.37 +     fun induct_tac a i = itac a i THEN
    5.38 +           COND (Datatype.occs_in_prems a i)
    5.39 +             (warning "Induction variable occurs also among premises!";
    5.40 +              all_tac) all_tac
    5.41   in
    5.42    (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,
    5.43          case_const = const (ty^"_case"),
    5.44          case_rewrites = map mk_rw case_rewrites,
    5.45 +        induct_tac = induct_tac,
    5.46          nchotomy = nchotomy,
    5.47          case_cong = case_cong})
    5.48   end
     6.1 --- a/src/HOL/ex/Mutil.ML	Thu Apr 24 18:03:23 1997 +0200
     6.2 +++ b/src/HOL/ex/Mutil.ML	Thu Apr 24 18:06:46 1997 +0200
     6.3 @@ -53,8 +53,8 @@
     6.4  by (resolve_tac tiling.intrs 1);
     6.5  by (assume_tac 2);
     6.6  by (subgoal_tac    (*seems the easiest way of turning one to the other*)
     6.7 -    "({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \
     6.8 -\    {(i, n1+n1), (i, Suc(n1+n1))}" 1);
     6.9 +    "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
    6.10 +\    {(i, n+n), (i, Suc(n+n))}" 1);
    6.11  by (Blast_tac 2);
    6.12  by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
    6.13  by (blast_tac (!claset addEs  [less_irrefl, less_asym]
     7.1 --- a/src/HOL/simpdata.ML	Thu Apr 24 18:03:23 1997 +0200
     7.2 +++ b/src/HOL/simpdata.ML	Thu Apr 24 18:06:46 1997 +0200
     7.3 @@ -347,8 +347,12 @@
     7.4       ("simpset", ThyMethods {merge = merge, put = put, get = get})
     7.5  end;
     7.6  
     7.7 -type dtype_info = {case_const:term, case_rewrites:thm list,
     7.8 -                   constructors:term list, nchotomy:thm, case_cong:thm};
     7.9 +type dtype_info = {case_const:term,
    7.10 +                   case_rewrites:thm list,
    7.11 +                   constructors:term list,
    7.12 +                   induct_tac: string -> int -> tactic,
    7.13 +                   nchotomy:thm,
    7.14 +                   case_cong:thm};
    7.15  
    7.16  exception DT_DATA of (string * dtype_info) list;
    7.17  val datatypes = ref [] : (string * dtype_info) list ref;
     8.1 --- a/src/HOL/thy_data.ML	Thu Apr 24 18:03:23 1997 +0200
     8.2 +++ b/src/HOL/thy_data.ML	Thu Apr 24 18:06:46 1997 +0200
     8.3 @@ -49,6 +49,27 @@
     8.4                in (map #case_cong info, flat (map #case_rewrites info)) end;
     8.5    in {case_congs = congs, case_rewrites = rewrites} end;
     8.6  
     8.7 +(* generic induction tactic for datatypes *)
     8.8 +fun induct_tac var i =
     8.9 +  let fun find_tname Bi =
    8.10 +        let val frees = map (fn Free x => x) (term_frees Bi)
    8.11 +            val params = Logic.strip_params Bi;
    8.12 +        in case assoc (frees@params, var) of
    8.13 +             None => error("No such variable in subgoal: " ^ quote var)
    8.14 +           | Some(Type(tn,_)) => tn
    8.15 +           | _ => error("Cannot induct on type of " ^ quote var)
    8.16 +        end;
    8.17 +      fun get_ind_tac sign tn =
    8.18 +        (case get_thydata (thyname_of_sign sign) "datatypes" of
    8.19 +           None => error ("No such datatype: " ^ quote tn)
    8.20 +         | Some (DT_DATA ds) =>
    8.21 +             (case assoc (ds, tn) of
    8.22 +                Some {induct_tac, ...} => induct_tac
    8.23 +              | None => error ("Not a datatype: " ^ quote tn)));
    8.24 +      fun induct state =
    8.25 +        let val (_, _, Bi, _) = dest_state (state, i) 
    8.26 +        in get_ind_tac (#sign(rep_thm state)) (find_tname Bi) var i end
    8.27 +  in STATE induct end;
    8.28  
    8.29  (*Must be redefined in order to refer to the new instance of bind_thm
    8.30    created by init_thy_reader.*)
    8.31 @@ -62,4 +83,3 @@
    8.32  
    8.33  fun qed_goalw_spec_mp name thy defs s p = 
    8.34  	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
    8.35 -