author  paulson 
Wed, 23 Sep 1998 10:12:01 +0200  
changeset 5537  c2bd39a2c0ee 
parent 5498  7b81cae2774f 
child 5983  79e301a6a51b 
permissions  rwrr 
3366  1 
(* Title: HOL/Divides.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
The division operators div, mod and the divides relation "dvd" 

7 
*) 

8 

9 

10 
(** Lessthen properties **) 

11 

12 
val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS 

13 
def_wfrec RS trans; 

14 

15 
(*** Remainder ***) 

16 

5069  17 
Goal "(%m. m mod n) = wfrec (trancl pred_nat) \ 
5415  18 
\ (%f j. if j<n then j else f (jn))"; 
4089  19 
by (simp_tac (simpset() addsimps [mod_def]) 1); 
3366  20 
qed "mod_eq"; 
21 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

22 
Goal "m<n ==> m mod n = m"; 
3366  23 
by (rtac (mod_eq RS wf_less_trans) 1); 
24 
by (Asm_simp_tac 1); 

25 
qed "mod_less"; 

26 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

27 
Goal "[ 0<n; ~m<n ] ==> m mod n = (mn) mod n"; 
3366  28 
by (rtac (mod_eq RS wf_less_trans) 1); 
4089  29 
by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1); 
3366  30 
qed "mod_geq"; 
31 

5415  32 
(*Avoids the ugly ~m<n above*) 
33 
Goal "[ 0<n; n<=m ] ==> m mod n = (mn) mod n"; 

34 
by (asm_simp_tac (simpset() addsimps [mod_geq, not_less_iff_le]) 1); 

35 
qed "le_mod_geq"; 

36 

4774  37 
(*NOT suitable for rewriting: loops*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

38 
Goal "0<n ==> m mod n = (if m<n then m else (mn) mod n)"; 
4774  39 
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1); 
40 
qed "mod_if"; 

41 

5069  42 
Goal "m mod 1 = 0"; 
3366  43 
by (induct_tac "m" 1); 
4089  44 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]))); 
3366  45 
qed "mod_1"; 
46 
Addsimps [mod_1]; 

47 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

48 
Goal "0<n ==> n mod n = 0"; 
4089  49 
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1); 
3366  50 
qed "mod_self"; 
51 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

52 
Goal "0<n ==> (m+n) mod n = m mod n"; 
3366  53 
by (subgoal_tac "(n + m) mod n = (n+mn) mod n" 1); 
54 
by (stac (mod_geq RS sym) 2); 

4089  55 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); 
4811  56 
qed "mod_add_self2"; 
4810  57 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

58 
Goal "0<n ==> (n+m) mod n = m mod n"; 
4811  59 
by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1); 
60 
qed "mod_add_self1"; 

4810  61 

5069  62 
Goal "!!n. 0<n ==> (m + k*n) mod n = m mod n"; 
4810  63 
by (induct_tac "k" 1); 
5537  64 
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [mod_add_self1]))); 
4811  65 
qed "mod_mult_self1"; 
4810  66 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

67 
Goal "0<n ==> (m + n*k) mod n = m mod n"; 
4811  68 
by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1); 
69 
qed "mod_mult_self2"; 

4810  70 

4811  71 
Addsimps [mod_mult_self1, mod_mult_self2]; 
3366  72 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

73 
Goal "[ 0<k; 0<n ] ==> (m mod n)*k = (m*k) mod (n*k)"; 
3366  74 
by (res_inst_tac [("n","m")] less_induct 1); 
4774  75 
by (stac mod_if 1); 
76 
by (Asm_simp_tac 1); 

77 
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, 

78 
diff_less, diff_mult_distrib]) 1); 

3366  79 
qed "mod_mult_distrib"; 
80 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

