author  paulson 
Fri, 04 Jul 1997 12:31:20 +0200  
changeset 3496  32e7edc609fd 
parent 3484  1e93eb09ebb9 
child 3718  d78cf498a88c 
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 
(*In ordinary notation: if 0<n and n<=m then mn < m *) 

13 
goal Arith.thy "!!m. [ 0<n; ~ m<n ] ==> m  n < m"; 

14 
by (subgoal_tac "0<n > ~ m<n > m  n < m" 1); 

15 
by (Blast_tac 1); 

16 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 

17 
by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc]))); 

18 
qed "diff_less"; 

19 

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

21 
def_wfrec RS trans; 

22 

23 
(*** Remainder ***) 

24 

25 
goal thy "(%m. m mod n) = wfrec (trancl pred_nat) \ 

26 
\ (%f j. if j<n then j else f (jn))"; 

27 
by (simp_tac (!simpset addsimps [mod_def]) 1); 

28 
qed "mod_eq"; 

29 

30 
goal thy "!!m. m<n ==> m mod n = m"; 

31 
by (rtac (mod_eq RS wf_less_trans) 1); 

32 
by (Asm_simp_tac 1); 

33 
qed "mod_less"; 

34 

35 
goal thy "!!m. [ 0<n; ~m<n ] ==> m mod n = (mn) mod n"; 

36 
by (rtac (mod_eq RS wf_less_trans) 1); 

37 
by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1); 

38 
qed "mod_geq"; 

39 

40 
goal thy "m mod 1 = 0"; 

41 
by (induct_tac "m" 1); 

42 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_less, mod_geq]))); 

43 
qed "mod_1"; 

44 
Addsimps [mod_1]; 

45 

46 
goal thy "!!n. 0<n ==> n mod n = 0"; 

47 
by (asm_simp_tac (!simpset addsimps [mod_less, mod_geq]) 1); 

48 
qed "mod_self"; 

49 

50 
goal thy "!!n. 0<n ==> (m+n) mod n = m mod n"; 

51 
by (subgoal_tac "(n + m) mod n = (n+mn) mod n" 1); 

52 
by (stac (mod_geq RS sym) 2); 

53 
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [add_commute]))); 

54 
qed "mod_eq_add"; 

55 

56 
goal thy "!!k. [ 0<k; 0<n ] ==> (m mod n)*k = (m*k) mod (n*k)"; 

57 
by (res_inst_tac [("n","m")] less_induct 1); 

58 
by (case_tac "na<n" 1); 

59 
(*case na<n*) 

60 
by (asm_simp_tac (!simpset addsimps [mod_less]) 1); 

61 
(*case n<=na*) 

62 
by (asm_simp_tac (!simpset addsimps [mod_geq, diff_less, zero_less_mult_iff, 

63 
diff_mult_distrib]) 1); 

64 
qed "mod_mult_distrib"; 

65 

66 
goal thy "!!k. [ 0<k; 0<n ] ==> k*(m mod n) = (k*m) mod (k*n)"; 

67 
by (res_inst_tac [("n","m")] less_induct 1); 

68 
by (case_tac "na<n" 1); 

69 
(*case na<n*) 

70 
by (asm_simp_tac (!simpset addsimps [mod_less]) 1); 

71 
(*case n<=na*) 

72 
by (asm_simp_tac (!simpset addsimps [mod_geq, diff_less, zero_less_mult_iff, 

73 
diff_mult_distrib2]) 1); 

74 
qed "mod_mult_distrib2"; 

75 

76 
goal thy "!!n. 0<n ==> m*n mod n = 0"; 

77 
by (induct_tac "m" 1); 

78 
by (asm_simp_tac (!simpset addsimps [mod_less]) 1); 

79 
by (dres_inst_tac [("m","m*n")] mod_eq_add 1); 

80 
by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1); 

81 
qed "mod_mult_self_is_0"; 

