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