81 
Goal "[ 0<k; 0<n ] ==> k*(m mod n) = (k*m) mod (k*n)"; 
3366  82 
by (res_inst_tac [("n","m")] less_induct 1); 
4774  83 
by (stac mod_if 1); 
84 
by (Asm_simp_tac 1); 

85 
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, 

86 
diff_less, diff_mult_distrib2]) 1); 

3366  87 
qed "mod_mult_distrib2"; 
88 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

89 
Goal "0<n ==> m*n mod n = 0"; 
3366  90 
by (induct_tac "m" 1); 
4089  91 
by (asm_simp_tac (simpset() addsimps [mod_less]) 1); 
5183  92 
by (dres_inst_tac [("m","na*n")] mod_add_self2 1); 
4089  93 
by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1); 
3366  94 
qed "mod_mult_self_is_0"; 
95 
Addsimps [mod_mult_self_is_0]; 

96 

97 
(*** Quotient ***) 

98 

5069  99 
Goal "(%m. m div n) = wfrec (trancl pred_nat) \ 
3366  100 
\ (%f j. if j<n then 0 else Suc (f (jn)))"; 
4089  101 
by (simp_tac (simpset() addsimps [div_def]) 1); 
3366  102 
qed "div_eq"; 
103 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

104 
Goal "m<n ==> m div n = 0"; 
3366  105 
by (rtac (div_eq RS wf_less_trans) 1); 
106 
by (Asm_simp_tac 1); 

107 
qed "div_less"; 

108 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

109 
Goal "[ 0<n; ~m<n ] ==> m div n = Suc((mn) div n)"; 
3366  110 
by (rtac (div_eq RS wf_less_trans) 1); 
4089  111 
by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1); 
3366  112 
qed "div_geq"; 
113 

5415  114 
(*Avoids the ugly ~m<n above*) 
115 
Goal "[ 0<n; n<=m ] ==> m div n = Suc((mn) div n)"; 

116 
by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1); 

117 
qed "le_div_geq"; 

118 

4774  119 
(*NOT suitable for rewriting: loops*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

120 
Goal "0<n ==> m div n = (if m<n then 0 else Suc((mn) div n))"; 
4774  121 
by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1); 
122 
qed "div_if"; 

123 

3366  124 
(*Main Result about quotient and remainder.*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

125 
Goal "0<n ==> (m div n)*n + m mod n = m"; 
3366  126 
by (res_inst_tac [("n","m")] less_induct 1); 
4774  127 
by (stac mod_if 1); 
128 
by (ALLGOALS (asm_simp_tac 

5537  129 
(simpset() addsimps [add_assoc, div_less, div_geq, 
130 
add_diff_inverse, diff_less]))); 

3366  131 
qed "mod_div_equality"; 
132 

4358  133 
(* a simple rearrangement of mod_div_equality: *) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

134 
Goal "0<k ==> k*(m div k) = m  (m mod k)"; 
4423  135 
by (dres_inst_tac [("m","m")] mod_div_equality 1); 
4358  136 
by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac), 
137 
K(IF_UNSOLVED no_tac)]); 

138 
qed "mult_div_cancel"; 

139 

5069  140 
Goal "m div 1 = m"; 
3366  141 
by (induct_tac "m" 1); 
4089  142 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_less, div_geq]))); 
3366  143 
qed "div_1"; 
144 
Addsimps [div_1]; 

145 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

146 
Goal "0<n ==> n div n = 1"; 
4089  147 
by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1); 
3366  148 
qed "div_self"; 
149 

4811  150 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

151 
Goal "0<n ==> (m+n) div n = Suc (m div n)"; 
4811  152 
by (subgoal_tac "(n + m) div n = Suc ((n+mn) div n)" 1); 
153 
by (stac (div_geq RS sym) 2); 

154 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); 

155 
qed "div_add_self2"; 

156 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

157 
Goal "0<n ==> (n+m) div n = Suc (m div n)"; 
4811  158 
by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1); 
159 
qed "div_add_self1"; 