82 
Addsimps [mod_mult_self_is_0]; 

83 

84 
(*** Quotient ***) 

85 

86 
goal thy "(%m. m div n) = wfrec (trancl pred_nat) \ 

87 
\ (%f j. if j<n then 0 else Suc (f (jn)))"; 

88 
by (simp_tac (!simpset addsimps [div_def]) 1); 

89 
qed "div_eq"; 

90 

91 
goal thy "!!m. m<n ==> m div n = 0"; 

92 
by (rtac (div_eq RS wf_less_trans) 1); 

93 
by (Asm_simp_tac 1); 

94 
qed "div_less"; 

95 

96 
goal thy "!!M. [ 0<n; ~m<n ] ==> m div n = Suc((mn) div n)"; 

97 
by (rtac (div_eq RS wf_less_trans) 1); 

98 
by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1); 

99 
qed "div_geq"; 

100 

101 
(*Main Result about quotient and remainder.*) 

102 
goal thy "!!m. 0<n ==> (m div n)*n + m mod n = m"; 

103 
by (res_inst_tac [("n","m")] less_induct 1); 

104 
by (rename_tac "k" 1); (*Variable name used in line below*) 

105 
by (case_tac "k<n" 1); 

106 
by (ALLGOALS (asm_simp_tac(!simpset addsimps ([add_assoc] @ 

107 
[mod_less, mod_geq, div_less, div_geq, 

108 
add_diff_inverse, diff_less])))); 

109 
qed "mod_div_equality"; 

110 

111 
goal thy "m div 1 = m"; 

112 
by (induct_tac "m" 1); 

113 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [div_less, div_geq]))); 

114 
qed "div_1"; 

115 
Addsimps [div_1]; 

116 

117 
goal thy "!!n. 0<n ==> n div n = 1"; 

118 
by (asm_simp_tac (!simpset addsimps [div_less, div_geq]) 1); 

119 
qed "div_self"; 

120 

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

121 
(* Monotonicity of div in first argument *) 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

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

