Moving div and mod from Arith to Divides
authorpaulson
Fri May 30 15:15:57 1997 +0200 (1997-05-30)
changeset 33662402c6ab1561
parent 3365 86c0d1988622
child 3367 832c245d967c
Moving div and mod from Arith to Divides
Moving dvd from ex/Primes to Divides
src/HOL/Arith.ML
src/HOL/Arith.thy
src/HOL/Divides.ML
src/HOL/Divides.thy
     1.1 --- a/src/HOL/Arith.ML	Fri May 30 15:14:59 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri May 30 15:15:57 1997 +0200
     1.3 @@ -388,6 +388,13 @@
     1.4  qed "diff_add_inverse2";
     1.5  Addsimps [diff_add_inverse2];
     1.6  
     1.7 +goal Arith.thy "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)";
     1.8 +by (Step_tac 1);
     1.9 +by (ALLGOALS 
    1.10 +    (asm_simp_tac
    1.11 +     (!simpset addsimps [add_diff_inverse, not_less_iff_le, add_commute])));
    1.12 +qed "le_imp_diff_is_add";
    1.13 +
    1.14  val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0";
    1.15  by (rtac (prem RS rev_mp) 1);
    1.16  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.17 @@ -470,154 +477,6 @@
    1.18  (*NOT added as rewrites, since sometimes they are used from right-to-left*)
    1.19  
    1.20  
    1.21 -(** Less-then properties **)
    1.22 -
    1.23 -(*In ordinary notation: if 0<n and n<=m then m-n < m *)
    1.24 -goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
    1.25 -by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
    1.26 -by (Blast_tac 1);
    1.27 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.28 -by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc])));
    1.29 -qed "diff_less";
    1.30 -
    1.31 -val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
    1.32 -                    def_wfrec RS trans;
    1.33 -
    1.34 -goalw Nat.thy [less_def] "(m,n) : pred_nat^+ = (m<n)";
    1.35 -by (rtac refl 1);
    1.36 -qed "less_eq";
    1.37 -
    1.38 -(*** Remainder ***)
    1.39 -
    1.40 -goal Arith.thy "(%m. m mod n) = wfrec (trancl pred_nat) \
    1.41 -             \                      (%f j. if j<n then j else f (j-n))";
    1.42 -by (simp_tac (!simpset addsimps [mod_def]) 1);
    1.43 -qed "mod_eq";
    1.44 -
    1.45 -goal Arith.thy "!!m. m<n ==> m mod n = m";
    1.46 -by (rtac (mod_eq RS wf_less_trans) 1);
    1.47 -by (Asm_simp_tac 1);
    1.48 -qed "mod_less";
    1.49 -
    1.50 -goal Arith.thy "!!m. [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
    1.51 -by (rtac (mod_eq RS wf_less_trans) 1);
    1.52 -by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
    1.53 -qed "mod_geq";
    1.54 -
    1.55 -goal thy "!!n. 0<n ==> n mod n = 0";
    1.56 -by (rtac (mod_eq RS wf_less_trans) 1);
    1.57 -by (asm_simp_tac (!simpset addsimps [mod_less, diff_self_eq_0,
    1.58 -				     cut_def, less_eq]) 1);
    1.59 -qed "mod_nn_is_0";
    1.60 -
    1.61 -goal thy "!!n. 0<n ==> (m+n) mod n = m mod n";
    1.62 -by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
    1.63 -by (stac (mod_geq RS sym) 2);
    1.64 -by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [add_commute])));
    1.65 -qed "mod_eq_add";
    1.66 -
    1.67 -goal thy "!!n. 0<n ==> m*n mod n = 0";
    1.68 -by (induct_tac "m" 1);
    1.69 -by (asm_simp_tac (!simpset addsimps [mod_less]) 1);
    1.70 -by (dres_inst_tac [("m","m*n")] mod_eq_add 1);
    1.71 -by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
    1.72 -qed "mod_prod_nn_is_0";
    1.73 -
    1.74 -
    1.75 -(*** Quotient ***)
    1.76 -
    1.77 -goal Arith.thy "(%m. m div n) = wfrec (trancl pred_nat) \
    1.78 -                        \            (%f j. if j<n then 0 else Suc (f (j-n)))";
    1.79 -by (simp_tac (!simpset addsimps [div_def]) 1);
    1.80 -qed "div_eq";
    1.81 -
    1.82 -goal Arith.thy "!!m. m<n ==> m div n = 0";
    1.83 -by (rtac (div_eq RS wf_less_trans) 1);
    1.84 -by (Asm_simp_tac 1);
    1.85 -qed "div_less";
    1.86 -
    1.87 -goal Arith.thy "!!M. [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
    1.88 -by (rtac (div_eq RS wf_less_trans) 1);
    1.89 -by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
    1.90 -qed "div_geq";
    1.91 -
    1.92 -(*Main Result about quotient and remainder.*)
    1.93 -goal Arith.thy "!!m. 0<n ==> (m div n)*n + m mod n = m";
    1.94 -by (res_inst_tac [("n","m")] less_induct 1);
    1.95 -by (rename_tac "k" 1);    (*Variable name used in line below*)
    1.96 -by (case_tac "k<n" 1);
    1.97 -by (ALLGOALS (asm_simp_tac(!simpset addsimps ([add_assoc] @
    1.98 -                       [mod_less, mod_geq, div_less, div_geq,
    1.99 -                        add_diff_inverse, diff_less]))));
   1.100 -qed "mod_div_equality";
   1.101 -
   1.102 -
   1.103 -(*** Further facts about mod (mainly for the mutilated chess board ***)
   1.104 -
   1.105 -goal Arith.thy
   1.106 -    "!!m n. 0<n ==> \
   1.107 -\           Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
   1.108 -by (res_inst_tac [("n","m")] less_induct 1);
   1.109 -by (excluded_middle_tac "Suc(na)<n" 1);
   1.110 -(* case Suc(na) < n *)
   1.111 -by (forward_tac [lessI RS less_trans] 2);
   1.112 -by (asm_simp_tac (!simpset addsimps [mod_less, less_not_refl2 RS not_sym]) 2);
   1.113 -(* case n <= Suc(na) *)
   1.114 -by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, mod_geq]) 1);
   1.115 -by (etac (le_imp_less_or_eq RS disjE) 1);
   1.116 -by (asm_simp_tac (!simpset addsimps [Suc_diff_n]) 1);
   1.117 -by (asm_full_simp_tac (!simpset addsimps [not_less_eq RS sym, 
   1.118 -                                          diff_less, mod_geq]) 1);
   1.119 -by (asm_simp_tac (!simpset addsimps [mod_less]) 1);
   1.120 -qed "mod_Suc";
   1.121 -
   1.122 -goal Arith.thy "!!m n. 0<n ==> m mod n < n";
   1.123 -by (res_inst_tac [("n","m")] less_induct 1);
   1.124 -by (excluded_middle_tac "na<n" 1);
   1.125 -(*case na<n*)
   1.126 -by (asm_simp_tac (!simpset addsimps [mod_less]) 2);
   1.127 -(*case n le na*)
   1.128 -by (asm_full_simp_tac (!simpset addsimps [mod_geq, diff_less]) 1);
   1.129 -qed "mod_less_divisor";
   1.130 -
   1.131 -
   1.132 -(** Evens and Odds **)
   1.133 -
   1.134 -(*With less_zeroE, causes case analysis on b<2*)
   1.135 -AddSEs [less_SucE];
   1.136 -
   1.137 -goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
   1.138 -by (subgoal_tac "k mod 2 < 2" 1);
   1.139 -by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
   1.140 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   1.141 -by (Blast_tac 1);
   1.142 -qed "mod2_cases";
   1.143 -
   1.144 -goal thy "Suc(Suc(m)) mod 2 = m mod 2";
   1.145 -by (subgoal_tac "m mod 2 < 2" 1);
   1.146 -by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
   1.147 -by (Step_tac 1);
   1.148 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_Suc])));
   1.149 -qed "mod2_Suc_Suc";
   1.150 -Addsimps [mod2_Suc_Suc];
   1.151 -
   1.152 -goal Arith.thy "!!m. m mod 2 ~= 0 ==> m mod 2 = 1";
   1.153 -by (subgoal_tac "m mod 2 < 2" 1);
   1.154 -by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
   1.155 -by (safe_tac (!claset addSEs [lessE]));
   1.156 -by (ALLGOALS (blast_tac (!claset addIs [sym])));
   1.157 -qed "mod2_neq_0";
   1.158 -
   1.159 -goal thy "(m+m) mod 2 = 0";
   1.160 -by (induct_tac "m" 1);
   1.161 -by (simp_tac (!simpset addsimps [mod_less]) 1);
   1.162 -by (asm_simp_tac (!simpset addsimps [mod2_Suc_Suc, add_Suc_right]) 1);
   1.163 -qed "mod2_add_self";
   1.164 -Addsimps [mod2_add_self];
   1.165 -
   1.166 -Delrules [less_SucE];
   1.167 -
   1.168 -
   1.169  (*** Monotonicity of Multiplication ***)
   1.170  
   1.171  goal Arith.thy "!!i::nat. i<=j ==> i*k<=j*k";
   1.172 @@ -688,44 +547,6 @@
   1.173  Addsimps [mult_cancel1, mult_cancel2];
   1.174  
   1.175  
   1.176 -(*** More division laws ***)
   1.177 -
   1.178 -goal thy "!!n. 0<n ==> m*n div n = m";
   1.179 -by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
   1.180 -ba 1;
   1.181 -by (asm_full_simp_tac (!simpset addsimps [mod_prod_nn_is_0]) 1);
   1.182 -qed "div_prod_nn_is_m";
   1.183 -Addsimps [div_prod_nn_is_m];
   1.184 -
   1.185 -(*Cancellation law for division*)
   1.186 -goal Arith.thy "!!k. [| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
   1.187 -by (res_inst_tac [("n","m")] less_induct 1);
   1.188 -by (case_tac "na<n" 1);
   1.189 -by (asm_simp_tac (!simpset addsimps [div_less, zero_less_mult_iff, 
   1.190 -                                     mult_less_mono2]) 1);
   1.191 -by (subgoal_tac "~ k*na < k*n" 1);
   1.192 -by (asm_simp_tac
   1.193 -     (!simpset addsimps [zero_less_mult_iff, div_geq,
   1.194 -                         diff_mult_distrib2 RS sym, diff_less]) 1);
   1.195 -by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, 
   1.196 -                                          le_refl RS mult_le_mono]) 1);
   1.197 -qed "div_cancel";
   1.198 -Addsimps [div_cancel];
   1.199 -
   1.200 -goal Arith.thy "!!k. [| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
   1.201 -by (res_inst_tac [("n","m")] less_induct 1);
   1.202 -by (case_tac "na<n" 1);
   1.203 -by (asm_simp_tac (!simpset addsimps [mod_less, zero_less_mult_iff, 
   1.204 -                                     mult_less_mono2]) 1);
   1.205 -by (subgoal_tac "~ k*na < k*n" 1);
   1.206 -by (asm_simp_tac
   1.207 -     (!simpset addsimps [zero_less_mult_iff, mod_geq,
   1.208 -                         diff_mult_distrib2 RS sym, diff_less]) 1);
   1.209 -by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, 
   1.210 -                                          le_refl RS mult_le_mono]) 1);
   1.211 -qed "mult_mod_distrib";
   1.212 -
   1.213 -
   1.214  (** Lemma for gcd **)
   1.215  
   1.216  goal Arith.thy "!!m n. m = m*n ==> n=1 | m=0";
     2.1 --- a/src/HOL/Arith.thy	Fri May 30 15:14:59 1997 +0200
     2.2 +++ b/src/HOL/Arith.thy	Fri May 30 15:15:57 1997 +0200
     2.3 @@ -3,38 +3,32 @@
     2.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.5      Copyright   1993  University of Cambridge
     2.6  
     2.7 -Arithmetic operators and their definitions
     2.8 +Arithmetic operators + - and * (for div, mod and dvd, see Divides)
     2.9  *)
    2.10  
    2.11  Arith = Nat +
    2.12  
    2.13  instance
    2.14 -  nat :: {plus, minus, times}
    2.15 +  nat :: {plus, minus, times, power}
    2.16  
    2.17  consts
    2.18    pred      :: nat => nat
    2.19 -  div, mod  :: [nat, nat] => nat  (infixl 70)
    2.20    (* size of a datatype value; overloaded *)
    2.21    size      :: 'a => nat
    2.22  
    2.23  defs
    2.24    pred_def  "pred(m) == case m of 0 => 0 | Suc n => n"
    2.25  
    2.26 -  mod_def   "m mod n == wfrec (trancl pred_nat)
    2.27 -                          (%f j. if j<n then j else f (j-n)) m"
    2.28 -  div_def   "m div n == wfrec (trancl pred_nat) 
    2.29 -                          (%f j. if j<n then 0 else Suc (f (j-n))) m"
    2.30 -
    2.31  primrec "op +" nat 
    2.32 -  "0 + n = n"
    2.33 -  "Suc m + n = Suc(m + n)"
    2.34 +  add_0    "0 + n = n"
    2.35 +  add_Suc  "Suc m + n = Suc(m + n)"
    2.36  
    2.37  primrec "op -" nat 
    2.38    diff_0   "m - 0 = m"
    2.39    diff_Suc "m - Suc n = pred(m - n)"
    2.40  
    2.41  primrec "op *"  nat 
    2.42 -  "0 * n = 0"
    2.43 -  "Suc m * n = n + (m * n)"
    2.44 +  mult_0   "0 * n = 0"
    2.45 +  mult_Suc "Suc m * n = n + (m * n)"
    2.46  
    2.47  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Divides.ML	Fri May 30 15:15:57 1997 +0200
     3.3 @@ -0,0 +1,333 @@
     3.4 +(*  Title:      HOL/Divides.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 division operators div, mod and the divides relation "dvd"
    3.10 +*)
    3.11 +
    3.12 +
    3.13 +(** Less-then properties **)
    3.14 +
    3.15 +(*In ordinary notation: if 0<n and n<=m then m-n < m *)
    3.16 +goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
    3.17 +by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
    3.18 +by (Blast_tac 1);
    3.19 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    3.20 +by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc])));
    3.21 +qed "diff_less";
    3.22 +
    3.23 +val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
    3.24 +                    def_wfrec RS trans;
    3.25 +
    3.26 +(*** Remainder ***)
    3.27 +
    3.28 +goal thy "(%m. m mod n) = wfrec (trancl pred_nat) \
    3.29 +             \                      (%f j. if j<n then j else f (j-n))";
    3.30 +by (simp_tac (!simpset addsimps [mod_def]) 1);
    3.31 +qed "mod_eq";
    3.32 +
    3.33 +goal thy "!!m. m<n ==> m mod n = m";
    3.34 +by (rtac (mod_eq RS wf_less_trans) 1);
    3.35 +by (Asm_simp_tac 1);
    3.36 +qed "mod_less";
    3.37 +
    3.38 +goal thy "!!m. [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
    3.39 +by (rtac (mod_eq RS wf_less_trans) 1);
    3.40 +by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
    3.41 +qed "mod_geq";
    3.42 +
    3.43 +goal thy "m mod 1 = 0";
    3.44 +by (induct_tac "m" 1);
    3.45 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_less, mod_geq])));
    3.46 +qed "mod_1";
    3.47 +Addsimps [mod_1];
    3.48 +
    3.49 +goal thy "!!n. 0<n ==> n mod n = 0";
    3.50 +by (asm_simp_tac (!simpset addsimps [mod_less, mod_geq]) 1);
    3.51 +qed "mod_self";
    3.52 +
    3.53 +goal thy "!!n. 0<n ==> (m+n) mod n = m mod n";
    3.54 +by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
    3.55 +by (stac (mod_geq RS sym) 2);
    3.56 +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [add_commute])));
    3.57 +qed "mod_eq_add";
    3.58 +
    3.59 +goal thy "!!k. [| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)";
    3.60 +by (res_inst_tac [("n","m")] less_induct 1);
    3.61 +by (case_tac "na<n" 1);
    3.62 +(*case na<n*)
    3.63 +by (asm_simp_tac (!simpset addsimps [mod_less]) 1);
    3.64 +(*case n<=na*)
    3.65 +by (asm_simp_tac (!simpset addsimps [mod_geq, diff_less, zero_less_mult_iff, 
    3.66 +				     diff_mult_distrib]) 1);
    3.67 +qed "mod_mult_distrib";
    3.68 +
    3.69 +goal thy "!!k. [| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)";
    3.70 +by (res_inst_tac [("n","m")] less_induct 1);
    3.71 +by (case_tac "na<n" 1);
    3.72 +(*case na<n*)
    3.73 +by (asm_simp_tac (!simpset addsimps [mod_less]) 1);
    3.74 +(*case n<=na*)
    3.75 +by (asm_simp_tac (!simpset addsimps [mod_geq, diff_less, zero_less_mult_iff, 
    3.76 +				     diff_mult_distrib2]) 1);
    3.77 +qed "mod_mult_distrib2";
    3.78 +
    3.79 +goal thy "!!n. 0<n ==> m*n mod n = 0";
    3.80 +by (induct_tac "m" 1);
    3.81 +by (asm_simp_tac (!simpset addsimps [mod_less]) 1);
    3.82 +by (dres_inst_tac [("m","m*n")] mod_eq_add 1);
    3.83 +by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
    3.84 +qed "mod_mult_self_is_0";
    3.85 +Addsimps [mod_mult_self_is_0];
    3.86 +
    3.87 +(*** Quotient ***)
    3.88 +
    3.89 +goal thy "(%m. m div n) = wfrec (trancl pred_nat) \
    3.90 +                        \            (%f j. if j<n then 0 else Suc (f (j-n)))";
    3.91 +by (simp_tac (!simpset addsimps [div_def]) 1);
    3.92 +qed "div_eq";
    3.93 +
    3.94 +goal thy "!!m. m<n ==> m div n = 0";
    3.95 +by (rtac (div_eq RS wf_less_trans) 1);
    3.96 +by (Asm_simp_tac 1);
    3.97 +qed "div_less";
    3.98 +
    3.99 +goal thy "!!M. [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
   3.100 +by (rtac (div_eq RS wf_less_trans) 1);
   3.101 +by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
   3.102 +qed "div_geq";
   3.103 +
   3.104 +(*Main Result about quotient and remainder.*)
   3.105 +goal thy "!!m. 0<n ==> (m div n)*n + m mod n = m";
   3.106 +by (res_inst_tac [("n","m")] less_induct 1);
   3.107 +by (rename_tac "k" 1);    (*Variable name used in line below*)
   3.108 +by (case_tac "k<n" 1);
   3.109 +by (ALLGOALS (asm_simp_tac(!simpset addsimps ([add_assoc] @
   3.110 +                       [mod_less, mod_geq, div_less, div_geq,
   3.111 +                        add_diff_inverse, diff_less]))));
   3.112 +qed "mod_div_equality";
   3.113 +
   3.114 +goal thy "m div 1 = m";
   3.115 +by (induct_tac "m" 1);
   3.116 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [div_less, div_geq])));
   3.117 +qed "div_1";
   3.118 +Addsimps [div_1];
   3.119 +
   3.120 +goal thy "!!n. 0<n ==> n div n = 1";
   3.121 +by (asm_simp_tac (!simpset addsimps [div_less, div_geq]) 1);
   3.122 +qed "div_self";
   3.123 +
   3.124 +
   3.125 +(*** Further facts about mod (mainly for the mutilated chess board ***)
   3.126 +
   3.127 +goal thy
   3.128 +    "!!m n. 0<n ==> \
   3.129 +\           Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
   3.130 +by (res_inst_tac [("n","m")] less_induct 1);
   3.131 +by (excluded_middle_tac "Suc(na)<n" 1);
   3.132 +(* case Suc(na) < n *)
   3.133 +by (forward_tac [lessI RS less_trans] 2);
   3.134 +by (asm_simp_tac (!simpset addsimps [mod_less, less_not_refl2 RS not_sym]) 2);
   3.135 +(* case n <= Suc(na) *)
   3.136 +by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, mod_geq]) 1);
   3.137 +by (etac (le_imp_less_or_eq RS disjE) 1);
   3.138 +by (asm_simp_tac (!simpset addsimps [Suc_diff_n]) 1);
   3.139 +by (asm_full_simp_tac (!simpset addsimps [not_less_eq RS sym, 
   3.140 +                                          diff_less, mod_geq]) 1);
   3.141 +by (asm_simp_tac (!simpset addsimps [mod_less]) 1);
   3.142 +qed "mod_Suc";
   3.143 +
   3.144 +goal thy "!!m n. 0<n ==> m mod n < n";
   3.145 +by (res_inst_tac [("n","m")] less_induct 1);
   3.146 +by (excluded_middle_tac "na<n" 1);
   3.147 +(*case na<n*)
   3.148 +by (asm_simp_tac (!simpset addsimps [mod_less]) 2);
   3.149 +(*case n le na*)
   3.150 +by (asm_full_simp_tac (!simpset addsimps [mod_geq, diff_less]) 1);
   3.151 +qed "mod_less_divisor";
   3.152 +
   3.153 +
   3.154 +(** Evens and Odds **)
   3.155 +
   3.156 +(*With less_zeroE, causes case analysis on b<2*)
   3.157 +AddSEs [less_SucE];
   3.158 +
   3.159 +goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
   3.160 +by (subgoal_tac "k mod 2 < 2" 1);
   3.161 +by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
   3.162 +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   3.163 +by (Blast_tac 1);
   3.164 +qed "mod2_cases";
   3.165 +
   3.166 +goal thy "Suc(Suc(m)) mod 2 = m mod 2";
   3.167 +by (subgoal_tac "m mod 2 < 2" 1);
   3.168 +by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
   3.169 +by (Step_tac 1);
   3.170 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_Suc])));
   3.171 +qed "mod2_Suc_Suc";
   3.172 +Addsimps [mod2_Suc_Suc];
   3.173 +
   3.174 +goal thy "!!m. m mod 2 ~= 0 ==> m mod 2 = 1";
   3.175 +by (subgoal_tac "m mod 2 < 2" 1);
   3.176 +by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
   3.177 +by (safe_tac (!claset addSEs [lessE]));
   3.178 +by (ALLGOALS (blast_tac (!claset addIs [sym])));
   3.179 +qed "mod2_neq_0";
   3.180 +
   3.181 +goal thy "(m+m) mod 2 = 0";
   3.182 +by (induct_tac "m" 1);
   3.183 +by (simp_tac (!simpset addsimps [mod_less]) 1);
   3.184 +by (asm_simp_tac (!simpset addsimps [mod2_Suc_Suc, add_Suc_right]) 1);
   3.185 +qed "mod2_add_self";
   3.186 +Addsimps [mod2_add_self];
   3.187 +
   3.188 +Delrules [less_SucE];
   3.189 +
   3.190 +
   3.191 +(*** More division laws ***)
   3.192 +
   3.193 +goal thy "!!n. 0<n ==> m*n div n = m";
   3.194 +by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
   3.195 +ba 1;
   3.196 +by (asm_full_simp_tac (!simpset addsimps [mod_mult_self_is_0]) 1);
   3.197 +qed "div_mult_self_is_m";
   3.198 +Addsimps [div_mult_self_is_m];
   3.199 +
   3.200 +(*Cancellation law for division*)
   3.201 +goal thy "!!k. [| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
   3.202 +by (res_inst_tac [("n","m")] less_induct 1);
   3.203 +by (case_tac "na<n" 1);
   3.204 +by (asm_simp_tac (!simpset addsimps [div_less, zero_less_mult_iff, 
   3.205 +                                     mult_less_mono2]) 1);
   3.206 +by (subgoal_tac "~ k*na < k*n" 1);
   3.207 +by (asm_simp_tac
   3.208 +     (!simpset addsimps [zero_less_mult_iff, div_geq,
   3.209 +                         diff_mult_distrib2 RS sym, diff_less]) 1);
   3.210 +by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, 
   3.211 +                                          le_refl RS mult_le_mono]) 1);
   3.212 +qed "div_cancel";
   3.213 +Addsimps [div_cancel];
   3.214 +
   3.215 +goal thy "!!k. [| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
   3.216 +by (res_inst_tac [("n","m")] less_induct 1);
   3.217 +by (case_tac "na<n" 1);
   3.218 +by (asm_simp_tac (!simpset addsimps [mod_less, zero_less_mult_iff, 
   3.219 +                                     mult_less_mono2]) 1);
   3.220 +by (subgoal_tac "~ k*na < k*n" 1);
   3.221 +by (asm_simp_tac
   3.222 +     (!simpset addsimps [zero_less_mult_iff, mod_geq,
   3.223 +                         diff_mult_distrib2 RS sym, diff_less]) 1);
   3.224 +by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, 
   3.225 +                                          le_refl RS mult_le_mono]) 1);
   3.226 +qed "mult_mod_distrib";
   3.227 +
   3.228 +
   3.229 +(************************************************)
   3.230 +(** Divides Relation                           **)
   3.231 +(************************************************)
   3.232 +
   3.233 +goalw thy [dvd_def] "m dvd 0";
   3.234 +by (fast_tac (!claset addIs [mult_0_right RS sym]) 1);
   3.235 +qed "dvd_0_right";
   3.236 +Addsimps [dvd_0_right];
   3.237 +
   3.238 +goalw thy [dvd_def] "!!m. 0 dvd m ==> m = 0";
   3.239 +by (fast_tac (!claset addss !simpset) 1);
   3.240 +qed "dvd_0_left";
   3.241 +
   3.242 +goalw thy [dvd_def] "1 dvd k";
   3.243 +by (Simp_tac 1);
   3.244 +qed "dvd_1_left";
   3.245 +AddIffs [dvd_1_left];
   3.246 +
   3.247 +goalw thy [dvd_def] "m dvd m";
   3.248 +by (fast_tac (!claset addIs [mult_1_right RS sym]) 1);
   3.249 +qed "dvd_refl";
   3.250 +Addsimps [dvd_refl];
   3.251 +
   3.252 +goalw thy [dvd_def] "!!m n p. [| m dvd n; n dvd p |] ==> m dvd p";
   3.253 +by (fast_tac (!claset addIs [mult_assoc] ) 1);
   3.254 +qed "dvd_trans";
   3.255 +
   3.256 +goalw thy [dvd_def] "!!m n. [| m dvd n; n dvd m |] ==> m=n";
   3.257 +by (fast_tac (!claset addDs [mult_eq_self_implies_10]
   3.258 +                     addss (!simpset addsimps [mult_assoc, mult_eq_1_iff])) 1);
   3.259 +qed "dvd_anti_sym";
   3.260 +
   3.261 +goalw thy [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m + n)";
   3.262 +by (blast_tac (!claset addIs [add_mult_distrib2 RS sym]) 1);
   3.263 +qed "dvd_add";
   3.264 +
   3.265 +goalw thy [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m-n)";
   3.266 +by (blast_tac (!claset addIs [diff_mult_distrib2 RS sym]) 1);
   3.267 +qed "dvd_diff";
   3.268 +
   3.269 +goal thy "!!k. [| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
   3.270 +be (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1;
   3.271 +by (blast_tac (!claset addIs [dvd_add]) 1);
   3.272 +qed "dvd_diffD";
   3.273 +
   3.274 +goalw thy [dvd_def] "!!k. k dvd n ==> k dvd (m*n)";
   3.275 +by (blast_tac (!claset addIs [mult_left_commute]) 1);
   3.276 +qed "dvd_mult";
   3.277 +
   3.278 +goal thy "!!k. k dvd m ==> k dvd (m*n)";
   3.279 +by (stac mult_commute 1);
   3.280 +by (etac dvd_mult 1);
   3.281 +qed "dvd_mult2";
   3.282 +
   3.283 +(* k dvd (m*k) *)
   3.284 +AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
   3.285 +
   3.286 +goalw thy [dvd_def] "!!m. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
   3.287 +by (Step_tac 1);
   3.288 +by (full_simp_tac (!simpset addsimps [zero_less_mult_iff]) 1);
   3.289 +by (res_inst_tac 
   3.290 +    [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] 
   3.291 +    exI 1);
   3.292 +by (asm_simp_tac (!simpset addsimps [diff_mult_distrib2, 
   3.293 +                                     mult_mod_distrib, add_mult_distrib2]) 1);
   3.294 +qed "dvd_mod";
   3.295 +
   3.296 +goal thy "!!k. [| k dvd (m mod n); k dvd n; n~=0 |] ==> k dvd m";
   3.297 +by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
   3.298 +by (asm_simp_tac (!simpset addsimps [dvd_add, dvd_mult]) 2);
   3.299 +by (asm_full_simp_tac (!simpset addsimps [mod_div_equality, zero_less_eq]) 1);
   3.300 +qed "dvd_mod_imp_dvd";
   3.301 +
   3.302 +goalw thy [dvd_def]  "!!k m n. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
   3.303 +by (etac exE 1);
   3.304 +by (asm_full_simp_tac (!simpset addsimps mult_ac) 1);
   3.305 +by (Blast_tac 1);
   3.306 +qed "dvd_mult_cancel";
   3.307 +
   3.308 +goalw thy [dvd_def] "!!i j. [| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
   3.309 +by (Step_tac 1);
   3.310 +by (res_inst_tac [("x","k*ka")] exI 1);
   3.311 +by (asm_simp_tac (!simpset addsimps mult_ac) 1);
   3.312 +qed "mult_dvd_mono";
   3.313 +
   3.314 +goalw thy [dvd_def] "!!c. (i*j) dvd k ==> i dvd k";
   3.315 +by (full_simp_tac (!simpset addsimps [mult_assoc]) 1);
   3.316 +by (Blast_tac 1);
   3.317 +qed "dvd_mult_left";
   3.318 +
   3.319 +goalw thy [dvd_def] "!!n. [| k dvd n; 0 < n |] ==> k <= n";
   3.320 +by (Step_tac 1);
   3.321 +by (ALLGOALS (full_simp_tac (!simpset addsimps [zero_less_mult_iff])));
   3.322 +be conjE 1;
   3.323 +br le_trans 1;
   3.324 +br (le_refl RS mult_le_mono) 2;
   3.325 +by (etac Suc_leI 2);
   3.326 +by (Simp_tac 1);
   3.327 +qed "dvd_imp_le";
   3.328 +
   3.329 +goalw thy [dvd_def] "!!k. 0<k ==> (k dvd n) = (n mod k = 0)";
   3.330 +by (Step_tac 1);
   3.331 +by (stac mult_commute 1);
   3.332 +by (Asm_simp_tac 1);
   3.333 +by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
   3.334 +by (asm_simp_tac (!simpset addsimps [mult_commute]) 1);
   3.335 +by (Blast_tac 1);
   3.336 +qed "dvd_eq_mod_eq_0";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Divides.thy	Fri May 30 15:15:57 1997 +0200
     4.3 @@ -0,0 +1,24 @@
     4.4 +(*  Title:      HOL/Divides.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1993  University of Cambridge
     4.8 +
     4.9 +The division operators div, mod and the divides relation "dvd"
    4.10 +*)
    4.11 +
    4.12 +Divides = Arith +
    4.13 +
    4.14 +consts
    4.15 +  div, mod  :: [nat, nat] => nat          (infixl 70)
    4.16 +  dvd     :: [nat,nat]=>bool              (infixl 70) 
    4.17 +
    4.18 +
    4.19 +defs
    4.20 +  mod_def   "m mod n == wfrec (trancl pred_nat)
    4.21 +                          (%f j. if j<n then j else f (j-n)) m"
    4.22 +  div_def   "m div n == wfrec (trancl pred_nat) 
    4.23 +                          (%f j. if j<n then 0 else Suc (f (j-n))) m"
    4.24 +
    4.25 +  dvd_def   "m dvd n == EX k. n = m*k"
    4.26 +
    4.27 +end