160 

5069  161 
Goal "!!n. 0<n ==> (m + k*n) div n = k + m div n"; 
4811  162 
by (induct_tac "k" 1); 
5537  163 
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [div_add_self1]))); 
4811  164 
qed "div_mult_self1"; 
165 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

166 
Goal "0<n ==> (m + n*k) div n = k + m div n"; 
4811  167 
by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1); 
168 
qed "div_mult_self2"; 

169 

170 
Addsimps [div_mult_self1, div_mult_self2]; 

171 

172 

3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

173 
(* Monotonicity of div in first argument *) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

174 
Goal "0<k ==> ALL m. m <= n > (m div k) <= (n div k)"; 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

175 
by (res_inst_tac [("n","n")] less_induct 1); 
3718  176 
by (Clarify_tac 1); 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

177 
by (case_tac "n<k" 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

178 
(* 1 case n<k *) 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

179 
by (subgoal_tac "m<k" 1); 
4089  180 
by (asm_simp_tac (simpset() addsimps [div_less]) 1); 
3496  181 
by (trans_tac 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

182 
(* 2 case n >= k *) 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

183 
by (case_tac "m<k" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

184 
(* 2.1 case m<k *) 
4089  185 
by (asm_simp_tac (simpset() addsimps [div_less]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

186 
(* 2.2 case m>=k *) 
4089  187 
by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

188 
qed_spec_mp "div_le_mono"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

189 

1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

190 

1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

191 
(* Antimonotonicity of div in second argument *) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

192 
Goal "[ 0<m; m<=n ] ==> (k div n) <= (k div m)"; 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

193 
by (subgoal_tac "0<n" 1); 
3496  194 
by (trans_tac 2); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

195 
by (res_inst_tac [("n","k")] less_induct 1); 
3496  196 
by (Simp_tac 1); 
197 
by (rename_tac "k" 1); 

3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

198 
by (case_tac "k<n" 1); 
4089  199 
by (asm_simp_tac (simpset() addsimps [div_less]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

200 
by (subgoal_tac "~(k<m)" 1); 
3496  201 
by (trans_tac 2); 
4089  202 
by (asm_simp_tac (simpset() addsimps [div_geq]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

203 
by (subgoal_tac "(kn) div n <= (km) div n" 1); 
5316  204 
by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2)); 
5318  205 
by (rtac le_trans 1); 
5316  206 
by (Asm_simp_tac 1); 
207 
by (asm_simp_tac (simpset() addsimps [diff_less]) 1); 

3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

208 
qed "div_le_mono2"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

209 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

210 
Goal "0<n ==> m div n <= m"; 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

211 
by (subgoal_tac "m div n <= m div 1" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

212 
by (Asm_full_simp_tac 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

213 
by (rtac div_le_mono2 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

214 
by (ALLGOALS trans_tac); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

215 
qed "div_le_dividend"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

216 
Addsimps [div_le_dividend]; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

217 

1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

218 
(* Similar for "less than" *) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

219 
Goal "1<n ==> (0 < m) > (m div n < m)"; 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

220 
by (res_inst_tac [("n","m")] less_induct 1); 
3496  221 
by (Simp_tac 1); 
222 
by (rename_tac "m" 1); 

3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

223 
by (case_tac "m<n" 1); 
4089  224 
by (asm_full_simp_tac (simpset() addsimps [div_less]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

225 
by (subgoal_tac "0<n" 1); 
3496  226 
by (trans_tac 2); 
4089  227 
by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

228 
by (case_tac "n<m" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

229 
by (subgoal_tac "(mn) div n < (mn)" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

230 
by (REPEAT (ares_tac [impI,less_trans_Suc] 1)); 
4089  231 
by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1); 
232 
by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1); 

3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

233 
(* case n=m *) 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

234 
by (subgoal_tac "m=n" 1); 
3496  235 
by (trans_tac 2); 
4089  236 
by (asm_simp_tac (simpset() addsimps [div_less]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

237 
qed_spec_mp "div_less_dividend"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

238 
Addsimps [div_less_dividend]; 
3366  239 

240 
(*** Further facts about mod (mainly for the mutilated chess board ***) 

241 

5278  242 
Goal "0<n ==> Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"; 
3366  243 
by (res_inst_tac [("n","m")] less_induct 1); 
244 
by (excluded_middle_tac "Suc(na)<n" 1); 

245 
(* case Suc(na) < n *) 

246 
by (forward_tac [lessI RS less_trans] 2); 

5355  247 
by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl3]) 2); 
3366  248 
(* case n <= Suc(na) *) 
5415  249 
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, 
250 
mod_geq]) 1); 

251 
by (etac disjE 1); 

252 
by (asm_simp_tac (simpset() addsimps [mod_less]) 2); 

253 
by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_diff_less, 

254 
le_mod_geq]) 1); 

3366  255 
qed "mod_Suc"; 
256 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

257 
Goal "0<n ==> m mod n < n"; 
3366  258 
by (res_inst_tac [("n","m")] less_induct 1); 
5498  259 
by (case_tac "na<n" 1); 
260 
(*case n le na*) 

261 
by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2); 

3366  262 
(*case na<n*) 
5498  263 
by (asm_simp_tac (simpset() addsimps [mod_less]) 1); 
3366  264 
qed "mod_less_divisor"; 
265 

266 

267 
(** Evens and Odds **) 

268 

269 
(*With less_zeroE, causes case analysis on b<2*) 

270 
AddSEs [less_SucE]; 

271 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

272 
Goal "b<2 ==> k mod 2 = b  k mod 2 = (if b=1 then 0 else 1)"; 
3366  273 
by (subgoal_tac "k mod 2 < 2" 1); 
4089  274 
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); 
4686  275 
by (Asm_simp_tac 1); 
4356  276 
by Safe_tac; 
3366  277 
qed "mod2_cases"; 
278 

5069  279 
Goal "Suc(Suc(m)) mod 2 = m mod 2"; 
3366  280 
by (subgoal_tac "m mod 2 < 2" 1); 
4089  281 
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); 
3724  282 
by Safe_tac; 
4089  283 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc]))); 
3366  284 
qed "mod2_Suc_Suc"; 
285 
Addsimps [mod2_Suc_Suc]; 

