induct_tac and exhaust_tac
authorpaulson
Wed Jan 06 13:24:33 1999 +0100 (1999-01-06)
changeset 60653b4a29166f26
parent 6064 0786b5afd8ee
child 6066 f4f0d637747c
induct_tac and exhaust_tac
src/ZF/Integ/Bin.ML
src/ZF/IsaMakefile
src/ZF/List.ML
src/ZF/ROOT.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/primrec_package.ML
src/ZF/Zorn.ML
src/ZF/ex/BT.ML
src/ZF/ex/Primrec.ML
     1.1 --- a/src/ZF/Integ/Bin.ML	Wed Jan 06 13:23:41 1999 +0100
     1.2 +++ b/src/ZF/Integ/Bin.ML	Wed Jan 06 13:24:33 1999 +0100
     1.3 @@ -10,13 +10,6 @@
     1.4  Addsimps bin.intrs;
     1.5  Addsimps int_typechecks;
     1.6  
     1.7 -(*Perform induction on l, then prove the major premise using prems. *)
     1.8 -fun bin_ind_tac a prems i = 
     1.9 -    EVERY [res_inst_tac [("x",a)] bin.induct i,
    1.10 -           rename_last_tac a ["1"] (i+3),
    1.11 -           ares_tac prems i];
    1.12 -
    1.13 -
    1.14  Goal "NCons(Pls,0) = Pls";
    1.15  by (Asm_simp_tac 1);
    1.16  qed "NCons_Pls_0";
    1.17 @@ -48,46 +41,47 @@
    1.18  Addsimps [bool_into_nat];
    1.19  
    1.20  Goal "w: bin ==> integ_of(w) : int";
    1.21 -by (bin_ind_tac "w" [] 1);
    1.22 +by (induct_tac "w" 1);
    1.23  by (ALLGOALS (Asm_simp_tac));
    1.24  qed "integ_of_type";
    1.25  Addsimps [integ_of_type];
    1.26  
    1.27  Goal "[| w: bin; b: bool |] ==> NCons(w,b) : bin";
    1.28 -by (bin_ind_tac "w" [] 1);
    1.29 +by (induct_tac "w" 1);
    1.30  by Auto_tac;
    1.31  qed "NCons_type";
    1.32  Addsimps [NCons_type];
    1.33  
    1.34  Goal "w: bin ==> bin_succ(w) : bin";
    1.35 -by (bin_ind_tac "w" [] 1);
    1.36 +by (induct_tac "w" 1);
    1.37  by Auto_tac;
    1.38  qed "bin_succ_type";
    1.39  Addsimps [bin_succ_type];
    1.40  
    1.41  Goal "w: bin ==> bin_pred(w) : bin";
    1.42 -by (bin_ind_tac "w" [] 1);
    1.43 +by (induct_tac "w" 1);
    1.44  by Auto_tac;
    1.45  qed "bin_pred_type";
    1.46  Addsimps [bin_pred_type];
    1.47  
    1.48  Goal "w: bin ==> bin_minus(w) : bin";
    1.49 -by (bin_ind_tac "w" [] 1);
    1.50 +by (induct_tac "w" 1);
    1.51  by Auto_tac;
    1.52  qed "bin_minus_type";
    1.53  Addsimps [bin_minus_type];
    1.54  
    1.55  (*This proof is complicated by the mutual recursion*)
    1.56  Goal "v: bin ==> ALL w: bin. bin_add(v,w) : bin";
    1.57 -by (bin_ind_tac "v" [] 1);
    1.58 +by (induct_tac "v" 1);
    1.59  by (rtac ballI 3);
    1.60 -by (bin_ind_tac "w" [] 3);
    1.61 +by (rename_tac "w'" 3);
    1.62 +by (induct_tac "w'" 3);
    1.63  by Auto_tac;
    1.64  bind_thm ("bin_add_type", result() RS bspec);
    1.65  Addsimps [bin_add_type];
    1.66  
    1.67  Goal "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
    1.68 -by (bin_ind_tac "v" [] 1);
    1.69 +by (induct_tac "v" 1);
    1.70  by Auto_tac;
    1.71  qed "bin_mult_type";
    1.72  Addsimps [bin_mult_type];
    1.73 @@ -173,7 +167,7 @@
    1.74  by (Simp_tac 1);
    1.75  by (Simp_tac 1);
    1.76  by (rtac ballI 1);
    1.77 -by (bin_ind_tac "wa" [] 1);
    1.78 +by (induct_tac "wa" 1);
    1.79  by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
    1.80  bind_thm("integ_of_add", result() RS bspec);
    1.81  
    1.82 @@ -184,13 +178,12 @@
    1.83  
    1.84  Goal "[| v: bin;  w: bin |]   \
    1.85  \     ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)";
    1.86 -by (bin_ind_tac "v" [major] 1);
    1.87 +by (induct_tac "v" 1);
    1.88  by (Asm_simp_tac 1);
    1.89  by (Asm_simp_tac 1);
    1.90  by (etac boolE 1);
    1.91  by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 2);
    1.92 -by (asm_simp_tac 
    1.93 -    (simpset() addsimps [zadd_zmult_distrib] @ zadd_ac) 1);
    1.94 +by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib] @ zadd_ac) 1);
    1.95  qed "integ_of_mult";
    1.96  
    1.97  (**** Computations ****)
     2.1 --- a/src/ZF/IsaMakefile	Wed Jan 06 13:23:41 1999 +0100
     2.2 +++ b/src/ZF/IsaMakefile	Wed Jan 06 13:24:33 1999 +0100
     2.3 @@ -43,7 +43,7 @@
     2.4    ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
     2.5    subset.thy thy_syntax.ML upair.ML upair.thy \
     2.6    Tools/cartprod.ML Tools/datatype_package.ML Tools/inductive_package.ML \
     2.7 -  Tools/primrec_package.ML Tools/typechk.ML \
     2.8 +  Tools/primrec_package.ML Tools/induct_tacs.ML Tools/typechk.ML \
     2.9    Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \
    2.10    Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy 
    2.11  	@$(ISATOOL) usedir -b $(OUT)/FOL ZF
     3.1 --- a/src/ZF/List.ML	Wed Jan 06 13:23:41 1999 +0100
     3.2 +++ b/src/ZF/List.ML	Wed Jan 06 13:24:33 1999 +0100
     3.3 @@ -15,12 +15,6 @@
     3.4  val Cons_iff     = list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";
     3.5  val Nil_Cons_iff = list.mk_free "~ Nil=Cons(a,l)";
     3.6  
     3.7 -(*Perform induction on l, then prove the major premise using prems. *)
     3.8 -fun list_ind_tac a prems i = 
     3.9 -    EVERY [res_inst_tac [("x",a)] list.induct i,
    3.10 -           rename_last_tac a ["1"] (i+2),
    3.11 -           ares_tac prems i];
    3.12 -
    3.13  Goal "list(A) = {0} + (A * list(A))";
    3.14  let open list;  val rew = rewrite_rule con_defs in  
    3.15  by (blast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
    3.16 @@ -63,7 +57,7 @@
    3.17  (*** List functions ***)
    3.18  
    3.19  Goal "l: list(A) ==> tl(l) : list(A)";
    3.20 -by (etac list.elim 1);
    3.21 +by (exhaust_tac "l" 1);
    3.22  by (ALLGOALS (asm_simp_tac (simpset() addsimps list.intrs)));
    3.23  qed "tl_type";
    3.24  
    3.25 @@ -102,7 +96,8 @@
    3.26  \       c: C(Nil);       \
    3.27  \       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
    3.28  \    |] ==> list_rec(c,h,l) : C(l)";
    3.29 -by (list_ind_tac "l" prems 1);
    3.30 +by (cut_facts_tac prems 1);
    3.31 +by (induct_tac "l" 1);
    3.32  by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
    3.33  qed "list_rec_type";
    3.34  
    3.35 @@ -183,29 +178,29 @@
    3.36  (*** theorems about map ***)
    3.37  
    3.38  Goal "l: list(A) ==> map(%u. u, l) = l";
    3.39 -by (list_ind_tac "l" [] 1);
    3.40 +by (induct_tac "l" 1);
    3.41  by (ALLGOALS Asm_simp_tac);
    3.42  qed "map_ident";
    3.43  
    3.44  Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
    3.45 -by (list_ind_tac "l" [] 1);
    3.46 +by (induct_tac "l" 1);
    3.47  by (ALLGOALS Asm_simp_tac);
    3.48  qed "map_compose";
    3.49  
    3.50  Goal "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
    3.51 -by (list_ind_tac "xs" [] 1);
    3.52 +by (induct_tac "xs" 1);
    3.53  by (ALLGOALS Asm_simp_tac);
    3.54  qed "map_app_distrib";
    3.55  
    3.56  Goal "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
    3.57 -by (list_ind_tac "ls" [] 1);
    3.58 +by (induct_tac "ls" 1);
    3.59  by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
    3.60  qed "map_flat";
    3.61  
    3.62  Goal "l: list(A) ==> \
    3.63  \    list_rec(c, d, map(h,l)) = \
    3.64  \    list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)";
    3.65 -by (list_ind_tac "l" [] 1);
    3.66 +by (induct_tac "l" 1);
    3.67  by (ALLGOALS Asm_simp_tac);
    3.68  qed "list_rec_map";
    3.69  
    3.70 @@ -215,19 +210,19 @@
    3.71  bind_thm ("list_CollectD", (Collect_subset RS list_mono RS subsetD));
    3.72  
    3.73  Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
    3.74 -by (list_ind_tac "l" [] 1);
    3.75 +by (induct_tac "l" 1);
    3.76  by (ALLGOALS Asm_simp_tac);
    3.77  qed "map_list_Collect";
    3.78  
    3.79  (*** theorems about length ***)
    3.80  
    3.81  Goal "xs: list(A) ==> length(map(h,xs)) = length(xs)";
    3.82 -by (list_ind_tac "xs" [] 1);
    3.83 +by (induct_tac "xs" 1);
    3.84  by (ALLGOALS Asm_simp_tac);
    3.85  qed "length_map";
    3.86  
    3.87  Goal "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
    3.88 -by (list_ind_tac "xs" [] 1);
    3.89 +by (induct_tac "xs" 1);
    3.90  by (ALLGOALS Asm_simp_tac);
    3.91  qed "length_app";
    3.92  
    3.93 @@ -236,12 +231,12 @@
    3.94  val add_commute_succ = nat_succI RSN (2,add_commute);
    3.95  
    3.96  Goal "xs: list(A) ==> length(rev(xs)) = length(xs)";
    3.97 -by (list_ind_tac "xs" [] 1);
    3.98 +by (induct_tac "xs" 1);
    3.99  by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app, add_commute_succ])));
   3.100  qed "length_rev";
   3.101  
   3.102  Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
   3.103 -by (list_ind_tac "ls" [] 1);
   3.104 +by (induct_tac "ls" 1);
   3.105  by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
   3.106  qed "length_flat";
   3.107  
   3.108 @@ -279,19 +274,19 @@
   3.109  qed "app_right_Nil";
   3.110  
   3.111  Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
   3.112 -by (list_ind_tac "xs" [] 1);
   3.113 +by (induct_tac "xs" 1);
   3.114  by (ALLGOALS Asm_simp_tac);
   3.115  qed "app_assoc";
   3.116  
   3.117  Goal "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
   3.118 -by (list_ind_tac "ls" [] 1);
   3.119 +by (induct_tac "ls" 1);
   3.120  by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
   3.121  qed "flat_app_distrib";
   3.122  
   3.123  (*** theorems about rev ***)
   3.124  
   3.125  Goal "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
   3.126 -by (list_ind_tac "l" [] 1);
   3.127 +by (induct_tac "l" 1);
   3.128  by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
   3.129  qed "rev_map_distrib";
   3.130  
   3.131 @@ -305,12 +300,12 @@
   3.132  qed "rev_app_distrib";
   3.133  
   3.134  Goal "l: list(A) ==> rev(rev(l))=l";
   3.135 -by (list_ind_tac "l" [] 1);
   3.136 +by (induct_tac "l" 1);
   3.137  by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib])));
   3.138  qed "rev_rev_ident";
   3.139  
   3.140  Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
   3.141 -by (list_ind_tac "ls" [] 1);
   3.142 +by (induct_tac "ls" 1);
   3.143  by (ALLGOALS (asm_simp_tac (simpset() addsimps 
   3.144         [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
   3.145  qed "rev_flat";
   3.146 @@ -320,7 +315,7 @@
   3.147  
   3.148  Goal "[| xs: list(nat);  ys: list(nat) |] ==> \
   3.149  \    list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
   3.150 -by (list_ind_tac "xs" [] 1);
   3.151 +by (induct_tac "xs" 1);
   3.152  by (ALLGOALS 
   3.153      (asm_simp_tac (simpset() addsimps [add_0_right, add_assoc RS sym])));
   3.154  by (rtac (add_commute RS subst_context) 1);
   3.155 @@ -328,13 +323,13 @@
   3.156  qed "list_add_app";
   3.157  
   3.158  Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
   3.159 -by (list_ind_tac "l" [] 1);
   3.160 +by (induct_tac "l" 1);
   3.161  by (ALLGOALS
   3.162      (asm_simp_tac (simpset() addsimps [list_add_app, add_0_right])));
   3.163  qed "list_add_rev";
   3.164  
   3.165  Goal "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
   3.166 -by (list_ind_tac "ls" [] 1);
   3.167 +by (induct_tac "ls" 1);
   3.168  by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
   3.169  by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
   3.170  qed "list_add_flat";
     4.1 --- a/src/ZF/ROOT.ML	Wed Jan 06 13:23:41 1999 +0100
     4.2 +++ b/src/ZF/ROOT.ML	Wed Jan 06 13:24:33 1999 +0100
     4.3 @@ -46,6 +46,7 @@
     4.4  use "Tools/datatype_package";
     4.5  use "Tools/primrec_package";
     4.6  use_thy "Datatype";
     4.7 +use "Tools/induct_tacs";
     4.8  use_thy "InfDatatype";
     4.9  use_thy "List";
    4.10  
     5.1 --- a/src/ZF/Tools/datatype_package.ML	Wed Jan 06 13:23:41 1999 +0100
     5.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed Jan 06 13:24:33 1999 +0100
     5.3 @@ -1,9 +1,9 @@
     5.4 -(*  Title:      ZF/datatype_package.ML
     5.5 +(*  Title:      ZF/Tools/datatype_package.ML
     5.6      ID:         $Id$
     5.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.8      Copyright   1994  University of Cambridge
     5.9  
    5.10 -Fixedpoint definition module -- for Inductive/Codatatype Definitions
    5.11 +Datatype/Codatatype Definitions
    5.12  
    5.13  The functor will be instantiated for normal sums/products (datatype defs)
    5.14                           and non-standard sums/products (codatatype defs)
    5.15 @@ -243,7 +243,7 @@
    5.16      | rec_args ((Const("op :",_)$arg$X)::prems) =
    5.17         (case head_of X of
    5.18  	    Const(a,_) => (*recursive occurrence?*)
    5.19 -			  if Sign.base_name a mem_string rec_base_names
    5.20 +			  if a mem_string rec_names
    5.21  			      then arg :: rec_args prems 
    5.22  			  else rec_args prems
    5.23  	  | _ => rec_args prems)
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Jan 06 13:24:33 1999 +0100
     6.3 @@ -0,0 +1,68 @@
     6.4 +(*  Title:      HOL/Tools/induct_tacs.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 +    Copyright   1994  University of Cambridge
     6.8 +
     6.9 +Induction and exhaustion tactics for Isabelle/ZF
    6.10 +*)
    6.11 +
    6.12 +
    6.13 +signature DATATYPE_TACTICS =
    6.14 +sig
    6.15 +  val induct_tac : string -> int -> tactic
    6.16 +  val exhaust_tac : string -> int -> tactic
    6.17 +end;
    6.18 +
    6.19 +
    6.20 +structure DatatypeTactics : DATATYPE_TACTICS =
    6.21 +struct
    6.22 +
    6.23 +fun datatype_info_sg sign name =
    6.24 +  (case Symtab.lookup (DatatypesData.get_sg sign, name) of
    6.25 +    Some info => info
    6.26 +  | None => error ("Unknown datatype " ^ quote name));
    6.27 +
    6.28 +
    6.29 +(*Given a variable, find the inductive set associated it in the assumptions*)
    6.30 +fun find_tname var Bi =
    6.31 +  let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) = 
    6.32 +             (v, #1 (dest_Const (head_of A)))
    6.33 +	| mk_pair _ = raise Match
    6.34 +      val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop))
    6.35 +	  (#2 (strip_context Bi))
    6.36 +  in case assoc (pairs, var) of
    6.37 +       None => error ("Cannot determine datatype of " ^ quote var)
    6.38 +     | Some t => t
    6.39 +  end;
    6.40 +
    6.41 +(** generic exhaustion and induction tactic for datatypes 
    6.42 +    Differences from HOL: 
    6.43 +      (1) no checking if the induction var occurs in premises, since it always
    6.44 +          appears in one of them, and it's hard to check for other occurrences
    6.45 +      (2) exhaustion works for VARIABLES in the premises, not general terms
    6.46 +**)
    6.47 +
    6.48 +fun exhaust_induct_tac exh var i state =
    6.49 +  let
    6.50 +    val (_, _, Bi, _) = dest_state (state, i)
    6.51 +    val {sign, ...} = rep_thm state
    6.52 +    val tn = find_tname var Bi
    6.53 +    val rule = 
    6.54 +	if exh then #exhaustion (datatype_info_sg sign tn)
    6.55 +	       else #induct  (datatype_info_sg sign tn)
    6.56 +    val (Const("op :",_) $ Var(ixn,_) $ _) = 
    6.57 +	FOLogic.dest_Trueprop (hd (prems_of rule))
    6.58 +    val ind_vname = Syntax.string_of_vname ixn
    6.59 +    val vname' = (*delete leading question mark*)
    6.60 +	String.substring (ind_vname, 1, size ind_vname-1)
    6.61 +  in
    6.62 +    eres_inst_tac [(vname',var)] rule i state
    6.63 +  end;
    6.64 +
    6.65 +val exhaust_tac = exhaust_induct_tac true;
    6.66 +val induct_tac = exhaust_induct_tac false;
    6.67 +
    6.68 +end;
    6.69 +
    6.70 +
    6.71 +open DatatypeTactics;
     7.1 --- a/src/ZF/Tools/primrec_package.ML	Wed Jan 06 13:23:41 1999 +0100
     7.2 +++ b/src/ZF/Tools/primrec_package.ML	Wed Jan 06 13:24:33 1999 +0100
     7.3 @@ -149,7 +149,10 @@
     7.4  		     $ rec_arg)
     7.5  
     7.6    in
     7.7 -      writeln ("def = " ^ Sign.string_of_term (sign_of thy) def_tm);
     7.8 +      if !Ind_Syntax.trace then
     7.9 +	    writeln ("primrec def:\n" ^ 
    7.10 +		     Sign.string_of_term (sign_of thy) def_tm)
    7.11 +      else();
    7.12        (Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def",
    7.13         def_tm)
    7.14    end;
    7.15 @@ -169,14 +172,16 @@
    7.16                     |> Theory.add_defs_i [def]
    7.17      val rewrites = get_axiom thy' (#1 def) ::
    7.18  	           map mk_meta_eq (#rec_rewrites con_info)
    7.19 -    val _ = writeln ("Proving equations for primrec function " ^ fname);
    7.20      val char_thms = 
    7.21 -	map (fn (_,t) => 
    7.22 -	     prove_goalw_cterm rewrites
    7.23 -	       (Ind_Syntax.traceIt "next primrec equation = "
    7.24 -		(cterm_of (sign_of thy') t))
    7.25 -	     (fn _ => [rtac refl 1]))
    7.26 -	recursion_eqns;
    7.27 +	(if !Ind_Syntax.trace then
    7.28 +	     writeln ("Proving equations for primrec function " ^ fname)
    7.29 +	 else ();
    7.30 +	 map (fn (_,t) => 
    7.31 +	      prove_goalw_cterm rewrites
    7.32 +		(Ind_Syntax.traceIt "next primrec equation = "
    7.33 +		 (cterm_of (sign_of thy') t))
    7.34 +	      (fn _ => [rtac refl 1]))
    7.35 +	 recursion_eqns);
    7.36      val tsimps = Attribute.tthms_of char_thms;
    7.37      val thy'' = thy' 
    7.38        |> PureThy.add_tthmss [(("simps", tsimps), [Simplifier.simp_add_global])]
     8.1 --- a/src/ZF/Zorn.ML	Wed Jan 06 13:23:41 1999 +0100
     8.2 +++ b/src/ZF/Zorn.ML	Wed Jan 06 13:24:33 1999 +0100
     8.3 @@ -49,12 +49,6 @@
     8.4  by (ALLGOALS (fast_tac (claset() addIs prems)));
     8.5  qed "TFin_induct";
     8.6  
     8.7 -(*Perform induction on n, then prove the major premise using prems. *)
     8.8 -fun TFin_ind_tac a prems i = 
     8.9 -    EVERY [res_inst_tac [("n",a)] TFin_induct i,
    8.10 -           rename_last_tac a ["1"] (i+1),
    8.11 -           rename_last_tac a ["2"] (i+2),
    8.12 -           ares_tac prems i];
    8.13  
    8.14  (*** Section 3.  Some Properties of the Transfinite Construction ***)
    8.15  
     9.1 --- a/src/ZF/ex/BT.ML	Wed Jan 06 13:23:41 1999 +0100
     9.2 +++ b/src/ZF/ex/BT.ML	Wed Jan 06 13:24:33 1999 +0100
     9.3 @@ -6,13 +6,6 @@
     9.4  Datatype definition of binary trees
     9.5  *)
     9.6  
     9.7 -(*Perform induction on l, then prove the major premise using prems. *)
     9.8 -fun bt_ind_tac a prems i = 
     9.9 -    EVERY [res_inst_tac [("x",a)] bt.induct i,
    9.10 -           rename_last_tac a ["1","2"] (i+2),
    9.11 -           ares_tac prems i];
    9.12 -
    9.13 -
    9.14  Addsimps bt.intrs;
    9.15  
    9.16  (**  Lemmas to justify using "bt" in other recursive type definitions **)
    9.17 @@ -34,20 +27,21 @@
    9.18  
    9.19  
    9.20  (*Type checking -- proved by induction, as usual*)
    9.21 -val prems = goal BT.thy
    9.22 +val major::prems = goal BT.thy
    9.23      "[| t: bt(A);    \
    9.24  \       c: C(Lf);       \
    9.25  \       !!x y z r s. [| x:A;  y:bt(A);  z:bt(A);  r:C(y);  s:C(z) |] ==> \
    9.26  \                    h(x,y,z,r,s): C(Br(x,y,z))  \
    9.27  \    |] ==> bt_rec(c,h,t) : C(t)";
    9.28 -by (bt_ind_tac "t" prems 1);
    9.29 +    (*instead of induct_tac "t", since t: bt(A) isn't an assumption*)
    9.30 +by (rtac (major RS bt.induct) 1);
    9.31  by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
    9.32  qed "bt_rec_type";
    9.33  
    9.34  (** n_nodes **)
    9.35  
    9.36  Goal "t: bt(A) ==> n_nodes(t) : nat";
    9.37 -by (bt_ind_tac "t" [] 1);
    9.38 +by (induct_tac "t" 1);
    9.39  by Auto_tac;
    9.40  qed "n_nodes_type";
    9.41  
    9.42 @@ -55,14 +49,14 @@
    9.43  (** n_leaves **)
    9.44  
    9.45  Goal "t: bt(A) ==> n_leaves(t) : nat";
    9.46 -by (bt_ind_tac "t" [] 1);
    9.47 +by (induct_tac "t" 1);
    9.48  by Auto_tac;
    9.49  qed "n_leaves_type";
    9.50  
    9.51  (** bt_reflect **)
    9.52  
    9.53  Goal "t: bt(A) ==> bt_reflect(t) : bt(A)";
    9.54 -by (bt_ind_tac "t" [] 1);
    9.55 +by (induct_tac "t" 1);
    9.56  by Auto_tac;
    9.57  by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1));
    9.58  qed "bt_reflect_type";
    9.59 @@ -76,23 +70,20 @@
    9.60  
    9.61  (*** theorems about n_leaves ***)
    9.62  
    9.63 -val prems = goal BT.thy
    9.64 -    "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
    9.65 -by (bt_ind_tac "t" prems 1);
    9.66 +Goal "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
    9.67 +by (induct_tac "t" 1);
    9.68  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute, n_leaves_type])));
    9.69  qed "n_leaves_reflect";
    9.70  
    9.71 -val prems = goal BT.thy
    9.72 -    "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
    9.73 -by (bt_ind_tac "t" prems 1);
    9.74 +Goal "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
    9.75 +by (induct_tac "t" 1);
    9.76  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_succ_right])));
    9.77  qed "n_leaves_nodes";
    9.78  
    9.79  (*** theorems about bt_reflect ***)
    9.80  
    9.81 -val prems = goal BT.thy
    9.82 -    "t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
    9.83 -by (bt_ind_tac "t" prems 1);
    9.84 +Goal "t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
    9.85 +by (induct_tac "t" 1);
    9.86  by (ALLGOALS Asm_simp_tac);
    9.87  qed "bt_reflect_bt_reflect_ident";
    9.88  
    10.1 --- a/src/ZF/ex/Primrec.ML	Wed Jan 06 13:23:41 1999 +0100
    10.2 +++ b/src/ZF/ex/Primrec.ML	Wed Jan 06 13:24:33 1999 +0100
    10.3 @@ -175,9 +175,8 @@
    10.4  
    10.5  Addsimps [list_add_type, nat_into_Ord];
    10.6  
    10.7 -Goalw [SC_def]
    10.8 -    "l: list(nat) ==> SC ` l < ack(1, list_add(l))";
    10.9 -by (etac list.elim 1);
   10.10 +Goalw [SC_def] "l: list(nat) ==> SC ` l < ack(1, list_add(l))";
   10.11 +by (exhaust_tac "l" 1);
   10.12  by (asm_simp_tac (simpset() addsimps [succ_iff]) 1);
   10.13  by (asm_simp_tac (simpset() addsimps [ack_1, add_le_self]) 1);
   10.14  qed "SC_case";
   10.15 @@ -258,7 +257,7 @@
   10.16  \           g: prim_rec;  kg: nat;                                       \
   10.17  \           l: list(nat)                                                \
   10.18  \        |] ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))";
   10.19 -by (etac list.elim 1);
   10.20 +by (exhaust_tac "l" 1);
   10.21  by (asm_simp_tac (simpset() addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
   10.22  by (Asm_simp_tac 1);
   10.23  by (etac ssubst 1);  (*get rid of the needless assumption*)