123 
by (res_inst_tac [("n","n")] less_induct 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

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

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

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

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

128 
by (asm_simp_tac (!simpset addsimps [div_less]) 1); 
3496  129 
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

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

131 
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

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

133 
by (asm_simp_tac (!simpset addsimps [div_less]) 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

134 
(* 2.2 case m>=k *) 
3496  135 
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

136 
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

137 

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

138 

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

139 
(* Antimonotonicity of div in second argument *) 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

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

141 
by (subgoal_tac "0<n" 1); 
3496  142 
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

143 
by (res_inst_tac [("n","k")] less_induct 1); 
3496  144 
by (Simp_tac 1); 
145 
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

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

147 
by (asm_simp_tac (!simpset addsimps [div_less]) 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

148 
by (subgoal_tac "~(k<m)" 1); 
3496  149 
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

150 
by (asm_simp_tac (!simpset addsimps [div_geq]) 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

151 
by (subgoal_tac "(kn) div n <= (km) div n" 1); 
3496  152 
by (best_tac (!claset addIs [le_trans] 
153 
addss (!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

154 
by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1)); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

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

156 

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

157 
goal thy "!!m n. 0<n ==> m div n <= m"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

158 
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

159 
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

160 
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

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

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

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

164 

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

165 
(* Similar for "less than" *) 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

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

167 
by (res_inst_tac [("n","m")] less_induct 1); 
3496  168 
by (Simp_tac 1); 
169 
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

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

171 
by (asm_full_simp_tac (!simpset addsimps [div_less]) 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

172 
by (subgoal_tac "0<n" 1); 
3496  173 
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

174 
by (asm_full_simp_tac (!simpset addsimps [div_geq]) 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

175 
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

176 
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

177 
by (REPEAT (ares_tac [impI,less_trans_Suc] 1)); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

178 
by (asm_full_simp_tac (!simpset addsimps [diff_less]) 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

179 
by (dres_inst_tac [("m","n")] less_imp_diff_positive 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

180 
by (asm_full_simp_tac (!simpset addsimps [diff_less]) 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

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

182 
by (subgoal_tac "m=n" 1); 
3496  183 
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

184 
by (asm_simp_tac (!simpset addsimps [div_less]) 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

185 
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

186 
Addsimps [div_less_dividend]; 
3366  187 

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

189 

190 
goal thy 

191 
"!!m n. 0<n ==> \ 

192 
\ Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"; 

193 
by (res_inst_tac [("n","m")] less_induct 1); 

194 
by (excluded_middle_tac "Suc(na)<n" 1); 

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

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

197 
by (asm_simp_tac (!simpset addsimps [mod_less, less_not_refl2 RS not_sym]) 2); 

198 
(* case n <= Suc(na) *) 

199 
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, mod_geq]) 1); 

200 
by (etac (le_imp_less_or_eq RS disjE) 1); 

201 
by (asm_simp_tac (!simpset addsimps [Suc_diff_n]) 1); 

202 
by (asm_full_simp_tac (!simpset addsimps [not_less_eq RS sym, 

203 
diff_less, mod_geq]) 1); 

204 
by (asm_simp_tac (!simpset addsimps [mod_less]) 1); 

205 
qed "mod_Suc"; 

206 

207 
goal thy "!!m n. 0<n ==> m mod n < n"; 

208 
by (res_inst_tac [("n","m")] less_induct 1); 

209 
by (excluded_middle_tac "na<n" 1); 

210 
(*case na<n*) 

211 
by (asm_simp_tac (!simpset addsimps [mod_less]) 2); 

212 
(*case n le na*) 

213 
by (asm_full_simp_tac (!simpset addsimps [mod_geq, diff_less]) 1); 

214 
qed "mod_less_divisor"; 

215 

216 

217 
(** Evens and Odds **) 

218 

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

220 
AddSEs [less_SucE]; 

221 

222 
goal thy "!!k b. b<2 ==> k mod 2 = b  k mod 2 = (if b=1 then 0 else 1)"; 

223 
by (subgoal_tac "k mod 2 < 2" 1); 

224 
by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2); 

225 
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1); 

226 
by (Blast_tac 1); 

227 
qed "mod2_cases"; 

228 

229 
goal thy "Suc(Suc(m)) mod 2 = m mod 2"; 

230 
by (subgoal_tac "m mod 2 < 2" 1); 

231 
by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2); 

232 
by (Step_tac 1); 

233 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_Suc]))); 

234 
qed "mod2_Suc_Suc"; 

235 
Addsimps [mod2_Suc_Suc]; 

236 

237 
goal thy "!!m. m mod 2 ~= 0 ==> m mod 2 = 1"; 

238 
by (subgoal_tac "m mod 2 < 2" 1); 

239 
by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2); 

240 
by (safe_tac (!claset addSEs [lessE])); 

241 
by (ALLGOALS (blast_tac (!claset addIs [sym]))); 

242 
qed "mod2_neq_0"; 

243 

244 
goal thy "(m+m) mod 2 = 0"; 

245 
by (induct_tac "m" 1); 

246 
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

247 
by (Asm_simp_tac 1); 
3366  248 
qed "mod2_add_self"; 
249 
Addsimps [mod2_add_self]; 

250 

251 
Delrules [less_SucE]; 

252 

253 

254 
(*** More division laws ***) 

255 

256 
goal thy "!!n. 0<n ==> m*n div n = m"; 

257 
by (cut_inst_tac [("m", "m*n")] mod_div_equality 1); 

3457  258 
by (assume_tac 1); 
3366  259 
by (asm_full_simp_tac (!simpset addsimps [mod_mult_self_is_0]) 1); 
260 
qed "div_mult_self_is_m"; 

261 
Addsimps [div_mult_self_is_m]; 