286 

5069  287 
Goal "(0 < m mod 2) = (m mod 2 = 1)"; 
3366  288 
by (subgoal_tac "m mod 2 < 2" 1); 
4089  289 
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset

290 
by Auto_tac; 
4356  291 
qed "mod2_gr_0"; 
292 
Addsimps [mod2_gr_0]; 

293 

5069  294 
Goal "(m+m) mod 2 = 0"; 
3366  295 
by (induct_tac "m" 1); 
4089  296 
by (simp_tac (simpset() addsimps [mod_less]) 1); 
3427
e7cef2081106
Removed a few redundant additions of simprules or classical rules
paulson
parents:
3366
diff
changeset

297 
by (Asm_simp_tac 1); 
4385  298 
qed "mod2_add_self_eq_0"; 
299 
Addsimps [mod2_add_self_eq_0]; 

300 

5069  301 
Goal "((m+m)+n) mod 2 = n mod 2"; 
4385  302 
by (induct_tac "m" 1); 
303 
by (simp_tac (simpset() addsimps [mod_less]) 1); 

304 
by (Asm_simp_tac 1); 

3366  305 
qed "mod2_add_self"; 
306 
Addsimps [mod2_add_self]; 

307 

5498  308 
(*Restore the default*) 
3366  309 
Delrules [less_SucE]; 
310 

311 
(*** More division laws ***) 

312 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

