src/ZF/Integ/Int.ML
changeset 5561 426c1e330903
child 5758 27a2b36efd95
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Integ/Int.ML	Fri Sep 25 13:18:07 1998 +0200
     1.3 @@ -0,0 +1,412 @@
     1.4 +(*  Title:      ZF/Integ/Int.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +The integers as equivalence classes over nat*nat.
    1.10 +
    1.11 +Could also prove...
    1.12 +"znegative(z) ==> $# zmagnitude(z) = $~ z"
    1.13 +"~ znegative(z) ==> $# zmagnitude(z) = z"
    1.14 +$< is a linear ordering
    1.15 +$+ and $* are monotonic wrt $<
    1.16 +*)
    1.17 +
    1.18 +AddSEs [quotientE];
    1.19 +
    1.20 +(*** Proving that intrel is an equivalence relation ***)
    1.21 +
    1.22 +(*By luck, requires no typing premises for y1, y2,y3*)
    1.23 +val eqa::eqb::prems = goal Arith.thy 
    1.24 +    "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
    1.25 +\       x1: nat; x2: nat; x3: nat |]    ==>    x1 #+ y3 = x3 #+ y1";
    1.26 +by (res_inst_tac [("k","x2")] add_left_cancel 1);
    1.27 +by (resolve_tac prems 2);
    1.28 +by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
    1.29 +by (stac eqb 1);
    1.30 +by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
    1.31 +by (stac eqa 1);
    1.32 +by (rtac (add_left_commute) 1 THEN typechk_tac prems);
    1.33 +qed "int_trans_lemma";
    1.34 +
    1.35 +(** Natural deduction for intrel **)
    1.36 +
    1.37 +Goalw [intrel_def]
    1.38 +    "<<x1,y1>,<x2,y2>>: intrel <-> \
    1.39 +\    x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1";
    1.40 +by (Fast_tac 1);
    1.41 +qed "intrel_iff";
    1.42 +
    1.43 +Goalw [intrel_def]
    1.44 +    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
    1.45 +\             <<x1,y1>,<x2,y2>>: intrel";
    1.46 +by (fast_tac (claset() addIs prems) 1);
    1.47 +qed "intrelI";
    1.48 +
    1.49 +(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
    1.50 +Goalw [intrel_def]
    1.51 +  "p: intrel --> (EX x1 y1 x2 y2. \
    1.52 +\                  p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
    1.53 +\                  x1: nat & y1: nat & x2: nat & y2: nat)";
    1.54 +by (Fast_tac 1);
    1.55 +qed "intrelE_lemma";
    1.56 +
    1.57 +val [major,minor] = goal thy
    1.58 +  "[| p: intrel;  \
    1.59 +\     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
    1.60 +\                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
    1.61 +\  ==> Q";
    1.62 +by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
    1.63 +by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
    1.64 +qed "intrelE";
    1.65 +
    1.66 +AddSIs [intrelI];
    1.67 +AddSEs [intrelE];
    1.68 +
    1.69 +Goalw [equiv_def, refl_def, sym_def, trans_def]
    1.70 +    "equiv(nat*nat, intrel)";
    1.71 +by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
    1.72 +qed "equiv_intrel";
    1.73 +
    1.74 +
    1.75 +Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
    1.76 +	  add_0_right, add_succ_right];
    1.77 +Addcongs [conj_cong];
    1.78 +
    1.79 +val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
    1.80 +
    1.81 +(** int_of: the injection from nat to int **)
    1.82 +
    1.83 +Goalw [int_def,quotient_def,int_of_def]
    1.84 +    "m : nat ==> $#m : int";
    1.85 +by (fast_tac (claset() addSIs [nat_0I]) 1);
    1.86 +qed "int_of_type";
    1.87 +
    1.88 +Addsimps [int_of_type];
    1.89 +
    1.90 +Goalw [int_of_def] "[| $#m = $#n;  m: nat |] ==> m=n";
    1.91 +by (dtac (sym RS eq_intrelD) 1);
    1.92 +by (typechk_tac [nat_0I, SigmaI]);
    1.93 +by (Asm_full_simp_tac 1);
    1.94 +qed "int_of_inject";
    1.95 +
    1.96 +AddSDs [int_of_inject];
    1.97 +
    1.98 +Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; 
    1.99 +by (Blast_tac 1); 
   1.100 +qed "int_of_eq"; 
   1.101 +Addsimps [int_of_eq]; 
   1.102 +
   1.103 +(**** zminus: unary negation on int ****)
   1.104 +
   1.105 +Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
   1.106 +by Safe_tac;
   1.107 +by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
   1.108 +qed "zminus_congruent";
   1.109 +
   1.110 +(*Resolve th against the corresponding facts for zminus*)
   1.111 +val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
   1.112 +
   1.113 +Goalw [int_def,zminus_def] "z : int ==> $~z : int";
   1.114 +by (typechk_tac [split_type, SigmaI, zminus_ize UN_equiv_class_type,
   1.115 +                 quotientI]);
   1.116 +qed "zminus_type";
   1.117 +
   1.118 +Goalw [int_def,zminus_def] "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
   1.119 +by (etac (zminus_ize UN_equiv_class_inject) 1);
   1.120 +by Safe_tac;
   1.121 +(*The setloop is only needed because assumptions are in the wrong order!*)
   1.122 +by (asm_full_simp_tac (simpset() addsimps add_ac
   1.123 +                       setloop dtac eq_intrelD) 1);
   1.124 +qed "zminus_inject";
   1.125 +
   1.126 +Goalw [zminus_def]
   1.127 +    "[| x: nat;  y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
   1.128 +by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
   1.129 +qed "zminus";
   1.130 +
   1.131 +Goalw [int_def] "z : int ==> $~ ($~ z) = z";
   1.132 +by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   1.133 +by (asm_simp_tac (simpset() addsimps [zminus]) 1);
   1.134 +qed "zminus_zminus";
   1.135 +
   1.136 +Goalw [int_def, int_of_def] "$~ ($#0) = $#0";
   1.137 +by (simp_tac (simpset() addsimps [zminus]) 1);
   1.138 +qed "zminus_0";
   1.139 +
   1.140 +Addsimps [zminus_zminus, zminus_0];
   1.141 +
   1.142 +
   1.143 +(**** znegative: the test for negative integers ****)
   1.144 +
   1.145 +(*No natural number is negative!*)
   1.146 +Goalw [znegative_def, int_of_def]  "~ znegative($# n)";
   1.147 +by Safe_tac;
   1.148 +by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
   1.149 +by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
   1.150 +by (force_tac (claset(),
   1.151 +	       simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
   1.152 +qed "not_znegative_int_of";
   1.153 +
   1.154 +Addsimps [not_znegative_int_of];
   1.155 +AddSEs   [not_znegative_int_of RS notE];
   1.156 +
   1.157 +Goalw [znegative_def, int_of_def] "n: nat ==> znegative($~ $# succ(n))";
   1.158 +by (asm_simp_tac (simpset() addsimps [zminus]) 1);
   1.159 +by (blast_tac (claset() addIs [nat_0_le]) 1);
   1.160 +qed "znegative_zminus_int_of";
   1.161 +
   1.162 +Addsimps [znegative_zminus_int_of];
   1.163 +
   1.164 +Goalw [znegative_def, int_of_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
   1.165 +by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
   1.166 +be natE 1;
   1.167 +by (dres_inst_tac [("x","0")] spec 2);
   1.168 +by Auto_tac;
   1.169 +qed "not_znegative_imp_zero";
   1.170 +
   1.171 +(**** zmagnitude: magnitide of an integer, as a natural number ****)
   1.172 +
   1.173 +Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n";
   1.174 +by Auto_tac;
   1.175 +qed "zmagnitude_int_of";
   1.176 +
   1.177 +Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
   1.178 +by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset()));
   1.179 +qed "zmagnitude_zminus_int_of";
   1.180 +
   1.181 +Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
   1.182 +
   1.183 +Goalw [zmagnitude_def] "zmagnitude(z) : nat";
   1.184 +br theI2 1;
   1.185 +by Auto_tac;
   1.186 +qed "zmagnitude_type";
   1.187 +
   1.188 +Goalw [int_def, znegative_def, int_of_def]
   1.189 +     "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
   1.190 +by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
   1.191 +by (rename_tac "i j" 1);
   1.192 +by (dres_inst_tac [("x", "i")] spec 1);
   1.193 +by (dres_inst_tac [("x", "j")] spec 1);
   1.194 +br bexI 1;
   1.195 +br (add_diff_inverse2 RS sym) 1;
   1.196 +by Auto_tac;
   1.197 +by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1);
   1.198 +qed "not_zneg_int_of";
   1.199 +
   1.200 +Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
   1.201 +bd not_zneg_int_of 1;
   1.202 +by Auto_tac;
   1.203 +qed "not_zneg_mag"; 
   1.204 +
   1.205 +Addsimps [not_zneg_mag];
   1.206 +
   1.207 +
   1.208 +Goalw [int_def, znegative_def, int_of_def]
   1.209 +     "[| z: int; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; 
   1.210 +by (auto_tac(claset() addSDs [less_imp_Suc_add], 
   1.211 +	     simpset() addsimps [zminus, image_singleton_iff]));
   1.212 +by (rename_tac "m n j k" 1);
   1.213 +by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
   1.214 +by (rotate_tac ~2 2);
   1.215 +by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
   1.216 +by (blast_tac (claset() addSDs [add_left_cancel]) 1);
   1.217 +qed "zneg_int_of";
   1.218 +
   1.219 +Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
   1.220 +bd zneg_int_of 1;
   1.221 +by Auto_tac;
   1.222 +qed "zneg_mag"; 
   1.223 +
   1.224 +Addsimps [zneg_mag];
   1.225 +
   1.226 +
   1.227 +(**** zadd: addition on int ****)
   1.228 +
   1.229 +(** Congruence property for addition **)
   1.230 +
   1.231 +Goalw [congruent2_def]
   1.232 +    "congruent2(intrel, %z1 z2.                      \
   1.233 +\         let <x1,y1>=z1; <x2,y2>=z2                 \
   1.234 +\                           in intrel``{<x1#+x2, y1#+y2>})";
   1.235 +(*Proof via congruent2_commuteI seems longer*)
   1.236 +by Safe_tac;
   1.237 +by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
   1.238 +(*The rest should be trivial, but rearranging terms is hard;
   1.239 +  add_ac does not help rewriting with the assumptions.*)
   1.240 +by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
   1.241 +by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
   1.242 +by (typechk_tac [add_type]);
   1.243 +by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
   1.244 +qed "zadd_congruent2";
   1.245 +
   1.246 +(*Resolve th against the corresponding facts for zadd*)
   1.247 +val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
   1.248 +
   1.249 +Goalw [int_def,zadd_def] "[| z: int;  w: int |] ==> z $+ w : int";
   1.250 +by (rtac (zadd_ize UN_equiv_class_type2) 1);
   1.251 +by (simp_tac (simpset() addsimps [Let_def]) 3);
   1.252 +by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
   1.253 +qed "zadd_type";
   1.254 +
   1.255 +Goalw [zadd_def]
   1.256 +  "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>       \
   1.257 +\           (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =        \
   1.258 +\           intrel `` {<x1#+x2, y1#+y2>}";
   1.259 +by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
   1.260 +by (simp_tac (simpset() addsimps [Let_def]) 1);
   1.261 +qed "zadd";
   1.262 +
   1.263 +Goalw [int_def,int_of_def] "z : int ==> $#0 $+ z = z";
   1.264 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.265 +by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   1.266 +qed "zadd_0";
   1.267 +
   1.268 +Goalw [int_def] "[| z: int;  w: int |] ==> $~ (z $+ w) = $~ z $+ $~ w";
   1.269 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.270 +by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
   1.271 +qed "zminus_zadd_distrib";
   1.272 +
   1.273 +Goalw [int_def] "[| z: int;  w: int |] ==> z $+ w = w $+ z";
   1.274 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.275 +by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
   1.276 +qed "zadd_commute";
   1.277 +
   1.278 +Goalw [int_def]
   1.279 +    "[| z1: int;  z2: int;  z3: int |]   \
   1.280 +\    ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
   1.281 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.282 +(*rewriting is much faster without intrel_iff, etc.*)
   1.283 +by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
   1.284 +qed "zadd_assoc";
   1.285 +
   1.286 +(*For AC rewriting*)
   1.287 +Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
   1.288 +by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_commute]) 1);
   1.289 +qed "zadd_left_commute";
   1.290 +
   1.291 +(*Integer addition is an AC operator*)
   1.292 +val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
   1.293 +
   1.294 +Goalw [int_of_def]
   1.295 +    "[| m: nat;  n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
   1.296 +by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   1.297 +qed "int_of_add";
   1.298 +
   1.299 +Goalw [int_def,int_of_def] "z : int ==> z $+ ($~ z) = $#0";
   1.300 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.301 +by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
   1.302 +qed "zadd_zminus_inverse";
   1.303 +
   1.304 +Goal "z : int ==> ($~ z) $+ z = $#0";
   1.305 +by (asm_simp_tac
   1.306 +    (simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1);
   1.307 +qed "zadd_zminus_inverse2";
   1.308 +
   1.309 +Goal "z:int ==> z $+ $#0 = z";
   1.310 +by (rtac (zadd_commute RS trans) 1);
   1.311 +by (REPEAT (ares_tac [int_of_type, nat_0I, zadd_0] 1));
   1.312 +qed "zadd_0_right";
   1.313 +
   1.314 +Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
   1.315 +
   1.316 +
   1.317 +(*Need properties of $- ???  Or use $- just as an abbreviation?
   1.318 +     [| m: nat;  n: nat;  m>=n |] ==> $# (m #- n) = ($#m) $- ($#n)
   1.319 +*)
   1.320 +
   1.321 +(**** zmult: multiplication on int ****)
   1.322 +
   1.323 +(** Congruence property for multiplication **)
   1.324 +
   1.325 +Goal "congruent2(intrel, %p1 p2.                 \
   1.326 +\               split(%x1 y1. split(%x2 y2.     \
   1.327 +\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
   1.328 +by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   1.329 +by Safe_tac;
   1.330 +by (ALLGOALS Asm_simp_tac);
   1.331 +(*Proof that zmult is congruent in one argument*)
   1.332 +by (asm_simp_tac 
   1.333 +    (simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2);
   1.334 +by (asm_simp_tac
   1.335 +    (simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2);
   1.336 +(*Proof that zmult is commutative on representatives*)
   1.337 +by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1);
   1.338 +qed "zmult_congruent2";
   1.339 +
   1.340 +
   1.341 +(*Resolve th against the corresponding facts for zmult*)
   1.342 +val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
   1.343 +
   1.344 +Goalw [int_def,zmult_def] "[| z: int;  w: int |] ==> z $* w : int";
   1.345 +by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
   1.346 +                      split_type, add_type, mult_type, 
   1.347 +                      quotientI, SigmaI] 1));
   1.348 +qed "zmult_type";
   1.349 +
   1.350 +Goalw [zmult_def]
   1.351 +     "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>    \
   1.352 +\              (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
   1.353 +\              intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   1.354 +by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
   1.355 +qed "zmult";
   1.356 +
   1.357 +Goalw [int_def,int_of_def] "z : int ==> $#0 $* z = $#0";
   1.358 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.359 +by (asm_simp_tac (simpset() addsimps [zmult]) 1);
   1.360 +qed "zmult_0";
   1.361 +
   1.362 +Goalw [int_def,int_of_def] "z : int ==> $#1 $* z = z";
   1.363 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.364 +by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1);
   1.365 +qed "zmult_1";
   1.366 +
   1.367 +Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* w = $~ (z $* w)";
   1.368 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.369 +by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
   1.370 +qed "zmult_zminus";
   1.371 +
   1.372 +Addsimps [zmult_0, zmult_1, zmult_zminus];
   1.373 +
   1.374 +Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* ($~ w) = (z $* w)";
   1.375 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.376 +by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
   1.377 +qed "zmult_zminus_zminus";
   1.378 +
   1.379 +Goalw [int_def] "[| z: int;  w: int |] ==> z $* w = w $* z";
   1.380 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.381 +by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
   1.382 +qed "zmult_commute";
   1.383 +
   1.384 +Goalw [int_def]
   1.385 +    "[| z1: int;  z2: int;  z3: int |]     \
   1.386 +\    ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
   1.387 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.388 +by (asm_simp_tac 
   1.389 +    (simpset() addsimps [zmult, add_mult_distrib_left, 
   1.390 +                         add_mult_distrib] @ add_ac @ mult_ac) 1);
   1.391 +qed "zmult_assoc";
   1.392 +
   1.393 +(*For AC rewriting*)
   1.394 +Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
   1.395 +by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym, zmult_commute]) 1);
   1.396 +qed "zmult_left_commute";
   1.397 +
   1.398 +(*Integer multiplication is an AC operator*)
   1.399 +val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
   1.400 +
   1.401 +Goalw [int_def]
   1.402 +    "[| z1: int;  z2: int;  w: int |] ==> \
   1.403 +\                (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
   1.404 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.405 +by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1);
   1.406 +by (asm_simp_tac (simpset() addsimps add_ac @ mult_ac) 1);
   1.407 +qed "zadd_zmult_distrib";
   1.408 +
   1.409 +val int_typechecks =
   1.410 +    [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
   1.411 +
   1.412 +Addsimps int_typechecks;
   1.413 +
   1.414 +
   1.415 +