new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
authorpaulson
Fri Aug 11 13:27:17 2000 +0200 (2000-08-11)
changeset 9578ab26d6c8ebfe
parent 9577 9e66e8ed8237
child 9579 28e26f468f08
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
src/ZF/Integ/Bin.ML
src/ZF/Integ/Int.ML
src/ZF/Integ/Int.thy
src/ZF/Integ/IntDiv.ML
src/ZF/Integ/IntDiv.thy
src/ZF/IsaMakefile
src/ZF/Main.thy
     1.1 --- a/src/ZF/Integ/Bin.ML	Fri Aug 11 13:26:40 2000 +0200
     1.2 +++ b/src/ZF/Integ/Bin.ML	Fri Aug 11 13:27:17 2000 +0200
     1.3 @@ -313,11 +313,6 @@
     1.4  
     1.5  Addsimps [zmult_minus1, zmult_minus1_right];
     1.6  
     1.7 -(*beware!  LOOPS with int_combine_numerals simproc*)
     1.8 -Goal "#2 $* z = z $+ z";
     1.9 -by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
    1.10 -qed "zmult_2";
    1.11 -
    1.12  
    1.13  (*** Simplification rules for comparison of binary numbers (N Voelker) ***)
    1.14  
     2.1 --- a/src/ZF/Integ/Int.ML	Fri Aug 11 13:26:40 2000 +0200
     2.2 +++ b/src/ZF/Integ/Int.ML	Fri Aug 11 13:27:17 2000 +0200
     2.3 @@ -702,15 +702,15 @@
     2.4  
     2.5  (*This lemma allows direct proofs of other <-properties*)
     2.6  Goalw [zless_def, znegative_def, zdiff_def, int_def] 
     2.7 -    "[| w $< z; w: int; z: int |] ==> (EX n. z = w $+ $#(succ(n)))";
     2.8 +    "[| w $< z; w: int; z: int |] ==> (EX n: nat. z = w $+ $#(succ(n)))";
     2.9  by (auto_tac (claset() addSDs [less_imp_succ_add], 
    2.10                simpset() addsimps [zadd, zminus, int_of_def]));  
    2.11 -by (res_inst_tac [("x","k")] exI 1);
    2.12 +by (res_inst_tac [("x","k")] bexI 1);
    2.13  by (etac add_left_cancel 1);
    2.14  by Auto_tac;  
    2.15  val lemma = result();
    2.16  
    2.17 -Goal "w $< z ==> (EX n. w $+ $#(succ(n)) = intify(z))";
    2.18 +Goal "w $< z ==> (EX n: nat. w $+ $#(succ(n)) = intify(z))";
    2.19  by (subgoal_tac "intify(w) $< intify(z)" 1);
    2.20  by (dres_inst_tac [("w","intify(w)")] lemma 1);
    2.21  by Auto_tac;  
    2.22 @@ -729,10 +729,11 @@
    2.23  by Auto_tac;  
    2.24  qed "zless_succ_zadd";
    2.25  
    2.26 -Goal "w $< z <-> (EX n. w $+ $#(succ(n)) = intify(z))";
    2.27 +Goal "w $< z <-> (EX n: nat. w $+ $#(succ(n)) = intify(z))";
    2.28  by (rtac iffI 1);
    2.29  by (etac zless_imp_succ_zadd 1);
    2.30  by Auto_tac;  
    2.31 +by (rename_tac "n" 1);
    2.32  by (cut_inst_tac [("w","w"),("n","n")] zless_succ_zadd 1);
    2.33  by Auto_tac;  
    2.34  qed "zless_iff_succ_zadd";
    2.35 @@ -763,6 +764,16 @@
    2.36  (* [| z $< w; ~ P ==> w $< z |] ==> P *)
    2.37  bind_thm ("zless_asym", zless_not_sym RS swap);
    2.38  
    2.39 +Goalw [zle_def] "z $< w ==> z $<= w";
    2.40 +by (blast_tac (claset() addEs [zless_asym]) 1);
    2.41 +qed "zless_imp_zle";
    2.42 +
    2.43 +Goal "z $<= w | w $<= z";
    2.44 +by (simp_tac (simpset() addsimps [zle_def]) 1);
    2.45 +by (cut_facts_tac [zless_linear] 1);
    2.46 +by (Blast_tac 1);
    2.47 +qed "zle_linear";
    2.48 +
    2.49  
    2.50  (*** "Less Than or Equals", $<= ***)
    2.51  
    2.52 @@ -770,9 +781,18 @@
    2.53  by Auto_tac;  
    2.54  qed "zle_refl";
    2.55  
    2.56 +Goal "x=y ==> x $<= y";
    2.57 +by (asm_simp_tac (simpset() addsimps [zle_refl]) 1);
    2.58 +qed "zle_eq_refl";
    2.59 +
    2.60  Goalw [zle_def] "[| x $<= y; y $<= x |] ==> intify(x) = intify(y)";
    2.61  by Auto_tac;  
    2.62  by (blast_tac (claset() addDs [zless_trans]) 1);
    2.63 +qed "zle_anti_sym_intify";
    2.64 +
    2.65 +Goal "[| x $<= y; y $<= x; x: int; y: int |] ==> x=y"; 
    2.66 +by (dtac zle_anti_sym_intify 1);
    2.67 +by Auto_tac;  
    2.68  qed "zle_anti_sym";
    2.69  
    2.70  Goalw [zle_def] "[| x: int; y: int; z: int; x $<= y; y $<= z |] ==> x $<= z";
     3.1 --- a/src/ZF/Integ/Int.thy	Fri Aug 11 13:26:40 2000 +0200
     3.2 +++ b/src/ZF/Integ/Int.thy	Fri Aug 11 13:27:17 2000 +0200
     3.3 @@ -67,10 +67,4 @@
     3.4    zle          ::      [i,i]=>o      (infixl "$<=" 50)
     3.5       "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
     3.6    
     3.7 -(*div and mod await definitions!*)
     3.8 -consts
     3.9 -  "$'/"       ::      [i,i]=>i      (infixl 70) 
    3.10 -
    3.11 -  "$'/'/"     ::      [i,i]=>i      (infixl 70)
    3.12 -    
    3.13  end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/ZF/Integ/IntDiv.ML	Fri Aug 11 13:27:17 2000 +0200
     4.3 @@ -0,0 +1,1298 @@
     4.4 +(*  Title:      HOL/IntDiv.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1999  University of Cambridge
     4.8 +
     4.9 +The division operators div, mod and the divides relation "dvd"
    4.10 +
    4.11 +Here is the division algorithm in ML:
    4.12 +
    4.13 +    fun posDivAlg (a,b) =
    4.14 +      if a<b then (0,a)
    4.15 +      else let val (q,r) = posDivAlg(a, 2*b)
    4.16 +	       in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
    4.17 +	   end;
    4.18 +
    4.19 +    fun negDivAlg (a,b) =
    4.20 +      if 0<=a+b then (~1,a+b)
    4.21 +      else let val (q,r) = negDivAlg(a, 2*b)
    4.22 +	       in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
    4.23 +	   end;
    4.24 +
    4.25 +    fun negateSnd (q,r:int) = (q,~r);
    4.26 +
    4.27 +    fun divAlg (a,b) = if 0<=a then 
    4.28 +			  if b>0 then posDivAlg (a,b) 
    4.29 +			   else if a=0 then (0,0)
    4.30 +				else negateSnd (negDivAlg (~a,~b))
    4.31 +		       else 
    4.32 +			  if 0<b then negDivAlg (a,b)
    4.33 +			  else        negateSnd (posDivAlg (~a,~b));
    4.34 +*)
    4.35 +
    4.36 +Goal "[| #0 $< k; k: int |] ==> 0 < zmagnitude(k)";
    4.37 +by (dtac zero_zless_imp_znegative_zminus 1);
    4.38 +by (dtac zneg_int_of 2);
    4.39 +by (auto_tac (claset(), simpset() addsimps [inst "x" "k" zminus_equation]));  
    4.40 +by (subgoal_tac "0 < zmagnitude($# succ(x))" 1);
    4.41 +by (Asm_full_simp_tac 1);
    4.42 +by (asm_full_simp_tac (simpset_of Arith.thy addsimps [zmagnitude_int_of]) 1);
    4.43 +qed "zero_lt_zmagnitude";
    4.44 +
    4.45 +
    4.46 +(*** Inequality lemmas involving $#succ(m) ***)
    4.47 +
    4.48 +Goal "(w $< z $+ $# succ(m)) <-> (w $< z $+ $#m | intify(w) = z $+ $#m)"; 
    4.49 +by (auto_tac (claset(),
    4.50 +	      simpset() addsimps [zless_iff_succ_zadd, zadd_assoc, 
    4.51 +                                  int_of_add RS sym]));
    4.52 +by (res_inst_tac [("x","0")] bexI 3);
    4.53 +by (TRYALL (dtac sym));
    4.54 +by (cut_inst_tac [("m","m")] int_succ_int_1 1);
    4.55 +by (cut_inst_tac [("m","n")] int_succ_int_1 1);
    4.56 +by (Asm_full_simp_tac 1);
    4.57 +by (eres_inst_tac [("n","x")] natE 1);
    4.58 +by Auto_tac;
    4.59 +by (res_inst_tac [("x","succ(x)")] bexI 1);
    4.60 +by Auto_tac;  
    4.61 +qed "zless_add_succ_iff";
    4.62 +
    4.63 +Goal "z : int ==> (w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)";
    4.64 +by (asm_simp_tac (simpset_of Int.thy addsimps
    4.65 +                  [not_zless_iff_zle RS iff_sym, zless_add_succ_iff]) 1);
    4.66 +by (auto_tac (claset() addIs [zle_anti_sym] addEs [zless_asym],
    4.67 +	      simpset() addsimps [zless_imp_zle, not_zless_iff_zle]));
    4.68 +qed "lemma";
    4.69 +
    4.70 +Goal "(w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)";
    4.71 +by (cut_inst_tac [("z","intify(z)")] lemma 1);
    4.72 +by Auto_tac;  
    4.73 +qed "zadd_succ_zle_iff";
    4.74 +
    4.75 +(** USED??
    4.76 +Goal "w $< $# succ(m) <-> w $< $# m | intify(w) = $# m";
    4.77 +by (cut_inst_tac [("z","#0")] zless_add_succ_iff 1);
    4.78 +by Auto_tac;  
    4.79 +qed "zless_succ_iff";
    4.80 +
    4.81 +Goal "(w $<= $# succ(m)) <-> (w $<= $#m | intify(w) = $# succ(m))";
    4.82 +by (simp_tac (simpset_of Int.thy addsimps [zless_succ_iff, zle_def]) 1);
    4.83 +qed "zle_succ_iff";
    4.84 +**)
    4.85 +
    4.86 +(** Inequality reasoning **)
    4.87 +
    4.88 +Goal "(w $< z $+ #1) <-> (w$<=z)";
    4.89 +by (subgoal_tac "#1 = $# 1" 1);
    4.90 +by (asm_simp_tac (simpset_of Int.thy addsimps [zless_add_succ_iff, zle_def]) 1);
    4.91 +by Auto_tac;  
    4.92 +qed "zless_add1_iff_zle";
    4.93 +
    4.94 +Goal "(w $+ #1 $<= z) <-> (w $< z)";
    4.95 +by (subgoal_tac "#1 = $# 1" 1);
    4.96 +by (asm_simp_tac (simpset_of Int.thy addsimps [zadd_succ_zle_iff]) 1);
    4.97 +by Auto_tac;  
    4.98 +qed "add1_zle_iff";
    4.99 +
   4.100 +Goal "(#1 $+ w $<= z) <-> (w $< z)";
   4.101 +by (stac zadd_commute 1);
   4.102 +by (rtac add1_zle_iff 1);
   4.103 +qed "add1_left_zle_iff";
   4.104 +
   4.105 +
   4.106 +(*** Monotonicity results ***)
   4.107 +
   4.108 +Goal "(v$+z $< w$+z) <-> (v $< w)";
   4.109 +by (Simp_tac 1);
   4.110 +qed "zadd_right_cancel_zless";
   4.111 +
   4.112 +Goal "(z$+v $< z$+w) <-> (v $< w)";
   4.113 +by (Simp_tac 1);
   4.114 +qed "zadd_left_cancel_zless";
   4.115 +
   4.116 +Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
   4.117 +
   4.118 +Goal "(v$+z $<= w$+z) <-> (v $<= w)";
   4.119 +by (Simp_tac 1);
   4.120 +qed "zadd_right_cancel_zle";
   4.121 +
   4.122 +Goal "(z$+v $<= z$+w) <-> (v $<= w)";
   4.123 +by (Simp_tac 1);
   4.124 +qed "zadd_left_cancel_zle";
   4.125 +
   4.126 +Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
   4.127 +
   4.128 +(*"v $<= w ==> v$+z $<= w$+z"*)
   4.129 +bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2);
   4.130 +
   4.131 +(*"v $<= w ==> z$+v $<= z$+w"*)
   4.132 +bind_thm ("zadd_zless_mono2", zadd_left_cancel_zless RS iffD2);
   4.133 +
   4.134 +(*"v $<= w ==> v$+z $<= w$+z"*)
   4.135 +bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2);
   4.136 +
   4.137 +(*"v $<= w ==> z$+v $<= z$+w"*)
   4.138 +bind_thm ("zadd_zle_mono2", zadd_left_cancel_zle RS iffD2);
   4.139 +
   4.140 +Goal "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z";
   4.141 +by (etac (zadd_zle_mono1 RS zle_trans) 1);
   4.142 +by (Simp_tac 1);
   4.143 +qed "zadd_zle_mono";
   4.144 +
   4.145 +Goal "[| w' $< w; z' $<= z |] ==> w' $+ z' $< w $+ z";
   4.146 +by (etac (zadd_zless_mono1 RS zless_zle_trans) 1);
   4.147 +by (Simp_tac 1);
   4.148 +qed "zadd_zless_mono";
   4.149 +
   4.150 +
   4.151 +(*** Monotonicity of Multiplication ***)
   4.152 +
   4.153 +Goal "k : nat ==> i $<= j ==> i $* $#k $<= j $* $#k";
   4.154 +by (induct_tac "k" 1);
   4.155 +by (stac int_succ_int_1 2);
   4.156 +by (ALLGOALS 
   4.157 +    (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2, zadd_zle_mono])));
   4.158 +val lemma = result();
   4.159 +
   4.160 +Goal "[| i $<= j;  #0 $<= k |] ==> i$*k $<= j$*k";
   4.161 +by (subgoal_tac "i $* intify(k) $<= j $* intify(k)" 1);
   4.162 +by (Full_simp_tac 1);
   4.163 +by (res_inst_tac [("b", "intify(k)")] (not_zneg_mag RS subst) 1);
   4.164 +by (rtac lemma 3);
   4.165 +by Auto_tac;
   4.166 +by (dtac znegative_imp_zless_0 1);
   4.167 +by (dtac zless_zle_trans 2);
   4.168 +by Auto_tac;  
   4.169 +qed "zmult_zle_mono1";
   4.170 +
   4.171 +Goal "[| i $<= j;  k $<= #0 |] ==> j$*k $<= i$*k";
   4.172 +by (rtac (zminus_zle_zminus RS iffD1) 1);
   4.173 +by (asm_simp_tac (simpset() delsimps [zmult_zminus_right]
   4.174 +                            addsimps [zmult_zminus_right RS sym,
   4.175 +				      zmult_zle_mono1, zle_zminus]) 1);
   4.176 +qed "zmult_zle_mono1_neg";
   4.177 +
   4.178 +Goal "[| i $<= j;  #0 $<= k |] ==> k$*i $<= k$*j";
   4.179 +by (dtac zmult_zle_mono1 1);
   4.180 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute])));
   4.181 +qed "zmult_zle_mono2";
   4.182 +
   4.183 +Goal "[| i $<= j;  k $<= #0 |] ==> k$*j $<= k$*i";
   4.184 +by (dtac zmult_zle_mono1_neg 1);
   4.185 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute])));
   4.186 +qed "zmult_zle_mono2_neg";
   4.187 +
   4.188 +(* $<= monotonicity, BOTH arguments*)
   4.189 +Goal "[| i $<= j;  k $<= l;  #0 $<= j;  #0 $<= k |] ==> i$*k $<= j$*l";
   4.190 +by (etac (zmult_zle_mono1 RS zle_trans) 1);
   4.191 +by (assume_tac 1);
   4.192 +by (etac zmult_zle_mono2 1);
   4.193 +by (assume_tac 1);
   4.194 +qed "zmult_zle_mono";
   4.195 +
   4.196 +
   4.197 +(** strict, in 1st argument; proof is by induction on k>0 **)
   4.198 +
   4.199 +Goal "[| i$<j; k : nat |] ==> 0<k --> $#k $* i $< $#k $* j";
   4.200 +by (induct_tac "k" 1);
   4.201 +by (stac int_succ_int_1 2);
   4.202 +by (etac natE 2);
   4.203 +by (ALLGOALS (asm_full_simp_tac
   4.204 +	      (simpset() addsimps [zadd_zmult_distrib, zadd_zless_mono, 
   4.205 +				   zle_def])));
   4.206 +by (ftac nat_0_le 1);
   4.207 +by (mp_tac 1);
   4.208 +by (subgoal_tac "i $+ (i $+ $# xa $* i) $< j $+ (j $+ $# xa $* j)" 1);
   4.209 +by (Full_simp_tac 1);
   4.210 +by (rtac zadd_zless_mono 1);
   4.211 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [zle_def])));
   4.212 +val lemma = result() RS mp;
   4.213 +
   4.214 +Goal "[| i$<j;  #0 $< k |] ==> k$*i $< k$*j";
   4.215 +by (subgoal_tac "intify(k) $* i $< intify(k) $* j" 1);
   4.216 +by (Full_simp_tac 1);
   4.217 +by (res_inst_tac [("b", "intify(k)")] (not_zneg_mag RS subst) 1);
   4.218 +by (rtac lemma 3);
   4.219 +by Auto_tac;
   4.220 +by (dtac znegative_imp_zless_0 1);
   4.221 +by (dtac zless_trans 2 THEN assume_tac 2);
   4.222 +by (auto_tac (claset(), simpset() addsimps [zero_lt_zmagnitude]));  
   4.223 +qed "zmult_zless_mono2";
   4.224 +
   4.225 +Goal "[| i$<j;  #0 $< k |] ==> i$*k $< j$*k";
   4.226 +by (dtac zmult_zless_mono2 1);
   4.227 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute])));
   4.228 +qed "zmult_zless_mono1";
   4.229 +
   4.230 +(* < monotonicity, BOTH arguments*)
   4.231 +Goal "[| i $< j;  k $< l;  #0 $< j;  #0 $< k |] ==> i$*k $< j$*l";
   4.232 +by (etac (zmult_zless_mono1 RS zless_trans) 1);
   4.233 +by (assume_tac 1);
   4.234 +by (etac zmult_zless_mono2 1);
   4.235 +by (assume_tac 1);
   4.236 +qed "zmult_zless_mono";
   4.237 +
   4.238 +Goal "[| i $< j;  k $< #0 |] ==> j$*k $< i$*k";
   4.239 +by (rtac (zminus_zless_zminus RS iffD1) 1);
   4.240 +by (asm_simp_tac (simpset() delsimps [zmult_zminus_right]
   4.241 +                            addsimps [zmult_zminus_right RS sym,
   4.242 +				      zmult_zless_mono1, zless_zminus]) 1);
   4.243 +qed "zmult_zless_mono1_neg";
   4.244 +
   4.245 +Goal "[| i $< j;  k $< #0 |] ==> k$*j $< k$*i";
   4.246 +by (rtac (zminus_zless_zminus RS iffD1) 1);
   4.247 +by (asm_simp_tac (simpset() delsimps [zmult_zminus]
   4.248 +                            addsimps [zmult_zminus RS sym,
   4.249 +				      zmult_zless_mono2, zless_zminus]) 1);
   4.250 +qed "zmult_zless_mono2_neg";
   4.251 +
   4.252 +Goal "[| m: int; n: int |] ==> (m$*n = #0) <-> (m = #0 | n = #0)";
   4.253 +by (case_tac "m $< #0" 1);
   4.254 +by (auto_tac (claset(), 
   4.255 +     simpset() addsimps [not_zless_iff_zle, zle_def, neq_iff_zless])); 
   4.256 +by (REPEAT 
   4.257 +    (force_tac (claset() addDs [zmult_zless_mono1_neg, zmult_zless_mono1], 
   4.258 +		simpset()) 1));
   4.259 +val lemma = result();
   4.260 +
   4.261 +Goal "(m$*n = #0) <-> (intify(m) = #0 | intify(n) = #0)";
   4.262 +by (asm_full_simp_tac (simpset() addsimps [lemma RS iff_sym]) 1);
   4.263 +qed "zmult_eq_0_iff";
   4.264 +
   4.265 +
   4.266 +Goal "[| m: int; n: int |] ==> #0 $< k ==> (m$*k $< n$*k) <-> (m$<n)";
   4.267 +by (safe_tac (claset() addSIs [zmult_zless_mono1]));
   4.268 +by (cut_facts_tac  [zless_linear] 1);
   4.269 +by Auto_tac;  
   4.270 +by (blast_tac (claset() addIs [zmult_zless_mono1] addEs [zless_asym]) 1);
   4.271 +val lemma = result();
   4.272 +
   4.273 +Goal "#0 $< k ==> (m$*k $< n$*k) <-> (m$<n)";
   4.274 +by (cut_inst_tac [("m","intify(m)"),("n","intify(n)")] lemma 1);
   4.275 +by Auto_tac;  
   4.276 +qed "zmult_zless_cancel2";
   4.277 +
   4.278 +Goal "#0 $< k ==> (k$*m $< k$*n) <-> (m$<n)";
   4.279 +by (dtac zmult_zless_cancel2 1);
   4.280 +by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 1);
   4.281 +qed "zmult_zless_cancel1";
   4.282 +Addsimps [zmult_zless_cancel1, zmult_zless_cancel2];
   4.283 +
   4.284 +Goal "[| m: int; n: int |] ==> k $< #0 ==> (m$*k $< n$*k) <-> (n$<m)";
   4.285 +by (safe_tac (claset() addSIs [zmult_zless_mono1_neg]));
   4.286 +by (cut_facts_tac [zless_linear] 1);
   4.287 +by Auto_tac;  
   4.288 +by (blast_tac (claset() addIs [zmult_zless_mono1_neg] 
   4.289 +                        addEs [zless_asym]) 1);
   4.290 +val lemma = result();
   4.291 +
   4.292 +Goal "k $< #0 ==> (m$*k $< n$*k) <-> (n$<m)";
   4.293 +by (cut_inst_tac [("m","intify(m)"),("n","intify(n)")] lemma 1);
   4.294 +by Auto_tac;  
   4.295 +qed "zmult_zless_cancel2_neg";
   4.296 +
   4.297 +Goal "k $< #0 ==> (k$*m $< k$*n) <-> (n$<m)";
   4.298 +by (dtac zmult_zless_cancel2_neg 1);
   4.299 +by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 1);
   4.300 +qed "zmult_zless_cancel1_neg";
   4.301 +Addsimps [zmult_zless_cancel1_neg, zmult_zless_cancel2_neg];
   4.302 +
   4.303 +Goal "#0 $< k ==> (m$*k $<= n$*k) <-> (m$<=n)";
   4.304 +by (asm_full_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
   4.305 +qed "zmult_zle_cancel2";
   4.306 +
   4.307 +Goal "#0 $< k ==> (k$*m $<= k$*n) <-> (m$<=n)";
   4.308 +by (asm_full_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
   4.309 +qed "zmult_zle_cancel1";
   4.310 +Addsimps [zmult_zle_cancel1, zmult_zle_cancel2];
   4.311 +
   4.312 +Goal "k $< #0 ==> (m$*k $<= n$*k) <-> (n$<=m)";
   4.313 +by (asm_full_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
   4.314 +qed "zmult_zle_cancel2_neg";
   4.315 +
   4.316 +Goal "k $< #0 ==> (k$*m $<= k$*n) <-> (n$<=m)";
   4.317 +by (asm_full_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
   4.318 +qed "zmult_zle_cancel1_neg";
   4.319 +Addsimps [zmult_zle_cancel1_neg, zmult_zle_cancel2_neg];
   4.320 +
   4.321 +Goal "[| k ~= #0; k: int; m: int; n: int |] ==> (m$*k = n$*k) <-> (m=n)";
   4.322 +by (rotate_tac 1 1); 
   4.323 +by (cut_inst_tac [("z","m"),("w","n")] zless_linear 1);
   4.324 +by Safe_tac;
   4.325 +by (asm_full_simp_tac (simpset() addsimps []) 2);
   4.326 +by (REPEAT 
   4.327 +    (force_tac (claset() addD2 ("mono_neg", zmult_zless_mono1_neg)
   4.328 +                         addD2 ("mono_pos", zmult_zless_mono1), 
   4.329 +		simpset() addsimps [neq_iff_zless]) 1));
   4.330 +qed "zmult_cancel2";
   4.331 +
   4.332 +Goal "intify(k) ~= #0 ==> (m$*k = n$*k) <-> (intify(m) = intify(n))";
   4.333 +by (rtac iff_trans 1);
   4.334 +by (rtac zmult_cancel2 2);
   4.335 +by Auto_tac;  
   4.336 +qed "zmult_cancel2_intify";
   4.337 +
   4.338 +Goal "[| k ~= #0; k: int; m: int; n: int |] ==> (k$*m = k$*n) <-> (m=n)";
   4.339 +by (dtac zmult_cancel2 1);
   4.340 +by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 4);
   4.341 +by Auto_tac;  
   4.342 +qed "zmult_cancel1";
   4.343 +
   4.344 +Goal "intify(k) ~= #0 ==> (k$*m = k$*n) <-> (intify(m) = intify(n))";
   4.345 +by (rtac iff_trans 1);
   4.346 +by (rtac zmult_cancel1 2);
   4.347 +by Auto_tac;  
   4.348 +qed "zmult_cancel1_intify";
   4.349 +Addsimps [zmult_cancel1, zmult_cancel2];
   4.350 +
   4.351 +
   4.352 +(*** Uniqueness and monotonicity of quotients and remainders ***)
   4.353 +
   4.354 +
   4.355 +Goal "[| b$*q' $+ r' $<= b$*q $+ r;  #0 $<= r';  #0 $< b;  r $< b |] \
   4.356 +\     ==> q' $<= q";
   4.357 +by (subgoal_tac "r' $+ b $* (q'$-q) $<= r" 1);
   4.358 +by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]@zadd_ac@zcompare_rls) 2);
   4.359 +by (subgoal_tac "#0 $< b $* (#1 $+ q $- q')" 1);
   4.360 +by (etac zle_zless_trans 2);
   4.361 +by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
   4.362 +				       zadd_zmult_distrib2]@zadd_ac@zcompare_rls) 2);
   4.363 +by (etac zle_zless_trans 2);
   4.364 +by (Asm_simp_tac 2);
   4.365 +by (subgoal_tac "b $* q' $< b $* (#1 $+ q)" 1);
   4.366 +by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
   4.367 +				       zadd_zmult_distrib2]@zadd_ac@zcompare_rls) 2);
   4.368 +by (asm_full_simp_tac (simpset() addsimps [zless_add1_iff_zle]@
   4.369 +                                          zadd_ac@zcompare_rls) 1);
   4.370 +qed "unique_quotient_lemma";
   4.371 +
   4.372 +Goal "[| b$*q' $+ r' $<= b$*q $+ r;  r $<= #0;  b $< #0;  b $< r' |] \
   4.373 +\     ==> q $<= q'";
   4.374 +by (res_inst_tac [("b", "$-b"), ("r", "$-r'"), ("r'", "$-r")] 
   4.375 +    unique_quotient_lemma 1);
   4.376 +by (auto_tac (claset(), 
   4.377 +	      simpset() delsimps [zminus_zadd_distrib]
   4.378 +			addsimps [zminus_zadd_distrib RS sym,
   4.379 +	                          zle_zminus, zless_zminus])); 
   4.380 +qed "unique_quotient_lemma_neg";
   4.381 +
   4.382 +
   4.383 +Goal "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b: int; b ~= #0; \
   4.384 +\        q: int; q' : int |] ==> q = q'";
   4.385 +by (asm_full_simp_tac 
   4.386 +    (simpset() addsimps split_ifs@
   4.387 +                        [quorem_def, neq_iff_zless]) 1);
   4.388 +by Safe_tac; 
   4.389 +by (ALLGOALS Asm_full_simp_tac);
   4.390 +by (REPEAT 
   4.391 +    (blast_tac (claset() addIs [zle_anti_sym]
   4.392 +			 addDs [zle_eq_refl RS unique_quotient_lemma, 
   4.393 +				zle_eq_refl RS unique_quotient_lemma_neg,
   4.394 +				sym]) 1));
   4.395 +qed "unique_quotient";
   4.396 +
   4.397 +
   4.398 +Goal "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b: int; b ~= #0; \
   4.399 +\        q: int; q' : int; \
   4.400 +\        r: int; r' : int |] ==> r = r'";
   4.401 +by (subgoal_tac "q = q'" 1);
   4.402 +by (blast_tac (claset() addIs [unique_quotient]) 2);
   4.403 +by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
   4.404 +by Auto_tac;  
   4.405 +qed "unique_remainder";
   4.406 +
   4.407 +
   4.408 +(*** THE REST TO PORT LATER.  The division algorithm can wait; most properties
   4.409 +     of division flow from the uniqueness properties proved above...
   4.410 +
   4.411 +
   4.412 + (*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)
   4.413 +
   4.414 +
   4.415 + Goal "adjust a b <q,r> = (let diff = r$-b in \
   4.416 + \                         if #0 $<= diff then <#2$*q $+ #1,diff>  \
   4.417 + \                                       else <#2$*q,r>)";
   4.418 + by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1);
   4.419 + qed "adjust_eq";
   4.420 + Addsimps [adjust_eq];
   4.421 +
   4.422 + (*Proving posDivAlg's termination condition*)
   4.423 + val [tc] = posDivAlg.tcs;
   4.424 + goalw_cterm [] (cterm_of (sign_of (the_context ())) (HOLogic.mk_Trueprop tc));
   4.425 + by Auto_tac;
   4.426 + val lemma = result();
   4.427 +
   4.428 + (* removing the termination condition from the generated theorems *)
   4.429 +
   4.430 + bind_thm ("posDivAlg_raw_eqn", lemma RS hd posDivAlg.simps);
   4.431 +
   4.432 + (**use with simproc to avoid re-proving the premise*)
   4.433 + Goal "#0 $< b ==> \
   4.434 + \     posDivAlg <a,b> =      \
   4.435 + \      (if a$<b then <#0,a> else adjust a b (posDivAlg<a,#2$*b>))";
   4.436 + by (rtac (posDivAlg_raw_eqn RS trans) 1);
   4.437 + by (Asm_simp_tac 1);
   4.438 + qed "posDivAlg_eqn";
   4.439 +
   4.440 + bind_thm ("posDivAlg_induct", lemma RS posDivAlg.induct);
   4.441 +
   4.442 +
   4.443 + (*Correctness of posDivAlg: it computes quotients correctly*)
   4.444 + Goal "#0 $<= a --> #0 $< b --> quorem (<a,b>, posDivAlg <a,b>)";
   4.445 + by (res_inst_tac [("u", "a"), ("v", "b")] posDivAlg_induct 1);
   4.446 + by Auto_tac;
   4.447 + by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
   4.448 + (*base case: a<b*)
   4.449 + by (asm_full_simp_tac (simpset() addsimps [posDivAlg_eqn]) 1);
   4.450 + (*main argument*)
   4.451 + by (stac posDivAlg_eqn 1);
   4.452 + by (ALLGOALS Asm_simp_tac);
   4.453 + by (etac splitE 1);
   4.454 + by (auto_tac (claset(), simpset() addsimps [zadd_zmult_distrib2, Let_def]));
   4.455 + qed_spec_mp "posDivAlg_correct";
   4.456 +
   4.457 +
   4.458 + (*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***)
   4.459 +
   4.460 + (*Proving negDivAlg's termination condition*)
   4.461 + val [tc] = negDivAlg.tcs;
   4.462 + goalw_cterm [] (cterm_of (sign_of (the_context ())) (HOLogic.mk_Trueprop tc));
   4.463 + by Auto_tac;
   4.464 + val lemma = result();
   4.465 +
   4.466 + (* removing the termination condition from the generated theorems *)
   4.467 +
   4.468 + bind_thm ("negDivAlg_raw_eqn", lemma RS hd negDivAlg.simps);
   4.469 +
   4.470 + (**use with simproc to avoid re-proving the premise*)
   4.471 + Goal "#0 $< b ==> \
   4.472 + \     negDivAlg <a,b> =      \
   4.473 + \      (if #0$<=a$+b then <#-1,a$+b> else adjust a b (negDivAlg<a,#2$*b>))";
   4.474 + by (rtac (negDivAlg_raw_eqn RS trans) 1);
   4.475 + by (Asm_simp_tac 1);
   4.476 + qed "negDivAlg_eqn";
   4.477 +
   4.478 + bind_thm ("negDivAlg_induct", lemma RS negDivAlg.induct);
   4.479 +
   4.480 +
   4.481 + (*Correctness of negDivAlg: it computes quotients correctly
   4.482 +   It doesn't work if a=0 because the 0/b=0 rather than -1*)
   4.483 + Goal "a $< #0 --> #0 $< b --> quorem (<a,b>, negDivAlg <a,b>)";
   4.484 + by (res_inst_tac [("u", "a"), ("v", "b")] negDivAlg_induct 1);
   4.485 + by Auto_tac;
   4.486 + by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
   4.487 + (*base case: 0$<=a$+b*)
   4.488 + by (asm_full_simp_tac (simpset() addsimps [negDivAlg_eqn]) 1);
   4.489 + (*main argument*)
   4.490 + by (stac negDivAlg_eqn 1);
   4.491 + by (ALLGOALS Asm_simp_tac);
   4.492 + by (etac splitE 1);
   4.493 + by (auto_tac (claset(), simpset() addsimps [zadd_zmult_distrib2, Let_def]));
   4.494 + qed_spec_mp "negDivAlg_correct";
   4.495 +
   4.496 +
   4.497 + (*** Existence shown by proving the division algorithm to be correct ***)
   4.498 +
   4.499 + (*the case a=0*)
   4.500 + Goal "b ~= #0 ==> quorem (<#0,b>, <#0,#0>)";
   4.501 + by (auto_tac (claset(), 
   4.502 +	       simpset() addsimps [quorem_def, neq_iff_zless]));
   4.503 + qed "quorem_0";
   4.504 +
   4.505 + Goal "posDivAlg <#0,b> = <#0,#0>";
   4.506 + by (stac posDivAlg_raw_eqn 1);
   4.507 + by Auto_tac;
   4.508 + qed "posDivAlg_0";
   4.509 + Addsimps [posDivAlg_0];
   4.510 +
   4.511 + Goal "negDivAlg <#-1,b> = <#-1,b-#1>";
   4.512 + by (stac negDivAlg_raw_eqn 1);
   4.513 + by Auto_tac;
   4.514 + qed "negDivAlg_minus1";
   4.515 + Addsimps [negDivAlg_minus1];
   4.516 +
   4.517 + Goalw [negateSnd_def] "negateSnd<q,r> = <q,-r>";
   4.518 + by Auto_tac;
   4.519 + qed "negateSnd_eq";
   4.520 + Addsimps [negateSnd_eq];
   4.521 +
   4.522 + Goal "quorem (<-a,-b>, qr) ==> quorem (<a,b>, negateSnd qr)";
   4.523 + by (auto_tac (claset(), simpset() addsimps split_ifs@[quorem_def]));
   4.524 + qed "quorem_neg";
   4.525 +
   4.526 + Goal "b ~= #0 ==> quorem (<a,b>, divAlg<a,b>)";
   4.527 + by (auto_tac (claset(), 
   4.528 +	       simpset() addsimps [quorem_0, divAlg_def]));
   4.529 + by (REPEAT_FIRST (resolve_tac [quorem_neg, posDivAlg_correct,
   4.530 +				negDivAlg_correct]));
   4.531 + by (auto_tac (claset(), 
   4.532 +	       simpset() addsimps [quorem_def, neq_iff_zless]));
   4.533 + qed "divAlg_correct";
   4.534 +
   4.535 + (** Aribtrary definitions for division by zero.  Useful to simplify 
   4.536 +     certain equations **)
   4.537 +
   4.538 + Goal "a div (#0::int) = #0";
   4.539 + by (simp_tac (simpset() addsimps [div_def, divAlg_def, posDivAlg_raw_eqn]) 1);
   4.540 + qed "DIVISION_BY_ZERO_ZDIV";  (*NOT for adding to default simpset*)
   4.541 +
   4.542 + Goal "a mod (#0::int) = a";
   4.543 + by (simp_tac (simpset() addsimps [mod_def, divAlg_def, posDivAlg_raw_eqn]) 1);
   4.544 + qed "DIVISION_BY_ZERO_ZMOD";  (*NOT for adding to default simpset*)
   4.545 +
   4.546 + fun zdiv_undefined_case_tac s i =
   4.547 +   case_tac s i THEN 
   4.548 +   asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_ZDIV, 
   4.549 +				     DIVISION_BY_ZERO_ZMOD]) i;
   4.550 +
   4.551 + (** Basic laws about division and remainder **)
   4.552 +
   4.553 + Goal "a = b $* (a div b) $+ (a mod b)";
   4.554 + by (zdiv_undefined_case_tac "b = #0" 1);
   4.555 + by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
   4.556 + by (auto_tac (claset(), 
   4.557 +	       simpset() addsimps [quorem_def, div_def, mod_def]));
   4.558 + qed "zmod_zdiv_equality";  
   4.559 +
   4.560 + Goal "(#0::int) $< b ==> #0 $<= a mod b & a mod b $< b";
   4.561 + by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
   4.562 + by (auto_tac (claset(), 
   4.563 +	       simpset() addsimps [quorem_def, mod_def]));
   4.564 + bind_thm ("pos_mod_sign", result() RS conjunct1);
   4.565 + bind_thm ("pos_mod_bound", result() RS conjunct2);
   4.566 +
   4.567 + Goal "b $< (#0::int) ==> a mod b $<= #0 & b $< a mod b";
   4.568 + by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
   4.569 + by (auto_tac (claset(), 
   4.570 +	       simpset() addsimps [quorem_def, div_def, mod_def]));
   4.571 + bind_thm ("neg_mod_sign", result() RS conjunct1);
   4.572 + bind_thm ("neg_mod_bound", result() RS conjunct2);
   4.573 +
   4.574 +
   4.575 + (** proving general properties of div and mod **)
   4.576 +
   4.577 + Goal "b ~= #0 ==> quorem (<a,b>, <a div b,a mod b>)";
   4.578 + by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   4.579 + by (auto_tac
   4.580 +     (claset(),
   4.581 +      simpset() addsimps [quorem_def, neq_iff_zless, 
   4.582 +			  pos_mod_sign,pos_mod_bound,
   4.583 +			  neg_mod_sign, neg_mod_bound]));
   4.584 + qed "quorem_div_mod";
   4.585 +
   4.586 + Goal "[| quorem(<a,b>,<q,r>);  b ~= #0 |] ==> a div b = q";
   4.587 + by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1);
   4.588 + qed "quorem_div";
   4.589 +
   4.590 + Goal "[| quorem(<a,b>,<q,r>);  b ~= #0 |] ==> a mod b = r";
   4.591 + by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1);
   4.592 + qed "quorem_mod";
   4.593 +
   4.594 + Goal "[| (#0::int) $<= a;  a $< b |] ==> a div b = #0";
   4.595 + by (rtac quorem_div 1);
   4.596 + by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   4.597 + qed "div_pos_pos_trivial";
   4.598 +
   4.599 + Goal "[| a $<= (#0::int);  b $< a |] ==> a div b = #0";
   4.600 + by (rtac quorem_div 1);
   4.601 + by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   4.602 + qed "div_neg_neg_trivial";
   4.603 +
   4.604 + Goal "[| (#0::int) $< a;  a$+b $<= #0 |] ==> a div b = #-1";
   4.605 + by (rtac quorem_div 1);
   4.606 + by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   4.607 + qed "div_pos_neg_trivial";
   4.608 +
   4.609 + (*There is no div_neg_pos_trivial because  #0 div b = #0 would supersede it*)
   4.610 +
   4.611 + Goal "[| (#0::int) $<= a;  a $< b |] ==> a mod b = a";
   4.612 + by (res_inst_tac [("q","#0")] quorem_mod 1);
   4.613 + by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   4.614 + qed "mod_pos_pos_trivial";
   4.615 +
   4.616 + Goal "[| a $<= (#0::int);  b $< a |] ==> a mod b = a";
   4.617 + by (res_inst_tac [("q","#0")] quorem_mod 1);
   4.618 + by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   4.619 + qed "mod_neg_neg_trivial";
   4.620 +
   4.621 + Goal "[| (#0::int) $< a;  a$+b $<= #0 |] ==> a mod b = a$+b";
   4.622 + by (res_inst_tac [("q","#-1")] quorem_mod 1);
   4.623 + by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   4.624 + qed "mod_pos_neg_trivial";
   4.625 +
   4.626 + (*There is no mod_neg_pos_trivial...*)
   4.627 +
   4.628 +
   4.629 + (*Simpler laws such as -a div b = -(a div b) FAIL*)
   4.630 + Goal "(-a) div (-b) = a div b";
   4.631 + by (zdiv_undefined_case_tac "b = #0" 1);
   4.632 + by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) 
   4.633 +	   RS quorem_div) 1);
   4.634 + by Auto_tac;
   4.635 + qed "zdiv_zminus_zminus";
   4.636 + Addsimps [zdiv_zminus_zminus];
   4.637 +
   4.638 + (*Simpler laws such as -a mod b = -(a mod b) FAIL*)
   4.639 + Goal "(-a) mod (-b) = - (a mod b)";
   4.640 + by (zdiv_undefined_case_tac "b = #0" 1);
   4.641 + by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) 
   4.642 +	   RS quorem_mod) 1);
   4.643 + by Auto_tac;
   4.644 + qed "zmod_zminus_zminus";
   4.645 + Addsimps [zmod_zminus_zminus];
   4.646 +
   4.647 +
   4.648 + (*** division of a number by itself ***)
   4.649 +
   4.650 + Goal "[| (#0::int) $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q";
   4.651 + by (subgoal_tac "#0 $< a$*q" 1);
   4.652 + by (arith_tac 2);
   4.653 + by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
   4.654 + val lemma1 = result();
   4.655 +
   4.656 + Goal "[| (#0::int) $< a; a = r $+ a$*q; #0 $<= r |] ==> q $<= #1";
   4.657 + by (subgoal_tac "#0 $<= a$*(#1$-q)" 1);
   4.658 + by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
   4.659 + by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
   4.660 + val lemma2 = result();
   4.661 +
   4.662 + Goal "[| quorem(<a,a>,<q,r>);  a ~= (#0::int) |] ==> q = #1";
   4.663 + by (asm_full_simp_tac 
   4.664 +     (simpset() addsimps split_ifs@[quorem_def, neq_iff_zless]) 1);
   4.665 + by (rtac order_antisym 1);
   4.666 + by Safe_tac;
   4.667 + by Auto_tac;
   4.668 + by (res_inst_tac [("a", "-a"),("r", "-r")] lemma1 3);
   4.669 + by (res_inst_tac [("a", "-a"),("r", "-r")] lemma2 1);
   4.670 + by (REPEAT (force_tac  (claset() addIs [lemma1,lemma2], 
   4.671 +	       simpset() addsimps [zadd_commute, zmult_zminus]) 1));
   4.672 + qed "self_quotient";
   4.673 +
   4.674 + Goal "[| quorem(<a,a>,<q,r>);  a ~= (#0::int) |] ==> r = #0";
   4.675 + by (ftac self_quotient 1);
   4.676 + by (assume_tac 1);
   4.677 + by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
   4.678 + qed "self_remainder";
   4.679 +
   4.680 + Goal "a ~= #0 ==> a div a = (#1::int)";
   4.681 + by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_quotient]) 1);
   4.682 + qed "zdiv_self";
   4.683 + Addsimps [zdiv_self];
   4.684 +
   4.685 + (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
   4.686 + Goal "a mod a = (#0::int)";
   4.687 + by (zdiv_undefined_case_tac "a = #0" 1);
   4.688 + by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_remainder]) 1);
   4.689 + qed "zmod_self";
   4.690 + Addsimps [zmod_self];
   4.691 +
   4.692 +
   4.693 + (*** Computation of division and remainder ***)
   4.694 +
   4.695 + Goal "(#0::int) div b = #0";
   4.696 + by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   4.697 + qed "zdiv_zero";
   4.698 +
   4.699 + Goal "(#0::int) $< b ==> #-1 div b = #-1";
   4.700 + by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   4.701 + qed "div_eq_minus1";
   4.702 +
   4.703 + Goal "(#0::int) mod b = #0";
   4.704 + by (simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   4.705 + qed "zmod_zero";
   4.706 +
   4.707 + Addsimps [zdiv_zero, zmod_zero];
   4.708 +
   4.709 + Goal "(#0::int) $< b ==> #-1 div b = #-1";
   4.710 + by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   4.711 + qed "zdiv_minus1";
   4.712 +
   4.713 + Goal "(#0::int) $< b ==> #-1 mod b = b-#1";
   4.714 + by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   4.715 + qed "zmod_minus1";
   4.716 +
   4.717 + (** a positive, b positive **)
   4.718 +
   4.719 + Goal "[| #0 $< a;  #0 $<= b |] ==> a div b = fst (posDivAlg<a,b>)";
   4.720 + by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   4.721 + qed "div_pos_pos";
   4.722 +
   4.723 + Goal "[| #0 $< a;  #0 $<= b |] ==> a mod b = snd (posDivAlg<a,b>)";
   4.724 + by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   4.725 + qed "mod_pos_pos";
   4.726 +
   4.727 + (** a negative, b positive **)
   4.728 +
   4.729 + Goal "[| a $< #0;  #0 $< b |] ==> a div b = fst (negDivAlg<a,b>)";
   4.730 + by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   4.731 + qed "div_neg_pos";
   4.732 +
   4.733 + Goal "[| a $< #0;  #0 $< b |] ==> a mod b = snd (negDivAlg<a,b>)";
   4.734 + by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   4.735 + qed "mod_neg_pos";
   4.736 +
   4.737 + (** a positive, b negative **)
   4.738 +
   4.739 + Goal "[| #0 $< a;  b $< #0 |] ==> a div b = fst (negateSnd(negDivAlg<-a,-b>))";
   4.740 + by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   4.741 + qed "div_pos_neg";
   4.742 +
   4.743 + Goal "[| #0 $< a;  b $< #0 |] ==> a mod b = snd (negateSnd(negDivAlg<-a,-b>))";
   4.744 + by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   4.745 + qed "mod_pos_neg";
   4.746 +
   4.747 + (** a negative, b negative **)
   4.748 +
   4.749 + Goal "[| a $< #0;  b $<= #0 |] ==> a div b = fst (negateSnd(posDivAlg<-a,-b>))";
   4.750 + by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   4.751 + qed "div_neg_neg";
   4.752 +
   4.753 + Goal "[| a $< #0;  b $<= #0 |] ==> a mod b = snd (negateSnd(posDivAlg<-a,-b>))";
   4.754 + by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   4.755 + qed "mod_neg_neg";
   4.756 +
   4.757 + Addsimps (map (read_instantiate_sg (sign_of (the_context ()))
   4.758 +		[("a", "number_of ?v"), ("b", "number_of ?w")])
   4.759 +	   [div_pos_pos, div_neg_pos, div_pos_neg, div_neg_neg,
   4.760 +	    mod_pos_pos, mod_neg_pos, mod_pos_neg, mod_neg_neg,
   4.761 +	    posDivAlg_eqn, negDivAlg_eqn]);
   4.762 +
   4.763 +
   4.764 + (** Special-case simplification **)
   4.765 +
   4.766 + Goal "a mod (#1::int) = #0";
   4.767 + by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_sign 1);
   4.768 + by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_bound 2);
   4.769 + by Auto_tac;
   4.770 + qed "zmod_1";
   4.771 + Addsimps [zmod_1];
   4.772 +
   4.773 + Goal "a div (#1::int) = a";
   4.774 + by (cut_inst_tac [("a","a"),("b","#1")] zmod_zdiv_equality 1);
   4.775 + by Auto_tac;
   4.776 + qed "zdiv_1";
   4.777 + Addsimps [zdiv_1];
   4.778 +
   4.779 + Goal "a mod (#-1::int) = #0";
   4.780 + by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_sign 1);
   4.781 + by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_bound 2);
   4.782 + by Auto_tac;
   4.783 + qed "zmod_minus1_right";
   4.784 + Addsimps [zmod_minus1_right];
   4.785 +
   4.786 + Goal "a div (#-1::int) = -a";
   4.787 + by (cut_inst_tac [("a","a"),("b","#-1")] zmod_zdiv_equality 1);
   4.788 + by Auto_tac;
   4.789 + qed "zdiv_minus1_right";
   4.790 + Addsimps [zdiv_minus1_right];
   4.791 +
   4.792 +
   4.793 + (*** Monotonicity in the first argument (divisor) ***)
   4.794 +
   4.795 + Goal "[| a $<= a';  #0 $< b |] ==> a div b $<= a' div b";
   4.796 + by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   4.797 + by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1);
   4.798 + by (rtac unique_quotient_lemma 1);
   4.799 + by (etac subst 1);
   4.800 + by (etac subst 1);
   4.801 + by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
   4.802 + qed "zdiv_mono1";
   4.803 +
   4.804 + Goal "[| a $<= a';  b $< #0 |] ==> a' div b $<= a div b";
   4.805 + by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   4.806 + by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1);
   4.807 + by (rtac unique_quotient_lemma_neg 1);
   4.808 + by (etac subst 1);
   4.809 + by (etac subst 1);
   4.810 + by (ALLGOALS (asm_simp_tac (simpset() addsimps [neg_mod_sign,neg_mod_bound])));
   4.811 + qed "zdiv_mono1_neg";
   4.812 +
   4.813 +
   4.814 + (*** Monotonicity in the second argument (dividend) ***)
   4.815 +
   4.816 + Goal "[| b$*q $+ r = b'$*q' $+ r';  #0 $<= b'$*q' $+ r';  \
   4.817 + \        r' $< b';  #0 $<= r;  #0 $< b';  b' $<= b |]  \
   4.818 + \     ==> q $<= q'";
   4.819 + by (subgoal_tac "#0 $<= q'" 1);
   4.820 +  by (subgoal_tac "#0 $< b'$*(q' $+ #1)" 2);
   4.821 +   by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3);
   4.822 +  by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 2);
   4.823 + by (subgoal_tac "b$*q $< b$*(q' $+ #1)" 1);
   4.824 +  by (Asm_full_simp_tac 1);
   4.825 + by (subgoal_tac "b$*q = r' $- r $+ b'$*q'" 1);
   4.826 +  by (Simp_tac 2);
   4.827 + by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
   4.828 + by (stac zadd_commute 1 THEN rtac zadd_zless_mono 1 THEN arith_tac 1);
   4.829 + by (rtac zmult_zle_mono1 1);
   4.830 + by Auto_tac;
   4.831 + qed "zdiv_mono2_lemma";
   4.832 +
   4.833 + Goal "[| (#0::int) $<= a;  #0 $< b';  b' $<= b |]  \
   4.834 + \     ==> a div b $<= a div b'";
   4.835 + by (subgoal_tac "b ~= #0" 1);
   4.836 + by (arith_tac 2);
   4.837 + by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   4.838 + by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1);
   4.839 + by (rtac zdiv_mono2_lemma 1);
   4.840 + by (etac subst 1);
   4.841 + by (etac subst 1);
   4.842 + by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
   4.843 + qed "zdiv_mono2";
   4.844 +
   4.845 + Goal "[| b$*q $+ r = b'$*q' $+ r';  b'$*q' $+ r' $< #0;  \
   4.846 + \        r $< b;  #0 $<= r';  #0 $< b';  b' $<= b |]  \
   4.847 + \     ==> q' $<= q";
   4.848 + by (subgoal_tac "q' $< #0" 1);
   4.849 +  by (subgoal_tac "b'$*q' $< #0" 2);
   4.850 +   by (arith_tac 3);
   4.851 +  by (asm_full_simp_tac (simpset() addsimps [zmult_less_0_iff]) 2);
   4.852 + by (subgoal_tac "b$*q' $< b$*(q $+ #1)" 1);
   4.853 +  by (Asm_full_simp_tac 1);
   4.854 + by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
   4.855 + by (subgoal_tac "b$*q' $<= b'$*q'" 1);
   4.856 +  by (asm_simp_tac (simpset() addsimps [zmult_zle_mono1_neg]) 2);
   4.857 + by (subgoal_tac "b'$*q' $< b $+ b$*q" 1);
   4.858 +  by (Asm_simp_tac 2);
   4.859 + by (arith_tac 1);
   4.860 + qed "zdiv_mono2_neg_lemma";
   4.861 +
   4.862 + Goal "[| a $< (#0::int);  #0 $< b';  b' $<= b |]  \
   4.863 + \     ==> a div b' $<= a div b";
   4.864 + by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   4.865 + by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1);
   4.866 + by (rtac zdiv_mono2_neg_lemma 1);
   4.867 + by (etac subst 1);
   4.868 + by (etac subst 1);
   4.869 + by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
   4.870 + qed "zdiv_mono2_neg";
   4.871 +
   4.872 +
   4.873 + (*** More algebraic laws for div and mod ***)
   4.874 +
   4.875 + (** proving (a*b) div c = a $* (b div c) $+ a * (b mod c) **)
   4.876 +
   4.877 + Goal "[| quorem(<b,c>,<q,r>);  c ~= #0 |] \
   4.878 + \     ==> quorem (<a$*b,c>, <a$*q $+ a$*r div c,a$*r mod c>)";
   4.879 + by (auto_tac
   4.880 +     (claset(),
   4.881 +      simpset() addsimps split_ifs@
   4.882 +			 [quorem_def, neq_iff_zless, 
   4.883 +			  zadd_zmult_distrib2,
   4.884 +			  pos_mod_sign,pos_mod_bound,
   4.885 +			  neg_mod_sign, neg_mod_bound]));
   4.886 + by (ALLGOALS(rtac zmod_zdiv_equality));
   4.887 + val lemma = result();
   4.888 +
   4.889 + Goal "(a$*b) div c = a$*(b div c) $+ a$*(b mod c) div c";
   4.890 + by (zdiv_undefined_case_tac "c = #0" 1);
   4.891 + by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
   4.892 + qed "zdiv_zmult1_eq";
   4.893 +
   4.894 + Goal "(a$*b) mod c = a$*(b mod c) mod c";
   4.895 + by (zdiv_undefined_case_tac "c = #0" 1);
   4.896 + by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
   4.897 + qed "zmod_zmult1_eq";
   4.898 +
   4.899 + Goal "(a$*b) mod c = ((a mod c) $* b) mod c";
   4.900 + by (rtac trans 1);
   4.901 + by (res_inst_tac [("s","b$*a mod c")] trans 1);
   4.902 + by (rtac zmod_zmult1_eq 2);
   4.903 + by (ALLGOALS (simp_tac (simpset() addsimps [zmult_commute])));
   4.904 + qed "zmod_zmult1_eq'";
   4.905 +
   4.906 + Goal "(a$*b) mod c = ((a mod c) $* (b mod c)) mod c";
   4.907 + by (rtac (zmod_zmult1_eq' RS trans) 1);
   4.908 + by (rtac zmod_zmult1_eq 1);
   4.909 + qed "zmod_zmult_distrib";
   4.910 +
   4.911 + Goal "b ~= (#0::int) ==> (a$*b) div b = a";
   4.912 + by (asm_simp_tac (simpset() addsimps [zdiv_zmult1_eq]) 1);
   4.913 + qed "zdiv_zmult_self1";
   4.914 +
   4.915 + Goal "b ~= (#0::int) ==> (b$*a) div b = a";
   4.916 + by (stac zmult_commute 1 THEN etac zdiv_zmult_self1 1);
   4.917 + qed "zdiv_zmult_self2";
   4.918 +
   4.919 + Addsimps [zdiv_zmult_self1, zdiv_zmult_self2];
   4.920 +
   4.921 + Goal "(a$*b) mod b = (#0::int)";
   4.922 + by (simp_tac (simpset() addsimps [zmod_zmult1_eq]) 1);
   4.923 + qed "zmod_zmult_self1";
   4.924 +
   4.925 + Goal "(b$*a) mod b = (#0::int)";
   4.926 + by (simp_tac (simpset() addsimps [zmult_commute, zmod_zmult1_eq]) 1);
   4.927 + qed "zmod_zmult_self2";
   4.928 +
   4.929 + Addsimps [zmod_zmult_self1, zmod_zmult_self2];
   4.930 +
   4.931 +
   4.932 + (** proving (a$+b) div c = a div c $+ b div c $+ ((a mod c $+ b mod c) div c) **)
   4.933 +
   4.934 + Goal "[| quorem(<a,c>,<aq,ar>);  quorem(<b,c>,<bq,br>);  c ~= #0 |] \
   4.935 + \     ==> quorem (<a$+b,c>, (aq $+ bq $+ (ar$+br) div c, (ar$+br) mod c))";
   4.936 + by (auto_tac
   4.937 +     (claset(),
   4.938 +      simpset() addsimps split_ifs@
   4.939 +			 [quorem_def, neq_iff_zless, 
   4.940 +			  zadd_zmult_distrib2,
   4.941 +			  pos_mod_sign,pos_mod_bound,
   4.942 +			  neg_mod_sign, neg_mod_bound]));
   4.943 + by (ALLGOALS(rtac zmod_zdiv_equality));
   4.944 + val lemma = result();
   4.945 +
   4.946 + (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   4.947 + Goal "(a$+b) div c = a div c $+ b div c $+ ((a mod c $+ b mod c) div c)";
   4.948 + by (zdiv_undefined_case_tac "c = #0" 1);
   4.949 + by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
   4.950 +				MRS lemma RS quorem_div]) 1);
   4.951 + qed "zdiv_zadd1_eq";
   4.952 +
   4.953 + Goal "(a$+b) mod c = (a mod c $+ b mod c) mod c";
   4.954 + by (zdiv_undefined_case_tac "c = #0" 1);
   4.955 + by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
   4.956 +				MRS lemma RS quorem_mod]) 1);
   4.957 + qed "zmod_zadd1_eq";
   4.958 +
   4.959 + Goal "(a mod b) div b = (#0::int)";
   4.960 + by (zdiv_undefined_case_tac "b = #0" 1);
   4.961 + by (auto_tac (claset(), 
   4.962 +	simpset() addsimps [neq_iff_zless, 
   4.963 +			    pos_mod_sign, pos_mod_bound, div_pos_pos_trivial, 
   4.964 +			    neg_mod_sign, neg_mod_bound, div_neg_neg_trivial]));
   4.965 + qed "mod_div_trivial";
   4.966 + Addsimps [mod_div_trivial];
   4.967 +
   4.968 + Goal "(a mod b) mod b = a mod b";
   4.969 + by (zdiv_undefined_case_tac "b = #0" 1);
   4.970 + by (auto_tac (claset(), 
   4.971 +	simpset() addsimps [neq_iff_zless, 
   4.972 +			    pos_mod_sign, pos_mod_bound, mod_pos_pos_trivial, 
   4.973 +			    neg_mod_sign, neg_mod_bound, mod_neg_neg_trivial]));
   4.974 + qed "mod_mod_trivial";
   4.975 + Addsimps [mod_mod_trivial];
   4.976 +
   4.977 + Goal "(a$+b) mod c = ((a mod c) $+ b) mod c";
   4.978 + by (rtac (trans RS sym) 1);
   4.979 + by (rtac zmod_zadd1_eq 1);
   4.980 + by (Simp_tac 1);
   4.981 + by (rtac (zmod_zadd1_eq RS sym) 1);
   4.982 + qed "zmod_zadd_left_eq";
   4.983 +
   4.984 + Goal "(a$+b) mod c = (a $+ (b mod c)) mod c";
   4.985 + by (rtac (trans RS sym) 1);
   4.986 + by (rtac zmod_zadd1_eq 1);
   4.987 + by (Simp_tac 1);
   4.988 + by (rtac (zmod_zadd1_eq RS sym) 1);
   4.989 + qed "zmod_zadd_right_eq";
   4.990 +
   4.991 +
   4.992 + Goal "a ~= (#0::int) ==> (a$+b) div a = b div a $+ #1";
   4.993 + by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1);
   4.994 + qed "zdiv_zadd_self1";
   4.995 +
   4.996 + Goal "a ~= (#0::int) ==> (b$+a) div a = b div a $+ #1";
   4.997 + by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1);
   4.998 + qed "zdiv_zadd_self2";
   4.999 + Addsimps [zdiv_zadd_self1, zdiv_zadd_self2];
  4.1000 +
  4.1001 + Goal "(a$+b) mod a = b mod a";
  4.1002 + by (zdiv_undefined_case_tac "a = #0" 1);
  4.1003 + by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
  4.1004 + qed "zmod_zadd_self1";
  4.1005 +
  4.1006 + Goal "(b$+a) mod a = b mod a";
  4.1007 + by (zdiv_undefined_case_tac "a = #0" 1);
  4.1008 + by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
  4.1009 + qed "zmod_zadd_self2";
  4.1010 + Addsimps [zmod_zadd_self1, zmod_zadd_self2];
  4.1011 +
  4.1012 +
  4.1013 + (*** proving  a div (b*c) = (a div b) div c ***)
  4.1014 +
  4.1015 + (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
  4.1016 +   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
  4.1017 +   to cause particular problems.*)
  4.1018 +
  4.1019 + (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
  4.1020 +
  4.1021 + Goal "[| (#0::int) $< c;  b $< r;  r $<= #0 |] ==> b$*c $< b$*(q mod c) $+ r";
  4.1022 + by (subgoal_tac "b $* (c $- q mod c) $< r $* #1" 1);
  4.1023 + by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1);
  4.1024 + by (rtac order_le_less_trans 1);
  4.1025 + by (etac zmult_zless_mono1 2);
  4.1026 + by (rtac zmult_zle_mono2_neg 1);
  4.1027 + by (auto_tac
  4.1028 +     (claset(),
  4.1029 +      simpset() addsimps zcompare_rls@
  4.1030 +			 [zadd_commute, add1_zle_eq, pos_mod_bound]));
  4.1031 + val lemma1 = result();
  4.1032 +
  4.1033 + Goal "[| (#0::int) $< c;   b $< r;  r $<= #0 |] ==> b $* (q mod c) $+ r $<= #0";
  4.1034 + by (subgoal_tac "b $* (q mod c) $<= #0" 1);
  4.1035 + by (arith_tac 1);
  4.1036 + by (asm_simp_tac (simpset() addsimps [zmult_le_0_iff, pos_mod_sign]) 1);
  4.1037 + val lemma2 = result();
  4.1038 +
  4.1039 + Goal "[| (#0::int) $< c;  #0 $<= r;  r $< b |] ==> #0 $<= b $* (q mod c) $+ r";
  4.1040 + by (subgoal_tac "#0 $<= b $* (q mod c)" 1);
  4.1041 + by (arith_tac 1);
  4.1042 + by (asm_simp_tac (simpset() addsimps [int_0_le_mult_iff, pos_mod_sign]) 1);
  4.1043 + val lemma3 = result();
  4.1044 +
  4.1045 + Goal "[| (#0::int) $< c; #0 $<= r; r $< b |] ==> b $* (q mod c) $+ r $< b $* c";
  4.1046 + by (subgoal_tac "r $* #1 $< b $* (c $- q mod c)" 1);
  4.1047 + by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1);
  4.1048 + by (rtac order_less_le_trans 1);
  4.1049 + by (etac zmult_zless_mono1 1);
  4.1050 + by (rtac zmult_zle_mono2 2);
  4.1051 + by (auto_tac
  4.1052 +     (claset(),
  4.1053 +      simpset() addsimps zcompare_rls@
  4.1054 +			 [zadd_commute, add1_zle_eq, pos_mod_bound]));
  4.1055 + val lemma4 = result();
  4.1056 +
  4.1057 + Goal "[| quorem (<a,b>, <q,r>);  b ~= #0;  #0 $< c |] \
  4.1058 + \     ==> quorem (<a,b$*c>, (q div c, b$*(q mod c) $+ r))";
  4.1059 + by (auto_tac  
  4.1060 +     (claset(),
  4.1061 +      simpset() addsimps zmult_ac@
  4.1062 +			 [zmod_zdiv_equality, quorem_def, neq_iff_zless,
  4.1063 +			  int_0_less_mult_iff,
  4.1064 +			  zadd_zmult_distrib2 RS sym,
  4.1065 +			  lemma1, lemma2, lemma3, lemma4]));
  4.1066 + val lemma = result();
  4.1067 +
  4.1068 + Goal "(#0::int) $< c ==> a div (b$*c) = (a div b) div c";
  4.1069 + by (zdiv_undefined_case_tac "b = #0" 1);
  4.1070 + by (force_tac (claset(),
  4.1071 +		simpset() addsimps [quorem_div_mod RS lemma RS quorem_div, 
  4.1072 +				    zmult_eq_0_iff]) 1);
  4.1073 + qed "zdiv_zmult2_eq";
  4.1074 +
  4.1075 + Goal "(#0::int) $< c ==> a mod (b$*c) = b$*(a div b mod c) $+ a mod b";
  4.1076 + by (zdiv_undefined_case_tac "b = #0" 1);
  4.1077 + by (force_tac (claset(),
  4.1078 +		simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod, 
  4.1079 +				    zmult_eq_0_iff]) 1);
  4.1080 + qed "zmod_zmult2_eq";
  4.1081 +
  4.1082 +
  4.1083 + (*** Cancellation of common factors in "div" ***)
  4.1084 +
  4.1085 + Goal "[| (#0::int) $< b;  c ~= #0 |] ==> (c$*a) div (c$*b) = a div b";
  4.1086 + by (stac zdiv_zmult2_eq 1);
  4.1087 + by Auto_tac;
  4.1088 + val lemma1 = result();
  4.1089 +
  4.1090 + Goal "[| b $< (#0::int);  c ~= #0 |] ==> (c$*a) div (c$*b) = a div b";
  4.1091 + by (subgoal_tac "(c $* (-a)) div (c $* (-b)) = (-a) div (-b)" 1);
  4.1092 + by (rtac lemma1 2);
  4.1093 + by Auto_tac;
  4.1094 + val lemma2 = result();
  4.1095 +
  4.1096 + Goal "c ~= (#0::int) ==> (c$*a) div (c$*b) = a div b";
  4.1097 + by (zdiv_undefined_case_tac "b = #0" 1);
  4.1098 + by (auto_tac
  4.1099 +     (claset(), 
  4.1100 +      simpset() addsimps [read_instantiate [("x", "b")] neq_iff_zless, 
  4.1101 +			  lemma1, lemma2]));
  4.1102 + qed "zdiv_zmult_zmult1";
  4.1103 +
  4.1104 + Goal "c ~= (#0::int) ==> (a$*c) div (b$*c) = a div b";
  4.1105 + by (dtac zdiv_zmult_zmult1 1);
  4.1106 + by (auto_tac (claset(), simpset() addsimps [zmult_commute]));
  4.1107 + qed "zdiv_zmult_zmult2";
  4.1108 +
  4.1109 +
  4.1110 +
  4.1111 + (*** Distribution of factors over "mod" ***)
  4.1112 +
  4.1113 + Goal "[| (#0::int) $< b;  c ~= #0 |] ==> (c$*a) mod (c$*b) = c $* (a mod b)";
  4.1114 + by (stac zmod_zmult2_eq 1);
  4.1115 + by Auto_tac;
  4.1116 + val lemma1 = result();
  4.1117 +
  4.1118 + Goal "[| b $< (#0::int);  c ~= #0 |] ==> (c$*a) mod (c$*b) = c $* (a mod b)";
  4.1119 + by (subgoal_tac "(c $* (-a)) mod (c $* (-b)) = c $* ((-a) mod (-b))" 1);
  4.1120 + by (rtac lemma1 2);
  4.1121 + by Auto_tac;
  4.1122 + val lemma2 = result();
  4.1123 +
  4.1124 + Goal "(c$*a) mod (c$*b) = c $* (a mod b)";
  4.1125 + by (zdiv_undefined_case_tac "b = #0" 1);
  4.1126 + by (zdiv_undefined_case_tac "c = #0" 1);
  4.1127 + by (auto_tac
  4.1128 +     (claset(), 
  4.1129 +      simpset() addsimps [read_instantiate [("x", "b")] neq_iff_zless, 
  4.1130 +			  lemma1, lemma2]));
  4.1131 + qed "zmod_zmult_zmult1";
  4.1132 +
  4.1133 + Goal "(a$*c) mod (b$*c) = (a mod b) $* c";
  4.1134 + by (cut_inst_tac [("c","c")] zmod_zmult_zmult1 1);
  4.1135 + by (auto_tac (claset(), simpset() addsimps [zmult_commute]));
  4.1136 + qed "zmod_zmult_zmult2";
  4.1137 +
  4.1138 +
  4.1139 + (*** Speeding up the division algorithm with shifting ***)
  4.1140 +
  4.1141 + (** computing "div" by shifting **)
  4.1142 +
  4.1143 + Goal "(#0::int) $<= a ==> (#1 $+ #2$*b) div (#2$*a) = b div a";
  4.1144 + by (zdiv_undefined_case_tac "a = #0" 1);
  4.1145 + by (subgoal_tac "#1 $<= a" 1);
  4.1146 +  by (arith_tac 2);
  4.1147 + by (subgoal_tac "#1 $< a $* #2" 1);
  4.1148 +  by (arith_tac 2);
  4.1149 + by (subgoal_tac "#2$*(#1 $+ b mod a) $<= #2$*a" 1);
  4.1150 +  by (rtac zmult_zle_mono2 2);
  4.1151 + by (auto_tac (claset(),
  4.1152 +	       simpset() addsimps [zadd_commute, zmult_commute, 
  4.1153 +				   add1_zle_eq, pos_mod_bound]));
  4.1154 + by (stac zdiv_zadd1_eq 1);
  4.1155 + by (asm_simp_tac (simpset() addsimps [zdiv_zmult_zmult2, zmod_zmult_zmult2, 
  4.1156 +				       div_pos_pos_trivial]) 1);
  4.1157 + by (stac div_pos_pos_trivial 1);
  4.1158 + by (asm_simp_tac (simpset() 
  4.1159 +	    addsimps [mod_pos_pos_trivial,
  4.1160 +		     pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
  4.1161 + by (auto_tac (claset(),
  4.1162 +	       simpset() addsimps [mod_pos_pos_trivial]));
  4.1163 + by (subgoal_tac "#0 $<= b mod a" 1);
  4.1164 +  by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
  4.1165 + by (arith_tac 1);
  4.1166 + qed "pos_zdiv_mult_2";
  4.1167 +
  4.1168 +
  4.1169 + Goal "a $<= (#0::int) ==> (#1 $+ #2$*b) div (#2$*a) = (b$+#1) div a";
  4.1170 + by (subgoal_tac "(#1 $+ #2$*(-b-#1)) div (#2 $* (-a)) = (-b-#1) div (-a)" 1);
  4.1171 + by (rtac pos_zdiv_mult_2 2);
  4.1172 + by (auto_tac (claset(),
  4.1173 +	       simpset() addsimps [zmult_zminus_right]));
  4.1174 + by (subgoal_tac "(#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))" 1);
  4.1175 + by (Simp_tac 2);
  4.1176 + by (asm_full_simp_tac (HOL_ss
  4.1177 +			addsimps [zdiv_zminus_zminus, zdiff_def,
  4.1178 +				  zminus_zadd_distrib RS sym]) 1);
  4.1179 + qed "neg_zdiv_mult_2";
  4.1180 +
  4.1181 +
  4.1182 + (*Not clear why this must be proved separately; probably number_of causes
  4.1183 +   simplification problems*)
  4.1184 + Goal "~ #0 $<= x ==> x $<= (#0::int)";
  4.1185 + by Auto_tac;
  4.1186 + val lemma = result();
  4.1187 +
  4.1188 + Goal "number_of (v BIT b) div number_of (w BIT False) = \
  4.1189 + \         (if ~b | (#0::int) $<= number_of w                   \
  4.1190 + \          then number_of v div (number_of w)    \
  4.1191 + \          else (number_of v $+ (#1::int)) div (number_of w))";
  4.1192 + by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
  4.1193 + by (asm_simp_tac (simpset()
  4.1194 +		   delsimps bin_arith_extra_simps@bin_rel_simps
  4.1195 +		   addsimps [zdiv_zmult_zmult1,
  4.1196 +			     pos_zdiv_mult_2, lemma, neg_zdiv_mult_2]) 1);
  4.1197 + qed "zdiv_number_of_BIT";
  4.1198 +
  4.1199 + Addsimps [zdiv_number_of_BIT];
  4.1200 +
  4.1201 +
  4.1202 + (** computing "mod" by shifting (proofs resemble those for "div") **)
  4.1203 +
  4.1204 + Goal "(#0::int) $<= a ==> (#1 $+ #2$*b) mod (#2$*a) = #1 $+ #2 $* (b mod a)";
  4.1205 + by (zdiv_undefined_case_tac "a = #0" 1);
  4.1206 + by (subgoal_tac "#1 $<= a" 1);
  4.1207 +  by (arith_tac 2);
  4.1208 + by (subgoal_tac "#1 $< a $* #2" 1);
  4.1209 +  by (arith_tac 2);
  4.1210 + by (subgoal_tac "#2$*(#1 $+ b mod a) $<= #2$*a" 1);
  4.1211 +  by (rtac zmult_zle_mono2 2);
  4.1212 + by (auto_tac (claset(),
  4.1213 +	       simpset() addsimps [zadd_commute, zmult_commute, 
  4.1214 +				   add1_zle_eq, pos_mod_bound]));
  4.1215 + by (stac zmod_zadd1_eq 1);
  4.1216 + by (asm_simp_tac (simpset() addsimps [zmod_zmult_zmult2, 
  4.1217 +				       mod_pos_pos_trivial]) 1);
  4.1218 + by (rtac mod_pos_pos_trivial 1);
  4.1219 + by (asm_simp_tac (simpset() 
  4.1220 +		   addsimps [mod_pos_pos_trivial,
  4.1221 +		     pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
  4.1222 + by (auto_tac (claset(),
  4.1223 +	       simpset() addsimps [mod_pos_pos_trivial]));
  4.1224 + by (subgoal_tac "#0 $<= b mod a" 1);
  4.1225 +  by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
  4.1226 + by (arith_tac 1);
  4.1227 + qed "pos_zmod_mult_2";
  4.1228 +
  4.1229 +
  4.1230 + Goal "a $<= (#0::int) ==> (#1 $+ #2$*b) mod (#2$*a) = #2 $* ((b$+#1) mod a) - #1";
  4.1231 + by (subgoal_tac 
  4.1232 +     "(#1 $+ #2$*(-b-#1)) mod (#2$*(-a)) = #1 $+ #2$*((-b-#1) mod (-a))" 1);
  4.1233 + by (rtac pos_zmod_mult_2 2);
  4.1234 + by (auto_tac (claset(),
  4.1235 +	       simpset() addsimps [zmult_zminus_right]));
  4.1236 + by (subgoal_tac "(#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))" 1);
  4.1237 + by (Simp_tac 2);
  4.1238 + by (asm_full_simp_tac (HOL_ss
  4.1239 +			addsimps [zmod_zminus_zminus, zdiff_def,
  4.1240 +				  zminus_zadd_distrib RS sym]) 1);
  4.1241 + by (dtac (zminus_equation RS iffD1 RS sym) 1);
  4.1242 + by Auto_tac;
  4.1243 + qed "neg_zmod_mult_2";
  4.1244 +
  4.1245 + Goal "number_of (v BIT b) mod number_of (w BIT False) = \
  4.1246 + \         (if b then \
  4.1247 + \               if (#0::int) $<= number_of w \
  4.1248 + \               then #2 $* (number_of v mod number_of w) $+ #1    \
  4.1249 + \               else #2 $* ((number_of v $+ (#1::int)) mod number_of w) - #1  \
  4.1250 + \          else #2 $* (number_of v mod number_of w))";
  4.1251 + by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
  4.1252 + by (asm_simp_tac (simpset()
  4.1253 +		   delsimps bin_arith_extra_simps@bin_rel_simps
  4.1254 +		   addsimps [zmod_zmult_zmult1,
  4.1255 +			     pos_zmod_mult_2, lemma, neg_zmod_mult_2]) 1);
  4.1256 + qed "zmod_number_of_BIT";
  4.1257 +
  4.1258 + Addsimps [zmod_number_of_BIT];
  4.1259 +
  4.1260 +
  4.1261 + (** Quotients of signs **)
  4.1262 +
  4.1263 + Goal "[| a $< (#0::int);  #0 $< b |] ==> a div b $< #0";
  4.1264 + by (subgoal_tac "a div b $<= #-1" 1);
  4.1265 + by (Force_tac 1);
  4.1266 + by (rtac order_trans 1);
  4.1267 + by (res_inst_tac [("a'","#-1")]  zdiv_mono1 1);
  4.1268 + by (auto_tac (claset(), simpset() addsimps [zdiv_minus1]));
  4.1269 + qed "div_neg_pos_less0";
  4.1270 +
  4.1271 + Goal "[| (#0::int) $<= a;  b $< #0 |] ==> a div b $<= #0";
  4.1272 + by (dtac zdiv_mono1_neg 1);
  4.1273 + by Auto_tac;
  4.1274 + qed "div_nonneg_neg_le0";
  4.1275 +
  4.1276 + Goal "(#0::int) $< b ==> (#0 $<= a div b) = (#0 $<= a)";
  4.1277 + by Auto_tac;
  4.1278 + by (dtac zdiv_mono1 2);
  4.1279 + by (auto_tac (claset(), simpset() addsimps [neq_iff_zless]));
  4.1280 + by (full_simp_tac (simpset() addsimps [not_zless_iff_zle RS sym]) 1);
  4.1281 + by (blast_tac (claset() addIs [div_neg_pos_less0]) 1);
  4.1282 + qed "pos_imp_zdiv_nonneg_iff";
  4.1283 +
  4.1284 + Goal "b $< (#0::int) ==> (#0 $<= a div b) = (a $<= (#0::int))";
  4.1285 + by (stac (zdiv_zminus_zminus RS sym) 1);
  4.1286 + by (stac pos_imp_zdiv_nonneg_iff 1);
  4.1287 + by Auto_tac;
  4.1288 + qed "neg_imp_zdiv_nonneg_iff";
  4.1289 +
  4.1290 + (*But not (a div b $<= 0 iff a$<=0); consider a=1, b=2 when a div b = 0.*)
  4.1291 + Goal "(#0::int) $< b ==> (a div b $< #0) = (a $< #0)";
  4.1292 + by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym,
  4.1293 +				       pos_imp_zdiv_nonneg_iff]) 1);
  4.1294 + qed "pos_imp_zdiv_neg_iff";
  4.1295 +
  4.1296 + (*Again the law fails for $<=: consider a = -1, b = -2 when a div b = 0*)
  4.1297 + Goal "b $< (#0::int) ==> (a div b $< #0) = (#0 $< a)";
  4.1298 + by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym,
  4.1299 +				       neg_imp_zdiv_nonneg_iff]) 1);
  4.1300 + qed "neg_imp_zdiv_neg_iff";
  4.1301 +*)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/ZF/Integ/IntDiv.thy	Fri Aug 11 13:27:17 2000 +0200
     5.3 @@ -0,0 +1,62 @@
     5.4 +(*  Title:      ZF/IntDiv.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 +    Copyright   1999  University of Cambridge
     5.8 +
     5.9 +The division operators div, mod
    5.10 +*)
    5.11 +
    5.12 +IntDiv = IntArith + 
    5.13 +
    5.14 +constdefs
    5.15 +  quorem :: "[i,i] => o"
    5.16 +    "quorem == %<a,b> <q,r>.
    5.17 +                      a = b$*q $+ r &
    5.18 +                      (#0$<b & #0$<=r & r$<b | ~(#0$<b) & b$<r & r $<= #0)"
    5.19 +
    5.20 +  adjust :: "[i,i,i] => i"
    5.21 +    "adjust(a,b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b>
    5.22 +                            else <#2$*q,r>"
    5.23 +
    5.24 +(**
    5.25 +(** the division algorithm **)
    5.26 +
    5.27 +(*for the case a>=0, b>0*)
    5.28 +consts posDivAlg :: "int*int => int*int"
    5.29 +recdef posDivAlg "inv_image less_than (%<a,b>. nat(a $- b $+ #1))"
    5.30 +    "posDivAlg <a,b> =
    5.31 +       (if (a$<b | b$<=#0) then <#0,a>
    5.32 +        else adjust a b (posDivAlg<a,#2$*b>))"
    5.33 +
    5.34 +(*for the case a<0, b>0*)
    5.35 +consts negDivAlg :: "int*int => int*int"
    5.36 +recdef negDivAlg "inv_image less_than (%<a,b>. nat(- a $- b))"
    5.37 +    "negDivAlg <a,b> =
    5.38 +       (if (#0$<=a$+b | b$<=#0) then <#-1,a$+b>
    5.39 +        else adjust a b (negDivAlg<a,#2$*b>))"
    5.40 +
    5.41 +(*for the general case b~=0*)
    5.42 +
    5.43 +constdefs
    5.44 +  negateSnd :: "int*int => int*int"
    5.45 +    "negateSnd == %<q,r>. <q,-r>"
    5.46 +
    5.47 +  (*The full division algorithm considers all possible signs for a, b
    5.48 +    including the special case a=0, b<0, because negDivAlg requires a<0*)
    5.49 +  divAlg :: "int*int => int*int"
    5.50 +    "divAlg ==
    5.51 +       %<a,b>. if #0$<=a then
    5.52 +                  if #0$<=b then posDivAlg <a,b>
    5.53 +                  else if a=#0 then <#0,#0>
    5.54 +                       else negateSnd (negDivAlg <-a,-b>)
    5.55 +               else 
    5.56 +                  if #0$<b then negDivAlg <a,b>
    5.57 +                  else         negateSnd (posDivAlg <-a,-b>)"
    5.58 +
    5.59 +defs
    5.60 +  div_def   "a div b == fst (divAlg <a,b>)"
    5.61 +  mod_def   "a mod b == snd (divAlg <a,b>)"
    5.62 +
    5.63 +**)
    5.64 +
    5.65 +end
     6.1 --- a/src/ZF/IsaMakefile	Fri Aug 11 13:26:40 2000 +0200
     6.2 +++ b/src/ZF/IsaMakefile	Fri Aug 11 13:27:17 2000 +0200
     6.3 @@ -31,10 +31,11 @@
     6.4    Cardinal.ML Cardinal.thy CardinalArith.ML CardinalArith.thy		\
     6.5    Cardinal_AC.ML Cardinal_AC.thy Datatype.ML Datatype.thy Epsilon.ML	\
     6.6    Epsilon.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy Inductive.ML	\
     6.7 -  Inductive.thy InfDatatype.ML InfDatatype.thy Integ/Bin.ML		\
     6.8 -  Integ/Bin.thy Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML	\
     6.9 -  Integ/Int.thy Integ/twos_compl.ML \
    6.10 -  Integ/int_arith.ML Integ/IntArith.thy \
    6.11 +  Inductive.thy InfDatatype.ML InfDatatype.thy \
    6.12 +  Integ/Bin.ML Integ/Bin.thy \
    6.13 +  Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML	Integ/Int.thy \
    6.14 +  Integ/IntDiv.ML Integ/IntDiv.thy \
    6.15 +  Integ/twos_compl.ML Integ/int_arith.ML Integ/IntArith.thy \
    6.16    Let.ML Let.thy List.ML List.thy	\
    6.17    Main.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML		\
    6.18    OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy	\
     7.1 --- a/src/ZF/Main.thy	Fri Aug 11 13:26:40 2000 +0200
     7.2 +++ b/src/ZF/Main.thy	Fri Aug 11 13:27:17 2000 +0200
     7.3 @@ -2,5 +2,5 @@
     7.4  (*$Id$
     7.5    theory Main includes everything*)
     7.6  
     7.7 -Main = Update + InfDatatype + List + EquivClass + IntArith
     7.8 +Main = Update + InfDatatype + List + EquivClass + IntDiv
     7.9