313 
Goal "0<n ==> m*n div n = m"; 
3366  314 
by (cut_inst_tac [("m", "m*n")] mod_div_equality 1); 
3457  315 
by (assume_tac 1); 
4089  316 
by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1); 
3366  317 
qed "div_mult_self_is_m"; 
318 
Addsimps [div_mult_self_is_m]; 

319 

320 
(*Cancellation law for division*) 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

321 
Goal "[ 0<n; 0<k ] ==> (k*m) div (k*n) = m div n"; 
3366  322 
by (res_inst_tac [("n","m")] less_induct 1); 
323 
by (case_tac "na<n" 1); 

4089  324 
by (asm_simp_tac (simpset() addsimps [div_less, zero_less_mult_iff, 
3366  325 
mult_less_mono2]) 1); 
326 
by (subgoal_tac "~ k*na < k*n" 1); 

327 
by (asm_simp_tac 

4089  328 
(simpset() addsimps [zero_less_mult_iff, div_geq, 
5415  329 
diff_mult_distrib2 RS sym, diff_less]) 1); 
4089  330 
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
3366  331 
le_refl RS mult_le_mono]) 1); 
332 
qed "div_cancel"; 

333 
Addsimps [div_cancel]; 

334 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

335 
Goal "[ 0<n; 0<k ] ==> (k*m) mod (k*n) = k * (m mod n)"; 
3366  336 
by (res_inst_tac [("n","m")] less_induct 1); 
337 
by (case_tac "na<n" 1); 

4089  338 
by (asm_simp_tac (simpset() addsimps [mod_less, zero_less_mult_iff, 
3366  339 
mult_less_mono2]) 1); 
340 
by (subgoal_tac "~ k*na < k*n" 1); 

341 
by (asm_simp_tac 

4089  342 
(simpset() addsimps [zero_less_mult_iff, mod_geq, 
3366  343 
diff_mult_distrib2 RS sym, diff_less]) 1); 
4089  344 
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
3366  345 
le_refl RS mult_le_mono]) 1); 
346 
qed "mult_mod_distrib"; 

347 

348 

349 
(************************************************) 

350 
(** Divides Relation **) 

351 
(************************************************) 

352 

5069  353 
Goalw [dvd_def] "m dvd 0"; 
4089  354 
by (blast_tac (claset() addIs [mult_0_right RS sym]) 1); 
3366  355 
qed "dvd_0_right"; 
356 
Addsimps [dvd_0_right]; 

357 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

358 
Goalw [dvd_def] "0 dvd m ==> m = 0"; 
4089  359 
by (fast_tac (claset() addss simpset()) 1); 
3366  360 
qed "dvd_0_left"; 
361 

5069  362 
Goalw [dvd_def] "1 dvd k"; 
3366  363 
by (Simp_tac 1); 
364 
qed "dvd_1_left"; 

365 
AddIffs [dvd_1_left]; 

366 

5069  367 
Goalw [dvd_def] "m dvd m"; 
4089  368 
by (blast_tac (claset() addIs [mult_1_right RS sym]) 1); 
3366  369 
qed "dvd_refl"; 
370 
Addsimps [dvd_refl]; 

371 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

372 
Goalw [dvd_def] "[ m dvd n; n dvd p ] ==> m dvd p"; 
4089  373 
by (blast_tac (claset() addIs [mult_assoc] ) 1); 
3366  374 
qed "dvd_trans"; 
375 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

376 
Goalw [dvd_def] "[ m dvd n; n dvd m ] ==> m=n"; 
4089  377 
by (fast_tac (claset() addDs [mult_eq_self_implies_10] 
378 
addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1); 

3366  379 
qed "dvd_anti_sym"; 
380 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

381 
Goalw [dvd_def] "[ k dvd m; k dvd n ] ==> k dvd (m + n)"; 
4089  382 
by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1); 
3366  383 
qed "dvd_add"; 
384 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