262 

263 
(*Cancellation law for division*) 

264 
goal thy "!!k. [ 0<n; 0<k ] ==> (k*m) div (k*n) = m div n"; 

265 
by (res_inst_tac [("n","m")] less_induct 1); 

266 
by (case_tac "na<n" 1); 

267 
by (asm_simp_tac (!simpset addsimps [div_less, zero_less_mult_iff, 

268 
mult_less_mono2]) 1); 

269 
by (subgoal_tac "~ k*na < k*n" 1); 

270 
by (asm_simp_tac 

271 
(!simpset addsimps [zero_less_mult_iff, div_geq, 

272 
diff_mult_distrib2 RS sym, diff_less]) 1); 

273 
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, 

274 
le_refl RS mult_le_mono]) 1); 

275 
qed "div_cancel"; 

276 
Addsimps [div_cancel]; 

277 

278 
goal thy "!!k. [ 0<n; 0<k ] ==> (k*m) mod (k*n) = k * (m mod n)"; 

279 
by (res_inst_tac [("n","m")] less_induct 1); 

280 
by (case_tac "na<n" 1); 

281 
by (asm_simp_tac (!simpset addsimps [mod_less, zero_less_mult_iff, 

282 
mult_less_mono2]) 1); 

283 
by (subgoal_tac "~ k*na < k*n" 1); 

284 
by (asm_simp_tac 

285 
(!simpset addsimps [zero_less_mult_iff, mod_geq, 

286 
diff_mult_distrib2 RS sym, diff_less]) 1); 

287 
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, 

288 
le_refl RS mult_le_mono]) 1); 

289 
qed "mult_mod_distrib"; 

290 

291 

292 
(************************************************) 

293 
(** Divides Relation **) 

294 
(************************************************) 

295 

296 
goalw thy [dvd_def] "m dvd 0"; 

297 
by (fast_tac (!claset addIs [mult_0_right RS sym]) 1); 

298 
qed "dvd_0_right"; 

299 
Addsimps [dvd_0_right]; 

300 

301 
goalw thy [dvd_def] "!!m. 0 dvd m ==> m = 0"; 

302 
by (fast_tac (!claset addss !simpset) 1); 

303 
qed "dvd_0_left"; 

304 

305 
goalw thy [dvd_def] "1 dvd k"; 

306 
by (Simp_tac 1); 

307 
qed "dvd_1_left"; 

308 
AddIffs [dvd_1_left]; 

309 

310 
goalw thy [dvd_def] "m dvd m"; 

311 
by (fast_tac (!claset addIs [mult_1_right RS sym]) 1); 

312 
qed "dvd_refl"; 

313 
Addsimps [dvd_refl]; 

314 

315 
goalw thy [dvd_def] "!!m n p. [ m dvd n; n dvd p ] ==> m dvd p"; 

316 
by (fast_tac (!claset addIs [mult_assoc] ) 1); 

317 
qed "dvd_trans"; 

318 

319 
goalw thy [dvd_def] "!!m n. [ m dvd n; n dvd m ] ==> m=n"; 

320 
by (fast_tac (!claset addDs [mult_eq_self_implies_10] 

321 
addss (!simpset addsimps [mult_assoc, mult_eq_1_iff])) 1); 

322 
qed "dvd_anti_sym"; 

323 

324 
goalw thy [dvd_def] "!!k. [ k dvd m; k dvd n ] ==> k dvd (m + n)"; 

325 
by (blast_tac (!claset addIs [add_mult_distrib2 RS sym]) 1); 

326 
qed "dvd_add"; 

327 

328 
goalw thy [dvd_def] "!!k. [ k dvd m; k dvd n ] ==> k dvd (mn)"; 

329 
by (blast_tac (!claset addIs [diff_mult_distrib2 RS sym]) 1); 

330 
qed "dvd_diff"; 

331 

