natify, a coercion to reduce the number of type constraints in arithmetic
authorpaulson
Tue Aug 01 15:28:21 2000 +0200 (2000-08-01)
changeset 94911a36151ee2fc
parent 9490 c2606af9922c
child 9492 72e429c66608
natify, a coercion to reduce the number of type constraints in arithmetic
src/ZF/AC/AC16_WO4.ML
src/ZF/AC/WO2_AC16.ML
src/ZF/Arith.ML
src/ZF/Arith.thy
src/ZF/CardinalArith.ML
src/ZF/Finite.thy
src/ZF/Inductive.thy
src/ZF/Integ/Int.ML
src/ZF/List.ML
src/ZF/List.thy
src/ZF/ex/Acc.ML
src/ZF/ex/Limit.ML
src/ZF/ex/ListN.ML
src/ZF/ex/Primes.ML
src/ZF/ex/Primrec.ML
     1.1 --- a/src/ZF/AC/AC16_WO4.ML	Tue Aug 01 13:43:22 2000 +0200
     1.2 +++ b/src/ZF/AC/AC16_WO4.ML	Tue Aug 01 15:28:21 2000 +0200
     1.3 @@ -146,7 +146,7 @@
     1.4  Goal "[| k:nat; m:nat |] ==>  \
     1.5  \       ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m";
     1.6  by (induct_tac "k" 1);
     1.7 -by (simp_tac (simpset() addsimps [add_0]) 1);
     1.8 +by (asm_simp_tac (simpset() addsimps [add_0]) 1);
     1.9  by (fast_tac (claset() addIs [eqpoll_imp_lepoll RS
    1.10          (Diff_subset RS subset_imp_lepoll RS lepoll_trans)]) 1);
    1.11  by (REPEAT (resolve_tac [allI,impI] 1));
     2.1 --- a/src/ZF/AC/WO2_AC16.ML	Tue Aug 01 13:43:22 2000 +0200
     2.2 +++ b/src/ZF/AC/WO2_AC16.ML	Tue Aug 01 15:28:21 2000 +0200
     2.3 @@ -256,8 +256,8 @@
     2.4  
     2.5  
     2.6  Goal "[| recfunAC16(f,g,y,a) <= {X: Pow(A). X eqpoll n};  \
     2.7 -\               A eqpoll a; y<a; ~Finite(a); Card(a); n:nat |]  \
     2.8 -\               ==> Union(recfunAC16(f,g,y,a)) lesspoll a";
     2.9 +\        A eqpoll a;  y<a;  ~Finite(a);  Card(a);  n:nat |]  \
    2.10 +\     ==> Union(recfunAC16(f,g,y,a)) lesspoll a";
    2.11  by (eresolve_tac [eqpoll_def RS def_imp_iff RS iffD1 RS exE] 1);
    2.12  by (rtac Union_lesspoll 1 THEN (TRYALL assume_tac));
    2.13  by (eresolve_tac [lt_Ord RS recfunAC16_lepoll_index] 3);
    2.14 @@ -270,12 +270,12 @@
    2.15  
    2.16  Goal "[| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)};  \
    2.17  \       Card(a); ~ Finite(a); A eqpoll a;  \
    2.18 -\       k : nat; m : nat; y<a;  \
    2.19 +\       k: nat;  y<a;  \
    2.20  \       fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}) |]  \
    2.21  \       ==> A - Union(recfunAC16(f, fa, y, a)) - fa`y eqpoll a";
    2.22  by (rtac dbl_Diff_eqpoll_Card 1 THEN (TRYALL assume_tac));
    2.23  by (rtac Union_recfunAC16_lesspoll 1 THEN (REPEAT (assume_tac 1)));
    2.24 -by (eresolve_tac [add_type RS nat_succI] 1 THEN (assume_tac 1));
    2.25 +by (Simp_tac 1);
    2.26  by (resolve_tac [nat_succI RSN 
    2.27  		 (2, bexI RS (Finite_def RS def_imp_iff RS iffD2)) RS 
    2.28  		 (Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord))] 1
     3.1 --- a/src/ZF/Arith.ML	Tue Aug 01 13:43:22 2000 +0200
     3.2 +++ b/src/ZF/Arith.ML	Tue Aug 01 15:28:21 2000 +0200
     3.3 @@ -28,163 +28,317 @@
     3.4  bind_thm ("zero_lt_natE", lemma RS bexE);
     3.5  
     3.6  
     3.7 +(** natify: coercion to "nat" **)
     3.8 +
     3.9 +Goalw [pred_def] "pred(succ(y)) = y";
    3.10 +by Auto_tac;  
    3.11 +qed "pred_succ_eq";
    3.12 +Addsimps [pred_succ_eq];
    3.13 +
    3.14 +Goal "natify(succ(x)) = succ(natify(x))";
    3.15 +by (rtac (natify_def RS def_Vrecursor RS trans) 1);
    3.16 +by Auto_tac;  
    3.17 +qed "natify_succ";
    3.18 +Addsimps [natify_succ];
    3.19 +
    3.20 +Goal "natify(0) = 0";
    3.21 +by (rtac (natify_def RS def_Vrecursor RS trans) 1);
    3.22 +by Auto_tac;  
    3.23 +qed "natify_0";
    3.24 +Addsimps [natify_0];
    3.25 +
    3.26 +Goal "ALL z. x ~= succ(z) ==> natify(x) = 0";
    3.27 +by (rtac (natify_def RS def_Vrecursor RS trans) 1);
    3.28 +by Auto_tac;  
    3.29 +qed "natify_non_succ";
    3.30 +
    3.31 +Goal "natify(x) : nat";
    3.32 +by (eps_ind_tac "x" 1);
    3.33 +by (case_tac "EX z. x1 = succ(z)" 1);
    3.34 +by (auto_tac (claset(), simpset() addsimps [natify_non_succ]));  
    3.35 +qed "natify_in_nat";
    3.36 +AddIffs [natify_in_nat];
    3.37 +AddTCs [natify_in_nat];
    3.38 +
    3.39 +Goal "n : nat ==> natify(n) = n";
    3.40 +by (induct_tac "n" 1);
    3.41 +by Auto_tac;
    3.42 +qed "natify_ident";
    3.43 +Addsimps [natify_ident];
    3.44 +
    3.45 +
    3.46 +(*** Collapsing rules: to remove natify from arithmetic expressions ***)
    3.47 +
    3.48 +Goal "natify(natify(x)) = natify(x)";
    3.49 +by (Simp_tac 1);
    3.50 +qed "natify_idem";
    3.51 +Addsimps [natify_idem];
    3.52 +
    3.53  (** Addition **)
    3.54  
    3.55 -Goal "[| m:nat;  n:nat |] ==> m #+ n : nat";
    3.56 +Goal "natify(m) #+ n = m #+ n";
    3.57 +by (simp_tac (simpset() addsimps [add_def]) 1);
    3.58 +qed "add_natify1";
    3.59 +
    3.60 +Goal "m #+ natify(n) = m #+ n";
    3.61 +by (simp_tac (simpset() addsimps [add_def]) 1);
    3.62 +qed "add_natify2";
    3.63 +Addsimps [add_natify1, add_natify2];
    3.64 +
    3.65 +(** Multiplication **)
    3.66 +
    3.67 +Goal "natify(m) #* n = m #* n";
    3.68 +by (simp_tac (simpset() addsimps [mult_def]) 1);
    3.69 +qed "mult_natify1";
    3.70 +
    3.71 +Goal "m #* natify(n) = m #* n";
    3.72 +by (simp_tac (simpset() addsimps [mult_def]) 1);
    3.73 +qed "mult_natify2";
    3.74 +Addsimps [mult_natify1, mult_natify2];
    3.75 +
    3.76 +(** Difference **)
    3.77 +
    3.78 +Goal "natify(m) #- n = m #- n";
    3.79 +by (simp_tac (simpset() addsimps [diff_def]) 1);
    3.80 +qed "diff_natify1";
    3.81 +
    3.82 +Goal "m #- natify(n) = m #- n";
    3.83 +by (simp_tac (simpset() addsimps [diff_def]) 1);
    3.84 +qed "diff_natify2";
    3.85 +Addsimps [diff_natify1, diff_natify2];
    3.86 +
    3.87 +
    3.88 +(*** Typing rules ***)
    3.89 +
    3.90 +(** Addition **)
    3.91 +
    3.92 +Goal "[| m:nat;  n:nat |] ==> m ##+ n : nat";
    3.93  by (induct_tac "m" 1);
    3.94  by Auto_tac;
    3.95 +qed "raw_add_type";
    3.96 +
    3.97 +Goal "m #+ n : nat";
    3.98 +by (simp_tac (simpset() addsimps [add_def, raw_add_type]) 1);
    3.99  qed "add_type";
   3.100 -Addsimps [add_type];
   3.101 +AddIffs [add_type];
   3.102  AddTCs [add_type];
   3.103  
   3.104  (** Multiplication **)
   3.105  
   3.106 -Goal "[| m:nat;  n:nat |] ==> m #* n : nat";
   3.107 +Goal "[| m:nat;  n:nat |] ==> m ##* n : nat";
   3.108  by (induct_tac "m" 1);
   3.109 -by Auto_tac;
   3.110 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [raw_add_type])));
   3.111 +qed "raw_mult_type";
   3.112 +
   3.113 +Goal "m #* n : nat";
   3.114 +by (simp_tac (simpset() addsimps [mult_def, raw_mult_type]) 1);
   3.115  qed "mult_type";
   3.116 -Addsimps [mult_type];
   3.117 +AddIffs [mult_type];
   3.118  AddTCs [mult_type];
   3.119  
   3.120  
   3.121  (** Difference **)
   3.122  
   3.123 -Goal "[| m:nat;  n:nat |] ==> m #- n : nat";
   3.124 +Goal "[| m:nat;  n:nat |] ==> m ##- n : nat";
   3.125  by (induct_tac "n" 1);
   3.126  by Auto_tac;
   3.127  by (fast_tac (claset() addIs [nat_case_type]) 1);
   3.128 +qed "raw_diff_type";
   3.129 +
   3.130 +Goal "m #- n : nat";
   3.131 +by (simp_tac (simpset() addsimps [diff_def, raw_diff_type]) 1);
   3.132  qed "diff_type";
   3.133 -Addsimps [diff_type];
   3.134 +AddIffs [diff_type];
   3.135  AddTCs [diff_type];
   3.136  
   3.137 -Goal "n:nat ==> 0 #- n = 0";
   3.138 -by (induct_tac "n" 1);
   3.139 +Goalw [diff_def] "0 #- n = 0";
   3.140 +by (rtac (natify_in_nat RS nat_induct) 1);
   3.141  by Auto_tac;
   3.142  qed "diff_0_eq_0";
   3.143  
   3.144  (*Must simplify BEFORE the induction: else we get a critical pair*)
   3.145 -Goal "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n";
   3.146 -by (Asm_simp_tac 1);
   3.147 -by (induct_tac "n" 1);
   3.148 +Goal "succ(m) #- succ(n) = m #- n";
   3.149 +by (simp_tac (simpset() addsimps [diff_def]) 1);
   3.150 +by (res_inst_tac [("x1","n")] (natify_in_nat RS nat_induct) 1);
   3.151  by Auto_tac;
   3.152  qed "diff_succ_succ";
   3.153  
   3.154 -Addsimps [diff_0_eq_0, diff_succ_succ];
   3.155 +(*This defining property is no longer wanted*)
   3.156 +Delsimps [raw_diff_succ];  
   3.157  
   3.158 -(*This defining property is no longer wanted*)
   3.159 -Delsimps [diff_SUCC];  
   3.160 +(*Natify has weakened this law, compared with the older approach*)
   3.161 +Goal "m #- 0 = natify(m)";
   3.162 +by (asm_simp_tac (simpset() addsimps [diff_def]) 1);
   3.163 +qed "diff_0";
   3.164  
   3.165 -val prems = goal Arith.thy 
   3.166 -    "[| m:nat;  n:nat |] ==> m #- n le m";
   3.167 -by (rtac (prems MRS diff_induct) 1);
   3.168 -by (etac leE 3);
   3.169 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems @ [le_iff])));
   3.170 +Addsimps [diff_0, diff_0_eq_0, diff_succ_succ];
   3.171 +
   3.172 +Goal "m:nat ==> (m #- n) le m";
   3.173 +by (subgoal_tac "(m #- natify(n)) le m" 1);
   3.174 +by (res_inst_tac [("m","m"), ("n","natify(n)")] diff_induct 2);
   3.175 +by (etac leE 6);
   3.176 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [le_iff])));
   3.177  qed "diff_le_self";
   3.178  
   3.179 -(*** Simplification over add, mult, diff ***)
   3.180 -
   3.181 -val arith_typechecks = [add_type, mult_type, diff_type];
   3.182 -
   3.183  
   3.184  (*** Addition ***)
   3.185  
   3.186 +(*Natify has weakened this law, compared with the older approach*)
   3.187 +Goal "0 #+ m = natify(m)";
   3.188 +by (asm_simp_tac (simpset() addsimps [add_def]) 1);
   3.189 +qed "add_0";
   3.190 +
   3.191 +Goal "succ(m) #+ n = succ(m #+ n)";
   3.192 +by (asm_simp_tac (simpset() addsimps [add_def]) 1);
   3.193 +qed "add_succ";
   3.194 +
   3.195 +Addsimps [add_0, add_succ];
   3.196 +
   3.197  (*Associative law for addition*)
   3.198 -Goal "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)";
   3.199 -by (induct_tac "m" 1);
   3.200 +Goal "(m #+ n) #+ k = m #+ (n #+ k)";
   3.201 +by (subgoal_tac "(natify(m) #+ natify(n)) #+ natify(k) = \
   3.202 +\                natify(m) #+ (natify(n) #+ natify(k))" 1);
   3.203 +by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   3.204  by Auto_tac;
   3.205  qed "add_assoc";
   3.206  
   3.207  (*The following two lemmas are used for add_commute and sometimes
   3.208    elsewhere, since they are safe for rewriting.*)
   3.209 -Goal "m:nat ==> m #+ 0 = m";
   3.210 -by (induct_tac "m" 1);
   3.211 +Goal "m #+ 0 = natify(m)";
   3.212 +by (subgoal_tac "natify(m) #+ 0 = natify(m)" 1);
   3.213 +by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   3.214 +by Auto_tac;
   3.215 +qed "add_0_right_natify";
   3.216 +
   3.217 +Goalw [add_def] "m #+ succ(n) = succ(m #+ n)";
   3.218 +by (res_inst_tac [("n","natify(m)")] nat_induct 1);
   3.219 +by Auto_tac;
   3.220 +qed "add_succ_right";
   3.221 +
   3.222 +Addsimps [add_0_right_natify, add_succ_right];
   3.223 +
   3.224 +Goal "m: nat ==> m #+ 0 = m";
   3.225  by Auto_tac;
   3.226  qed "add_0_right";
   3.227  
   3.228 -Goal "m:nat ==> m #+ succ(n) = succ(m #+ n)";
   3.229 -by (induct_tac "m" 1);
   3.230 -by Auto_tac;
   3.231 -qed "add_succ_right";
   3.232 -
   3.233 -Addsimps [add_0_right, add_succ_right];
   3.234 -
   3.235  (*Commutative law for addition*)  
   3.236 -Goal "[| m:nat;  n:nat |] ==> m #+ n = n #+ m";
   3.237 -by (induct_tac "n" 1);
   3.238 +Goal "m #+ n = n #+ m";
   3.239 +by (subgoal_tac "natify(m) #+ natify(n) = natify(n) #+ natify(m)" 1);
   3.240 +by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   3.241  by Auto_tac;
   3.242  qed "add_commute";
   3.243  
   3.244  (*for a/c rewriting*)
   3.245 -Goal "[| m:nat;  n:nat |] ==> m#+(n#+k)=n#+(m#+k)";
   3.246 -by (asm_simp_tac (simpset() addsimps [add_assoc RS sym, add_commute]) 1);
   3.247 +Goal "m#+(n#+k)=n#+(m#+k)";
   3.248 +by (rtac (add_commute RS trans) 1);
   3.249 +by (rtac (add_assoc RS trans) 1);
   3.250 +by (rtac (add_commute RS subst_context) 1);
   3.251  qed "add_left_commute";
   3.252  
   3.253  (*Addition is an AC-operator*)
   3.254  val add_ac = [add_assoc, add_commute, add_left_commute];
   3.255  
   3.256  (*Cancellation law on the left*)
   3.257 -Goal "[| k #+ m = k #+ n;  k:nat |] ==> m=n";
   3.258 +Goal "[| k ##+ m = k ##+ n;  k:nat |] ==> m=n";
   3.259  by (etac rev_mp 1);
   3.260  by (induct_tac "k" 1);
   3.261  by Auto_tac;
   3.262 +qed "raw_add_left_cancel";
   3.263 +
   3.264 +Goalw [add_def] "k #+ m = k #+ n ==> natify(m) = natify(n)";
   3.265 +by (dtac raw_add_left_cancel 1);
   3.266 +by Auto_tac;
   3.267 +qed "add_left_cancel_natify";
   3.268 +
   3.269 +Goal "[| k #+ m = k #+ n;  m:nat;  n:nat |] ==> m = n";
   3.270 +by (dtac add_left_cancel_natify 1);
   3.271 +by Auto_tac;
   3.272  qed "add_left_cancel";
   3.273  
   3.274 +
   3.275  (*** Multiplication ***)
   3.276  
   3.277 +Goal "0 #* m = 0";
   3.278 +by (simp_tac (simpset() addsimps [mult_def]) 1);
   3.279 +qed "mult_0";
   3.280 +
   3.281 +Goal "succ(m) #* n = n #+ (m #* n)";
   3.282 +by (simp_tac (simpset() addsimps [add_def, mult_def, raw_mult_type]) 1);
   3.283 +qed "mult_succ";
   3.284 +
   3.285 +Addsimps [mult_0, mult_succ];
   3.286 +
   3.287  (*right annihilation in product*)
   3.288 -Goal "m:nat ==> m #* 0 = 0";
   3.289 -by (induct_tac "m" 1);
   3.290 +Goalw [mult_def] "m #* 0 = 0";
   3.291 +by (res_inst_tac [("n","natify(m)")] nat_induct 1);
   3.292  by Auto_tac;
   3.293  qed "mult_0_right";
   3.294  
   3.295  (*right successor law for multiplication*)
   3.296 -Goal "[| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)";
   3.297 -by (induct_tac "m" 1);
   3.298 +Goal "m #* succ(n) = m #+ (m #* n)";
   3.299 +by (subgoal_tac "natify(m) #* succ(natify(n)) = \
   3.300 +\                natify(m) #+ (natify(m) #* natify(n))" 1);
   3.301 +by (full_simp_tac (simpset() addsimps [add_def, mult_def]) 1);
   3.302 +by (res_inst_tac [("n","natify(m)")] nat_induct 1);
   3.303  by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
   3.304  qed "mult_succ_right";
   3.305  
   3.306  Addsimps [mult_0_right, mult_succ_right];
   3.307  
   3.308 -Goal "n:nat ==> 1 #* n = n";
   3.309 +Goal "1 #* n = natify(n)";
   3.310 +by Auto_tac;
   3.311 +qed "mult_1_natify";
   3.312 +
   3.313 +Goal "n #* 1 = natify(n)";
   3.314 +by Auto_tac;
   3.315 +qed "mult_1_right_natify";
   3.316 +
   3.317 +Addsimps [mult_1_natify, mult_1_right_natify];
   3.318 +
   3.319 +Goal "n : nat ==> 1 #* n = n";
   3.320  by (Asm_simp_tac 1);
   3.321  qed "mult_1";
   3.322  
   3.323 -Goal "n:nat ==> n #* 1 = n";
   3.324 +Goal "n : nat ==> n #* 1 = n";
   3.325  by (Asm_simp_tac 1);
   3.326  qed "mult_1_right";
   3.327  
   3.328 -Addsimps [mult_1, mult_1_right];
   3.329 -
   3.330  (*Commutative law for multiplication*)
   3.331 -Goal "[| m:nat;  n:nat |] ==> m #* n = n #* m";
   3.332 -by (induct_tac "m" 1);
   3.333 +Goal "m #* n = n #* m";
   3.334 +by (subgoal_tac "natify(m) #* natify(n) = natify(n) #* natify(m)" 1);
   3.335 +by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   3.336  by Auto_tac;
   3.337  qed "mult_commute";
   3.338  
   3.339  (*addition distributes over multiplication*)
   3.340 -Goal "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)";
   3.341 -by (induct_tac "m" 1);
   3.342 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
   3.343 +Goal "(m #+ n) #* k = (m #* k) #+ (n #* k)";
   3.344 +by (subgoal_tac "(natify(m) #+ natify(n)) #* natify(k) = \
   3.345 +\                (natify(m) #* natify(k)) #+ (natify(n) #* natify(k))" 1);
   3.346 +by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   3.347 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_assoc RS sym])));
   3.348  qed "add_mult_distrib";
   3.349  
   3.350 -(*Distributive law on the left; requires an extra typing premise*)
   3.351 -Goal "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)";
   3.352 -by (induct_tac "m" 1);
   3.353 -by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
   3.354 +(*Distributive law on the left*)
   3.355 +Goal "k #* (m #+ n) = (k #* m) #+ (k #* n)";
   3.356 +by (subgoal_tac "natify(k) #* (natify(m) #+ natify(n)) = \
   3.357 +\                (natify(k) #* natify(m)) #+ (natify(k) #* natify(n))" 1);
   3.358 +by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   3.359 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
   3.360  qed "add_mult_distrib_left";
   3.361  
   3.362  (*Associative law for multiplication*)
   3.363 -Goal "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)";
   3.364 -by (induct_tac "m" 1);
   3.365 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
   3.366 +Goal "(m #* n) #* k = m #* (n #* k)";
   3.367 +by (subgoal_tac "(natify(m) #* natify(n)) #* natify(k) = \
   3.368 +\                natify(m) #* (natify(n) #* natify(k))" 1);
   3.369 +by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   3.370 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_mult_distrib])));
   3.371  qed "mult_assoc";
   3.372  
   3.373  (*for a/c rewriting*)
   3.374 -Goal "[| m:nat;  n:nat;  k:nat |] ==> m #* (n #* k) = n #* (m #* k)";
   3.375 +Goal "m #* (n #* k) = n #* (m #* k)";
   3.376  by (rtac (mult_commute RS trans) 1);
   3.377 -by (rtac (mult_assoc RS trans) 3);
   3.378 -by (rtac (mult_commute RS subst_context) 6);
   3.379 -by (REPEAT (ares_tac [mult_type] 1));
   3.380 +by (rtac (mult_assoc RS trans) 1);
   3.381 +by (rtac (mult_commute RS subst_context) 1);
   3.382  qed "mult_left_commute";
   3.383  
   3.384  val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
   3.385 @@ -192,18 +346,22 @@
   3.386  
   3.387  (*** Difference ***)
   3.388  
   3.389 -Goal "m:nat ==> m #- m = 0";
   3.390 -by (induct_tac "m" 1);
   3.391 +Goal "m #- m = 0";
   3.392 +by (subgoal_tac "natify(m) #- natify(m) = 0" 1);
   3.393 +by (rtac (natify_in_nat RS nat_induct) 2);
   3.394  by Auto_tac;
   3.395  qed "diff_self_eq_0";
   3.396  
   3.397 -(*Addition is the inverse of subtraction*)
   3.398 +(**Addition is the inverse of subtraction**)
   3.399 +
   3.400 +(*We need m:nat even if we replace the RHS by natify(m), for consider e.g.
   3.401 +  n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 ~= 0 = natify(m).*)
   3.402  Goal "[| n le m;  m:nat |] ==> n #+ (m#-n) = m";
   3.403  by (ftac lt_nat_in_nat 1);
   3.404  by (etac nat_succI 1);
   3.405  by (etac rev_mp 1);
   3.406  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   3.407 -by (ALLGOALS Asm_simp_tac);
   3.408 +by Auto_tac;
   3.409  qed "add_diff_inverse";
   3.410  
   3.411  Goal "[| n le m;  m:nat |] ==> (m#-n) #+ n = m";
   3.412 @@ -212,7 +370,7 @@
   3.413  by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1);
   3.414  qed "add_diff_inverse2";
   3.415  
   3.416 -(*Proof is IDENTICAL to that above*)
   3.417 +(*Proof is IDENTICAL to that of add_diff_inverse*)
   3.418  Goal "[| n le m;  m:nat |] ==> succ(m) #- n = succ(m#-n)";
   3.419  by (ftac lt_nat_in_nat 1);
   3.420  by (etac nat_succI 1);
   3.421 @@ -221,7 +379,7 @@
   3.422  by (ALLGOALS Asm_simp_tac);
   3.423  qed "diff_succ";
   3.424  
   3.425 -Goal "[| m: nat; n: nat |] ==> 0 < n #- m  <->  m<n";
   3.426 +Goal "[| m: nat; n: nat |] ==> 0 < (n #- m)   <->   m<n";
   3.427  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   3.428  by (ALLGOALS Asm_simp_tac);
   3.429  qed "zero_less_diff";
   3.430 @@ -230,45 +388,52 @@
   3.431  
   3.432  (** Subtraction is the inverse of addition. **)
   3.433  
   3.434 -Goal "[| m:nat;  n:nat |] ==> (n#+m) #- n = m";
   3.435 -by (induct_tac "n" 1);
   3.436 +Goal "(n#+m) #- n = natify(m)";
   3.437 +by (subgoal_tac "(natify(n) #+ m) #- natify(n) = natify(m)" 1);
   3.438 +by (res_inst_tac [("n","natify(n)")] nat_induct 2);
   3.439  by Auto_tac;
   3.440  qed "diff_add_inverse";
   3.441  
   3.442 -Goal "[| m:nat;  n:nat |] ==> (m#+n) #- n = m";
   3.443 -by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1);
   3.444 -by (REPEAT (ares_tac [diff_add_inverse] 1));
   3.445 +Goal "(m#+n) #- n = natify(m)";
   3.446 +by (simp_tac (simpset() addsimps [inst "m" "m" add_commute, 
   3.447 +				  diff_add_inverse]) 1);
   3.448  qed "diff_add_inverse2";
   3.449  
   3.450 -Goal "[| k:nat; m: nat; n: nat |] ==> (k#+m) #- (k#+n) = m #- n";
   3.451 -by (induct_tac "k" 1);
   3.452 -by (ALLGOALS Asm_simp_tac);
   3.453 +Goal "(k#+m) #- (k#+n) = m #- n";
   3.454 +by (subgoal_tac "(natify(k) #+ natify(m)) #- (natify(k) #+ natify(n)) = \
   3.455 +\                natify(m) #- natify(n)" 1);
   3.456 +by (res_inst_tac [("n","natify(k)")] nat_induct 2);
   3.457 +by Auto_tac;
   3.458  qed "diff_cancel";
   3.459  
   3.460 -Goal "[| k:nat; m: nat; n: nat |] ==> (m#+k) #- (n#+k) = m #- n";
   3.461 -by (asm_simp_tac
   3.462 -    (simpset() addsimps [inst "n" "k" add_commute, diff_cancel]) 1);
   3.463 +Goal "(m#+k) #- (n#+k) = m #- n";
   3.464 +by (simp_tac (simpset() addsimps [inst "n" "k" add_commute, diff_cancel]) 1);
   3.465  qed "diff_cancel2";
   3.466  
   3.467 -Goal "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
   3.468 -by (induct_tac "n" 1);
   3.469 +Goal "n #- (n#+m) = 0";
   3.470 +by (subgoal_tac "natify(n) #- (natify(n) #+ natify(m)) = 0" 1);
   3.471 +by (res_inst_tac [("n","natify(n)")] nat_induct 2);
   3.472  by Auto_tac;
   3.473  qed "diff_add_0";
   3.474  
   3.475  (** Difference distributes over multiplication **)
   3.476  
   3.477 -Goal "[| m:nat; n: nat; k:nat |] ==> (m #- n) #* k = (m #* k) #- (n #* k)";
   3.478 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   3.479 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
   3.480 +Goal "(m #- n) #* k = (m #* k) #- (n #* k)";
   3.481 +by (subgoal_tac "(natify(m) #- natify(n)) #* natify(k) = \
   3.482 +\                (natify(m) #* natify(k)) #- (natify(n) #* natify(k))" 1);
   3.483 +by (res_inst_tac [("m","natify(m)"),("n","natify(n)")] diff_induct 2);
   3.484 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [diff_cancel])));
   3.485  qed "diff_mult_distrib" ;
   3.486  
   3.487 -Goal "[| m:nat; n: nat; k:nat |] ==> k #* (m #- n) = (k #* m) #- (k #* n)";
   3.488 -by (asm_simp_tac
   3.489 +Goal "k #* (m #- n) = (k #* m) #- (k #* n)";
   3.490 +by (simp_tac
   3.491      (simpset() addsimps [inst "m" "k" mult_commute, diff_mult_distrib]) 1);
   3.492 -qed "diff_mult_distrib2" ;
   3.493 +qed "diff_mult_distrib2";
   3.494 +
   3.495  
   3.496  (*** Remainder ***)
   3.497  
   3.498 +(*We need m:nat even with natify*)
   3.499  Goal "[| 0<n;  n le m;  m:nat |] ==> m #- n < m";
   3.500  by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   3.501  by (etac rev_mp 1);
   3.502 @@ -390,20 +555,22 @@
   3.503  
   3.504  (**** Additional theorems about "le" ****)
   3.505  
   3.506 -Goal "[| m:nat;  n:nat |] ==> m le m #+ n";
   3.507 +Goal "m:nat ==> m le (m #+ n)";
   3.508  by (induct_tac "m" 1);
   3.509  by (ALLGOALS Asm_simp_tac);
   3.510  qed "add_le_self";
   3.511  
   3.512 -Goal "[| m:nat;  n:nat |] ==> m le n #+ m";
   3.513 +Goal "m:nat ==> m le (n #+ m)";
   3.514  by (stac add_commute 1);
   3.515 -by (REPEAT (ares_tac [add_le_self] 1));
   3.516 +by (etac add_le_self 1);
   3.517  qed "add_le_self2";
   3.518  
   3.519  (*** Monotonicity of Addition ***)
   3.520  
   3.521 -(*strict, in 1st argument; proof is by rule induction on 'less than'*)
   3.522 -Goal "[| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
   3.523 +(*strict, in 1st argument; proof is by rule induction on 'less than'.
   3.524 +  Still need j:nat, for consider j = omega.  Then we can have i<omega,
   3.525 +  which is the same as i:nat, but natify(j)=0, so the conclusion fails.*)
   3.526 +Goal "[| i<j; j:nat |] ==> i#+k < j#+k";
   3.527  by (ftac lt_nat_in_nat 1);
   3.528  by (assume_tac 1);
   3.529  by (etac succ_lt_induct 1);
   3.530 @@ -413,11 +580,11 @@
   3.531  (*strict, in both arguments*)
   3.532  Goal "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
   3.533  by (rtac (add_lt_mono1 RS lt_trans) 1);
   3.534 -by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
   3.535 +by (REPEAT (assume_tac 1));
   3.536  by (EVERY [stac add_commute 1,
   3.537 -           stac add_commute 3,
   3.538 -           rtac add_lt_mono1 5]);
   3.539 -by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
   3.540 +           stac add_commute 1,
   3.541 +           rtac add_lt_mono1 1]);
   3.542 +by (REPEAT (assume_tac 1));
   3.543  qed "add_lt_mono";
   3.544  
   3.545  (*A [clumsy] way of lifting < monotonicity to le monotonicity *)
   3.546 @@ -431,7 +598,7 @@
   3.547  qed "Ord_lt_mono_imp_le_mono";
   3.548  
   3.549  (*le monotonicity, 1st argument*)
   3.550 -Goal "[| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
   3.551 +Goal "[| i le j; j:nat |] ==> i#+k le j#+k";
   3.552  by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1);
   3.553  by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1));
   3.554  qed "add_le_mono1";
   3.555 @@ -439,32 +606,34 @@
   3.556  (* le monotonicity, BOTH arguments*)
   3.557  Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
   3.558  by (rtac (add_le_mono1 RS le_trans) 1);
   3.559 -by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   3.560 +by (REPEAT (assume_tac 1));
   3.561  by (EVERY [stac add_commute 1,
   3.562 -           stac add_commute 3,
   3.563 -           rtac add_le_mono1 5]);
   3.564 -by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   3.565 +           stac add_commute 1,
   3.566 +           rtac add_le_mono1 1]);
   3.567 +by (REPEAT (assume_tac 1));
   3.568  qed "add_le_mono";
   3.569  
   3.570  (*** Monotonicity of Multiplication ***)
   3.571  
   3.572 -Goal "[| i le j; j:nat; k:nat |] ==> i#*k le j#*k";
   3.573 -by (ftac lt_nat_in_nat 1);
   3.574 -by (induct_tac "k" 2);
   3.575 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
   3.576 +Goal "[| i le j; j:nat |] ==> (i#*k) le (j#*k)";
   3.577 +by (subgoal_tac "natify(i)#*natify(k) le j#*natify(k)" 1);
   3.578 +by (ftac lt_nat_in_nat 2);
   3.579 +by (res_inst_tac [("n","natify(k)")] nat_induct 3);
   3.580 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_le_mono])));
   3.581  qed "mult_le_mono1";
   3.582  
   3.583  (* le monotonicity, BOTH arguments*)
   3.584  Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l";
   3.585  by (rtac (mult_le_mono1 RS le_trans) 1);
   3.586 -by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   3.587 +by (REPEAT (assume_tac 1));
   3.588  by (EVERY [stac mult_commute 1,
   3.589 -           stac mult_commute 3,
   3.590 -           rtac mult_le_mono1 5]);
   3.591 -by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   3.592 +           stac mult_commute 1,
   3.593 +           rtac mult_le_mono1 1]);
   3.594 +by (REPEAT (assume_tac 1));
   3.595  qed "mult_le_mono";
   3.596  
   3.597 -(*strict, in 1st argument; proof is by induction on k>0*)
   3.598 +(*strict, in 1st argument; proof is by induction on k>0.
   3.599 +  I can't see how to relax the typing conditions.*)
   3.600  Goal "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
   3.601  by (etac zero_lt_natE 1);
   3.602  by (ftac lt_nat_in_nat 2);
   3.603 @@ -473,17 +642,35 @@
   3.604  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
   3.605  qed "mult_lt_mono2";
   3.606  
   3.607 -Goal "[| i<j; 0<c; i:nat; j:nat; c:nat |] ==> i#*c < j#*c";
   3.608 -by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, mult_commute]) 1);
   3.609 +Goal "[| i<j; 0<k; j:nat; k:nat |] ==> i#*k < j#*k";
   3.610 +by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, 
   3.611 +				      inst "n" "k" mult_commute]) 1);
   3.612  qed "mult_lt_mono1";
   3.613  
   3.614 -Goal "[| m: nat; n: nat |] ==> 0 < m#*n <-> 0<m & 0<n";
   3.615 -by (best_tac (claset() addEs [natE] addss (simpset())) 1);
   3.616 +Goal "m#+n = 0 <-> natify(m)=0 & natify(n)=0";
   3.617 +by (subgoal_tac "natify(m) #+ natify(n) = 0 <-> natify(m)=0 & natify(n)=0" 1);
   3.618 +by (res_inst_tac [("n","natify(m)")] natE 2);
   3.619 + by (res_inst_tac [("n","natify(n)")] natE 4);
   3.620 +by Auto_tac;  
   3.621 +qed "add_eq_0_iff";
   3.622 +AddIffs [add_eq_0_iff];
   3.623 +
   3.624 +Goal "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)";
   3.625 +by (subgoal_tac "0 < natify(m)#*natify(n) <-> \
   3.626 +\                0 < natify(m) & 0 < natify(n)" 1);
   3.627 +by (res_inst_tac [("n","natify(m)")] natE 2);
   3.628 + by (res_inst_tac [("n","natify(n)")] natE 4);
   3.629 +  by (res_inst_tac [("n","natify(n)")] natE 3);
   3.630 +by Auto_tac;  
   3.631  qed "zero_lt_mult_iff";
   3.632  
   3.633 -Goal "[| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1";
   3.634 -by (best_tac (claset() addEs [natE] addss (simpset())) 1);
   3.635 +Goal "m#*n = 1 <-> natify(m)=1 & natify(n)=1";
   3.636 +by (subgoal_tac "natify(m) #* natify(n) = 1 <-> natify(m)=1 & natify(n)=1" 1);
   3.637 +by (res_inst_tac [("n","natify(m)")] natE 2);
   3.638 + by (res_inst_tac [("n","natify(n)")] natE 4);
   3.639 +by Auto_tac;  
   3.640  qed "mult_eq_1_iff";
   3.641 +AddIffs [zero_lt_mult_iff, mult_eq_1_iff];
   3.642  
   3.643  (*Cancellation law for division*)
   3.644  Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n";
   3.645 @@ -512,21 +699,24 @@
   3.646  qed "mult_mod_distrib";
   3.647  
   3.648  (*Lemma for gcd*)
   3.649 -Goal "[| m = m#*n; m: nat; n: nat |] ==> n=1 | m=0";
   3.650 +Goal "m = m#*n ==> natify(n)=1 | m=0";
   3.651 +by (subgoal_tac "m: nat" 1);
   3.652 +by (etac ssubst 2);
   3.653  by (rtac disjCI 1);
   3.654  by (dtac sym 1);
   3.655  by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
   3.656 -by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 2);
   3.657 +by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 3);
   3.658  by Auto_tac;
   3.659 +by (subgoal_tac "m #* n = 0" 1);
   3.660 +by (stac (mult_natify2 RS sym) 2);
   3.661 +by (auto_tac (claset(), simpset() delsimps [mult_natify2]));  
   3.662  qed "mult_eq_self_implies_10";
   3.663  
   3.664  (*Thanks to Sten Agerholm*)
   3.665 -Goal "[|k#+m le k#+n; k:nat |] ==> m le n";
   3.666 -by (etac rev_mp 1);
   3.667 -by (induct_tac "k" 1);
   3.668 -by (Asm_simp_tac 1);
   3.669 -by Safe_tac;
   3.670 -by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt]) 1);
   3.671 +Goal "[| k#+m le k#+n; m: nat; n: nat |] ==> m le n";
   3.672 +by (res_inst_tac [("P", "natify(k)#+m le natify(k)#+n")] rev_mp 1);
   3.673 +by (res_inst_tac [("n","natify(k)")] nat_induct 2);
   3.674 +by Auto_tac;
   3.675  qed "add_le_elim1";
   3.676  
   3.677  Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
     4.1 --- a/src/ZF/Arith.thy	Tue Aug 01 13:43:22 2000 +0200
     4.2 +++ b/src/ZF/Arith.thy	Tue Aug 01 15:28:21 2000 +0200
     4.3 @@ -6,38 +6,47 @@
     4.4  Arithmetic operators and their definitions
     4.5  *)
     4.6  
     4.7 -Arith = Epsilon + 
     4.8 -
     4.9 -setup setup_datatypes
    4.10 +Arith = Univ + 
    4.11  
    4.12 -(*The natural numbers as a datatype*)
    4.13 -rep_datatype 
    4.14 -  elim		natE
    4.15 -  induct	nat_induct
    4.16 -  case_eqns	nat_case_0, nat_case_succ
    4.17 -  recursor_eqns recursor_0, recursor_succ
    4.18 +constdefs
    4.19 +  pred   :: i=>i    (*inverse of succ*)
    4.20 +    "pred(y) == THE x. y = succ(x)"
    4.21  
    4.22 +  natify :: i=>i    (*coerces non-nats to nats*)
    4.23 +    "natify == Vrecursor(%f a. if a = succ(pred(a)) then succ(f`pred(a))
    4.24 +                                                    else 0)"
    4.25  
    4.26  consts
    4.27 -    "#*" :: [i,i]=>i                    (infixl 70)
    4.28 -    div  :: [i,i]=>i                    (infixl 70) 
    4.29 -    mod  :: [i,i]=>i                    (infixl 70)
    4.30 -    "#+" :: [i,i]=>i                    (infixl 65)
    4.31 -    "#-" :: [i,i]=>i                    (infixl 65)
    4.32 +    "##*" :: [i,i]=>i                    (infixl 70)
    4.33 +    "##+" :: [i,i]=>i                    (infixl 65)
    4.34 +    "##-" :: [i,i]=>i                    (infixl 65)
    4.35  
    4.36  primrec
    4.37 -  add_0     "0 #+ n = n"
    4.38 -  add_succ  "succ(m) #+ n = succ(m #+ n)"
    4.39 +  raw_add_0     "0 ##+ n = n"
    4.40 +  raw_add_succ  "succ(m) ##+ n = succ(m ##+ n)"
    4.41 +
    4.42 +primrec
    4.43 +  raw_diff_0     "m ##- 0 = m"
    4.44 +  raw_diff_succ  "m ##- succ(n) = nat_case(0, %x. x, m ##- n)"
    4.45  
    4.46  primrec
    4.47 -  diff_0     "m #- 0 = m"
    4.48 -  diff_SUCC  "m #- succ(n) = nat_case(0, %x. x, m #- n)"
    4.49 +  raw_mult_0    "0 ##* n = 0"
    4.50 +  raw_mult_succ "succ(m) ##* n = n ##+ (m ##* n)"
    4.51 + 
    4.52 +constdefs
    4.53 +  add :: [i,i]=>i                    (infixl "#+" 65)
    4.54 +    "m #+ n == natify(m) ##+ natify(n)"
    4.55 +
    4.56 +  diff :: [i,i]=>i                    (infixl "#-" 65)
    4.57 +    "m #- n == natify(m) ##- natify(n)"
    4.58  
    4.59 -primrec
    4.60 -  mult_0    "0 #* n = 0"
    4.61 -  mult_succ "succ(m) #* n = n #+ (m #* n)"
    4.62 - 
    4.63 -defs
    4.64 -    mod_def  "m mod n == transrec(m, %j f. if j<n then j else f`(j#-n))"
    4.65 -    div_def  "m div n == transrec(m, %j f. if j<n then 0 else succ(f`(j#-n)))"
    4.66 +  mult :: [i,i]=>i                    (infixl "#*" 70)
    4.67 +    "m #* n == natify(m) ##* natify(n)"
    4.68 +
    4.69 +  div  :: [i,i]=>i                    (infixl "div" 70) 
    4.70 +    "m div n == transrec(m, %j f. if j<n then 0 else succ(f`(j#-n)))"
    4.71 +
    4.72 +  mod  :: [i,i]=>i                    (infixl "mod" 70)
    4.73 +    "m mod n == transrec(m, %j f. if j<n then j else f`(j#-n))"
    4.74 +
    4.75  end
     5.1 --- a/src/ZF/CardinalArith.ML	Tue Aug 01 13:43:22 2000 +0200
     5.2 +++ b/src/ZF/CardinalArith.ML	Tue Aug 01 15:28:21 2000 +0200
     5.3 @@ -404,9 +404,9 @@
     5.4  by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2])));
     5.5  qed "csquareD";
     5.6  
     5.7 -Goalw [pred_def]
     5.8 +Goalw [Order.pred_def]
     5.9   "z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)";
    5.10 -by (safe_tac (claset() delrules [SigmaI,succCI]));  (*avoids using succCI,...*)
    5.11 +by (safe_tac (claset() delrules [SigmaI, succCI]));  
    5.12  by (etac (csquareD RS conjE) 1);
    5.13  by (rewtac lt_def);
    5.14  by (ALLGOALS Blast_tac);
     6.1 --- a/src/ZF/Finite.thy	Tue Aug 01 13:43:22 2000 +0200
     6.2 +++ b/src/ZF/Finite.thy	Tue Aug 01 15:28:21 2000 +0200
     6.3 @@ -6,7 +6,18 @@
     6.4  Finite powerset operator
     6.5  *)
     6.6  
     6.7 -Finite = Arith + Inductive +
     6.8 +Finite = Inductive + Nat +
     6.9 +
    6.10 +setup setup_datatypes
    6.11 +
    6.12 +(*The natural numbers as a datatype*)
    6.13 +rep_datatype 
    6.14 +  elim		natE
    6.15 +  induct	nat_induct
    6.16 +  case_eqns	nat_case_0, nat_case_succ
    6.17 +  recursor_eqns recursor_0, recursor_succ
    6.18 +
    6.19 +
    6.20  consts
    6.21    Fin       :: i=>i
    6.22    FiniteFun :: [i,i]=>i         ("(_ -||>/ _)" [61, 60] 60)
     7.1 --- a/src/ZF/Inductive.thy	Tue Aug 01 13:43:22 2000 +0200
     7.2 +++ b/src/ZF/Inductive.thy	Tue Aug 01 15:28:21 2000 +0200
     7.3 @@ -1,5 +1,5 @@
     7.4  (*Dummy theory to document dependencies *)
     7.5  
     7.6 -Inductive = Fixedpt + Sum + QPair + 
     7.7 +Inductive = Fixedpt + mono + 
     7.8  
     7.9  end
     8.1 --- a/src/ZF/Integ/Int.ML	Tue Aug 01 13:43:22 2000 +0200
     8.2 +++ b/src/ZF/Integ/Int.ML	Tue Aug 01 15:28:21 2000 +0200
     8.3 @@ -16,20 +16,6 @@
     8.4  
     8.5  (*** Proving that intrel is an equivalence relation ***)
     8.6  
     8.7 -(*By luck, requires no typing premises for y1, y2,y3*)
     8.8 -val eqa::eqb::prems = goal Arith.thy 
     8.9 -    "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
    8.10 -\       x1: nat; x2: nat; x3: nat |]    ==>    x1 #+ y3 = x3 #+ y1";
    8.11 -by (cut_facts_tac prems 1);
    8.12 -by (res_inst_tac [("k","x2")] add_left_cancel 1);
    8.13 -by (rtac (add_left_commute RS trans) 1);
    8.14 -by Auto_tac;
    8.15 -by (stac eqb 1);
    8.16 -by (rtac (add_left_commute RS trans) 1);
    8.17 -by (stac eqa 3);
    8.18 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_left_commute])));
    8.19 -qed "int_trans_lemma";
    8.20 -
    8.21  (** Natural deduction for intrel **)
    8.22  
    8.23  Goalw [intrel_def]
    8.24 @@ -64,6 +50,16 @@
    8.25  AddSIs [intrelI];
    8.26  AddSEs [intrelE];
    8.27  
    8.28 +val eqa::eqb::prems = goal Arith.thy 
    8.29 +    "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
    8.30 +by (res_inst_tac [("k","x2")] add_left_cancel 1);
    8.31 +by (rtac (add_left_commute RS trans) 1);
    8.32 +by Auto_tac;
    8.33 +by (stac eqb 1);
    8.34 +by (rtac (add_left_commute RS trans) 1);
    8.35 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [eqa, add_left_commute])));
    8.36 +qed "int_trans_lemma";
    8.37 +
    8.38  Goalw [equiv_def, refl_def, sym_def, trans_def]
    8.39      "equiv(nat*nat, intrel)";
    8.40  by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
    8.41 @@ -239,8 +235,7 @@
    8.42  (*The rest should be trivial, but rearranging terms is hard;
    8.43    add_ac does not help rewriting with the assumptions.*)
    8.44  by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
    8.45 -by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
    8.46 -by Auto_tac;
    8.47 +by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 1);
    8.48  by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
    8.49  qed "zadd_congruent2";
    8.50  
     9.1 --- a/src/ZF/List.ML	Tue Aug 01 13:43:22 2000 +0200
     9.2 +++ b/src/ZF/List.ML	Tue Aug 01 15:28:21 2000 +0200
     9.3 @@ -216,7 +216,8 @@
     9.4  by (ALLGOALS Asm_simp_tac);
     9.5  qed "length_map";
     9.6  
     9.7 -Goal "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
     9.8 +Goal "[| xs: list(A); ys: list(A) |] \
     9.9 +\     ==> length(xs@ys) = length(xs) #+ length(ys)";
    9.10  by (induct_tac "xs" 1);
    9.11  by (ALLGOALS Asm_simp_tac);
    9.12  qed "length_app";
    10.1 --- a/src/ZF/List.thy	Tue Aug 01 13:43:22 2000 +0200
    10.2 +++ b/src/ZF/List.thy	Tue Aug 01 15:28:21 2000 +0200
    10.3 @@ -10,7 +10,7 @@
    10.4  although complicating its derivation.
    10.5  *)
    10.6  
    10.7 -List = Datatype + 
    10.8 +List = Datatype + Arith +
    10.9  
   10.10  consts
   10.11    list       :: i=>i
    11.1 --- a/src/ZF/ex/Acc.ML	Tue Aug 01 13:43:22 2000 +0200
    11.2 +++ b/src/ZF/ex/Acc.ML	Tue Aug 01 15:28:21 2000 +0200
    11.3 @@ -9,8 +9,6 @@
    11.4  Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    11.5  *)
    11.6  
    11.7 -open Acc;
    11.8 -
    11.9  (*The introduction rule must require  a:field(r)  
   11.10    Otherwise acc(r) would be a proper class!    *)
   11.11  
    12.1 --- a/src/ZF/ex/Limit.ML	Tue Aug 01 13:43:22 2000 +0200
    12.2 +++ b/src/ZF/ex/Limit.ML	Tue Aug 01 15:28:21 2000 +0200
    12.3 @@ -1345,69 +1345,38 @@
    12.4  (* ARITH_CONV proves the following in HOL. Would like something similar 
    12.5     in Isabelle/ZF. *)
    12.6  
    12.7 -Goal "[|n:nat; m:nat|] ==> succ(m#+n)#-m = succ(n)";
    12.8 -(*Uses add_succ_right the wrong way round!*)
    12.9 +Goal "succ(m#+n)#-m = succ(natify(n))";
   12.10  by (asm_simp_tac
   12.11 -    (simpset_of Nat.thy addsimps [add_succ_right RS sym, diff_add_inverse]) 1);
   12.12 +    (simpset() delsimps [add_succ_right]
   12.13 +	       addsimps [add_succ_right RS sym, diff_add_inverse]) 1);
   12.14  val lemma_succ_sub = result();
   12.15  
   12.16 -Goalw [e_less_def] (* e_less_add *)
   12.17 -    "[|m:nat; k:nat|] ==>    \
   12.18 -\         e_less(DD,ee,m,succ(m#+k)) = (ee`(m#+k))O(e_less(DD,ee,m,m#+k))";
   12.19 +Goalw [e_less_def]
   12.20 +     "e_less(DD,ee,m,succ(m#+k)) = (ee`(m#+k))O(e_less(DD,ee,m,m#+k))";
   12.21  by (asm_simp_tac (simpset() addsimps [lemma_succ_sub,diff_add_inverse]) 1);
   12.22  qed "e_less_add";
   12.23  
   12.24 -(* Again, would like more theorems about arithmetic. *)
   12.25 -
   12.26  Goal "n:nat ==> succ(n) = n #+ 1";
   12.27  by (Asm_simp_tac 1);
   12.28  qed "add1";
   12.29  
   12.30 -Goal "x:nat ==> 0 < x --> succ(x #- 1)=x";
   12.31 -by (induct_tac "x" 1);
   12.32 -by Auto_tac;
   12.33 -qed "succ_sub1";
   12.34 -
   12.35 -Goal (* succ_le_pos *)
   12.36 -    "[|m:nat; k:nat|] ==> succ(m) le m #+ k --> 0 < k";
   12.37 -by (induct_tac "m" 1);
   12.38 -by Auto_tac;
   12.39 -qed "succ_le_pos";
   12.40 -
   12.41 -Goal "[|n:nat; m:nat|] ==> m le n --> (EX k:nat. n = m #+ k)";
   12.42 -by (induct_tac "m" 1);
   12.43 -by Safe_tac;
   12.44 -by (rtac bexI 1);
   12.45 -by (rtac (add_0 RS sym) 1);
   12.46 -by (assume_tac 1);
   12.47 -by (Asm_full_simp_tac 1);
   12.48 -(* Great, by luck I found le_cs. Such cs's and ss's should be documented. *)
   12.49 -by (fast_tac le_cs 1); 
   12.50 -by (asm_simp_tac
   12.51 -    (simpset_of Nat.thy addsimps[add_succ, add_succ_right RS sym]) 1);
   12.52 -by (rtac bexI 1);
   12.53 -by (stac (succ_sub1 RS mp) 1);
   12.54 -(* Instantiation. *)
   12.55 -by (rtac refl 3);
   12.56 -by (assume_tac 1);
   12.57 -by (rtac (succ_le_pos RS mp) 1);
   12.58 -by (assume_tac 3); (* Instantiation *)
   12.59 -by (ALLGOALS Asm_simp_tac);
   12.60 +Goal "[| m le n; n: nat |] ==> EX k: nat. n = m #+ k";
   12.61 +by (dtac less_imp_Suc_add 1);
   12.62 +by Auto_tac;  
   12.63  val lemma_le_exists = result();
   12.64  
   12.65 -val prems = goal thy  (* le_exists *)
   12.66 -    "[|m le n;  !!x. [|n=m#+x; x:nat|] ==> Q; m:nat; n:nat|] ==> Q";
   12.67 -by (rtac (lemma_le_exists RS mp RS bexE) 1);
   12.68 +val prems = Goal
   12.69 +    "[| m le n;  !!x. [|n=m#+x; x:nat|] ==> Q;  n:nat |] ==> Q";
   12.70 +by (rtac (lemma_le_exists RS bexE) 1);
   12.71  by (DEPTH_SOLVE (ares_tac prems 1));
   12.72  qed "le_exists";
   12.73  
   12.74 -Goal  (* e_less_le *)
   12.75 -    "[|m le n; m:nat; n:nat|] ==>   \
   12.76 -\    e_less(DD,ee,m,succ(n)) = ee`n O e_less(DD,ee,m,n)";
   12.77 +Goal "[| m le n;  n:nat |] ==>   \
   12.78 +\     e_less(DD,ee,m,succ(n)) = ee`n O e_less(DD,ee,m,n)";
   12.79  by (rtac le_exists 1);
   12.80  by (assume_tac 1);
   12.81  by (asm_simp_tac(simpset() addsimps[e_less_add]) 1);
   12.82 -by (REPEAT (assume_tac 1));
   12.83 +by (assume_tac 1);
   12.84  qed "e_less_le";
   12.85  
   12.86  (* All theorems assume variables m and n are natural numbers. *)
   12.87 @@ -1416,7 +1385,7 @@
   12.88  by (asm_simp_tac(simpset() addsimps[e_less_le, e_less_eq]) 1);
   12.89  qed "e_less_succ";
   12.90  
   12.91 -val prems = Goal  (* e_less_succ_emb *)
   12.92 +val prems = Goal
   12.93      "[|!!n. n:nat ==> emb(DD`n,DD`succ(n),ee`n); m:nat|] ==>   \
   12.94  \    e_less(DD,ee,m,succ(m)) = ee`m";
   12.95  by (asm_simp_tac(simpset() addsimps e_less_succ::prems) 1);
   12.96 @@ -1427,23 +1396,26 @@
   12.97  (* Compare this proof with the HOL one, here we do type checking. *)
   12.98  (* In any case the one below was very easy to write. *)
   12.99  
  12.100 -Goal "[|emb_chain(DD,ee); m:nat; k:nat|] ==>   \
  12.101 -\    emb(DD`m,DD`(m#+k),e_less(DD,ee,m,m#+k))";
  12.102 -by (induct_tac "k" 1);
  12.103 -by (asm_simp_tac(simpset() addsimps[e_less_eq]) 1);
  12.104 +Goal "[| emb_chain(DD,ee); m:nat |] ==>   \
  12.105 +\     emb(DD`m, DD`(m#+k), e_less(DD,ee,m,m#+k))";
  12.106 +by (subgoal_tac "emb(DD`m, DD`(m#+natify(k)), e_less(DD,ee,m,m#+natify(k)))" 1);
  12.107 +by (res_inst_tac [("n","natify(k)")] nat_induct 2);
  12.108 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps[e_less_eq])));
  12.109  brr[emb_id,emb_chain_cpo] 1;
  12.110  by (asm_simp_tac(simpset() addsimps[e_less_add]) 1);
  12.111  by (auto_tac (claset() addIs [emb_comp,emb_chain_emb,emb_chain_cpo,add_type],
  12.112  	      simpset()));
  12.113  qed "emb_e_less_add";
  12.114  
  12.115 -Goal "[|m le n; emb_chain(DD,ee); m:nat; n:nat|] ==>   \
  12.116 -\    emb(DD`m,DD`n,e_less(DD,ee,m,n))";
  12.117 +Goal "[| m le n;  emb_chain(DD,ee);  n:nat |] ==>   \
  12.118 +\    emb(DD`m, DD`n, e_less(DD,ee,m,n))";
  12.119 +by (ftac lt_nat_in_nat 1);
  12.120 +by (etac nat_succI 1);
  12.121  (* same proof as e_less_le *)
  12.122  by (rtac le_exists 1);
  12.123  by (assume_tac 1);
  12.124  by (asm_simp_tac(simpset() addsimps[emb_e_less_add]) 1);
  12.125 -by (REPEAT (assume_tac 1));
  12.126 +by (assume_tac 1);
  12.127  qed "emb_e_less";
  12.128  
  12.129  Goal "[|f=f'; g=g'|] ==> f O g = f' O g'";
  12.130 @@ -1752,20 +1724,17 @@
  12.131  
  12.132  (* Arithmetic, little support in Isabelle/ZF. *)
  12.133  
  12.134 -val prems = Goal  (* le_exists_lemma *)
  12.135 -    "[|n le k; k le m;  \
  12.136 -\      !!p q. [|p le q; k=n#+p; m=n#+q; p:nat; q:nat|] ==> R; \
  12.137 -\      m:nat; n:nat; k:nat|]==>R";
  12.138 -by (rtac (hd prems RS le_exists) 1);
  12.139 -by (rtac (le_exists) 1);
  12.140 -by (rtac le_trans 1);
  12.141 -(* Careful *)
  12.142 -by (resolve_tac prems 1);
  12.143 -by (resolve_tac prems 1);
  12.144 -by (resolve_tac prems 1);
  12.145 +val [prem1,prem2,prem3,prem4] = Goal
  12.146 +    "[| n le k; k le m;  \
  12.147 +\       !!p q. [|p le q; k=n#+p; m=n#+q; p:nat; q:nat|] ==> R; \
  12.148 +\       m:nat |]==>R";
  12.149 +by (rtac (prem1 RS le_exists) 1);
  12.150 +by (simp_tac (simpset() addsimps [prem2 RS lt_nat_in_nat, prem4]) 2);
  12.151 +by (rtac ([prem1,prem2] MRS le_trans RS le_exists) 1);
  12.152 +by (rtac prem3 1);
  12.153  by (assume_tac 2);
  12.154  by (assume_tac 2);
  12.155 -by (cut_facts_tac[hd prems,hd(tl prems)]1);
  12.156 +by (cut_facts_tac [prem1,prem2] 1);
  12.157  by (Asm_full_simp_tac 1);
  12.158  by (etac add_le_elim1 1);
  12.159  by (REPEAT (ares_tac prems 1));
    13.1 --- a/src/ZF/ex/ListN.ML	Tue Aug 01 13:43:22 2000 +0200
    13.2 +++ b/src/ZF/ex/ListN.ML	Tue Aug 01 15:28:21 2000 +0200
    13.3 @@ -35,7 +35,8 @@
    13.4  
    13.5  Goal "[| <n,l> : listn(A); <n',l'> : listn(A) |] ==> <n#+n', l@l'> : listn(A)";
    13.6  by (etac listn.induct 1);
    13.7 -by (ALLGOALS (asm_simp_tac (simpset() addsimps listn.intrs)));
    13.8 +by (ftac (impOfSubs listn.dom_subset) 1);
    13.9 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps listn.intrs)));
   13.10  qed "listn_append";
   13.11  
   13.12  val Nil_listn_case  = listn.mk_cases "<i,Nil> : listn(A)"
    14.1 --- a/src/ZF/ex/Primes.ML	Tue Aug 01 13:43:22 2000 +0200
    14.2 +++ b/src/ZF/ex/Primes.ML	Tue Aug 01 15:28:21 2000 +0200
    14.3 @@ -8,8 +8,6 @@
    14.4  
    14.5  eta_contract:=false;
    14.6  
    14.7 -open Primes;
    14.8 -
    14.9  (************************************************)
   14.10  (** Divides Relation                           **)
   14.11  (************************************************)
   14.12 @@ -125,10 +123,9 @@
   14.13  (* if f divides a and b then f divides egcd(a,b) *)
   14.14  
   14.15  Goalw [dvd_def] "[| f dvd a; f dvd b; 0<b |] ==> f dvd (a mod b)";
   14.16 -by (safe_tac (claset() addSIs [mult_type, mod_type]));
   14.17 +by (safe_tac (claset() addSIs [mod_type]));
   14.18  ren "m n" 1;
   14.19 -by (rtac (zero_lt_mult_iff RS iffD1 RS conjE) 1);
   14.20 -by (REPEAT_SOME assume_tac);
   14.21 +by (Asm_full_simp_tac 1);
   14.22  by (res_inst_tac 
   14.23      [("x", "(((m div n)#*n #+ m mod n) #- ((f#*m) div (f#*n)) #* n)")] 
   14.24      bexI 1);
    15.1 --- a/src/ZF/ex/Primrec.ML	Tue Aug 01 13:43:22 2000 +0200
    15.2 +++ b/src/ZF/ex/Primrec.ML	Tue Aug 01 15:28:21 2000 +0200
    15.3 @@ -137,7 +137,7 @@
    15.4  by (rtac (ack2_le_ack1 RSN (2,lt_trans2)) 1);
    15.5  by (Asm_simp_tac 1);
    15.6  by (rtac (add_le_self RS ack_le_mono1 RS lt_trans1) 1);
    15.7 -by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 5);
    15.8 +by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 4);
    15.9  by Auto_tac;
   15.10  qed "ack_nest_bound";
   15.11  
   15.12 @@ -265,7 +265,7 @@
   15.13  (*final part of the simplification*)
   15.14  by (Asm_simp_tac 1);
   15.15  by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1);
   15.16 -by (etac ack_lt_mono2 5);
   15.17 +by (etac ack_lt_mono2 4);
   15.18  by Auto_tac;
   15.19  qed "PREC_case_lemma";
   15.20