conversion of ZF/Integ/{Int,Bin} to Isar scripts
authorpaulson
Sat Sep 07 22:04:28 2002 +0200 (2002-09-07)
changeset 13560d9651081578b
parent 13559 51c3ac47d127
child 13561 daefa3ac8933
conversion of ZF/Integ/{Int,Bin} to Isar scripts
src/ZF/Integ/Bin.ML
src/ZF/Integ/Bin.thy
src/ZF/Integ/Int.ML
src/ZF/Integ/Int.thy
src/ZF/Integ/IntDiv.thy
src/ZF/Integ/int_arith.ML
src/ZF/IsaMakefile
     1.1 --- a/src/ZF/Integ/Bin.ML	Thu Sep 05 14:03:03 2002 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,612 +0,0 @@
     1.4 -(*  Title:      ZF/ex/Bin.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1994  University of Cambridge
     1.8 -
     1.9 -Arithmetic on binary integers.
    1.10 -*)
    1.11 -
    1.12 -
    1.13 -Addsimps bin.intrs;
    1.14 -AddTCs bin.intrs;
    1.15 -
    1.16 -Goal "NCons(Pls,0) = Pls";
    1.17 -by (Asm_simp_tac 1);
    1.18 -qed "NCons_Pls_0";
    1.19 -
    1.20 -Goal "NCons(Pls,1) = Pls BIT 1";
    1.21 -by (Asm_simp_tac 1);
    1.22 -qed "NCons_Pls_1";
    1.23 -
    1.24 -Goal "NCons(Min,0) = Min BIT 0";
    1.25 -by (Asm_simp_tac 1);
    1.26 -qed "NCons_Min_0";
    1.27 -
    1.28 -Goal "NCons(Min,1) = Min";
    1.29 -by (Asm_simp_tac 1);
    1.30 -qed "NCons_Min_1";
    1.31 -
    1.32 -Goal "NCons(w BIT x,b) = w BIT x BIT b";
    1.33 -by (asm_simp_tac (simpset() addsimps bin.case_eqns) 1);
    1.34 -qed "NCons_BIT";
    1.35 -
    1.36 -bind_thms ("NCons_simps",
    1.37 - [NCons_Pls_0, NCons_Pls_1,
    1.38 -  NCons_Min_0, NCons_Min_1,
    1.39 -  NCons_BIT]);
    1.40 -Addsimps NCons_simps;
    1.41 -
    1.42 -
    1.43 -(** Type checking **)
    1.44 -
    1.45 -Goal "w: bin ==> integ_of(w) : int";
    1.46 -by (induct_tac "w" 1);
    1.47 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [bool_into_nat])));
    1.48 -qed "integ_of_type";
    1.49 -AddTCs [integ_of_type];
    1.50 -
    1.51 -Goal "[| w: bin; b: bool |] ==> NCons(w,b) : bin";
    1.52 -by (induct_tac "w" 1);
    1.53 -by Auto_tac;
    1.54 -qed "NCons_type";
    1.55 -AddTCs [NCons_type];
    1.56 -
    1.57 -Goal "w: bin ==> bin_succ(w) : bin";
    1.58 -by (induct_tac "w" 1);
    1.59 -by Auto_tac;
    1.60 -qed "bin_succ_type";
    1.61 -AddTCs [bin_succ_type];
    1.62 -
    1.63 -Goal "w: bin ==> bin_pred(w) : bin";
    1.64 -by (induct_tac "w" 1);
    1.65 -by Auto_tac;
    1.66 -qed "bin_pred_type";
    1.67 -AddTCs [bin_pred_type];
    1.68 -
    1.69 -Goal "w: bin ==> bin_minus(w) : bin";
    1.70 -by (induct_tac "w" 1);
    1.71 -by Auto_tac;
    1.72 -qed "bin_minus_type";
    1.73 -AddTCs [bin_minus_type];
    1.74 -
    1.75 -(*This proof is complicated by the mutual recursion*)
    1.76 -Goalw [bin_add_def] "v: bin ==> ALL w: bin. bin_add(v,w) : bin";
    1.77 -by (induct_tac "v" 1);
    1.78 -by (rtac ballI 3);
    1.79 -by (rename_tac "w'" 3);
    1.80 -by (induct_tac "w'" 3);
    1.81 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [NCons_type])));
    1.82 -qed_spec_mp "bin_add_type";
    1.83 -AddTCs [bin_add_type];
    1.84 -
    1.85 -Goal "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
    1.86 -by (induct_tac "v" 1);
    1.87 -by Auto_tac;
    1.88 -qed "bin_mult_type";
    1.89 -AddTCs [bin_mult_type];
    1.90 -
    1.91 -
    1.92 -(**** The carry/borrow functions, bin_succ and bin_pred ****)
    1.93 -
    1.94 -(*NCons preserves the integer value of its argument*)
    1.95 -Goal "[| w: bin; b: bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)";
    1.96 -by (etac bin.elim 1);
    1.97 -by (Asm_simp_tac 3);
    1.98 -by (ALLGOALS (etac boolE));
    1.99 -by (ALLGOALS Asm_simp_tac);
   1.100 -qed "integ_of_NCons";
   1.101 -
   1.102 -Addsimps [integ_of_NCons];
   1.103 -
   1.104 -Goal "w: bin ==> integ_of(bin_succ(w)) = $#1 $+ integ_of(w)";
   1.105 -by (etac bin.induct 1);
   1.106 -by (Simp_tac 1);
   1.107 -by (Simp_tac 1);
   1.108 -by (etac boolE 1);
   1.109 -by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
   1.110 -qed "integ_of_succ";
   1.111 -
   1.112 -Goal "w: bin ==> integ_of(bin_pred(w)) = $- ($#1) $+ integ_of(w)";
   1.113 -by (etac bin.induct 1);
   1.114 -by (Simp_tac 1);
   1.115 -by (Simp_tac 1);
   1.116 -by (etac boolE 1);
   1.117 -by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
   1.118 -qed "integ_of_pred";
   1.119 -
   1.120 -Addsimps [integ_of_succ, integ_of_pred];
   1.121 -
   1.122 -
   1.123 -(*** bin_minus: (unary!) negation of binary integers ***)
   1.124 -
   1.125 -Goal "w: bin ==> integ_of(bin_minus(w)) = $- integ_of(w)";
   1.126 -by (etac bin.induct 1);
   1.127 -by (Simp_tac 1);
   1.128 -by (Simp_tac 1);
   1.129 -by (etac boolE 1);
   1.130 -by (ALLGOALS 
   1.131 -    (asm_simp_tac (simpset() addsimps zadd_ac@[zminus_zadd_distrib])));
   1.132 -qed "integ_of_minus";
   1.133 -
   1.134 -
   1.135 -(*** bin_add: binary addition ***)
   1.136 -
   1.137 -Goalw [bin_add_def] "w: bin ==> bin_add(Pls,w) = w";
   1.138 -by (Asm_simp_tac 1);
   1.139 -qed "bin_add_Pls";
   1.140 -
   1.141 -Goalw [bin_add_def] "w: bin ==> bin_add(w,Pls) = w";
   1.142 -by (etac bin.induct 1);
   1.143 -by Auto_tac;
   1.144 -qed "bin_add_Pls_right";
   1.145 -
   1.146 -Goalw [bin_add_def] "w: bin ==> bin_add(Min,w) = bin_pred(w)";
   1.147 -by (Asm_simp_tac 1);
   1.148 -qed "bin_add_Min";
   1.149 -
   1.150 -Goalw [bin_add_def] "w: bin ==> bin_add(w,Min) = bin_pred(w)";
   1.151 -by (etac bin.induct 1);
   1.152 -by Auto_tac;
   1.153 -qed "bin_add_Min_right";
   1.154 -
   1.155 -Goalw [bin_add_def] "bin_add(v BIT x,Pls) = v BIT x";
   1.156 -by (Simp_tac 1);
   1.157 -qed "bin_add_BIT_Pls";
   1.158 -
   1.159 -Goalw [bin_add_def] "bin_add(v BIT x,Min) = bin_pred(v BIT x)";
   1.160 -by (Simp_tac 1);
   1.161 -qed "bin_add_BIT_Min";
   1.162 -
   1.163 -Goalw [bin_add_def] "[| w: bin;  y: bool |]              \
   1.164 -\     ==> bin_add(v BIT x, w BIT y) = \
   1.165 -\         NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)";
   1.166 -by (Asm_simp_tac 1);
   1.167 -qed "bin_add_BIT_BIT";
   1.168 -
   1.169 -Addsimps [bin_add_Pls, bin_add_Min, bin_add_BIT_Pls,
   1.170 -	  bin_add_BIT_Min, bin_add_BIT_BIT,
   1.171 -	  integ_of_succ, integ_of_pred];
   1.172 -
   1.173 -Goal "v: bin ==> \
   1.174 -\         ALL w: bin. integ_of(bin_add(v,w)) = integ_of(v) $+ integ_of(w)";
   1.175 -by (etac bin.induct 1);
   1.176 -by (Simp_tac 1);
   1.177 -by (Simp_tac 1);
   1.178 -by (rtac ballI 1);
   1.179 -by (induct_tac "wa" 1);
   1.180 -by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
   1.181 -qed_spec_mp "integ_of_add";
   1.182 -
   1.183 -(*Subtraction*)
   1.184 -Goalw [zdiff_def]
   1.185 -     "[| v: bin;  w: bin |]   \
   1.186 -\     ==> integ_of(v) $- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))";
   1.187 -by (asm_simp_tac (simpset() addsimps [integ_of_add, integ_of_minus]) 1);
   1.188 -qed "diff_integ_of_eq";
   1.189 -
   1.190 -
   1.191 -(*** bin_mult: binary multiplication ***)
   1.192 -
   1.193 -Goal "[| v: bin;  w: bin |]   \
   1.194 -\     ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)";
   1.195 -by (induct_tac "v" 1);
   1.196 -by (Asm_simp_tac 1);
   1.197 -by (asm_simp_tac (simpset() addsimps [integ_of_minus]) 1);
   1.198 -by (etac boolE 1);
   1.199 -by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 2);
   1.200 -by (asm_simp_tac (simpset() addsimps [integ_of_add,
   1.201 -				      zadd_zmult_distrib] @ zadd_ac) 1);
   1.202 -qed "integ_of_mult";
   1.203 -
   1.204 -(**** Computations ****)
   1.205 -
   1.206 -(** extra rules for bin_succ, bin_pred **)
   1.207 -
   1.208 -Goal "bin_succ(w BIT 1) = bin_succ(w) BIT 0";
   1.209 -by (Simp_tac 1);
   1.210 -qed "bin_succ_1";
   1.211 -
   1.212 -Goal "bin_succ(w BIT 0) = NCons(w,1)";
   1.213 -by (Simp_tac 1);
   1.214 -qed "bin_succ_0";
   1.215 -
   1.216 -Goal "bin_pred(w BIT 1) = NCons(w,0)";
   1.217 -by (Simp_tac 1);
   1.218 -qed "bin_pred_1";
   1.219 -
   1.220 -Goal "bin_pred(w BIT 0) = bin_pred(w) BIT 1";
   1.221 -by (Simp_tac 1);
   1.222 -qed "bin_pred_0";
   1.223 -
   1.224 -(** extra rules for bin_minus **)
   1.225 -
   1.226 -Goal "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))";
   1.227 -by (Simp_tac 1);
   1.228 -qed "bin_minus_1";
   1.229 -
   1.230 -Goal "bin_minus(w BIT 0) = bin_minus(w) BIT 0";
   1.231 -by (Simp_tac 1);
   1.232 -qed "bin_minus_0";
   1.233 -
   1.234 -(** extra rules for bin_add **)
   1.235 -
   1.236 -Goal "w: bin ==> bin_add(v BIT 1, w BIT 1) = \
   1.237 -\                    NCons(bin_add(v, bin_succ(w)), 0)";
   1.238 -by (Asm_simp_tac 1);
   1.239 -qed "bin_add_BIT_11";
   1.240 -
   1.241 -Goal "w: bin ==> bin_add(v BIT 1, w BIT 0) =  \
   1.242 -\                    NCons(bin_add(v,w), 1)";
   1.243 -by (Asm_simp_tac 1);
   1.244 -qed "bin_add_BIT_10";
   1.245 -
   1.246 -Goal "[| w: bin;  y: bool |] \
   1.247 -\     ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)";
   1.248 -by (Asm_simp_tac 1);
   1.249 -qed "bin_add_BIT_0";
   1.250 -
   1.251 -(** extra rules for bin_mult **)
   1.252 -
   1.253 -Goal "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)";
   1.254 -by (Simp_tac 1);
   1.255 -qed "bin_mult_1";
   1.256 -
   1.257 -Goal "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)";
   1.258 -by (Simp_tac 1);
   1.259 -qed "bin_mult_0";
   1.260 -
   1.261 -
   1.262 -(** Simplification rules with integer constants **)
   1.263 -
   1.264 -Goal "$#0 = #0";
   1.265 -by (Simp_tac 1);
   1.266 -qed "int_of_0";
   1.267 -
   1.268 -Goal "$# succ(n) = #1 $+ $#n";
   1.269 -by (simp_tac (simpset() addsimps [int_of_add RS sym, natify_succ]) 1);
   1.270 -qed "int_of_succ";
   1.271 -
   1.272 -Goal "$- #0 = #0";
   1.273 -by (Simp_tac 1);
   1.274 -qed "zminus_0";
   1.275 -
   1.276 -Addsimps [zminus_0];
   1.277 -
   1.278 -Goal "#0 $+ z = intify(z)";
   1.279 -by (Simp_tac 1);
   1.280 -qed "zadd_0_intify";
   1.281 -
   1.282 -Goal "z $+ #0 = intify(z)";
   1.283 -by (Simp_tac 1);
   1.284 -qed "zadd_0_right_intify";
   1.285 -
   1.286 -Addsimps [zadd_0_intify, zadd_0_right_intify];
   1.287 -
   1.288 -Goal "#1 $* z = intify(z)";
   1.289 -by (Simp_tac 1);
   1.290 -qed "zmult_1_intify";
   1.291 -
   1.292 -Goal "z $* #1 = intify(z)";
   1.293 -by (stac zmult_commute 1);
   1.294 -by (Simp_tac 1);
   1.295 -qed "zmult_1_right_intify";
   1.296 -
   1.297 -Addsimps [zmult_1_intify, zmult_1_right_intify];
   1.298 -
   1.299 -Goal "#0 $* z = #0";
   1.300 -by (Simp_tac 1);
   1.301 -qed "zmult_0";
   1.302 -
   1.303 -Goal "z $* #0 = #0";
   1.304 -by (stac zmult_commute 1);
   1.305 -by (Simp_tac 1);
   1.306 -qed "zmult_0_right";
   1.307 -
   1.308 -Addsimps [zmult_0, zmult_0_right];
   1.309 -
   1.310 -Goal "#-1 $* z = $-z";
   1.311 -by (simp_tac (simpset() addsimps zcompare_rls) 1);
   1.312 -qed "zmult_minus1";
   1.313 -
   1.314 -Goal "z $* #-1 = $-z";
   1.315 -by (stac zmult_commute 1);
   1.316 -by (rtac zmult_minus1 1);
   1.317 -qed "zmult_minus1_right";
   1.318 -
   1.319 -Addsimps [zmult_minus1, zmult_minus1_right];
   1.320 -
   1.321 -
   1.322 -(*** Simplification rules for comparison of binary numbers (N Voelker) ***)
   1.323 -
   1.324 -(** Equals (=) **)
   1.325 -
   1.326 -Goalw [iszero_def]
   1.327 -     "[| v: bin;  w: bin |]   \
   1.328 -\     ==> ((integ_of(v)) = integ_of(w)) <-> \
   1.329 -\         iszero (integ_of (bin_add (v, bin_minus(w))))"; 
   1.330 -by (asm_simp_tac (simpset() addsimps
   1.331 -              (zcompare_rls @ [integ_of_add, integ_of_minus])) 1); 
   1.332 -qed "eq_integ_of_eq"; 
   1.333 -
   1.334 -Goalw [iszero_def] "iszero (integ_of(Pls))"; 
   1.335 -by (Simp_tac 1); 
   1.336 -qed "iszero_integ_of_Pls";
   1.337 -
   1.338 -
   1.339 -Goalw [iszero_def] "~ iszero (integ_of(Min))"; 
   1.340 -by (simp_tac (simpset() addsimps [zminus_equation]) 1);
   1.341 -qed "nonzero_integ_of_Min"; 
   1.342 -
   1.343 -Goalw [iszero_def]
   1.344 -     "[| w: bin; x: bool |] \
   1.345 -\     ==> iszero (integ_of (w BIT x)) <-> (x=0 & iszero (integ_of(w)))"; 
   1.346 -by (Simp_tac 1);
   1.347 -by (subgoal_tac "integ_of(w) : int" 1);
   1.348 -by (Asm_simp_tac 2);
   1.349 -by (dtac int_cases 1);
   1.350 -by (auto_tac (claset() addSEs [boolE], 
   1.351 -              simpset() addsimps [int_of_add RS sym]));  
   1.352 -by (ALLGOALS (asm_full_simp_tac 
   1.353 -	      (simpset() addsimps zcompare_rls @ 
   1.354 -			  [zminus_zadd_distrib RS sym, int_of_add RS sym])));
   1.355 -by (subgoal_tac "znegative ($- $# succ(n)) <-> znegative ($# succ(n))" 1);
   1.356 -by (Asm_simp_tac 2);
   1.357 -by (Full_simp_tac 1);
   1.358 -qed "iszero_integ_of_BIT"; 
   1.359 -
   1.360 -Goal "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"; 
   1.361 -by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1); 
   1.362 -qed "iszero_integ_of_0"; 
   1.363 -
   1.364 -Goal "w: bin ==> ~ iszero (integ_of (w BIT 1))"; 
   1.365 -by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1); 
   1.366 -qed "iszero_integ_of_1"; 
   1.367 -
   1.368 -
   1.369 -
   1.370 -(** Less-than (<) **)
   1.371 -
   1.372 -Goalw [zless_def,zdiff_def] 
   1.373 -     "[| v: bin;  w: bin |]   \
   1.374 -\     ==> integ_of(v) $< integ_of(w) \
   1.375 -\         <-> znegative (integ_of (bin_add (v, bin_minus(w))))";
   1.376 -by (asm_simp_tac (simpset() addsimps [integ_of_minus, integ_of_add]) 1);
   1.377 -qed "less_integ_of_eq_neg"; 
   1.378 -
   1.379 -Goal "~ znegative (integ_of(Pls))"; 
   1.380 -by (Simp_tac 1); 
   1.381 -qed "not_neg_integ_of_Pls"; 
   1.382 -
   1.383 -Goal "znegative (integ_of(Min))"; 
   1.384 -by (Simp_tac 1);
   1.385 -qed "neg_integ_of_Min"; 
   1.386 -
   1.387 -Goal "[| w: bin; x: bool |] \
   1.388 -\     ==> znegative (integ_of (w BIT x)) <-> znegative (integ_of(w))"; 
   1.389 -by (Asm_simp_tac 1); 
   1.390 -by (subgoal_tac "integ_of(w) : int" 1);
   1.391 -by (Asm_simp_tac 2);
   1.392 -by (dtac int_cases 1);
   1.393 -by (auto_tac (claset() addSEs [boolE], 
   1.394 -              simpset() addsimps [int_of_add RS sym] @ zcompare_rls));  
   1.395 -by (ALLGOALS (asm_full_simp_tac 
   1.396 -	      (simpset() addsimps [zminus_zadd_distrib RS sym, zdiff_def,
   1.397 -				   int_of_add RS sym])));
   1.398 -by (subgoal_tac "$#1 $- $# succ(succ(n #+ n)) = $- $# succ(n #+ n)" 1);
   1.399 -by (asm_full_simp_tac (simpset() addsimps [zdiff_def])1);
   1.400 -by (asm_simp_tac (simpset() addsimps [equation_zminus, int_of_diff RS sym])1);
   1.401 -qed "neg_integ_of_BIT"; 
   1.402 -
   1.403 -(** Less-than-or-equals (<=) **)
   1.404 -
   1.405 -Goal "(integ_of(x) $<= (integ_of(w))) <-> ~ (integ_of(w) $< (integ_of(x)))";
   1.406 -by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
   1.407 -qed "le_integ_of_eq_not_less"; 
   1.408 -
   1.409 -
   1.410 -(*Delete the original rewrites, with their clumsy conditional expressions*)
   1.411 -Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
   1.412 -          NCons_Pls, NCons_Min, bin_adder_BIT, bin_mult_BIT];
   1.413 -
   1.414 -(*Hide the binary representation of integer constants*)
   1.415 -Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
   1.416 -
   1.417 -
   1.418 -bind_thms ("bin_arith_extra_simps",
   1.419 -    [integ_of_add RS sym,   (*invoke bin_add*)
   1.420 -     integ_of_minus RS sym, (*invoke bin_minus*)
   1.421 -     integ_of_mult RS sym,  (*invoke bin_mult*)
   1.422 -     bin_succ_1, bin_succ_0, 
   1.423 -     bin_pred_1, bin_pred_0, 
   1.424 -     bin_minus_1, bin_minus_0,  
   1.425 -     bin_add_Pls_right, bin_add_Min_right,
   1.426 -     bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
   1.427 -     diff_integ_of_eq,
   1.428 -     bin_mult_1, bin_mult_0] @ NCons_simps);
   1.429 -
   1.430 -
   1.431 -(*For making a minimal simpset, one must include these default simprules
   1.432 -  of thy.  Also include simp_thms, or at least (~False)=True*)
   1.433 -bind_thms ("bin_arith_simps",
   1.434 -    [bin_pred_Pls, bin_pred_Min,
   1.435 -     bin_succ_Pls, bin_succ_Min,
   1.436 -     bin_add_Pls, bin_add_Min,
   1.437 -     bin_minus_Pls, bin_minus_Min,
   1.438 -     bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps);
   1.439 -
   1.440 -(*Simplification of relational operations*)
   1.441 -bind_thms ("bin_rel_simps",
   1.442 -    [eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min,
   1.443 -     iszero_integ_of_0, iszero_integ_of_1,
   1.444 -     less_integ_of_eq_neg,
   1.445 -     not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT,
   1.446 -     le_integ_of_eq_not_less]);
   1.447 -
   1.448 -Addsimps bin_arith_simps;
   1.449 -Addsimps bin_rel_simps;
   1.450 -
   1.451 -
   1.452 -(** Simplification of arithmetic when nested to the right **)
   1.453 -
   1.454 -Goal "[| v: bin;  w: bin |]   \
   1.455 -\     ==> integ_of(v) $+ (integ_of(w) $+ z) = (integ_of(bin_add(v,w)) $+ z)";
   1.456 -by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
   1.457 -qed "add_integ_of_left";
   1.458 -
   1.459 -Goal "[| v: bin;  w: bin |]   \
   1.460 -\     ==> integ_of(v) $* (integ_of(w) $* z) = (integ_of(bin_mult(v,w)) $* z)";
   1.461 -by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
   1.462 -qed "mult_integ_of_left";
   1.463 -
   1.464 -Goalw [zdiff_def]
   1.465 -    "[| v: bin;  w: bin |]   \
   1.466 -\     ==> integ_of(v) $+ (integ_of(w) $- c) = integ_of(bin_add(v,w)) $- (c)";
   1.467 -by (rtac add_integ_of_left 1);
   1.468 -by Auto_tac;  
   1.469 -qed "add_integ_of_diff1";
   1.470 -
   1.471 -Goal "[| v: bin;  w: bin |]   \
   1.472 -\     ==> integ_of(v) $+ (c $- integ_of(w)) = \
   1.473 -\         integ_of (bin_add (v, bin_minus(w))) $+ (c)";
   1.474 -by (stac (diff_integ_of_eq RS sym) 1);
   1.475 -by (ALLGOALS (asm_simp_tac (simpset() addsimps zdiff_def::zadd_ac)));
   1.476 -qed "add_integ_of_diff2";
   1.477 -
   1.478 -Addsimps [add_integ_of_left, mult_integ_of_left,
   1.479 -	  add_integ_of_diff1, add_integ_of_diff2]; 
   1.480 -
   1.481 -
   1.482 -(** More for integer constants **)
   1.483 -
   1.484 -Addsimps [int_of_0, int_of_succ];
   1.485 -
   1.486 -Goal "#0 $- x = $-x";
   1.487 -by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   1.488 -qed "zdiff0";
   1.489 -
   1.490 -Goal "x $- #0 = intify(x)";
   1.491 -by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   1.492 -qed "zdiff0_right";
   1.493 -
   1.494 -Goal "x $- x = #0";
   1.495 -by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   1.496 -qed "zdiff_self";
   1.497 -
   1.498 -Addsimps [zdiff0, zdiff0_right, zdiff_self];
   1.499 -
   1.500 -Goal "k: int ==> znegative(k) <-> k $< #0";
   1.501 -by (asm_simp_tac (simpset() addsimps [zless_def]) 1);
   1.502 -qed "znegative_iff_zless_0";
   1.503 -
   1.504 -Goal "[| #0 $< k; k: int |] ==> znegative($-k)";
   1.505 -by (asm_full_simp_tac (simpset() addsimps [zless_def]) 1);
   1.506 -qed "zero_zless_imp_znegative_zminus";
   1.507 -
   1.508 -Goal "#0 $<= $# n";
   1.509 -by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, 
   1.510 -                                  znegative_iff_zless_0 RS iff_sym]) 1); 
   1.511 -qed "zero_zle_int_of";
   1.512 -Addsimps [zero_zle_int_of];
   1.513 -
   1.514 -Goal "nat_of(#0) = 0";
   1.515 -by (simp_tac (ZF_ss addsimps [natify_0, int_of_0 RS sym, nat_of_int_of]) 1);
   1.516 -qed "nat_of_0";
   1.517 -Addsimps [nat_of_0];
   1.518 -
   1.519 -Goal "[| z $<= $#0; z: int |] ==> nat_of(z) = 0"; 
   1.520 -by (auto_tac (claset(), 
   1.521 -	      simpset() addsimps [znegative_iff_zless_0 RS iff_sym, 
   1.522 -				  zle_def, zneg_nat_of])); 
   1.523 -val lemma = result();
   1.524 -
   1.525 -Goal "z $<= $#0 ==> nat_of(z) = 0"; 
   1.526 -by (subgoal_tac "nat_of(intify(z)) = 0" 1);
   1.527 -by (rtac lemma 2);
   1.528 -by Auto_tac;  
   1.529 -qed "nat_le_int0";
   1.530 -
   1.531 -Goal "$# n = #0 ==> natify(n) = 0";
   1.532 -by (rtac not_znegative_imp_zero 1);
   1.533 -by Auto_tac;  
   1.534 -qed "int_of_eq_0_imp_natify_eq_0";
   1.535 -
   1.536 -Goalw [nat_of_def, raw_nat_of_def] "nat_of($- $# n) = 0";
   1.537 -by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq], 
   1.538 -              simpset())     delIffs [int_of_eq]));
   1.539 -by (rtac the_equality 1);
   1.540 -by Auto_tac;  
   1.541 -by (blast_tac (claset() addIs [int_of_eq_0_imp_natify_eq_0, sym]) 1); 
   1.542 -qed "nat_of_zminus_int_of";
   1.543 -
   1.544 -Goal "#0 $<= z ==> $# nat_of(z) = intify(z)";
   1.545 -by (rtac not_zneg_nat_of_intify 1);
   1.546 -by (asm_simp_tac (simpset() addsimps [znegative_iff_zless_0, 
   1.547 -                                      not_zless_iff_zle]) 1); 
   1.548 -qed "int_of_nat_of";
   1.549 -
   1.550 -Addsimps [int_of_nat_of, nat_of_zminus_int_of];
   1.551 -
   1.552 -Goal "$# nat_of(z) = (if #0 $<= z then intify(z) else #0)";
   1.553 -by (simp_tac (simpset() addsimps [int_of_nat_of,
   1.554 -                              znegative_iff_zless_0, not_zle_iff_zless]) 1);
   1.555 -qed "int_of_nat_of_if";
   1.556 -
   1.557 -Goal "[| m: nat; z: int |] ==> (m < nat_of(z)) <-> ($#m $< z)";
   1.558 -by (case_tac "znegative(z)" 1);
   1.559 -by (etac (not_zneg_nat_of RS subst) 2);
   1.560 -by (auto_tac (claset() addDs [zless_trans]
   1.561 -		       addSDs [zero_zle_int_of RS zle_zless_trans], 
   1.562 -	      simpset() addsimps [znegative_iff_zless_0])); 
   1.563 -qed "zless_nat_iff_int_zless";
   1.564 -
   1.565 -
   1.566 -(** nat_of and zless **)
   1.567 -
   1.568 -(*An alternative condition is  $#0 <= w  *)
   1.569 -Goal "$#0 $< z ==> (nat_of(w) < nat_of(z)) <-> (w $< z)";
   1.570 -by (rtac iff_trans 1);
   1.571 -by (rtac (zless_int_of RS iff_sym) 1);
   1.572 -by (auto_tac (claset(), 
   1.573 -       simpset() addsimps [int_of_nat_of_if] delsimps [zless_int_of]));  
   1.574 -by (auto_tac (claset() addEs [zless_asym],
   1.575 -              simpset() addsimps [not_zle_iff_zless]));  
   1.576 -by (blast_tac (claset() addIs [zless_zle_trans]) 1); 
   1.577 -val lemma = result();
   1.578 -
   1.579 -Goal "(nat_of(w) < nat_of(z)) <-> ($#0 $< z & w $< z)";
   1.580 -by (case_tac "$#0 $< z" 1);
   1.581 -by (auto_tac (claset(), 
   1.582 -	      simpset() addsimps [lemma, nat_le_int0, not_zless_iff_zle])); 
   1.583 -qed "zless_nat_conj";
   1.584 -
   1.585 -(*This simprule cannot be added unless we can find a way to make eq_integ_of_eq
   1.586 -  unconditional!
   1.587 -
   1.588 -  (*The condition "True" is a hack to prevent looping.
   1.589 -    Conditional rewrite rules are tried after unconditional ones, so a rule
   1.590 -    like eq_nat_number_of will be tried first to eliminate #mm=#nn. *)
   1.591 -  Goal "True ==> (integ_of(w) = x) <-> (x = integ_of(w))";
   1.592 -  by Auto_tac;  
   1.593 -  qed "integ_of_reorient";
   1.594 -  Addsimps [integ_of_reorient];
   1.595 -*)
   1.596 -
   1.597 -Goal "(integ_of(w) = $- x) <-> ($- x = integ_of(w))";
   1.598 -by Auto_tac;  
   1.599 -qed "integ_of_minus_reorient";
   1.600 -Addsimps [integ_of_minus_reorient];
   1.601 -
   1.602 -Goal "(integ_of(w) = x $+ y) <-> (x $+ y = integ_of(w))";
   1.603 -by Auto_tac;  
   1.604 -qed "integ_of_add_reorient";
   1.605 -Addsimps [integ_of_add_reorient];
   1.606 -
   1.607 -Goal "(integ_of(w) = x $- y) <-> (x $- y = integ_of(w))";
   1.608 -by Auto_tac;  
   1.609 -qed "integ_of_diff_reorient";
   1.610 -Addsimps [integ_of_diff_reorient];
   1.611 -
   1.612 -Goal "(integ_of(w) = x $* y) <-> (x $* y = integ_of(w))";
   1.613 -by Auto_tac;  
   1.614 -qed "integ_of_mult_reorient";
   1.615 -Addsimps [integ_of_mult_reorient];
     2.1 --- a/src/ZF/Integ/Bin.thy	Thu Sep 05 14:03:03 2002 +0200
     2.2 +++ b/src/ZF/Integ/Bin.thy	Sat Sep 07 22:04:28 2002 +0200
     2.3 @@ -3,8 +3,6 @@
     2.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.5      Copyright   1994  University of Cambridge
     2.6  
     2.7 -Arithmetic on binary integers.
     2.8 -
     2.9     The sign Pls stands for an infinite string of leading 0's.
    2.10     The sign Min stands for an infinite string of leading 1's.
    2.11  
    2.12 @@ -16,7 +14,9 @@
    2.13  For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
    2.14  *)
    2.15  
    2.16 -Bin = Int + Datatype +
    2.17 +header{*Arithmetic on Binary Integers*}
    2.18 +
    2.19 +theory Bin = Int + Datatype:
    2.20  
    2.21  consts  bin :: i
    2.22  datatype
    2.23 @@ -25,55 +25,54 @@
    2.24          | Bit ("w: bin", "b: bool")	(infixl "BIT" 90)
    2.25  
    2.26  syntax
    2.27 -  "_Int"           :: xnum => i        ("_")
    2.28 +  "_Int"    :: "xnum => i"        ("_")
    2.29  
    2.30  consts
    2.31 -  integ_of  :: i=>i
    2.32 -  NCons     :: [i,i]=>i
    2.33 -  bin_succ  :: i=>i
    2.34 -  bin_pred  :: i=>i
    2.35 -  bin_minus :: i=>i
    2.36 -  bin_add   :: [i,i]=>i
    2.37 -  bin_adder :: i=>i
    2.38 -  bin_mult  :: [i,i]=>i
    2.39 +  integ_of  :: "i=>i"
    2.40 +  NCons     :: "[i,i]=>i"
    2.41 +  bin_succ  :: "i=>i"
    2.42 +  bin_pred  :: "i=>i"
    2.43 +  bin_minus :: "i=>i"
    2.44 +  bin_adder :: "i=>i"
    2.45 +  bin_mult  :: "[i,i]=>i"
    2.46  
    2.47  primrec
    2.48 -  integ_of_Pls  "integ_of (Pls)     = $# 0"
    2.49 -  integ_of_Min  "integ_of (Min)     = $-($#1)"
    2.50 -  integ_of_BIT  "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)"
    2.51 +  integ_of_Pls:  "integ_of (Pls)     = $# 0"
    2.52 +  integ_of_Min:  "integ_of (Min)     = $-($#1)"
    2.53 +  integ_of_BIT:  "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)"
    2.54  
    2.55      (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
    2.56  
    2.57  primrec (*NCons adds a bit, suppressing leading 0s and 1s*)
    2.58 -  NCons_Pls "NCons (Pls,b)     = cond(b,Pls BIT b,Pls)"
    2.59 -  NCons_Min "NCons (Min,b)     = cond(b,Min,Min BIT b)"
    2.60 -  NCons_BIT "NCons (w BIT c,b) = w BIT c BIT b"
    2.61 +  NCons_Pls: "NCons (Pls,b)     = cond(b,Pls BIT b,Pls)"
    2.62 +  NCons_Min: "NCons (Min,b)     = cond(b,Min,Min BIT b)"
    2.63 +  NCons_BIT: "NCons (w BIT c,b) = w BIT c BIT b"
    2.64  
    2.65  primrec (*successor.  If a BIT, can change a 0 to a 1 without recursion.*)
    2.66 -  bin_succ_Pls  "bin_succ (Pls)     = Pls BIT 1"
    2.67 -  bin_succ_Min  "bin_succ (Min)     = Pls"
    2.68 -  bin_succ_BIT  "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"
    2.69 +  bin_succ_Pls:  "bin_succ (Pls)     = Pls BIT 1"
    2.70 +  bin_succ_Min:  "bin_succ (Min)     = Pls"
    2.71 +  bin_succ_BIT:  "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"
    2.72  
    2.73  primrec (*predecessor*)
    2.74 -  bin_pred_Pls  "bin_pred (Pls)     = Min"
    2.75 -  bin_pred_Min  "bin_pred (Min)     = Min BIT 0"
    2.76 -  bin_pred_BIT  "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"
    2.77 +  bin_pred_Pls:  "bin_pred (Pls)     = Min"
    2.78 +  bin_pred_Min:  "bin_pred (Min)     = Min BIT 0"
    2.79 +  bin_pred_BIT:  "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"
    2.80  
    2.81  primrec (*unary negation*)
    2.82 -  bin_minus_Pls
    2.83 +  bin_minus_Pls:
    2.84      "bin_minus (Pls)       = Pls"
    2.85 -  bin_minus_Min
    2.86 +  bin_minus_Min:
    2.87      "bin_minus (Min)       = Pls BIT 1"
    2.88 -  bin_minus_BIT
    2.89 +  bin_minus_BIT:
    2.90      "bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)),
    2.91  				bin_minus(w) BIT 0)"
    2.92  
    2.93  primrec (*sum*)
    2.94 -  bin_adder_Pls
    2.95 +  bin_adder_Pls:
    2.96      "bin_adder (Pls)     = (lam w:bin. w)"
    2.97 -  bin_adder_Min
    2.98 +  bin_adder_Min:
    2.99      "bin_adder (Min)     = (lam w:bin. bin_pred(w))"
   2.100 -  bin_adder_BIT
   2.101 +  bin_adder_BIT:
   2.102      "bin_adder (v BIT x) = 
   2.103         (lam w:bin. 
   2.104           bin_case (v BIT x, bin_pred(v BIT x), 
   2.105 @@ -89,19 +88,610 @@
   2.106  				x xor y)"
   2.107  *)
   2.108  
   2.109 -defs
   2.110 -  bin_add_def "bin_add(v,w) == bin_adder(v)`w"
   2.111 +constdefs
   2.112 +  bin_add   :: "[i,i]=>i"
   2.113 +    "bin_add(v,w) == bin_adder(v)`w"
   2.114  
   2.115  
   2.116  primrec
   2.117 -  bin_mult_Pls
   2.118 +  bin_mult_Pls:
   2.119      "bin_mult (Pls,w)     = Pls"
   2.120 -  bin_mult_Min
   2.121 +  bin_mult_Min:
   2.122      "bin_mult (Min,w)     = bin_minus(w)"
   2.123 -  bin_mult_BIT
   2.124 +  bin_mult_BIT:
   2.125      "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
   2.126  				 NCons(bin_mult(v,w),0))"
   2.127  
   2.128  setup NumeralSyntax.setup
   2.129  
   2.130 +
   2.131 +declare bin.intros [simp,TC]
   2.132 +
   2.133 +lemma NCons_Pls_0: "NCons(Pls,0) = Pls"
   2.134 +by simp
   2.135 +
   2.136 +lemma NCons_Pls_1: "NCons(Pls,1) = Pls BIT 1"
   2.137 +by simp
   2.138 +
   2.139 +lemma NCons_Min_0: "NCons(Min,0) = Min BIT 0"
   2.140 +by simp
   2.141 +
   2.142 +lemma NCons_Min_1: "NCons(Min,1) = Min"
   2.143 +by simp
   2.144 +
   2.145 +lemma NCons_BIT: "NCons(w BIT x,b) = w BIT x BIT b"
   2.146 +by (simp add: bin.case_eqns)
   2.147 +
   2.148 +lemmas NCons_simps [simp] = 
   2.149 +    NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
   2.150 +
   2.151 +
   2.152 +
   2.153 +(** Type checking **)
   2.154 +
   2.155 +lemma integ_of_type [TC]: "w: bin ==> integ_of(w) : int"
   2.156 +apply (induct_tac "w")
   2.157 +apply (simp_all add: bool_into_nat)
   2.158 +done
   2.159 +
   2.160 +lemma NCons_type [TC]: "[| w: bin; b: bool |] ==> NCons(w,b) : bin"
   2.161 +by (induct_tac "w", auto)
   2.162 +
   2.163 +lemma bin_succ_type [TC]: "w: bin ==> bin_succ(w) : bin"
   2.164 +by (induct_tac "w", auto)
   2.165 +
   2.166 +lemma bin_pred_type [TC]: "w: bin ==> bin_pred(w) : bin"
   2.167 +by (induct_tac "w", auto)
   2.168 +
   2.169 +lemma bin_minus_type [TC]: "w: bin ==> bin_minus(w) : bin"
   2.170 +by (induct_tac "w", auto)
   2.171 +
   2.172 +(*This proof is complicated by the mutual recursion*)
   2.173 +lemma bin_add_type [rule_format,TC]:
   2.174 +     "v: bin ==> ALL w: bin. bin_add(v,w) : bin"
   2.175 +apply (unfold bin_add_def)
   2.176 +apply (induct_tac "v")
   2.177 +apply (rule_tac [3] ballI)
   2.178 +apply (rename_tac [3] "w'")
   2.179 +apply (induct_tac [3] "w'")
   2.180 +apply (simp_all add: NCons_type)
   2.181 +done
   2.182 +
   2.183 +lemma bin_mult_type [TC]: "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin"
   2.184 +by (induct_tac "v", auto)
   2.185 +
   2.186 +
   2.187 +subsubsection{*The Carry and Borrow Functions, 
   2.188 +            @{term bin_succ} and @{term bin_pred}*}
   2.189 +
   2.190 +(*NCons preserves the integer value of its argument*)
   2.191 +lemma integ_of_NCons [simp]:
   2.192 +     "[| w: bin; b: bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)"
   2.193 +apply (erule bin.cases)
   2.194 +apply (auto elim!: boolE) 
   2.195 +done
   2.196 +
   2.197 +lemma integ_of_succ [simp]:
   2.198 +     "w: bin ==> integ_of(bin_succ(w)) = $#1 $+ integ_of(w)"
   2.199 +apply (erule bin.induct)
   2.200 +apply (auto simp add: zadd_ac elim!: boolE) 
   2.201 +done
   2.202 +
   2.203 +lemma integ_of_pred [simp]:
   2.204 +     "w: bin ==> integ_of(bin_pred(w)) = $- ($#1) $+ integ_of(w)"
   2.205 +apply (erule bin.induct)
   2.206 +apply (auto simp add: zadd_ac elim!: boolE) 
   2.207 +done
   2.208 +
   2.209 +
   2.210 +subsubsection{*@{term bin_minus}: Unary Negation of Binary Integers*}
   2.211 +
   2.212 +lemma integ_of_minus: "w: bin ==> integ_of(bin_minus(w)) = $- integ_of(w)"
   2.213 +apply (erule bin.induct)
   2.214 +apply (auto simp add: zadd_ac zminus_zadd_distrib  elim!: boolE) 
   2.215 +done
   2.216 +
   2.217 +
   2.218 +subsubsection{*@{term bin_add}: Binary Addition*}
   2.219 +
   2.220 +lemma bin_add_Pls [simp]: "w: bin ==> bin_add(Pls,w) = w"
   2.221 +by (unfold bin_add_def, simp)
   2.222 +
   2.223 +lemma bin_add_Pls_right: "w: bin ==> bin_add(w,Pls) = w"
   2.224 +apply (unfold bin_add_def)
   2.225 +apply (erule bin.induct, auto)
   2.226 +done
   2.227 +
   2.228 +lemma bin_add_Min [simp]: "w: bin ==> bin_add(Min,w) = bin_pred(w)"
   2.229 +by (unfold bin_add_def, simp)
   2.230 +
   2.231 +lemma bin_add_Min_right: "w: bin ==> bin_add(w,Min) = bin_pred(w)"
   2.232 +apply (unfold bin_add_def)
   2.233 +apply (erule bin.induct, auto)
   2.234 +done
   2.235 +
   2.236 +lemma bin_add_BIT_Pls [simp]: "bin_add(v BIT x,Pls) = v BIT x"
   2.237 +by (unfold bin_add_def, simp)
   2.238 +
   2.239 +lemma bin_add_BIT_Min [simp]: "bin_add(v BIT x,Min) = bin_pred(v BIT x)"
   2.240 +by (unfold bin_add_def, simp)
   2.241 +
   2.242 +lemma bin_add_BIT_BIT [simp]:
   2.243 +     "[| w: bin;  y: bool |]               
   2.244 +      ==> bin_add(v BIT x, w BIT y) =  
   2.245 +          NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)"
   2.246 +by (unfold bin_add_def, simp)
   2.247 +
   2.248 +lemma integ_of_add [rule_format]:
   2.249 +     "v: bin ==>  
   2.250 +          ALL w: bin. integ_of(bin_add(v,w)) = integ_of(v) $+ integ_of(w)"
   2.251 +apply (erule bin.induct, simp, simp)
   2.252 +apply (rule ballI)
   2.253 +apply (induct_tac "wa")
   2.254 +apply (auto simp add: zadd_ac elim!: boolE) 
   2.255 +done
   2.256 +
   2.257 +(*Subtraction*)
   2.258 +lemma diff_integ_of_eq: 
   2.259 +     "[| v: bin;  w: bin |]    
   2.260 +      ==> integ_of(v) $- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))"
   2.261 +apply (unfold zdiff_def)
   2.262 +apply (simp add: integ_of_add integ_of_minus)
   2.263 +done
   2.264 +
   2.265 +
   2.266 +subsubsection{*@{term bin_mult}: Binary Multiplication*}
   2.267 +
   2.268 +lemma integ_of_mult:
   2.269 +     "[| v: bin;  w: bin |]    
   2.270 +      ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)"
   2.271 +apply (induct_tac "v", simp)
   2.272 +apply (simp add: integ_of_minus)
   2.273 +apply (auto simp add: zadd_ac integ_of_add zadd_zmult_distrib  elim!: boolE) 
   2.274 +done
   2.275 +
   2.276 +
   2.277 +subsection{*Computations*}
   2.278 +
   2.279 +(** extra rules for bin_succ, bin_pred **)
   2.280 +
   2.281 +lemma bin_succ_1: "bin_succ(w BIT 1) = bin_succ(w) BIT 0"
   2.282 +by simp
   2.283 +
   2.284 +lemma bin_succ_0: "bin_succ(w BIT 0) = NCons(w,1)"
   2.285 +by simp
   2.286 +
   2.287 +lemma bin_pred_1: "bin_pred(w BIT 1) = NCons(w,0)"
   2.288 +by simp
   2.289 +
   2.290 +lemma bin_pred_0: "bin_pred(w BIT 0) = bin_pred(w) BIT 1"
   2.291 +by simp
   2.292 +
   2.293 +(** extra rules for bin_minus **)
   2.294 +
   2.295 +lemma bin_minus_1: "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))"
   2.296 +by simp
   2.297 +
   2.298 +lemma bin_minus_0: "bin_minus(w BIT 0) = bin_minus(w) BIT 0"
   2.299 +by simp
   2.300 +
   2.301 +(** extra rules for bin_add **)
   2.302 +
   2.303 +lemma bin_add_BIT_11: "w: bin ==> bin_add(v BIT 1, w BIT 1) =  
   2.304 +                     NCons(bin_add(v, bin_succ(w)), 0)"
   2.305 +by simp
   2.306 +
   2.307 +lemma bin_add_BIT_10: "w: bin ==> bin_add(v BIT 1, w BIT 0) =   
   2.308 +                     NCons(bin_add(v,w), 1)"
   2.309 +by simp
   2.310 +
   2.311 +lemma bin_add_BIT_0: "[| w: bin;  y: bool |]  
   2.312 +      ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)"
   2.313 +by simp
   2.314 +
   2.315 +(** extra rules for bin_mult **)
   2.316 +
   2.317 +lemma bin_mult_1: "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)"
   2.318 +by simp
   2.319 +
   2.320 +lemma bin_mult_0: "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)"
   2.321 +by simp
   2.322 +
   2.323 +
   2.324 +(** Simplification rules with integer constants **)
   2.325 +
   2.326 +lemma int_of_0: "$#0 = #0"
   2.327 +by simp
   2.328 +
   2.329 +lemma int_of_succ: "$# succ(n) = #1 $+ $#n"
   2.330 +by (simp add: int_of_add [symmetric] natify_succ)
   2.331 +
   2.332 +lemma zminus_0 [simp]: "$- #0 = #0"
   2.333 +by simp
   2.334 +
   2.335 +lemma zadd_0_intify [simp]: "#0 $+ z = intify(z)"
   2.336 +by simp
   2.337 +
   2.338 +lemma zadd_0_right_intify [simp]: "z $+ #0 = intify(z)"
   2.339 +by simp
   2.340 +
   2.341 +lemma zmult_1_intify [simp]: "#1 $* z = intify(z)"
   2.342 +by simp
   2.343 +
   2.344 +lemma zmult_1_right_intify [simp]: "z $* #1 = intify(z)"
   2.345 +by (subst zmult_commute, simp)
   2.346 +
   2.347 +lemma zmult_0 [simp]: "#0 $* z = #0"
   2.348 +by simp
   2.349 +
   2.350 +lemma zmult_0_right [simp]: "z $* #0 = #0"
   2.351 +by (subst zmult_commute, simp)
   2.352 +
   2.353 +lemma zmult_minus1 [simp]: "#-1 $* z = $-z"
   2.354 +by (simp add: zcompare_rls)
   2.355 +
   2.356 +lemma zmult_minus1_right [simp]: "z $* #-1 = $-z"
   2.357 +apply (subst zmult_commute)
   2.358 +apply (rule zmult_minus1)
   2.359 +done
   2.360 +
   2.361 +
   2.362 +subsection{*Simplification Rules for Comparison of Binary Numbers*}
   2.363 +text{*Thanks to Norbert Voelker*}
   2.364 +
   2.365 +(** Equals (=) **)
   2.366 +
   2.367 +lemma eq_integ_of_eq: 
   2.368 +     "[| v: bin;  w: bin |]    
   2.369 +      ==> ((integ_of(v)) = integ_of(w)) <->  
   2.370 +          iszero (integ_of (bin_add (v, bin_minus(w))))"
   2.371 +apply (unfold iszero_def)
   2.372 +apply (simp add: zcompare_rls integ_of_add integ_of_minus)
   2.373 +done
   2.374 +
   2.375 +lemma iszero_integ_of_Pls: "iszero (integ_of(Pls))"
   2.376 +by (unfold iszero_def, simp)
   2.377 +
   2.378 +
   2.379 +lemma nonzero_integ_of_Min: "~ iszero (integ_of(Min))"
   2.380 +apply (unfold iszero_def)
   2.381 +apply (simp add: zminus_equation)
   2.382 +done
   2.383 +
   2.384 +lemma iszero_integ_of_BIT: 
   2.385 +     "[| w: bin; x: bool |]  
   2.386 +      ==> iszero (integ_of (w BIT x)) <-> (x=0 & iszero (integ_of(w)))"
   2.387 +apply (unfold iszero_def, simp)
   2.388 +apply (subgoal_tac "integ_of (w) : int")
   2.389 +apply typecheck
   2.390 +apply (drule int_cases)
   2.391 +apply (auto elim!: boolE simp add: int_of_add [symmetric])
   2.392 +apply (simp_all add: zcompare_rls zminus_zadd_distrib [symmetric]
   2.393 +                     int_of_add [symmetric])
   2.394 +apply (subgoal_tac "znegative ($- $# succ (n)) <-> znegative ($# succ (n))")
   2.395 + apply (simp (no_asm_use))
   2.396 +apply simp 
   2.397 +done
   2.398 +
   2.399 +lemma iszero_integ_of_0:
   2.400 +     "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"
   2.401 +by (simp only: iszero_integ_of_BIT, blast) 
   2.402 +
   2.403 +lemma iszero_integ_of_1: "w: bin ==> ~ iszero (integ_of (w BIT 1))"
   2.404 +by (simp only: iszero_integ_of_BIT, blast)
   2.405 +
   2.406 +
   2.407 +
   2.408 +(** Less-than (<) **)
   2.409 +
   2.410 +lemma less_integ_of_eq_neg: 
   2.411 +     "[| v: bin;  w: bin |]    
   2.412 +      ==> integ_of(v) $< integ_of(w)  
   2.413 +          <-> znegative (integ_of (bin_add (v, bin_minus(w))))"
   2.414 +apply (unfold zless_def zdiff_def)
   2.415 +apply (simp add: integ_of_minus integ_of_add)
   2.416 +done
   2.417 +
   2.418 +lemma not_neg_integ_of_Pls: "~ znegative (integ_of(Pls))"
   2.419 +by simp
   2.420 +
   2.421 +lemma neg_integ_of_Min: "znegative (integ_of(Min))"
   2.422 +by simp
   2.423 +
   2.424 +lemma neg_integ_of_BIT:
   2.425 +     "[| w: bin; x: bool |]  
   2.426 +      ==> znegative (integ_of (w BIT x)) <-> znegative (integ_of(w))"
   2.427 +apply simp
   2.428 +apply (subgoal_tac "integ_of (w) : int")
   2.429 +apply typecheck
   2.430 +apply (drule int_cases)
   2.431 +apply (auto elim!: boolE simp add: int_of_add [symmetric]  zcompare_rls)
   2.432 +apply (simp_all add: zminus_zadd_distrib [symmetric] zdiff_def 
   2.433 +                     int_of_add [symmetric])
   2.434 +apply (subgoal_tac "$#1 $- $# succ (succ (n #+ n)) = $- $# succ (n #+ n) ")
   2.435 + apply (simp add: zdiff_def)
   2.436 +apply (simp add: equation_zminus int_of_diff [symmetric])
   2.437 +done
   2.438 +
   2.439 +(** Less-than-or-equals (<=) **)
   2.440 +
   2.441 +lemma le_integ_of_eq_not_less:
   2.442 +     "(integ_of(x) $<= (integ_of(w))) <-> ~ (integ_of(w) $< (integ_of(x)))"
   2.443 +by (simp add: not_zless_iff_zle [THEN iff_sym])
   2.444 +
   2.445 +
   2.446 +(*Delete the original rewrites, with their clumsy conditional expressions*)
   2.447 +declare bin_succ_BIT [simp del] 
   2.448 +        bin_pred_BIT [simp del] 
   2.449 +        bin_minus_BIT [simp del]
   2.450 +        NCons_Pls [simp del]
   2.451 +        NCons_Min [simp del]
   2.452 +        bin_adder_BIT [simp del]
   2.453 +        bin_mult_BIT [simp del]
   2.454 +
   2.455 +(*Hide the binary representation of integer constants*)
   2.456 +declare integ_of_Pls [simp del] integ_of_Min [simp del] integ_of_BIT [simp del]
   2.457 +
   2.458 +
   2.459 +lemmas bin_arith_extra_simps =
   2.460 +     integ_of_add [symmetric]   
   2.461 +     integ_of_minus [symmetric] 
   2.462 +     integ_of_mult [symmetric]  
   2.463 +     bin_succ_1 bin_succ_0 
   2.464 +     bin_pred_1 bin_pred_0 
   2.465 +     bin_minus_1 bin_minus_0  
   2.466 +     bin_add_Pls_right bin_add_Min_right
   2.467 +     bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
   2.468 +     diff_integ_of_eq
   2.469 +     bin_mult_1 bin_mult_0 NCons_simps
   2.470 +
   2.471 +
   2.472 +(*For making a minimal simpset, one must include these default simprules
   2.473 +  of thy.  Also include simp_thms, or at least (~False)=True*)
   2.474 +lemmas bin_arith_simps =
   2.475 +     bin_pred_Pls bin_pred_Min
   2.476 +     bin_succ_Pls bin_succ_Min
   2.477 +     bin_add_Pls bin_add_Min
   2.478 +     bin_minus_Pls bin_minus_Min
   2.479 +     bin_mult_Pls bin_mult_Min 
   2.480 +     bin_arith_extra_simps
   2.481 +
   2.482 +(*Simplification of relational operations*)
   2.483 +lemmas bin_rel_simps =
   2.484 +     eq_integ_of_eq iszero_integ_of_Pls nonzero_integ_of_Min
   2.485 +     iszero_integ_of_0 iszero_integ_of_1
   2.486 +     less_integ_of_eq_neg
   2.487 +     not_neg_integ_of_Pls neg_integ_of_Min neg_integ_of_BIT
   2.488 +     le_integ_of_eq_not_less
   2.489 +
   2.490 +declare bin_arith_simps [simp]
   2.491 +declare bin_rel_simps [simp]
   2.492 +
   2.493 +
   2.494 +(** Simplification of arithmetic when nested to the right **)
   2.495 +
   2.496 +lemma add_integ_of_left [simp]:
   2.497 +     "[| v: bin;  w: bin |]    
   2.498 +      ==> integ_of(v) $+ (integ_of(w) $+ z) = (integ_of(bin_add(v,w)) $+ z)"
   2.499 +by (simp add: zadd_assoc [symmetric])
   2.500 +
   2.501 +lemma mult_integ_of_left [simp]:
   2.502 +     "[| v: bin;  w: bin |]    
   2.503 +      ==> integ_of(v) $* (integ_of(w) $* z) = (integ_of(bin_mult(v,w)) $* z)"
   2.504 +by (simp add: zmult_assoc [symmetric])
   2.505 +
   2.506 +lemma add_integ_of_diff1 [simp]: 
   2.507 +    "[| v: bin;  w: bin |]    
   2.508 +      ==> integ_of(v) $+ (integ_of(w) $- c) = integ_of(bin_add(v,w)) $- (c)"
   2.509 +apply (unfold zdiff_def)
   2.510 +apply (rule add_integ_of_left, auto)
   2.511 +done
   2.512 +
   2.513 +lemma add_integ_of_diff2 [simp]:
   2.514 +     "[| v: bin;  w: bin |]    
   2.515 +      ==> integ_of(v) $+ (c $- integ_of(w)) =  
   2.516 +          integ_of (bin_add (v, bin_minus(w))) $+ (c)"
   2.517 +apply (subst diff_integ_of_eq [symmetric])
   2.518 +apply (simp_all add: zdiff_def zadd_ac)
   2.519 +done
   2.520 +
   2.521 +
   2.522 +(** More for integer constants **)
   2.523 +
   2.524 +declare int_of_0 [simp] int_of_succ [simp]
   2.525 +
   2.526 +lemma zdiff0 [simp]: "#0 $- x = $-x"
   2.527 +by (simp add: zdiff_def)
   2.528 +
   2.529 +lemma zdiff0_right [simp]: "x $- #0 = intify(x)"
   2.530 +by (simp add: zdiff_def)
   2.531 +
   2.532 +lemma zdiff_self [simp]: "x $- x = #0"
   2.533 +by (simp add: zdiff_def)
   2.534 +
   2.535 +lemma znegative_iff_zless_0: "k: int ==> znegative(k) <-> k $< #0"
   2.536 +by (simp add: zless_def)
   2.537 +
   2.538 +lemma zero_zless_imp_znegative_zminus: "[|#0 $< k; k: int|] ==> znegative($-k)"
   2.539 +by (simp add: zless_def)
   2.540 +
   2.541 +lemma zero_zle_int_of [simp]: "#0 $<= $# n"
   2.542 +by (simp add: not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym])
   2.543 +
   2.544 +lemma nat_of_0 [simp]: "nat_of(#0) = 0"
   2.545 +by (simp only: natify_0 int_of_0 [symmetric] nat_of_int_of)
   2.546 +
   2.547 +lemma nat_le_int0_lemma: "[| z $<= $#0; z: int |] ==> nat_of(z) = 0"
   2.548 +by (auto simp add: znegative_iff_zless_0 [THEN iff_sym] zle_def zneg_nat_of)
   2.549 +
   2.550 +lemma nat_le_int0: "z $<= $#0 ==> nat_of(z) = 0"
   2.551 +apply (subgoal_tac "nat_of (intify (z)) = 0")
   2.552 +apply (rule_tac [2] nat_le_int0_lemma, auto)
   2.553 +done
   2.554 +
   2.555 +lemma int_of_eq_0_imp_natify_eq_0: "$# n = #0 ==> natify(n) = 0"
   2.556 +by (rule not_znegative_imp_zero, auto)
   2.557 +
   2.558 +lemma nat_of_zminus_int_of: "nat_of($- $# n) = 0"
   2.559 +apply (unfold nat_of_def raw_nat_of_def)
   2.560 +apply (auto dest!: not_znegative_imp_zero natify_int_of_eq
   2.561 +            iff del: int_of_eq)
   2.562 +apply (rule the_equality, auto)
   2.563 +apply (blast intro: int_of_eq_0_imp_natify_eq_0 sym)
   2.564 +done
   2.565 +
   2.566 +lemma int_of_nat_of: "#0 $<= z ==> $# nat_of(z) = intify(z)"
   2.567 +apply (rule not_zneg_nat_of_intify)
   2.568 +apply (simp add: znegative_iff_zless_0 not_zless_iff_zle)
   2.569 +done
   2.570 +
   2.571 +declare int_of_nat_of [simp] nat_of_zminus_int_of [simp]
   2.572 +
   2.573 +lemma int_of_nat_of_if: "$# nat_of(z) = (if #0 $<= z then intify(z) else #0)"
   2.574 +by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless)
   2.575 +
   2.576 +lemma zless_nat_iff_int_zless: "[| m: nat; z: int |] ==> (m < nat_of(z)) <-> ($#m $< z)"
   2.577 +apply (case_tac "znegative (z) ")
   2.578 +apply (erule_tac [2] not_zneg_nat_of [THEN subst])
   2.579 +apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans]
   2.580 +            simp add: znegative_iff_zless_0)
   2.581 +done
   2.582 +
   2.583 +
   2.584 +(** nat_of and zless **)
   2.585 +
   2.586 +(*An alternative condition is  $#0 <= w  *)
   2.587 +lemma zless_nat_conj_lemma: "$#0 $< z ==> (nat_of(w) < nat_of(z)) <-> (w $< z)"
   2.588 +apply (rule iff_trans)
   2.589 +apply (rule zless_int_of [THEN iff_sym])
   2.590 +apply (auto simp add: int_of_nat_of_if simp del: zless_int_of)
   2.591 +apply (auto elim: zless_asym simp add: not_zle_iff_zless)
   2.592 +apply (blast intro: zless_zle_trans)
   2.593 +done
   2.594 +
   2.595 +lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) <-> ($#0 $< z & w $< z)"
   2.596 +apply (case_tac "$#0 $< z")
   2.597 +apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle)
   2.598 +done
   2.599 +
   2.600 +(*This simprule cannot be added unless we can find a way to make eq_integ_of_eq
   2.601 +  unconditional!
   2.602 +  [The condition "True" is a hack to prevent looping.
   2.603 +    Conditional rewrite rules are tried after unconditional ones, so a rule
   2.604 +    like eq_nat_number_of will be tried first to eliminate #mm=#nn.]
   2.605 +  lemma integ_of_reorient [simp]:
   2.606 +       "True ==> (integ_of(w) = x) <-> (x = integ_of(w))"
   2.607 +  by auto
   2.608 +*)
   2.609 +
   2.610 +lemma integ_of_minus_reorient [simp]:
   2.611 +     "(integ_of(w) = $- x) <-> ($- x = integ_of(w))"
   2.612 +by auto
   2.613 +
   2.614 +lemma integ_of_add_reorient [simp]:
   2.615 +     "(integ_of(w) = x $+ y) <-> (x $+ y = integ_of(w))"
   2.616 +by auto
   2.617 +
   2.618 +lemma integ_of_diff_reorient [simp]:
   2.619 +     "(integ_of(w) = x $- y) <-> (x $- y = integ_of(w))"
   2.620 +by auto
   2.621 +
   2.622 +lemma integ_of_mult_reorient [simp]:
   2.623 +     "(integ_of(w) = x $* y) <-> (x $* y = integ_of(w))"
   2.624 +by auto
   2.625 +
   2.626 +ML
   2.627 +{*
   2.628 +val bin_pred_Pls = thm "bin_pred_Pls";
   2.629 +val bin_pred_Min = thm "bin_pred_Min";
   2.630 +val bin_minus_Pls = thm "bin_minus_Pls";
   2.631 +val bin_minus_Min = thm "bin_minus_Min";
   2.632 +
   2.633 +val NCons_Pls_0 = thm "NCons_Pls_0";
   2.634 +val NCons_Pls_1 = thm "NCons_Pls_1";
   2.635 +val NCons_Min_0 = thm "NCons_Min_0";
   2.636 +val NCons_Min_1 = thm "NCons_Min_1";
   2.637 +val NCons_BIT = thm "NCons_BIT";
   2.638 +val NCons_simps = thms "NCons_simps";
   2.639 +val integ_of_type = thm "integ_of_type";
   2.640 +val NCons_type = thm "NCons_type";
   2.641 +val bin_succ_type = thm "bin_succ_type";
   2.642 +val bin_pred_type = thm "bin_pred_type";
   2.643 +val bin_minus_type = thm "bin_minus_type";
   2.644 +val bin_add_type = thm "bin_add_type";
   2.645 +val bin_mult_type = thm "bin_mult_type";
   2.646 +val integ_of_NCons = thm "integ_of_NCons";
   2.647 +val integ_of_succ = thm "integ_of_succ";
   2.648 +val integ_of_pred = thm "integ_of_pred";
   2.649 +val integ_of_minus = thm "integ_of_minus";
   2.650 +val bin_add_Pls = thm "bin_add_Pls";
   2.651 +val bin_add_Pls_right = thm "bin_add_Pls_right";
   2.652 +val bin_add_Min = thm "bin_add_Min";
   2.653 +val bin_add_Min_right = thm "bin_add_Min_right";
   2.654 +val bin_add_BIT_Pls = thm "bin_add_BIT_Pls";
   2.655 +val bin_add_BIT_Min = thm "bin_add_BIT_Min";
   2.656 +val bin_add_BIT_BIT = thm "bin_add_BIT_BIT";
   2.657 +val integ_of_add = thm "integ_of_add";
   2.658 +val diff_integ_of_eq = thm "diff_integ_of_eq";
   2.659 +val integ_of_mult = thm "integ_of_mult";
   2.660 +val bin_succ_1 = thm "bin_succ_1";
   2.661 +val bin_succ_0 = thm "bin_succ_0";
   2.662 +val bin_pred_1 = thm "bin_pred_1";
   2.663 +val bin_pred_0 = thm "bin_pred_0";
   2.664 +val bin_minus_1 = thm "bin_minus_1";
   2.665 +val bin_minus_0 = thm "bin_minus_0";
   2.666 +val bin_add_BIT_11 = thm "bin_add_BIT_11";
   2.667 +val bin_add_BIT_10 = thm "bin_add_BIT_10";
   2.668 +val bin_add_BIT_0 = thm "bin_add_BIT_0";
   2.669 +val bin_mult_1 = thm "bin_mult_1";
   2.670 +val bin_mult_0 = thm "bin_mult_0";
   2.671 +val int_of_0 = thm "int_of_0";
   2.672 +val int_of_succ = thm "int_of_succ";
   2.673 +val zminus_0 = thm "zminus_0";
   2.674 +val zadd_0_intify = thm "zadd_0_intify";
   2.675 +val zadd_0_right_intify = thm "zadd_0_right_intify";
   2.676 +val zmult_1_intify = thm "zmult_1_intify";
   2.677 +val zmult_1_right_intify = thm "zmult_1_right_intify";
   2.678 +val zmult_0 = thm "zmult_0";
   2.679 +val zmult_0_right = thm "zmult_0_right";
   2.680 +val zmult_minus1 = thm "zmult_minus1";
   2.681 +val zmult_minus1_right = thm "zmult_minus1_right";
   2.682 +val eq_integ_of_eq = thm "eq_integ_of_eq";
   2.683 +val iszero_integ_of_Pls = thm "iszero_integ_of_Pls";
   2.684 +val nonzero_integ_of_Min = thm "nonzero_integ_of_Min";
   2.685 +val iszero_integ_of_BIT = thm "iszero_integ_of_BIT";
   2.686 +val iszero_integ_of_0 = thm "iszero_integ_of_0";
   2.687 +val iszero_integ_of_1 = thm "iszero_integ_of_1";
   2.688 +val less_integ_of_eq_neg = thm "less_integ_of_eq_neg";
   2.689 +val not_neg_integ_of_Pls = thm "not_neg_integ_of_Pls";
   2.690 +val neg_integ_of_Min = thm "neg_integ_of_Min";
   2.691 +val neg_integ_of_BIT = thm "neg_integ_of_BIT";
   2.692 +val le_integ_of_eq_not_less = thm "le_integ_of_eq_not_less";
   2.693 +val bin_arith_extra_simps = thms "bin_arith_extra_simps";
   2.694 +val bin_arith_simps = thms "bin_arith_simps";
   2.695 +val bin_rel_simps = thms "bin_rel_simps";
   2.696 +val add_integ_of_left = thm "add_integ_of_left";
   2.697 +val mult_integ_of_left = thm "mult_integ_of_left";
   2.698 +val add_integ_of_diff1 = thm "add_integ_of_diff1";
   2.699 +val add_integ_of_diff2 = thm "add_integ_of_diff2";
   2.700 +val zdiff0 = thm "zdiff0";
   2.701 +val zdiff0_right = thm "zdiff0_right";
   2.702 +val zdiff_self = thm "zdiff_self";
   2.703 +val znegative_iff_zless_0 = thm "znegative_iff_zless_0";
   2.704 +val zero_zless_imp_znegative_zminus = thm "zero_zless_imp_znegative_zminus";
   2.705 +val zero_zle_int_of = thm "zero_zle_int_of";
   2.706 +val nat_of_0 = thm "nat_of_0";
   2.707 +val nat_le_int0 = thm "nat_le_int0";
   2.708 +val int_of_eq_0_imp_natify_eq_0 = thm "int_of_eq_0_imp_natify_eq_0";
   2.709 +val nat_of_zminus_int_of = thm "nat_of_zminus_int_of";
   2.710 +val int_of_nat_of = thm "int_of_nat_of";
   2.711 +val int_of_nat_of_if = thm "int_of_nat_of_if";
   2.712 +val zless_nat_iff_int_zless = thm "zless_nat_iff_int_zless";
   2.713 +val zless_nat_conj = thm "zless_nat_conj";
   2.714 +val integ_of_minus_reorient = thm "integ_of_minus_reorient";
   2.715 +val integ_of_add_reorient = thm "integ_of_add_reorient";
   2.716 +val integ_of_diff_reorient = thm "integ_of_diff_reorient";
   2.717 +val integ_of_mult_reorient = thm "integ_of_mult_reorient";
   2.718 +*}
   2.719 +
   2.720  end
     3.1 --- a/src/ZF/Integ/Int.ML	Thu Sep 05 14:03:03 2002 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,1064 +0,0 @@
     3.4 -(*  Title:      ZF/Integ/Int.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   1993  University of Cambridge
     3.8 -
     3.9 -The integers as equivalence classes over nat*nat.
    3.10 -
    3.11 -Could also prove...
    3.12 -"znegative(z) ==> $# zmagnitude(z) = $- z"
    3.13 -"~ znegative(z) ==> $# zmagnitude(z) = z"
    3.14 -*)
    3.15 -
    3.16 -AddSEs [quotientE];
    3.17 -
    3.18 -(*** Proving that intrel is an equivalence relation ***)
    3.19 -
    3.20 -(** Natural deduction for intrel **)
    3.21 -
    3.22 -Goalw [intrel_def]
    3.23 -    "<<x1,y1>,<x2,y2>>: intrel <-> \
    3.24 -\    x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1";
    3.25 -by (Fast_tac 1);
    3.26 -qed "intrel_iff";
    3.27 -
    3.28 -Goalw [intrel_def]
    3.29 -    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |]  \
    3.30 -\    ==> <<x1,y1>,<x2,y2>>: intrel";
    3.31 -by (fast_tac (claset() addIs prems) 1);
    3.32 -qed "intrelI";
    3.33 -
    3.34 -(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
    3.35 -Goalw [intrel_def]
    3.36 -  "p: intrel --> (EX x1 y1 x2 y2. \
    3.37 -\                  p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
    3.38 -\                  x1: nat & y1: nat & x2: nat & y2: nat)";
    3.39 -by (Fast_tac 1);
    3.40 -qed "intrelE_lemma";
    3.41 -
    3.42 -val [major,minor] = goal (the_context ())
    3.43 -  "[| p: intrel;  \
    3.44 -\     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
    3.45 -\                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
    3.46 -\  ==> Q";
    3.47 -by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
    3.48 -by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
    3.49 -qed "intrelE";
    3.50 -
    3.51 -AddSIs [intrelI];
    3.52 -AddSEs [intrelE];
    3.53 -
    3.54 -Goal "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
    3.55 -by (rtac sym 1);
    3.56 -by (REPEAT (etac add_left_cancel 1));
    3.57 -by (ALLGOALS Asm_simp_tac);
    3.58 -qed "int_trans_lemma";
    3.59 -
    3.60 -Goalw [equiv_def, refl_def, sym_def, trans_def]
    3.61 -    "equiv(nat*nat, intrel)";
    3.62 -by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
    3.63 -qed "equiv_intrel";
    3.64 -
    3.65 -
    3.66 -Goalw [int_def] "[| m: nat; n: nat |] ==> intrel `` {<m,n>} : int";
    3.67 -by (blast_tac (claset() addIs [quotientI]) 1);
    3.68 -qed "image_intrel_int";
    3.69 -
    3.70 -
    3.71 -Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
    3.72 -	  add_0_right, add_succ_right];
    3.73 -Addcongs [conj_cong];
    3.74 -
    3.75 -bind_thm ("eq_intrelD", equiv_intrel RSN (2,eq_equiv_class));
    3.76 -
    3.77 -(** int_of: the injection from nat to int **)
    3.78 -
    3.79 -Goalw [int_def,quotient_def,int_of_def]  "$#m : int";
    3.80 -by Auto_tac;
    3.81 -qed "int_of_type";
    3.82 -
    3.83 -Addsimps [int_of_type];
    3.84 -AddTCs  [int_of_type];
    3.85 -
    3.86 -
    3.87 -Goalw [int_of_def] "($# m = $# n) <-> natify(m)=natify(n)"; 
    3.88 -by Auto_tac;  
    3.89 -qed "int_of_eq"; 
    3.90 -AddIffs [int_of_eq];
    3.91 -
    3.92 -Goal "[| $#m = $#n;  m: nat;  n: nat |] ==> m=n";
    3.93 -by (dtac (int_of_eq RS iffD1) 1);
    3.94 -by Auto_tac;
    3.95 -qed "int_of_inject";
    3.96 -
    3.97 -
    3.98 -(** intify: coercion from anything to int **)
    3.99 -
   3.100 -Goal "intify(x) : int";
   3.101 -by (simp_tac (simpset() addsimps [intify_def]) 1);
   3.102 -qed "intify_in_int";
   3.103 -AddIffs [intify_in_int];
   3.104 -AddTCs [intify_in_int];
   3.105 -
   3.106 -Goal "n : int ==> intify(n) = n";
   3.107 -by (asm_simp_tac (simpset() addsimps [intify_def]) 1);
   3.108 -qed "intify_ident";
   3.109 -Addsimps [intify_ident];
   3.110 -
   3.111 -
   3.112 -(*** Collapsing rules: to remove intify from arithmetic expressions ***)
   3.113 -
   3.114 -Goal "intify(intify(x)) = intify(x)";
   3.115 -by (Simp_tac 1);
   3.116 -qed "intify_idem";
   3.117 -Addsimps [intify_idem];
   3.118 -
   3.119 -Goal "$# (natify(m)) = $# m";
   3.120 -by (simp_tac (simpset() addsimps [int_of_def]) 1);
   3.121 -qed "int_of_natify";
   3.122 -
   3.123 -Goal "$- (intify(m)) = $- m";
   3.124 -by (simp_tac (simpset() addsimps [zminus_def]) 1);
   3.125 -qed "zminus_intify";
   3.126 -
   3.127 -Addsimps [int_of_natify, zminus_intify];
   3.128 -
   3.129 -(** Addition **)
   3.130 -
   3.131 -Goal "intify(x) $+ y = x $+ y";
   3.132 -by (simp_tac (simpset() addsimps [zadd_def]) 1);
   3.133 -qed "zadd_intify1";
   3.134 -
   3.135 -Goal "x $+ intify(y) = x $+ y";
   3.136 -by (simp_tac (simpset() addsimps [zadd_def]) 1);
   3.137 -qed "zadd_intify2";
   3.138 -Addsimps [zadd_intify1, zadd_intify2];
   3.139 -
   3.140 -(** Subtraction **)
   3.141 -
   3.142 -Goal "intify(x) $- y = x $- y";
   3.143 -by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   3.144 -qed "zdiff_intify1";
   3.145 -
   3.146 -Goal "x $- intify(y) = x $- y";
   3.147 -by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   3.148 -qed "zdiff_intify2";
   3.149 -Addsimps [zdiff_intify1, zdiff_intify2];
   3.150 -
   3.151 -(** Multiplication **)
   3.152 -
   3.153 -Goal "intify(x) $* y = x $* y";
   3.154 -by (simp_tac (simpset() addsimps [zmult_def]) 1);
   3.155 -qed "zmult_intify1";
   3.156 -
   3.157 -Goal "x $* intify(y) = x $* y";
   3.158 -by (simp_tac (simpset() addsimps [zmult_def]) 1);
   3.159 -qed "zmult_intify2";
   3.160 -Addsimps [zmult_intify1, zmult_intify2];
   3.161 -
   3.162 -(** Orderings **)
   3.163 -
   3.164 -Goal "intify(x) $< y <-> x $< y";
   3.165 -by (simp_tac (simpset() addsimps [zless_def]) 1);
   3.166 -qed "zless_intify1";
   3.167 -
   3.168 -Goal "x $< intify(y) <-> x $< y";
   3.169 -by (simp_tac (simpset() addsimps [zless_def]) 1);
   3.170 -qed "zless_intify2";
   3.171 -Addsimps [zless_intify1, zless_intify2];
   3.172 -
   3.173 -Goal "intify(x) $<= y <-> x $<= y";
   3.174 -by (simp_tac (simpset() addsimps [zle_def]) 1);
   3.175 -qed "zle_intify1";
   3.176 -
   3.177 -Goal "x $<= intify(y) <-> x $<= y";
   3.178 -by (simp_tac (simpset() addsimps [zle_def]) 1);
   3.179 -qed "zle_intify2";
   3.180 -Addsimps [zle_intify1, zle_intify2];
   3.181 -
   3.182 -
   3.183 -(**** zminus: unary negation on int ****)
   3.184 -
   3.185 -Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
   3.186 -by Safe_tac;
   3.187 -by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
   3.188 -qed "zminus_congruent";
   3.189 -
   3.190 -val RSLIST = curry (op MRS);
   3.191 -
   3.192 -(*Resolve th against the corresponding facts for zminus*)
   3.193 -val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
   3.194 -
   3.195 -Goalw [int_def,raw_zminus_def] "z : int ==> raw_zminus(z) : int";
   3.196 -by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
   3.197 -qed "raw_zminus_type";
   3.198 -
   3.199 -Goalw [zminus_def] "$-z : int";
   3.200 -by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type]) 1);
   3.201 -qed "zminus_type";
   3.202 -AddIffs [zminus_type];
   3.203 -AddTCs [zminus_type];
   3.204 -
   3.205 -
   3.206 -Goalw [int_def,raw_zminus_def]
   3.207 -     "[| raw_zminus(z) = raw_zminus(w);  z: int;  w: int |] ==> z=w";
   3.208 -by (etac (zminus_ize UN_equiv_class_inject) 1);
   3.209 -by Safe_tac;
   3.210 -by (auto_tac (claset() addDs [eq_intrelD], simpset() addsimps add_ac));  
   3.211 -qed "raw_zminus_inject";
   3.212 -
   3.213 -Goalw [zminus_def] "$-z = $-w ==> intify(z) = intify(w)";
   3.214 -by (blast_tac (claset() addSDs [raw_zminus_inject]) 1);
   3.215 -qed "zminus_inject_intify";
   3.216 -
   3.217 -AddSDs [zminus_inject_intify];
   3.218 -
   3.219 -Goal "[| $-z = $-w;  z: int;  w: int |] ==> z=w";
   3.220 -by Auto_tac;  
   3.221 -qed "zminus_inject";
   3.222 -
   3.223 -Goalw [raw_zminus_def]
   3.224 -    "[| x: nat;  y: nat |] \
   3.225 -\    ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}";
   3.226 -by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
   3.227 -qed "raw_zminus";
   3.228 -
   3.229 -Goalw [zminus_def]
   3.230 -    "[| x: nat;  y: nat |] \
   3.231 -\    ==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}";
   3.232 -by (asm_simp_tac (simpset() addsimps [raw_zminus, image_intrel_int]) 1);
   3.233 -qed "zminus";
   3.234 -
   3.235 -Goalw [int_def] "z : int ==> raw_zminus (raw_zminus(z)) = z";
   3.236 -by (auto_tac (claset(), simpset() addsimps [raw_zminus]));  
   3.237 -qed "raw_zminus_zminus";
   3.238 -
   3.239 -Goal "$- ($- z) = intify(z)";
   3.240 -by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type, 
   3.241 -	                          raw_zminus_zminus]) 1);
   3.242 -qed "zminus_zminus_intify"; 
   3.243 -
   3.244 -Goalw [int_of_def] "$- ($#0) = $#0";
   3.245 -by (simp_tac (simpset() addsimps [zminus]) 1);
   3.246 -qed "zminus_int0";
   3.247 -
   3.248 -Addsimps [zminus_zminus_intify, zminus_int0];
   3.249 -
   3.250 -Goal "z : int ==> $- ($- z) = z";
   3.251 -by (Asm_simp_tac 1);
   3.252 -qed "zminus_zminus";
   3.253 -
   3.254 -
   3.255 -(**** znegative: the test for negative integers ****)
   3.256 -
   3.257 -(*No natural number is negative!*)
   3.258 -Goalw [znegative_def, int_of_def]  "~ znegative($# n)";
   3.259 -by Safe_tac;
   3.260 -by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
   3.261 -by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
   3.262 -by (force_tac (claset(),
   3.263 -	       simpset() addsimps [add_le_self2 RS le_imp_not_lt,
   3.264 -				   natify_succ]) 1);
   3.265 -qed "not_znegative_int_of";
   3.266 -
   3.267 -Addsimps [not_znegative_int_of];
   3.268 -AddSEs   [not_znegative_int_of RS notE];
   3.269 -
   3.270 -Goalw [znegative_def, int_of_def] "znegative($- $# succ(n))";
   3.271 -by (asm_simp_tac (simpset() addsimps [zminus, natify_succ]) 1);
   3.272 -by (blast_tac (claset() addIs [nat_0_le]) 1);
   3.273 -qed "znegative_zminus_int_of";
   3.274 -
   3.275 -Addsimps [znegative_zminus_int_of];
   3.276 -
   3.277 -Goalw [znegative_def, int_of_def] "~ znegative($- $# n) ==> natify(n)=0";
   3.278 -by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
   3.279 -by (dres_inst_tac [("x","0")] spec 1);
   3.280 -by (auto_tac(claset(), 
   3.281 -             simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff RS iff_sym]));
   3.282 -qed "not_znegative_imp_zero";
   3.283 -
   3.284 -(**** nat_of: coercion of an integer to a natural number ****)
   3.285 -
   3.286 -Goalw [nat_of_def] "nat_of(intify(z)) = nat_of(z)";
   3.287 -by Auto_tac;  
   3.288 -qed "nat_of_intify";
   3.289 -Addsimps [nat_of_intify];
   3.290 -
   3.291 -Goalw [nat_of_def, raw_nat_of_def] "nat_of($# n) = natify(n)";
   3.292 -by (auto_tac (claset(), simpset() addsimps [int_of_eq]));  
   3.293 -qed "nat_of_int_of";
   3.294 -Addsimps [nat_of_int_of];
   3.295 -
   3.296 -Goalw [raw_nat_of_def] "raw_nat_of(z) : nat";
   3.297 -by Auto_tac;
   3.298 -by (case_tac "EX! m. m: nat & z = int_of(m)" 1);
   3.299 -by (asm_simp_tac (simpset() addsimps [the_0]) 2); 
   3.300 -by (rtac theI2 1);
   3.301 -by Auto_tac;  
   3.302 -qed "raw_nat_of_type";
   3.303 -
   3.304 -Goalw [nat_of_def] "nat_of(z) : nat";
   3.305 -by (simp_tac (simpset() addsimps [raw_nat_of_type]) 1); 
   3.306 -qed "nat_of_type";
   3.307 -AddIffs [nat_of_type];
   3.308 -AddTCs [nat_of_type];
   3.309 -
   3.310 -(**** zmagnitude: magnitide of an integer, as a natural number ****)
   3.311 -
   3.312 -Goalw [zmagnitude_def] "zmagnitude($# n) = natify(n)";
   3.313 -by (auto_tac (claset(), simpset() addsimps [int_of_eq]));  
   3.314 -qed "zmagnitude_int_of";
   3.315 -
   3.316 -Goal "natify(x)=n ==> $#x = $# n";
   3.317 -by (dtac sym 1);
   3.318 -by (asm_simp_tac (simpset() addsimps [int_of_eq]) 1);
   3.319 -qed "natify_int_of_eq";
   3.320 -
   3.321 -Goalw [zmagnitude_def] "zmagnitude($- $# n) = natify(n)";
   3.322 -by (rtac the_equality 1);
   3.323 -by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq], 
   3.324 -              simpset())
   3.325 -             delIffs [int_of_eq]));
   3.326 -by Auto_tac;  
   3.327 -qed "zmagnitude_zminus_int_of";
   3.328 -
   3.329 -Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
   3.330 -
   3.331 -Goalw [zmagnitude_def] "zmagnitude(z) : nat";
   3.332 -by (rtac theI2 1);
   3.333 -by Auto_tac;
   3.334 -qed "zmagnitude_type";
   3.335 -AddIffs [zmagnitude_type];
   3.336 -AddTCs [zmagnitude_type];
   3.337 -
   3.338 -Goalw [int_def, znegative_def, int_of_def]
   3.339 -     "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
   3.340 -by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
   3.341 -by (rename_tac "i j" 1);
   3.342 -by (dres_inst_tac [("x", "i")] spec 1);
   3.343 -by (dres_inst_tac [("x", "j")] spec 1);
   3.344 -by (rtac bexI 1);
   3.345 -by (rtac (add_diff_inverse2 RS sym) 1);
   3.346 -by Auto_tac;
   3.347 -by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1);
   3.348 -qed "not_zneg_int_of";
   3.349 -
   3.350 -Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
   3.351 -by (dtac not_zneg_int_of 1);
   3.352 -by Auto_tac;
   3.353 -qed "not_zneg_mag"; 
   3.354 -
   3.355 -Addsimps [not_zneg_mag];
   3.356 -
   3.357 -Goalw [int_def, znegative_def, int_of_def]
   3.358 -     "[| znegative(z); z: int |] ==> EX n:nat. z = $- ($# succ(n))"; 
   3.359 -by (auto_tac(claset() addSDs [less_imp_succ_add], 
   3.360 -	     simpset() addsimps [zminus, image_singleton_iff]));
   3.361 -qed "zneg_int_of";
   3.362 -
   3.363 -Goal "[| znegative(z); z: int |] ==> $# (zmagnitude(z)) = $- z"; 
   3.364 -by (dtac zneg_int_of 1);
   3.365 -by Auto_tac;
   3.366 -qed "zneg_mag"; 
   3.367 -
   3.368 -Addsimps [zneg_mag];
   3.369 -
   3.370 -Goal "z : int ==> EX n: nat. z = $# n | z = $- ($# succ(n))"; 
   3.371 -by (case_tac "znegative(z)" 1);
   3.372 -by (blast_tac (claset() addDs [not_zneg_mag, sym]) 2);
   3.373 -by (blast_tac (claset() addDs [zneg_int_of]) 1);
   3.374 -qed "int_cases"; 
   3.375 -
   3.376 -Goal "[| ~ znegative(z); z: int |] ==> $# (raw_nat_of(z)) = z";  
   3.377 -by (dtac not_zneg_int_of 1);
   3.378 -by (auto_tac (claset(), simpset() addsimps [raw_nat_of_type]));
   3.379 -by (auto_tac (claset(), simpset() addsimps [raw_nat_of_def]));
   3.380 -qed "not_zneg_raw_nat_of"; 
   3.381 -
   3.382 -Goal "~ znegative(intify(z)) ==> $# (nat_of(z)) = intify(z)";  
   3.383 -by (asm_simp_tac (simpset() addsimps [nat_of_def, not_zneg_raw_nat_of]) 1);
   3.384 -qed "not_zneg_nat_of_intify"; 
   3.385 -
   3.386 -Goal "[| ~ znegative(z); z: int |] ==> $# (nat_of(z)) = z";  
   3.387 -by (asm_simp_tac (simpset() addsimps [not_zneg_nat_of_intify]) 1);
   3.388 -qed "not_zneg_nat_of"; 
   3.389 -
   3.390 -Goalw [nat_of_def, raw_nat_of_def] "znegative(intify(z)) ==> nat_of(z) = 0"; 
   3.391 -by Auto_tac;  
   3.392 -qed "zneg_nat_of"; 
   3.393 -Addsimps [zneg_nat_of];
   3.394 -
   3.395 -
   3.396 -(**** zadd: addition on int ****)
   3.397 -
   3.398 -(** Congruence property for addition **)
   3.399 -
   3.400 -Goalw [congruent2_def]
   3.401 -    "congruent2(intrel, %z1 z2.                      \
   3.402 -\         let <x1,y1>=z1; <x2,y2>=z2                 \
   3.403 -\                           in intrel``{<x1#+x2, y1#+y2>})";
   3.404 -(*Proof via congruent2_commuteI seems longer*)
   3.405 -by Safe_tac;
   3.406 -by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
   3.407 -(*The rest should be trivial, but rearranging terms is hard;
   3.408 -  add_ac does not help rewriting with the assumptions.*)
   3.409 -by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
   3.410 -by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 1);
   3.411 -by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
   3.412 -qed "zadd_congruent2";
   3.413 -
   3.414 -(*Resolve th against the corresponding facts for zadd*)
   3.415 -val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
   3.416 -
   3.417 -Goalw [int_def,raw_zadd_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) : int";
   3.418 -by (rtac (zadd_ize UN_equiv_class_type2) 1);
   3.419 -by (simp_tac (simpset() addsimps [Let_def]) 3);
   3.420 -by (REPEAT (assume_tac 1));
   3.421 -qed "raw_zadd_type";
   3.422 -
   3.423 -Goal "z $+ w : int";
   3.424 -by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type]) 1);
   3.425 -qed "zadd_type";
   3.426 -AddIffs [zadd_type];  AddTCs [zadd_type];
   3.427 -
   3.428 -Goalw [raw_zadd_def]
   3.429 -  "[| x1: nat; y1: nat;  x2: nat; y2: nat |]              \
   3.430 -\  ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =  \
   3.431 -\      intrel `` {<x1#+x2, y1#+y2>}";
   3.432 -by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
   3.433 -by (simp_tac (simpset() addsimps [Let_def]) 1);
   3.434 -qed "raw_zadd";
   3.435 -
   3.436 -Goalw [zadd_def]
   3.437 -  "[| x1: nat; y1: nat;  x2: nat; y2: nat |]         \
   3.438 -\  ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =  \
   3.439 -\      intrel `` {<x1#+x2, y1#+y2>}";
   3.440 -by (asm_simp_tac (simpset() addsimps [raw_zadd, image_intrel_int]) 1);
   3.441 -qed "zadd";
   3.442 -
   3.443 -Goalw [int_def,int_of_def] "z : int ==> raw_zadd ($#0,z) = z";
   3.444 -by (auto_tac (claset(), simpset() addsimps [raw_zadd]));  
   3.445 -qed "raw_zadd_int0";
   3.446 -
   3.447 -Goal "$#0 $+ z = intify(z)";
   3.448 -by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_int0]) 1);
   3.449 -qed "zadd_int0_intify";
   3.450 -Addsimps [zadd_int0_intify];
   3.451 -
   3.452 -Goal "z: int ==> $#0 $+ z = z";
   3.453 -by (Asm_simp_tac 1);
   3.454 -qed "zadd_int0";
   3.455 -
   3.456 -Goalw [int_def]
   3.457 -     "[| z: int;  w: int |] ==> $- raw_zadd(z,w) = raw_zadd($- z, $- w)";
   3.458 -by (auto_tac (claset(), simpset() addsimps [zminus,raw_zadd]));  
   3.459 -qed "raw_zminus_zadd_distrib";
   3.460 -
   3.461 -Goal "$- (z $+ w) = $- z $+ $- w";
   3.462 -by (simp_tac (simpset() addsimps [zadd_def, raw_zminus_zadd_distrib]) 1);
   3.463 -qed "zminus_zadd_distrib";
   3.464 -
   3.465 -Addsimps [zminus_zadd_distrib];
   3.466 -
   3.467 -Goalw [int_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)";
   3.468 -by (auto_tac (claset(), simpset() addsimps raw_zadd::add_ac));  
   3.469 -qed "raw_zadd_commute";
   3.470 -
   3.471 -Goal "z $+ w = w $+ z";
   3.472 -by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_commute]) 1);
   3.473 -qed "zadd_commute";
   3.474 -
   3.475 -Goalw [int_def]
   3.476 -    "[| z1: int;  z2: int;  z3: int |]   \
   3.477 -\    ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))";
   3.478 -by (auto_tac (claset(), simpset() addsimps [raw_zadd, add_assoc]));  
   3.479 -qed "raw_zadd_assoc";
   3.480 -
   3.481 -Goal "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
   3.482 -by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type, raw_zadd_assoc]) 1);
   3.483 -qed "zadd_assoc";
   3.484 -
   3.485 -(*For AC rewriting*)
   3.486 -Goal "z1$+(z2$+z3) = z2$+(z1$+z3)";
   3.487 -by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
   3.488 -by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
   3.489 -qed "zadd_left_commute";
   3.490 -
   3.491 -(*Integer addition is an AC operator*)
   3.492 -bind_thms ("zadd_ac", [zadd_assoc, zadd_commute, zadd_left_commute]);
   3.493 -
   3.494 -Goalw [int_of_def] "$# (m #+ n) = ($#m) $+ ($#n)";
   3.495 -by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   3.496 -qed "int_of_add";
   3.497 -
   3.498 -Goal "$# succ(m) = $# 1 $+ ($# m)";
   3.499 -by (simp_tac (simpset() addsimps [int_of_add RS sym, natify_succ]) 1);
   3.500 -qed "int_succ_int_1";
   3.501 -
   3.502 -Goalw [int_of_def,zdiff_def]
   3.503 -     "[| m: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)";
   3.504 -by (ftac lt_nat_in_nat 1);
   3.505 -by (asm_simp_tac (simpset() addsimps [zadd,zminus,add_diff_inverse2]) 2);
   3.506 -by Auto_tac;  
   3.507 -qed "int_of_diff";
   3.508 -
   3.509 -Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $- z) = $#0";
   3.510 -by (auto_tac (claset(), simpset() addsimps [zminus, raw_zadd, add_commute]));  
   3.511 -qed "raw_zadd_zminus_inverse";
   3.512 -
   3.513 -Goal "z $+ ($- z) = $#0";
   3.514 -by (simp_tac (simpset() addsimps [zadd_def]) 1);
   3.515 -by (stac (zminus_intify RS sym) 1);
   3.516 -by (rtac (intify_in_int RS raw_zadd_zminus_inverse) 1); 
   3.517 -qed "zadd_zminus_inverse";
   3.518 -
   3.519 -Goal "($- z) $+ z = $#0";
   3.520 -by (simp_tac (simpset() addsimps [zadd_commute, zadd_zminus_inverse]) 1);
   3.521 -qed "zadd_zminus_inverse2";
   3.522 -
   3.523 -Goal "z $+ $#0 = intify(z)";
   3.524 -by (rtac ([zadd_commute, zadd_int0_intify] MRS trans) 1);
   3.525 -qed "zadd_int0_right_intify";
   3.526 -Addsimps [zadd_int0_right_intify];
   3.527 -
   3.528 -Goal "z:int ==> z $+ $#0 = z";
   3.529 -by (Asm_simp_tac 1);
   3.530 -qed "zadd_int0_right";
   3.531 -
   3.532 -Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
   3.533 -
   3.534 -
   3.535 -
   3.536 -(**** zmult: multiplication on int ****)
   3.537 -
   3.538 -(** Congruence property for multiplication **)
   3.539 -
   3.540 -Goal "congruent2(intrel, %p1 p2.                 \
   3.541 -\               split(%x1 y1. split(%x2 y2.     \
   3.542 -\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
   3.543 -by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   3.544 -by Auto_tac;
   3.545 -(*Proof that zmult is congruent in one argument*)
   3.546 -by (rename_tac "x y" 1);
   3.547 -by (forw_inst_tac [("t", "%u. x#*u")] (sym RS subst_context) 1);
   3.548 -by (dres_inst_tac [("t", "%u. y#*u")] subst_context 1);
   3.549 -by (REPEAT (etac add_left_cancel 1));
   3.550 -by (asm_simp_tac (simpset() addsimps [add_mult_distrib_left]) 1);
   3.551 -by Auto_tac;
   3.552 -qed "zmult_congruent2";
   3.553 -
   3.554 -
   3.555 -(*Resolve th against the corresponding facts for zmult*)
   3.556 -val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
   3.557 -
   3.558 -Goalw [int_def,raw_zmult_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) : int";
   3.559 -by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
   3.560 -                      split_type, add_type, mult_type, 
   3.561 -                      quotientI, SigmaI] 1));
   3.562 -qed "raw_zmult_type";
   3.563 -
   3.564 -Goal "z $* w : int";
   3.565 -by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type]) 1);
   3.566 -qed "zmult_type";
   3.567 -AddIffs [zmult_type];  AddTCs [zmult_type];
   3.568 -
   3.569 -Goalw [raw_zmult_def]
   3.570 -     "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
   3.571 -\     ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =     \
   3.572 -\         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   3.573 -by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
   3.574 -qed "raw_zmult";
   3.575 -
   3.576 -Goalw [zmult_def]
   3.577 -     "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
   3.578 -\     ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
   3.579 -\         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   3.580 -by (asm_simp_tac (simpset() addsimps [raw_zmult, image_intrel_int]) 1);
   3.581 -qed "zmult";
   3.582 -
   3.583 -Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#0,z) = $#0";
   3.584 -by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
   3.585 -qed "raw_zmult_int0";
   3.586 -
   3.587 -Goal "$#0 $* z = $#0";
   3.588 -by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_int0]) 1);
   3.589 -qed "zmult_int0";
   3.590 -Addsimps [zmult_int0];
   3.591 -
   3.592 -Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#1,z) = z";
   3.593 -by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
   3.594 -qed "raw_zmult_int1";
   3.595 -
   3.596 -Goal "$#1 $* z = intify(z)";
   3.597 -by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_int1]) 1);
   3.598 -qed "zmult_int1_intify";
   3.599 -Addsimps [zmult_int1_intify];
   3.600 -
   3.601 -Goal "z : int ==> $#1 $* z = z";
   3.602 -by (Asm_simp_tac 1);
   3.603 -qed "zmult_int1";
   3.604 -
   3.605 -Goalw [int_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)";
   3.606 -by (auto_tac (claset(), simpset() addsimps [raw_zmult] @ add_ac @ mult_ac));  
   3.607 -qed "raw_zmult_commute";
   3.608 -
   3.609 -Goal "z $* w = w $* z";
   3.610 -by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_commute]) 1);
   3.611 -qed "zmult_commute";
   3.612 -
   3.613 -Goalw [int_def]
   3.614 -     "[| z: int;  w: int |] ==> raw_zmult($- z, w) = $- raw_zmult(z, w)";
   3.615 -by (auto_tac (claset(), simpset() addsimps [zminus, raw_zmult] @ add_ac));  
   3.616 -qed "raw_zmult_zminus";
   3.617 -
   3.618 -Goal "($- z) $* w = $- (z $* w)";
   3.619 -by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_zminus]) 1);
   3.620 -by (stac (zminus_intify RS sym) 1 THEN rtac raw_zmult_zminus 1); 
   3.621 -by Auto_tac;  
   3.622 -qed "zmult_zminus";
   3.623 -Addsimps [zmult_zminus];
   3.624 -
   3.625 -Goal "w $* ($- z) = $- (w $* z)";
   3.626 -by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute]) 1);
   3.627 -qed "zmult_zminus_right";
   3.628 -Addsimps [zmult_zminus_right];
   3.629 -
   3.630 -Goalw [int_def]
   3.631 -    "[| z1: int;  z2: int;  z3: int |]   \
   3.632 -\    ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))";
   3.633 -by (auto_tac (claset(), 
   3.634 -  simpset() addsimps [raw_zmult, add_mult_distrib_left] @ add_ac @ mult_ac));  
   3.635 -qed "raw_zmult_assoc";
   3.636 -
   3.637 -Goal "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
   3.638 -by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type, 
   3.639 -                                  raw_zmult_assoc]) 1);
   3.640 -qed "zmult_assoc";
   3.641 -
   3.642 -(*For AC rewriting*)
   3.643 -Goal "z1$*(z2$*z3) = z2$*(z1$*z3)";
   3.644 -by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
   3.645 -by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
   3.646 -qed "zmult_left_commute";
   3.647 -
   3.648 -(*Integer multiplication is an AC operator*)
   3.649 -bind_thms ("zmult_ac", [zmult_assoc, zmult_commute, zmult_left_commute]);
   3.650 -
   3.651 -Goalw [int_def]
   3.652 -    "[| z1: int;  z2: int;  w: int |]  \
   3.653 -\    ==> raw_zmult(raw_zadd(z1,z2), w) = \
   3.654 -\        raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))";
   3.655 -by (auto_tac (claset(), 
   3.656 -              simpset() addsimps [raw_zadd, raw_zmult, add_mult_distrib_left] @ 
   3.657 -                                 add_ac @ mult_ac));  
   3.658 -qed "raw_zadd_zmult_distrib";
   3.659 -
   3.660 -Goal "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
   3.661 -by (simp_tac (simpset() addsimps [zmult_def, zadd_def, raw_zadd_type, 
   3.662 -     	                          raw_zmult_type, raw_zadd_zmult_distrib]) 1);
   3.663 -qed "zadd_zmult_distrib";
   3.664 -
   3.665 -Goal "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)";
   3.666 -by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute,
   3.667 -                                  zadd_zmult_distrib]) 1);
   3.668 -qed "zadd_zmult_distrib2";
   3.669 -
   3.670 -bind_thms ("int_typechecks",
   3.671 -  [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type]);
   3.672 -
   3.673 -
   3.674 -(*** Subtraction laws ***)
   3.675 -
   3.676 -Goal "z $- w : int";
   3.677 -by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   3.678 -qed "zdiff_type";
   3.679 -AddIffs [zdiff_type];  AddTCs [zdiff_type];
   3.680 -
   3.681 -Goal "$- (z $- y) = y $- z";
   3.682 -by (simp_tac (simpset() addsimps [zdiff_def, zadd_commute])1);
   3.683 -qed "zminus_zdiff_eq";
   3.684 -Addsimps [zminus_zdiff_eq];
   3.685 -
   3.686 -Goalw [zdiff_def] "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)";
   3.687 -by (stac zadd_zmult_distrib 1);
   3.688 -by (simp_tac (simpset() addsimps [zmult_zminus]) 1);
   3.689 -qed "zdiff_zmult_distrib";
   3.690 -
   3.691 -Goal "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)";
   3.692 -by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute, zdiff_zmult_distrib]) 1);
   3.693 -qed "zdiff_zmult_distrib2";
   3.694 -
   3.695 -Goal "x $+ (y $- z) = (x $+ y) $- z";
   3.696 -by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   3.697 -qed "zadd_zdiff_eq";
   3.698 -
   3.699 -Goal "(x $- y) $+ z = (x $+ z) $- y";
   3.700 -by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   3.701 -qed "zdiff_zadd_eq";
   3.702 -
   3.703 -
   3.704 -(*** "Less Than" ***)
   3.705 -
   3.706 -(*"Less than" is a linear ordering*)
   3.707 -Goalw [int_def, zless_def, znegative_def, zdiff_def] 
   3.708 -     "[| z: int; w: int |] ==> z$<w | z=w | w$<z"; 
   3.709 -by Auto_tac;  
   3.710 -by (asm_full_simp_tac
   3.711 -    (simpset() addsimps [zadd, zminus, image_iff, Bex_def]) 1);
   3.712 -by (res_inst_tac [("i", "xb#+ya"), ("j", "xc #+ y")] Ord_linear_lt 1);
   3.713 -by (ALLGOALS (force_tac (claset() addSDs [spec], 
   3.714 -                         simpset() addsimps add_ac)));
   3.715 -qed "zless_linear_lemma";
   3.716 -
   3.717 -Goal "z$<w | intify(z)=intify(w) | w$<z"; 
   3.718 -by (cut_inst_tac [("z"," intify(z)"),("w"," intify(w)")] zless_linear_lemma 1);
   3.719 -by Auto_tac;  
   3.720 -qed "zless_linear";
   3.721 -
   3.722 -Goal "~ (z$<z)";
   3.723 -by (auto_tac (claset(), 
   3.724 -              simpset() addsimps  [zless_def, znegative_def, int_of_def,
   3.725 -                                   zdiff_def]));  
   3.726 -by (rotate_tac 2 1);
   3.727 -by Auto_tac;  
   3.728 -qed "zless_not_refl";
   3.729 -AddIffs [zless_not_refl];
   3.730 -
   3.731 -Goal "[| x: int; y: int |] ==> (x ~= y) <-> (x $< y | y $< x)";
   3.732 -by (cut_inst_tac [("z","x"),("w","y")] zless_linear 1);
   3.733 -by Auto_tac;  
   3.734 -qed "neq_iff_zless";
   3.735 -
   3.736 -Goal "w $< z ==> intify(w) ~= intify(z)";
   3.737 -by Auto_tac;  
   3.738 -by (subgoal_tac "~ (intify(w) $< intify(z))" 1);
   3.739 -by (etac ssubst 2);
   3.740 -by (Full_simp_tac 1);
   3.741 -by Auto_tac;  
   3.742 -qed "zless_imp_intify_neq";
   3.743 -
   3.744 -(*This lemma allows direct proofs of other <-properties*)
   3.745 -Goalw [zless_def, znegative_def, zdiff_def, int_def] 
   3.746 -    "[| w $< z; w: int; z: int |] ==> (EX n: nat. z = w $+ $#(succ(n)))";
   3.747 -by (auto_tac (claset() addSDs [less_imp_succ_add], 
   3.748 -              simpset() addsimps [zadd, zminus, int_of_def]));  
   3.749 -by (res_inst_tac [("x","k")] bexI 1);
   3.750 -by (etac add_left_cancel 1);
   3.751 -by Auto_tac;  
   3.752 -val lemma = result();
   3.753 -
   3.754 -Goal "w $< z ==> (EX n: nat. w $+ $#(succ(n)) = intify(z))";
   3.755 -by (subgoal_tac "intify(w) $< intify(z)" 1);
   3.756 -by (dres_inst_tac [("w","intify(w)")] lemma 1);
   3.757 -by Auto_tac;  
   3.758 -qed "zless_imp_succ_zadd";
   3.759 -
   3.760 -Goalw [zless_def, znegative_def, zdiff_def, int_def] 
   3.761 -    "w : int ==> w $< w $+ $# succ(n)";
   3.762 -by (auto_tac (claset(), 
   3.763 -              simpset() addsimps [zadd, zminus, int_of_def, image_iff]));  
   3.764 -by (res_inst_tac [("x","0")] exI 1);
   3.765 -by Auto_tac;  
   3.766 -val lemma = result();
   3.767 -
   3.768 -Goal "w $< w $+ $# succ(n)";
   3.769 -by (cut_facts_tac [intify_in_int RS lemma] 1);
   3.770 -by Auto_tac;  
   3.771 -qed "zless_succ_zadd";
   3.772 -
   3.773 -Goal "w $< z <-> (EX n: nat. w $+ $#(succ(n)) = intify(z))";
   3.774 -by (rtac iffI 1);
   3.775 -by (etac zless_imp_succ_zadd 1);
   3.776 -by Auto_tac;  
   3.777 -by (rename_tac "n" 1);
   3.778 -by (cut_inst_tac [("w","w"),("n","n")] zless_succ_zadd 1);
   3.779 -by Auto_tac;  
   3.780 -qed "zless_iff_succ_zadd";
   3.781 -
   3.782 -Goal "[| m: nat; n: nat |] ==> ($#m $< $#n) <-> (m<n)";
   3.783 -by (asm_simp_tac (simpset() addsimps [less_iff_succ_add, zless_iff_succ_zadd, 
   3.784 -	 		  	      int_of_add RS sym]) 1);
   3.785 -by (blast_tac (claset() addIs [sym]) 1); 
   3.786 -qed "zless_int_of";
   3.787 -Addsimps [zless_int_of];
   3.788 -
   3.789 -Goalw [zless_def, znegative_def, zdiff_def, int_def] 
   3.790 -    "[| x $< y; y $< z; x: int; y : int; z: int |] ==> x $< z"; 
   3.791 -by (auto_tac (claset(), simpset() addsimps [zadd, zminus, image_iff]));
   3.792 -by (rename_tac "x1 x2 y1 y2" 1);
   3.793 -by (res_inst_tac [("x","x1#+x2")] exI 1);  
   3.794 -by (res_inst_tac [("x","y1#+y2")] exI 1);  
   3.795 -by (auto_tac (claset(), simpset() addsimps [add_lt_mono]));  
   3.796 -by (rtac sym 1);
   3.797 -by (REPEAT (etac add_left_cancel 1));
   3.798 -by Auto_tac;  
   3.799 -qed "zless_trans_lemma";
   3.800 -
   3.801 -Goal "[| x $< y; y $< z |] ==> x $< z"; 
   3.802 -by (subgoal_tac "intify(x) $< intify(z)" 1);
   3.803 -by (res_inst_tac [("y", "intify(y)")] zless_trans_lemma 2);
   3.804 -by Auto_tac;  
   3.805 -qed "zless_trans";
   3.806 -
   3.807 -Goal "z $< w ==> ~ (w $< z)";
   3.808 -by (blast_tac (claset() addDs [zless_trans]) 1);
   3.809 -qed "zless_not_sym";
   3.810 -
   3.811 -(* [| z $< w; ~ P ==> w $< z |] ==> P *)
   3.812 -bind_thm ("zless_asym", zless_not_sym RS swap);
   3.813 -
   3.814 -Goalw [zle_def] "z $< w ==> z $<= w";
   3.815 -by (blast_tac (claset() addEs [zless_asym]) 1);
   3.816 -qed "zless_imp_zle";
   3.817 -
   3.818 -Goal "z $<= w | w $<= z";
   3.819 -by (simp_tac (simpset() addsimps [zle_def]) 1);
   3.820 -by (cut_facts_tac [zless_linear] 1);
   3.821 -by (Blast_tac 1);
   3.822 -qed "zle_linear";
   3.823 -
   3.824 -
   3.825 -(*** "Less Than or Equals", $<= ***)
   3.826 -
   3.827 -Goalw [zle_def] "z $<= z";
   3.828 -by Auto_tac;  
   3.829 -qed "zle_refl";
   3.830 -
   3.831 -Goal "x=y ==> x $<= y";
   3.832 -by (asm_simp_tac (simpset() addsimps [zle_refl]) 1);
   3.833 -qed "zle_eq_refl";
   3.834 -
   3.835 -Goalw [zle_def] "[| x $<= y; y $<= x |] ==> intify(x) = intify(y)";
   3.836 -by Auto_tac;  
   3.837 -by (blast_tac (claset() addDs [zless_trans]) 1);
   3.838 -qed "zle_anti_sym_intify";
   3.839 -
   3.840 -Goal "[| x $<= y; y $<= x; x: int; y: int |] ==> x=y"; 
   3.841 -by (dtac zle_anti_sym_intify 1);
   3.842 -by Auto_tac;  
   3.843 -qed "zle_anti_sym";
   3.844 -
   3.845 -Goalw [zle_def] "[| x: int; y: int; z: int; x $<= y; y $<= z |] ==> x $<= z";
   3.846 -by Auto_tac;  
   3.847 -by (blast_tac (claset() addIs [zless_trans]) 1);
   3.848 -val lemma = result();
   3.849 -
   3.850 -Goal "[| x $<= y; y $<= z |] ==> x $<= z";
   3.851 -by (subgoal_tac "intify(x) $<= intify(z)" 1);
   3.852 -by (res_inst_tac [("y", "intify(y)")] lemma 2);
   3.853 -by Auto_tac;  
   3.854 -qed "zle_trans";
   3.855 -
   3.856 -Goal "[| i $<= j; j $< k |] ==> i $< k";
   3.857 -by (auto_tac (claset(), simpset() addsimps [zle_def]));  
   3.858 -by (blast_tac (claset() addIs [zless_trans]) 1);
   3.859 -by (asm_full_simp_tac (simpset() addsimps [zless_def, zdiff_def, zadd_def]) 1);
   3.860 -qed "zle_zless_trans";
   3.861 -
   3.862 -Goal "[| i $< j; j $<= k |] ==> i $< k";
   3.863 -by (auto_tac (claset(), simpset() addsimps [zle_def]));  
   3.864 -by (blast_tac (claset() addIs [zless_trans]) 1);
   3.865 -by (asm_full_simp_tac
   3.866 -    (simpset() addsimps [zless_def, zdiff_def, zminus_def]) 1);
   3.867 -qed "zless_zle_trans";
   3.868 -
   3.869 -Goal "~ (z $< w) <-> (w $<= z)";
   3.870 -by (cut_inst_tac [("z","z"),("w","w")] zless_linear 1);
   3.871 -by (auto_tac (claset() addDs [zless_trans], simpset() addsimps [zle_def]));  
   3.872 -by (auto_tac (claset() addSDs [zless_imp_intify_neq],  simpset()));
   3.873 -qed "not_zless_iff_zle";
   3.874 -
   3.875 -Goal "~ (z $<= w) <-> (w $< z)";
   3.876 -by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
   3.877 -qed "not_zle_iff_zless";
   3.878 -
   3.879 -
   3.880 -(*** More subtraction laws (for zcompare_rls) ***)
   3.881 -
   3.882 -Goal "(x $- y) $- z = x $- (y $+ z)";
   3.883 -by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   3.884 -qed "zdiff_zdiff_eq";
   3.885 -
   3.886 -Goal "x $- (y $- z) = (x $+ z) $- y";
   3.887 -by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   3.888 -qed "zdiff_zdiff_eq2";
   3.889 -
   3.890 -Goalw [zless_def, zdiff_def] "(x$-y $< z) <-> (x $< z $+ y)";
   3.891 -by (simp_tac (simpset() addsimps zadd_ac) 1);
   3.892 -qed "zdiff_zless_iff";
   3.893 -
   3.894 -Goalw [zless_def, zdiff_def] "(x $< z$-y) <-> (x $+ y $< z)";
   3.895 -by (simp_tac (simpset() addsimps zadd_ac) 1);
   3.896 -qed "zless_zdiff_iff";
   3.897 -
   3.898 -Goalw [zdiff_def] "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)";
   3.899 -by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
   3.900 -qed "zdiff_eq_iff";
   3.901 -
   3.902 -Goalw [zdiff_def] "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)";
   3.903 -by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
   3.904 -qed "eq_zdiff_iff";
   3.905 -
   3.906 -Goalw [zle_def] "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)";
   3.907 -by (auto_tac (claset(), simpset() addsimps [zdiff_eq_iff, zdiff_zless_iff]));  
   3.908 -val lemma = result();
   3.909 -
   3.910 -Goal "(x$-y $<= z) <-> (x $<= z $+ y)";
   3.911 -by (cut_facts_tac [[intify_in_int, intify_in_int] MRS lemma] 1);
   3.912 -by (Asm_full_simp_tac 1);
   3.913 -qed "zdiff_zle_iff";
   3.914 -
   3.915 -Goalw [zle_def] "[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)";
   3.916 -by (auto_tac (claset(), simpset() addsimps [zdiff_eq_iff, zless_zdiff_iff]));  
   3.917 -by (auto_tac (claset(), simpset() addsimps [zdiff_def, zadd_assoc]));  
   3.918 -val lemma = result();
   3.919 -
   3.920 -Goal "(x $<= z$-y) <-> (x $+ y $<= z)";
   3.921 -by (cut_facts_tac [[intify_in_int, intify_in_int] MRS lemma] 1);
   3.922 -by (Asm_full_simp_tac 1);
   3.923 -qed "zle_zdiff_iff";
   3.924 -
   3.925 -(*This list of rewrites simplifies (in)equalities by bringing subtractions
   3.926 -  to the top and then moving negative terms to the other side.  
   3.927 -  Use with zadd_ac*)
   3.928 -bind_thms ("zcompare_rls",
   3.929 -    [symmetric zdiff_def,
   3.930 -     zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, 
   3.931 -     zdiff_zless_iff, zless_zdiff_iff, zdiff_zle_iff, zle_zdiff_iff, 
   3.932 -     zdiff_eq_iff, eq_zdiff_iff]);
   3.933 -
   3.934 -
   3.935 -(*** Monotonicity/cancellation results that could allow instantiation
   3.936 -     of the CancelNumerals simprocs ***)
   3.937 -
   3.938 -Goal "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)";
   3.939 -by Safe_tac;
   3.940 -by (dres_inst_tac [("t", "%x. x $+ ($-z)")] subst_context 1);
   3.941 -by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
   3.942 -qed "zadd_left_cancel";
   3.943 -
   3.944 -Goal "(z $+ w' = z $+ w) <-> intify(w') = intify(w)";
   3.945 -by (rtac iff_trans 1);
   3.946 -by (rtac zadd_left_cancel 2);
   3.947 -by Auto_tac;  
   3.948 -qed "zadd_left_cancel_intify";
   3.949 -
   3.950 -Addsimps [zadd_left_cancel_intify];
   3.951 -
   3.952 -Goal "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)";
   3.953 -by Safe_tac;
   3.954 -by (dres_inst_tac [("t", "%x. x $+ ($-z)")] subst_context 1);
   3.955 -by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
   3.956 -qed "zadd_right_cancel";
   3.957 -
   3.958 -Goal "(w' $+ z = w $+ z) <-> intify(w') = intify(w)";
   3.959 -by (rtac iff_trans 1);
   3.960 -by (rtac zadd_right_cancel 2);
   3.961 -by Auto_tac;  
   3.962 -qed "zadd_right_cancel_intify";
   3.963 -
   3.964 -Addsimps [zadd_right_cancel_intify];
   3.965 -
   3.966 -
   3.967 -Goal "(w' $+ z $< w $+ z) <-> (w' $< w)";
   3.968 -by (simp_tac (simpset() addsimps [zdiff_zless_iff RS iff_sym]) 1);
   3.969 -by (simp_tac (simpset() addsimps [zdiff_def, zadd_assoc]) 1);
   3.970 -qed "zadd_right_cancel_zless";
   3.971 -
   3.972 -Goal "(z $+ w' $< z $+ w) <-> (w' $< w)";
   3.973 -by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
   3.974 -                                  zadd_right_cancel_zless]) 1);
   3.975 -qed "zadd_left_cancel_zless";
   3.976 -
   3.977 -Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
   3.978 -
   3.979 -
   3.980 -Goal "(w' $+ z $<= w $+ z) <-> w' $<= w";
   3.981 -by (simp_tac (simpset() addsimps [zle_def]) 1);
   3.982 -qed "zadd_right_cancel_zle";
   3.983 -
   3.984 -Goal "(z $+ w' $<= z $+ w) <->  w' $<= w";
   3.985 -by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
   3.986 -                                  zadd_right_cancel_zle]) 1);
   3.987 -qed "zadd_left_cancel_zle";
   3.988 -
   3.989 -Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
   3.990 -
   3.991 -
   3.992 -(*"v $<= w ==> v$+z $<= w$+z"*)
   3.993 -bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2);
   3.994 -
   3.995 -(*"v $<= w ==> z$+v $<= z$+w"*)
   3.996 -bind_thm ("zadd_zless_mono2", zadd_left_cancel_zless RS iffD2);
   3.997 -
   3.998 -(*"v $<= w ==> v$+z $<= w$+z"*)
   3.999 -bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2);
  3.1000 -
  3.1001 -(*"v $<= w ==> z$+v $<= z$+w"*)
  3.1002 -bind_thm ("zadd_zle_mono2", zadd_left_cancel_zle RS iffD2);
  3.1003 -
  3.1004 -Goal "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z";
  3.1005 -by (etac (zadd_zle_mono1 RS zle_trans) 1);
  3.1006 -by (Simp_tac 1);
  3.1007 -qed "zadd_zle_mono";
  3.1008 -
  3.1009 -Goal "[| w' $< w; z' $<= z |] ==> w' $+ z' $< w $+ z";
  3.1010 -by (etac (zadd_zless_mono1 RS zless_zle_trans) 1);
  3.1011 -by (Simp_tac 1);
  3.1012 -qed "zadd_zless_mono";
  3.1013 -
  3.1014 -
  3.1015 -(*** Comparison laws ***)
  3.1016 -
  3.1017 -Goal "($- x $< $- y) <-> (y $< x)";
  3.1018 -by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
  3.1019 -qed "zminus_zless_zminus"; 
  3.1020 -Addsimps [zminus_zless_zminus];
  3.1021 -
  3.1022 -Goal "($- x $<= $- y) <-> (y $<= x)";
  3.1023 -by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
  3.1024 -qed "zminus_zle_zminus"; 
  3.1025 -Addsimps [zminus_zle_zminus];
  3.1026 -
  3.1027 -
  3.1028 -(*** More inequality lemmas ***)
  3.1029 -
  3.1030 -Goal "[| x: int;  y: int |] ==> (x = $- y) <-> (y = $- x)";
  3.1031 -by Auto_tac;
  3.1032 -qed "equation_zminus";
  3.1033 -
  3.1034 -Goal "[| x: int;  y: int |] ==> ($- x = y) <-> ($- y = x)";
  3.1035 -by Auto_tac;
  3.1036 -qed "zminus_equation";
  3.1037 -
  3.1038 -Goal "(intify(x) = $- y) <-> (intify(y) = $- x)";
  3.1039 -by (cut_inst_tac [("x","intify(x)"), ("y","intify(y)")] equation_zminus 1);
  3.1040 -by Auto_tac;
  3.1041 -qed "equation_zminus_intify";
  3.1042 -
  3.1043 -Goal "($- x = intify(y)) <-> ($- y = intify(x))";
  3.1044 -by (cut_inst_tac [("x","intify(x)"), ("y","intify(y)")] zminus_equation 1);
  3.1045 -by Auto_tac;
  3.1046 -qed "zminus_equation_intify";
  3.1047 -
  3.1048 -
  3.1049 -(** The next several equations are permutative: watch out! **)
  3.1050 -
  3.1051 -Goal "(x $< $- y) <-> (y $< $- x)";
  3.1052 -by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
  3.1053 -qed "zless_zminus"; 
  3.1054 -
  3.1055 -Goal "($- x $< y) <-> ($- y $< x)";
  3.1056 -by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
  3.1057 -qed "zminus_zless"; 
  3.1058 -
  3.1059 -Goal "(x $<= $- y) <-> (y $<= $- x)";
  3.1060 -by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, 
  3.1061 -                                  zminus_zless]) 1);
  3.1062 -qed "zle_zminus"; 
  3.1063 -
  3.1064 -Goal "($- x $<= y) <-> ($- y $<= x)";
  3.1065 -by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, 
  3.1066 -                                  zless_zminus]) 1);
  3.1067 -qed "zminus_zle"; 
     4.1 --- a/src/ZF/Integ/Int.thy	Thu Sep 05 14:03:03 2002 +0200
     4.2 +++ b/src/ZF/Integ/Int.thy	Sat Sep 07 22:04:28 2002 +0200
     4.3 @@ -3,51 +3,52 @@
     4.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.5      Copyright   1993  University of Cambridge
     4.6  
     4.7 -The integers as equivalence classes over nat*nat.
     4.8  *)
     4.9  
    4.10 -Int = EquivClass + ArithSimp +
    4.11 +header{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*}
    4.12 +
    4.13 +theory Int = EquivClass + ArithSimp:
    4.14  
    4.15  constdefs
    4.16    intrel :: i
    4.17 -    "intrel == {p:(nat*nat)*(nat*nat).                 
    4.18 +    "intrel == {p : (nat*nat)*(nat*nat).                 
    4.19                  EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    4.20  
    4.21    int :: i
    4.22      "int == (nat*nat)//intrel"  
    4.23  
    4.24 -  int_of :: i=>i (*coercion from nat to int*)    ("$# _" [80] 80)
    4.25 +  int_of :: "i=>i" --{*coercion from nat to int*}    ("$# _" [80] 80)
    4.26      "$# m == intrel `` {<natify(m), 0>}"
    4.27  
    4.28 -  intify :: i=>i (*coercion from ANYTHING to int*) 
    4.29 +  intify :: "i=>i" --{*coercion from ANYTHING to int*}
    4.30      "intify(m) == if m : int then m else $#0"
    4.31  
    4.32 -  raw_zminus :: i=>i
    4.33 +  raw_zminus :: "i=>i"
    4.34      "raw_zminus(z) == UN <x,y>: z. intrel``{<y,x>}"
    4.35  
    4.36 -  zminus :: i=>i                                 ("$- _" [80] 80)
    4.37 +  zminus :: "i=>i"                                 ("$- _" [80] 80)
    4.38      "$- z == raw_zminus (intify(z))"
    4.39  
    4.40 -  znegative   ::      i=>o
    4.41 +  znegative   ::      "i=>o"
    4.42      "znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
    4.43  
    4.44 -  iszero      ::      i=>o
    4.45 +  iszero      ::      "i=>o"
    4.46      "iszero(z) == z = $# 0"
    4.47      
    4.48 -  raw_nat_of  :: i => i
    4.49 +  raw_nat_of  :: "i=>i"
    4.50    "raw_nat_of(z) == if znegative(z) then 0
    4.51                      else (THE m. m: nat & z = int_of(m))"
    4.52  
    4.53 -  nat_of  :: i => i
    4.54 +  nat_of  :: "i=>i"
    4.55    "nat_of(z) == raw_nat_of (intify(z))"
    4.56  
    4.57 -  (*could be replaced by an absolute value function from int to int?*)
    4.58 -  zmagnitude  ::      i=>i
    4.59 +  zmagnitude  ::      "i=>i"
    4.60 +  --{*could be replaced by an absolute value function from int to int?*}
    4.61      "zmagnitude(z) ==
    4.62       THE m. m : nat & ((~ znegative(z) & z = $# m) |
    4.63  		       (znegative(z) & $- z = $# m))"
    4.64  
    4.65 -  raw_zmult   ::      [i,i]=>i
    4.66 +  raw_zmult   ::      "[i,i]=>i"
    4.67      (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
    4.68        Perhaps a "curried" or even polymorphic congruent predicate would be
    4.69        better.*)
    4.70 @@ -55,31 +56,1069 @@
    4.71         UN p1:z1. UN p2:z2.  split(%x1 y1. split(%x2 y2.        
    4.72                     intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
    4.73  
    4.74 -  zmult       ::      [i,i]=>i      (infixl "$*" 70)
    4.75 +  zmult       ::      "[i,i]=>i"      (infixl "$*" 70)
    4.76       "z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
    4.77  
    4.78 -  raw_zadd    ::      [i,i]=>i
    4.79 +  raw_zadd    ::      "[i,i]=>i"
    4.80       "raw_zadd (z1, z2) == 
    4.81         UN z1:z1. UN z2:z2. let <x1,y1>=z1; <x2,y2>=z2                 
    4.82                             in intrel``{<x1#+x2, y1#+y2>}"
    4.83  
    4.84 -  zadd        ::      [i,i]=>i      (infixl "$+" 65)
    4.85 +  zadd        ::      "[i,i]=>i"      (infixl "$+" 65)
    4.86       "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
    4.87  
    4.88 -  zdiff        ::      [i,i]=>i      (infixl "$-" 65)
    4.89 +  zdiff        ::      "[i,i]=>i"      (infixl "$-" 65)
    4.90       "z1 $- z2 == z1 $+ zminus(z2)"
    4.91  
    4.92 -  zless        ::      [i,i]=>o      (infixl "$<" 50)
    4.93 +  zless        ::      "[i,i]=>o"      (infixl "$<" 50)
    4.94       "z1 $< z2 == znegative(z1 $- z2)"
    4.95    
    4.96 -  zle          ::      [i,i]=>o      (infixl "$<=" 50)
    4.97 +  zle          ::      "[i,i]=>o"      (infixl "$<=" 50)
    4.98       "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
    4.99    
   4.100  
   4.101  syntax (xsymbols)
   4.102 -  "zmult"     :: [i,i] => i          (infixl "$\\<times>" 70)
   4.103 -  "zle"       :: [i,i] => o          (infixl "$\\<le>" 50)  (*less than / equals*)
   4.104 +  zmult :: "[i,i]=>i"          (infixl "$\<times>" 70)
   4.105 +  zle   :: "[i,i]=>o"          (infixl "$\<le>" 50)  --{*less than or equals*}
   4.106  
   4.107  syntax (HTML output)
   4.108 -  "zmult"     :: [i,i] => i          (infixl "$\\<times>" 70)
   4.109 +  zmult :: "[i,i]=>i"          (infixl "$\<times>" 70)
   4.110 +
   4.111 +
   4.112 +declare quotientE [elim!]
   4.113 +
   4.114 +subsection{*Proving that @{term intrel} is an equivalence relation*}
   4.115 +
   4.116 +(** Natural deduction for intrel **)
   4.117 +
   4.118 +lemma intrel_iff [simp]: 
   4.119 +    "<<x1,y1>,<x2,y2>>: intrel <->  
   4.120 +     x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1"
   4.121 +by (unfold intrel_def, fast)
   4.122 +
   4.123 +lemma intrelI [intro!]: 
   4.124 +    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |]   
   4.125 +     ==> <<x1,y1>,<x2,y2>>: intrel"
   4.126 +by (unfold intrel_def, fast)
   4.127 +
   4.128 +lemma intrelE [elim!]:
   4.129 +  "[| p: intrel;   
   4.130 +      !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1;  
   4.131 +                        x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |]  
   4.132 +   ==> Q"
   4.133 +by (unfold intrel_def, blast) 
   4.134 +
   4.135 +lemma int_trans_lemma:
   4.136 +     "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1"
   4.137 +apply (rule sym)
   4.138 +apply (erule add_left_cancel)+
   4.139 +apply (simp_all (no_asm_simp))
   4.140 +done
   4.141 +
   4.142 +lemma equiv_intrel: "equiv(nat*nat, intrel)"
   4.143 +apply (unfold equiv_def refl_def sym_def trans_def)
   4.144 +apply (fast elim!: sym int_trans_lemma)
   4.145 +done
   4.146 +
   4.147 +lemma image_intrel_int: "[| m: nat; n: nat |] ==> intrel `` {<m,n>} : int"
   4.148 +apply (unfold int_def)
   4.149 +apply (blast intro: quotientI)
   4.150 +done
   4.151 +
   4.152 +declare equiv_intrel [THEN eq_equiv_class_iff, simp]
   4.153 +declare conj_cong [cong]
   4.154 +
   4.155 +lemmas eq_intrelD = eq_equiv_class [OF _ equiv_intrel]
   4.156 +
   4.157 +(** int_of: the injection from nat to int **)
   4.158 +
   4.159 +lemma int_of_type [simp,TC]: "$#m : int"
   4.160 +by (unfold int_def quotient_def int_of_def, auto)
   4.161 +
   4.162 +lemma int_of_eq [iff]: "($# m = $# n) <-> natify(m)=natify(n)"
   4.163 +by (unfold int_of_def, auto)
   4.164 +
   4.165 +lemma int_of_inject: "[| $#m = $#n;  m: nat;  n: nat |] ==> m=n"
   4.166 +by (drule int_of_eq [THEN iffD1], auto)
   4.167 +
   4.168 +
   4.169 +(** intify: coercion from anything to int **)
   4.170 +
   4.171 +lemma intify_in_int [iff,TC]: "intify(x) : int"
   4.172 +by (simp add: intify_def)
   4.173 +
   4.174 +lemma intify_ident [simp]: "n : int ==> intify(n) = n"
   4.175 +by (simp add: intify_def)
   4.176 +
   4.177 +
   4.178 +subsection{*Collapsing rules: to remove @{term intify}
   4.179 +            from arithmetic expressions*}
   4.180 +
   4.181 +lemma intify_idem [simp]: "intify(intify(x)) = intify(x)"
   4.182 +by simp
   4.183 +
   4.184 +lemma int_of_natify [simp]: "$# (natify(m)) = $# m"
   4.185 +by (simp add: int_of_def)
   4.186 +
   4.187 +lemma zminus_intify [simp]: "$- (intify(m)) = $- m"
   4.188 +by (simp add: zminus_def)
   4.189 +
   4.190 +(** Addition **)
   4.191 +
   4.192 +lemma zadd_intify1 [simp]: "intify(x) $+ y = x $+ y"
   4.193 +by (simp add: zadd_def)
   4.194 +
   4.195 +lemma zadd_intify2 [simp]: "x $+ intify(y) = x $+ y"
   4.196 +by (simp add: zadd_def)
   4.197 +
   4.198 +(** Subtraction **)
   4.199 +
   4.200 +lemma zdiff_intify1 [simp]:"intify(x) $- y = x $- y"
   4.201 +by (simp add: zdiff_def)
   4.202 +
   4.203 +lemma zdiff_intify2 [simp]:"x $- intify(y) = x $- y"
   4.204 +by (simp add: zdiff_def)
   4.205 +
   4.206 +(** Multiplication **)
   4.207 +
   4.208 +lemma zmult_intify1 [simp]:"intify(x) $* y = x $* y"
   4.209 +by (simp add: zmult_def)
   4.210 +
   4.211 +lemma zmult_intify2 [simp]:"x $* intify(y) = x $* y"
   4.212 +by (simp add: zmult_def)
   4.213 +
   4.214 +(** Orderings **)
   4.215 +
   4.216 +lemma zless_intify1 [simp]:"intify(x) $< y <-> x $< y"
   4.217 +by (simp add: zless_def)
   4.218 +
   4.219 +lemma zless_intify2 [simp]:"x $< intify(y) <-> x $< y"
   4.220 +by (simp add: zless_def)
   4.221 +
   4.222 +lemma zle_intify1 [simp]:"intify(x) $<= y <-> x $<= y"
   4.223 +by (simp add: zle_def)
   4.224 +
   4.225 +lemma zle_intify2 [simp]:"x $<= intify(y) <-> x $<= y"
   4.226 +by (simp add: zle_def)
   4.227 +
   4.228 +
   4.229 +subsection{*@{term zminus}: unary negation on @{term int}*}
   4.230 +
   4.231 +lemma zminus_congruent: "congruent(intrel, %<x,y>. intrel``{<y,x>})"
   4.232 +apply (unfold congruent_def, safe)
   4.233 +apply (simp add: add_ac)
   4.234 +done
   4.235 +
   4.236 +lemma raw_zminus_type: "z : int ==> raw_zminus(z) : int"
   4.237 +apply (unfold int_def raw_zminus_def)
   4.238 +apply (typecheck add: UN_equiv_class_type [OF equiv_intrel zminus_congruent])
   4.239 +done
   4.240 +
   4.241 +lemma zminus_type [TC,iff]: "$-z : int"
   4.242 +apply (unfold zminus_def)
   4.243 +apply (simp add: zminus_def raw_zminus_type)
   4.244 +done
   4.245 +
   4.246 +lemma raw_zminus_inject: 
   4.247 +     "[| raw_zminus(z) = raw_zminus(w);  z: int;  w: int |] ==> z=w"
   4.248 +apply (unfold int_def raw_zminus_def)
   4.249 +apply (erule UN_equiv_class_inject [OF equiv_intrel zminus_congruent], safe)
   4.250 +apply (auto dest: eq_intrelD simp add: add_ac)
   4.251 +done
   4.252 +
   4.253 +lemma zminus_inject_intify [dest!]: "$-z = $-w ==> intify(z) = intify(w)"
   4.254 +apply (unfold zminus_def)
   4.255 +apply (blast dest!: raw_zminus_inject)
   4.256 +done
   4.257 +
   4.258 +lemma zminus_inject: "[| $-z = $-w;  z: int;  w: int |] ==> z=w"
   4.259 +by auto
   4.260 +
   4.261 +lemma raw_zminus: 
   4.262 +    "[| x: nat;  y: nat |] ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}"
   4.263 +apply (unfold raw_zminus_def)
   4.264 +apply (simp add: UN_equiv_class [OF equiv_intrel zminus_congruent])
   4.265 +done
   4.266 +
   4.267 +lemma zminus: 
   4.268 +    "[| x: nat;  y: nat |]  
   4.269 +     ==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}"
   4.270 +apply (unfold zminus_def)
   4.271 +apply (simp (no_asm_simp) add: raw_zminus image_intrel_int)
   4.272 +done
   4.273 +
   4.274 +lemma raw_zminus_zminus: "z : int ==> raw_zminus (raw_zminus(z)) = z"
   4.275 +apply (unfold int_def)
   4.276 +apply (auto simp add: raw_zminus)
   4.277 +done
   4.278 +
   4.279 +lemma zminus_zminus_intify [simp]: "$- ($- z) = intify(z)"
   4.280 +by (simp add: zminus_def raw_zminus_type raw_zminus_zminus)
   4.281 +
   4.282 +lemma zminus_int0 [simp]: "$- ($#0) = $#0"
   4.283 +apply (unfold int_of_def)
   4.284 +apply (simp add: zminus)
   4.285 +done
   4.286 +
   4.287 +lemma zminus_zminus: "z : int ==> $- ($- z) = z"
   4.288 +by simp
   4.289 +
   4.290 +
   4.291 +subsection{*@{term znegative}: the test for negative integers*}
   4.292 +
   4.293 +(*No natural number is negative!*)
   4.294 +lemma not_znegative_int_of [iff]: "~ znegative($# n)"
   4.295 +apply (unfold znegative_def int_of_def, safe)
   4.296 +apply (drule_tac psi = "?lhs=?rhs" in asm_rl)
   4.297 +apply (drule_tac psi = "?lhs<?rhs" in asm_rl)
   4.298 +apply (force simp add: add_le_self2 [THEN le_imp_not_lt] natify_succ)
   4.299 +done
   4.300 +
   4.301 +lemma znegative_zminus_int_of [simp]: "znegative($- $# succ(n))"
   4.302 +apply (unfold znegative_def int_of_def)
   4.303 +apply (simp (no_asm_simp) add: zminus natify_succ)
   4.304 +apply (blast intro: nat_0_le)
   4.305 +done
   4.306 +
   4.307 +lemma not_znegative_imp_zero: "~ znegative($- $# n) ==> natify(n)=0"
   4.308 +apply (unfold znegative_def int_of_def)
   4.309 +apply (simp add: zminus image_singleton_iff)
   4.310 +apply (drule_tac x = 0 in spec)
   4.311 +apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff, THEN iff_sym])
   4.312 +done
   4.313 +
   4.314 +
   4.315 +subsection{*@{term nat_of}: Coercion of an Integer to a Natural Number*}
   4.316 +
   4.317 +lemma nat_of_intify [simp]: "nat_of(intify(z)) = nat_of(z)"
   4.318 +by (unfold nat_of_def, auto)
   4.319 +
   4.320 +lemma nat_of_int_of [simp]: "nat_of($# n) = natify(n)"
   4.321 +apply (unfold nat_of_def raw_nat_of_def)
   4.322 +apply (auto simp add: int_of_eq)
   4.323 +done
   4.324 +
   4.325 +lemma raw_nat_of_type: "raw_nat_of(z) : nat"
   4.326 +apply (unfold raw_nat_of_def, auto)
   4.327 +apply (case_tac "EX! m. m: nat & z = int_of (m) ")
   4.328 +apply (rule theI2)
   4.329 +apply (simp_all add: the_0) 
   4.330 +done
   4.331 +
   4.332 +lemma nat_of_type [iff,TC]: "nat_of(z) : nat"
   4.333 +apply (unfold nat_of_def)
   4.334 +apply (simp add: raw_nat_of_type)
   4.335 +done
   4.336 +
   4.337 +subsection{*zmagnitude: magnitide of an integer, as a natural number*}
   4.338 +
   4.339 +lemma zmagnitude_int_of [simp]: "zmagnitude($# n) = natify(n)"
   4.340 +apply (unfold zmagnitude_def)
   4.341 +apply (auto simp add: int_of_eq)
   4.342 +done
   4.343 +
   4.344 +lemma natify_int_of_eq: "natify(x)=n ==> $#x = $# n"
   4.345 +apply (drule sym)
   4.346 +apply (simp (no_asm_simp) add: int_of_eq)
   4.347 +done
   4.348 +
   4.349 +lemma zmagnitude_zminus_int_of [simp]: "zmagnitude($- $# n) = natify(n)"
   4.350 +apply (unfold zmagnitude_def)
   4.351 +apply (rule the_equality)
   4.352 +apply (auto dest!: not_znegative_imp_zero natify_int_of_eq
   4.353 +            iff del: int_of_eq, auto)
   4.354 +done
   4.355 +
   4.356 +lemma zmagnitude_type [iff,TC]: "zmagnitude(z) : nat"
   4.357 +apply (unfold zmagnitude_def)
   4.358 +apply (rule theI2, auto)
   4.359 +done
   4.360 +
   4.361 +lemma not_zneg_int_of: 
   4.362 +     "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"
   4.363 +apply (unfold int_def znegative_def int_of_def)
   4.364 +apply (auto simp add: image_singleton_iff)
   4.365 +apply (rename_tac i j)
   4.366 +apply (drule_tac x = i in spec)
   4.367 +apply (drule_tac x = j in spec)
   4.368 +apply (rule bexI)
   4.369 +apply (rule add_diff_inverse2 [symmetric], auto)
   4.370 +apply (simp add: not_lt_iff_le)
   4.371 +done
   4.372 +
   4.373 +lemma not_zneg_mag [simp]:
   4.374 +     "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"
   4.375 +by (drule not_zneg_int_of, auto)
   4.376 +
   4.377 +lemma zneg_int_of: 
   4.378 +     "[| znegative(z); z: int |] ==> EX n:nat. z = $- ($# succ(n))"
   4.379 +apply (unfold int_def znegative_def int_of_def)
   4.380 +apply (auto dest!: less_imp_succ_add simp add: zminus image_singleton_iff)
   4.381 +done
   4.382 +
   4.383 +lemma zneg_mag [simp]:
   4.384 +     "[| znegative(z); z: int |] ==> $# (zmagnitude(z)) = $- z"
   4.385 +apply (drule zneg_int_of, auto)
   4.386 +done
   4.387 +
   4.388 +lemma int_cases: "z : int ==> EX n: nat. z = $# n | z = $- ($# succ(n))"
   4.389 +apply (case_tac "znegative (z) ")
   4.390 +prefer 2 apply (blast dest: not_zneg_mag sym)
   4.391 +apply (blast dest: zneg_int_of)
   4.392 +done
   4.393 +
   4.394 +lemma not_zneg_raw_nat_of:
   4.395 +     "[| ~ znegative(z); z: int |] ==> $# (raw_nat_of(z)) = z"
   4.396 +apply (drule not_zneg_int_of)
   4.397 +apply (auto simp add: raw_nat_of_type)
   4.398 +apply (auto simp add: raw_nat_of_def)
   4.399 +done
   4.400 +
   4.401 +lemma not_zneg_nat_of_intify:
   4.402 +     "~ znegative(intify(z)) ==> $# (nat_of(z)) = intify(z)"
   4.403 +by (simp (no_asm_simp) add: nat_of_def not_zneg_raw_nat_of)
   4.404 +
   4.405 +lemma not_zneg_nat_of: "[| ~ znegative(z); z: int |] ==> $# (nat_of(z)) = z"
   4.406 +apply (simp (no_asm_simp) add: not_zneg_nat_of_intify)
   4.407 +done
   4.408 +
   4.409 +lemma zneg_nat_of [simp]: "znegative(intify(z)) ==> nat_of(z) = 0"
   4.410 +by (unfold nat_of_def raw_nat_of_def, auto)
   4.411 +
   4.412 +
   4.413 +subsection{*@{term zadd}: addition on int*}
   4.414 +
   4.415 +text{*Congruence Property for Addition*}
   4.416 +lemma zadd_congruent2: 
   4.417 +    "congruent2(intrel, %z1 z2.                       
   4.418 +          let <x1,y1>=z1; <x2,y2>=z2                  
   4.419 +                            in intrel``{<x1#+x2, y1#+y2>})"
   4.420 +apply (unfold congruent2_def)
   4.421 +(*Proof via congruent2_commuteI seems longer*)
   4.422 +apply safe
   4.423 +apply (simp (no_asm_simp) add: add_assoc Let_def)
   4.424 +(*The rest should be trivial, but rearranging terms is hard
   4.425 +  add_ac does not help rewriting with the assumptions.*)
   4.426 +apply (rule_tac m1 = x1a in add_left_commute [THEN ssubst])
   4.427 +apply (rule_tac m1 = x2a in add_left_commute [THEN ssubst])
   4.428 +apply (simp (no_asm_simp) add: add_assoc [symmetric])
   4.429 +done
   4.430 +
   4.431 +lemma raw_zadd_type: "[| z: int;  w: int |] ==> raw_zadd(z,w) : int"
   4.432 +apply (unfold int_def raw_zadd_def)
   4.433 +apply (rule UN_equiv_class_type2 [OF equiv_intrel zadd_congruent2], assumption+)
   4.434 +apply (simp add: Let_def)
   4.435 +done
   4.436 +
   4.437 +lemma zadd_type [iff,TC]: "z $+ w : int"
   4.438 +by (simp add: zadd_def raw_zadd_type)
   4.439 +
   4.440 +lemma raw_zadd: 
   4.441 +  "[| x1: nat; y1: nat;  x2: nat; y2: nat |]               
   4.442 +   ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =   
   4.443 +       intrel `` {<x1#+x2, y1#+y2>}"
   4.444 +apply (unfold raw_zadd_def)
   4.445 +apply (simp add: UN_equiv_class2 [OF equiv_intrel zadd_congruent2])
   4.446 +apply (simp add: Let_def)
   4.447 +done
   4.448 +
   4.449 +lemma zadd: 
   4.450 +  "[| x1: nat; y1: nat;  x2: nat; y2: nat |]          
   4.451 +   ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =   
   4.452 +       intrel `` {<x1#+x2, y1#+y2>}"
   4.453 +apply (unfold zadd_def)
   4.454 +apply (simp (no_asm_simp) add: raw_zadd image_intrel_int)
   4.455 +done
   4.456 +
   4.457 +lemma raw_zadd_int0: "z : int ==> raw_zadd ($#0,z) = z"
   4.458 +apply (unfold int_def int_of_def)
   4.459 +apply (auto simp add: raw_zadd)
   4.460 +done
   4.461 +
   4.462 +lemma zadd_int0_intify [simp]: "$#0 $+ z = intify(z)"
   4.463 +by (simp add: zadd_def raw_zadd_int0)
   4.464 +
   4.465 +lemma zadd_int0: "z: int ==> $#0 $+ z = z"
   4.466 +by simp
   4.467 +
   4.468 +lemma raw_zminus_zadd_distrib: 
   4.469 +     "[| z: int;  w: int |] ==> $- raw_zadd(z,w) = raw_zadd($- z, $- w)"
   4.470 +apply (unfold int_def)
   4.471 +apply (auto simp add: zminus raw_zadd)
   4.472 +done
   4.473 +
   4.474 +lemma zminus_zadd_distrib [simp]: "$- (z $+ w) = $- z $+ $- w"
   4.475 +by (simp add: zadd_def raw_zminus_zadd_distrib)
   4.476 +
   4.477 +lemma raw_zadd_commute:
   4.478 +     "[| z: int;  w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)"
   4.479 +apply (unfold int_def)
   4.480 +apply (auto simp add: raw_zadd add_ac)
   4.481 +done
   4.482 +
   4.483 +lemma zadd_commute: "z $+ w = w $+ z"
   4.484 +by (simp add: zadd_def raw_zadd_commute)
   4.485 +
   4.486 +lemma raw_zadd_assoc: 
   4.487 +    "[| z1: int;  z2: int;  z3: int |]    
   4.488 +     ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))"
   4.489 +apply (unfold int_def)
   4.490 +apply (auto simp add: raw_zadd add_assoc)
   4.491 +done
   4.492 +
   4.493 +lemma zadd_assoc: "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)"
   4.494 +by (simp add: zadd_def raw_zadd_type raw_zadd_assoc)
   4.495 +
   4.496 +(*For AC rewriting*)
   4.497 +lemma zadd_left_commute: "z1$+(z2$+z3) = z2$+(z1$+z3)"
   4.498 +apply (simp add: zadd_assoc [symmetric])
   4.499 +apply (simp add: zadd_commute)
   4.500 +done
   4.501 +
   4.502 +(*Integer addition is an AC operator*)
   4.503 +lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
   4.504 +
   4.505 +lemma int_of_add: "$# (m #+ n) = ($#m) $+ ($#n)"
   4.506 +apply (unfold int_of_def)
   4.507 +apply (simp add: zadd)
   4.508 +done
   4.509 +
   4.510 +lemma int_succ_int_1: "$# succ(m) = $# 1 $+ ($# m)"
   4.511 +by (simp add: int_of_add [symmetric] natify_succ)
   4.512 +
   4.513 +lemma int_of_diff: 
   4.514 +     "[| m: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)"
   4.515 +apply (unfold int_of_def zdiff_def)
   4.516 +apply (frule lt_nat_in_nat)
   4.517 +apply (simp_all add: zadd zminus add_diff_inverse2)
   4.518 +done
   4.519 +
   4.520 +lemma raw_zadd_zminus_inverse: "z : int ==> raw_zadd (z, $- z) = $#0"
   4.521 +apply (unfold int_def int_of_def)
   4.522 +apply (auto simp add: zminus raw_zadd add_commute)
   4.523 +done
   4.524 +
   4.525 +lemma zadd_zminus_inverse [simp]: "z $+ ($- z) = $#0"
   4.526 +apply (simp add: zadd_def)
   4.527 +apply (subst zminus_intify [symmetric])
   4.528 +apply (rule intify_in_int [THEN raw_zadd_zminus_inverse])
   4.529 +done
   4.530 +
   4.531 +lemma zadd_zminus_inverse2 [simp]: "($- z) $+ z = $#0"
   4.532 +by (simp add: zadd_commute zadd_zminus_inverse)
   4.533 +
   4.534 +lemma zadd_int0_right_intify [simp]: "z $+ $#0 = intify(z)"
   4.535 +by (rule trans [OF zadd_commute zadd_int0_intify])
   4.536 +
   4.537 +lemma zadd_int0_right: "z:int ==> z $+ $#0 = z"
   4.538 +by simp
   4.539 +
   4.540 +
   4.541 +subsection{*@{term zmult}: Integer Multiplication*}
   4.542 +
   4.543 +text{*Congruence property for multiplication*}
   4.544 +lemma zmult_congruent2:
   4.545 +    "congruent2(intrel, %p1 p2.                  
   4.546 +                split(%x1 y1. split(%x2 y2.      
   4.547 +                    intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))"
   4.548 +apply (rule equiv_intrel [THEN congruent2_commuteI], auto)
   4.549 +(*Proof that zmult is congruent in one argument*)
   4.550 +apply (rename_tac x y)
   4.551 +apply (frule_tac t = "%u. x#*u" in sym [THEN subst_context])
   4.552 +apply (drule_tac t = "%u. y#*u" in subst_context)
   4.553 +apply (erule add_left_cancel)+
   4.554 +apply (simp_all add: add_mult_distrib_left)
   4.555 +done
   4.556 +
   4.557 +
   4.558 +lemma raw_zmult_type: "[| z: int;  w: int |] ==> raw_zmult(z,w) : int"
   4.559 +apply (unfold int_def raw_zmult_def)
   4.560 +apply (rule UN_equiv_class_type2 [OF equiv_intrel zmult_congruent2], assumption+)
   4.561 +apply (simp add: Let_def)
   4.562 +done
   4.563 +
   4.564 +lemma zmult_type [iff,TC]: "z $* w : int"
   4.565 +by (simp add: zmult_def raw_zmult_type)
   4.566 +
   4.567 +lemma raw_zmult: 
   4.568 +     "[| x1: nat; y1: nat;  x2: nat; y2: nat |]     
   4.569 +      ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =      
   4.570 +          intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"
   4.571 +apply (unfold raw_zmult_def)
   4.572 +apply (simp add: UN_equiv_class2 [OF equiv_intrel zmult_congruent2])
   4.573 +done
   4.574 +
   4.575 +lemma zmult: 
   4.576 +     "[| x1: nat; y1: nat;  x2: nat; y2: nat |]     
   4.577 +      ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =      
   4.578 +          intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"
   4.579 +apply (unfold zmult_def)
   4.580 +apply (simp add: raw_zmult image_intrel_int)
   4.581 +done
   4.582 +
   4.583 +lemma raw_zmult_int0: "z : int ==> raw_zmult ($#0,z) = $#0"
   4.584 +apply (unfold int_def int_of_def)
   4.585 +apply (auto simp add: raw_zmult)
   4.586 +done
   4.587 +
   4.588 +lemma zmult_int0 [simp]: "$#0 $* z = $#0"
   4.589 +by (simp add: zmult_def raw_zmult_int0)
   4.590 +
   4.591 +lemma raw_zmult_int1: "z : int ==> raw_zmult ($#1,z) = z"
   4.592 +apply (unfold int_def int_of_def)
   4.593 +apply (auto simp add: raw_zmult)
   4.594 +done
   4.595 +
   4.596 +lemma zmult_int1_intify [simp]: "$#1 $* z = intify(z)"
   4.597 +by (simp add: zmult_def raw_zmult_int1)
   4.598 +
   4.599 +lemma zmult_int1: "z : int ==> $#1 $* z = z"
   4.600 +by simp
   4.601 +
   4.602 +lemma raw_zmult_commute:
   4.603 +     "[| z: int;  w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)"
   4.604 +apply (unfold int_def)
   4.605 +apply (auto simp add: raw_zmult add_ac mult_ac)
   4.606 +done
   4.607 +
   4.608 +lemma zmult_commute: "z $* w = w $* z"
   4.609 +by (simp add: zmult_def raw_zmult_commute)
   4.610 +
   4.611 +lemma raw_zmult_zminus: 
   4.612 +     "[| z: int;  w: int |] ==> raw_zmult($- z, w) = $- raw_zmult(z, w)"
   4.613 +apply (unfold int_def)
   4.614 +apply (auto simp add: zminus raw_zmult add_ac)
   4.615 +done
   4.616 +
   4.617 +lemma zmult_zminus [simp]: "($- z) $* w = $- (z $* w)"
   4.618 +apply (simp add: zmult_def raw_zmult_zminus)
   4.619 +apply (subst zminus_intify [symmetric], rule raw_zmult_zminus, auto)
   4.620 +done
   4.621 +
   4.622 +lemma zmult_zminus_right [simp]: "w $* ($- z) = $- (w $* z)"
   4.623 +by (simp add: zmult_commute [of w])
   4.624 +
   4.625 +lemma raw_zmult_assoc: 
   4.626 +    "[| z1: int;  z2: int;  z3: int |]    
   4.627 +     ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))"
   4.628 +apply (unfold int_def)
   4.629 +apply (auto simp add: raw_zmult add_mult_distrib_left add_ac mult_ac)
   4.630 +done
   4.631 +
   4.632 +lemma zmult_assoc: "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)"
   4.633 +by (simp add: zmult_def raw_zmult_type raw_zmult_assoc)
   4.634 +
   4.635 +(*For AC rewriting*)
   4.636 +lemma zmult_left_commute: "z1$*(z2$*z3) = z2$*(z1$*z3)"
   4.637 +apply (simp add: zmult_assoc [symmetric])
   4.638 +apply (simp add: zmult_commute)
   4.639 +done
   4.640 +
   4.641 +(*Integer multiplication is an AC operator*)
   4.642 +lemmas zmult_ac = zmult_assoc zmult_commute zmult_left_commute
   4.643 +
   4.644 +lemma raw_zadd_zmult_distrib: 
   4.645 +    "[| z1: int;  z2: int;  w: int |]   
   4.646 +     ==> raw_zmult(raw_zadd(z1,z2), w) =  
   4.647 +         raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))"
   4.648 +apply (unfold int_def)
   4.649 +apply (auto simp add: raw_zadd raw_zmult add_mult_distrib_left add_ac mult_ac)
   4.650 +done
   4.651 +
   4.652 +lemma zadd_zmult_distrib: "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)"
   4.653 +by (simp add: zmult_def zadd_def raw_zadd_type raw_zmult_type 
   4.654 +              raw_zadd_zmult_distrib)
   4.655 +
   4.656 +lemma zadd_zmult_distrib2: "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)"
   4.657 +by (simp add: zmult_commute [of w] zadd_zmult_distrib)
   4.658 +
   4.659 +lemmas int_typechecks = 
   4.660 +  int_of_type zminus_type zmagnitude_type zadd_type zmult_type
   4.661 +
   4.662 +
   4.663 +(*** Subtraction laws ***)
   4.664 +
   4.665 +lemma zdiff_type [iff,TC]: "z $- w : int"
   4.666 +by (simp add: zdiff_def)
   4.667 +
   4.668 +lemma zminus_zdiff_eq [simp]: "$- (z $- y) = y $- z"
   4.669 +by (simp add: zdiff_def zadd_commute)
   4.670 +
   4.671 +lemma zdiff_zmult_distrib: "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)"
   4.672 +apply (unfold zdiff_def)
   4.673 +apply (subst zadd_zmult_distrib)
   4.674 +apply (simp add: zmult_zminus)
   4.675 +done
   4.676 +
   4.677 +lemma zdiff_zmult_distrib2: "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)"
   4.678 +by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
   4.679 +
   4.680 +lemma zadd_zdiff_eq: "x $+ (y $- z) = (x $+ y) $- z"
   4.681 +by (simp add: zdiff_def zadd_ac)
   4.682 +
   4.683 +lemma zdiff_zadd_eq: "(x $- y) $+ z = (x $+ z) $- y"
   4.684 +by (simp add: zdiff_def zadd_ac)
   4.685 +
   4.686 +
   4.687 +subsection{*The "Less Than" Relation*}
   4.688 +
   4.689 +(*"Less than" is a linear ordering*)
   4.690 +lemma zless_linear_lemma: 
   4.691 +     "[| z: int; w: int |] ==> z$<w | z=w | w$<z"
   4.692 +apply (unfold int_def zless_def znegative_def zdiff_def, auto)
   4.693 +apply (simp add: zadd zminus image_iff Bex_def)
   4.694 +apply (rule_tac i = "xb#+ya" and j = "xc #+ y" in Ord_linear_lt)
   4.695 +apply (force dest!: spec simp add: add_ac)+
   4.696 +done
   4.697 +
   4.698 +lemma zless_linear: "z$<w | intify(z)=intify(w) | w$<z"
   4.699 +apply (cut_tac z = " intify (z) " and w = " intify (w) " in zless_linear_lemma)
   4.700 +apply auto
   4.701 +done
   4.702 +
   4.703 +lemma zless_not_refl [iff]: "~ (z$<z)"
   4.704 +apply (auto simp add: zless_def znegative_def int_of_def zdiff_def)
   4.705 +apply (rotate_tac 2, auto)
   4.706 +done
   4.707 +
   4.708 +lemma neq_iff_zless: "[| x: int; y: int |] ==> (x ~= y) <-> (x $< y | y $< x)"
   4.709 +by (cut_tac z = x and w = y in zless_linear, auto)
   4.710 +
   4.711 +lemma zless_imp_intify_neq: "w $< z ==> intify(w) ~= intify(z)"
   4.712 +apply auto
   4.713 +apply (subgoal_tac "~ (intify (w) $< intify (z))")
   4.714 +apply (erule_tac [2] ssubst)
   4.715 +apply (simp (no_asm_use))
   4.716 +apply auto
   4.717 +done
   4.718 +
   4.719 +(*This lemma allows direct proofs of other <-properties*)
   4.720 +lemma zless_imp_succ_zadd_lemma: 
   4.721 +    "[| w $< z; w: int; z: int |] ==> (EX n: nat. z = w $+ $#(succ(n)))"
   4.722 +apply (unfold zless_def znegative_def zdiff_def int_def)
   4.723 +apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def)
   4.724 +apply (rule_tac x = k in bexI)
   4.725 +apply (erule add_left_cancel, auto)
   4.726 +done
   4.727 +
   4.728 +lemma zless_imp_succ_zadd:
   4.729 +     "w $< z ==> (EX n: nat. w $+ $#(succ(n)) = intify(z))"
   4.730 +apply (subgoal_tac "intify (w) $< intify (z) ")
   4.731 +apply (drule_tac w = "intify (w) " in zless_imp_succ_zadd_lemma)
   4.732 +apply auto
   4.733 +done
   4.734 +
   4.735 +lemma zless_succ_zadd_lemma: 
   4.736 +    "w : int ==> w $< w $+ $# succ(n)"
   4.737 +apply (unfold zless_def znegative_def zdiff_def int_def)
   4.738 +apply (auto simp add: zadd zminus int_of_def image_iff)
   4.739 +apply (rule_tac x = 0 in exI, auto)
   4.740 +done
   4.741 +
   4.742 +lemma zless_succ_zadd: "w $< w $+ $# succ(n)"
   4.743 +by (cut_tac intify_in_int [THEN zless_succ_zadd_lemma], auto)
   4.744 +
   4.745 +lemma zless_iff_succ_zadd:
   4.746 +     "w $< z <-> (EX n: nat. w $+ $#(succ(n)) = intify(z))"
   4.747 +apply (rule iffI)
   4.748 +apply (erule zless_imp_succ_zadd, auto)
   4.749 +apply (rename_tac "n")
   4.750 +apply (cut_tac w = w and n = n in zless_succ_zadd, auto)
   4.751 +done
   4.752 +
   4.753 +lemma zless_int_of [simp]: "[| m: nat; n: nat |] ==> ($#m $< $#n) <-> (m<n)"
   4.754 +apply (simp add: less_iff_succ_add zless_iff_succ_zadd int_of_add [symmetric])
   4.755 +apply (blast intro: sym)
   4.756 +done
   4.757 +
   4.758 +lemma zless_trans_lemma: 
   4.759 +    "[| x $< y; y $< z; x: int; y : int; z: int |] ==> x $< z"
   4.760 +apply (unfold zless_def znegative_def zdiff_def int_def)
   4.761 +apply (auto simp add: zadd zminus image_iff)
   4.762 +apply (rename_tac x1 x2 y1 y2)
   4.763 +apply (rule_tac x = "x1#+x2" in exI)
   4.764 +apply (rule_tac x = "y1#+y2" in exI)
   4.765 +apply (auto simp add: add_lt_mono)
   4.766 +apply (rule sym)
   4.767 +apply (erule add_left_cancel)+
   4.768 +apply auto
   4.769 +done
   4.770 +
   4.771 +lemma zless_trans: "[| x $< y; y $< z |] ==> x $< z"
   4.772 +apply (subgoal_tac "intify (x) $< intify (z) ")
   4.773 +apply (rule_tac [2] y = "intify (y) " in zless_trans_lemma)
   4.774 +apply auto
   4.775 +done
   4.776 +
   4.777 +lemma zless_not_sym: "z $< w ==> ~ (w $< z)"
   4.778 +by (blast dest: zless_trans)
   4.779 +
   4.780 +(* [| z $< w; ~ P ==> w $< z |] ==> P *)
   4.781 +lemmas zless_asym = zless_not_sym [THEN swap, standard]
   4.782 +
   4.783 +lemma zless_imp_zle: "z $< w ==> z $<= w"
   4.784 +apply (unfold zle_def)
   4.785 +apply (blast elim: zless_asym)
   4.786 +done
   4.787 +
   4.788 +lemma zle_linear: "z $<= w | w $<= z"
   4.789 +apply (simp add: zle_def)
   4.790 +apply (cut_tac zless_linear, blast)
   4.791 +done
   4.792 +
   4.793 +
   4.794 +subsection{*Less Than or Equals*}
   4.795 +
   4.796 +lemma zle_refl: "z $<= z"
   4.797 +by (unfold zle_def, auto)
   4.798 +
   4.799 +lemma zle_eq_refl: "x=y ==> x $<= y"
   4.800 +by (simp add: zle_refl)
   4.801 +
   4.802 +lemma zle_anti_sym_intify: "[| x $<= y; y $<= x |] ==> intify(x) = intify(y)"
   4.803 +apply (unfold zle_def, auto)
   4.804 +apply (blast dest: zless_trans)
   4.805 +done
   4.806 +
   4.807 +lemma zle_anti_sym: "[| x $<= y; y $<= x; x: int; y: int |] ==> x=y"
   4.808 +by (drule zle_anti_sym_intify, auto)
   4.809 +
   4.810 +lemma zle_trans_lemma:
   4.811 +     "[| x: int; y: int; z: int; x $<= y; y $<= z |] ==> x $<= z"
   4.812 +apply (unfold zle_def, auto)
   4.813 +apply (blast intro: zless_trans)
   4.814 +done
   4.815 +
   4.816 +lemma zle_trans: "[| x $<= y; y $<= z |] ==> x $<= z"
   4.817 +apply (subgoal_tac "intify (x) $<= intify (z) ")
   4.818 +apply (rule_tac [2] y = "intify (y) " in zle_trans_lemma)
   4.819 +apply auto
   4.820 +done
   4.821 +
   4.822 +lemma zle_zless_trans: "[| i $<= j; j $< k |] ==> i $< k"
   4.823 +apply (auto simp add: zle_def)
   4.824 +apply (blast intro: zless_trans)
   4.825 +apply (simp add: zless_def zdiff_def zadd_def)
   4.826 +done
   4.827 +
   4.828 +lemma zless_zle_trans: "[| i $< j; j $<= k |] ==> i $< k"
   4.829 +apply (auto simp add: zle_def)
   4.830 +apply (blast intro: zless_trans)
   4.831 +apply (simp add: zless_def zdiff_def zminus_def)
   4.832 +done
   4.833 +
   4.834 +lemma not_zless_iff_zle: "~ (z $< w) <-> (w $<= z)"
   4.835 +apply (cut_tac z = z and w = w in zless_linear)
   4.836 +apply (auto dest: zless_trans simp add: zle_def)
   4.837 +apply (auto dest!: zless_imp_intify_neq)
   4.838 +done
   4.839 +
   4.840 +lemma not_zle_iff_zless: "~ (z $<= w) <-> (w $< z)"
   4.841 +by (simp add: not_zless_iff_zle [THEN iff_sym])
   4.842 +
   4.843 +
   4.844 +subsection{*More subtraction laws (for @{text zcompare_rls})*}
   4.845 +
   4.846 +lemma zdiff_zdiff_eq: "(x $- y) $- z = x $- (y $+ z)"
   4.847 +by (simp add: zdiff_def zadd_ac)
   4.848 +
   4.849 +lemma zdiff_zdiff_eq2: "x $- (y $- z) = (x $+ z) $- y"
   4.850 +by (simp add: zdiff_def zadd_ac)
   4.851 +
   4.852 +lemma zdiff_zless_iff: "(x$-y $< z) <-> (x $< z $+ y)"
   4.853 +apply (unfold zless_def zdiff_def)
   4.854 +apply (simp add: zadd_ac)
   4.855 +done
   4.856 +
   4.857 +lemma zless_zdiff_iff: "(x $< z$-y) <-> (x $+ y $< z)"
   4.858 +apply (unfold zless_def zdiff_def)
   4.859 +apply (simp add: zadd_ac)
   4.860 +done
   4.861 +
   4.862 +lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)"
   4.863 +apply (unfold zdiff_def)
   4.864 +apply (auto simp add: zadd_assoc)
   4.865 +done
   4.866 +
   4.867 +lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)"
   4.868 +apply (unfold zdiff_def)
   4.869 +apply (auto simp add: zadd_assoc)
   4.870 +done
   4.871 +
   4.872 +lemma zdiff_zle_iff_lemma:
   4.873 +     "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)"
   4.874 +apply (unfold zle_def)
   4.875 +apply (auto simp add: zdiff_eq_iff zdiff_zless_iff)
   4.876 +done
   4.877 +
   4.878 +lemma zdiff_zle_iff: "(x$-y $<= z) <-> (x $<= z $+ y)"
   4.879 +by (cut_tac zdiff_zle_iff_lemma [OF intify_in_int intify_in_int], simp)
   4.880 +
   4.881 +lemma zle_zdiff_iff_lemma:
   4.882 +     "[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)"
   4.883 +apply (unfold zle_def)
   4.884 +apply (auto simp add: zdiff_eq_iff zless_zdiff_iff)
   4.885 +apply (auto simp add: zdiff_def zadd_assoc)
   4.886 +done
   4.887 +
   4.888 +lemma zle_zdiff_iff: "(x $<= z$-y) <-> (x $+ y $<= z)"
   4.889 +by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp)
   4.890 +
   4.891 +text{*This list of rewrites simplifies (in)equalities by bringing subtractions
   4.892 +  to the top and then moving negative terms to the other side.  
   4.893 +  Use with @{text zadd_ac}*}
   4.894 +lemmas zcompare_rls =
   4.895 +     zdiff_def [symmetric]
   4.896 +     zadd_zdiff_eq zdiff_zadd_eq zdiff_zdiff_eq zdiff_zdiff_eq2 
   4.897 +     zdiff_zless_iff zless_zdiff_iff zdiff_zle_iff zle_zdiff_iff 
   4.898 +     zdiff_eq_iff eq_zdiff_iff
   4.899 +
   4.900 +
   4.901 +subsection{*Monotonicity and Cancellation Results for Instantiation
   4.902 +     of the CancelNumerals Simprocs*}
   4.903 +
   4.904 +lemma zadd_left_cancel:
   4.905 +     "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)"
   4.906 +apply safe
   4.907 +apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
   4.908 +apply (simp add: zadd_ac)
   4.909 +done
   4.910 +
   4.911 +lemma zadd_left_cancel_intify [simp]:
   4.912 +     "(z $+ w' = z $+ w) <-> intify(w') = intify(w)"
   4.913 +apply (rule iff_trans)
   4.914 +apply (rule_tac [2] zadd_left_cancel, auto)
   4.915 +done
   4.916 +
   4.917 +lemma zadd_right_cancel:
   4.918 +     "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)"
   4.919 +apply safe
   4.920 +apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
   4.921 +apply (simp add: zadd_ac)
   4.922 +done
   4.923 +
   4.924 +lemma zadd_right_cancel_intify [simp]:
   4.925 +     "(w' $+ z = w $+ z) <-> intify(w') = intify(w)"
   4.926 +apply (rule iff_trans)
   4.927 +apply (rule_tac [2] zadd_right_cancel, auto)
   4.928 +done
   4.929 +
   4.930 +lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) <-> (w' $< w)"
   4.931 +apply (simp add: zdiff_zless_iff [THEN iff_sym])
   4.932 +apply (simp add: zdiff_def zadd_assoc)
   4.933 +done
   4.934 +
   4.935 +lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) <-> (w' $< w)"
   4.936 +by (simp add: zadd_commute [of z] zadd_right_cancel_zless)
   4.937 +
   4.938 +lemma zadd_right_cancel_zle [simp]: "(w' $+ z $<= w $+ z) <-> w' $<= w"
   4.939 +by (simp add: zle_def)
   4.940 +
   4.941 +lemma zadd_left_cancel_zle [simp]: "(z $+ w' $<= z $+ w) <->  w' $<= w"
   4.942 +by (simp add: zadd_commute [of z]  zadd_right_cancel_zle)
   4.943 +
   4.944 +
   4.945 +(*"v $<= w ==> v$+z $<= w$+z"*)
   4.946 +lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
   4.947 +
   4.948 +(*"v $<= w ==> z$+v $<= z$+w"*)
   4.949 +lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
   4.950 +
   4.951 +(*"v $<= w ==> v$+z $<= w$+z"*)
   4.952 +lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
   4.953 +
   4.954 +(*"v $<= w ==> z$+v $<= z$+w"*)
   4.955 +lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
   4.956 +
   4.957 +lemma zadd_zle_mono: "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z"
   4.958 +by (erule zadd_zle_mono1 [THEN zle_trans], simp)
   4.959 +
   4.960 +lemma zadd_zless_mono: "[| w' $< w; z' $<= z |] ==> w' $+ z' $< w $+ z"
   4.961 +by (erule zadd_zless_mono1 [THEN zless_zle_trans], simp)
   4.962 +
   4.963 +
   4.964 +subsection{*Comparison laws*}
   4.965 +
   4.966 +lemma zminus_zless_zminus [simp]: "($- x $< $- y) <-> (y $< x)"
   4.967 +by (simp add: zless_def zdiff_def zadd_ac)
   4.968 +
   4.969 +lemma zminus_zle_zminus [simp]: "($- x $<= $- y) <-> (y $<= x)"
   4.970 +by (simp add: not_zless_iff_zle [THEN iff_sym])
   4.971 +
   4.972 +subsubsection{*More inequality lemmas*}
   4.973 +
   4.974 +lemma equation_zminus: "[| x: int;  y: int |] ==> (x = $- y) <-> (y = $- x)"
   4.975 +by auto
   4.976 +
   4.977 +lemma zminus_equation: "[| x: int;  y: int |] ==> ($- x = y) <-> ($- y = x)"
   4.978 +by auto
   4.979 +
   4.980 +lemma equation_zminus_intify: "(intify(x) = $- y) <-> (intify(y) = $- x)"
   4.981 +apply (cut_tac x = "intify (x) " and y = "intify (y) " in equation_zminus)
   4.982 +apply auto
   4.983 +done
   4.984 +
   4.985 +lemma zminus_equation_intify: "($- x = intify(y)) <-> ($- y = intify(x))"
   4.986 +apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation)
   4.987 +apply auto
   4.988 +done
   4.989 +
   4.990 +
   4.991 +subsubsection{*The next several equations are permutative: watch out!*}
   4.992 +
   4.993 +lemma zless_zminus: "(x $< $- y) <-> (y $< $- x)"
   4.994 +by (simp add: zless_def zdiff_def zadd_ac)
   4.995 +
   4.996 +lemma zminus_zless: "($- x $< y) <-> ($- y $< x)"
   4.997 +by (simp add: zless_def zdiff_def zadd_ac)
   4.998 +
   4.999 +lemma zle_zminus: "(x $<= $- y) <-> (y $<= $- x)"
  4.1000 +by (simp add: not_zless_iff_zle [THEN iff_sym] zminus_zless)
  4.1001 +
  4.1002 +lemma zminus_zle: "($- x $<= y) <-> ($- y $<= x)"
  4.1003 +by (simp add: not_zless_iff_zle [THEN iff_sym] zless_zminus)
  4.1004 +
  4.1005 +ML
  4.1006 +{*
  4.1007 +val zdiff_def = thm "zdiff_def";
  4.1008 +val int_of_type = thm "int_of_type";
  4.1009 +val int_of_eq = thm "int_of_eq";
  4.1010 +val int_of_inject = thm "int_of_inject";
  4.1011 +val intify_in_int = thm "intify_in_int";
  4.1012 +val intify_ident = thm "intify_ident";
  4.1013 +val intify_idem = thm "intify_idem";
  4.1014 +val int_of_natify = thm "int_of_natify";
  4.1015 +val zminus_intify = thm "zminus_intify";
  4.1016 +val zadd_intify1 = thm "zadd_intify1";
  4.1017 +val zadd_intify2 = thm "zadd_intify2";
  4.1018 +val zdiff_intify1 = thm "zdiff_intify1";
  4.1019 +val zdiff_intify2 = thm "zdiff_intify2";
  4.1020 +val zmult_intify1 = thm "zmult_intify1";
  4.1021 +val zmult_intify2 = thm "zmult_intify2";
  4.1022 +val zless_intify1 = thm "zless_intify1";
  4.1023 +val zless_intify2 = thm "zless_intify2";
  4.1024 +val zle_intify1 = thm "zle_intify1";
  4.1025 +val zle_intify2 = thm "zle_intify2";
  4.1026 +val zminus_congruent = thm "zminus_congruent";
  4.1027 +val zminus_type = thm "zminus_type";
  4.1028 +val zminus_inject_intify = thm "zminus_inject_intify";
  4.1029 +val zminus_inject = thm "zminus_inject";
  4.1030 +val zminus = thm "zminus";
  4.1031 +val zminus_zminus_intify = thm "zminus_zminus_intify";
  4.1032 +val zminus_int0 = thm "zminus_int0";
  4.1033 +val zminus_zminus = thm "zminus_zminus";
  4.1034 +val not_znegative_int_of = thm "not_znegative_int_of";
  4.1035 +val znegative_zminus_int_of = thm "znegative_zminus_int_of";
  4.1036 +val not_znegative_imp_zero = thm "not_znegative_imp_zero";
  4.1037 +val nat_of_intify = thm "nat_of_intify";
  4.1038 +val nat_of_int_of = thm "nat_of_int_of";
  4.1039 +val nat_of_type = thm "nat_of_type";
  4.1040 +val zmagnitude_int_of = thm "zmagnitude_int_of";
  4.1041 +val natify_int_of_eq = thm "natify_int_of_eq";
  4.1042 +val zmagnitude_zminus_int_of = thm "zmagnitude_zminus_int_of";
  4.1043 +val zmagnitude_type = thm "zmagnitude_type";
  4.1044 +val not_zneg_int_of = thm "not_zneg_int_of";
  4.1045 +val not_zneg_mag = thm "not_zneg_mag";
  4.1046 +val zneg_int_of = thm "zneg_int_of";
  4.1047 +val zneg_mag = thm "zneg_mag";
  4.1048 +val int_cases = thm "int_cases";
  4.1049 +val not_zneg_nat_of_intify = thm "not_zneg_nat_of_intify";
  4.1050 +val not_zneg_nat_of = thm "not_zneg_nat_of";
  4.1051 +val zneg_nat_of = thm "zneg_nat_of";
  4.1052 +val zadd_congruent2 = thm "zadd_congruent2";
  4.1053 +val zadd_type = thm "zadd_type";
  4.1054 +val zadd = thm "zadd";
  4.1055 +val zadd_int0_intify = thm "zadd_int0_intify";
  4.1056 +val zadd_int0 = thm "zadd_int0";
  4.1057 +val zminus_zadd_distrib = thm "zminus_zadd_distrib";
  4.1058 +val zadd_commute = thm "zadd_commute";
  4.1059 +val zadd_assoc = thm "zadd_assoc";
  4.1060 +val zadd_left_commute = thm "zadd_left_commute";
  4.1061 +val zadd_ac = thms "zadd_ac";
  4.1062 +val int_of_add = thm "int_of_add";
  4.1063 +val int_succ_int_1 = thm "int_succ_int_1";
  4.1064 +val int_of_diff = thm "int_of_diff";
  4.1065 +val zadd_zminus_inverse = thm "zadd_zminus_inverse";
  4.1066 +val zadd_zminus_inverse2 = thm "zadd_zminus_inverse2";
  4.1067 +val zadd_int0_right_intify = thm "zadd_int0_right_intify";
  4.1068 +val zadd_int0_right = thm "zadd_int0_right";
  4.1069 +val zmult_congruent2 = thm "zmult_congruent2";
  4.1070 +val zmult_type = thm "zmult_type";
  4.1071 +val zmult = thm "zmult";
  4.1072 +val zmult_int0 = thm "zmult_int0";
  4.1073 +val zmult_int1_intify = thm "zmult_int1_intify";
  4.1074 +val zmult_int1 = thm "zmult_int1";
  4.1075 +val zmult_commute = thm "zmult_commute";
  4.1076 +val zmult_zminus = thm "zmult_zminus";
  4.1077 +val zmult_zminus_right = thm "zmult_zminus_right";
  4.1078 +val zmult_assoc = thm "zmult_assoc";
  4.1079 +val zmult_left_commute = thm "zmult_left_commute";
  4.1080 +val zmult_ac = thms "zmult_ac";
  4.1081 +val zadd_zmult_distrib = thm "zadd_zmult_distrib";
  4.1082 +val zadd_zmult_distrib2 = thm "zadd_zmult_distrib2";
  4.1083 +val int_typechecks = thms "int_typechecks";
  4.1084 +val zdiff_type = thm "zdiff_type";
  4.1085 +val zminus_zdiff_eq = thm "zminus_zdiff_eq";
  4.1086 +val zdiff_zmult_distrib = thm "zdiff_zmult_distrib";
  4.1087 +val zdiff_zmult_distrib2 = thm "zdiff_zmult_distrib2";
  4.1088 +val zadd_zdiff_eq = thm "zadd_zdiff_eq";
  4.1089 +val zdiff_zadd_eq = thm "zdiff_zadd_eq";
  4.1090 +val zless_linear = thm "zless_linear";
  4.1091 +val zless_not_refl = thm "zless_not_refl";
  4.1092 +val neq_iff_zless = thm "neq_iff_zless";
  4.1093 +val zless_imp_intify_neq = thm "zless_imp_intify_neq";
  4.1094 +val zless_imp_succ_zadd = thm "zless_imp_succ_zadd";
  4.1095 +val zless_succ_zadd = thm "zless_succ_zadd";
  4.1096 +val zless_iff_succ_zadd = thm "zless_iff_succ_zadd";
  4.1097 +val zless_int_of = thm "zless_int_of";
  4.1098 +val zless_trans = thm "zless_trans";
  4.1099 +val zless_not_sym = thm "zless_not_sym";
  4.1100 +val zless_asym = thm "zless_asym";
  4.1101 +val zless_imp_zle = thm "zless_imp_zle";
  4.1102 +val zle_linear = thm "zle_linear";
  4.1103 +val zle_refl = thm "zle_refl";
  4.1104 +val zle_eq_refl = thm "zle_eq_refl";
  4.1105 +val zle_anti_sym_intify = thm "zle_anti_sym_intify";
  4.1106 +val zle_anti_sym = thm "zle_anti_sym";
  4.1107 +val zle_trans = thm "zle_trans";
  4.1108 +val zle_zless_trans = thm "zle_zless_trans";
  4.1109 +val zless_zle_trans = thm "zless_zle_trans";
  4.1110 +val not_zless_iff_zle = thm "not_zless_iff_zle";
  4.1111 +val not_zle_iff_zless = thm "not_zle_iff_zless";
  4.1112 +val zdiff_zdiff_eq = thm "zdiff_zdiff_eq";
  4.1113 +val zdiff_zdiff_eq2 = thm "zdiff_zdiff_eq2";
  4.1114 +val zdiff_zless_iff = thm "zdiff_zless_iff";
  4.1115 +val zless_zdiff_iff = thm "zless_zdiff_iff";
  4.1116 +val zdiff_eq_iff = thm "zdiff_eq_iff";
  4.1117 +val eq_zdiff_iff = thm "eq_zdiff_iff";
  4.1118 +val zdiff_zle_iff = thm "zdiff_zle_iff";
  4.1119 +val zle_zdiff_iff = thm "zle_zdiff_iff";
  4.1120 +val zcompare_rls = thms "zcompare_rls";
  4.1121 +val zadd_left_cancel = thm "zadd_left_cancel";
  4.1122 +val zadd_left_cancel_intify = thm "zadd_left_cancel_intify";
  4.1123 +val zadd_right_cancel = thm "zadd_right_cancel";
  4.1124 +val zadd_right_cancel_intify = thm "zadd_right_cancel_intify";
  4.1125 +val zadd_right_cancel_zless = thm "zadd_right_cancel_zless";
  4.1126 +val zadd_left_cancel_zless = thm "zadd_left_cancel_zless";
  4.1127 +val zadd_right_cancel_zle = thm "zadd_right_cancel_zle";
  4.1128 +val zadd_left_cancel_zle = thm "zadd_left_cancel_zle";
  4.1129 +val zadd_zless_mono1 = thm "zadd_zless_mono1";
  4.1130 +val zadd_zless_mono2 = thm "zadd_zless_mono2";
  4.1131 +val zadd_zle_mono1 = thm "zadd_zle_mono1";
  4.1132 +val zadd_zle_mono2 = thm "zadd_zle_mono2";
  4.1133 +val zadd_zle_mono = thm "zadd_zle_mono";
  4.1134 +val zadd_zless_mono = thm "zadd_zless_mono";
  4.1135 +val zminus_zless_zminus = thm "zminus_zless_zminus";
  4.1136 +val zminus_zle_zminus = thm "zminus_zle_zminus";
  4.1137 +val equation_zminus = thm "equation_zminus";
  4.1138 +val zminus_equation = thm "zminus_equation";
  4.1139 +val equation_zminus_intify = thm "equation_zminus_intify";
  4.1140 +val zminus_equation_intify = thm "zminus_equation_intify";
  4.1141 +val zless_zminus = thm "zless_zminus";
  4.1142 +val zminus_zless = thm "zminus_zless";
  4.1143 +val zle_zminus = thm "zle_zminus";
  4.1144 +val zminus_zle = thm "zminus_zle";
  4.1145 +*}
  4.1146 +
  4.1147 +
  4.1148  end
     5.1 --- a/src/ZF/Integ/IntDiv.thy	Thu Sep 05 14:03:03 2002 +0200
     5.2 +++ b/src/ZF/Integ/IntDiv.thy	Sat Sep 07 22:04:28 2002 +0200
     5.3 @@ -3,8 +3,6 @@
     5.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.5      Copyright   1999  University of Cambridge
     5.6  
     5.7 -The division operators div and mod (borrowed from the HOL equivalent)
     5.8 -
     5.9  Here is the division algorithm in ML:
    5.10  
    5.11      fun posDivAlg (a,b) =
    5.12 @@ -31,6 +29,8 @@
    5.13  
    5.14  *)
    5.15  
    5.16 +header{*The Division Operators Div and Mod*}
    5.17 +
    5.18  theory IntDiv = IntArith + OrderArith:
    5.19  
    5.20  constdefs
     6.1 --- a/src/ZF/Integ/int_arith.ML	Thu Sep 05 14:03:03 2002 +0200
     6.2 +++ b/src/ZF/Integ/int_arith.ML	Sat Sep 07 22:04:28 2002 +0200
     6.3 @@ -184,7 +184,8 @@
     6.4                 zmult_minus1, zmult_minus1_right];
     6.5  
     6.6  val tc_rules = [integ_of_type, intify_in_int,
     6.7 -                int_of_type, zadd_type, zdiff_type, zmult_type] @ bin.intrs;
     6.8 +                int_of_type, zadd_type, zdiff_type, zmult_type] @ 
     6.9 +               thms "bin.intros";
    6.10  val intifys = [intify_ident, zadd_intify1, zadd_intify2,
    6.11                 zdiff_intify1, zdiff_intify2, zmult_intify1, zmult_intify2,
    6.12                 zless_intify1, zless_intify2, zle_intify1, zle_intify2];
     7.1 --- a/src/ZF/IsaMakefile	Thu Sep 05 14:03:03 2002 +0200
     7.2 +++ b/src/ZF/IsaMakefile	Sat Sep 07 22:04:28 2002 +0200
     7.3 @@ -33,8 +33,8 @@
     7.4    CardinalArith.thy Cardinal_AC.thy \
     7.5    Datatype.ML Datatype.thy Epsilon.thy Finite.thy	\
     7.6    Fixedpt.thy Inductive.ML Inductive.thy 	\
     7.7 -  InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML	\
     7.8 -  Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy	\
     7.9 +  InfDatatype.thy Integ/Bin.thy Integ/EquivClass.ML	\
    7.10 +  Integ/EquivClass.thy Integ/Int.thy Integ/IntArith.thy	\
    7.11    Integ/IntDiv.thy Integ/int_arith.ML			\
    7.12    Let.ML Let.thy List.thy Main.ML Main.thy	\
    7.13    Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy	\