ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
authorlcp
Thu Sep 30 10:10:21 1993 +0100 (1993-09-30)
changeset 141c0926788772
parent 13 b73f7e42135e
child 15 6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext

domrange/image_subset,vimage_subset: deleted needless premise!
misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem

ind-syntax/rule_concl: recoded to avoid exceptions
intr-elim: now checks conclusions of introduction rules

func/fun_disjoint_Un: now uses ex_ex1I
list-fn/hd,tl,drop: new
simpdata/bquant_simps: new

list/list_case_type: restored!

bool.thy: changed 1 from a "def" to a translation
Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML

nat/succ_less_induct: new induction principle
arith/add_mono: new results about monotonicity

simpdata/mem_simps: removed the ones for succ and cons; added succI1,
consI2 to ZF_ss

upair/succ_iff: new, for use with simp_tac (cons_iff already existed)

ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ
nat/nat_0_in_succ: new

ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
src/ZF/Arith.ML
src/ZF/Bool.ML
src/ZF/Bool.thy
src/ZF/Epsilon.ML
src/ZF/Fixedpt.ML
src/ZF/ROOT.ML
src/ZF/arith.ML
src/ZF/bool.ML
src/ZF/bool.thy
src/ZF/domrange.ML
src/ZF/epsilon.ML
src/ZF/fixedpt.ML
src/ZF/func.ML
src/ZF/ind-syntax.ML
src/ZF/ind_syntax.ML
src/ZF/intr-elim.ML
src/ZF/intr_elim.ML
src/ZF/list.ML
src/ZF/listfn.ML
src/ZF/listfn.thy
src/ZF/nat.ML
src/ZF/ord.ML
src/ZF/quniv.ML
src/ZF/simpdata.ML
src/ZF/univ.ML
src/ZF/upair.ML
     1.1 --- a/src/ZF/Arith.ML	Fri Sep 24 11:27:15 1993 +0200
     1.2 +++ b/src/ZF/Arith.ML	Thu Sep 30 10:10:21 1993 +0100
     1.3 @@ -28,10 +28,8 @@
     1.4  val rec_0 = result();
     1.5  
     1.6  goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
     1.7 -val rec_ss = ZF_ss 
     1.8 -      addsimps [nat_case_succ, nat_succI];
     1.9  by (rtac rec_trans 1);
    1.10 -by (simp_tac rec_ss 1);
    1.11 +by (simp_tac (ZF_ss addsimps [nat_case_succ, nat_succI]) 1);
    1.12  val rec_succ = result();
    1.13  
    1.14  val major::prems = goal Arith.thy
    1.15 @@ -103,6 +101,7 @@
    1.16      (nat_ind_tac "n" prems 1),
    1.17      (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
    1.18  
    1.19 +(*The conclusion is equivalent to m#-n <= m *)
    1.20  val prems = goal Arith.thy 
    1.21      "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
    1.22  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.23 @@ -111,8 +110,9 @@
    1.24  by (etac succE 3);
    1.25  by (ALLGOALS
    1.26      (asm_simp_tac
    1.27 -     (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
    1.28 -val diff_leq = result();
    1.29 +     (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0, 
    1.30 +				diff_succ_succ]))));
    1.31 +val diff_less_succ = result();
    1.32  
    1.33  (*** Simplification over add, mult, diff ***)
    1.34  
    1.35 @@ -193,10 +193,10 @@
    1.36  
    1.37  (*addition distributes over multiplication*)
    1.38  val add_mult_distrib = prove_goal Arith.thy 
    1.39 -    "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
    1.40 - (fn prems=>
    1.41 -  [ (nat_ind_tac "m" prems 1),
    1.42 -    (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
    1.43 +    "!!m n. [| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
    1.44 + (fn _=>
    1.45 +  [ (etac nat_induct 1),
    1.46 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]);
    1.47  
    1.48  (*Distributive law on the left; requires an extra typing premise*)
    1.49  val add_mult_distrib_left = prove_goal Arith.thy 
    1.50 @@ -209,10 +209,10 @@
    1.51  
    1.52  (*Associative law for multiplication*)
    1.53  val mult_assoc = prove_goal Arith.thy 
    1.54 -    "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
    1.55 - (fn prems=>
    1.56 -  [ (nat_ind_tac "m" prems 1),
    1.57 -    (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
    1.58 +    "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
    1.59 + (fn _=>
    1.60 +  [ (etac nat_induct 1),
    1.61 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]);
    1.62  
    1.63  
    1.64  (*** Difference ***)
    1.65 @@ -231,8 +231,8 @@
    1.66  by (resolve_tac prems 1);
    1.67  by (resolve_tac prems 1);
    1.68  by (ALLGOALS (asm_simp_tac
    1.69 -	      (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ, 
    1.70 -				  naturals_are_ordinals]))));
    1.71 +	      (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ,
    1.72 +					 naturals_are_ordinals]))));
    1.73  val add_diff_inverse = result();
    1.74  
    1.75  
    1.76 @@ -257,7 +257,7 @@
    1.77  by (etac rev_mp 1);
    1.78  by (etac rev_mp 1);
    1.79  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.80 -by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
    1.81 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ])));
    1.82  val div_termination = result();
    1.83  
    1.84  val div_rls =
    1.85 @@ -335,6 +335,65 @@
    1.86  (*May not simplify even with ZF_ss because it would expand m:succ(...) *)
    1.87  by (rtac (add_0 RS ssubst) 1);
    1.88  by (rtac (add_succ RS ssubst) 2);
    1.89 -by (REPEAT (ares_tac [nnat, Ord_0_mem_succ, succ_mem_succI, 
    1.90 +by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI, 
    1.91  		      naturals_are_ordinals, nat_succI, add_type] 1));
    1.92  val add_less_succ_self = result();
    1.93 +
    1.94 +goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= m #+ n";
    1.95 +by (rtac (add_less_succ_self RS member_succD) 1);
    1.96 +by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1));
    1.97 +val add_leq_self = result();
    1.98 +
    1.99 +goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= n #+ m";
   1.100 +by (rtac (add_commute RS ssubst) 1);
   1.101 +by (REPEAT (ares_tac [add_leq_self] 1));
   1.102 +val add_leq_self2 = result();
   1.103 +
   1.104 +(** Monotonicity of addition **)
   1.105 +
   1.106 +(*strict, in 1st argument*)
   1.107 +goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k";
   1.108 +by (etac succ_less_induct 1);
   1.109 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff])));
   1.110 +val add_less_mono1 = result();
   1.111 +
   1.112 +(*strict, in both arguments*)
   1.113 +goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l";
   1.114 +by (rtac (add_less_mono1 RS Ord_trans) 1);
   1.115 +by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals]));
   1.116 +by (EVERY [rtac (add_commute RS ssubst) 1,
   1.117 +	   rtac (add_commute RS ssubst) 3,
   1.118 +	   rtac add_less_mono1 5]);
   1.119 +by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1));
   1.120 +val add_less_mono = result();
   1.121 +
   1.122 +(*A [clumsy] way of lifting < monotonictity to <= monotonicity *)
   1.123 +val less_mono::ford::prems = goal Ord.thy
   1.124 +     "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j);	\
   1.125 +\        !!i. i:k ==> f(i):k;			\
   1.126 +\        i<=j;  i:k;  j:k;  Ord(k)		\
   1.127 +\     |] ==> f(i) <= f(j)";
   1.128 +by (cut_facts_tac prems 1);
   1.129 +by (rtac member_succD 1);
   1.130 +by (dtac member_succI 1);
   1.131 +by (fast_tac (ZF_cs addSIs [less_mono]) 3);
   1.132 +by (REPEAT (ares_tac [ford,Ord_in_Ord] 1));
   1.133 +val Ord_less_mono_imp_mono = result();
   1.134 +
   1.135 +(*<=, in 1st argument*)
   1.136 +goal Arith.thy
   1.137 +    "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k";
   1.138 +by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1);
   1.139 +by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1));
   1.140 +val add_mono1 = result();
   1.141 +
   1.142 +(*<=, in both arguments*)
   1.143 +goal Arith.thy
   1.144 +    "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l";
   1.145 +by (rtac (add_mono1 RS subset_trans) 1);
   1.146 +by (REPEAT (assume_tac 1));
   1.147 +by (EVERY [rtac (add_commute RS ssubst) 1,
   1.148 +	   rtac (add_commute RS ssubst) 3,
   1.149 +	   rtac add_mono1 5]);
   1.150 +by (REPEAT (assume_tac 1));
   1.151 +val add_mono = result();
     2.1 --- a/src/ZF/Bool.ML	Fri Sep 24 11:27:15 1993 +0200
     2.2 +++ b/src/ZF/Bool.ML	Thu Sep 30 10:10:21 1993 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  
     2.5  open Bool;
     2.6  
     2.7 -val bool_defs = [bool_def,one_def,cond_def];
     2.8 +val bool_defs = [bool_def,cond_def];
     2.9  
    2.10  (* Introduction rules *)
    2.11  
     3.1 --- a/src/ZF/Bool.thy	Fri Sep 24 11:27:15 1993 +0200
     3.2 +++ b/src/ZF/Bool.thy	Thu Sep 30 10:10:21 1993 +0100
     3.3 @@ -16,8 +16,10 @@
     3.4      or		::      "[i,i]=>i"      (infixl 65)
     3.5      xor		::      "[i,i]=>i"      (infixl 65)
     3.6  
     3.7 +translations
     3.8 +   "1"  == "succ(0)"
     3.9 +
    3.10  rules
    3.11 -    one_def 	"1    == succ(0)"
    3.12      bool_def	"bool == {0,1}"
    3.13      cond_def	"cond(b,c,d) == if(b=1,c,d)"
    3.14      not_def	"not(b) == cond(b,0,1)"
     4.1 --- a/src/ZF/Epsilon.ML	Fri Sep 24 11:27:15 1993 +0200
     4.2 +++ b/src/ZF/Epsilon.ML	Thu Sep 30 10:10:21 1993 +0100
     4.3 @@ -12,7 +12,7 @@
     4.4  
     4.5  goalw Epsilon.thy [eclose_def] "A <= eclose(A)";
     4.6  by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1);
     4.7 -br (nat_0I RS UN_upper) 1;
     4.8 +by (rtac (nat_0I RS UN_upper) 1);
     4.9  val arg_subset_eclose = result();
    4.10  
    4.11  val arg_into_eclose = arg_subset_eclose RS subsetD;
    4.12 @@ -71,7 +71,7 @@
    4.13  
    4.14  goalw Epsilon.thy [eclose_def]
    4.15       "!!X A. [| Transset(X);  A<=X |] ==> eclose(A) <= X";
    4.16 -br (eclose_least_lemma RS UN_least) 1;
    4.17 +by (rtac (eclose_least_lemma RS UN_least) 1);
    4.18  by (REPEAT (assume_tac 1));
    4.19  val eclose_least = result();
    4.20  
    4.21 @@ -90,8 +90,8 @@
    4.22  val eclose_induct_down = result();
    4.23  
    4.24  goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X";
    4.25 -be ([eclose_least, arg_subset_eclose] MRS equalityI) 1;
    4.26 -br subset_refl 1;
    4.27 +by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1);
    4.28 +by (rtac subset_refl 1);
    4.29  val Transset_eclose_eq_arg = result();
    4.30  
    4.31  
    4.32 @@ -233,8 +233,8 @@
    4.33  
    4.34  goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
    4.35  by (rtac (rank RS trans) 1);
    4.36 -br ([UN_least, succI1 RS UN_upper] MRS equalityI) 1;
    4.37 -be succE 1;
    4.38 +by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
    4.39 +by (etac succE 1);
    4.40  by (fast_tac ZF_cs 1);
    4.41  by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1));
    4.42  val rank_succ = result();
     5.1 --- a/src/ZF/Fixedpt.ML	Fri Sep 24 11:27:15 1993 +0200
     5.2 +++ b/src/ZF/Fixedpt.ML	Thu Sep 30 10:10:21 1993 +0100
     5.3 @@ -88,7 +88,7 @@
     5.4  val prems = goalw Fixedpt.thy [lfp_def]
     5.5      "[| h(D) <= D;  !!X. [| h(X) <= X;  X<=D |] ==> A<=X |] ==> \
     5.6  \    A <= lfp(D,h)";
     5.7 -br (Pow_top RS CollectI RS Inter_greatest) 1;
     5.8 +by (rtac (Pow_top RS CollectI RS Inter_greatest) 1);
     5.9  by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1));
    5.10  val lfp_greatest = result();
    5.11  
    5.12 @@ -174,8 +174,8 @@
    5.13  val [hmono,imono,subhi] = goal Fixedpt.thy
    5.14      "[| bnd_mono(D,h);  bnd_mono(E,i); 		\
    5.15  \       !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(E,i)";
    5.16 -br (bnd_monoD1 RS lfp_greatest) 1;
    5.17 -br imono 1;
    5.18 +by (rtac (bnd_monoD1 RS lfp_greatest) 1);
    5.19 +by (rtac imono 1);
    5.20  by (rtac (hmono RSN (2, lfp_Int_lowerbound)) 1);
    5.21  by (rtac (Int_lower1 RS subhi RS subset_trans) 1);
    5.22  by (rtac (imono RS bnd_monoD2 RS subset_trans) 1);
    5.23 @@ -186,10 +186,10 @@
    5.24    but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)
    5.25  val [isubD,subhi] = goal Fixedpt.thy
    5.26      "[| i(D) <= D;  !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(D,i)";
    5.27 -br lfp_greatest 1;
    5.28 -br isubD 1;
    5.29 +by (rtac lfp_greatest 1);
    5.30 +by (rtac isubD 1);
    5.31  by (rtac lfp_lowerbound 1);
    5.32 -be (subhi RS subset_trans) 1;
    5.33 +by (etac (subhi RS subset_trans) 1);
    5.34  by (REPEAT (assume_tac 1));
    5.35  val lfp_mono2 = result();
    5.36  
     6.1 --- a/src/ZF/ROOT.ML	Fri Sep 24 11:27:15 1993 +0200
     6.2 +++ b/src/ZF/ROOT.ML	Thu Sep 30 10:10:21 1993 +0100
     6.3 @@ -11,20 +11,7 @@
     6.4  val banner = "ZF Set Theory (in FOL)";
     6.5  writeln banner;
     6.6  
     6.7 -(*For Pure/drule??  Multiple resolution infixes*)
     6.8 -infix 0 MRS MRL;
     6.9 -
    6.10 -(*Resolve a list of rules against bottom_rl from right to left*)
    6.11 -fun rls MRS bottom_rl = 
    6.12 -  let fun rs_aux i [] = bottom_rl
    6.13 -	| rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
    6.14 -  in  rs_aux 1 rls  end;
    6.15 -
    6.16 -fun rlss MRL bottom_rls = 
    6.17 -  let fun rs_aux i [] = bottom_rls
    6.18 -	| rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
    6.19 -  in  rs_aux 1 rlss  end;
    6.20 -
    6.21 +(*For Pure/tactic??  A crude way of adding structure to rules*)
    6.22  fun CHECK_SOLVED (Tactic tf) = 
    6.23    Tactic (fn state => 
    6.24      case Sequence.pull (tf state) of
     7.1 --- a/src/ZF/arith.ML	Fri Sep 24 11:27:15 1993 +0200
     7.2 +++ b/src/ZF/arith.ML	Thu Sep 30 10:10:21 1993 +0100
     7.3 @@ -28,10 +28,8 @@
     7.4  val rec_0 = result();
     7.5  
     7.6  goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
     7.7 -val rec_ss = ZF_ss 
     7.8 -      addsimps [nat_case_succ, nat_succI];
     7.9  by (rtac rec_trans 1);
    7.10 -by (simp_tac rec_ss 1);
    7.11 +by (simp_tac (ZF_ss addsimps [nat_case_succ, nat_succI]) 1);
    7.12  val rec_succ = result();
    7.13  
    7.14  val major::prems = goal Arith.thy
    7.15 @@ -103,6 +101,7 @@
    7.16      (nat_ind_tac "n" prems 1),
    7.17      (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
    7.18  
    7.19 +(*The conclusion is equivalent to m#-n <= m *)
    7.20  val prems = goal Arith.thy 
    7.21      "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
    7.22  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    7.23 @@ -111,8 +110,9 @@
    7.24  by (etac succE 3);
    7.25  by (ALLGOALS
    7.26      (asm_simp_tac
    7.27 -     (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
    7.28 -val diff_leq = result();
    7.29 +     (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0, 
    7.30 +				diff_succ_succ]))));
    7.31 +val diff_less_succ = result();
    7.32  
    7.33  (*** Simplification over add, mult, diff ***)
    7.34  
    7.35 @@ -193,10 +193,10 @@
    7.36  
    7.37  (*addition distributes over multiplication*)
    7.38  val add_mult_distrib = prove_goal Arith.thy 
    7.39 -    "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
    7.40 - (fn prems=>
    7.41 -  [ (nat_ind_tac "m" prems 1),
    7.42 -    (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
    7.43 +    "!!m n. [| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
    7.44 + (fn _=>
    7.45 +  [ (etac nat_induct 1),
    7.46 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]);
    7.47  
    7.48  (*Distributive law on the left; requires an extra typing premise*)
    7.49  val add_mult_distrib_left = prove_goal Arith.thy 
    7.50 @@ -209,10 +209,10 @@
    7.51  
    7.52  (*Associative law for multiplication*)
    7.53  val mult_assoc = prove_goal Arith.thy 
    7.54 -    "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
    7.55 - (fn prems=>
    7.56 -  [ (nat_ind_tac "m" prems 1),
    7.57 -    (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
    7.58 +    "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
    7.59 + (fn _=>
    7.60 +  [ (etac nat_induct 1),
    7.61 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]);
    7.62  
    7.63  
    7.64  (*** Difference ***)
    7.65 @@ -231,8 +231,8 @@
    7.66  by (resolve_tac prems 1);
    7.67  by (resolve_tac prems 1);
    7.68  by (ALLGOALS (asm_simp_tac
    7.69 -	      (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ, 
    7.70 -				  naturals_are_ordinals]))));
    7.71 +	      (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ,
    7.72 +					 naturals_are_ordinals]))));
    7.73  val add_diff_inverse = result();
    7.74  
    7.75  
    7.76 @@ -257,7 +257,7 @@
    7.77  by (etac rev_mp 1);
    7.78  by (etac rev_mp 1);
    7.79  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    7.80 -by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
    7.81 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ])));
    7.82  val div_termination = result();
    7.83  
    7.84  val div_rls =
    7.85 @@ -335,6 +335,65 @@
    7.86  (*May not simplify even with ZF_ss because it would expand m:succ(...) *)
    7.87  by (rtac (add_0 RS ssubst) 1);
    7.88  by (rtac (add_succ RS ssubst) 2);
    7.89 -by (REPEAT (ares_tac [nnat, Ord_0_mem_succ, succ_mem_succI, 
    7.90 +by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI, 
    7.91  		      naturals_are_ordinals, nat_succI, add_type] 1));
    7.92  val add_less_succ_self = result();
    7.93 +
    7.94 +goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= m #+ n";
    7.95 +by (rtac (add_less_succ_self RS member_succD) 1);
    7.96 +by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1));
    7.97 +val add_leq_self = result();
    7.98 +
    7.99 +goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= n #+ m";
   7.100 +by (rtac (add_commute RS ssubst) 1);
   7.101 +by (REPEAT (ares_tac [add_leq_self] 1));
   7.102 +val add_leq_self2 = result();
   7.103 +
   7.104 +(** Monotonicity of addition **)
   7.105 +
   7.106 +(*strict, in 1st argument*)
   7.107 +goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k";
   7.108 +by (etac succ_less_induct 1);
   7.109 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff])));
   7.110 +val add_less_mono1 = result();
   7.111 +
   7.112 +(*strict, in both arguments*)
   7.113 +goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l";
   7.114 +by (rtac (add_less_mono1 RS Ord_trans) 1);
   7.115 +by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals]));
   7.116 +by (EVERY [rtac (add_commute RS ssubst) 1,
   7.117 +	   rtac (add_commute RS ssubst) 3,
   7.118 +	   rtac add_less_mono1 5]);
   7.119 +by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1));
   7.120 +val add_less_mono = result();
   7.121 +
   7.122 +(*A [clumsy] way of lifting < monotonictity to <= monotonicity *)
   7.123 +val less_mono::ford::prems = goal Ord.thy
   7.124 +     "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j);	\
   7.125 +\        !!i. i:k ==> f(i):k;			\
   7.126 +\        i<=j;  i:k;  j:k;  Ord(k)		\
   7.127 +\     |] ==> f(i) <= f(j)";
   7.128 +by (cut_facts_tac prems 1);
   7.129 +by (rtac member_succD 1);
   7.130 +by (dtac member_succI 1);
   7.131 +by (fast_tac (ZF_cs addSIs [less_mono]) 3);
   7.132 +by (REPEAT (ares_tac [ford,Ord_in_Ord] 1));
   7.133 +val Ord_less_mono_imp_mono = result();
   7.134 +
   7.135 +(*<=, in 1st argument*)
   7.136 +goal Arith.thy
   7.137 +    "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k";
   7.138 +by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1);
   7.139 +by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1));
   7.140 +val add_mono1 = result();
   7.141 +
   7.142 +(*<=, in both arguments*)
   7.143 +goal Arith.thy
   7.144 +    "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l";
   7.145 +by (rtac (add_mono1 RS subset_trans) 1);
   7.146 +by (REPEAT (assume_tac 1));
   7.147 +by (EVERY [rtac (add_commute RS ssubst) 1,
   7.148 +	   rtac (add_commute RS ssubst) 3,
   7.149 +	   rtac add_mono1 5]);
   7.150 +by (REPEAT (assume_tac 1));
   7.151 +val add_mono = result();
     8.1 --- a/src/ZF/bool.ML	Fri Sep 24 11:27:15 1993 +0200
     8.2 +++ b/src/ZF/bool.ML	Thu Sep 30 10:10:21 1993 +0100
     8.3 @@ -8,7 +8,7 @@
     8.4  
     8.5  open Bool;
     8.6  
     8.7 -val bool_defs = [bool_def,one_def,cond_def];
     8.8 +val bool_defs = [bool_def,cond_def];
     8.9  
    8.10  (* Introduction rules *)
    8.11  
     9.1 --- a/src/ZF/bool.thy	Fri Sep 24 11:27:15 1993 +0200
     9.2 +++ b/src/ZF/bool.thy	Thu Sep 30 10:10:21 1993 +0100
     9.3 @@ -16,8 +16,10 @@
     9.4      or		::      "[i,i]=>i"      (infixl 65)
     9.5      xor		::      "[i,i]=>i"      (infixl 65)
     9.6  
     9.7 +translations
     9.8 +   "1"  == "succ(0)"
     9.9 +
    9.10  rules
    9.11 -    one_def 	"1    == succ(0)"
    9.12      bool_def	"bool == {0,1}"
    9.13      cond_def	"cond(b,c,d) == if(b=1,c,d)"
    9.14      not_def	"not(b) == cond(b,0,1)"
    10.1 --- a/src/ZF/domrange.ML	Fri Sep 24 11:27:15 1993 +0200
    10.2 +++ b/src/ZF/domrange.ML	Thu Sep 30 10:10:21 1993 +0100
    10.3 @@ -174,7 +174,7 @@
    10.4      (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
    10.5  
    10.6  val image_subset = prove_goal ZF.thy
    10.7 -    "!!A B r. [| r <= A*B;  C<=A |] ==> r``C <= B"
    10.8 +    "!!A B r. r <= A*B ==> r``C <= B"
    10.9   (fn _ =>
   10.10    [ (rtac subsetI 1),
   10.11      (REPEAT (eresolve_tac [asm_rl, imageE, subsetD RS SigmaD2] 1)) ]);
   10.12 @@ -202,8 +202,8 @@
   10.13      (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]);
   10.14  
   10.15  val vimage_subset = prove_goalw ZF.thy [vimage_def]
   10.16 -    "!!A B r. [| r <= A*B;  C<=B |] ==> r-``C <= A"
   10.17 - (fn _ => [ (REPEAT (ares_tac [converse_type RS image_subset] 1)) ]);
   10.18 +    "!!A B r. r <= A*B ==> r-``C <= A"
   10.19 + (fn _ => [ (etac (converse_type RS image_subset) 1) ]);
   10.20  
   10.21  
   10.22  (** Theorem-proving for ZF set theory **)
    11.1 --- a/src/ZF/epsilon.ML	Fri Sep 24 11:27:15 1993 +0200
    11.2 +++ b/src/ZF/epsilon.ML	Thu Sep 30 10:10:21 1993 +0100
    11.3 @@ -12,7 +12,7 @@
    11.4  
    11.5  goalw Epsilon.thy [eclose_def] "A <= eclose(A)";
    11.6  by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1);
    11.7 -br (nat_0I RS UN_upper) 1;
    11.8 +by (rtac (nat_0I RS UN_upper) 1);
    11.9  val arg_subset_eclose = result();
   11.10  
   11.11  val arg_into_eclose = arg_subset_eclose RS subsetD;
   11.12 @@ -71,7 +71,7 @@
   11.13  
   11.14  goalw Epsilon.thy [eclose_def]
   11.15       "!!X A. [| Transset(X);  A<=X |] ==> eclose(A) <= X";
   11.16 -br (eclose_least_lemma RS UN_least) 1;
   11.17 +by (rtac (eclose_least_lemma RS UN_least) 1);
   11.18  by (REPEAT (assume_tac 1));
   11.19  val eclose_least = result();
   11.20  
   11.21 @@ -90,8 +90,8 @@
   11.22  val eclose_induct_down = result();
   11.23  
   11.24  goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X";
   11.25 -be ([eclose_least, arg_subset_eclose] MRS equalityI) 1;
   11.26 -br subset_refl 1;
   11.27 +by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1);
   11.28 +by (rtac subset_refl 1);
   11.29  val Transset_eclose_eq_arg = result();
   11.30  
   11.31  
   11.32 @@ -233,8 +233,8 @@
   11.33  
   11.34  goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
   11.35  by (rtac (rank RS trans) 1);
   11.36 -br ([UN_least, succI1 RS UN_upper] MRS equalityI) 1;
   11.37 -be succE 1;
   11.38 +by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
   11.39 +by (etac succE 1);
   11.40  by (fast_tac ZF_cs 1);
   11.41  by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1));
   11.42  val rank_succ = result();
    12.1 --- a/src/ZF/fixedpt.ML	Fri Sep 24 11:27:15 1993 +0200
    12.2 +++ b/src/ZF/fixedpt.ML	Thu Sep 30 10:10:21 1993 +0100
    12.3 @@ -88,7 +88,7 @@
    12.4  val prems = goalw Fixedpt.thy [lfp_def]
    12.5      "[| h(D) <= D;  !!X. [| h(X) <= X;  X<=D |] ==> A<=X |] ==> \
    12.6  \    A <= lfp(D,h)";
    12.7 -br (Pow_top RS CollectI RS Inter_greatest) 1;
    12.8 +by (rtac (Pow_top RS CollectI RS Inter_greatest) 1);
    12.9  by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1));
   12.10  val lfp_greatest = result();
   12.11  
   12.12 @@ -174,8 +174,8 @@
   12.13  val [hmono,imono,subhi] = goal Fixedpt.thy
   12.14      "[| bnd_mono(D,h);  bnd_mono(E,i); 		\
   12.15  \       !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(E,i)";
   12.16 -br (bnd_monoD1 RS lfp_greatest) 1;
   12.17 -br imono 1;
   12.18 +by (rtac (bnd_monoD1 RS lfp_greatest) 1);
   12.19 +by (rtac imono 1);
   12.20  by (rtac (hmono RSN (2, lfp_Int_lowerbound)) 1);
   12.21  by (rtac (Int_lower1 RS subhi RS subset_trans) 1);
   12.22  by (rtac (imono RS bnd_monoD2 RS subset_trans) 1);
   12.23 @@ -186,10 +186,10 @@
   12.24    but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)
   12.25  val [isubD,subhi] = goal Fixedpt.thy
   12.26      "[| i(D) <= D;  !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(D,i)";
   12.27 -br lfp_greatest 1;
   12.28 -br isubD 1;
   12.29 +by (rtac lfp_greatest 1);
   12.30 +by (rtac isubD 1);
   12.31  by (rtac lfp_lowerbound 1);
   12.32 -be (subhi RS subset_trans) 1;
   12.33 +by (etac (subhi RS subset_trans) 1);
   12.34  by (REPEAT (assume_tac 1));
   12.35  val lfp_mono2 = result();
   12.36  
    13.1 --- a/src/ZF/func.ML	Fri Sep 24 11:27:15 1993 +0200
    13.2 +++ b/src/ZF/func.ML	Thu Sep 30 10:10:21 1993 +0100
    13.3 @@ -293,12 +293,14 @@
    13.4  \    (f Un g) : (A Un C) -> (B Un D)";
    13.5       (*Contradiction if A Int C = 0, a:A, a:B*)
    13.6  val [disjoint] = prems RL ([IntI] RLN (2, [equals0D]));
    13.7 +val Pair_UnE = read_instantiate [("c","<?a,?b>")] UnE;  (* ignores x: A Un C *)
    13.8  by (cut_facts_tac prems 1);
    13.9  by (rtac PiI 1);
   13.10 -(*solve subgoal 2 first!!*)
   13.11 -by (DEPTH_SOLVE_1 (eresolve_tac [UnE, Pair_mem_PiE, sym, disjoint] 2
   13.12 -       INTLEAVE ares_tac [ex1I, apply_Pair RS UnI1, apply_Pair RS UnI2] 2));
   13.13 -by (REPEAT (eresolve_tac [asm_rl,UnE,rel_Un,PiE] 1));
   13.14 +by (REPEAT (ares_tac [rel_Un, fun_is_rel] 1));
   13.15 +by (rtac ex_ex1I 1);
   13.16 +by (fast_tac (ZF_cs addDs [apply_Pair]) 1);
   13.17 +by (REPEAT_FIRST (eresolve_tac [asm_rl, Pair_UnE, sym RS trans]
   13.18 +	     ORELSE' eresolve_tac [Pair_mem_PiE,disjoint] THEN' atac));
   13.19  val fun_disjoint_Un = result();
   13.20  
   13.21  goal ZF.thy
    14.1 --- a/src/ZF/ind-syntax.ML	Fri Sep 24 11:27:15 1993 +0200
    14.2 +++ b/src/ZF/ind-syntax.ML	Thu Sep 30 10:10:21 1993 +0100
    14.3 @@ -127,10 +127,11 @@
    14.4  val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
    14.5  		   ex_mono, Collect_mono, Part_mono, in_mono];
    14.6  
    14.7 +(*Return the conclusion of a rule, of the form t:X*)
    14.8  fun rule_concl rl = 
    14.9 -  let val Const("op :",_) $ t $ X = dest_tprop (Logic.strip_imp_concl rl)
   14.10 -  in (t,X) end
   14.11 -  handle _ => error "Conclusion of rule should be a set membership";
   14.12 +    case dest_tprop (Logic.strip_imp_concl rl) of
   14.13 +        Const("op :",_) $ t $ X => (t,X) 
   14.14 +      | _ => error "Conclusion of rule should be a set membership";
   14.15  
   14.16  (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   14.17    read_instantiate replaces a propositional variable by a formula variable*)
    15.1 --- a/src/ZF/ind_syntax.ML	Fri Sep 24 11:27:15 1993 +0200
    15.2 +++ b/src/ZF/ind_syntax.ML	Thu Sep 30 10:10:21 1993 +0100
    15.3 @@ -127,10 +127,11 @@
    15.4  val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
    15.5  		   ex_mono, Collect_mono, Part_mono, in_mono];
    15.6  
    15.7 +(*Return the conclusion of a rule, of the form t:X*)
    15.8  fun rule_concl rl = 
    15.9 -  let val Const("op :",_) $ t $ X = dest_tprop (Logic.strip_imp_concl rl)
   15.10 -  in (t,X) end
   15.11 -  handle _ => error "Conclusion of rule should be a set membership";
   15.12 +    case dest_tprop (Logic.strip_imp_concl rl) of
   15.13 +        Const("op :",_) $ t $ X => (t,X) 
   15.14 +      | _ => error "Conclusion of rule should be a set membership";
   15.15  
   15.16  (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   15.17    read_instantiate replaces a propositional variable by a formula variable*)
    16.1 --- a/src/ZF/intr-elim.ML	Fri Sep 24 11:27:15 1993 +0200
    16.2 +++ b/src/ZF/intr-elim.ML	Thu Sep 30 10:10:21 1993 +0100
    16.3 @@ -117,7 +117,20 @@
    16.4     (fn a => "Name of recursive set not declared as constant: " ^ a);
    16.5  
    16.6  val intr_tms = map (Sign.term_of o rd propT) sintrs;
    16.7 -val (Const(_,recT),rec_params) = strip_comb (#2 (rule_concl(hd intr_tms)))
    16.8 +
    16.9 +local (*Checking the introduction rules*)
   16.10 +  val intr_sets = map (#2 o rule_concl) intr_tms;
   16.11 +
   16.12 +  fun intr_ok set =
   16.13 +      case head_of set of Const(a,recT) => a mem rec_names | _ => false;
   16.14 +
   16.15 +  val dummy =  assert_all intr_ok intr_sets
   16.16 +     (fn t => "Conclusion of rule does not name a recursive set: " ^ 
   16.17 +	      Sign.string_of_term sign t);
   16.18 +in
   16.19 +val (Const(_,recT),rec_params) = strip_comb (hd intr_sets)
   16.20 +end;
   16.21 +
   16.22  val rec_hds = map (fn a=> Const(a,recT)) rec_names;
   16.23  val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;
   16.24  
   16.25 @@ -262,8 +275,9 @@
   16.26  
   16.27  val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
   16.28  
   16.29 -(*Applies freeness of the given constructors.
   16.30 -  NB for datatypes, defs=con_defs; for inference systems, con_defs=[]! *)
   16.31 +(*Applies freeness of the given constructors, which *must* be unfolded by
   16.32 +  the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   16.33 +  for inference systems. *)
   16.34  fun con_elim_tac defs =
   16.35      rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;
   16.36  
    17.1 --- a/src/ZF/intr_elim.ML	Fri Sep 24 11:27:15 1993 +0200
    17.2 +++ b/src/ZF/intr_elim.ML	Thu Sep 30 10:10:21 1993 +0100
    17.3 @@ -117,7 +117,20 @@
    17.4     (fn a => "Name of recursive set not declared as constant: " ^ a);
    17.5  
    17.6  val intr_tms = map (Sign.term_of o rd propT) sintrs;
    17.7 -val (Const(_,recT),rec_params) = strip_comb (#2 (rule_concl(hd intr_tms)))
    17.8 +
    17.9 +local (*Checking the introduction rules*)
   17.10 +  val intr_sets = map (#2 o rule_concl) intr_tms;
   17.11 +
   17.12 +  fun intr_ok set =
   17.13 +      case head_of set of Const(a,recT) => a mem rec_names | _ => false;
   17.14 +
   17.15 +  val dummy =  assert_all intr_ok intr_sets
   17.16 +     (fn t => "Conclusion of rule does not name a recursive set: " ^ 
   17.17 +	      Sign.string_of_term sign t);
   17.18 +in
   17.19 +val (Const(_,recT),rec_params) = strip_comb (hd intr_sets)
   17.20 +end;
   17.21 +
   17.22  val rec_hds = map (fn a=> Const(a,recT)) rec_names;
   17.23  val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;
   17.24  
   17.25 @@ -262,8 +275,9 @@
   17.26  
   17.27  val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
   17.28  
   17.29 -(*Applies freeness of the given constructors.
   17.30 -  NB for datatypes, defs=con_defs; for inference systems, con_defs=[]! *)
   17.31 +(*Applies freeness of the given constructors, which *must* be unfolded by
   17.32 +  the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   17.33 +  for inference systems. *)
   17.34  fun con_elim_tac defs =
   17.35      rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;
   17.36  
    18.1 --- a/src/ZF/list.ML	Fri Sep 24 11:27:15 1993 +0200
    18.2 +++ b/src/ZF/list.ML	Thu Sep 30 10:10:21 1993 +0100
    18.3 @@ -55,17 +55,14 @@
    18.4  val list_subset_univ = standard
    18.5      (list_mono RS (list_univ RSN (2,subset_trans)));
    18.6  
    18.7 -(*****
    18.8  val major::prems = goal List.thy
    18.9      "[| l: list(A);    \
   18.10 -\       c: C(0);       \
   18.11 -\       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(<x,y>)  \
   18.12 -\    |] ==> list_case(l,c,h) : C(l)";
   18.13 -by (rtac (major RS list_induct) 1);
   18.14 -by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
   18.15 -			    ([list_case_0,list_case_Pair]@prems))));
   18.16 +\       c: C(Nil);       \
   18.17 +\       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))  \
   18.18 +\    |] ==> list_case(c,h,l) : C(l)";
   18.19 +by (rtac (major RS List.induct) 1);
   18.20 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.case_eqns @ prems))));
   18.21  val list_case_type = result();
   18.22 -****)
   18.23  
   18.24  
   18.25  (** For recursion **)
    19.1 --- a/src/ZF/listfn.ML	Fri Sep 24 11:27:15 1993 +0200
    19.2 +++ b/src/ZF/listfn.ML	Thu Sep 30 10:10:21 1993 +0100
    19.3 @@ -8,6 +8,47 @@
    19.4  
    19.5  open ListFn;
    19.6  
    19.7 +(** hd and tl **)
    19.8 +
    19.9 +goalw ListFn.thy [hd_def] "hd(Cons(a,l)) = a";
   19.10 +by (resolve_tac List.case_eqns 1);
   19.11 +val hd_Cons = result();
   19.12 +
   19.13 +goalw ListFn.thy [tl_def] "tl(Nil) = Nil";
   19.14 +by (resolve_tac List.case_eqns 1);
   19.15 +val tl_Nil = result();
   19.16 +
   19.17 +goalw ListFn.thy [tl_def] "tl(Cons(a,l)) = l";
   19.18 +by (resolve_tac List.case_eqns 1);
   19.19 +val tl_Cons = result();
   19.20 +
   19.21 +goal ListFn.thy "!!l. l: list(A) ==> tl(l) : list(A)";
   19.22 +by (etac List.elim 1);
   19.23 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.intrs @ [tl_Nil,tl_Cons]))));
   19.24 +val tl_type = result();
   19.25 +
   19.26 +(** drop **)
   19.27 +
   19.28 +goalw ListFn.thy [drop_def] "drop(0, l) = l";
   19.29 +by (rtac rec_0 1);
   19.30 +val drop_0 = result();
   19.31 +
   19.32 +goalw ListFn.thy [drop_def] "!!i. i:nat ==> drop(i, Nil) = Nil";
   19.33 +by (etac nat_induct 1);
   19.34 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Nil])));
   19.35 +val drop_Nil = result();
   19.36 +
   19.37 +goalw ListFn.thy [drop_def]
   19.38 +    "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
   19.39 +by (etac nat_induct 1);
   19.40 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Cons])));
   19.41 +val drop_succ_Cons = result();
   19.42 +
   19.43 +goalw ListFn.thy [drop_def] 
   19.44 +    "!!i l. [| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
   19.45 +by (etac nat_induct 1);
   19.46 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_type])));
   19.47 +val drop_type = result();
   19.48  
   19.49  (** list_rec -- by Vset recursion **)
   19.50  
   19.51 @@ -67,18 +108,18 @@
   19.52  
   19.53  val [length_Nil,length_Cons] = list_recs length_def;
   19.54  
   19.55 -val prems = goalw ListFn.thy [length_def] 
   19.56 -    "l: list(A) ==> length(l) : nat";
   19.57 -by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, nat_succI]) 1));
   19.58 +goalw ListFn.thy [length_def] 
   19.59 +    "!!l. l: list(A) ==> length(l) : nat";
   19.60 +by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
   19.61  val length_type = result();
   19.62  
   19.63  (** app **)
   19.64  
   19.65  val [app_Nil,app_Cons] = list_recs app_def;
   19.66  
   19.67 -val prems = goalw ListFn.thy [app_def] 
   19.68 -    "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
   19.69 -by (REPEAT (ares_tac (prems @ [list_rec_type, ConsI]) 1));
   19.70 +goalw ListFn.thy [app_def] 
   19.71 +    "!!xs ys. [| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
   19.72 +by (REPEAT (ares_tac [list_rec_type, ConsI] 1));
   19.73  val app_type = result();
   19.74  
   19.75  (** rev **)
   19.76 @@ -204,6 +245,38 @@
   19.77  by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
   19.78  val length_flat = result();
   19.79  
   19.80 +(** Length and drop **)
   19.81 +
   19.82 +(*Lemma for the inductive step of drop_length*)
   19.83 +goal ListFn.thy
   19.84 +    "!!xs. xs: list(A) ==> \
   19.85 +\          ALL x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
   19.86 +by (etac List.induct 1);
   19.87 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [drop_0,drop_succ_Cons])));
   19.88 +by (fast_tac ZF_cs 1);
   19.89 +val drop_length_Cons_lemma = result();
   19.90 +val drop_length_Cons = standard (drop_length_Cons_lemma RS spec);
   19.91 +
   19.92 +goal ListFn.thy
   19.93 +    "!!l. l: list(A) ==> ALL i: length(l).  EX z zs. drop(i,l) = Cons(z,zs)";
   19.94 +by (etac List.induct 1);
   19.95 +by (ALLGOALS (asm_simp_tac (list_ss addsimps bquant_simps)));
   19.96 +by (rtac conjI 1);
   19.97 +by (etac drop_length_Cons 1);
   19.98 +by (rtac ballI 1);
   19.99 +by (rtac natE 1);
  19.100 +by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
  19.101 +by (assume_tac 1);
  19.102 +by (asm_simp_tac (list_ss addsimps [drop_0]) 1);
  19.103 +by (fast_tac ZF_cs 1);
  19.104 +by (asm_simp_tac (list_ss addsimps [drop_succ_Cons]) 1);
  19.105 +by (dtac bspec 1);
  19.106 +by (fast_tac ZF_cs 2);
  19.107 +by (fast_tac (ZF_cs addEs [succ_in_naturalD,length_type]) 1);
  19.108 +val drop_length_lemma = result();
  19.109 +val drop_length = standard (drop_length_lemma RS bspec);
  19.110 +
  19.111 +
  19.112  (*** theorems about app ***)
  19.113  
  19.114  val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";
    20.1 --- a/src/ZF/listfn.thy	Fri Sep 24 11:27:15 1993 +0200
    20.2 +++ b/src/ZF/listfn.thy	Thu Sep 30 10:10:21 1993 +0100
    20.3 @@ -18,6 +18,8 @@
    20.4    length,rev :: "i=>i"
    20.5    flat       :: "i=>i"
    20.6    list_add   :: "i=>i"
    20.7 +  hd,tl      :: "i=>i"
    20.8 +  drop	     :: "[i,i]=>i"
    20.9  
   20.10   (* List Enumeration *)
   20.11   "[]"        :: "i" 	                           	("[]")
   20.12 @@ -31,6 +33,11 @@
   20.13  
   20.14  
   20.15  rules
   20.16 +
   20.17 +  hd_def	"hd(l)	     == list_case(0, %x xs.x, l)"
   20.18 +  tl_def	"tl(l)       == list_case(Nil, %x xs.xs, l)"
   20.19 +  drop_def	"drop(i,l)   == rec(i, l, %j r. tl(r))"
   20.20 +
   20.21    list_rec_def
   20.22        "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
   20.23  
   20.24 @@ -40,5 +47,4 @@
   20.25    rev_def       "rev(l)      == list_rec(l,  Nil,  %x xs r. r @ [x])"
   20.26    flat_def      "flat(ls)    == list_rec(ls, Nil,  %l ls r. l @ r)"
   20.27    list_add_def  "list_add(l) == list_rec(l, 0,  %x xs r. x#+r)"
   20.28 -
   20.29  end
    21.1 --- a/src/ZF/nat.ML	Fri Sep 24 11:27:15 1993 +0200
    21.2 +++ b/src/ZF/nat.ML	Thu Sep 30 10:10:21 1993 +0100
    21.3 @@ -31,7 +31,7 @@
    21.4  by (resolve_tac prems 1);
    21.5  val nat_succI = result();
    21.6  
    21.7 -goalw Nat.thy [one_def] "1 : nat";
    21.8 +goal Nat.thy "1 : nat";
    21.9  by (rtac (nat_0I RS nat_succI) 1);
   21.10  val nat_1I = result();
   21.11  
   21.12 @@ -59,7 +59,7 @@
   21.13  
   21.14  val major::prems = goal Nat.thy
   21.15      "[| n: nat;  n=0 ==> P;  !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P";
   21.16 -br (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1;
   21.17 +by (rtac (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1);
   21.18  by (DEPTH_SOLVE (eresolve_tac [singletonE,RepFunE] 1
   21.19            ORELSE ares_tac prems 1));
   21.20  val natE = result();
   21.21 @@ -69,10 +69,13 @@
   21.22  by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));
   21.23  val naturals_are_ordinals = result();
   21.24  
   21.25 +(* i: nat ==> 0: succ(i) *)
   21.26 +val nat_0_in_succ = naturals_are_ordinals RS Ord_0_in_succ;
   21.27 +
   21.28  goal Nat.thy "!!n. n: nat ==> n=0 | 0:n";
   21.29  by (etac nat_induct 1);
   21.30  by (fast_tac ZF_cs 1);
   21.31 -by (fast_tac (ZF_cs addIs [naturals_are_ordinals RS Ord_0_mem_succ]) 1);
   21.32 +by (fast_tac (ZF_cs addIs [nat_0_in_succ]) 1);
   21.33  val natE0 = result();
   21.34  
   21.35  goal Nat.thy "Ord(nat)";
   21.36 @@ -84,6 +87,12 @@
   21.37  by (REPEAT (ares_tac [empty_subsetI,succ_subsetI] 1));
   21.38  val Ord_nat = result();
   21.39  
   21.40 +(* succ(i): nat ==> i: nat *)
   21.41 +val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans;
   21.42 +
   21.43 +(* [| succ(i): k;  k: nat |] ==> i: k *)
   21.44 +val succ_in_naturalD = [succI1, asm_rl, naturals_are_ordinals] MRS Ord_trans;
   21.45 +
   21.46  (** Variations on mathematical induction **)
   21.47  
   21.48  (*complete induction*)
   21.49 @@ -97,7 +106,7 @@
   21.50  by (ALLGOALS
   21.51      (asm_simp_tac
   21.52       (ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff, 
   21.53 -					 Ord_nat RS Ord_in_Ord]))));
   21.54 +					  naturals_are_ordinals]))));
   21.55  val nat_induct_from_lemma = result();
   21.56  
   21.57  (*Induction starting from m rather than 0*)
   21.58 @@ -125,6 +134,28 @@
   21.59  by (REPEAT (ares_tac (prems@[ballI]) 1 ORELSE etac bspec 1));
   21.60  val diff_induct = result();
   21.61  
   21.62 +(** Induction principle analogous to trancl_induct **)
   21.63 +
   21.64 +goal Nat.thy
   21.65 + "!!m. m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \
   21.66 +\               (ALL n:nat. m:n --> P(m,n))";
   21.67 +by (etac nat_induct 1);
   21.68 +by (ALLGOALS
   21.69 +    (EVERY' [rtac (impI RS impI), rtac (nat_induct RS ballI), assume_tac,
   21.70 +	     fast_tac ZF_cs, fast_tac ZF_cs]));
   21.71 +val succ_less_induct_lemma = result();
   21.72 +
   21.73 +val prems = goal Nat.thy
   21.74 +    "[| m: n;  n: nat;  	\
   21.75 +\       P(m,succ(m));  		\
   21.76 +\       !!x. [| x: nat;  P(m,x) |] ==> P(m,succ(x)) \
   21.77 +\    |] ==> P(m,n)";
   21.78 +by (res_inst_tac [("P4","P")] 
   21.79 +     (succ_less_induct_lemma RS mp RS mp RS bspec RS mp) 1);
   21.80 +by (rtac (Ord_nat RSN (3,Ord_trans)) 1);
   21.81 +by (REPEAT (ares_tac (prems @ [ballI,impI]) 1));
   21.82 +val succ_less_induct = result();
   21.83 +
   21.84  (** nat_case **)
   21.85  
   21.86  goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a";
   21.87 @@ -157,18 +188,16 @@
   21.88  
   21.89  val [prem] = goal Nat.thy 
   21.90      "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
   21.91 -val nat_rec_ss = ZF_ss 
   21.92 -      addsimps [prem, nat_case_succ, nat_succI, Memrel_iff, 
   21.93 -		vimage_singleton_iff];
   21.94  by (rtac nat_rec_trans 1);
   21.95 -by (simp_tac nat_rec_ss 1);
   21.96 +by (simp_tac (ZF_ss addsimps [prem, nat_case_succ, nat_succI, Memrel_iff, 
   21.97 +			      vimage_singleton_iff]) 1);
   21.98  val nat_rec_succ = result();
   21.99  
  21.100  (** The union of two natural numbers is a natural number -- their maximum **)
  21.101  
  21.102 -(*  [| ?i : nat; ?j : nat |] ==> ?i Un ?j : nat  *)
  21.103 +(*  [| i : nat; j : nat |] ==> i Un j : nat  *)
  21.104  val Un_nat_type = standard (Ord_nat RSN (3,Ord_member_UnI));
  21.105  
  21.106 -(*  [| ?i : nat; ?j : nat |] ==> ?i Int ?j : nat  *)
  21.107 +(*  [| i : nat; j : nat |] ==> i Int j : nat  *)
  21.108  val Int_nat_type = standard (Ord_nat RSN (3,Ord_member_IntI));
  21.109  
    22.1 --- a/src/ZF/ord.ML	Fri Sep 24 11:27:15 1993 +0200
    22.2 +++ b/src/ZF/ord.ML	Thu Sep 30 10:10:21 1993 +0100
    22.3 @@ -47,14 +47,14 @@
    22.4  
    22.5  val [prem1,prem2] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]
    22.6      "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
    22.7 -br (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1;
    22.8 +by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1);
    22.9  by (REPEAT (etac (prem1 RS Transset_includes_range) 1
   22.10       ORELSE resolve_tac [conjI, singletonI] 1));
   22.11  val Transset_includes_summands = result();
   22.12  
   22.13  val [prem] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]
   22.14      "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
   22.15 -br (Int_Un_distrib RS ssubst) 1;
   22.16 +by (rtac (Int_Un_distrib RS ssubst) 1);
   22.17  by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);
   22.18  val Transset_sum_Int_subset = result();
   22.19  
   22.20 @@ -281,7 +281,7 @@
   22.21  by (fast_tac ZF_cs 1);
   22.22  by (rtac (prem RS Ord_succ) 1);
   22.23  by (rtac Ord_0 1);
   22.24 -val Ord_0_mem_succ = result();
   22.25 +val Ord_0_in_succ = result();
   22.26  
   22.27  goal Ord.thy "!!i j. [| Ord(i);  Ord(j) |] ==> j:i <-> j<=i & ~(i<=j)";
   22.28  by (rtac iffI 1);
   22.29 @@ -293,7 +293,7 @@
   22.30  val Ord_member_iff = result();
   22.31  
   22.32  goal Ord.thy "!!i. Ord(i) ==> 0:i  <-> ~ i=0";
   22.33 -be (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1;
   22.34 +by (etac (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1);
   22.35  by (fast_tac eq_cs 1);
   22.36  val Ord_0_member_iff = result();
   22.37  
   22.38 @@ -307,6 +307,7 @@
   22.39  by (ALLGOALS (fast_tac ZF_cs));
   22.40  val member_succI = result();
   22.41  
   22.42 +(*Recall Ord_succ_subsetI, namely  [| i:j;  Ord(j) |] ==> succ(i) <= j *)
   22.43  goalw Ord.thy [Transset_def,Ord_def]
   22.44      "!!i j. [| i : succ(j);  Ord(j) |] ==> i<=j";
   22.45  by (fast_tac ZF_cs 1);
   22.46 @@ -353,6 +354,8 @@
   22.47  by (REPEAT (ares_tac [Ord_succ] 1));
   22.48  val Ord_succ_mono = result();
   22.49  
   22.50 +(** Union and Intersection **)
   22.51 +
   22.52  goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Un j : k";
   22.53  by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
   22.54  by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
    23.1 --- a/src/ZF/quniv.ML	Fri Sep 24 11:27:15 1993 +0200
    23.2 +++ b/src/ZF/quniv.ML	Thu Sep 30 10:10:21 1993 +0100
    23.3 @@ -12,12 +12,12 @@
    23.4  
    23.5  goalw QUniv.thy [quniv_def]
    23.6      "!!X A. X <= univ(eclose(A)) ==> X : quniv(A)";
    23.7 -be PowI 1;
    23.8 +by (etac PowI 1);
    23.9  val qunivI = result();
   23.10  
   23.11  goalw QUniv.thy [quniv_def]
   23.12      "!!X A. X : quniv(A) ==> X <= univ(eclose(A))";
   23.13 -be PowD 1;
   23.14 +by (etac PowD 1);
   23.15  val qunivD = result();
   23.16  
   23.17  goalw QUniv.thy [quniv_def] "!!A B. A<=B ==> quniv(A) <= quniv(B)";
   23.18 @@ -152,8 +152,8 @@
   23.19  goal Univ.thy
   23.20      "!!X. [| {a,b} : Vfrom(X,succ(i));  Transset(X) |] ==> \
   23.21  \         a: Vfrom(X,i)  &  b: Vfrom(X,i)";
   23.22 -bd (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1;
   23.23 -ba 1;
   23.24 +by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
   23.25 +by (assume_tac 1);
   23.26  by (fast_tac ZF_cs 1);
   23.27  val doubleton_in_Vfrom_D = result();
   23.28  
   23.29 @@ -185,8 +185,8 @@
   23.30  goalw QUniv.thy [QPair_def,sum_def]
   23.31   "!!X. Transset(X) ==> 		\
   23.32  \      <a;b> Int Vfrom(X, succ(i))  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>";
   23.33 -br (Int_Un_distrib RS ssubst) 1;
   23.34 -br Un_mono 1;
   23.35 +by (rtac (Int_Un_distrib RS ssubst) 1);
   23.36 +by (rtac Un_mono 1);
   23.37  by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans,
   23.38  		      [Int_lower1, subset_refl] MRS Sigma_mono] 1));
   23.39  val QPair_Int_Vfrom_succ_subset = result();
   23.40 @@ -194,12 +194,12 @@
   23.41  (** Pairs in quniv -- for handling the base case **)
   23.42  
   23.43  goal QUniv.thy "!!X. <a,b> : quniv(X) ==> <a,b> : univ(eclose(X))";
   23.44 -be ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1;
   23.45 +by (etac ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1);
   23.46  val Pair_in_quniv_D = result();
   23.47  
   23.48  goal QUniv.thy "a*b Int quniv(A) = a*b Int univ(eclose(A))";
   23.49 -br equalityI 1;
   23.50 -br ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2;
   23.51 +by (rtac equalityI 1);
   23.52 +by (rtac ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2);
   23.53  by (fast_tac (ZF_cs addSEs [Pair_in_quniv_D]) 1);
   23.54  val product_Int_quniv_eq = result();
   23.55  
   23.56 @@ -211,33 +211,33 @@
   23.57  (**** "Take-lemma" rules for proving c: quniv(A) ****)
   23.58  
   23.59  goalw QUniv.thy [quniv_def] "Transset(quniv(A))";
   23.60 -br (Transset_eclose RS Transset_univ RS Transset_Pow) 1;
   23.61 +by (rtac (Transset_eclose RS Transset_univ RS Transset_Pow) 1);
   23.62  val Transset_quniv = result();
   23.63  
   23.64  val [aprem, iprem] = goal QUniv.thy
   23.65      "[| a: quniv(quniv(X));  	\
   23.66  \       !!i. i:nat ==> a Int Vfrom(quniv(X),i) : quniv(A) \
   23.67  \    |] ==> a : quniv(A)";
   23.68 -br (univ_Int_Vfrom_subset RS qunivI) 1;
   23.69 -br (aprem RS qunivD) 1;
   23.70 +by (rtac (univ_Int_Vfrom_subset RS qunivI) 1);
   23.71 +by (rtac (aprem RS qunivD) 1);
   23.72  by (rtac (Transset_quniv RS Transset_eclose_eq_arg RS ssubst) 1);
   23.73 -be (iprem RS qunivD) 1;
   23.74 +by (etac (iprem RS qunivD) 1);
   23.75  val quniv_Int_Vfrom = result();
   23.76  
   23.77  (** Rules for level 0 **)
   23.78  
   23.79  goal QUniv.thy "<a;b> Int quniv(A) : quniv(A)";
   23.80 -br (QPair_Int_quniv_eq RS ssubst) 1;
   23.81 -br (Int_lower2 RS qunivI) 1;
   23.82 +by (rtac (QPair_Int_quniv_eq RS ssubst) 1);
   23.83 +by (rtac (Int_lower2 RS qunivI) 1);
   23.84  val QPair_Int_quniv_in_quniv = result();
   23.85  
   23.86  (*Unused; kept as an example.  QInr rule is similar*)
   23.87  goalw QUniv.thy [QInl_def] "QInl(a) Int quniv(A) : quniv(A)";
   23.88 -br QPair_Int_quniv_in_quniv 1;
   23.89 +by (rtac QPair_Int_quniv_in_quniv 1);
   23.90  val QInl_Int_quniv_in_quniv = result();
   23.91  
   23.92  goal QUniv.thy "!!a A X. a : quniv(A) ==> a Int X : quniv(A)";
   23.93 -be ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1;
   23.94 +by (etac ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1);
   23.95  val Int_quniv_in_quniv = result();
   23.96  
   23.97  goal QUniv.thy 
   23.98 @@ -252,8 +252,8 @@
   23.99  \         b Int Vfrom(X,i) : quniv(A);	\
  23.100  \         Transset(X) 			\
  23.101  \      |] ==> <a;b> Int Vfrom(X, succ(i)) : quniv(A)";
  23.102 -br (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1;
  23.103 -br (QPair_in_quniv RS qunivD) 2;
  23.104 +by (rtac (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1);
  23.105 +by (rtac (QPair_in_quniv RS qunivD) 2);
  23.106  by (REPEAT (assume_tac 1));
  23.107  val QPair_Int_Vfrom_succ_in_quniv = result();
  23.108  
  23.109 @@ -267,7 +267,7 @@
  23.110  goalw QUniv.thy [QInl_def]
  23.111   "!!X. [| a Int Vfrom(X,i) : quniv(A);	Transset(X) 		\
  23.112  \      |] ==> QInl(a) Int Vfrom(X, succ(i)) : quniv(A)";
  23.113 -br QPair_Int_Vfrom_succ_in_quniv 1;
  23.114 +by (rtac QPair_Int_Vfrom_succ_in_quniv 1);
  23.115  by (REPEAT (ares_tac [zero_Int_in_quniv] 1));
  23.116  val QInl_Int_Vfrom_succ_in_quniv = result();
  23.117  
  23.118 @@ -276,7 +276,7 @@
  23.119  goalw QUniv.thy [QPair_def]
  23.120   "!!X. Transset(X) ==> 		\
  23.121  \      <a;b> Int Vfrom(X,i)  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>";
  23.122 -be (Transset_Vfrom RS Transset_sum_Int_subset) 1;
  23.123 +by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1);
  23.124  val QPair_Int_Vfrom_subset = result();
  23.125  
  23.126  goal QUniv.thy 
  23.127 @@ -284,8 +284,8 @@
  23.128  \         b Int Vfrom(X,i) : quniv(A);	\
  23.129  \         Transset(X) 			\
  23.130  \      |] ==> <a;b> Int Vfrom(X,i) : quniv(A)";
  23.131 -br (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1;
  23.132 -br (QPair_in_quniv RS qunivD) 2;
  23.133 +by (rtac (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1);
  23.134 +by (rtac (QPair_in_quniv RS qunivD) 2);
  23.135  by (REPEAT (assume_tac 1));
  23.136  val QPair_Int_Vfrom_in_quniv = result();
  23.137  
  23.138 @@ -309,15 +309,15 @@
  23.139   "!!i. [| a Int Vset(i) <= c;	\
  23.140  \         b Int Vset(i) <= d	\
  23.141  \      |] ==> <a;b> Int Vset(succ(i))  <=  <c;d>";
  23.142 -br ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono] 
  23.143 -    MRS subset_trans) 1;
  23.144 +by (rtac ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono] 
  23.145 +	  MRS subset_trans) 1);
  23.146  by (REPEAT (assume_tac 1));
  23.147  val QPair_Int_Vset_succ_subset_trans = result();
  23.148  
  23.149  (*Unused; kept as an example.  QInr rule is similar*)
  23.150  goalw QUniv.thy [QInl_def] 
  23.151   "!!i. a Int Vset(i) <= b ==> QInl(a) Int Vset(succ(i)) <= QInl(b)";
  23.152 -be (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1;
  23.153 +by (etac (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1);
  23.154  val QInl_Int_Vset_succ_subset_trans = result();
  23.155  
  23.156  (*Rule for level i -- preserving the level, not decreasing it*)
  23.157 @@ -325,8 +325,8 @@
  23.158   "!!i. [| a Int Vset(i) <= c;	\
  23.159  \         b Int Vset(i) <= d	\
  23.160  \      |] ==> <a;b> Int Vset(i)  <=  <c;d>";
  23.161 -br ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] 
  23.162 -    MRS subset_trans) 1;
  23.163 +by (rtac ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] 
  23.164 +	  MRS subset_trans) 1);
  23.165  by (REPEAT (assume_tac 1));
  23.166  val QPair_Int_Vset_subset_trans = result();
  23.167  
    24.1 --- a/src/ZF/simpdata.ML	Fri Sep 24 11:27:15 1993 +0200
    24.2 +++ b/src/ZF/simpdata.ML	Thu Sep 30 10:10:21 1993 +0100
    24.3 @@ -10,15 +10,21 @@
    24.4      (writeln s;  prove_goal ZF.thy s
    24.5         (fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));
    24.6  
    24.7 +(*INCLUDED IN ZF_ss*)
    24.8  val mem_simps = map prove_fun
    24.9 - [ "a:0 <-> False",
   24.10 -   "a : A Un B <-> a:A | a:B",
   24.11 -   "a : A Int B <-> a:A & a:B",
   24.12 -   "a : A-B <-> a:A & ~a:B",
   24.13 -   "a : cons(b,B) <-> a=b | a:B",
   24.14 -   "i : succ(j) <-> i=j | i:j",
   24.15 + [ "a : 0             <-> False",
   24.16 +   "a : A Un B        <-> a:A | a:B",
   24.17 +   "a : A Int B       <-> a:A & a:B",
   24.18 +   "a : A-B           <-> a:A & ~a:B",
   24.19     "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
   24.20 -   "a : Collect(A,P) <-> a:A & P(a)" ];
   24.21 +   "a : Collect(A,P)  <-> a:A & P(a)" ];
   24.22 +
   24.23 +(*INCLUDED: should be??*)
   24.24 +val bquant_simps = map prove_fun
   24.25 + [ "(ALL x:0.P(x)) <-> True",
   24.26 +   "(EX  x:0.P(x)) <-> False",
   24.27 +   "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
   24.28 +   "(EX  x:succ(i).P(x)) <-> P(i) | (EX  x:i.P(x))" ];
   24.29  
   24.30  (** Tactics for type checking -- from CTT **)
   24.31  
   24.32 @@ -83,7 +89,7 @@
   24.33  fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
   24.34  
   24.35  
   24.36 -val ZF_simps = [empty_subsetI, ball_simp, if_true, if_false, 
   24.37 +val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
   24.38  		beta, eta, restrict, fst_conv, snd_conv, split];
   24.39  
   24.40  (*Sigma_cong, Pi_cong NOT included by default since they cause
   24.41 @@ -94,5 +100,5 @@
   24.42  
   24.43  val ZF_ss = FOL_ss 
   24.44        setmksimps ZF_mk_rew_rules
   24.45 -      addsimps (ZF_simps@mem_simps)
   24.46 +      addsimps (ZF_simps @ mem_simps @ bquant_simps)
   24.47        addcongs ZF_congs;
    25.1 --- a/src/ZF/univ.ML	Fri Sep 24 11:27:15 1993 +0200
    25.2 +++ b/src/ZF/univ.ML	Thu Sep 30 10:10:21 1993 +0100
    25.3 @@ -47,11 +47,11 @@
    25.4  by (eps_ind_tac "x" 1);
    25.5  by (rtac (Vfrom RS ssubst) 1);
    25.6  by (rtac (Vfrom RS ssubst) 1);
    25.7 -br (subset_refl RS Un_mono) 1;
    25.8 -br UN_least 1;
    25.9 +by (rtac (subset_refl RS Un_mono) 1);
   25.10 +by (rtac UN_least 1);
   25.11  by (etac (rank_implies_mem RS bexE) 1);
   25.12 -br subset_trans 1;
   25.13 -be UN_upper 2;
   25.14 +by (rtac subset_trans 1);
   25.15 +by (etac UN_upper 2);
   25.16  by (etac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1);
   25.17  by (etac bspec 1);
   25.18  by (assume_tac 1);
   25.19 @@ -144,16 +144,16 @@
   25.20  by (rtac equalityI 1);
   25.21  (*first inclusion*)
   25.22  by (rtac Un_least 1);
   25.23 -br (A_subset_Vfrom RS subset_trans) 1;
   25.24 -br (prem RS UN_upper) 1;
   25.25 -br UN_least 1;
   25.26 -be UnionE 1;
   25.27 -br subset_trans 1;
   25.28 -be UN_upper 2;
   25.29 +by (rtac (A_subset_Vfrom RS subset_trans) 1);
   25.30 +by (rtac (prem RS UN_upper) 1);
   25.31 +by (rtac UN_least 1);
   25.32 +by (etac UnionE 1);
   25.33 +by (rtac subset_trans 1);
   25.34 +by (etac UN_upper 2);
   25.35  by (rtac (Vfrom RS ssubst) 1);
   25.36 -be ([UN_upper, Un_upper2] MRS subset_trans) 1;
   25.37 +by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
   25.38  (*opposite inclusion*)
   25.39 -br UN_least 1;
   25.40 +by (rtac UN_least 1);
   25.41  by (rtac (Vfrom RS ssubst) 1);
   25.42  by (fast_tac ZF_cs 1);
   25.43  val Vfrom_Union = result();
   25.44 @@ -183,9 +183,9 @@
   25.45  goalw Univ.thy [Limit_def]
   25.46      "!!i. [| Ord(i);  0:i;  ALL y. ~ succ(y)=i |] ==> Limit(i)";
   25.47  by (safe_tac subset_cs);
   25.48 -br Ord_member 1;
   25.49 +by (rtac Ord_member 1);
   25.50  by (REPEAT_FIRST (eresolve_tac [asm_rl, Ord_in_Ord RS Ord_succ]
   25.51 -          ORELSE' dresolve_tac [Ord_succ_subsetI]));
   25.52 +          ORELSE' dtac Ord_succ_subsetI ));
   25.53  by (fast_tac (subset_cs addSIs [equalityI]) 1);
   25.54  val non_succ_LimitI = result();
   25.55  
   25.56 @@ -271,10 +271,10 @@
   25.57  
   25.58  goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
   25.59  by (rtac (Vfrom_succ RS trans) 1);
   25.60 -br (Un_upper2 RSN (2,equalityI)) 1;;
   25.61 -br (subset_refl RSN (2,Un_least)) 1;;
   25.62 -br (A_subset_Vfrom RS subset_trans) 1;
   25.63 -be (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1;
   25.64 +by (rtac (Un_upper2 RSN (2,equalityI)) 1);
   25.65 +by (rtac (subset_refl RSN (2,Un_least)) 1);
   25.66 +by (rtac (A_subset_Vfrom RS subset_trans) 1);
   25.67 +by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
   25.68  val Transset_Vfrom_succ = result();
   25.69  
   25.70  goalw Ord.thy [Pair_def,Transset_def]
   25.71 @@ -285,8 +285,8 @@
   25.72  goal Univ.thy
   25.73      "!!a b.[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |] ==> \
   25.74  \          <a,b> : Vfrom(A,i)";
   25.75 -be (Transset_Pair_subset RS conjE) 1;
   25.76 -be Transset_Vfrom 1;
   25.77 +by (etac (Transset_Pair_subset RS conjE) 1);
   25.78 +by (etac Transset_Vfrom 1);
   25.79  by (REPEAT (ares_tac [Pair_in_Vfrom_limit] 1));
   25.80  val Transset_Pair_subset_Vfrom_limit = result();
   25.81  
   25.82 @@ -346,7 +346,7 @@
   25.83  by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
   25.84  by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   25.85  by (rtac UN_I 1);
   25.86 -by (rtac (rewrite_rule [one_def] sum_in_Vfrom) 2);
   25.87 +by (rtac sum_in_Vfrom 2);
   25.88  by (rtac (succI1 RS UnI1) 5);
   25.89  (*Infer that succ(succ(succ(x Un xa))) < i *)
   25.90  by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
   25.91 @@ -456,14 +456,14 @@
   25.92  val Vset_rankI = Ord_rank RS VsetI;
   25.93  
   25.94  goal Univ.thy "a <= Vset(rank(a))";
   25.95 -br subsetI 1;
   25.96 -be (rank_lt RS Vset_rankI) 1;
   25.97 +by (rtac subsetI 1);
   25.98 +by (etac (rank_lt RS Vset_rankI) 1);
   25.99  val arg_subset_Vset_rank = result();
  25.100  
  25.101  val [iprem] = goal Univ.thy
  25.102      "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
  25.103 -br ([subset_refl, arg_subset_Vset_rank] MRS Int_greatest RS subset_trans) 1;
  25.104 -br (Ord_rank RS iprem) 1;
  25.105 +by (rtac ([subset_refl, arg_subset_Vset_rank] MRS Int_greatest RS subset_trans) 1);
  25.106 +by (rtac (Ord_rank RS iprem) 1);
  25.107  val Int_Vset_subset = result();
  25.108  
  25.109  (** Set up an environment for simplification **)
  25.110 @@ -507,28 +507,28 @@
  25.111  (** univ(A) as a limit **)
  25.112  
  25.113  goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
  25.114 -br (Limit_nat RS Limit_Vfrom_eq) 1;
  25.115 +by (rtac (Limit_nat RS Limit_Vfrom_eq) 1);
  25.116  val univ_eq_UN = result();
  25.117  
  25.118  goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
  25.119 -br (subset_UN_iff_eq RS iffD1) 1;
  25.120 -be (univ_eq_UN RS subst) 1;
  25.121 +by (rtac (subset_UN_iff_eq RS iffD1) 1);
  25.122 +by (etac (univ_eq_UN RS subst) 1);
  25.123  val subset_univ_eq_Int = result();
  25.124  
  25.125  val [aprem, iprem] = goal Univ.thy
  25.126      "[| a <= univ(X);			 	\
  25.127  \       !!i. i:nat ==> a Int Vfrom(X,i) <= b 	\
  25.128  \    |] ==> a <= b";
  25.129 -br (aprem RS subset_univ_eq_Int RS ssubst) 1;
  25.130 -br UN_least 1;
  25.131 -be iprem 1;
  25.132 +by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1);
  25.133 +by (rtac UN_least 1);
  25.134 +by (etac iprem 1);
  25.135  val univ_Int_Vfrom_subset = result();
  25.136  
  25.137  val prems = goal Univ.thy
  25.138      "[| a <= univ(X);   b <= univ(X);   \
  25.139  \       !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
  25.140  \    |] ==> a = b";
  25.141 -br equalityI 1;
  25.142 +by (rtac equalityI 1);
  25.143  by (ALLGOALS
  25.144      (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN'
  25.145       eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN'
  25.146 @@ -576,7 +576,7 @@
  25.147  
  25.148  goalw Univ.thy [univ_def]
  25.149      "!!a b.[| <a,b> <= univ(A);  Transset(A) |] ==> <a,b> : univ(A)";
  25.150 -be Transset_Pair_subset_Vfrom_limit 1;
  25.151 +by (etac Transset_Pair_subset_Vfrom_limit 1);
  25.152  by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
  25.153  val Transset_Pair_subset_univ = result();
  25.154  
  25.155 @@ -592,7 +592,7 @@
  25.156  
  25.157  (** instances for 1 and 2 **)
  25.158  
  25.159 -goalw Univ.thy [one_def] "1 : univ(A)";
  25.160 +goal Univ.thy "1 : univ(A)";
  25.161  by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
  25.162  val one_in_univ = result();
  25.163  
    26.1 --- a/src/ZF/upair.ML	Fri Sep 24 11:27:15 1993 +0200
    26.2 +++ b/src/ZF/upair.ML	Thu Sep 30 10:10:21 1993 +0100
    26.3 @@ -235,17 +235,21 @@
    26.4      "i : j ==> i : succ(j)"
    26.5   (fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
    26.6  
    26.7 -(*Classical introduction rule*)
    26.8 -val succCI = prove_goalw ZF.thy [succ_def]
    26.9 -   "(~ i:j ==> i=j) ==> i: succ(j)"
   26.10 - (fn prems=> [ (rtac consCI 1), (eresolve_tac prems 1) ]);
   26.11 -
   26.12  val succE = prove_goalw ZF.thy [succ_def]
   26.13      "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"
   26.14   (fn major::prems=>
   26.15    [ (rtac (major RS consE) 1),
   26.16      (REPEAT (eresolve_tac prems 1)) ]);
   26.17  
   26.18 +val succ_iff = prove_goal ZF.thy "i : succ(j) <-> i=j | i:j"
   26.19 + (fn _ => [ (fast_tac (lemmas_cs addIs [succI1,succI2] addSEs [succE]) 1) ]);
   26.20 +
   26.21 +(*Classical introduction rule*)
   26.22 +val succCI = prove_goal ZF.thy "(~ i:j ==> i=j) ==> i: succ(j)"
   26.23 + (fn [prem]=>
   26.24 +  [ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
   26.25 +    (etac prem 1) ]);
   26.26 +
   26.27  val succ_neq_0 = prove_goal ZF.thy "succ(n)=0 ==> P"
   26.28   (fn [major]=>
   26.29    [ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),