instantiated Cancel_Numerals for "nat" in ZF
authorpaulson
Mon Aug 07 10:29:54 2000 +0200 (2000-08-07)
changeset 954815bee2731e43
parent 9547 8dad21f06b24
child 9549 40d64cb4f4e6
instantiated Cancel_Numerals for "nat" in ZF
src/ZF/Arith.ML
src/ZF/ArithSimp.ML
src/ZF/ArithSimp.thy
src/ZF/CardinalArith.thy
src/ZF/Integ/Bin.ML
src/ZF/Integ/Bin.thy
src/ZF/Integ/Int.ML
src/ZF/Integ/Int.thy
src/ZF/IsaMakefile
src/ZF/List.ML
src/ZF/List.thy
src/ZF/ROOT.ML
src/ZF/arith_data.ML
src/ZF/ex/BinEx.ML
src/ZF/ex/Limit.ML
src/ZF/ex/Mutil.ML
src/ZF/ex/Primes.thy
     1.1 --- a/src/ZF/Arith.ML	Mon Aug 07 10:29:04 2000 +0200
     1.2 +++ b/src/ZF/Arith.ML	Mon Aug 07 10:29:54 2000 +0200
     1.3 @@ -39,7 +39,6 @@
     1.4  by (rtac (natify_def RS def_Vrecursor RS trans) 1);
     1.5  by Auto_tac;  
     1.6  qed "natify_succ";
     1.7 -Addsimps [natify_succ];
     1.8  
     1.9  Goal "natify(0) = 0";
    1.10  by (rtac (natify_def RS def_Vrecursor RS trans) 1);
    1.11 @@ -55,14 +54,14 @@
    1.12  Goal "natify(x) : nat";
    1.13  by (eps_ind_tac "x" 1);
    1.14  by (case_tac "EX z. x1 = succ(z)" 1);
    1.15 -by (auto_tac (claset(), simpset() addsimps [natify_non_succ]));  
    1.16 +by (auto_tac (claset(), simpset() addsimps [natify_succ, natify_non_succ]));  
    1.17  qed "natify_in_nat";
    1.18  AddIffs [natify_in_nat];
    1.19  AddTCs [natify_in_nat];
    1.20  
    1.21  Goal "n : nat ==> natify(n) = n";
    1.22  by (induct_tac "n" 1);
    1.23 -by Auto_tac;
    1.24 +by (auto_tac (claset(), simpset() addsimps [natify_succ]));  
    1.25  qed "natify_ident";
    1.26  Addsimps [natify_ident];
    1.27  
    1.28 @@ -180,7 +179,7 @@
    1.29  
    1.30  (*Must simplify BEFORE the induction: else we get a critical pair*)
    1.31  Goal "succ(m) #- succ(n) = m #- n";
    1.32 -by (simp_tac (simpset() addsimps [diff_def]) 1);
    1.33 +by (simp_tac (simpset() addsimps [natify_succ, diff_def]) 1);
    1.34  by (res_inst_tac [("x1","n")] (natify_in_nat RS nat_induct) 1);
    1.35  by Auto_tac;
    1.36  qed "diff_succ_succ";
    1.37 @@ -208,13 +207,17 @@
    1.38  (*Natify has weakened this law, compared with the older approach*)
    1.39  Goal "0 #+ m = natify(m)";
    1.40  by (asm_simp_tac (simpset() addsimps [add_def]) 1);
    1.41 -qed "add_0";
    1.42 +qed "add_0_natify";
    1.43  
    1.44  Goal "succ(m) #+ n = succ(m #+ n)";
    1.45 -by (asm_simp_tac (simpset() addsimps [add_def]) 1);
    1.46 +by (asm_simp_tac (simpset() addsimps [natify_succ, add_def]) 1);
    1.47  qed "add_succ";
    1.48  
    1.49 -Addsimps [add_0, add_succ];
    1.50 +Addsimps [add_0_natify, add_succ];
    1.51 +
    1.52 +Goal "m: nat ==> 0 #+ m = m";
    1.53 +by (Asm_simp_tac 1);
    1.54 +qed "add_0";
    1.55  
    1.56  (*Associative law for addition*)
    1.57  Goal "(m #+ n) #+ k = m #+ (n #+ k)";
    1.58 @@ -234,7 +237,7 @@
    1.59  
    1.60  Goalw [add_def] "m #+ succ(n) = succ(m #+ n)";
    1.61  by (res_inst_tac [("n","natify(m)")] nat_induct 1);
    1.62 -by Auto_tac;
    1.63 +by (auto_tac (claset(), simpset() addsimps [natify_succ]));  
    1.64  qed "add_succ_right";
    1.65  
    1.66  Addsimps [add_0_right_natify, add_succ_right];
    1.67 @@ -272,20 +275,150 @@
    1.68  by Auto_tac;
    1.69  qed "add_left_cancel_natify";
    1.70  
    1.71 -Goal "[| k #+ m = k #+ n;  m:nat;  n:nat |] ==> m = n";
    1.72 -by (dtac add_left_cancel_natify 1);
    1.73 -by Auto_tac;
    1.74 +Goal "[| i = j;  i #+ m = j #+ n;  m:nat;  n:nat |] ==> m = n";
    1.75 +by (force_tac (claset() addSDs [add_left_cancel_natify], simpset()) 1);
    1.76  qed "add_left_cancel";
    1.77  
    1.78 +(*Thanks to Sten Agerholm*)
    1.79 +Goal "k#+m le k#+n ==> natify(m) le natify(n)";
    1.80 +by (res_inst_tac [("P", "natify(k)#+m le natify(k)#+n")] rev_mp 1);
    1.81 +by (res_inst_tac [("n","natify(k)")] nat_induct 2);
    1.82 +by Auto_tac;
    1.83 +qed "add_le_elim1_natify";
    1.84  
    1.85 -(*** Multiplication ***)
    1.86 +Goal "[| k#+m le k#+n; m: nat; n: nat |] ==> m le n";
    1.87 +by (dtac add_le_elim1_natify 1);
    1.88 +by Auto_tac;
    1.89 +qed "add_le_elim1";
    1.90 +
    1.91 +Goal "k#+m < k#+n ==> natify(m) < natify(n)";
    1.92 +by (res_inst_tac [("P", "natify(k)#+m < natify(k)#+n")] rev_mp 1);
    1.93 +by (res_inst_tac [("n","natify(k)")] nat_induct 2);
    1.94 +by Auto_tac;
    1.95 +qed "add_lt_elim1_natify";
    1.96 +
    1.97 +Goal "[| k#+m < k#+n; m: nat; n: nat |] ==> m < n";
    1.98 +by (dtac add_lt_elim1_natify 1);
    1.99 +by Auto_tac;
   1.100 +qed "add_lt_elim1";
   1.101 +
   1.102 +
   1.103 +(*** Monotonicity of Addition ***)
   1.104 +
   1.105 +(*strict, in 1st argument; proof is by rule induction on 'less than'.
   1.106 +  Still need j:nat, for consider j = omega.  Then we can have i<omega,
   1.107 +  which is the same as i:nat, but natify(j)=0, so the conclusion fails.*)
   1.108 +Goal "[| i<j; j:nat |] ==> i#+k < j#+k";
   1.109 +by (ftac lt_nat_in_nat 1);
   1.110 +by (assume_tac 1);
   1.111 +by (etac succ_lt_induct 1);
   1.112 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI])));
   1.113 +qed "add_lt_mono1";
   1.114 +
   1.115 +(*strict, in both arguments*)
   1.116 +Goal "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
   1.117 +by (rtac (add_lt_mono1 RS lt_trans) 1);
   1.118 +by (REPEAT (assume_tac 1));
   1.119 +by (EVERY [stac add_commute 1,
   1.120 +           stac add_commute 1,
   1.121 +           rtac add_lt_mono1 1]);
   1.122 +by (REPEAT (assume_tac 1));
   1.123 +qed "add_lt_mono";
   1.124 +
   1.125 +(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
   1.126 +val lt_mono::ford::prems = Goal
   1.127 +     "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
   1.128 +\        !!i. i:k ==> Ord(f(i));                \
   1.129 +\        i le j;  j:k                           \
   1.130 +\     |] ==> f(i) le f(j)";
   1.131 +by (cut_facts_tac prems 1);
   1.132 +by (blast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
   1.133 +qed "Ord_lt_mono_imp_le_mono";
   1.134 +
   1.135 +(*le monotonicity, 1st argument*)
   1.136 +Goal "[| i le j; j:nat |] ==> i#+k le j#+k";
   1.137 +by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1);
   1.138 +by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1));
   1.139 +qed "add_le_mono1";
   1.140 +
   1.141 +(* le monotonicity, BOTH arguments*)
   1.142 +Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
   1.143 +by (rtac (add_le_mono1 RS le_trans) 1);
   1.144 +by (REPEAT (assume_tac 1));
   1.145 +by (EVERY [stac add_commute 1,
   1.146 +           stac add_commute 1,
   1.147 +           rtac add_le_mono1 1]);
   1.148 +by (REPEAT (assume_tac 1));
   1.149 +qed "add_le_mono";
   1.150 +
   1.151 +(** Subtraction is the inverse of addition. **)
   1.152 +
   1.153 +Goal "(n#+m) #- n = natify(m)";
   1.154 +by (subgoal_tac "(natify(n) #+ m) #- natify(n) = natify(m)" 1);
   1.155 +by (res_inst_tac [("n","natify(n)")] nat_induct 2);
   1.156 +by Auto_tac;
   1.157 +qed "diff_add_inverse";
   1.158 +
   1.159 +Goal "(m#+n) #- n = natify(m)";
   1.160 +by (simp_tac (simpset() addsimps [inst "m" "m" add_commute, 
   1.161 +				  diff_add_inverse]) 1);
   1.162 +qed "diff_add_inverse2";
   1.163 +
   1.164 +Goal "(k#+m) #- (k#+n) = m #- n";
   1.165 +by (subgoal_tac "(natify(k) #+ natify(m)) #- (natify(k) #+ natify(n)) = \
   1.166 +\                natify(m) #- natify(n)" 1);
   1.167 +by (res_inst_tac [("n","natify(k)")] nat_induct 2);
   1.168 +by Auto_tac;
   1.169 +qed "diff_cancel";
   1.170 +
   1.171 +Goal "(m#+k) #- (n#+k) = m #- n";
   1.172 +by (simp_tac (simpset() addsimps [inst "n" "k" add_commute, diff_cancel]) 1);
   1.173 +qed "diff_cancel2";
   1.174 +
   1.175 +Goal "n #- (n#+m) = 0";
   1.176 +by (subgoal_tac "natify(n) #- (natify(n) #+ natify(m)) = 0" 1);
   1.177 +by (res_inst_tac [("n","natify(n)")] nat_induct 2);
   1.178 +by Auto_tac;
   1.179 +qed "diff_add_0";
   1.180 +
   1.181 +
   1.182 +(** Lemmas for the CancelNumerals simproc **)
   1.183 +
   1.184 +Goal "(u #+ m = u #+ n) <-> (0 #+ m = natify(n))";
   1.185 +by Auto_tac;  
   1.186 +by (blast_tac (claset() addDs [add_left_cancel_natify]) 1);
   1.187 +by (asm_full_simp_tac (simpset() addsimps [add_def]) 1);
   1.188 +qed "eq_add_iff";
   1.189 +
   1.190 +Goal "(u #+ m < u #+ n) <-> (0 #+ m < natify(n))";
   1.191 +by (auto_tac (claset(), simpset() addsimps [add_lt_elim1_natify]));
   1.192 +by (dtac add_lt_mono1 1);
   1.193 +by (auto_tac (claset(), simpset() addsimps [inst "m" "u" add_commute]));
   1.194 +qed "less_add_iff";
   1.195 +
   1.196 +Goal "((u #+ m) #- (u #+ n)) = ((0 #+ m) #- n)";
   1.197 +by (asm_simp_tac (simpset() addsimps [diff_cancel]) 1);
   1.198 +qed "diff_add_eq";
   1.199 +
   1.200 +(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
   1.201 +Goal "u = u' ==> (t==u) == (t==u')";
   1.202 +by Auto_tac;
   1.203 +qed "eq_cong2";
   1.204 +
   1.205 +Goal "u <-> u' ==> (t==u) == (t==u')";
   1.206 +by Auto_tac;
   1.207 +qed "iff_cong2";
   1.208 +
   1.209 +
   1.210 +(*** Multiplication [the simprocs need these laws] ***)
   1.211  
   1.212  Goal "0 #* m = 0";
   1.213  by (simp_tac (simpset() addsimps [mult_def]) 1);
   1.214  qed "mult_0";
   1.215  
   1.216  Goal "succ(m) #* n = n #+ (m #* n)";
   1.217 -by (simp_tac (simpset() addsimps [add_def, mult_def, raw_mult_type]) 1);
   1.218 +by (simp_tac (simpset() addsimps [add_def, mult_def, natify_succ, 
   1.219 +                                  raw_mult_type]) 1);
   1.220  qed "mult_succ";
   1.221  
   1.222  Addsimps [mult_0, mult_succ];
   1.223 @@ -300,7 +433,7 @@
   1.224  Goal "m #* succ(n) = m #+ (m #* n)";
   1.225  by (subgoal_tac "natify(m) #* succ(natify(n)) = \
   1.226  \                natify(m) #+ (natify(m) #* natify(n))" 1);
   1.227 -by (full_simp_tac (simpset() addsimps [add_def, mult_def]) 1);
   1.228 +by (full_simp_tac (simpset() addsimps [natify_succ, add_def, mult_def]) 1);
   1.229  by (res_inst_tac [("n","natify(m)")] nat_induct 1);
   1.230  by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
   1.231  qed "mult_succ_right";
   1.232 @@ -366,474 +499,3 @@
   1.233  val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
   1.234  
   1.235  
   1.236 -(*** Difference ***)
   1.237 -
   1.238 -Goal "m #- m = 0";
   1.239 -by (subgoal_tac "natify(m) #- natify(m) = 0" 1);
   1.240 -by (rtac (natify_in_nat RS nat_induct) 2);
   1.241 -by Auto_tac;
   1.242 -qed "diff_self_eq_0";
   1.243 -
   1.244 -(**Addition is the inverse of subtraction**)
   1.245 -
   1.246 -(*We need m:nat even if we replace the RHS by natify(m), for consider e.g.
   1.247 -  n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 ~= 0 = natify(m).*)
   1.248 -Goal "[| n le m;  m:nat |] ==> n #+ (m#-n) = m";
   1.249 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   1.250 -by (etac rev_mp 1);
   1.251 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.252 -by Auto_tac;
   1.253 -qed "add_diff_inverse";
   1.254 -
   1.255 -Goal "[| n le m;  m:nat |] ==> (m#-n) #+ n = m";
   1.256 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   1.257 -by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1);
   1.258 -qed "add_diff_inverse2";
   1.259 -
   1.260 -(*Proof is IDENTICAL to that of add_diff_inverse*)
   1.261 -Goal "[| n le m;  m:nat |] ==> succ(m) #- n = succ(m#-n)";
   1.262 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   1.263 -by (etac rev_mp 1);
   1.264 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.265 -by (ALLGOALS Asm_simp_tac);
   1.266 -qed "diff_succ";
   1.267 -
   1.268 -Goal "[| m: nat; n: nat |] ==> 0 < (n #- m)   <->   m<n";
   1.269 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.270 -by (ALLGOALS Asm_simp_tac);
   1.271 -qed "zero_less_diff";
   1.272 -Addsimps [zero_less_diff];
   1.273 -
   1.274 -
   1.275 -(** Subtraction is the inverse of addition. **)
   1.276 -
   1.277 -Goal "(n#+m) #- n = natify(m)";
   1.278 -by (subgoal_tac "(natify(n) #+ m) #- natify(n) = natify(m)" 1);
   1.279 -by (res_inst_tac [("n","natify(n)")] nat_induct 2);
   1.280 -by Auto_tac;
   1.281 -qed "diff_add_inverse";
   1.282 -
   1.283 -Goal "(m#+n) #- n = natify(m)";
   1.284 -by (simp_tac (simpset() addsimps [inst "m" "m" add_commute, 
   1.285 -				  diff_add_inverse]) 1);
   1.286 -qed "diff_add_inverse2";
   1.287 -
   1.288 -Goal "(k#+m) #- (k#+n) = m #- n";
   1.289 -by (subgoal_tac "(natify(k) #+ natify(m)) #- (natify(k) #+ natify(n)) = \
   1.290 -\                natify(m) #- natify(n)" 1);
   1.291 -by (res_inst_tac [("n","natify(k)")] nat_induct 2);
   1.292 -by Auto_tac;
   1.293 -qed "diff_cancel";
   1.294 -
   1.295 -Goal "(m#+k) #- (n#+k) = m #- n";
   1.296 -by (simp_tac (simpset() addsimps [inst "n" "k" add_commute, diff_cancel]) 1);
   1.297 -qed "diff_cancel2";
   1.298 -
   1.299 -Goal "n #- (n#+m) = 0";
   1.300 -by (subgoal_tac "natify(n) #- (natify(n) #+ natify(m)) = 0" 1);
   1.301 -by (res_inst_tac [("n","natify(n)")] nat_induct 2);
   1.302 -by Auto_tac;
   1.303 -qed "diff_add_0";
   1.304 -
   1.305 -(** Difference distributes over multiplication **)
   1.306 -
   1.307 -Goal "(m #- n) #* k = (m #* k) #- (n #* k)";
   1.308 -by (subgoal_tac "(natify(m) #- natify(n)) #* natify(k) = \
   1.309 -\                (natify(m) #* natify(k)) #- (natify(n) #* natify(k))" 1);
   1.310 -by (res_inst_tac [("m","natify(m)"),("n","natify(n)")] diff_induct 2);
   1.311 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [diff_cancel])));
   1.312 -qed "diff_mult_distrib" ;
   1.313 -
   1.314 -Goal "k #* (m #- n) = (k #* m) #- (k #* n)";
   1.315 -by (simp_tac
   1.316 -    (simpset() addsimps [inst "m" "k" mult_commute, diff_mult_distrib]) 1);
   1.317 -qed "diff_mult_distrib2";
   1.318 -
   1.319 -
   1.320 -(*** Remainder ***)
   1.321 -
   1.322 -(*We need m:nat even with natify*)
   1.323 -Goal "[| 0<n;  n le m;  m:nat |] ==> m #- n < m";
   1.324 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   1.325 -by (etac rev_mp 1);
   1.326 -by (etac rev_mp 1);
   1.327 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.328 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self])));
   1.329 -qed "div_termination";
   1.330 -
   1.331 -val div_rls =   (*for mod and div*)
   1.332 -    nat_typechecks @
   1.333 -    [Ord_transrec_type, apply_funtype, div_termination RS ltD,
   1.334 -     nat_into_Ord, not_lt_iff_le RS iffD1];
   1.335 -
   1.336 -val div_ss = simpset() addsimps [div_termination RS ltD,
   1.337 -				 not_lt_iff_le RS iffD2];
   1.338 -
   1.339 -Goalw [raw_mod_def] "[| m:nat;  n:nat |] ==> raw_mod (m, n) : nat";
   1.340 -by (rtac Ord_transrec_type 1);
   1.341 -by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]));
   1.342 -by (REPEAT (ares_tac div_rls 1));
   1.343 -qed "raw_mod_type";
   1.344 -
   1.345 -Goalw [mod_def] "m mod n : nat";
   1.346 -by (simp_tac (simpset() addsimps [mod_def, raw_mod_type]) 1);
   1.347 -qed "mod_type";
   1.348 -AddTCs [mod_type];
   1.349 -AddIffs [mod_type];
   1.350 -
   1.351 -
   1.352 -(** Aribtrary definitions for division by zero.  Useful to simplify 
   1.353 -    certain equations **)
   1.354 -
   1.355 -Goalw [div_def] "a div 0 = 0";
   1.356 -by (rtac (raw_div_def RS def_transrec RS trans) 1);
   1.357 -by (Asm_simp_tac 1);
   1.358 -qed "DIVISION_BY_ZERO_DIV";  (*NOT for adding to default simpset*)
   1.359 -
   1.360 -Goalw [mod_def] "a mod 0 = natify(a)";
   1.361 -by (rtac (raw_mod_def RS def_transrec RS trans) 1);
   1.362 -by (Asm_simp_tac 1);
   1.363 -qed "DIVISION_BY_ZERO_MOD";  (*NOT for adding to default simpset*)
   1.364 -
   1.365 -fun div_undefined_case_tac s i =
   1.366 -  case_tac s i THEN 
   1.367 -  asm_full_simp_tac
   1.368 -         (simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]) (i+1) THEN
   1.369 -  asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV, 
   1.370 -				    DIVISION_BY_ZERO_MOD]) i;
   1.371 -
   1.372 -Goal "m<n ==> raw_mod (m,n) = m";
   1.373 -by (rtac (raw_mod_def RS def_transrec RS trans) 1);
   1.374 -by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1);
   1.375 -qed "raw_mod_less";
   1.376 -
   1.377 -Goal "[| m<n; n : nat |] ==> m mod n = m";
   1.378 -by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
   1.379 -by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_less]) 1);
   1.380 -qed "mod_less";
   1.381 -
   1.382 -Goal "[| 0<n; n le m;  m:nat |] ==> raw_mod (m, n) = raw_mod (m#-n, n)";
   1.383 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   1.384 -by (rtac (raw_mod_def RS def_transrec RS trans) 1);
   1.385 -by (asm_simp_tac div_ss 1);
   1.386 -by (Blast_tac 1);
   1.387 -qed "raw_mod_geq";
   1.388 -
   1.389 -Goal "[| n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
   1.390 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   1.391 -by (div_undefined_case_tac "n=0" 1);
   1.392 -by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_geq]) 1);
   1.393 -qed "mod_geq";
   1.394 -
   1.395 -Addsimps [mod_less];
   1.396 -
   1.397 -
   1.398 -(*** Division ***)
   1.399 -
   1.400 -Goalw [raw_div_def] "[| m:nat;  n:nat |] ==> raw_div (m, n) : nat";
   1.401 -by (rtac Ord_transrec_type 1);
   1.402 -by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]));
   1.403 -by (REPEAT (ares_tac div_rls 1));
   1.404 -qed "raw_div_type";
   1.405 -
   1.406 -Goalw [div_def] "m div n : nat";
   1.407 -by (simp_tac (simpset() addsimps [div_def, raw_div_type]) 1);
   1.408 -qed "div_type";
   1.409 -AddTCs [div_type];
   1.410 -AddIffs [div_type];
   1.411 -
   1.412 -Goal "m<n ==> raw_div (m,n) = 0";
   1.413 -by (rtac (raw_div_def RS def_transrec RS trans) 1);
   1.414 -by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1);
   1.415 -qed "raw_div_less";
   1.416 -
   1.417 -Goal "[| m<n; n : nat |] ==> m div n = 0";
   1.418 -by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
   1.419 -by (asm_simp_tac (simpset() addsimps [div_def, raw_div_less]) 1);
   1.420 -qed "div_less";
   1.421 -
   1.422 -Goal "[| 0<n;  n le m;  m:nat |] ==> raw_div(m,n) = succ(raw_div(m#-n, n))";
   1.423 -by (subgoal_tac "n ~= 0" 1);
   1.424 -by (Blast_tac 2);
   1.425 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   1.426 -by (rtac (raw_div_def RS def_transrec RS trans) 1);
   1.427 -by (asm_simp_tac div_ss 1);
   1.428 -qed "raw_div_geq";
   1.429 -
   1.430 -Goal "[| 0<n;  n le m;  m:nat |] ==> m div n = succ ((m#-n) div n)";
   1.431 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   1.432 -by (asm_simp_tac (simpset() addsimps [div_def, raw_div_geq]) 1);
   1.433 -qed "div_geq";
   1.434 -
   1.435 -Addsimps [div_less, div_geq];
   1.436 -
   1.437 -
   1.438 -(*A key result*)
   1.439 -Goal "[| m: nat;  n: nat |] ==> (m div n)#*n #+ m mod n = m";
   1.440 -by (div_undefined_case_tac "n=0" 1);
   1.441 -by (etac complete_induct 1);
   1.442 -by (case_tac "x<n" 1);
   1.443 -(*case n le x*)
   1.444 -by (asm_full_simp_tac
   1.445 -     (simpset() addsimps [not_lt_iff_le, add_assoc, mod_geq,
   1.446 -                         div_termination RS ltD, add_diff_inverse]) 2);
   1.447 -(*case x<n*)
   1.448 -by (Asm_simp_tac 1);
   1.449 -val lemma = result();
   1.450 -
   1.451 -Goal "(m div n)#*n #+ m mod n = natify(m)";
   1.452 -by (subgoal_tac
   1.453 -    "(natify(m) div natify(n))#*natify(n) #+ natify(m) mod natify(n) = \
   1.454 -\    natify(m)" 1);
   1.455 -by (stac lemma 2);
   1.456 -by Auto_tac;
   1.457 -qed "mod_div_equality_natify";
   1.458 -
   1.459 -Goal "m: nat ==> (m div n)#*n #+ m mod n = m";
   1.460 -by (asm_simp_tac (simpset() addsimps [mod_div_equality_natify]) 1);
   1.461 -qed "mod_div_equality";
   1.462 -
   1.463 -
   1.464 -(*** Further facts about mod (mainly for mutilated chess board) ***)
   1.465 -
   1.466 -Goal "[| 0<n;  m:nat;  n:nat |] \
   1.467 -\     ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
   1.468 -by (etac complete_induct 1);
   1.469 -by (excluded_middle_tac "succ(x)<n" 1);
   1.470 -(* case succ(x) < n *)
   1.471 -by (asm_simp_tac (simpset() addsimps [nat_le_refl RS lt_trans, 
   1.472 -				      succ_neq_self]) 2);
   1.473 -by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2);
   1.474 -(* case n le succ(x) *)
   1.475 -by (asm_full_simp_tac (simpset() addsimps [mod_geq, not_lt_iff_le]) 1);
   1.476 -by (etac leE 1);
   1.477 -(*equality case*)
   1.478 -by (asm_full_simp_tac (simpset() addsimps [diff_self_eq_0]) 2);
   1.479 -by (asm_simp_tac (simpset() addsimps [mod_geq, div_termination RS ltD, 
   1.480 -				      diff_succ]) 1);
   1.481 -val lemma = result();
   1.482 -
   1.483 -Goal "n:nat ==> \
   1.484 -\     succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
   1.485 -by (case_tac "n=0" 1);
   1.486 -by (asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_MOD]) 1);
   1.487 -by (subgoal_tac
   1.488 -    "natify(succ(m)) mod n = \
   1.489 -\      (if succ(natify(m) mod n) = n then 0 else succ(natify(m) mod n))" 1);
   1.490 -by (stac natify_succ 2);
   1.491 -by (rtac lemma 2);
   1.492 -by (auto_tac(claset(), 
   1.493 -	     simpset() delsimps [natify_succ] 
   1.494 -             addsimps [nat_into_Ord RS Ord_0_lt_iff]));
   1.495 -qed "mod_succ";
   1.496 -
   1.497 -Goal "[| 0<n;  n:nat |] ==> m mod n < n";
   1.498 -by (subgoal_tac "natify(m) mod n < n" 1);
   1.499 -by (res_inst_tac [("i","natify(m)")] complete_induct 2);
   1.500 -by (case_tac "x<n" 3);
   1.501 -(*case x<n*)
   1.502 -by (Asm_simp_tac 3);
   1.503 -(*case n le x*)
   1.504 -by (asm_full_simp_tac
   1.505 -     (simpset() addsimps [mod_geq, not_lt_iff_le, div_termination RS ltD]) 3);
   1.506 -by Auto_tac;
   1.507 -qed "mod_less_divisor";
   1.508 -
   1.509 -Goal "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
   1.510 -by (subgoal_tac "k mod 2: 2" 1);
   1.511 -by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
   1.512 -by (dtac ltD 1);
   1.513 -by Auto_tac;
   1.514 -qed "mod2_cases";
   1.515 -
   1.516 -Goal "succ(succ(m)) mod 2 = m mod 2";
   1.517 -by (subgoal_tac "m mod 2: 2" 1);
   1.518 -by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
   1.519 -by (auto_tac (claset(), simpset() addsimps [mod_succ]));  
   1.520 -qed "mod2_succ_succ";
   1.521 -
   1.522 -Addsimps [mod2_succ_succ];
   1.523 -
   1.524 -Goal "(m#+m) mod 2 = 0";
   1.525 -by (subgoal_tac "(natify(m)#+natify(m)) mod 2 = 0" 1);
   1.526 -by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   1.527 -by Auto_tac;
   1.528 -qed "mod2_add_self";
   1.529 -
   1.530 -Addsimps [mod2_add_self];
   1.531 -
   1.532 -
   1.533 -(**** Additional theorems about "le" ****)
   1.534 -
   1.535 -Goal "m:nat ==> m le (m #+ n)";
   1.536 -by (induct_tac "m" 1);
   1.537 -by (ALLGOALS Asm_simp_tac);
   1.538 -qed "add_le_self";
   1.539 -
   1.540 -Goal "m:nat ==> m le (n #+ m)";
   1.541 -by (stac add_commute 1);
   1.542 -by (etac add_le_self 1);
   1.543 -qed "add_le_self2";
   1.544 -
   1.545 -(*** Monotonicity of Addition ***)
   1.546 -
   1.547 -(*strict, in 1st argument; proof is by rule induction on 'less than'.
   1.548 -  Still need j:nat, for consider j = omega.  Then we can have i<omega,
   1.549 -  which is the same as i:nat, but natify(j)=0, so the conclusion fails.*)
   1.550 -Goal "[| i<j; j:nat |] ==> i#+k < j#+k";
   1.551 -by (ftac lt_nat_in_nat 1);
   1.552 -by (assume_tac 1);
   1.553 -by (etac succ_lt_induct 1);
   1.554 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI])));
   1.555 -qed "add_lt_mono1";
   1.556 -
   1.557 -(*strict, in both arguments*)
   1.558 -Goal "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
   1.559 -by (rtac (add_lt_mono1 RS lt_trans) 1);
   1.560 -by (REPEAT (assume_tac 1));
   1.561 -by (EVERY [stac add_commute 1,
   1.562 -           stac add_commute 1,
   1.563 -           rtac add_lt_mono1 1]);
   1.564 -by (REPEAT (assume_tac 1));
   1.565 -qed "add_lt_mono";
   1.566 -
   1.567 -(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
   1.568 -val lt_mono::ford::prems = Goal
   1.569 -     "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
   1.570 -\        !!i. i:k ==> Ord(f(i));                \
   1.571 -\        i le j;  j:k                           \
   1.572 -\     |] ==> f(i) le f(j)";
   1.573 -by (cut_facts_tac prems 1);
   1.574 -by (blast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
   1.575 -qed "Ord_lt_mono_imp_le_mono";
   1.576 -
   1.577 -(*le monotonicity, 1st argument*)
   1.578 -Goal "[| i le j; j:nat |] ==> i#+k le j#+k";
   1.579 -by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1);
   1.580 -by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1));
   1.581 -qed "add_le_mono1";
   1.582 -
   1.583 -(* le monotonicity, BOTH arguments*)
   1.584 -Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
   1.585 -by (rtac (add_le_mono1 RS le_trans) 1);
   1.586 -by (REPEAT (assume_tac 1));
   1.587 -by (EVERY [stac add_commute 1,
   1.588 -           stac add_commute 1,
   1.589 -           rtac add_le_mono1 1]);
   1.590 -by (REPEAT (assume_tac 1));
   1.591 -qed "add_le_mono";
   1.592 -
   1.593 -(*** Monotonicity of Multiplication ***)
   1.594 -
   1.595 -Goal "[| i le j; j:nat |] ==> (i#*k) le (j#*k)";
   1.596 -by (subgoal_tac "natify(i)#*natify(k) le j#*natify(k)" 1);
   1.597 -by (ftac lt_nat_in_nat 2);
   1.598 -by (res_inst_tac [("n","natify(k)")] nat_induct 3);
   1.599 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_le_mono])));
   1.600 -qed "mult_le_mono1";
   1.601 -
   1.602 -(* le monotonicity, BOTH arguments*)
   1.603 -Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l";
   1.604 -by (rtac (mult_le_mono1 RS le_trans) 1);
   1.605 -by (REPEAT (assume_tac 1));
   1.606 -by (EVERY [stac mult_commute 1,
   1.607 -           stac mult_commute 1,
   1.608 -           rtac mult_le_mono1 1]);
   1.609 -by (REPEAT (assume_tac 1));
   1.610 -qed "mult_le_mono";
   1.611 -
   1.612 -(*strict, in 1st argument; proof is by induction on k>0.
   1.613 -  I can't see how to relax the typing conditions.*)
   1.614 -Goal "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
   1.615 -by (etac zero_lt_natE 1);
   1.616 -by (ftac lt_nat_in_nat 2);
   1.617 -by (ALLGOALS Asm_simp_tac);
   1.618 -by (induct_tac "x" 1);
   1.619 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
   1.620 -qed "mult_lt_mono2";
   1.621 -
   1.622 -Goal "[| i<j; 0<k; j:nat; k:nat |] ==> i#*k < j#*k";
   1.623 -by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, 
   1.624 -				      inst "n" "k" mult_commute]) 1);
   1.625 -qed "mult_lt_mono1";
   1.626 -
   1.627 -Goal "m#+n = 0 <-> natify(m)=0 & natify(n)=0";
   1.628 -by (subgoal_tac "natify(m) #+ natify(n) = 0 <-> natify(m)=0 & natify(n)=0" 1);
   1.629 -by (res_inst_tac [("n","natify(m)")] natE 2);
   1.630 - by (res_inst_tac [("n","natify(n)")] natE 4);
   1.631 -by Auto_tac;  
   1.632 -qed "add_eq_0_iff";
   1.633 -AddIffs [add_eq_0_iff];
   1.634 -
   1.635 -Goal "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)";
   1.636 -by (subgoal_tac "0 < natify(m)#*natify(n) <-> \
   1.637 -\                0 < natify(m) & 0 < natify(n)" 1);
   1.638 -by (res_inst_tac [("n","natify(m)")] natE 2);
   1.639 - by (res_inst_tac [("n","natify(n)")] natE 4);
   1.640 -  by (res_inst_tac [("n","natify(n)")] natE 3);
   1.641 -by Auto_tac;  
   1.642 -qed "zero_lt_mult_iff";
   1.643 -
   1.644 -Goal "m#*n = 1 <-> natify(m)=1 & natify(n)=1";
   1.645 -by (subgoal_tac "natify(m) #* natify(n) = 1 <-> natify(m)=1 & natify(n)=1" 1);
   1.646 -by (res_inst_tac [("n","natify(m)")] natE 2);
   1.647 - by (res_inst_tac [("n","natify(n)")] natE 4);
   1.648 -by Auto_tac;  
   1.649 -qed "mult_eq_1_iff";
   1.650 -AddIffs [zero_lt_mult_iff, mult_eq_1_iff];
   1.651 -
   1.652 -(*Cancellation law for division*)
   1.653 -Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n";
   1.654 -by (eres_inst_tac [("i","m")] complete_induct 1);
   1.655 -by (excluded_middle_tac "x<n" 1);
   1.656 -by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff, 
   1.657 -                                     mult_lt_mono2]) 2);
   1.658 -by (asm_full_simp_tac
   1.659 -     (simpset() addsimps [not_lt_iff_le, 
   1.660 -                         zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq,
   1.661 -                         diff_mult_distrib2 RS sym,
   1.662 -                         div_termination RS ltD]) 1);
   1.663 -qed "div_cancel";
   1.664 -
   1.665 -Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> \
   1.666 -\        (k#*m) mod (k#*n) = k #* (m mod n)";
   1.667 -by (eres_inst_tac [("i","m")] complete_induct 1);
   1.668 -by (excluded_middle_tac "x<n" 1);
   1.669 -by (asm_simp_tac (simpset() addsimps [mod_less, zero_lt_mult_iff, 
   1.670 -                                     mult_lt_mono2]) 2);
   1.671 -by (asm_full_simp_tac
   1.672 -     (simpset() addsimps [not_lt_iff_le, 
   1.673 -                         zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq,
   1.674 -                         diff_mult_distrib2 RS sym,
   1.675 -                         div_termination RS ltD]) 1);
   1.676 -qed "mult_mod_distrib";
   1.677 -
   1.678 -(*Lemma for gcd*)
   1.679 -Goal "m = m#*n ==> natify(n)=1 | m=0";
   1.680 -by (subgoal_tac "m: nat" 1);
   1.681 -by (etac ssubst 2);
   1.682 -by (rtac disjCI 1);
   1.683 -by (dtac sym 1);
   1.684 -by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
   1.685 -by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 3);
   1.686 -by Auto_tac;
   1.687 -by (subgoal_tac "m #* n = 0" 1);
   1.688 -by (stac (mult_natify2 RS sym) 2);
   1.689 -by (auto_tac (claset(), simpset() delsimps [mult_natify2]));  
   1.690 -qed "mult_eq_self_implies_10";
   1.691 -
   1.692 -(*Thanks to Sten Agerholm*)
   1.693 -Goal "[| k#+m le k#+n; m: nat; n: nat |] ==> m le n";
   1.694 -by (res_inst_tac [("P", "natify(k)#+m le natify(k)#+n")] rev_mp 1);
   1.695 -by (res_inst_tac [("n","natify(k)")] nat_induct 2);
   1.696 -by Auto_tac;
   1.697 -qed "add_le_elim1";
   1.698 -
   1.699 -Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
   1.700 -by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
   1.701 -by (etac rev_mp 1);
   1.702 -by (induct_tac "n" 1);
   1.703 -by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
   1.704 -by (blast_tac (claset() addSEs [leE] 
   1.705 -                        addSIs [add_0_right RS sym, add_succ_right RS sym]) 1);
   1.706 -qed_spec_mp "less_imp_Suc_add";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/ZF/ArithSimp.ML	Mon Aug 07 10:29:54 2000 +0200
     2.3 @@ -0,0 +1,406 @@
     2.4 +(*  Title:      ZF/ArithSimp.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   2000  University of Cambridge
     2.8 +
     2.9 +Arithmetic with simplification
    2.10 +*)
    2.11 +
    2.12 +
    2.13 +Addsimprocs ArithData.nat_cancel;
    2.14 +
    2.15 +
    2.16 +(*** Difference ***)
    2.17 +
    2.18 +Goal "m #- m = 0";
    2.19 +by (subgoal_tac "natify(m) #- natify(m) = 0" 1);
    2.20 +by (rtac (natify_in_nat RS nat_induct) 2);
    2.21 +by Auto_tac;
    2.22 +qed "diff_self_eq_0";
    2.23 +
    2.24 +(**Addition is the inverse of subtraction**)
    2.25 +
    2.26 +(*We need m:nat even if we replace the RHS by natify(m), for consider e.g.
    2.27 +  n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 ~= 0 = natify(m).*)
    2.28 +Goal "[| n le m;  m:nat |] ==> n #+ (m#-n) = m";
    2.29 +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
    2.30 +by (etac rev_mp 1);
    2.31 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    2.32 +by Auto_tac;
    2.33 +qed "add_diff_inverse";
    2.34 +
    2.35 +Goal "[| n le m;  m:nat |] ==> (m#-n) #+ n = m";
    2.36 +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
    2.37 +by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1);
    2.38 +qed "add_diff_inverse2";
    2.39 +
    2.40 +(*Proof is IDENTICAL to that of add_diff_inverse*)
    2.41 +Goal "[| n le m;  m:nat |] ==> succ(m) #- n = succ(m#-n)";
    2.42 +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
    2.43 +by (etac rev_mp 1);
    2.44 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    2.45 +by (ALLGOALS Asm_simp_tac);
    2.46 +qed "diff_succ";
    2.47 +
    2.48 +Goal "[| m: nat; n: nat |] ==> 0 < (n #- m)   <->   m<n";
    2.49 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    2.50 +by (ALLGOALS Asm_simp_tac);
    2.51 +qed "zero_less_diff";
    2.52 +Addsimps [zero_less_diff];
    2.53 +
    2.54 +
    2.55 +(** Difference distributes over multiplication **)
    2.56 +
    2.57 +Goal "(m #- n) #* k = (m #* k) #- (n #* k)";
    2.58 +by (subgoal_tac "(natify(m) #- natify(n)) #* natify(k) = \
    2.59 +\                (natify(m) #* natify(k)) #- (natify(n) #* natify(k))" 1);
    2.60 +by (res_inst_tac [("m","natify(m)"),("n","natify(n)")] diff_induct 2);
    2.61 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [diff_cancel])));
    2.62 +qed "diff_mult_distrib" ;
    2.63 +
    2.64 +Goal "k #* (m #- n) = (k #* m) #- (k #* n)";
    2.65 +by (simp_tac
    2.66 +    (simpset() addsimps [inst "m" "k" mult_commute, diff_mult_distrib]) 1);
    2.67 +qed "diff_mult_distrib2";
    2.68 +
    2.69 +
    2.70 +(*** Remainder ***)
    2.71 +
    2.72 +(*We need m:nat even with natify*)
    2.73 +Goal "[| 0<n;  n le m;  m:nat |] ==> m #- n < m";
    2.74 +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
    2.75 +by (etac rev_mp 1);
    2.76 +by (etac rev_mp 1);
    2.77 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    2.78 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self])));
    2.79 +qed "div_termination";
    2.80 +
    2.81 +val div_rls =   (*for mod and div*)
    2.82 +    nat_typechecks @
    2.83 +    [Ord_transrec_type, apply_funtype, div_termination RS ltD,
    2.84 +     nat_into_Ord, not_lt_iff_le RS iffD1];
    2.85 +
    2.86 +val div_ss = simpset() addsimps [div_termination RS ltD,
    2.87 +				 not_lt_iff_le RS iffD2];
    2.88 +
    2.89 +Goalw [raw_mod_def] "[| m:nat;  n:nat |] ==> raw_mod (m, n) : nat";
    2.90 +by (rtac Ord_transrec_type 1);
    2.91 +by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]));
    2.92 +by (REPEAT (ares_tac div_rls 1));
    2.93 +qed "raw_mod_type";
    2.94 +
    2.95 +Goalw [mod_def] "m mod n : nat";
    2.96 +by (simp_tac (simpset() addsimps [mod_def, raw_mod_type]) 1);
    2.97 +qed "mod_type";
    2.98 +AddTCs [mod_type];
    2.99 +AddIffs [mod_type];
   2.100 +
   2.101 +
   2.102 +(** Aribtrary definitions for division by zero.  Useful to simplify 
   2.103 +    certain equations **)
   2.104 +
   2.105 +Goalw [div_def] "a div 0 = 0";
   2.106 +by (rtac (raw_div_def RS def_transrec RS trans) 1);
   2.107 +by (Asm_simp_tac 1);
   2.108 +qed "DIVISION_BY_ZERO_DIV";  (*NOT for adding to default simpset*)
   2.109 +
   2.110 +Goalw [mod_def] "a mod 0 = natify(a)";
   2.111 +by (rtac (raw_mod_def RS def_transrec RS trans) 1);
   2.112 +by (Asm_simp_tac 1);
   2.113 +qed "DIVISION_BY_ZERO_MOD";  (*NOT for adding to default simpset*)
   2.114 +
   2.115 +fun div_undefined_case_tac s i =
   2.116 +  case_tac s i THEN 
   2.117 +  asm_full_simp_tac
   2.118 +         (simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]) (i+1) THEN
   2.119 +  asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV, 
   2.120 +				    DIVISION_BY_ZERO_MOD]) i;
   2.121 +
   2.122 +Goal "m<n ==> raw_mod (m,n) = m";
   2.123 +by (rtac (raw_mod_def RS def_transrec RS trans) 1);
   2.124 +by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1);
   2.125 +qed "raw_mod_less";
   2.126 +
   2.127 +Goal "[| m<n; n : nat |] ==> m mod n = m";
   2.128 +by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
   2.129 +by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_less]) 1);
   2.130 +qed "mod_less";
   2.131 +
   2.132 +Goal "[| 0<n; n le m;  m:nat |] ==> raw_mod (m, n) = raw_mod (m#-n, n)";
   2.133 +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   2.134 +by (rtac (raw_mod_def RS def_transrec RS trans) 1);
   2.135 +by (asm_simp_tac div_ss 1);
   2.136 +by (Blast_tac 1);
   2.137 +qed "raw_mod_geq";
   2.138 +
   2.139 +Goal "[| n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
   2.140 +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   2.141 +by (div_undefined_case_tac "n=0" 1);
   2.142 +by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_geq]) 1);
   2.143 +qed "mod_geq";
   2.144 +
   2.145 +Addsimps [mod_less];
   2.146 +
   2.147 +
   2.148 +(*** Division ***)
   2.149 +
   2.150 +Goalw [raw_div_def] "[| m:nat;  n:nat |] ==> raw_div (m, n) : nat";
   2.151 +by (rtac Ord_transrec_type 1);
   2.152 +by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]));
   2.153 +by (REPEAT (ares_tac div_rls 1));
   2.154 +qed "raw_div_type";
   2.155 +
   2.156 +Goalw [div_def] "m div n : nat";
   2.157 +by (simp_tac (simpset() addsimps [div_def, raw_div_type]) 1);
   2.158 +qed "div_type";
   2.159 +AddTCs [div_type];
   2.160 +AddIffs [div_type];
   2.161 +
   2.162 +Goal "m<n ==> raw_div (m,n) = 0";
   2.163 +by (rtac (raw_div_def RS def_transrec RS trans) 1);
   2.164 +by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1);
   2.165 +qed "raw_div_less";
   2.166 +
   2.167 +Goal "[| m<n; n : nat |] ==> m div n = 0";
   2.168 +by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
   2.169 +by (asm_simp_tac (simpset() addsimps [div_def, raw_div_less]) 1);
   2.170 +qed "div_less";
   2.171 +
   2.172 +Goal "[| 0<n;  n le m;  m:nat |] ==> raw_div(m,n) = succ(raw_div(m#-n, n))";
   2.173 +by (subgoal_tac "n ~= 0" 1);
   2.174 +by (Blast_tac 2);
   2.175 +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   2.176 +by (rtac (raw_div_def RS def_transrec RS trans) 1);
   2.177 +by (asm_simp_tac div_ss 1);
   2.178 +qed "raw_div_geq";
   2.179 +
   2.180 +Goal "[| 0<n;  n le m;  m:nat |] ==> m div n = succ ((m#-n) div n)";
   2.181 +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   2.182 +by (asm_simp_tac (simpset() addsimps [div_def, raw_div_geq]) 1);
   2.183 +qed "div_geq";
   2.184 +
   2.185 +Addsimps [div_less, div_geq];
   2.186 +
   2.187 +
   2.188 +(*A key result*)
   2.189 +Goal "[| m: nat;  n: nat |] ==> (m div n)#*n #+ m mod n = m";
   2.190 +by (div_undefined_case_tac "n=0" 1);
   2.191 +by (etac complete_induct 1);
   2.192 +by (case_tac "x<n" 1);
   2.193 +(*case n le x*)
   2.194 +by (asm_full_simp_tac
   2.195 +     (simpset() addsimps [not_lt_iff_le, add_assoc, mod_geq,
   2.196 +                         div_termination RS ltD, add_diff_inverse]) 2);
   2.197 +(*case x<n*)
   2.198 +by (Asm_simp_tac 1);
   2.199 +val lemma = result();
   2.200 +
   2.201 +Goal "(m div n)#*n #+ m mod n = natify(m)";
   2.202 +by (subgoal_tac
   2.203 +    "(natify(m) div natify(n))#*natify(n) #+ natify(m) mod natify(n) = \
   2.204 +\    natify(m)" 1);
   2.205 +by (stac lemma 2);
   2.206 +by Auto_tac;
   2.207 +qed "mod_div_equality_natify";
   2.208 +
   2.209 +Goal "m: nat ==> (m div n)#*n #+ m mod n = m";
   2.210 +by (asm_simp_tac (simpset() addsimps [mod_div_equality_natify]) 1);
   2.211 +qed "mod_div_equality";
   2.212 +
   2.213 +
   2.214 +(*** Further facts about mod (mainly for mutilated chess board) ***)
   2.215 +
   2.216 +Goal "[| 0<n;  m:nat;  n:nat |] \
   2.217 +\     ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
   2.218 +by (etac complete_induct 1);
   2.219 +by (excluded_middle_tac "succ(x)<n" 1);
   2.220 +(* case succ(x) < n *)
   2.221 +by (asm_simp_tac (simpset() addsimps [nat_le_refl RS lt_trans, 
   2.222 +				      succ_neq_self]) 2);
   2.223 +by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2);
   2.224 +(* case n le succ(x) *)
   2.225 +by (asm_full_simp_tac (simpset() addsimps [mod_geq, not_lt_iff_le]) 1);
   2.226 +by (etac leE 1);
   2.227 +(*equality case*)
   2.228 +by (asm_full_simp_tac (simpset() addsimps [diff_self_eq_0]) 2);
   2.229 +by (asm_simp_tac (simpset() addsimps [mod_geq, div_termination RS ltD, 
   2.230 +				      diff_succ]) 1);
   2.231 +val lemma = result();
   2.232 +
   2.233 +Goal "n:nat ==> \
   2.234 +\     succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
   2.235 +by (case_tac "n=0" 1);
   2.236 +by (asm_simp_tac (simpset() addsimps [natify_succ, DIVISION_BY_ZERO_MOD]) 1);
   2.237 +by (subgoal_tac
   2.238 +    "natify(succ(m)) mod n = \
   2.239 +\      (if succ(natify(m) mod n) = n then 0 else succ(natify(m) mod n))" 1);
   2.240 +by (stac natify_succ 2);
   2.241 +by (rtac lemma 2);
   2.242 +by (auto_tac(claset(), 
   2.243 +	     simpset() delsimps [natify_succ] 
   2.244 +             addsimps [nat_into_Ord RS Ord_0_lt_iff]));
   2.245 +qed "mod_succ";
   2.246 +
   2.247 +Goal "[| 0<n;  n:nat |] ==> m mod n < n";
   2.248 +by (subgoal_tac "natify(m) mod n < n" 1);
   2.249 +by (res_inst_tac [("i","natify(m)")] complete_induct 2);
   2.250 +by (case_tac "x<n" 3);
   2.251 +(*case x<n*)
   2.252 +by (Asm_simp_tac 3);
   2.253 +(*case n le x*)
   2.254 +by (asm_full_simp_tac
   2.255 +     (simpset() addsimps [mod_geq, not_lt_iff_le, div_termination RS ltD]) 3);
   2.256 +by Auto_tac;
   2.257 +qed "mod_less_divisor";
   2.258 +
   2.259 +Goal "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
   2.260 +by (subgoal_tac "k mod 2: 2" 1);
   2.261 +by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
   2.262 +by (dtac ltD 1);
   2.263 +by Auto_tac;
   2.264 +qed "mod2_cases";
   2.265 +
   2.266 +Goal "succ(succ(m)) mod 2 = m mod 2";
   2.267 +by (subgoal_tac "m mod 2: 2" 1);
   2.268 +by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
   2.269 +by (auto_tac (claset(), simpset() addsimps [mod_succ]));  
   2.270 +qed "mod2_succ_succ";
   2.271 +
   2.272 +Addsimps [mod2_succ_succ];
   2.273 +
   2.274 +Goal "(m#+m#+n) mod 2 = n mod 2";
   2.275 +by (subgoal_tac "(natify(m)#+natify(m)#+n) mod 2 = n mod 2" 1);
   2.276 +by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   2.277 +by Auto_tac;
   2.278 +qed "mod2_add_more";
   2.279 +
   2.280 +Goal "(m#+m) mod 2 = 0";
   2.281 +by (cut_inst_tac [("n","0")] mod2_add_more 1);
   2.282 +by Auto_tac;
   2.283 +qed "mod2_add_self";
   2.284 +
   2.285 +Addsimps [mod2_add_more, mod2_add_self];
   2.286 +
   2.287 +
   2.288 +(**** Additional theorems about "le" ****)
   2.289 +
   2.290 +Goal "m:nat ==> m le (m #+ n)";
   2.291 +by (induct_tac "m" 1);
   2.292 +by (ALLGOALS Asm_simp_tac);
   2.293 +qed "add_le_self";
   2.294 +
   2.295 +Goal "m:nat ==> m le (n #+ m)";
   2.296 +by (stac add_commute 1);
   2.297 +by (etac add_le_self 1);
   2.298 +qed "add_le_self2";
   2.299 +
   2.300 +(*** Monotonicity of Multiplication ***)
   2.301 +
   2.302 +Goal "[| i le j; j:nat |] ==> (i#*k) le (j#*k)";
   2.303 +by (subgoal_tac "natify(i)#*natify(k) le j#*natify(k)" 1);
   2.304 +by (ftac lt_nat_in_nat 2);
   2.305 +by (res_inst_tac [("n","natify(k)")] nat_induct 3);
   2.306 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_le_mono])));
   2.307 +qed "mult_le_mono1";
   2.308 +
   2.309 +(* le monotonicity, BOTH arguments*)
   2.310 +Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l";
   2.311 +by (rtac (mult_le_mono1 RS le_trans) 1);
   2.312 +by (REPEAT (assume_tac 1));
   2.313 +by (EVERY [stac mult_commute 1,
   2.314 +           stac mult_commute 1,
   2.315 +           rtac mult_le_mono1 1]);
   2.316 +by (REPEAT (assume_tac 1));
   2.317 +qed "mult_le_mono";
   2.318 +
   2.319 +(*strict, in 1st argument; proof is by induction on k>0.
   2.320 +  I can't see how to relax the typing conditions.*)
   2.321 +Goal "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
   2.322 +by (etac zero_lt_natE 1);
   2.323 +by (ftac lt_nat_in_nat 2);
   2.324 +by (ALLGOALS Asm_simp_tac);
   2.325 +by (induct_tac "x" 1);
   2.326 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
   2.327 +qed "mult_lt_mono2";
   2.328 +
   2.329 +Goal "[| i<j; 0<k; j:nat; k:nat |] ==> i#*k < j#*k";
   2.330 +by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, 
   2.331 +				      inst "n" "k" mult_commute]) 1);
   2.332 +qed "mult_lt_mono1";
   2.333 +
   2.334 +Goal "m#+n = 0 <-> natify(m)=0 & natify(n)=0";
   2.335 +by (subgoal_tac "natify(m) #+ natify(n) = 0 <-> natify(m)=0 & natify(n)=0" 1);
   2.336 +by (res_inst_tac [("n","natify(m)")] natE 2);
   2.337 + by (res_inst_tac [("n","natify(n)")] natE 4);
   2.338 +by Auto_tac;  
   2.339 +qed "add_eq_0_iff";
   2.340 +AddIffs [add_eq_0_iff];
   2.341 +
   2.342 +Goal "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)";
   2.343 +by (subgoal_tac "0 < natify(m)#*natify(n) <-> \
   2.344 +\                0 < natify(m) & 0 < natify(n)" 1);
   2.345 +by (res_inst_tac [("n","natify(m)")] natE 2);
   2.346 + by (res_inst_tac [("n","natify(n)")] natE 4);
   2.347 +  by (res_inst_tac [("n","natify(n)")] natE 3);
   2.348 +by Auto_tac;  
   2.349 +qed "zero_lt_mult_iff";
   2.350 +
   2.351 +Goal "m#*n = 1 <-> natify(m)=1 & natify(n)=1";
   2.352 +by (subgoal_tac "natify(m) #* natify(n) = 1 <-> natify(m)=1 & natify(n)=1" 1);
   2.353 +by (res_inst_tac [("n","natify(m)")] natE 2);
   2.354 + by (res_inst_tac [("n","natify(n)")] natE 4);
   2.355 +by Auto_tac;  
   2.356 +qed "mult_eq_1_iff";
   2.357 +AddIffs [zero_lt_mult_iff, mult_eq_1_iff];
   2.358 +
   2.359 +(*Cancellation law for division*)
   2.360 +Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n";
   2.361 +by (eres_inst_tac [("i","m")] complete_induct 1);
   2.362 +by (excluded_middle_tac "x<n" 1);
   2.363 +by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff, 
   2.364 +                                     mult_lt_mono2]) 2);
   2.365 +by (asm_full_simp_tac
   2.366 +     (simpset() addsimps [not_lt_iff_le, 
   2.367 +                         zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq,
   2.368 +                         diff_mult_distrib2 RS sym,
   2.369 +                         div_termination RS ltD]) 1);
   2.370 +qed "div_cancel";
   2.371 +
   2.372 +Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> \
   2.373 +\        (k#*m) mod (k#*n) = k #* (m mod n)";
   2.374 +by (eres_inst_tac [("i","m")] complete_induct 1);
   2.375 +by (excluded_middle_tac "x<n" 1);
   2.376 +by (asm_simp_tac (simpset() addsimps [mod_less, zero_lt_mult_iff, 
   2.377 +                                     mult_lt_mono2]) 2);
   2.378 +by (asm_full_simp_tac
   2.379 +     (simpset() addsimps [not_lt_iff_le, 
   2.380 +                         zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq,
   2.381 +                         diff_mult_distrib2 RS sym,
   2.382 +                         div_termination RS ltD]) 1);
   2.383 +qed "mult_mod_distrib";
   2.384 +
   2.385 +(*Lemma for gcd*)
   2.386 +Goal "m = m#*n ==> natify(n)=1 | m=0";
   2.387 +by (subgoal_tac "m: nat" 1);
   2.388 +by (etac ssubst 2);
   2.389 +by (rtac disjCI 1);
   2.390 +by (dtac sym 1);
   2.391 +by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
   2.392 +by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 3);
   2.393 +by Auto_tac;
   2.394 +by (subgoal_tac "m #* n = 0" 1);
   2.395 +by (stac (mult_natify2 RS sym) 2);
   2.396 +by (auto_tac (claset(), simpset() delsimps [mult_natify2]));  
   2.397 +qed "mult_eq_self_implies_10";
   2.398 +
   2.399 +Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
   2.400 +by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
   2.401 +by (etac rev_mp 1);
   2.402 +by (induct_tac "n" 1);
   2.403 +by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
   2.404 +by (blast_tac (claset() addSEs [leE] 
   2.405 +                        addSIs [add_0_right RS sym, add_succ_right RS sym]) 1);
   2.406 +qed_spec_mp "less_imp_succ_add";
   2.407 +
   2.408 +
   2.409 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/ArithSimp.thy	Mon Aug 07 10:29:54 2000 +0200
     3.3 @@ -0,0 +1,11 @@
     3.4 +(*  Title:      ZF/ArithSimp.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   2000  University of Cambridge
     3.8 +
     3.9 +Arithmetic with simplification
    3.10 +*)
    3.11 +
    3.12 +theory ArithSimp = Arith
    3.13 +files "arith_data.ML":
    3.14 +end
     4.1 --- a/src/ZF/CardinalArith.thy	Mon Aug 07 10:29:04 2000 +0200
     4.2 +++ b/src/ZF/CardinalArith.thy	Mon Aug 07 10:29:54 2000 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  Cardinal Arithmetic
     4.5  *)
     4.6  
     4.7 -CardinalArith = Cardinal + OrderArith + Arith + Finite + 
     4.8 +CardinalArith = Cardinal + OrderArith + ArithSimp + Finite + 
     4.9  consts
    4.10  
    4.11    InfCard       :: i=>o
     5.1 --- a/src/ZF/Integ/Bin.ML	Mon Aug 07 10:29:04 2000 +0200
     5.2 +++ b/src/ZF/Integ/Bin.ML	Mon Aug 07 10:29:54 2000 +0200
     5.3 @@ -105,7 +105,7 @@
     5.4  by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
     5.5  qed "integ_of_succ";
     5.6  
     5.7 -Goal "w: bin ==> integ_of(bin_pred(w)) = $~ ($#1) $+ integ_of(w)";
     5.8 +Goal "w: bin ==> integ_of(bin_pred(w)) = $- ($#1) $+ integ_of(w)";
     5.9  by (etac bin.induct 1);
    5.10  by (Simp_tac 1);
    5.11  by (Simp_tac 1);
    5.12 @@ -118,7 +118,7 @@
    5.13  
    5.14  (*** bin_minus: (unary!) negation of binary integers ***)
    5.15  
    5.16 -Goal "w: bin ==> integ_of(bin_minus(w)) = $~ integ_of(w)";
    5.17 +Goal "w: bin ==> integ_of(bin_minus(w)) = $- integ_of(w)";
    5.18  by (etac bin.induct 1);
    5.19  by (Simp_tac 1);
    5.20  by (Simp_tac 1);
    5.21 @@ -238,6 +238,41 @@
    5.22  qed "bin_mult_BIT0";
    5.23  
    5.24  
    5.25 +(** Simplification rules with integer constants **)
    5.26 +
    5.27 +Goal "#0 $+ z = intify(z)";
    5.28 +by (Simp_tac 1);
    5.29 +qed "zadd_0_intify";
    5.30 +
    5.31 +Goal "z $+ #0 = intify(z)";
    5.32 +by (Simp_tac 1);
    5.33 +qed "zadd_0_right_intify";
    5.34 +
    5.35 +Addsimps [zadd_0_intify, zadd_0_right_intify];
    5.36 +
    5.37 +Goal "#1 $* z = intify(z)";
    5.38 +by (Simp_tac 1);
    5.39 +qed "zmult_1_intify";
    5.40 +
    5.41 +Goal "z $* #1 = intify(z)";
    5.42 +by (stac zmult_commute 1);
    5.43 +by (Simp_tac 1);
    5.44 +qed "zmult_1_right_intify";
    5.45 +
    5.46 +Addsimps [zmult_1_intify, zmult_1_right_intify];
    5.47 +
    5.48 +Goal "#0 $* z = #0";
    5.49 +by (Simp_tac 1);
    5.50 +qed "zmult_0";
    5.51 +
    5.52 +Goal "z $* #0 = #0";
    5.53 +by (stac zmult_commute 1);
    5.54 +by (Simp_tac 1);
    5.55 +qed "zmult_0_right";
    5.56 +
    5.57 +Addsimps [zmult_0, zmult_0_right];
    5.58 +
    5.59 +
    5.60  (*Delete the original rewrites, with their clumsy conditional expressions*)
    5.61  Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
    5.62            NCons_Pls, NCons_Min, bin_adder_BIT, bin_mult_BIT];
     6.1 --- a/src/ZF/Integ/Bin.thy	Mon Aug 07 10:29:04 2000 +0200
     6.2 +++ b/src/ZF/Integ/Bin.thy	Mon Aug 07 10:29:54 2000 +0200
     6.3 @@ -41,7 +41,7 @@
     6.4  
     6.5  primrec
     6.6    integ_of_Pls  "integ_of (Pls)     = $# 0"
     6.7 -  integ_of_Min  "integ_of (Min)     = $~($#1)"
     6.8 +  integ_of_Min  "integ_of (Min)     = $-($#1)"
     6.9    integ_of_BIT  "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)"
    6.10  
    6.11      (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
     7.1 --- a/src/ZF/Integ/Int.ML	Mon Aug 07 10:29:04 2000 +0200
     7.2 +++ b/src/ZF/Integ/Int.ML	Mon Aug 07 10:29:54 2000 +0200
     7.3 @@ -6,10 +6,10 @@
     7.4  The integers as equivalence classes over nat*nat.
     7.5  
     7.6  Could also prove...
     7.7 -"znegative(z) ==> $# zmagnitude(z) = $~ z"
     7.8 +"znegative(z) ==> $# zmagnitude(z) = $- z"
     7.9  "~ znegative(z) ==> $# zmagnitude(z) = z"
    7.10 -$< is a linear ordering
    7.11  $+ and $* are monotonic wrt $<
    7.12 +[| m: nat;  n: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
    7.13  *)
    7.14  
    7.15  AddSEs [quotientE];
    7.16 @@ -50,14 +50,10 @@
    7.17  AddSIs [intrelI];
    7.18  AddSEs [intrelE];
    7.19  
    7.20 -val eqa::eqb::prems = goal Arith.thy 
    7.21 -    "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
    7.22 -by (res_inst_tac [("k","x2")] add_left_cancel 1);
    7.23 -by (rtac (add_left_commute RS trans) 1);
    7.24 -by Auto_tac;
    7.25 -by (stac eqb 1);
    7.26 -by (rtac (add_left_commute RS trans) 1);
    7.27 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [eqa, add_left_commute])));
    7.28 +Goal "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
    7.29 +by (rtac sym 1);
    7.30 +by (REPEAT (etac add_left_cancel 1));
    7.31 +by (ALLGOALS Asm_simp_tac);
    7.32  qed "int_trans_lemma";
    7.33  
    7.34  Goalw [equiv_def, refl_def, sym_def, trans_def]
    7.35 @@ -123,7 +119,7 @@
    7.36  by (simp_tac (simpset() addsimps [int_of_def]) 1);
    7.37  qed "int_of_natify";
    7.38  
    7.39 -Goal "$~ (intify(m)) = $~ m";
    7.40 +Goal "$- (intify(m)) = $- m";
    7.41  by (simp_tac (simpset() addsimps [zminus_def]) 1);
    7.42  qed "zminus_intify";
    7.43  
    7.44 @@ -140,6 +136,17 @@
    7.45  qed "zadd_intify2";
    7.46  Addsimps [zadd_intify1, zadd_intify2];
    7.47  
    7.48 +(** Subtraction **)
    7.49 +
    7.50 +Goal "intify(x) $- y = x $- y";
    7.51 +by (simp_tac (simpset() addsimps [zdiff_def]) 1);
    7.52 +qed "zdiff_intify1";
    7.53 +
    7.54 +Goal "x $- intify(y) = x $- y";
    7.55 +by (simp_tac (simpset() addsimps [zdiff_def]) 1);
    7.56 +qed "zdiff_intify2";
    7.57 +Addsimps [zdiff_intify1, zdiff_intify2];
    7.58 +
    7.59  (** Multiplication **)
    7.60  
    7.61  Goal "intify(x) $* y = x $* y";
    7.62 @@ -151,6 +158,17 @@
    7.63  qed "zmult_intify2";
    7.64  Addsimps [zmult_intify1, zmult_intify2];
    7.65  
    7.66 +(** Orderings **)
    7.67 +
    7.68 +Goal "intify(x) $< y <-> x $< y";
    7.69 +by (simp_tac (simpset() addsimps [zless_def]) 1);
    7.70 +qed "zless_intify1";
    7.71 +
    7.72 +Goal "x $< intify(y) <-> x $< y";
    7.73 +by (simp_tac (simpset() addsimps [zless_def]) 1);
    7.74 +qed "zless_intify2";
    7.75 +Addsimps [zless_intify1, zless_intify2];
    7.76 +
    7.77  
    7.78  (**** zminus: unary negation on int ****)
    7.79  
    7.80 @@ -168,7 +186,7 @@
    7.81  by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
    7.82  qed "raw_zminus_type";
    7.83  
    7.84 -Goalw [zminus_def] "$~z : int";
    7.85 +Goalw [zminus_def] "$-z : int";
    7.86  by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type]) 1);
    7.87  qed "zminus_type";
    7.88  AddIffs [zminus_type];
    7.89 @@ -182,13 +200,13 @@
    7.90  by (auto_tac (claset() addDs [eq_intrelD], simpset() addsimps add_ac));  
    7.91  qed "raw_zminus_inject";
    7.92  
    7.93 -Goalw [zminus_def] "$~z = $~w ==> intify(z) = intify(w)";
    7.94 +Goalw [zminus_def] "$-z = $-w ==> intify(z) = intify(w)";
    7.95  by (blast_tac (claset() addSDs [raw_zminus_inject]) 1);
    7.96  qed "zminus_inject_intify";
    7.97  
    7.98  AddSDs [zminus_inject_intify];
    7.99  
   7.100 -Goal "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
   7.101 +Goal "[| $-z = $-w;  z: int;  w: int |] ==> z=w";
   7.102  by Auto_tac;  
   7.103  qed "zminus_inject";
   7.104  
   7.105 @@ -200,7 +218,7 @@
   7.106  
   7.107  Goalw [zminus_def]
   7.108      "[| x: nat;  y: nat |] \
   7.109 -\    ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
   7.110 +\    ==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}";
   7.111  by (asm_simp_tac (simpset() addsimps [raw_zminus, image_intrel_int]) 1);
   7.112  qed "zminus";
   7.113  
   7.114 @@ -208,18 +226,18 @@
   7.115  by (auto_tac (claset(), simpset() addsimps [raw_zminus]));  
   7.116  qed "raw_zminus_zminus";
   7.117  
   7.118 -Goal "$~ ($~ z) = intify(z)";
   7.119 +Goal "$- ($- z) = intify(z)";
   7.120  by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type, 
   7.121  	                          raw_zminus_zminus]) 1);
   7.122  qed "zminus_zminus_intify"; 
   7.123  
   7.124 -Goalw [int_of_def] "$~ ($#0) = $#0";
   7.125 +Goalw [int_of_def] "$- ($#0) = $#0";
   7.126  by (simp_tac (simpset() addsimps [zminus]) 1);
   7.127  qed "zminus_0";
   7.128  
   7.129  Addsimps [zminus_zminus_intify, zminus_0];
   7.130  
   7.131 -Goal "z : int ==> $~ ($~ z) = z";
   7.132 +Goal "z : int ==> $- ($- z) = z";
   7.133  by (Asm_simp_tac 1);
   7.134  qed "zminus_zminus";
   7.135  
   7.136 @@ -232,20 +250,21 @@
   7.137  by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
   7.138  by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
   7.139  by (force_tac (claset(),
   7.140 -	       simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
   7.141 +	       simpset() addsimps [add_le_self2 RS le_imp_not_lt,
   7.142 +				   natify_succ]) 1);
   7.143  qed "not_znegative_int_of";
   7.144  
   7.145  Addsimps [not_znegative_int_of];
   7.146  AddSEs   [not_znegative_int_of RS notE];
   7.147  
   7.148 -Goalw [znegative_def, int_of_def] "znegative($~ $# succ(n))";
   7.149 -by (asm_simp_tac (simpset() addsimps [zminus]) 1);
   7.150 +Goalw [znegative_def, int_of_def] "znegative($- $# succ(n))";
   7.151 +by (asm_simp_tac (simpset() addsimps [zminus, natify_succ]) 1);
   7.152  by (blast_tac (claset() addIs [nat_0_le]) 1);
   7.153  qed "znegative_zminus_int_of";
   7.154  
   7.155  Addsimps [znegative_zminus_int_of];
   7.156  
   7.157 -Goalw [znegative_def, int_of_def] "~ znegative($~ $# n) ==> natify(n)=0";
   7.158 +Goalw [znegative_def, int_of_def] "~ znegative($- $# n) ==> natify(n)=0";
   7.159  by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
   7.160  by (dres_inst_tac [("x","0")] spec 1);
   7.161  by (auto_tac(claset(), 
   7.162 @@ -263,7 +282,7 @@
   7.163  by (asm_simp_tac (simpset() addsimps [int_of_eq]) 1);
   7.164  qed "natify_int_of_eq";
   7.165  
   7.166 -Goalw [zmagnitude_def] "zmagnitude($~ $# n) = natify(n)";
   7.167 +Goalw [zmagnitude_def] "zmagnitude($- $# n) = natify(n)";
   7.168  by (rtac the_equality 1);
   7.169  by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq], 
   7.170                simpset())
   7.171 @@ -300,17 +319,12 @@
   7.172  
   7.173  
   7.174  Goalw [int_def, znegative_def, int_of_def]
   7.175 -     "[| z: int; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; 
   7.176 -by (auto_tac(claset() addSDs [less_imp_Suc_add], 
   7.177 +     "[| z: int; znegative(z) |] ==> EX n:nat. z = $- ($# succ(n))"; 
   7.178 +by (auto_tac(claset() addSDs [less_imp_succ_add], 
   7.179  	     simpset() addsimps [zminus, image_singleton_iff]));
   7.180 -by (rename_tac "m n j k" 1);
   7.181 -by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
   7.182 -by (rotate_tac ~2 2);
   7.183 -by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
   7.184 -by (blast_tac (claset() addSDs [add_left_cancel]) 1);
   7.185  qed "zneg_int_of";
   7.186  
   7.187 -Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
   7.188 +Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $- z"; 
   7.189  by (dtac zneg_int_of 1);
   7.190  by Auto_tac;
   7.191  qed "zneg_mag"; 
   7.192 @@ -367,26 +381,28 @@
   7.193  
   7.194  Goalw [int_def,int_of_def] "z : int ==> raw_zadd ($#0,z) = z";
   7.195  by (auto_tac (claset(), simpset() addsimps [raw_zadd]));  
   7.196 -qed "raw_zadd_0";
   7.197 +qed "raw_zadd_int0";
   7.198  
   7.199  Goal "$#0 $+ z = intify(z)";
   7.200 -by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_0]) 1);
   7.201 -qed "zadd_0_intify";
   7.202 -Addsimps [zadd_0_intify];
   7.203 +by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_int0]) 1);
   7.204 +qed "zadd_int0_intify";
   7.205 +Addsimps [zadd_int0_intify];
   7.206  
   7.207  Goal "z: int ==> $#0 $+ z = z";
   7.208  by (Asm_simp_tac 1);
   7.209 -qed "zadd_0";
   7.210 +qed "zadd_int0";
   7.211  
   7.212  Goalw [int_def]
   7.213 -     "[| z: int;  w: int |] ==> $~ raw_zadd(z,w) = raw_zadd($~ z, $~ w)";
   7.214 +     "[| z: int;  w: int |] ==> $- raw_zadd(z,w) = raw_zadd($- z, $- w)";
   7.215  by (auto_tac (claset(), simpset() addsimps [zminus,raw_zadd]));  
   7.216  qed "raw_zminus_zadd_distrib";
   7.217  
   7.218 -Goal "$~ (z $+ w) = $~ z $+ $~ w";
   7.219 +Goal "$- (z $+ w) = $- z $+ $- w";
   7.220  by (simp_tac (simpset() addsimps [zadd_def, raw_zminus_zadd_distrib]) 1);
   7.221  qed "zminus_zadd_distrib";
   7.222  
   7.223 +Addsimps [zminus_zadd_distrib];
   7.224 +
   7.225  Goalw [int_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)";
   7.226  by (auto_tac (claset(), simpset() addsimps raw_zadd::add_ac));  
   7.227  qed "raw_zadd_commute";
   7.228 @@ -418,35 +434,32 @@
   7.229  by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   7.230  qed "int_of_add";
   7.231  
   7.232 -Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $~ z) = $#0";
   7.233 +Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $- z) = $#0";
   7.234  by (auto_tac (claset(), simpset() addsimps [zminus, raw_zadd, add_commute]));  
   7.235  qed "raw_zadd_zminus_inverse";
   7.236  
   7.237 -Goal "z $+ ($~ z) = $#0";
   7.238 +Goal "z $+ ($- z) = $#0";
   7.239  by (simp_tac (simpset() addsimps [zadd_def]) 1);
   7.240  by (stac (zminus_intify RS sym) 1);
   7.241  by (rtac (intify_in_int RS raw_zadd_zminus_inverse) 1); 
   7.242  qed "zadd_zminus_inverse";
   7.243  
   7.244 -Goal "($~ z) $+ z = $#0";
   7.245 +Goal "($- z) $+ z = $#0";
   7.246  by (simp_tac (simpset() addsimps [zadd_commute, zadd_zminus_inverse]) 1);
   7.247  qed "zadd_zminus_inverse2";
   7.248  
   7.249  Goal "z $+ $#0 = intify(z)";
   7.250 -by (rtac ([zadd_commute, zadd_0_intify] MRS trans) 1);
   7.251 -qed "zadd_0_right_intify";
   7.252 -Addsimps [zadd_0_right_intify];
   7.253 +by (rtac ([zadd_commute, zadd_int0_intify] MRS trans) 1);
   7.254 +qed "zadd_int0_right_intify";
   7.255 +Addsimps [zadd_int0_right_intify];
   7.256  
   7.257  Goal "z:int ==> z $+ $#0 = z";
   7.258  by (Asm_simp_tac 1);
   7.259 -qed "zadd_0_right";
   7.260 +qed "zadd_int0_right";
   7.261  
   7.262  Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
   7.263  
   7.264  
   7.265 -(*Need properties of $- ???  Or use $- just as an abbreviation?
   7.266 -     [| m: nat;  n: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
   7.267 -*)
   7.268  
   7.269  (**** zmult: multiplication on int ****)
   7.270  
   7.271 @@ -456,15 +469,14 @@
   7.272  \               split(%x1 y1. split(%x2 y2.     \
   7.273  \                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
   7.274  by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   7.275 -by Safe_tac;
   7.276 -by (ALLGOALS Asm_simp_tac);
   7.277 +by Auto_tac;
   7.278  (*Proof that zmult is congruent in one argument*)
   7.279 -by (asm_simp_tac 
   7.280 -    (simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2);
   7.281 -by (asm_simp_tac
   7.282 -    (simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2);
   7.283 -(*Proof that zmult is commutative on representatives*)
   7.284 -by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1);
   7.285 +by (rename_tac "x y" 1);
   7.286 +by (forw_inst_tac [("t", "%u. x#*u")] (sym RS subst_context) 1);
   7.287 +by (dres_inst_tac [("t", "%u. y#*u")] subst_context 1);
   7.288 +by (REPEAT (etac add_left_cancel 1));
   7.289 +by (asm_simp_tac (simpset() addsimps [add_mult_distrib_left]) 1);
   7.290 +by Auto_tac;
   7.291  qed "zmult_congruent2";
   7.292  
   7.293  
   7.294 @@ -498,25 +510,25 @@
   7.295  
   7.296  Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#0,z) = $#0";
   7.297  by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
   7.298 -qed "raw_zmult_0";
   7.299 +qed "raw_zmult_int0";
   7.300  
   7.301  Goal "$#0 $* z = $#0";
   7.302 -by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_0]) 1);
   7.303 -qed "zmult_0";
   7.304 -Addsimps [zmult_0];
   7.305 +by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_int0]) 1);
   7.306 +qed "zmult_int0";
   7.307 +Addsimps [zmult_int0];
   7.308  
   7.309  Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#1,z) = z";
   7.310  by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
   7.311 -qed "raw_zmult_1";
   7.312 +qed "raw_zmult_int1";
   7.313  
   7.314  Goal "$#1 $* z = intify(z)";
   7.315 -by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_1]) 1);
   7.316 -qed "zmult_1_intify";
   7.317 -Addsimps [zmult_1_intify];
   7.318 +by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_int1]) 1);
   7.319 +qed "zmult_int1_intify";
   7.320 +Addsimps [zmult_int1_intify];
   7.321  
   7.322  Goal "z : int ==> $#1 $* z = z";
   7.323  by (Asm_simp_tac 1);
   7.324 -qed "zmult_1";
   7.325 +qed "zmult_int1";
   7.326  
   7.327  Goalw [int_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)";
   7.328  by (auto_tac (claset(), simpset() addsimps [raw_zmult] @ add_ac @ mult_ac));  
   7.329 @@ -527,18 +539,18 @@
   7.330  qed "zmult_commute";
   7.331  
   7.332  Goalw [int_def]
   7.333 -     "[| z: int;  w: int |] ==> raw_zmult($~ z, w) = $~ raw_zmult(z, w)";
   7.334 +     "[| z: int;  w: int |] ==> raw_zmult($- z, w) = $- raw_zmult(z, w)";
   7.335  by (auto_tac (claset(), simpset() addsimps [zminus, raw_zmult] @ add_ac));  
   7.336  qed "raw_zmult_zminus";
   7.337  
   7.338 -Goal "($~ z) $* w = $~ (z $* w)";
   7.339 +Goal "($- z) $* w = $- (z $* w)";
   7.340  by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_zminus]) 1);
   7.341  by (stac (zminus_intify RS sym) 1 THEN rtac raw_zmult_zminus 1); 
   7.342  by Auto_tac;  
   7.343  qed "zmult_zminus";
   7.344  Addsimps [zmult_zminus];
   7.345  
   7.346 -Goal "($~ z) $* ($~ w) = (z $* w)";
   7.347 +Goal "($- z) $* ($- w) = (z $* w)";
   7.348  by (stac zmult_zminus 1);
   7.349  by (stac zmult_commute 1 THEN stac zmult_zminus 1);
   7.350  by (simp_tac (simpset() addsimps [zmult_commute])1);
   7.351 @@ -588,3 +600,230 @@
   7.352      [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
   7.353  
   7.354  
   7.355 +(*** Subtraction laws ***)
   7.356 +
   7.357 +Goal "$#0 $- x = $-x";
   7.358 +by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   7.359 +qed "zdiff_int0";
   7.360 +
   7.361 +Goal "x $- $#0 = intify(x)";
   7.362 +by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   7.363 +qed "zdiff_int0_right";
   7.364 +
   7.365 +Goal "x $- x = $#0";
   7.366 +by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   7.367 +qed "zdiff_self";
   7.368 +
   7.369 +Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self];
   7.370 +
   7.371 +
   7.372 +Goalw [zdiff_def] "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)";
   7.373 +by (stac zadd_zmult_distrib 1);
   7.374 +by (simp_tac (simpset() addsimps [zmult_zminus]) 1);
   7.375 +qed "zdiff_zmult_distrib";
   7.376 +
   7.377 +val zmult_commute'= inst "z" "w" zmult_commute;
   7.378 +
   7.379 +Goal "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)";
   7.380 +by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1);
   7.381 +qed "zdiff_zmult_distrib2";
   7.382 +
   7.383 +Goal "x $+ (y $- z) = (x $+ y) $- z";
   7.384 +by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   7.385 +qed "zadd_zdiff_eq";
   7.386 +
   7.387 +Goal "(x $- y) $+ z = (x $+ z) $- y";
   7.388 +by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   7.389 +qed "zdiff_zadd_eq";
   7.390 +
   7.391 +
   7.392 +(*** "Less Than" ***)
   7.393 +
   7.394 +(*"Less than" is a linear ordering*)
   7.395 +Goalw [int_def, zless_def, znegative_def, zdiff_def] 
   7.396 +     "[| z: int; w: int |] ==> z$<w | z=w | w$<z"; 
   7.397 +by Auto_tac;  
   7.398 +by (asm_full_simp_tac
   7.399 +    (simpset() addsimps [zadd, zminus, image_iff, Bex_def]) 1);
   7.400 +by (res_inst_tac [("i", "xb#+ya"), ("j", "xc #+ y")] Ord_linear_lt 1);
   7.401 +by (ALLGOALS (force_tac (claset() addSDs [spec], 
   7.402 +                         simpset() addsimps add_ac)));
   7.403 +qed "zless_linear_lemma";
   7.404 +
   7.405 +Goal "z$<w | intify(z)=intify(w) | w$<z"; 
   7.406 +by (cut_inst_tac [("z"," intify(z)"),("w"," intify(w)")] zless_linear_lemma 1);
   7.407 +by Auto_tac;  
   7.408 +qed "zless_linear";
   7.409 +
   7.410 +Goal "~ (z$<z)";
   7.411 +by (auto_tac (claset(), 
   7.412 +              simpset() addsimps  [zless_def, znegative_def, int_of_def]));  
   7.413 +by (rotate_tac 2 1);
   7.414 +by Auto_tac;  
   7.415 +qed "zless_not_refl";
   7.416 +AddIffs [zless_not_refl];
   7.417 +
   7.418 +(*This lemma allows direct proofs of other <-properties*)
   7.419 +Goalw [zless_def, znegative_def, zdiff_def, int_def] 
   7.420 +    "[| w $< z; w: int; z: int |] ==> (EX n. z = w $+ $#(succ(n)))";
   7.421 +by (auto_tac (claset() addSDs [less_imp_succ_add], 
   7.422 +              simpset() addsimps [zadd, zminus, int_of_def]));  
   7.423 +by (res_inst_tac [("x","k")] exI 1);
   7.424 +by (etac add_left_cancel 1);
   7.425 +by Auto_tac;  
   7.426 +qed "zless_imp_succ_zadd_lemma";
   7.427 +
   7.428 +Goal "w $< z ==> (EX n. w $+ $#(succ(n)) = intify(z))";
   7.429 +by (subgoal_tac "intify(w) $< intify(z)" 1);
   7.430 +by (dres_inst_tac [("w","intify(w)")] zless_imp_succ_zadd_lemma 1);
   7.431 +by Auto_tac;  
   7.432 +qed "zless_imp_succ_zadd";
   7.433 +
   7.434 +Goalw [zless_def, znegative_def, zdiff_def, int_def] 
   7.435 +    "w : int ==> w $< w $+ $# succ(n)";
   7.436 +by (auto_tac (claset(), 
   7.437 +              simpset() addsimps [zadd, zminus, int_of_def, image_iff]));  
   7.438 +by (res_inst_tac [("x","0")] exI 1);
   7.439 +by Auto_tac;  
   7.440 +qed "zless_succ_zadd_lemma";
   7.441 +
   7.442 +Goal "w $< w $+ $# succ(n)";
   7.443 +by (cut_facts_tac [intify_in_int RS zless_succ_zadd_lemma] 1);
   7.444 +by Auto_tac;  
   7.445 +qed "zless_succ_zadd";
   7.446 +
   7.447 +Goal "w $< z <-> (EX n. w $+ $#(succ(n)) = intify(z))";
   7.448 +by (rtac iffI 1);
   7.449 +by (etac zless_imp_succ_zadd 1);
   7.450 +by Auto_tac;  
   7.451 +by (cut_inst_tac [("w","w"),("n","n")] zless_succ_zadd 1);
   7.452 +by Auto_tac;  
   7.453 +qed "zless_iff_succ_zadd";
   7.454 +
   7.455 +Goalw [zless_def, znegative_def, zdiff_def, int_def] 
   7.456 +    "[| x $< y; y $< z; x: int; y : int; z: int |] ==> x $< z"; 
   7.457 +by (auto_tac (claset(), 
   7.458 +              simpset() addsimps [zadd, zminus, int_of_def, image_iff]));
   7.459 +by (rename_tac "x1 x2 y1 y2" 1);
   7.460 +by (res_inst_tac [("x","x1#+x2")] exI 1);  
   7.461 +by (res_inst_tac [("x","y1#+y2")] exI 1);  
   7.462 +by (auto_tac (claset(), simpset() addsimps [add_lt_mono]));  
   7.463 +by (rtac sym 1);
   7.464 +by (REPEAT (etac add_left_cancel 1));
   7.465 +by Auto_tac;  
   7.466 +qed "zless_trans_lemma";
   7.467 +
   7.468 +Goal "[| x $< y; y $< z |] ==> x $< z"; 
   7.469 +by (subgoal_tac "intify(x) $< intify(z)" 1);
   7.470 +by (res_inst_tac [("y", "intify(y)")] zless_trans_lemma 2);
   7.471 +by Auto_tac;  
   7.472 +qed "zless_trans";
   7.473 +
   7.474 +
   7.475 +Goalw [zle_def] "z $<= z";
   7.476 +by Auto_tac;  
   7.477 +qed "zle_refl";
   7.478 +
   7.479 +Goalw [zle_def] "[| x $<= y; y $<= x |] ==> x=y";
   7.480 +by (blast_tac (claset() addDs [zless_trans]) 1);
   7.481 +qed "zle_anti_sym";
   7.482 +
   7.483 +Goalw [zle_def] "[| x $<= y; y $<= z |] ==> x $<= z";
   7.484 +by (blast_tac (claset() addIs [zless_trans]) 1);
   7.485 +qed "zle_trans";
   7.486 +
   7.487 +
   7.488 +(*** More subtraction laws (for zcompare_rls): useful? ***)
   7.489 +
   7.490 +Goal "(x $- y) $- z = x $- (y $+ z)";
   7.491 +by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   7.492 +qed "zdiff_zdiff_eq";
   7.493 +
   7.494 +Goal "x $- (y $- z) = (x $+ z) $- y";
   7.495 +by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   7.496 +qed "zdiff_zdiff_eq2";
   7.497 +
   7.498 +Goalw [zless_def, zdiff_def] "(x$-y $< z) <-> (x $< z $+ y)";
   7.499 +by (simp_tac (simpset() addsimps zadd_ac) 1);
   7.500 +qed "zdiff_zless_iff";
   7.501 +
   7.502 +Goalw [zless_def, zdiff_def] "(x $< z$-y) <-> (x $+ y $< z)";
   7.503 +by (simp_tac (simpset() addsimps zadd_ac) 1);
   7.504 +qed "zless_zdiff_iff";
   7.505 +
   7.506 +Goalw [zdiff_def] "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)";
   7.507 +by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
   7.508 +qed "zdiff_eq_iff";
   7.509 +
   7.510 +Goalw [zdiff_def] "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)";
   7.511 +by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
   7.512 +qed "eq_zdiff_iff";
   7.513 +
   7.514 +(**Could not prove these!
   7.515 +Goalw [zle_def] "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)";
   7.516 +by (asm_simp_tac (simpset() addsimps [zdiff_eq_iff, zless_zdiff_iff]) 1);
   7.517 +by Auto_tac;  
   7.518 +qed "zdiff_zle_iff";
   7.519 +
   7.520 +Goalw [zle_def] "(x $<= z$-y) <-> (x $+ y $<= z)";
   7.521 +by (simp_tac (simpset() addsimps [zdiff_zless_iff]) 1);
   7.522 +qed "zle_zdiff_iff";
   7.523 +**)
   7.524 +
   7.525 +
   7.526 +(*** Monotonicity/cancellation results that could allow instantiation
   7.527 +     of the CancelNumerals simprocs ***)
   7.528 +
   7.529 +Goal "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)";
   7.530 +by Safe_tac;
   7.531 +by (dres_inst_tac [("t", "%x. x $+ ($-z)")] subst_context 1);
   7.532 +by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
   7.533 +qed "zadd_left_cancel";
   7.534 +
   7.535 +Goal "(z $+ w' = z $+ w) <-> intify(w') = intify(w)";
   7.536 +by (rtac iff_trans 1);
   7.537 +by (rtac zadd_left_cancel 2);
   7.538 +by Auto_tac;  
   7.539 +qed "zadd_left_cancel_intify";
   7.540 +
   7.541 +Addsimps [zadd_left_cancel_intify];
   7.542 +
   7.543 +Goal "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)";
   7.544 +by Safe_tac;
   7.545 +by (dres_inst_tac [("t", "%x. x $+ ($-z)")] subst_context 1);
   7.546 +by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
   7.547 +qed "zadd_right_cancel";
   7.548 +
   7.549 +Goal "(w' $+ z = w $+ z) <-> intify(w') = intify(w)";
   7.550 +by (rtac iff_trans 1);
   7.551 +by (rtac zadd_right_cancel 2);
   7.552 +by Auto_tac;  
   7.553 +qed "zadd_right_cancel_intify";
   7.554 +
   7.555 +Addsimps [zadd_right_cancel_intify];
   7.556 +
   7.557 +
   7.558 +Goal "(w' $+ z $< w $+ z) <-> (w' $< w)";
   7.559 +by (simp_tac (simpset() addsimps [zdiff_zless_iff RS iff_sym]) 1);
   7.560 +by (simp_tac (simpset() addsimps [zdiff_def, zadd_assoc]) 1);
   7.561 +qed "zadd_right_cancel_zless";
   7.562 +
   7.563 +Goal "(z $+ w' $< z $+ w) <-> (w' $< w)";
   7.564 +by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
   7.565 +                                  zadd_right_cancel_zless]) 1);
   7.566 +qed "zadd_left_cancel_zless";
   7.567 +
   7.568 +Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
   7.569 +
   7.570 +
   7.571 +Goal "(w' $+ z $<= w $+ z) <-> (intify(w') $<= intify(w))";
   7.572 +by (simp_tac (simpset() addsimps [zle_def]) 1);
   7.573 +qed "zadd_right_cancel_zle";
   7.574 +
   7.575 +Goal "(z $+ w' $<= z $+ w) <->  (intify(w') $<= intify(w))";
   7.576 +by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
   7.577 +                                  zadd_right_cancel_zle]) 1);
   7.578 +qed "zadd_left_cancel_zle";
   7.579 +
   7.580 +Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
   7.581 +
     8.1 --- a/src/ZF/Integ/Int.thy	Mon Aug 07 10:29:04 2000 +0200
     8.2 +++ b/src/ZF/Integ/Int.thy	Mon Aug 07 10:29:54 2000 +0200
     8.3 @@ -6,7 +6,7 @@
     8.4  The integers as equivalence classes over nat*nat.
     8.5  *)
     8.6  
     8.7 -Int = EquivClass + Arith +
     8.8 +Int = EquivClass + ArithSimp +
     8.9  
    8.10  constdefs
    8.11    intrel :: i
    8.12 @@ -25,8 +25,8 @@
    8.13    raw_zminus :: i=>i
    8.14      "raw_zminus(z) == UN <x,y>: z. intrel``{<y,x>}"
    8.15  
    8.16 -  zminus :: i=>i                                 ("$~ _" [80] 80)
    8.17 -    "$~ z == raw_zminus (intify(z))"
    8.18 +  zminus :: i=>i                                 ("$- _" [80] 80)
    8.19 +    "$- z == raw_zminus (intify(z))"
    8.20  
    8.21    znegative   ::      i=>o
    8.22      "znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
    8.23 @@ -34,7 +34,7 @@
    8.24    zmagnitude  ::      i=>i
    8.25      "zmagnitude(z) ==
    8.26       THE m. m : nat & ((~ znegative(z) & z = $# m) |
    8.27 -		       (znegative(z) & $~ z = $# m))"
    8.28 +		       (znegative(z) & $- z = $# m))"
    8.29  
    8.30    raw_zmult   ::      [i,i]=>i
    8.31      (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
    8.32 @@ -61,6 +61,9 @@
    8.33    zless        ::      [i,i]=>o      (infixl "$<" 50)
    8.34       "z1 $< z2 == znegative(z1 $- z2)"
    8.35    
    8.36 +  zle          ::      [i,i]=>o      (infixl "$<=" 50)
    8.37 +     "z1 $<= z2 == z1 $< z2 | z1=z2"
    8.38 +  
    8.39  (*div and mod await definitions!*)
    8.40  consts
    8.41    "$'/"       ::      [i,i]=>i      (infixl 70) 
     9.1 --- a/src/ZF/IsaMakefile	Mon Aug 07 10:29:04 2000 +0200
     9.2 +++ b/src/ZF/IsaMakefile	Mon Aug 07 10:29:54 2000 +0200
     9.3 @@ -26,7 +26,8 @@
     9.4  FOL:
     9.5  	@cd $(SRC)/FOL; $(ISATOOL) make FOL
     9.6  
     9.7 -$(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy Bool.ML Bool.thy	\
     9.8 +$(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy Bool.ML           \
     9.9 +  arith_data.ML ArithSimp.thy ArithSimp.ML Bool.thy                	\
    9.10    Cardinal.ML Cardinal.thy CardinalArith.ML CardinalArith.thy		\
    9.11    Cardinal_AC.ML Cardinal_AC.thy Datatype.ML Datatype.thy Epsilon.ML	\
    9.12    Epsilon.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy Inductive.ML	\
    10.1 --- a/src/ZF/List.ML	Mon Aug 07 10:29:04 2000 +0200
    10.2 +++ b/src/ZF/List.ML	Mon Aug 07 10:29:54 2000 +0200
    10.3 @@ -308,16 +308,12 @@
    10.4  Goal "[| xs: list(nat);  ys: list(nat) |] ==> \
    10.5  \    list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
    10.6  by (induct_tac "xs" 1);
    10.7 -by (ALLGOALS 
    10.8 -    (asm_simp_tac (simpset() addsimps [add_0_right, add_assoc RS sym])));
    10.9 -by (rtac (add_commute RS subst_context) 1);
   10.10 -by (REPEAT (ares_tac [refl, list_add_type] 1));
   10.11 +by (ALLGOALS Asm_simp_tac);
   10.12  qed "list_add_app";
   10.13  
   10.14  Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
   10.15  by (induct_tac "l" 1);
   10.16 -by (ALLGOALS
   10.17 -    (asm_simp_tac (simpset() addsimps [list_add_app, add_0_right])));
   10.18 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
   10.19  qed "list_add_rev";
   10.20  
   10.21  Goal "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
    11.1 --- a/src/ZF/List.thy	Mon Aug 07 10:29:04 2000 +0200
    11.2 +++ b/src/ZF/List.thy	Mon Aug 07 10:29:54 2000 +0200
    11.3 @@ -10,7 +10,7 @@
    11.4  although complicating its derivation.
    11.5  *)
    11.6  
    11.7 -List = Datatype + Arith +
    11.8 +List = Datatype + ArithSimp +
    11.9  
   11.10  consts
   11.11    list       :: i=>i
    12.1 --- a/src/ZF/ROOT.ML	Mon Aug 07 10:29:04 2000 +0200
    12.2 +++ b/src/ZF/ROOT.ML	Mon Aug 07 10:29:54 2000 +0200
    12.3 @@ -18,6 +18,8 @@
    12.4  (*Add user sections for inductive/datatype definitions*)
    12.5  use     "thy_syntax";
    12.6  
    12.7 +use "~~/src/Provers/Arith/cancel_numerals.ML";
    12.8 +
    12.9  use_thy "ZF";
   12.10  use     "Tools/typechk";
   12.11  use_thy "mono";
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/ZF/arith_data.ML	Mon Aug 07 10:29:54 2000 +0200
    13.3 @@ -0,0 +1,256 @@
    13.4 +(*  Title:      ZF/arith_data.ML
    13.5 +    ID:         $Id$
    13.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7 +    Copyright   2000  University of Cambridge
    13.8 +
    13.9 +Arithmetic simplification: cancellation of common terms
   13.10 +*)
   13.11 +
   13.12 +signature ARITH_DATA =
   13.13 +sig
   13.14 +  val nat_cancel: simproc list
   13.15 +end;
   13.16 +
   13.17 +structure ArithData: ARITH_DATA =
   13.18 +struct
   13.19 +
   13.20 +val iT = Ind_Syntax.iT;
   13.21 +
   13.22 +val zero = Const("0", iT);
   13.23 +val succ = Const("succ", iT --> iT);
   13.24 +fun mk_succ t = succ $ t;
   13.25 +val one = mk_succ zero;
   13.26 +
   13.27 +(*Not FOLogic.mk_binop, since it calls fastype_of, which can fail*)
   13.28 +fun mk_binop_i  c (t,u) = Const (c, [iT,iT] ---> iT) $ t $ u;
   13.29 +fun mk_binrel_i c (t,u) = Const (c, [iT,iT] ---> oT) $ t $ u;
   13.30 +
   13.31 +val mk_plus = mk_binop_i "Arith.add";
   13.32 +
   13.33 +(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
   13.34 +fun mk_sum []        = zero
   13.35 +  | mk_sum [t,u]     = mk_plus (t, u)
   13.36 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   13.37 +
   13.38 +(*this version ALWAYS includes a trailing zero*)
   13.39 +fun long_mk_sum []        = zero
   13.40 +  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   13.41 +
   13.42 +val dest_plus = FOLogic.dest_bin "Arith.add" iT;
   13.43 +
   13.44 +(* dest_sum *)
   13.45 +
   13.46 +fun dest_sum (Const("0",_)) = []
   13.47 +  | dest_sum (Const("succ",_) $ t) = one :: dest_sum t
   13.48 +  | dest_sum (Const("Arith.add",_) $ t $ u) = dest_sum t @ dest_sum u
   13.49 +  | dest_sum tm = [tm];
   13.50 +
   13.51 +(*Apply the given rewrite (if present) just once*)
   13.52 +fun gen_trans_tac th2 None      = all_tac
   13.53 +  | gen_trans_tac th2 (Some th) = ALLGOALS (rtac (th RS th2));
   13.54 +
   13.55 +(*Use <-> or = depending on the type of t*)
   13.56 +fun mk_eq_iff(t,u) =
   13.57 +  if fastype_of t = iT then FOLogic.mk_eq(t,u)
   13.58 +                       else FOLogic.mk_iff(t,u);
   13.59 +
   13.60 +
   13.61 +fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
   13.62 +
   13.63 +fun prove_conv name tacs sg hyps (t,u) =
   13.64 +  if t aconv u then None
   13.65 +  else
   13.66 +  let val ct = add_chyps hyps
   13.67 +                  (cterm_of sg (FOLogic.mk_Trueprop (mk_eq_iff(t, u))))
   13.68 +  in Some
   13.69 +      (hyps MRS 
   13.70 +       (prove_goalw_cterm_nocheck [] ct 
   13.71 +	(fn prems => cut_facts_tac prems 1 :: tacs)))
   13.72 +      handle ERROR => 
   13.73 +	(warning 
   13.74 +	 ("Cancellation failed: no typing information? (" ^ name ^ ")"); 
   13.75 +	 None)
   13.76 +  end;
   13.77 +
   13.78 +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   13.79 +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
   13.80 +                      (s, TypeInfer.anyT ["logic"]);
   13.81 +val prep_pats = map prep_pat;
   13.82 +
   13.83 +
   13.84 +(*** Use CancelNumerals simproc without binary numerals, 
   13.85 +     just for cancellation ***)
   13.86 +
   13.87 +val mk_times = mk_binop_i "Arith.mult";
   13.88 +
   13.89 +fun mk_prod [] = one
   13.90 +  | mk_prod [t] = t
   13.91 +  | mk_prod (t :: ts) = if t = one then mk_prod ts
   13.92 +                        else mk_times (t, mk_prod ts);
   13.93 +
   13.94 +val dest_times = FOLogic.dest_bin "Arith.mult" iT;
   13.95 +
   13.96 +fun dest_prod t =
   13.97 +      let val (t,u) = dest_times t
   13.98 +      in  dest_prod t @ dest_prod u  end
   13.99 +      handle TERM _ => [t];
  13.100 +
  13.101 +(*Dummy version: the only arguments are 0 and 1*)
  13.102 +fun mk_coeff (0, t) = zero
  13.103 +  | mk_coeff (1, t) = t
  13.104 +  | mk_coeff _       = raise TERM("mk_coeff", []);
  13.105 +
  13.106 +(*Dummy version: the "coefficient" is always 1.
  13.107 +  In the result, the factors are sorted terms*)
  13.108 +fun dest_coeff t = (1, mk_prod (sort Term.term_ord (dest_prod t)));
  13.109 +
  13.110 +(*Find first coefficient-term THAT MATCHES u*)
  13.111 +fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
  13.112 +  | find_first_coeff past u (t::terms) =
  13.113 +        let val (n,u') = dest_coeff t
  13.114 +        in  if u aconv u' then (n, rev past @ terms)
  13.115 +                          else find_first_coeff (t::past) u terms
  13.116 +        end
  13.117 +        handle TERM _ => find_first_coeff (t::past) u terms;
  13.118 +
  13.119 +
  13.120 +(*Simplify #1*n and n*#1 to n*)
  13.121 +val add_0s = [add_0_natify, add_0_right_natify];
  13.122 +val add_succs = [add_succ, add_succ_right];
  13.123 +val mult_1s = [mult_1_natify, mult_1_right_natify];
  13.124 +val tc_rules = [natify_in_nat, add_type, diff_type, mult_type];
  13.125 +val natifys = [natify_0, natify_ident, add_natify1, add_natify2,
  13.126 +               add_natify1, add_natify2, diff_natify1, diff_natify2];
  13.127 +
  13.128 +(*Final simplification: cancel + and **)
  13.129 +fun simplify_meta_eq rules =
  13.130 +    mk_meta_eq o
  13.131 +    simplify (FOL_ss addeqcongs[eq_cong2,iff_cong2] 
  13.132 +                     delsimps iff_simps (*these could erase the whole rule!*)
  13.133 +		     addsimps rules)
  13.134 +
  13.135 +val final_rules = add_0s @ mult_1s @ [mult_0, mult_0_right];
  13.136 +
  13.137 +structure CancelNumeralsCommon =
  13.138 +  struct
  13.139 +  val mk_sum            = mk_sum
  13.140 +  val dest_sum          = dest_sum
  13.141 +  val mk_coeff          = mk_coeff
  13.142 +  val dest_coeff        = dest_coeff
  13.143 +  val find_first_coeff  = find_first_coeff []
  13.144 +  val norm_tac_ss1 = ZF_ss addsimps add_0s@add_succs@mult_1s@add_ac
  13.145 +  val norm_tac_ss2 = ZF_ss addsimps add_ac@mult_ac@tc_rules@natifys
  13.146 +  val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
  13.147 +                 THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
  13.148 +  val numeral_simp_tac_ss = ZF_ss addsimps add_0s@tc_rules@natifys
  13.149 +  val numeral_simp_tac  = ALLGOALS (asm_simp_tac numeral_simp_tac_ss)
  13.150 +  val simplify_meta_eq  = simplify_meta_eq final_rules
  13.151 +  end;
  13.152 +
  13.153 +
  13.154 +structure EqCancelNumerals = CancelNumeralsFun
  13.155 + (open CancelNumeralsCommon
  13.156 +  val prove_conv = prove_conv "nateq_cancel_numerals"
  13.157 +  val mk_bal   = FOLogic.mk_eq
  13.158 +  val dest_bal = FOLogic.dest_bin "op =" iT
  13.159 +  val bal_add1 = eq_add_iff RS iff_trans
  13.160 +  val bal_add2 = eq_add_iff RS iff_trans
  13.161 +  val trans_tac = gen_trans_tac iff_trans
  13.162 +);
  13.163 +
  13.164 +structure LessCancelNumerals = CancelNumeralsFun
  13.165 + (open CancelNumeralsCommon
  13.166 +  val prove_conv = prove_conv "natless_cancel_numerals"
  13.167 +  val mk_bal   = mk_binrel_i "Ordinal.op <"
  13.168 +  val dest_bal = FOLogic.dest_bin "Ordinal.op <" iT
  13.169 +  val bal_add1 = less_add_iff RS iff_trans
  13.170 +  val bal_add2 = less_add_iff RS iff_trans
  13.171 +  val trans_tac = gen_trans_tac iff_trans
  13.172 +);
  13.173 +
  13.174 +structure DiffCancelNumerals = CancelNumeralsFun
  13.175 + (open CancelNumeralsCommon
  13.176 +  val prove_conv = prove_conv "natdiff_cancel_numerals"
  13.177 +  val mk_bal   = mk_binop_i "Arith.diff"
  13.178 +  val dest_bal = FOLogic.dest_bin "Arith.diff" iT
  13.179 +  val bal_add1 = diff_add_eq RS trans
  13.180 +  val bal_add2 = diff_add_eq RS trans
  13.181 +  val trans_tac = gen_trans_tac trans
  13.182 +);
  13.183 +
  13.184 +
  13.185 +val nat_cancel =
  13.186 +      map prep_simproc
  13.187 +       [("nateq_cancel_numerals",
  13.188 +	 prep_pats ["l #+ m = n", "l = m #+ n",
  13.189 +		    "l #* m = n", "l = m #* n",
  13.190 +		    "succ(m) = n", "m = succ(n)"],
  13.191 +	 EqCancelNumerals.proc),
  13.192 +	("natless_cancel_numerals",
  13.193 +	 prep_pats ["l #+ m < n", "l < m #+ n",
  13.194 +		    "l #* m < n", "l < m #* n",
  13.195 +		    "succ(m) < n", "m < succ(n)"],
  13.196 +	 LessCancelNumerals.proc),
  13.197 +	("natdiff_cancel_numerals",
  13.198 +	 prep_pats ["(l #+ m) #- n", "l #- (m #+ n)",
  13.199 +		    "(l #* m) #- n", "l #- (m #* n)",
  13.200 +		    "succ(m) #- n", "m #- succ(n)"],
  13.201 +	 DiffCancelNumerals.proc)];
  13.202 +
  13.203 +end;
  13.204 +
  13.205 +(*examples:
  13.206 +print_depth 22;
  13.207 +set timing;
  13.208 +set trace_simp;
  13.209 +fun test s = (Goal s; by (Asm_simp_tac 1));
  13.210 +
  13.211 +test "x #+ y = x #+ z";
  13.212 +test "y #+ x = x #+ z";
  13.213 +test "x #+ y #+ z = x #+ z";
  13.214 +test "y #+ (z #+ x) = z #+ x";
  13.215 +test "x #+ y #+ z = (z #+ y) #+ (x #+ w)";
  13.216 +test "x#*y #+ z = (z #+ y) #+ (y#*x #+ w)";
  13.217 +
  13.218 +test "x #+ succ(y) = x #+ z";
  13.219 +test "x #+ succ(y) = succ(z #+ x)";
  13.220 +test "succ(x) #+ succ(y) #+ z = succ(z #+ y) #+ succ(x #+ w)";
  13.221 +
  13.222 +test "(x #+ y) #- (x #+ z) = w";
  13.223 +test "(y #+ x) #- (x #+ z) = dd";
  13.224 +test "(x #+ y #+ z) #- (x #+ z) = dd";
  13.225 +test "(y #+ (z #+ x)) #- (z #+ x) = dd";
  13.226 +test "(x #+ y #+ z) #- ((z #+ y) #+ (x #+ w)) = dd";
  13.227 +test "(x#*y #+ z) #- ((z #+ y) #+ (y#*x #+ w)) = dd";
  13.228 +
  13.229 +(*BAD occurrence of natify*)
  13.230 +test "(x #+ succ(y)) #- (x #+ z) = dd";
  13.231 +
  13.232 +test "x #* y2 #+ y #* x2 = y #* x2 #+ x #* y2";
  13.233 +
  13.234 +test "(x #+ succ(y)) #- (succ(z #+ x)) = dd";
  13.235 +test "(succ(x) #+ succ(y) #+ z) #- (succ(z #+ y) #+ succ(x #+ w)) = dd";
  13.236 +
  13.237 +(*use of typing information*)
  13.238 +test "x : nat ==> x #+ y = x";
  13.239 +test "x : nat --> x #+ y = x";
  13.240 +test "x : nat ==> x #+ y < x";
  13.241 +test "x : nat ==> x < y#+x";
  13.242 +
  13.243 +(*fails: no typing information isn't visible*)
  13.244 +test "x #+ y = x";
  13.245 +
  13.246 +test "x #+ y < x #+ z";
  13.247 +test "y #+ x < x #+ z";
  13.248 +test "x #+ y #+ z < x #+ z";
  13.249 +test "y #+ z #+ x < x #+ z";
  13.250 +test "y #+ (z #+ x) < z #+ x";
  13.251 +test "x #+ y #+ z < (z #+ y) #+ (x #+ w)";
  13.252 +test "x#*y #+ z < (z #+ y) #+ (y#*x #+ w)";
  13.253 +
  13.254 +test "x #+ succ(y) < x #+ z";
  13.255 +test "x #+ succ(y) < succ(z #+ x)";
  13.256 +test "succ(x) #+ succ(y) #+ z < succ(z #+ y) #+ succ(x #+ w)";
  13.257 +
  13.258 +test "x #+ succ(y) le succ(z #+ x)";
  13.259 +*)
    14.1 --- a/src/ZF/ex/BinEx.ML	Mon Aug 07 10:29:04 2000 +0200
    14.2 +++ b/src/ZF/ex/BinEx.ML	Mon Aug 07 10:29:54 2000 +0200
    14.3 @@ -26,12 +26,12 @@
    14.4  by (Simp_tac 1);    (*300 msec*)
    14.5  result();
    14.6  
    14.7 -Goal "$~ #65745 = #-65745";
    14.8 +Goal "$- #65745 = #-65745";
    14.9  by (Simp_tac 1);    (*80 msec*)
   14.10  result();
   14.11  
   14.12  (* negation of ~54321 *)
   14.13 -Goal "$~ #-54321 = #54321";
   14.14 +Goal "$- #-54321 = #54321";
   14.15  by (Simp_tac 1);    (*90 msec*)
   14.16  result();
   14.17  
    15.1 --- a/src/ZF/ex/Limit.ML	Mon Aug 07 10:29:04 2000 +0200
    15.2 +++ b/src/ZF/ex/Limit.ML	Mon Aug 07 10:29:54 2000 +0200
    15.3 @@ -1345,13 +1345,8 @@
    15.4  by (asm_simp_tac (simpset() addsimps[diff_self_eq_0]) 1);
    15.5  qed "e_less_eq";
    15.6   
    15.7 -(* ARITH_CONV proves the following in HOL. Would like something similar 
    15.8 -   in Isabelle/ZF. *)
    15.9 -
   15.10  Goal "succ(m#+n)#-m = succ(natify(n))";
   15.11 -by (asm_simp_tac
   15.12 -    (simpset() delsimps [add_succ_right]
   15.13 -	       addsimps [add_succ_right RS sym, diff_add_inverse]) 1);
   15.14 +by (Asm_simp_tac 1);
   15.15  val lemma_succ_sub = result();
   15.16  
   15.17  Goalw [e_less_def]
   15.18 @@ -1364,7 +1359,7 @@
   15.19  qed "add1";
   15.20  
   15.21  Goal "[| m le n; n: nat |] ==> EX k: nat. n = m #+ k";
   15.22 -by (dtac less_imp_Suc_add 1);
   15.23 +by (dtac less_imp_succ_add 1);
   15.24  by Auto_tac;  
   15.25  val lemma_le_exists = result();
   15.26  
   15.27 @@ -1725,7 +1720,7 @@
   15.28  by (auto_tac (claset() addIs [e_gr_e_less_split_add], simpset()));
   15.29  qed "eps_split_add_right_rev";
   15.30  
   15.31 -(* Arithmetic, little support in Isabelle/ZF. *)
   15.32 +(* Arithmetic *)
   15.33  
   15.34  val [prem1,prem2,prem3,prem4] = Goal
   15.35      "[| n le k; k le m;  \
   15.36 @@ -1734,13 +1729,12 @@
   15.37  by (rtac (prem1 RS le_exists) 1);
   15.38  by (simp_tac (simpset() addsimps [prem2 RS lt_nat_in_nat, prem4]) 2);
   15.39  by (rtac ([prem1,prem2] MRS le_trans RS le_exists) 1);
   15.40 +by (rtac prem4 2);
   15.41  by (rtac prem3 1);
   15.42  by (assume_tac 2);
   15.43  by (assume_tac 2);
   15.44  by (cut_facts_tac [prem1,prem2] 1);
   15.45 -by (Asm_full_simp_tac 1);
   15.46 -by (etac add_le_elim1 1);
   15.47 -by (REPEAT (ares_tac prems 1));
   15.48 +by Auto_tac;
   15.49  qed "le_exists_lemma";
   15.50  
   15.51  Goal  (* eps_split_left_le *)
    16.1 --- a/src/ZF/ex/Mutil.ML	Mon Aug 07 10:29:04 2000 +0200
    16.2 +++ b/src/ZF/ex/Mutil.ML	Mon Aug 07 10:29:54 2000 +0200
    16.3 @@ -117,22 +117,22 @@
    16.4                      addEs [mem_irrefl]) 1);
    16.5  qed "dominoes_tile_matrix";
    16.6  
    16.7 +Goal "[| x=y; x<y |] ==> P";
    16.8 +by Auto_tac;
    16.9 +qed "eq_lt_E";
   16.10  
   16.11 -Goal "[| m: nat;  n: nat;  \
   16.12 -\                   t = (succ(m)#+succ(m))*(succ(n)#+succ(n));  \
   16.13 -\                   t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] ==> \
   16.14 -\                t' ~: tiling(domino)";
   16.15 +Goal "[| m: nat;  n: nat;                                 \
   16.16 +\        t = (succ(m)#+succ(m))*(succ(n)#+succ(n));       \
   16.17 +\        t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] \
   16.18 +\     ==> t' ~: tiling(domino)";
   16.19  by (rtac notI 1);
   16.20  by (dtac tiling_domino_0_1 1);
   16.21 -by (subgoal_tac "|evnodd(t',0)| < |evnodd(t',1)|" 1);
   16.22 -by (asm_full_simp_tac (simpset() addsimps [lt_not_refl]) 1);
   16.23 +by (eres_inst_tac [("x", "|?A|")] eq_lt_E 1);
   16.24  by (subgoal_tac "t : tiling(domino)" 1);
   16.25  (*Requires a small simpset that won't move the succ applications*)
   16.26  by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type, 
   16.27                                    dominoes_tile_matrix]) 2);
   16.28 -by (subgoal_tac "(m#+m)#+(n#+n) = (m#+n)#+(m#+n)" 1);
   16.29 -by (asm_simp_tac (simpset() addsimps add_ac) 2);
   16.30 -by (asm_lr_simp_tac 
   16.31 +by (asm_full_simp_tac 
   16.32      (simpset() addsimps [evnodd_Diff, mod2_add_self,
   16.33                          mod2_succ_succ, tiling_domino_0_1 RS sym]) 1);
   16.34  by (rtac lt_trans 1);
    17.1 --- a/src/ZF/ex/Primes.thy	Mon Aug 07 10:29:04 2000 +0200
    17.2 +++ b/src/ZF/ex/Primes.thy	Mon Aug 07 10:29:54 2000 +0200
    17.3 @@ -6,7 +6,7 @@
    17.4  The "divides" relation, the greatest common divisor and Euclid's algorithm
    17.5  *)
    17.6  
    17.7 -Primes = Arith +
    17.8 +Primes = Main +
    17.9  consts
   17.10    dvd     :: [i,i]=>o              (infixl 70) 
   17.11    gcd     :: [i,i,i]=>o            (* great common divisor *)