many new div and mod properties (borrowed from Integ/IntDiv)
authorpaulson
Fri Dec 01 11:03:31 2000 +0100 (2000-12-01)
changeset 10559d3fd54fc659b
parent 10558 09a91221ced1
child 10560 f4da791d4850
many new div and mod properties (borrowed from Integ/IntDiv)
src/HOL/Divides.ML
src/HOL/Divides.thy
     1.1 --- a/src/HOL/Divides.ML	Fri Dec 01 11:02:55 2000 +0100
     1.2 +++ b/src/HOL/Divides.ML	Fri Dec 01 11:03:31 2000 +0100
     1.3 @@ -75,6 +75,7 @@
     1.4  by (div_undefined_case_tac "n=0" 1);
     1.5  by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
     1.6  qed "mod_self";
     1.7 +Addsimps [mod_self];
     1.8  
     1.9  Goal "(m+n) mod n = m mod (n::nat)";
    1.10  by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
    1.11 @@ -172,6 +173,208 @@
    1.12  by (arith_tac 1);
    1.13  qed "mult_div_cancel";
    1.14  
    1.15 +Goal "0<n ==> m mod n < (n::nat)";
    1.16 +by (induct_thm_tac nat_less_induct "m" 1);
    1.17 +by (case_tac "na<n" 1);
    1.18 +(*case n le na*)
    1.19 +by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
    1.20 +(*case na<n*)
    1.21 +by (Asm_simp_tac 1);
    1.22 +qed "mod_less_divisor";
    1.23 +Addsimps [mod_less_divisor];
    1.24 +
    1.25 +(*** More division laws ***)
    1.26 +
    1.27 +Goal "0<n ==> (m*n) div n = (m::nat)";
    1.28 +by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1);
    1.29 +by Auto_tac;
    1.30 +qed "div_mult_self_is_m";
    1.31 +
    1.32 +Goal "0<n ==> (n*m) div n = (m::nat)";
    1.33 +by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1);
    1.34 +qed "div_mult_self1_is_m";
    1.35 +Addsimps [div_mult_self_is_m, div_mult_self1_is_m];
    1.36 +
    1.37 +(*mod_mult_distrib2 above is the counterpart for remainder*)
    1.38 +
    1.39 +
    1.40 +(*** Proving facts about div and mod using quorem ***)
    1.41 +
    1.42 +Goal "[| b*q' + r'  <= b*q + r;  0 < b;  r < b |] \
    1.43 +\     ==> q' <= (q::nat)";
    1.44 +by (rtac leI 1); 
    1.45 +by (stac less_iff_Suc_add 1);
    1.46 +by (auto_tac (claset(), simpset() addsimps [add_mult_distrib2]));   
    1.47 +qed "unique_quotient_lemma";
    1.48 +
    1.49 +Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |] \
    1.50 +\     ==> q = q'";
    1.51 +by (asm_full_simp_tac 
    1.52 +    (simpset() addsimps split_ifs @ [quorem_def]) 1);
    1.53 +by Auto_tac;  
    1.54 +by (REPEAT 
    1.55 +    (blast_tac (claset() addIs [order_antisym]
    1.56 +			 addDs [order_eq_refl RS unique_quotient_lemma, 
    1.57 +				sym]) 1));
    1.58 +qed "unique_quotient";
    1.59 +
    1.60 +Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |] \
    1.61 +\     ==> r = r'";
    1.62 +by (subgoal_tac "q = q'" 1);
    1.63 +by (blast_tac (claset() addIs [unique_quotient]) 2);
    1.64 +by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
    1.65 +qed "unique_remainder";
    1.66 +
    1.67 +Goal "0 < b ==> quorem ((a, b), (a div b, a mod b))";
    1.68 +by (cut_inst_tac [("m","a"),("n","b")] mod_div_equality 1);
    1.69 +by (auto_tac
    1.70 +    (claset() addEs [sym],
    1.71 +     simpset() addsimps mult_ac@[quorem_def]));
    1.72 +qed "quorem_div_mod";
    1.73 +
    1.74 +Goal "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q";
    1.75 +by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1);
    1.76 +qed "quorem_div";
    1.77 +
    1.78 +Goal "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r";
    1.79 +by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1);
    1.80 +qed "quorem_mod";
    1.81 +
    1.82 +(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
    1.83 +
    1.84 +Goal "[| quorem((b,c),(q,r));  0 < c |] \
    1.85 +\     ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
    1.86 +by (cut_inst_tac [("m", "a*r"), ("n","c")] mod_div_equality 1);
    1.87 +by (auto_tac
    1.88 +    (claset(),
    1.89 +     simpset() addsimps split_ifs@mult_ac@
    1.90 +                        [quorem_def, add_mult_distrib2]));
    1.91 +val lemma = result();
    1.92 +
    1.93 +Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)";
    1.94 +by (div_undefined_case_tac "c = 0" 1);
    1.95 +by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
    1.96 +qed "div_mult1_eq";
    1.97 +
    1.98 +Goal "(a*b) mod c = a*(b mod c) mod (c::nat)";
    1.99 +by (div_undefined_case_tac "c = 0" 1);
   1.100 +by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
   1.101 +qed "mod_mult1_eq";
   1.102 +
   1.103 +Goal "(a*b) mod (c::nat) = ((a mod c) * b) mod c";
   1.104 +by (rtac trans 1);
   1.105 +by (res_inst_tac [("s","b*a mod c")] trans 1);
   1.106 +by (rtac mod_mult1_eq 2);
   1.107 +by (ALLGOALS (simp_tac (simpset() addsimps [mult_commute])));
   1.108 +qed "mod_mult1_eq'";
   1.109 +
   1.110 +Goal "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c";
   1.111 +by (rtac (mod_mult1_eq' RS trans) 1);
   1.112 +by (rtac mod_mult1_eq 1);
   1.113 +qed "mod_mult_distrib_mod";
   1.114 +
   1.115 +(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
   1.116 +
   1.117 +Goal "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |] \
   1.118 +\     ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
   1.119 +by (cut_inst_tac [("m", "ar+br"), ("n","c")] mod_div_equality 1);
   1.120 +by (auto_tac
   1.121 +    (claset(),
   1.122 +     simpset() addsimps split_ifs@mult_ac@
   1.123 +                        [quorem_def, add_mult_distrib2]));
   1.124 +val lemma = result();
   1.125 +
   1.126 +(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   1.127 +Goal "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)";
   1.128 +by (div_undefined_case_tac "c = 0" 1);
   1.129 +by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
   1.130 +			       MRS lemma RS quorem_div]) 1);
   1.131 +qed "div_add1_eq";
   1.132 +
   1.133 +Goal "(a+b) mod (c::nat) = (a mod c + b mod c) mod c";
   1.134 +by (div_undefined_case_tac "c = 0" 1);
   1.135 +by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
   1.136 +			       MRS lemma RS quorem_mod]) 1);
   1.137 +qed "mod_add1_eq";
   1.138 +
   1.139 +
   1.140 +(*** proving  a div (b*c) = (a div b) div c ***)
   1.141 +
   1.142 +(** first, two lemmas to bound the remainder for the cases b<0 and b>0 **)
   1.143 +
   1.144 +Goal "[| (0::nat) < c;  r < b |] ==> 0 <= b * (q mod c) + r";
   1.145 +by (subgoal_tac "0 <= b * (q mod c)" 1);
   1.146 +by Auto_tac;  
   1.147 +val lemma3 = result();
   1.148 +
   1.149 +Goal "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c";
   1.150 +by (cut_inst_tac [("m","q"),("n","c")] mod_less_divisor 1);
   1.151 +by (dres_inst_tac [("m","q mod c")] less_imp_Suc_add 2); 
   1.152 +by Auto_tac;  
   1.153 +by (eres_inst_tac [("P","%x. ?lhs < ?rhs x")] ssubst 1); 
   1.154 +by (asm_simp_tac (simpset() addsimps [add_mult_distrib2]) 1);
   1.155 +val lemma4 = result();
   1.156 +
   1.157 +Goal "[| quorem ((a,b), (q,r));  0 < b;  0 < c |] \
   1.158 +\     ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
   1.159 +by (cut_inst_tac [("m", "q"), ("n","c")] mod_div_equality 1);
   1.160 +by (auto_tac  
   1.161 +    (claset(),
   1.162 +     simpset() addsimps mult_ac@
   1.163 +                        [quorem_def, add_mult_distrib2 RS sym,
   1.164 +			 lemma3, lemma4]));
   1.165 +val lemma = result();
   1.166 +
   1.167 +Goal "(0::nat) < c ==> a div (b*c) = (a div b) div c";
   1.168 +by (div_undefined_case_tac "b = 0" 1);
   1.169 +by (force_tac (claset(),
   1.170 +	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_div]) 1);
   1.171 +qed "div_mult2_eq";
   1.172 +
   1.173 +Goal "(0::nat) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b";
   1.174 +by (div_undefined_case_tac "b = 0" 1);
   1.175 +by (force_tac (claset(),
   1.176 +	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod]) 1);
   1.177 +qed "mod_mult2_eq";
   1.178 +
   1.179 +
   1.180 +(*** Cancellation of common factors in "div" ***)
   1.181 +
   1.182 +Goal "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b";
   1.183 +by (stac div_mult2_eq 1);
   1.184 +by Auto_tac;
   1.185 +val lemma1 = result();
   1.186 +
   1.187 +Goal "(0::nat) < c ==> (c*a) div (c*b) = a div b";
   1.188 +by (div_undefined_case_tac "b = 0" 1);
   1.189 +by (auto_tac
   1.190 +    (claset(), 
   1.191 +     simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, 
   1.192 +			 lemma1, lemma2]));
   1.193 +qed "div_mult_mult1";
   1.194 +
   1.195 +Goal "(0::nat) < c ==> (a*c) div (b*c) = a div b";
   1.196 +by (dtac div_mult_mult1 1);
   1.197 +by (auto_tac (claset(), simpset() addsimps [mult_commute]));
   1.198 +qed "div_mult_mult2";
   1.199 +
   1.200 +Addsimps [div_mult_mult1, div_mult_mult2];
   1.201 +
   1.202 +
   1.203 +(*** Distribution of factors over "mod"
   1.204 +
   1.205 +Could prove these as in Integ/IntDiv.ML, but we already have
   1.206 +mod_mult_distrib and mod_mult_distrib2 above!
   1.207 +
   1.208 +Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)";
   1.209 +qed "mod_mult_mult1";
   1.210 +
   1.211 +Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
   1.212 +qed "mod_mult_mult2";
   1.213 + ***)
   1.214 +
   1.215 +(*** Further facts about div and mod ***)
   1.216 +
   1.217  Goal "m div 1 = m";
   1.218  by (induct_tac "m" 1);
   1.219  by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq])));
   1.220 @@ -181,7 +384,7 @@
   1.221  Goal "0<n ==> n div n = (1::nat)";
   1.222  by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
   1.223  qed "div_self";
   1.224 -
   1.225 +Addsimps [div_self];
   1.226  
   1.227  Goal "0<n ==> (m+n) div n = Suc (m div n)";
   1.228  by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1);
   1.229 @@ -194,8 +397,9 @@
   1.230  qed "div_add_self1";
   1.231  
   1.232  Goal "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n";
   1.233 -by (induct_tac "k" 1);
   1.234 -by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [div_add_self1])));
   1.235 +by (stac div_add1_eq 1); 
   1.236 +by (stac div_mult1_eq 1); 
   1.237 +by (Asm_simp_tac 1); 
   1.238  qed "div_mult_self1";
   1.239  
   1.240  Goal "0<n ==> (m + n*k) div n = k + m div (n::nat)";
   1.241 @@ -296,45 +500,6 @@
   1.242  	      simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq]));
   1.243  qed "mod_Suc";
   1.244  
   1.245 -Goal "0<n ==> m mod n < (n::nat)";
   1.246 -by (induct_thm_tac nat_less_induct "m" 1);
   1.247 -by (case_tac "na<n" 1);
   1.248 -(*case n le na*)
   1.249 -by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
   1.250 -(*case na<n*)
   1.251 -by (Asm_simp_tac 1);
   1.252 -qed "mod_less_divisor";
   1.253 -Addsimps [mod_less_divisor];
   1.254 -
   1.255 -(*** More division laws ***)
   1.256 -
   1.257 -Goal "0<n ==> (m*n) div n = (m::nat)";
   1.258 -by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1);
   1.259 -by Auto_tac;
   1.260 -qed "div_mult_self_is_m";
   1.261 -
   1.262 -Goal "0<n ==> (n*m) div n = (m::nat)";
   1.263 -by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1);
   1.264 -qed "div_mult_self1_is_m";
   1.265 -Addsimps [div_mult_self_is_m, div_mult_self1_is_m];
   1.266 -
   1.267 -(*Cancellation law for division*)
   1.268 -Goal "0<k ==> (k*m) div (k*n) = m div (n::nat)";
   1.269 -by (div_undefined_case_tac "n=0" 1);
   1.270 -by (induct_thm_tac nat_less_induct "m" 1);
   1.271 -by (case_tac "na<n" 1);
   1.272 -by (asm_simp_tac (simpset() addsimps [zero_less_mult_iff, mult_less_mono2]) 1);
   1.273 -by (subgoal_tac "~ k*na < k*n" 1);
   1.274 -by (asm_simp_tac
   1.275 -     (simpset() addsimps [zero_less_mult_iff, div_geq,
   1.276 -			  diff_mult_distrib2 RS sym, diff_less]) 1);
   1.277 -by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
   1.278 -                                          le_refl RS mult_le_mono]) 1);
   1.279 -qed "div_cancel";
   1.280 -Addsimps [div_cancel];
   1.281 -
   1.282 -(*mod_mult_distrib2 above is the counterpart for remainder*)
   1.283 -
   1.284  
   1.285  (************************************************)
   1.286  (** Divides Relation                           **)
     2.1 --- a/src/HOL/Divides.thy	Fri Dec 01 11:02:55 2000 +0100
     2.2 +++ b/src/HOL/Divides.thy	Fri Dec 01 11:03:31 2000 +0100
     2.3 @@ -36,4 +36,12 @@
     2.4  (*The definition of dvd is polymorphic!*)
     2.5    dvd_def   "m dvd n == EX k. n = m*k"
     2.6  
     2.7 +(*This definition helps prove the harder properties of div and mod.
     2.8 +  It is copied from IntDiv.thy; should it be overloaded?*)
     2.9 +constdefs
    2.10 +  quorem :: "(nat*nat) * (nat*nat) => bool"
    2.11 +    "quorem == %((a,b), (q,r)).
    2.12 +                      a = b*q + r &
    2.13 +                      (if 0<b then 0<=r & r<b else b<r & r <=0)"
    2.14 +
    2.15  end