385 
Goalw [dvd_def] "[ k dvd m; k dvd n ] ==> k dvd (mn)"; 
4089  386 
by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1); 
3366  387 
qed "dvd_diff"; 
388 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

389 
Goal "[ k dvd (mn); k dvd n; n<=m ] ==> k dvd m"; 
3457  390 
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); 
4089  391 
by (blast_tac (claset() addIs [dvd_add]) 1); 
3366  392 
qed "dvd_diffD"; 
393 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

394 
Goalw [dvd_def] "k dvd n ==> k dvd (m*n)"; 
4089  395 
by (blast_tac (claset() addIs [mult_left_commute]) 1); 
3366  396 
qed "dvd_mult"; 
397 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

398 
Goal "k dvd m ==> k dvd (m*n)"; 
3366  399 
by (stac mult_commute 1); 
400 
by (etac dvd_mult 1); 

401 
qed "dvd_mult2"; 

402 

403 
(* k dvd (m*k) *) 

404 
AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2]; 

405 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

406 
Goalw [dvd_def] "[ f dvd m; f dvd n; 0<n ] ==> f dvd (m mod n)"; 
3718  407 
by (Clarify_tac 1); 
4089  408 
by (full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1); 
3366  409 
by (res_inst_tac 
410 
[("x", "(((k div ka)*ka + k mod ka)  ((f*k) div (f*ka)) * ka)")] 

411 
exI 1); 

4089  412 
by (asm_simp_tac (simpset() addsimps [diff_mult_distrib2, 
3366  413 
mult_mod_distrib, add_mult_distrib2]) 1); 
414 
qed "dvd_mod"; 

415 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

416 
Goal "[ k dvd (m mod n); k dvd n; 0<n ] ==> k dvd m"; 
3366  417 
by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1); 
4089  418 
by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2); 
4356  419 
by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1); 
3366  420 
qed "dvd_mod_imp_dvd"; 
421 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

422 
Goalw [dvd_def] "!!k. [ (k*m) dvd (k*n); 0<k ] ==> m dvd n"; 
3366  423 
by (etac exE 1); 
4089  424 
by (asm_full_simp_tac (simpset() addsimps mult_ac) 1); 
3366  425 
by (Blast_tac 1); 
426 
qed "dvd_mult_cancel"; 

427 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

428 
Goalw [dvd_def] "[ i dvd m; j dvd n] ==> (i*j) dvd (m*n)"; 
3718  429 
by (Clarify_tac 1); 
3366  430 
by (res_inst_tac [("x","k*ka")] exI 1); 
4089  431 
by (asm_simp_tac (simpset() addsimps mult_ac) 1); 
3366  432 
qed "mult_dvd_mono"; 
433 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

434 
Goalw [dvd_def] "(i*j) dvd k ==> i dvd k"; 
4089  435 
by (full_simp_tac (simpset() addsimps [mult_assoc]) 1); 
3366  436 
by (Blast_tac 1); 
437 
qed "dvd_mult_left"; 

438 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

439 
Goalw [dvd_def] "[ k dvd n; 0 < n ] ==> k <= n"; 
3718  440 
by (Clarify_tac 1); 
4089  441 
by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff]))); 
3457  442 
by (etac conjE 1); 
443 
by (rtac le_trans 1); 

444 
by (rtac (le_refl RS mult_le_mono) 2); 

3366  445 
by (etac Suc_leI 2); 
446 
by (Simp_tac 1); 

447 
qed "dvd_imp_le"; 

448 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

449 
Goalw [dvd_def] "0<k ==> (k dvd n) = (n mod k = 0)"; 
3724  450 
by Safe_tac; 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

451 
by (asm_simp_tac (simpset() addsimps [mult_commute]) 1); 
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

452 
by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1); 
3366  453 
by (stac mult_commute 1); 
454 
by (Asm_simp_tac 1); 

455 
by (Blast_tac 1); 

456 
qed "dvd_eq_mod_eq_0"; 