ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
authorlcp
Tue Oct 05 15:21:29 1993 +0100 (1993-10-05)
changeset 253ac1c0c0016e
parent 24 f3d4ff75d9f2
child 26 5aa9c39b480d
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
changes

epsilon,arith: many changes

ordinal/succ_mem_succI/E: deleted; use succ_leI/E
nat/nat_0_in_succ: deleted; use nat_0_le
univ/Vset_rankI: deleted; use VsetI
src/ZF/Arith.ML
src/ZF/Arith.thy
src/ZF/Epsilon.ML
src/ZF/arith.ML
src/ZF/arith.thy
src/ZF/epsilon.ML
src/ZF/intr-elim.ML
src/ZF/intr_elim.ML
src/ZF/listfn.ML
     1.1 --- a/src/ZF/Arith.ML	Tue Oct 05 13:15:01 1993 +0100
     1.2 +++ b/src/ZF/Arith.ML	Tue Oct 05 15:21:29 1993 +0100
     1.3 @@ -42,9 +42,14 @@
     1.4      (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
     1.5  val rec_type = result();
     1.6  
     1.7 -val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
     1.8 +val nat_le_refl = naturals_are_ordinals RS le_refl;
     1.9 +
    1.10 +val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
    1.11  
    1.12 -val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
    1.13 +val nat_simps = [rec_0, rec_succ, not_lt0, nat_0_le, le0_iff, succ_le_iff,
    1.14 +		 nat_le_refl];
    1.15 +
    1.16 +val nat_ss = ZF_ss addsimps (nat_simps @ nat_typechecks);
    1.17  
    1.18  
    1.19  (** Addition **)
    1.20 @@ -101,27 +106,24 @@
    1.21      (nat_ind_tac "n" prems 1),
    1.22      (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
    1.23  
    1.24 -(*The conclusion is equivalent to m#-n <= m *)
    1.25  val prems = goal Arith.thy 
    1.26 -    "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
    1.27 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.28 -by (resolve_tac prems 1);
    1.29 -by (resolve_tac prems 1);
    1.30 -by (etac succE 3);
    1.31 +    "[| m:nat;  n:nat |] ==> m #- n le m";
    1.32 +by (rtac (prems MRS diff_induct) 1);
    1.33 +by (etac leE 3);
    1.34  by (ALLGOALS
    1.35      (asm_simp_tac
    1.36 -     (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0, 
    1.37 -				diff_succ_succ]))));
    1.38 -val diff_less_succ = result();
    1.39 +     (nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0, 
    1.40 +				diff_succ_succ, naturals_are_ordinals]))));
    1.41 +val diff_le_self = result();
    1.42  
    1.43  (*** Simplification over add, mult, diff ***)
    1.44  
    1.45  val arith_typechecks = [add_type, mult_type, diff_type];
    1.46 -val arith_rews = [add_0, add_succ,
    1.47 -		  mult_0, mult_succ,
    1.48 -		  diff_0, diff_0_eq_0, diff_succ_succ];
    1.49 +val arith_simps = [add_0, add_succ,
    1.50 +		   mult_0, mult_succ,
    1.51 +		   diff_0, diff_0_eq_0, diff_succ_succ];
    1.52  
    1.53 -val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
    1.54 +val arith_ss = nat_ss addsimps (arith_simps@arith_typechecks);
    1.55  
    1.56  (*** Addition ***)
    1.57  
    1.58 @@ -223,19 +225,15 @@
    1.59    [ (nat_ind_tac "m" prems 1),
    1.60      (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
    1.61  
    1.62 -(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
    1.63 -val notless::prems = goal Arith.thy
    1.64 -    "[| ~m:n;  m:nat;  n:nat |] ==> n #+ (m#-n) = m";
    1.65 -by (rtac (notless RS rev_mp) 1);
    1.66 +(*Addition is the inverse of subtraction*)
    1.67 +goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
    1.68 +by (forward_tac [lt_nat_in_nat] 1);
    1.69 +be nat_succI 1;
    1.70 +by (etac rev_mp 1);
    1.71  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.72 -by (resolve_tac prems 1);
    1.73 -by (resolve_tac prems 1);
    1.74 -by (ALLGOALS (asm_simp_tac
    1.75 -	      (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ,
    1.76 -					 naturals_are_ordinals]))));
    1.77 +by (ALLGOALS (asm_simp_tac arith_ss));
    1.78  val add_diff_inverse = result();
    1.79  
    1.80 -
    1.81  (*Subtraction is the inverse of addition. *)
    1.82  val [mnat,nnat] = goal Arith.thy
    1.83      "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
    1.84 @@ -252,148 +250,129 @@
    1.85  
    1.86  (*** Remainder ***)
    1.87  
    1.88 -(*In ordinary notation: if 0<n and n<=m then m-n < m *)
    1.89 -goal Arith.thy "!!m n. [| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
    1.90 +goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m #- n < m";
    1.91 +by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
    1.92  by (etac rev_mp 1);
    1.93  by (etac rev_mp 1);
    1.94  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.95 -by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ])));
    1.96 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_le_self,diff_succ_succ])));
    1.97  val div_termination = result();
    1.98  
    1.99 -val div_rls =
   1.100 -    [Ord_transrec_type, apply_type, div_termination, if_type] @ 
   1.101 -    nat_typechecks;
   1.102 +val div_rls =	(*for mod and div*)
   1.103 +    nat_typechecks @
   1.104 +    [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
   1.105 +     naturals_are_ordinals, not_lt_iff_le RS iffD1];
   1.106 +
   1.107 +val div_ss = ZF_ss addsimps [naturals_are_ordinals, div_termination RS ltD,
   1.108 +			     not_lt_iff_le RS iffD2];
   1.109  
   1.110  (*Type checking depends upon termination!*)
   1.111 -val prems = goalw Arith.thy [mod_def]
   1.112 -    "[| 0:n;  m:nat;  n:nat |] ==> m mod n : nat";
   1.113 -by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
   1.114 +goalw Arith.thy [mod_def] "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
   1.115 +by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
   1.116  val mod_type = result();
   1.117  
   1.118 -val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
   1.119 -
   1.120 -val prems = goal Arith.thy "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m mod n = m";
   1.121 +goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m mod n = m";
   1.122  by (rtac (mod_def RS def_transrec RS trans) 1);
   1.123 -by (simp_tac (div_ss addsimps prems) 1);
   1.124 +by (asm_simp_tac div_ss 1);
   1.125  val mod_less = result();
   1.126  
   1.127 -val prems = goal Arith.thy
   1.128 -    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
   1.129 +goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
   1.130 +by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   1.131  by (rtac (mod_def RS def_transrec RS trans) 1);
   1.132 -by (simp_tac (div_ss addsimps prems) 1);
   1.133 +by (asm_simp_tac div_ss 1);
   1.134  val mod_geq = result();
   1.135  
   1.136  (*** Quotient ***)
   1.137  
   1.138  (*Type checking depends upon termination!*)
   1.139 -val prems = goalw Arith.thy [div_def]
   1.140 -    "[| 0:n;  m:nat;  n:nat |] ==> m div n : nat";
   1.141 -by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
   1.142 +goalw Arith.thy [div_def]
   1.143 +    "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m div n : nat";
   1.144 +by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
   1.145  val div_type = result();
   1.146  
   1.147 -val prems = goal Arith.thy
   1.148 -    "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
   1.149 +goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m div n = 0";
   1.150  by (rtac (div_def RS def_transrec RS trans) 1);
   1.151 -by (simp_tac (div_ss addsimps prems) 1);
   1.152 +by (asm_simp_tac div_ss 1);
   1.153  val div_less = result();
   1.154  
   1.155 -val prems = goal Arith.thy
   1.156 -    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
   1.157 +goal Arith.thy
   1.158 + "!!m n. [| 0<n;  n le m;  m:nat |] ==> m div n = succ((m#-n) div n)";
   1.159 +by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   1.160  by (rtac (div_def RS def_transrec RS trans) 1);
   1.161 -by (simp_tac (div_ss addsimps prems) 1);
   1.162 +by (asm_simp_tac div_ss 1);
   1.163  val div_geq = result();
   1.164  
   1.165  (*Main Result.*)
   1.166 -val prems = goal Arith.thy
   1.167 -    "[| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
   1.168 -by (res_inst_tac [("i","m")] complete_induct 1);
   1.169 -by (resolve_tac prems 1);
   1.170 -by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
   1.171 -by (ALLGOALS 
   1.172 -    (asm_simp_tac
   1.173 -     (arith_ss addsimps ([mod_type,div_type] @ prems @
   1.174 -        [mod_less,mod_geq, div_less, div_geq,
   1.175 -	 add_assoc, add_diff_inverse, div_termination]))));
   1.176 +goal Arith.thy
   1.177 +    "!!m n. [| 0<n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
   1.178 +by (etac complete_induct 1);
   1.179 +by (res_inst_tac [("Q","x<n")] (excluded_middle RS disjE) 1);
   1.180 +(*case x<n*)
   1.181 +by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2);
   1.182 +(*case n le x*)
   1.183 +by (asm_full_simp_tac
   1.184 +     (arith_ss addsimps [not_lt_iff_le, naturals_are_ordinals,
   1.185 +			 mod_geq, div_geq, add_assoc,
   1.186 +			 div_termination RS ltD, add_diff_inverse]) 1);
   1.187  val mod_div_equality = result();
   1.188  
   1.189  
   1.190 -(**** Additional theorems about "less than" ****)
   1.191 -
   1.192 -val [mnat,nnat] = goal Arith.thy
   1.193 -    "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
   1.194 -by (rtac (mnat RS nat_induct) 1);
   1.195 -by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
   1.196 -by (rtac notI 1);
   1.197 -by (etac notE 1);
   1.198 -by (etac (succI1 RS Ord_trans) 1);
   1.199 -by (rtac (nnat RS naturals_are_ordinals) 1);
   1.200 -val add_not_less_self = result();
   1.201 +(**** Additional theorems about "le" ****)
   1.202  
   1.203 -val [mnat,nnat] = goal Arith.thy
   1.204 -    "[| m:nat;  n:nat |] ==> m : succ(m #+ n)";
   1.205 -by (rtac (mnat RS nat_induct) 1);
   1.206 -(*May not simplify even with ZF_ss because it would expand m:succ(...) *)
   1.207 -by (rtac (add_0 RS ssubst) 1);
   1.208 -by (rtac (add_succ RS ssubst) 2);
   1.209 -by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI, 
   1.210 -		      naturals_are_ordinals, nat_succI, add_type] 1));
   1.211 -val add_less_succ_self = result();
   1.212 +goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le m #+ n";
   1.213 +by (etac nat_induct 1);
   1.214 +by (ALLGOALS (asm_simp_tac arith_ss));
   1.215 +val add_le_self = result();
   1.216  
   1.217 -goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= m #+ n";
   1.218 -by (rtac (add_less_succ_self RS member_succD) 1);
   1.219 -by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1));
   1.220 -val add_leq_self = result();
   1.221 -
   1.222 -goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= n #+ m";
   1.223 +goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le n #+ m";
   1.224  by (rtac (add_commute RS ssubst) 1);
   1.225 -by (REPEAT (ares_tac [add_leq_self] 1));
   1.226 -val add_leq_self2 = result();
   1.227 +by (REPEAT (ares_tac [add_le_self] 1));
   1.228 +val add_le_self2 = result();
   1.229  
   1.230  (** Monotonicity of addition **)
   1.231  
   1.232  (*strict, in 1st argument*)
   1.233 -goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k";
   1.234 -by (etac succ_less_induct 1);
   1.235 -by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff])));
   1.236 -val add_less_mono1 = result();
   1.237 +goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
   1.238 +by (forward_tac [lt_nat_in_nat] 1);
   1.239 +ba 1;
   1.240 +by (etac succ_lt_induct 1);
   1.241 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
   1.242 +val add_lt_mono1 = result();
   1.243  
   1.244  (*strict, in both arguments*)
   1.245 -goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l";
   1.246 -by (rtac (add_less_mono1 RS Ord_trans) 1);
   1.247 -by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals]));
   1.248 +goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
   1.249 +by (rtac (add_lt_mono1 RS lt_trans) 1);
   1.250 +by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
   1.251  by (EVERY [rtac (add_commute RS ssubst) 1,
   1.252  	   rtac (add_commute RS ssubst) 3,
   1.253 -	   rtac add_less_mono1 5]);
   1.254 -by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1));
   1.255 -val add_less_mono = result();
   1.256 +	   rtac add_lt_mono1 5]);
   1.257 +by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
   1.258 +val add_lt_mono = result();
   1.259  
   1.260 -(*A [clumsy] way of lifting < monotonictity to <= monotonicity *)
   1.261 -val less_mono::ford::prems = goal Ord.thy
   1.262 -     "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j);	\
   1.263 -\        !!i. i:k ==> f(i):k;			\
   1.264 -\        i<=j;  i:k;  j:k;  Ord(k)		\
   1.265 -\     |] ==> f(i) <= f(j)";
   1.266 +(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
   1.267 +val lt_mono::ford::prems = goal Ord.thy
   1.268 +     "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j);	\
   1.269 +\        !!i. i:k ==> Ord(f(i));		\
   1.270 +\        i le j;  j:k				\
   1.271 +\     |] ==> f(i) le f(j)";
   1.272  by (cut_facts_tac prems 1);
   1.273 -by (rtac member_succD 1);
   1.274 -by (dtac member_succI 1);
   1.275 -by (fast_tac (ZF_cs addSIs [less_mono]) 3);
   1.276 -by (REPEAT (ares_tac [ford,Ord_in_Ord] 1));
   1.277 -val Ord_less_mono_imp_mono = result();
   1.278 +by (fast_tac (lt_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
   1.279 +val Ord_lt_mono_imp_le_mono = result();
   1.280  
   1.281 -(*<=, in 1st argument*)
   1.282 +(*le monotonicity, 1st argument*)
   1.283  goal Arith.thy
   1.284 -    "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k";
   1.285 -by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1);
   1.286 -by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1));
   1.287 -val add_mono1 = result();
   1.288 +    "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
   1.289 +by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1);
   1.290 +by (REPEAT (ares_tac [add_lt_mono1, add_type RS naturals_are_ordinals] 1));
   1.291 +val add_le_mono1 = result();
   1.292  
   1.293 -(*<=, in both arguments*)
   1.294 +(* le monotonicity, BOTH arguments*)
   1.295  goal Arith.thy
   1.296 -    "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l";
   1.297 -by (rtac (add_mono1 RS subset_trans) 1);
   1.298 -by (REPEAT (assume_tac 1));
   1.299 +    "!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
   1.300 +by (rtac (add_le_mono1 RS le_trans) 1);
   1.301 +by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   1.302  by (EVERY [rtac (add_commute RS ssubst) 1,
   1.303  	   rtac (add_commute RS ssubst) 3,
   1.304 -	   rtac add_mono1 5]);
   1.305 -by (REPEAT (assume_tac 1));
   1.306 -val add_mono = result();
   1.307 +	   rtac add_le_mono1 5]);
   1.308 +by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   1.309 +val add_le_mono = result();
     2.1 --- a/src/ZF/Arith.thy	Tue Oct 05 13:15:01 1993 +0100
     2.2 +++ b/src/ZF/Arith.thy	Tue Oct 05 15:21:29 1993 +0100
     2.3 @@ -21,6 +21,6 @@
     2.4      add_def  "m#+n == rec(m, n, %u v.succ(v))"
     2.5      diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
     2.6      mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
     2.7 -    mod_def  "m mod n == transrec(m, %j f. if(j:n, j, f`(j#-n)))"
     2.8 -    div_def  "m div n == transrec(m, %j f. if(j:n, 0, succ(f`(j#-n))))"
     2.9 +    mod_def  "m mod n == transrec(m, %j f. if(j<n, j, f`(j#-n)))"
    2.10 +    div_def  "m div n == transrec(m, %j f. if(j<n, 0, succ(f`(j#-n))))"
    2.11  end
     3.1 --- a/src/ZF/Epsilon.ML	Tue Oct 05 13:15:01 1993 +0100
     3.2 +++ b/src/ZF/Epsilon.ML	Tue Oct 05 15:21:29 1993 +0100
     3.3 @@ -195,35 +195,35 @@
     3.4  by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
     3.5  val rank_of_Ord = result();
     3.6  
     3.7 -val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
     3.8 +goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)";
     3.9  by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
    3.10 -by (rtac (prem RS UN_I) 1);
    3.11 +be (UN_I RS ltI) 1;
    3.12  by (rtac succI1 1);
    3.13 +by (REPEAT (ares_tac [Ord_UN, Ord_succ, Ord_rank] 1));
    3.14  val rank_lt = result();
    3.15  
    3.16 -val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) : rank(b)";
    3.17 +val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)";
    3.18  by (rtac (major RS eclose_induct_down) 1);
    3.19  by (etac rank_lt 1);
    3.20 -by (etac (rank_lt RS Ord_trans) 1);
    3.21 +by (etac (rank_lt RS lt_trans) 1);
    3.22  by (assume_tac 1);
    3.23 -by (rtac Ord_rank 1);
    3.24  val eclose_rank_lt = result();
    3.25  
    3.26 -goal Epsilon.thy "!!a b. a<=b ==> rank(a) <= rank(b)";
    3.27 +goal Epsilon.thy "!!a b. a<=b ==> rank(a) le rank(b)";
    3.28 +by (rtac subset_imp_le 1);
    3.29  by (rtac (rank RS ssubst) 1);
    3.30  by (rtac (rank RS ssubst) 1);
    3.31  by (etac UN_mono 1);
    3.32 -by (rtac subset_refl 1);
    3.33 +by (REPEAT (resolve_tac [subset_refl, Ord_rank] 1));
    3.34  val rank_mono = result();
    3.35  
    3.36  goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))";
    3.37  by (rtac (rank RS trans) 1);
    3.38 -by (rtac equalityI 1);
    3.39 -by (fast_tac ZF_cs 2);
    3.40 -by (rtac UN_least 1);
    3.41 -by (etac (PowD RS rank_mono RS Ord_succ_mono) 1);
    3.42 -by (rtac Ord_rank 1);
    3.43 -by (rtac Ord_rank 1);
    3.44 +by (rtac le_asym 1);
    3.45 +by (DO_GOAL [rtac (Ord_rank RS Ord_succ RS UN_least_le),
    3.46 +	     etac (PowD RS rank_mono RS succ_leI)] 1);
    3.47 +by (DO_GOAL [rtac ([Pow_top, le_refl] MRS UN_upper_le),
    3.48 +	     REPEAT o rtac (Ord_rank RS Ord_succ)] 1);
    3.49  val rank_Pow = result();
    3.50  
    3.51  goal Epsilon.thy "rank(0) = 0";
    3.52 @@ -236,62 +236,47 @@
    3.53  by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
    3.54  by (etac succE 1);
    3.55  by (fast_tac ZF_cs 1);
    3.56 -by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1));
    3.57 +be (rank_lt RS leI RS succ_leI RS le_imp_subset) 1;
    3.58  val rank_succ = result();
    3.59  
    3.60  goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
    3.61  by (rtac equalityI 1);
    3.62 -by (rtac (rank_mono RS UN_least) 2);
    3.63 +by (rtac (rank_mono RS le_imp_subset RS UN_least) 2);
    3.64  by (etac Union_upper 2);
    3.65  by (rtac (rank RS ssubst) 1);
    3.66  by (rtac UN_least 1);
    3.67  by (etac UnionE 1);
    3.68  by (rtac subset_trans 1);
    3.69  by (etac (RepFunI RS Union_upper) 2);
    3.70 -by (etac (rank_lt RS Ord_succ_subsetI) 1);
    3.71 -by (rtac Ord_rank 1);
    3.72 +by (etac (rank_lt RS succ_leI RS le_imp_subset) 1);
    3.73  val rank_Union = result();
    3.74  
    3.75  goal Epsilon.thy "rank(eclose(a)) = rank(a)";
    3.76 -by (rtac equalityI 1);
    3.77 +by (rtac le_asym 1);
    3.78  by (rtac (arg_subset_eclose RS rank_mono) 2);
    3.79  by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
    3.80 -by (rtac UN_least 1);
    3.81 -by (etac ([eclose_rank_lt, Ord_rank] MRS Ord_succ_subsetI) 1);
    3.82 +by (rtac (Ord_rank RS UN_least_le) 1);
    3.83 +by (etac (eclose_rank_lt RS succ_leI) 1);
    3.84  val rank_eclose = result();
    3.85  
    3.86 -(*  [| i: j; j: rank(a) |] ==> i: rank(a)  *)
    3.87 -val rank_trans = Ord_rank RSN (3, Ord_trans);
    3.88 -
    3.89 -goalw Epsilon.thy [Pair_def] "rank(a) : rank(<a,b>)";
    3.90 -by (rtac (consI1 RS rank_lt RS Ord_trans) 1);
    3.91 +goalw Epsilon.thy [Pair_def] "rank(a) < rank(<a,b>)";
    3.92 +by (rtac (consI1 RS rank_lt RS lt_trans) 1);
    3.93  by (rtac (consI1 RS consI2 RS rank_lt) 1);
    3.94 -by (rtac Ord_rank 1);
    3.95  val rank_pair1 = result();
    3.96  
    3.97 -goalw Epsilon.thy [Pair_def] "rank(b) : rank(<a,b>)";
    3.98 -by (rtac (consI1 RS consI2 RS rank_lt RS Ord_trans) 1);
    3.99 +goalw Epsilon.thy [Pair_def] "rank(b) < rank(<a,b>)";
   3.100 +by (rtac (consI1 RS consI2 RS rank_lt RS lt_trans) 1);
   3.101  by (rtac (consI1 RS consI2 RS rank_lt) 1);
   3.102 -by (rtac Ord_rank 1);
   3.103  val rank_pair2 = result();
   3.104  
   3.105 -goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) : rank(Inl(a))";
   3.106 +goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) < rank(Inl(a))";
   3.107  by (rtac rank_pair2 1);
   3.108  val rank_Inl = result();
   3.109  
   3.110 -goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) : rank(Inr(a))";
   3.111 +goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) < rank(Inr(a))";
   3.112  by (rtac rank_pair2 1);
   3.113  val rank_Inr = result();
   3.114  
   3.115 -val [major] = goal Epsilon.thy "i: rank(a) ==> (EX x:a. i<=rank(x))";
   3.116 -by (resolve_tac ([major] RL [rank RS subst] RL [UN_E]) 1);
   3.117 -by (rtac bexI 1);
   3.118 -by (etac member_succD 1);
   3.119 -by (rtac Ord_rank 1);
   3.120 -by (assume_tac 1);
   3.121 -val rank_implies_mem = result();
   3.122 -
   3.123 -
   3.124  (*** Corollaries of leastness ***)
   3.125  
   3.126  goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)";
     4.1 --- a/src/ZF/arith.ML	Tue Oct 05 13:15:01 1993 +0100
     4.2 +++ b/src/ZF/arith.ML	Tue Oct 05 15:21:29 1993 +0100
     4.3 @@ -42,9 +42,14 @@
     4.4      (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
     4.5  val rec_type = result();
     4.6  
     4.7 -val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
     4.8 +val nat_le_refl = naturals_are_ordinals RS le_refl;
     4.9 +
    4.10 +val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
    4.11  
    4.12 -val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
    4.13 +val nat_simps = [rec_0, rec_succ, not_lt0, nat_0_le, le0_iff, succ_le_iff,
    4.14 +		 nat_le_refl];
    4.15 +
    4.16 +val nat_ss = ZF_ss addsimps (nat_simps @ nat_typechecks);
    4.17  
    4.18  
    4.19  (** Addition **)
    4.20 @@ -101,27 +106,24 @@
    4.21      (nat_ind_tac "n" prems 1),
    4.22      (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
    4.23  
    4.24 -(*The conclusion is equivalent to m#-n <= m *)
    4.25  val prems = goal Arith.thy 
    4.26 -    "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
    4.27 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    4.28 -by (resolve_tac prems 1);
    4.29 -by (resolve_tac prems 1);
    4.30 -by (etac succE 3);
    4.31 +    "[| m:nat;  n:nat |] ==> m #- n le m";
    4.32 +by (rtac (prems MRS diff_induct) 1);
    4.33 +by (etac leE 3);
    4.34  by (ALLGOALS
    4.35      (asm_simp_tac
    4.36 -     (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0, 
    4.37 -				diff_succ_succ]))));
    4.38 -val diff_less_succ = result();
    4.39 +     (nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0, 
    4.40 +				diff_succ_succ, naturals_are_ordinals]))));
    4.41 +val diff_le_self = result();
    4.42  
    4.43  (*** Simplification over add, mult, diff ***)
    4.44  
    4.45  val arith_typechecks = [add_type, mult_type, diff_type];
    4.46 -val arith_rews = [add_0, add_succ,
    4.47 -		  mult_0, mult_succ,
    4.48 -		  diff_0, diff_0_eq_0, diff_succ_succ];
    4.49 +val arith_simps = [add_0, add_succ,
    4.50 +		   mult_0, mult_succ,
    4.51 +		   diff_0, diff_0_eq_0, diff_succ_succ];
    4.52  
    4.53 -val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
    4.54 +val arith_ss = nat_ss addsimps (arith_simps@arith_typechecks);
    4.55  
    4.56  (*** Addition ***)
    4.57  
    4.58 @@ -223,19 +225,15 @@
    4.59    [ (nat_ind_tac "m" prems 1),
    4.60      (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
    4.61  
    4.62 -(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
    4.63 -val notless::prems = goal Arith.thy
    4.64 -    "[| ~m:n;  m:nat;  n:nat |] ==> n #+ (m#-n) = m";
    4.65 -by (rtac (notless RS rev_mp) 1);
    4.66 +(*Addition is the inverse of subtraction*)
    4.67 +goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
    4.68 +by (forward_tac [lt_nat_in_nat] 1);
    4.69 +be nat_succI 1;
    4.70 +by (etac rev_mp 1);
    4.71  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    4.72 -by (resolve_tac prems 1);
    4.73 -by (resolve_tac prems 1);
    4.74 -by (ALLGOALS (asm_simp_tac
    4.75 -	      (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ,
    4.76 -					 naturals_are_ordinals]))));
    4.77 +by (ALLGOALS (asm_simp_tac arith_ss));
    4.78  val add_diff_inverse = result();
    4.79  
    4.80 -
    4.81  (*Subtraction is the inverse of addition. *)
    4.82  val [mnat,nnat] = goal Arith.thy
    4.83      "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
    4.84 @@ -252,148 +250,129 @@
    4.85  
    4.86  (*** Remainder ***)
    4.87  
    4.88 -(*In ordinary notation: if 0<n and n<=m then m-n < m *)
    4.89 -goal Arith.thy "!!m n. [| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
    4.90 +goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m #- n < m";
    4.91 +by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
    4.92  by (etac rev_mp 1);
    4.93  by (etac rev_mp 1);
    4.94  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    4.95 -by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ])));
    4.96 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_le_self,diff_succ_succ])));
    4.97  val div_termination = result();
    4.98  
    4.99 -val div_rls =
   4.100 -    [Ord_transrec_type, apply_type, div_termination, if_type] @ 
   4.101 -    nat_typechecks;
   4.102 +val div_rls =	(*for mod and div*)
   4.103 +    nat_typechecks @
   4.104 +    [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
   4.105 +     naturals_are_ordinals, not_lt_iff_le RS iffD1];
   4.106 +
   4.107 +val div_ss = ZF_ss addsimps [naturals_are_ordinals, div_termination RS ltD,
   4.108 +			     not_lt_iff_le RS iffD2];
   4.109  
   4.110  (*Type checking depends upon termination!*)
   4.111 -val prems = goalw Arith.thy [mod_def]
   4.112 -    "[| 0:n;  m:nat;  n:nat |] ==> m mod n : nat";
   4.113 -by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
   4.114 +goalw Arith.thy [mod_def] "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
   4.115 +by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
   4.116  val mod_type = result();
   4.117  
   4.118 -val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
   4.119 -
   4.120 -val prems = goal Arith.thy "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m mod n = m";
   4.121 +goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m mod n = m";
   4.122  by (rtac (mod_def RS def_transrec RS trans) 1);
   4.123 -by (simp_tac (div_ss addsimps prems) 1);
   4.124 +by (asm_simp_tac div_ss 1);
   4.125  val mod_less = result();
   4.126  
   4.127 -val prems = goal Arith.thy
   4.128 -    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
   4.129 +goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
   4.130 +by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   4.131  by (rtac (mod_def RS def_transrec RS trans) 1);
   4.132 -by (simp_tac (div_ss addsimps prems) 1);
   4.133 +by (asm_simp_tac div_ss 1);
   4.134  val mod_geq = result();
   4.135  
   4.136  (*** Quotient ***)
   4.137  
   4.138  (*Type checking depends upon termination!*)
   4.139 -val prems = goalw Arith.thy [div_def]
   4.140 -    "[| 0:n;  m:nat;  n:nat |] ==> m div n : nat";
   4.141 -by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
   4.142 +goalw Arith.thy [div_def]
   4.143 +    "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m div n : nat";
   4.144 +by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
   4.145  val div_type = result();
   4.146  
   4.147 -val prems = goal Arith.thy
   4.148 -    "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
   4.149 +goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m div n = 0";
   4.150  by (rtac (div_def RS def_transrec RS trans) 1);
   4.151 -by (simp_tac (div_ss addsimps prems) 1);
   4.152 +by (asm_simp_tac div_ss 1);
   4.153  val div_less = result();
   4.154  
   4.155 -val prems = goal Arith.thy
   4.156 -    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
   4.157 +goal Arith.thy
   4.158 + "!!m n. [| 0<n;  n le m;  m:nat |] ==> m div n = succ((m#-n) div n)";
   4.159 +by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   4.160  by (rtac (div_def RS def_transrec RS trans) 1);
   4.161 -by (simp_tac (div_ss addsimps prems) 1);
   4.162 +by (asm_simp_tac div_ss 1);
   4.163  val div_geq = result();
   4.164  
   4.165  (*Main Result.*)
   4.166 -val prems = goal Arith.thy
   4.167 -    "[| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
   4.168 -by (res_inst_tac [("i","m")] complete_induct 1);
   4.169 -by (resolve_tac prems 1);
   4.170 -by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
   4.171 -by (ALLGOALS 
   4.172 -    (asm_simp_tac
   4.173 -     (arith_ss addsimps ([mod_type,div_type] @ prems @
   4.174 -        [mod_less,mod_geq, div_less, div_geq,
   4.175 -	 add_assoc, add_diff_inverse, div_termination]))));
   4.176 +goal Arith.thy
   4.177 +    "!!m n. [| 0<n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
   4.178 +by (etac complete_induct 1);
   4.179 +by (res_inst_tac [("Q","x<n")] (excluded_middle RS disjE) 1);
   4.180 +(*case x<n*)
   4.181 +by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2);
   4.182 +(*case n le x*)
   4.183 +by (asm_full_simp_tac
   4.184 +     (arith_ss addsimps [not_lt_iff_le, naturals_are_ordinals,
   4.185 +			 mod_geq, div_geq, add_assoc,
   4.186 +			 div_termination RS ltD, add_diff_inverse]) 1);
   4.187  val mod_div_equality = result();
   4.188  
   4.189  
   4.190 -(**** Additional theorems about "less than" ****)
   4.191 -
   4.192 -val [mnat,nnat] = goal Arith.thy
   4.193 -    "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
   4.194 -by (rtac (mnat RS nat_induct) 1);
   4.195 -by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
   4.196 -by (rtac notI 1);
   4.197 -by (etac notE 1);
   4.198 -by (etac (succI1 RS Ord_trans) 1);
   4.199 -by (rtac (nnat RS naturals_are_ordinals) 1);
   4.200 -val add_not_less_self = result();
   4.201 +(**** Additional theorems about "le" ****)
   4.202  
   4.203 -val [mnat,nnat] = goal Arith.thy
   4.204 -    "[| m:nat;  n:nat |] ==> m : succ(m #+ n)";
   4.205 -by (rtac (mnat RS nat_induct) 1);
   4.206 -(*May not simplify even with ZF_ss because it would expand m:succ(...) *)
   4.207 -by (rtac (add_0 RS ssubst) 1);
   4.208 -by (rtac (add_succ RS ssubst) 2);
   4.209 -by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI, 
   4.210 -		      naturals_are_ordinals, nat_succI, add_type] 1));
   4.211 -val add_less_succ_self = result();
   4.212 +goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le m #+ n";
   4.213 +by (etac nat_induct 1);
   4.214 +by (ALLGOALS (asm_simp_tac arith_ss));
   4.215 +val add_le_self = result();
   4.216  
   4.217 -goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= m #+ n";
   4.218 -by (rtac (add_less_succ_self RS member_succD) 1);
   4.219 -by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1));
   4.220 -val add_leq_self = result();
   4.221 -
   4.222 -goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= n #+ m";
   4.223 +goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le n #+ m";
   4.224  by (rtac (add_commute RS ssubst) 1);
   4.225 -by (REPEAT (ares_tac [add_leq_self] 1));
   4.226 -val add_leq_self2 = result();
   4.227 +by (REPEAT (ares_tac [add_le_self] 1));
   4.228 +val add_le_self2 = result();
   4.229  
   4.230  (** Monotonicity of addition **)
   4.231  
   4.232  (*strict, in 1st argument*)
   4.233 -goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k";
   4.234 -by (etac succ_less_induct 1);
   4.235 -by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff])));
   4.236 -val add_less_mono1 = result();
   4.237 +goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
   4.238 +by (forward_tac [lt_nat_in_nat] 1);
   4.239 +ba 1;
   4.240 +by (etac succ_lt_induct 1);
   4.241 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
   4.242 +val add_lt_mono1 = result();
   4.243  
   4.244  (*strict, in both arguments*)
   4.245 -goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l";
   4.246 -by (rtac (add_less_mono1 RS Ord_trans) 1);
   4.247 -by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals]));
   4.248 +goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
   4.249 +by (rtac (add_lt_mono1 RS lt_trans) 1);
   4.250 +by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
   4.251  by (EVERY [rtac (add_commute RS ssubst) 1,
   4.252  	   rtac (add_commute RS ssubst) 3,
   4.253 -	   rtac add_less_mono1 5]);
   4.254 -by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1));
   4.255 -val add_less_mono = result();
   4.256 +	   rtac add_lt_mono1 5]);
   4.257 +by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
   4.258 +val add_lt_mono = result();
   4.259  
   4.260 -(*A [clumsy] way of lifting < monotonictity to <= monotonicity *)
   4.261 -val less_mono::ford::prems = goal Ord.thy
   4.262 -     "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j);	\
   4.263 -\        !!i. i:k ==> f(i):k;			\
   4.264 -\        i<=j;  i:k;  j:k;  Ord(k)		\
   4.265 -\     |] ==> f(i) <= f(j)";
   4.266 +(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
   4.267 +val lt_mono::ford::prems = goal Ord.thy
   4.268 +     "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j);	\
   4.269 +\        !!i. i:k ==> Ord(f(i));		\
   4.270 +\        i le j;  j:k				\
   4.271 +\     |] ==> f(i) le f(j)";
   4.272  by (cut_facts_tac prems 1);
   4.273 -by (rtac member_succD 1);
   4.274 -by (dtac member_succI 1);
   4.275 -by (fast_tac (ZF_cs addSIs [less_mono]) 3);
   4.276 -by (REPEAT (ares_tac [ford,Ord_in_Ord] 1));
   4.277 -val Ord_less_mono_imp_mono = result();
   4.278 +by (fast_tac (lt_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
   4.279 +val Ord_lt_mono_imp_le_mono = result();
   4.280  
   4.281 -(*<=, in 1st argument*)
   4.282 +(*le monotonicity, 1st argument*)
   4.283  goal Arith.thy
   4.284 -    "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k";
   4.285 -by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1);
   4.286 -by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1));
   4.287 -val add_mono1 = result();
   4.288 +    "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
   4.289 +by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1);
   4.290 +by (REPEAT (ares_tac [add_lt_mono1, add_type RS naturals_are_ordinals] 1));
   4.291 +val add_le_mono1 = result();
   4.292  
   4.293 -(*<=, in both arguments*)
   4.294 +(* le monotonicity, BOTH arguments*)
   4.295  goal Arith.thy
   4.296 -    "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l";
   4.297 -by (rtac (add_mono1 RS subset_trans) 1);
   4.298 -by (REPEAT (assume_tac 1));
   4.299 +    "!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
   4.300 +by (rtac (add_le_mono1 RS le_trans) 1);
   4.301 +by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   4.302  by (EVERY [rtac (add_commute RS ssubst) 1,
   4.303  	   rtac (add_commute RS ssubst) 3,
   4.304 -	   rtac add_mono1 5]);
   4.305 -by (REPEAT (assume_tac 1));
   4.306 -val add_mono = result();
   4.307 +	   rtac add_le_mono1 5]);
   4.308 +by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   4.309 +val add_le_mono = result();
     5.1 --- a/src/ZF/arith.thy	Tue Oct 05 13:15:01 1993 +0100
     5.2 +++ b/src/ZF/arith.thy	Tue Oct 05 15:21:29 1993 +0100
     5.3 @@ -21,6 +21,6 @@
     5.4      add_def  "m#+n == rec(m, n, %u v.succ(v))"
     5.5      diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
     5.6      mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
     5.7 -    mod_def  "m mod n == transrec(m, %j f. if(j:n, j, f`(j#-n)))"
     5.8 -    div_def  "m div n == transrec(m, %j f. if(j:n, 0, succ(f`(j#-n))))"
     5.9 +    mod_def  "m mod n == transrec(m, %j f. if(j<n, j, f`(j#-n)))"
    5.10 +    div_def  "m div n == transrec(m, %j f. if(j<n, 0, succ(f`(j#-n))))"
    5.11  end
     6.1 --- a/src/ZF/epsilon.ML	Tue Oct 05 13:15:01 1993 +0100
     6.2 +++ b/src/ZF/epsilon.ML	Tue Oct 05 15:21:29 1993 +0100
     6.3 @@ -195,35 +195,35 @@
     6.4  by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
     6.5  val rank_of_Ord = result();
     6.6  
     6.7 -val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
     6.8 +goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)";
     6.9  by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
    6.10 -by (rtac (prem RS UN_I) 1);
    6.11 +be (UN_I RS ltI) 1;
    6.12  by (rtac succI1 1);
    6.13 +by (REPEAT (ares_tac [Ord_UN, Ord_succ, Ord_rank] 1));
    6.14  val rank_lt = result();
    6.15  
    6.16 -val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) : rank(b)";
    6.17 +val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)";
    6.18  by (rtac (major RS eclose_induct_down) 1);
    6.19  by (etac rank_lt 1);
    6.20 -by (etac (rank_lt RS Ord_trans) 1);
    6.21 +by (etac (rank_lt RS lt_trans) 1);
    6.22  by (assume_tac 1);
    6.23 -by (rtac Ord_rank 1);
    6.24  val eclose_rank_lt = result();
    6.25  
    6.26 -goal Epsilon.thy "!!a b. a<=b ==> rank(a) <= rank(b)";
    6.27 +goal Epsilon.thy "!!a b. a<=b ==> rank(a) le rank(b)";
    6.28 +by (rtac subset_imp_le 1);
    6.29  by (rtac (rank RS ssubst) 1);
    6.30  by (rtac (rank RS ssubst) 1);
    6.31  by (etac UN_mono 1);
    6.32 -by (rtac subset_refl 1);
    6.33 +by (REPEAT (resolve_tac [subset_refl, Ord_rank] 1));
    6.34  val rank_mono = result();
    6.35  
    6.36  goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))";
    6.37  by (rtac (rank RS trans) 1);
    6.38 -by (rtac equalityI 1);
    6.39 -by (fast_tac ZF_cs 2);
    6.40 -by (rtac UN_least 1);
    6.41 -by (etac (PowD RS rank_mono RS Ord_succ_mono) 1);
    6.42 -by (rtac Ord_rank 1);
    6.43 -by (rtac Ord_rank 1);
    6.44 +by (rtac le_asym 1);
    6.45 +by (DO_GOAL [rtac (Ord_rank RS Ord_succ RS UN_least_le),
    6.46 +	     etac (PowD RS rank_mono RS succ_leI)] 1);
    6.47 +by (DO_GOAL [rtac ([Pow_top, le_refl] MRS UN_upper_le),
    6.48 +	     REPEAT o rtac (Ord_rank RS Ord_succ)] 1);
    6.49  val rank_Pow = result();
    6.50  
    6.51  goal Epsilon.thy "rank(0) = 0";
    6.52 @@ -236,62 +236,47 @@
    6.53  by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
    6.54  by (etac succE 1);
    6.55  by (fast_tac ZF_cs 1);
    6.56 -by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1));
    6.57 +be (rank_lt RS leI RS succ_leI RS le_imp_subset) 1;
    6.58  val rank_succ = result();
    6.59  
    6.60  goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
    6.61  by (rtac equalityI 1);
    6.62 -by (rtac (rank_mono RS UN_least) 2);
    6.63 +by (rtac (rank_mono RS le_imp_subset RS UN_least) 2);
    6.64  by (etac Union_upper 2);
    6.65  by (rtac (rank RS ssubst) 1);
    6.66  by (rtac UN_least 1);
    6.67  by (etac UnionE 1);
    6.68  by (rtac subset_trans 1);
    6.69  by (etac (RepFunI RS Union_upper) 2);
    6.70 -by (etac (rank_lt RS Ord_succ_subsetI) 1);
    6.71 -by (rtac Ord_rank 1);
    6.72 +by (etac (rank_lt RS succ_leI RS le_imp_subset) 1);
    6.73  val rank_Union = result();
    6.74  
    6.75  goal Epsilon.thy "rank(eclose(a)) = rank(a)";
    6.76 -by (rtac equalityI 1);
    6.77 +by (rtac le_asym 1);
    6.78  by (rtac (arg_subset_eclose RS rank_mono) 2);
    6.79  by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
    6.80 -by (rtac UN_least 1);
    6.81 -by (etac ([eclose_rank_lt, Ord_rank] MRS Ord_succ_subsetI) 1);
    6.82 +by (rtac (Ord_rank RS UN_least_le) 1);
    6.83 +by (etac (eclose_rank_lt RS succ_leI) 1);
    6.84  val rank_eclose = result();
    6.85  
    6.86 -(*  [| i: j; j: rank(a) |] ==> i: rank(a)  *)
    6.87 -val rank_trans = Ord_rank RSN (3, Ord_trans);
    6.88 -
    6.89 -goalw Epsilon.thy [Pair_def] "rank(a) : rank(<a,b>)";
    6.90 -by (rtac (consI1 RS rank_lt RS Ord_trans) 1);
    6.91 +goalw Epsilon.thy [Pair_def] "rank(a) < rank(<a,b>)";
    6.92 +by (rtac (consI1 RS rank_lt RS lt_trans) 1);
    6.93  by (rtac (consI1 RS consI2 RS rank_lt) 1);
    6.94 -by (rtac Ord_rank 1);
    6.95  val rank_pair1 = result();
    6.96  
    6.97 -goalw Epsilon.thy [Pair_def] "rank(b) : rank(<a,b>)";
    6.98 -by (rtac (consI1 RS consI2 RS rank_lt RS Ord_trans) 1);
    6.99 +goalw Epsilon.thy [Pair_def] "rank(b) < rank(<a,b>)";
   6.100 +by (rtac (consI1 RS consI2 RS rank_lt RS lt_trans) 1);
   6.101  by (rtac (consI1 RS consI2 RS rank_lt) 1);
   6.102 -by (rtac Ord_rank 1);
   6.103  val rank_pair2 = result();
   6.104  
   6.105 -goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) : rank(Inl(a))";
   6.106 +goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) < rank(Inl(a))";
   6.107  by (rtac rank_pair2 1);
   6.108  val rank_Inl = result();
   6.109  
   6.110 -goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) : rank(Inr(a))";
   6.111 +goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) < rank(Inr(a))";
   6.112  by (rtac rank_pair2 1);
   6.113  val rank_Inr = result();
   6.114  
   6.115 -val [major] = goal Epsilon.thy "i: rank(a) ==> (EX x:a. i<=rank(x))";
   6.116 -by (resolve_tac ([major] RL [rank RS subst] RL [UN_E]) 1);
   6.117 -by (rtac bexI 1);
   6.118 -by (etac member_succD 1);
   6.119 -by (rtac Ord_rank 1);
   6.120 -by (assume_tac 1);
   6.121 -val rank_implies_mem = result();
   6.122 -
   6.123 -
   6.124  (*** Corollaries of leastness ***)
   6.125  
   6.126  goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)";
     7.1 --- a/src/ZF/intr-elim.ML	Tue Oct 05 13:15:01 1993 +0100
     7.2 +++ b/src/ZF/intr-elim.ML	Tue Oct 05 15:21:29 1993 +0100
     7.3 @@ -19,7 +19,7 @@
     7.4    where M is some monotone operator (usually the identity)
     7.5    P(x) is any (non-conjunctive) side condition on the free variables
     7.6    ti, t are any terms
     7.7 -  Sj, Sk are two of the sets being defiend in mutual recursion
     7.8 +  Sj, Sk are two of the sets being defined in mutual recursion
     7.9  
    7.10  Sums are used only for mutual recursion;
    7.11  Products are used only to derive "streamlined" induction rules for relations
     8.1 --- a/src/ZF/intr_elim.ML	Tue Oct 05 13:15:01 1993 +0100
     8.2 +++ b/src/ZF/intr_elim.ML	Tue Oct 05 15:21:29 1993 +0100
     8.3 @@ -19,7 +19,7 @@
     8.4    where M is some monotone operator (usually the identity)
     8.5    P(x) is any (non-conjunctive) side condition on the free variables
     8.6    ti, t are any terms
     8.7 -  Sj, Sk are two of the sets being defiend in mutual recursion
     8.8 +  Sj, Sk are two of the sets being defined in mutual recursion
     8.9  
    8.10  Sums are used only for mutual recursion;
    8.11  Products are used only to derive "streamlined" induction rules for relations
     9.1 --- a/src/ZF/listfn.ML	Tue Oct 05 13:15:01 1993 +0100
     9.2 +++ b/src/ZF/listfn.ML	Tue Oct 05 15:21:29 1993 +0100
     9.3 @@ -59,7 +59,7 @@
     9.4  
     9.5  goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
     9.6  by (rtac (list_rec_def RS def_Vrec RS trans) 1);
     9.7 -by (simp_tac (ZF_ss addsimps (List.case_eqns @ [Vset_rankI, rank_Cons2])) 1);
     9.8 +by (simp_tac (rank_ss addsimps (rank_Cons2::List.case_eqns)) 1);
     9.9  val list_rec_Cons = result();
    9.10  
    9.11  (*Type checking -- proved by induction, as usual*)