332 
goal thy "!!k. [ k dvd (mn); k dvd n; n<=m ] ==> k dvd m"; 

3457  333 
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); 
3366  334 
by (blast_tac (!claset addIs [dvd_add]) 1); 
335 
qed "dvd_diffD"; 

336 

337 
goalw thy [dvd_def] "!!k. k dvd n ==> k dvd (m*n)"; 

338 
by (blast_tac (!claset addIs [mult_left_commute]) 1); 

339 
qed "dvd_mult"; 

340 

341 
goal thy "!!k. k dvd m ==> k dvd (m*n)"; 

342 
by (stac mult_commute 1); 

343 
by (etac dvd_mult 1); 

344 
qed "dvd_mult2"; 

345 

346 
(* k dvd (m*k) *) 

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

348 

349 
goalw thy [dvd_def] "!!m. [ f dvd m; f dvd n; 0<n ] ==> f dvd (m mod n)"; 

350 
by (Step_tac 1); 

351 
by (full_simp_tac (!simpset addsimps [zero_less_mult_iff]) 1); 

352 
by (res_inst_tac 

353 
[("x", "(((k div ka)*ka + k mod ka)  ((f*k) div (f*ka)) * ka)")] 

354 
exI 1); 

355 
by (asm_simp_tac (!simpset addsimps [diff_mult_distrib2, 

356 
mult_mod_distrib, add_mult_distrib2]) 1); 

357 
qed "dvd_mod"; 

358 

359 
goal thy "!!k. [ k dvd (m mod n); k dvd n; n~=0 ] ==> k dvd m"; 

360 
by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1); 

361 
by (asm_simp_tac (!simpset addsimps [dvd_add, dvd_mult]) 2); 

362 
by (asm_full_simp_tac (!simpset addsimps [mod_div_equality, zero_less_eq]) 1); 

363 
qed "dvd_mod_imp_dvd"; 

364 

365 
goalw thy [dvd_def] "!!k m n. [ (k*m) dvd (k*n); 0<k ] ==> m dvd n"; 

366 
by (etac exE 1); 

367 
by (asm_full_simp_tac (!simpset addsimps mult_ac) 1); 

368 
by (Blast_tac 1); 

369 
qed "dvd_mult_cancel"; 

370 

371 
goalw thy [dvd_def] "!!i j. [ i dvd m; j dvd n] ==> (i*j) dvd (m*n)"; 

372 
by (Step_tac 1); 

373 
by (res_inst_tac [("x","k*ka")] exI 1); 

374 
by (asm_simp_tac (!simpset addsimps mult_ac) 1); 

375 
qed "mult_dvd_mono"; 

376 

377 
goalw thy [dvd_def] "!!c. (i*j) dvd k ==> i dvd k"; 

378 
by (full_simp_tac (!simpset addsimps [mult_assoc]) 1); 

379 
by (Blast_tac 1); 

380 
qed "dvd_mult_left"; 

381 

382 
goalw thy [dvd_def] "!!n. [ k dvd n; 0 < n ] ==> k <= n"; 

383 
by (Step_tac 1); 

384 
by (ALLGOALS (full_simp_tac (!simpset addsimps [zero_less_mult_iff]))); 

3457  385 
by (etac conjE 1); 
386 
by (rtac le_trans 1); 

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

3366  388 
by (etac Suc_leI 2); 
389 
by (Simp_tac 1); 

390 
qed "dvd_imp_le"; 

391 

392 
goalw thy [dvd_def] "!!k. 0<k ==> (k dvd n) = (n mod k = 0)"; 

393 
by (Step_tac 1); 

394 
by (stac mult_commute 1); 

395 
by (Asm_simp_tac 1); 

396 
by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1); 

397 
by (asm_simp_tac (!simpset addsimps [mult_commute]) 1); 

398 
by (Blast_tac 1); 

399 
qed "dvd_eq_mod_eq_0"; 