author  haftmann 
Thu, 16 Apr 2009 10:11:34 +0200  
changeset 30930  11010e5f18f0 
parent 30652  752329615264 
child 30934  ed5377c2b0a3 
permissions  rwrr 
23164  1 
(* Title: HOL/IntDiv.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
Copyright 1999 University of Cambridge 

4 

5 
*) 

6 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

7 
header{* The Division Operators div and mod *} 
23164  8 

9 
theory IntDiv 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

10 
imports Int Divides FunDef 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30517
diff
changeset

11 
uses 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30517
diff
changeset

12 
"~~/src/Provers/Arith/cancel_numeral_factor.ML" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30517
diff
changeset

13 
"~~/src/Provers/Arith/extract_common_term.ML" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30517
diff
changeset

14 
("Tools/int_factor_simprocs.ML") 
23164  15 
begin 
16 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

17 
definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where 
23164  18 
{*definition of quotient and remainder*} 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

19 
[code]: "divmod_rel a b = (\<lambda>(q, r). a = b * q + r \<and> 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

20 
(if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0))" 
23164  21 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

22 
definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where 
23164  23 
{*for the division algorithm*} 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

24 
[code]: "adjust b = (\<lambda>(q, r). if 0 \<le> r  b then (2 * q + 1, r  b) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

25 
else (2 * q, r))" 
23164  26 

27 
text{*algorithm for the case @{text "a\<ge>0, b>0"}*} 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

28 
function posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

29 
"posDivAlg a b = (if a < b \<or> b \<le> 0 then (0, a) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

30 
else adjust b (posDivAlg a (2 * b)))" 
23164  31 
by auto 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

32 
termination by (relation "measure (\<lambda>(a, b). nat (a  b + 1))") auto 
23164  33 

34 
text{*algorithm for the case @{text "a<0, b>0"}*} 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

35 
function negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

36 
"negDivAlg a b = (if 0 \<le>a + b \<or> b \<le> 0 then (1, a + b) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

37 
else adjust b (negDivAlg a (2 * b)))" 
23164  38 
by auto 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

39 
termination by (relation "measure (\<lambda>(a, b). nat ( a  b))") auto 
23164  40 

41 
text{*algorithm for the general case @{term "b\<noteq>0"}*} 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

42 
definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

43 
[code inline]: "negateSnd = apsnd uminus" 
23164  44 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

45 
definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where 
23164  46 
{*The full division algorithm considers all possible signs for a, b 
47 
including the special case @{text "a=0, b<0"} because 

48 
@{term negDivAlg} requires @{term "a<0"}.*} 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

49 
"divmod a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

50 
else if a = 0 then (0, 0) 
23164  51 
else negateSnd (negDivAlg (a) (b)) 
52 
else 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

53 
if 0 < b then negDivAlg a b 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

54 
else negateSnd (posDivAlg (a) (b)))" 
23164  55 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25134
diff
changeset

56 
instantiation int :: Divides.div 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25134
diff
changeset

57 
begin 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25134
diff
changeset

58 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25134
diff
changeset

59 
definition 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

60 
div_def: "a div b = fst (divmod a b)" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25134
diff
changeset

61 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25134
diff
changeset

62 
definition 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

63 
mod_def: "a mod b = snd (divmod a b)" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25134
diff
changeset

64 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25134
diff
changeset

65 
instance .. 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25134
diff
changeset

66 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25134
diff
changeset

67 
end 
23164  68 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

69 
lemma divmod_mod_div: 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

70 
"divmod p q = (p div q, p mod q)" 
23164  71 
by (auto simp add: div_def mod_def) 
72 

73 
text{* 

74 
Here is the division algorithm in ML: 

75 

76 
\begin{verbatim} 

77 
fun posDivAlg (a,b) = 

78 
if a<b then (0,a) 

79 
else let val (q,r) = posDivAlg(a, 2*b) 

80 
in if 0\<le>rb then (2*q+1, rb) else (2*q, r) 

81 
end 

82 

83 
fun negDivAlg (a,b) = 

84 
if 0\<le>a+b then (~1,a+b) 

85 
else let val (q,r) = negDivAlg(a, 2*b) 

86 
in if 0\<le>rb then (2*q+1, rb) else (2*q, r) 

87 
end; 

88 

89 
fun negateSnd (q,r:int) = (q,~r); 

90 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

91 
fun divmod (a,b) = if 0\<le>a then 
23164  92 
if b>0 then posDivAlg (a,b) 
93 
else if a=0 then (0,0) 

94 
else negateSnd (negDivAlg (~a,~b)) 

95 
else 

96 
if 0<b then negDivAlg (a,b) 

97 
else negateSnd (posDivAlg (~a,~b)); 

98 
\end{verbatim} 

99 
*} 

100 

101 

102 

103 
subsection{*Uniqueness and Monotonicity of Quotients and Remainders*} 

104 

105 
lemma unique_quotient_lemma: 

106 
"[ b*q' + r' \<le> b*q + r; 0 \<le> r'; r' < b; r < b ] 

107 
==> q' \<le> (q::int)" 

108 
apply (subgoal_tac "r' + b * (q'q) \<le> r") 

109 
prefer 2 apply (simp add: right_diff_distrib) 

110 
apply (subgoal_tac "0 < b * (1 + q  q') ") 

111 
apply (erule_tac [2] order_le_less_trans) 

112 
prefer 2 apply (simp add: right_diff_distrib right_distrib) 

113 
apply (subgoal_tac "b * q' < b * (1 + q) ") 

114 
prefer 2 apply (simp add: right_diff_distrib right_distrib) 

115 
apply (simp add: mult_less_cancel_left) 

116 
done 

117 

118 
lemma unique_quotient_lemma_neg: 

119 
"[ b*q' + r' \<le> b*q + r; r \<le> 0; b < r; b < r' ] 

120 
==> q \<le> (q'::int)" 

121 
by (rule_tac b = "b" and r = "r'" and r' = "r" in unique_quotient_lemma, 

122 
auto) 

123 

124 
lemma unique_quotient: 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

125 
"[ divmod_rel a b (q, r); divmod_rel a b (q', r'); b \<noteq> 0 ] 
23164  126 
==> q = q'" 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

127 
apply (simp add: divmod_rel_def linorder_neq_iff split: split_if_asm) 
23164  128 
apply (blast intro: order_antisym 
129 
dest: order_eq_refl [THEN unique_quotient_lemma] 

130 
order_eq_refl [THEN unique_quotient_lemma_neg] sym)+ 

131 
done 

132 

133 

134 
lemma unique_remainder: 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

135 
"[ divmod_rel a b (q, r); divmod_rel a b (q', r'); b \<noteq> 0 ] 
23164  136 
==> r = r'" 
137 
apply (subgoal_tac "q = q'") 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

138 
apply (simp add: divmod_rel_def) 
23164  139 
apply (blast intro: unique_quotient) 
140 
done 

141 

142 

143 
subsection{*Correctness of @{term posDivAlg}, the Algorithm for NonNegative Dividends*} 

144 

145 
text{*And positive divisors*} 

146 

147 
lemma adjust_eq [simp]: 

148 
"adjust b (q,r) = 

149 
(let diff = rb in 

150 
if 0 \<le> diff then (2*q + 1, diff) 

151 
else (2*q, r))" 

152 
by (simp add: Let_def adjust_def) 

153 

154 
declare posDivAlg.simps [simp del] 

155 

156 
text{*use with a simproc to avoid repeatedly proving the premise*} 

157 
lemma posDivAlg_eqn: 

158 
"0 < b ==> 

159 
posDivAlg a b = (if a<b then (0,a) else adjust b (posDivAlg a (2*b)))" 

160 
by (rule posDivAlg.simps [THEN trans], simp) 

161 

162 
text{*Correctness of @{term posDivAlg}: it computes quotients correctly*} 

163 
theorem posDivAlg_correct: 

164 
assumes "0 \<le> a" and "0 < b" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

165 
shows "divmod_rel a b (posDivAlg a b)" 
23164  166 
using prems apply (induct a b rule: posDivAlg.induct) 
167 
apply auto 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

168 
apply (simp add: divmod_rel_def) 
23164  169 
apply (subst posDivAlg_eqn, simp add: right_distrib) 
170 
apply (case_tac "a < b") 

171 
apply simp_all 

172 
apply (erule splitE) 

173 
apply (auto simp add: right_distrib Let_def) 

174 
done 

175 

176 

177 
subsection{*Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends*} 

178 

179 
text{*And positive divisors*} 

180 

181 
declare negDivAlg.simps [simp del] 

182 

183 
text{*use with a simproc to avoid repeatedly proving the premise*} 

184 
lemma negDivAlg_eqn: 

185 
"0 < b ==> 

186 
negDivAlg a b = 

187 
(if 0\<le>a+b then (1,a+b) else adjust b (negDivAlg a (2*b)))" 

188 
by (rule negDivAlg.simps [THEN trans], simp) 

189 

190 
(*Correctness of negDivAlg: it computes quotients correctly 

191 
It doesn't work if a=0 because the 0/b equals 0, not 1*) 

192 
lemma negDivAlg_correct: 

193 
assumes "a < 0" and "b > 0" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

194 
shows "divmod_rel a b (negDivAlg a b)" 
23164  195 
using prems apply (induct a b rule: negDivAlg.induct) 
196 
apply (auto simp add: linorder_not_le) 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

197 
apply (simp add: divmod_rel_def) 
23164  198 
apply (subst negDivAlg_eqn, assumption) 
199 
apply (case_tac "a + b < (0\<Colon>int)") 

200 
apply simp_all 

201 
apply (erule splitE) 

202 
apply (auto simp add: right_distrib Let_def) 

203 
done 

204 

205 

206 
subsection{*Existence Shown by Proving the Division Algorithm to be Correct*} 

207 

208 
(*the case a=0*) 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

209 
lemma divmod_rel_0: "b \<noteq> 0 ==> divmod_rel 0 b (0, 0)" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

210 
by (auto simp add: divmod_rel_def linorder_neq_iff) 
23164  211 

212 
lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)" 

213 
by (subst posDivAlg.simps, auto) 

214 

215 
lemma negDivAlg_minus1 [simp]: "negDivAlg 1 b = (1, b  1)" 

216 
by (subst negDivAlg.simps, auto) 

217 

218 
lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,r)" 

219 
by (simp add: negateSnd_def) 

220 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

221 
lemma divmod_rel_neg: "divmod_rel (a) (b) qr ==> divmod_rel a b (negateSnd qr)" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

222 
by (auto simp add: split_ifs divmod_rel_def) 
23164  223 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

224 
lemma divmod_correct: "b \<noteq> 0 ==> divmod_rel a b (divmod a b)" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

225 
by (force simp add: linorder_neq_iff divmod_rel_0 divmod_def divmod_rel_neg 
23164  226 
posDivAlg_correct negDivAlg_correct) 
227 

228 
text{*Arbitrary definitions for division by zero. Useful to simplify 

229 
certain equations.*} 

230 

231 
lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

232 
by (simp add: div_def mod_def divmod_def posDivAlg.simps) 
23164  233 

234 

235 
text{*Basic laws about division and remainder*} 

236 

237 
lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" 

238 
apply (case_tac "b = 0", simp) 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

239 
apply (cut_tac a = a and b = b in divmod_correct) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

240 
apply (auto simp add: divmod_rel_def div_def mod_def) 
23164  241 
done 
242 

243 
lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k" 

244 
by(simp add: zmod_zdiv_equality[symmetric]) 

245 

246 
lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k" 

247 
by(simp add: mult_commute zmod_zdiv_equality[symmetric]) 

248 

249 
text {* Tool setup *} 

250 

26480  251 
ML {* 
23164  252 
local 
253 

254 
structure CancelDivMod = CancelDivModFun( 

255 
struct 

256 
val div_name = @{const_name Divides.div}; 

257 
val mod_name = @{const_name Divides.mod}; 

258 
val mk_binop = HOLogic.mk_binop; 

259 
val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT; 

260 
val dest_sum = Int_Numeral_Simprocs.dest_sum; 

261 
val div_mod_eqs = 

262 
map mk_meta_eq [@{thm zdiv_zmod_equality}, 

263 
@{thm zdiv_zmod_equality2}]; 

264 
val trans = trans; 

265 
val prove_eq_sums = 

266 
let 

23365  267 
val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac} 
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30323
diff
changeset

268 
in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end; 
23164  269 
end) 
270 

271 
in 

272 

28262
aa7ca36d67fd
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents:
27667
diff
changeset

273 
val cancel_zdiv_zmod_proc = Simplifier.simproc (the_context ()) 
26101  274 
"cancel_zdiv_zmod" ["(m::int) + n"] (K CancelDivMod.proc) 
23164  275 

276 
end; 

277 

278 
Addsimprocs [cancel_zdiv_zmod_proc] 

279 
*} 

280 

281 
lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

282 
apply (cut_tac a = a and b = b in divmod_correct) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

283 
apply (auto simp add: divmod_rel_def mod_def) 
23164  284 
done 
285 

286 
lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1, standard] 

287 
and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard] 

288 

289 
lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

290 
apply (cut_tac a = a and b = b in divmod_correct) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

291 
apply (auto simp add: divmod_rel_def div_def mod_def) 
23164  292 
done 
293 

294 
lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1, standard] 

295 
and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2, standard] 

296 

297 

298 

299 
subsection{*General Properties of div and mod*} 

300 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

301 
lemma divmod_rel_div_mod: "b \<noteq> 0 ==> divmod_rel a b (a div b, a mod b)" 
23164  302 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

303 
apply (force simp add: divmod_rel_def linorder_neq_iff) 
23164  304 
done 
305 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

306 
lemma divmod_rel_div: "[ divmod_rel a b (q, r); b \<noteq> 0 ] ==> a div b = q" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

307 
by (simp add: divmod_rel_div_mod [THEN unique_quotient]) 
23164  308 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

309 
lemma divmod_rel_mod: "[ divmod_rel a b (q, r); b \<noteq> 0 ] ==> a mod b = r" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

310 
by (simp add: divmod_rel_div_mod [THEN unique_remainder]) 
23164  311 

312 
lemma div_pos_pos_trivial: "[ (0::int) \<le> a; a < b ] ==> a div b = 0" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

313 
apply (rule divmod_rel_div) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

314 
apply (auto simp add: divmod_rel_def) 
23164  315 
done 
316 

317 
lemma div_neg_neg_trivial: "[ a \<le> (0::int); b < a ] ==> a div b = 0" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

318 
apply (rule divmod_rel_div) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

319 
apply (auto simp add: divmod_rel_def) 
23164  320 
done 
321 

322 
lemma div_pos_neg_trivial: "[ (0::int) < a; a+b \<le> 0 ] ==> a div b = 1" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

323 
apply (rule divmod_rel_div) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

324 
apply (auto simp add: divmod_rel_def) 
23164  325 
done 
326 

327 
(*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*) 

328 

329 
lemma mod_pos_pos_trivial: "[ (0::int) \<le> a; a < b ] ==> a mod b = a" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

330 
apply (rule_tac q = 0 in divmod_rel_mod) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

331 
apply (auto simp add: divmod_rel_def) 
23164  332 
done 
333 

334 
lemma mod_neg_neg_trivial: "[ a \<le> (0::int); b < a ] ==> a mod b = a" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

335 
apply (rule_tac q = 0 in divmod_rel_mod) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

336 
apply (auto simp add: divmod_rel_def) 
23164  337 
done 
338 

339 
lemma mod_pos_neg_trivial: "[ (0::int) < a; a+b \<le> 0 ] ==> a mod b = a+b" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

340 
apply (rule_tac q = "1" in divmod_rel_mod) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

341 
apply (auto simp add: divmod_rel_def) 
23164  342 
done 
343 

344 
text{*There is no @{text mod_neg_pos_trivial}.*} 

345 

346 

347 
(*Simpler laws such as a div b = (a div b) FAIL, but see just below*) 

348 
lemma zdiv_zminus_zminus [simp]: "(a) div (b) = a div (b::int)" 

349 
apply (case_tac "b = 0", simp) 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

350 
apply (simp add: divmod_rel_div_mod [THEN divmod_rel_neg, simplified, 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

351 
THEN divmod_rel_div, THEN sym]) 
23164  352 

353 
done 

354 

355 
(*Simpler laws such as a mod b = (a mod b) FAIL, but see just below*) 

356 
lemma zmod_zminus_zminus [simp]: "(a) mod (b) =  (a mod (b::int))" 

357 
apply (case_tac "b = 0", simp) 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

358 
apply (subst divmod_rel_div_mod [THEN divmod_rel_neg, simplified, THEN divmod_rel_mod], 
23164  359 
auto) 
360 
done 

361 

362 

363 
subsection{*Laws for div and mod with Unary Minus*} 

364 

365 
lemma zminus1_lemma: 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

366 
"divmod_rel a b (q, r) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

367 
==> divmod_rel (a) b (if r=0 then q else q  1, 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

368 
if r=0 then 0 else br)" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

369 
by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_diff_distrib) 
23164  370 

371 

372 
lemma zdiv_zminus1_eq_if: 

373 
"b \<noteq> (0::int) 

374 
==> (a) div b = 

375 
(if a mod b = 0 then  (a div b) else  (a div b)  1)" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

376 
by (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_div]) 
23164  377 

378 
lemma zmod_zminus1_eq_if: 

379 
"(a::int) mod b = (if a mod b = 0 then 0 else b  (a mod b))" 

380 
apply (case_tac "b = 0", simp) 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

381 
apply (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_mod]) 
23164  382 
done 
383 

29936  384 
lemma zmod_zminus1_not_zero: 
385 
fixes k l :: int 

386 
shows " k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0" 

387 
unfolding zmod_zminus1_eq_if by auto 

388 

23164  389 
lemma zdiv_zminus2: "a div (b) = (a::int) div b" 
390 
by (cut_tac a = "a" in zdiv_zminus_zminus, auto) 

391 

392 
lemma zmod_zminus2: "a mod (b) =  ((a::int) mod b)" 

393 
by (cut_tac a = "a" and b = b in zmod_zminus_zminus, auto) 

394 

395 
lemma zdiv_zminus2_eq_if: 

396 
"b \<noteq> (0::int) 

397 
==> a div (b) = 

398 
(if a mod b = 0 then  (a div b) else  (a div b)  1)" 

399 
by (simp add: zdiv_zminus1_eq_if zdiv_zminus2) 

400 

401 
lemma zmod_zminus2_eq_if: 

402 
"a mod (b::int) = (if a mod b = 0 then 0 else (a mod b)  b)" 

403 
by (simp add: zmod_zminus1_eq_if zmod_zminus2) 

404 

29936  405 
lemma zmod_zminus2_not_zero: 
406 
fixes k l :: int 

407 
shows "k mod  l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0" 

408 
unfolding zmod_zminus2_eq_if by auto 

409 

23164  410 

411 
subsection{*Division of a Number by Itself*} 

412 

413 
lemma self_quotient_aux1: "[ (0::int) < a; a = r + a*q; r < a ] ==> 1 \<le> q" 

414 
apply (subgoal_tac "0 < a*q") 

415 
apply (simp add: zero_less_mult_iff, arith) 

416 
done 

417 

418 
lemma self_quotient_aux2: "[ (0::int) < a; a = r + a*q; 0 \<le> r ] ==> q \<le> 1" 

419 
apply (subgoal_tac "0 \<le> a* (1q) ") 

420 
apply (simp add: zero_le_mult_iff) 

421 
apply (simp add: right_diff_distrib) 

422 
done 

423 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

424 
lemma self_quotient: "[ divmod_rel a a (q, r); a \<noteq> (0::int) ] ==> q = 1" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

425 
apply (simp add: split_ifs divmod_rel_def linorder_neq_iff) 
23164  426 
apply (rule order_antisym, safe, simp_all) 
427 
apply (rule_tac [3] a = "a" and r = "r" in self_quotient_aux1) 

428 
apply (rule_tac a = "a" and r = "r" in self_quotient_aux2) 

429 
apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+ 

430 
done 

431 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

432 
lemma self_remainder: "[ divmod_rel a a (q, r); a \<noteq> (0::int) ] ==> r = 0" 
23164  433 
apply (frule self_quotient, assumption) 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

434 
apply (simp add: divmod_rel_def) 
23164  435 
done 
436 

437 
lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

438 
by (simp add: divmod_rel_div_mod [THEN self_quotient]) 
23164  439 

440 
(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) 

441 
lemma zmod_self [simp]: "a mod a = (0::int)" 

442 
apply (case_tac "a = 0", simp) 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

443 
apply (simp add: divmod_rel_div_mod [THEN self_remainder]) 
23164  444 
done 
445 

446 

447 
subsection{*Computation of Division and Remainder*} 

448 

449 
lemma zdiv_zero [simp]: "(0::int) div b = 0" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

450 
by (simp add: div_def divmod_def) 
23164  451 

452 
lemma div_eq_minus1: "(0::int) < b ==> 1 div b = 1" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

453 
by (simp add: div_def divmod_def) 
23164  454 

455 
lemma zmod_zero [simp]: "(0::int) mod b = 0" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

456 
by (simp add: mod_def divmod_def) 
23164  457 

458 
lemma zmod_minus1: "(0::int) < b ==> 1 mod b = b  1" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

459 
by (simp add: mod_def divmod_def) 
23164  460 

461 
text{*a positive, b positive *} 

462 

463 
lemma div_pos_pos: "[ 0 < a; 0 \<le> b ] ==> a div b = fst (posDivAlg a b)" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

464 
by (simp add: div_def divmod_def) 
23164  465 

466 
lemma mod_pos_pos: "[ 0 < a; 0 \<le> b ] ==> a mod b = snd (posDivAlg a b)" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

467 
by (simp add: mod_def divmod_def) 
23164  468 

469 
text{*a negative, b positive *} 

470 

471 
lemma div_neg_pos: "[ a < 0; 0 < b ] ==> a div b = fst (negDivAlg a b)" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

472 
by (simp add: div_def divmod_def) 
23164  473 

474 
lemma mod_neg_pos: "[ a < 0; 0 < b ] ==> a mod b = snd (negDivAlg a b)" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

475 
by (simp add: mod_def divmod_def) 
23164  476 

477 
text{*a positive, b negative *} 

478 

479 
lemma div_pos_neg: 

480 
"[ 0 < a; b < 0 ] ==> a div b = fst (negateSnd (negDivAlg (a) (b)))" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

481 
by (simp add: div_def divmod_def) 
23164  482 

483 
lemma mod_pos_neg: 

484 
"[ 0 < a; b < 0 ] ==> a mod b = snd (negateSnd (negDivAlg (a) (b)))" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

485 
by (simp add: mod_def divmod_def) 
23164  486 

487 
text{*a negative, b negative *} 

488 

489 
lemma div_neg_neg: 

490 
"[ a < 0; b \<le> 0 ] ==> a div b = fst (negateSnd (posDivAlg (a) (b)))" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

491 
by (simp add: div_def divmod_def) 
23164  492 

493 
lemma mod_neg_neg: 

494 
"[ a < 0; b \<le> 0 ] ==> a mod b = snd (negateSnd (posDivAlg (a) (b)))" 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

495 
by (simp add: mod_def divmod_def) 
23164  496 

497 
text {*Simplify expresions in which div and mod combine numerical constants*} 

498 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

499 
lemma divmod_relI: 
24481  500 
"\<lbrakk>a == b * q + r; if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0\<rbrakk> 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

501 
\<Longrightarrow> divmod_rel a b (q, r)" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

502 
unfolding divmod_rel_def by simp 
24481  503 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

504 
lemmas divmod_rel_div_eq = divmod_relI [THEN divmod_rel_div, THEN eq_reflection] 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

505 
lemmas divmod_rel_mod_eq = divmod_relI [THEN divmod_rel_mod, THEN eq_reflection] 
24481  506 
lemmas arithmetic_simps = 
507 
arith_simps 

508 
add_special 

509 
OrderedGroup.add_0_left 

510 
OrderedGroup.add_0_right 

511 
mult_zero_left 

512 
mult_zero_right 

513 
mult_1_left 

514 
mult_1_right 

515 

516 
(* simprocs adapted from HOL/ex/Binary.thy *) 

517 
ML {* 

518 
local 

30517  519 
val mk_number = HOLogic.mk_number HOLogic.intT; 
520 
fun mk_cert u k l = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"} $ 

521 
(@{term "times :: int \<Rightarrow> int \<Rightarrow> int"} $ u $ mk_number k) $ 

522 
mk_number l; 

523 
fun prove ctxt prop = Goal.prove ctxt [] [] prop 

524 
(K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps @{thms arithmetic_simps})))); 

24481  525 
fun binary_proc proc ss ct = 
526 
(case Thm.term_of ct of 

527 
_ $ t $ u => 

528 
(case try (pairself (`(snd o HOLogic.dest_number))) (t, u) of 

529 
SOME args => proc (Simplifier.the_context ss) args 

530 
 NONE => NONE) 

531 
 _ => NONE); 

532 
in 

30517  533 
fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) => 
534 
if n = 0 then NONE 

535 
else let val (k, l) = Integer.div_mod m n; 

536 
in SOME (rule OF [prove ctxt (Logic.mk_equals (t, mk_cert u k l))]) end); 

537 
end 

24481  538 
*} 
539 

540 
simproc_setup binary_int_div ("number_of m div number_of n :: int") = 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

541 
{* K (divmod_proc (@{thm divmod_rel_div_eq})) *} 
24481  542 

543 
simproc_setup binary_int_mod ("number_of m mod number_of n :: int") = 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

544 
{* K (divmod_proc (@{thm divmod_rel_mod_eq})) *} 
24481  545 

23164  546 
lemmas posDivAlg_eqn_number_of [simp] = 
547 
posDivAlg_eqn [of "number_of v" "number_of w", standard] 

548 

549 
lemmas negDivAlg_eqn_number_of [simp] = 

550 
negDivAlg_eqn [of "number_of v" "number_of w", standard] 

551 

552 

553 
text{*Specialcase simplification *} 

554 

555 
lemma zmod_minus1_right [simp]: "a mod (1::int) = 0" 

556 
apply (cut_tac a = a and b = "1" in neg_mod_sign) 

557 
apply (cut_tac [2] a = a and b = "1" in neg_mod_bound) 

558 
apply (auto simp del: neg_mod_sign neg_mod_bound) 

559 
done 

560 

561 
lemma zdiv_minus1_right [simp]: "a div (1::int) = a" 

562 
by (cut_tac a = a and b = "1" in zmod_zdiv_equality, auto) 

563 

564 
(** The last remaining special cases for constant arithmetic: 

565 
1 div z and 1 mod z **) 

566 

567 
lemmas div_pos_pos_1_number_of [simp] = 

568 
div_pos_pos [OF int_0_less_1, of "number_of w", standard] 

569 

570 
lemmas div_pos_neg_1_number_of [simp] = 

571 
div_pos_neg [OF int_0_less_1, of "number_of w", standard] 

572 

573 
lemmas mod_pos_pos_1_number_of [simp] = 

574 
mod_pos_pos [OF int_0_less_1, of "number_of w", standard] 

575 

576 
lemmas mod_pos_neg_1_number_of [simp] = 

577 
mod_pos_neg [OF int_0_less_1, of "number_of w", standard] 

578 

579 

580 
lemmas posDivAlg_eqn_1_number_of [simp] = 

581 
posDivAlg_eqn [of concl: 1 "number_of w", standard] 

582 

583 
lemmas negDivAlg_eqn_1_number_of [simp] = 

584 
negDivAlg_eqn [of concl: 1 "number_of w", standard] 

585 

586 

587 

588 
subsection{*Monotonicity in the First Argument (Dividend)*} 

589 

590 
lemma zdiv_mono1: "[ a \<le> a'; 0 < (b::int) ] ==> a div b \<le> a' div b" 

591 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 

592 
apply (cut_tac a = a' and b = b in zmod_zdiv_equality) 

593 
apply (rule unique_quotient_lemma) 

594 
apply (erule subst) 

595 
apply (erule subst, simp_all) 

596 
done 

597 

598 
lemma zdiv_mono1_neg: "[ a \<le> a'; (b::int) < 0 ] ==> a' div b \<le> a div b" 

599 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 

600 
apply (cut_tac a = a' and b = b in zmod_zdiv_equality) 

601 
apply (rule unique_quotient_lemma_neg) 

602 
apply (erule subst) 

603 
apply (erule subst, simp_all) 

604 
done 

605 

606 

607 
subsection{*Monotonicity in the Second Argument (Divisor)*} 

608 

609 
lemma q_pos_lemma: 

610 
"[ 0 \<le> b'*q' + r'; r' < b'; 0 < b' ] ==> 0 \<le> (q'::int)" 

611 
apply (subgoal_tac "0 < b'* (q' + 1) ") 

612 
apply (simp add: zero_less_mult_iff) 

613 
apply (simp add: right_distrib) 

614 
done 

615 

616 
lemma zdiv_mono2_lemma: 

617 
"[ b*q + r = b'*q' + r'; 0 \<le> b'*q' + r'; 

618 
r' < b'; 0 \<le> r; 0 < b'; b' \<le> b ] 

619 
==> q \<le> (q'::int)" 

620 
apply (frule q_pos_lemma, assumption+) 

621 
apply (subgoal_tac "b*q < b* (q' + 1) ") 

622 
apply (simp add: mult_less_cancel_left) 

623 
apply (subgoal_tac "b*q = r'  r + b'*q'") 

624 
prefer 2 apply simp 

625 
apply (simp (no_asm_simp) add: right_distrib) 

626 
apply (subst add_commute, rule zadd_zless_mono, arith) 

627 
apply (rule mult_right_mono, auto) 

628 
done 

629 

630 
lemma zdiv_mono2: 

631 
"[ (0::int) \<le> a; 0 < b'; b' \<le> b ] ==> a div b \<le> a div b'" 

632 
apply (subgoal_tac "b \<noteq> 0") 

633 
prefer 2 apply arith 

634 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 

635 
apply (cut_tac a = a and b = b' in zmod_zdiv_equality) 

636 
apply (rule zdiv_mono2_lemma) 

637 
apply (erule subst) 

638 
apply (erule subst, simp_all) 

639 
done 

640 

641 
lemma q_neg_lemma: 

642 
"[ b'*q' + r' < 0; 0 \<le> r'; 0 < b' ] ==> q' \<le> (0::int)" 

643 
apply (subgoal_tac "b'*q' < 0") 

644 
apply (simp add: mult_less_0_iff, arith) 

645 
done 

646 

647 
lemma zdiv_mono2_neg_lemma: 

648 
"[ b*q + r = b'*q' + r'; b'*q' + r' < 0; 

649 
r < b; 0 \<le> r'; 0 < b'; b' \<le> b ] 

650 
==> q' \<le> (q::int)" 

651 
apply (frule q_neg_lemma, assumption+) 

652 
apply (subgoal_tac "b*q' < b* (q + 1) ") 

653 
apply (simp add: mult_less_cancel_left) 

654 
apply (simp add: right_distrib) 

655 
apply (subgoal_tac "b*q' \<le> b'*q'") 

656 
prefer 2 apply (simp add: mult_right_mono_neg, arith) 

657 
done 

658 

659 
lemma zdiv_mono2_neg: 

660 
"[ a < (0::int); 0 < b'; b' \<le> b ] ==> a div b' \<le> a div b" 

661 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 

662 
apply (cut_tac a = a and b = b' in zmod_zdiv_equality) 

663 
apply (rule zdiv_mono2_neg_lemma) 

664 
apply (erule subst) 

665 
apply (erule subst, simp_all) 

666 
done 

667 

25942  668 

23164  669 
subsection{*More Algebraic Laws for div and mod*} 
670 

671 
text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *} 

672 

673 
lemma zmult1_lemma: 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

674 
"[ divmod_rel b c (q, r); c \<noteq> 0 ] 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

675 
==> divmod_rel (a * b) c (a*q + a*r div c, a*r mod c)" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

676 
by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_distrib) 
23164  677 

678 
lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)" 

679 
apply (case_tac "c = 0", simp) 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

680 
apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_div]) 
23164  681 
done 
682 

683 
lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)" 

684 
apply (case_tac "c = 0", simp) 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

685 
apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod]) 
23164  686 
done 
687 

29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29045
diff
changeset

688 
lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)" 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

689 
apply (case_tac "b = 0", simp) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

690 
apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

691 
done 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

692 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

693 
text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *} 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

694 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

695 
lemma zadd1_lemma: 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

696 
"[ divmod_rel a c (aq, ar); divmod_rel b c (bq, br); c \<noteq> 0 ] 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

697 
==> divmod_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

698 
by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_distrib) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

699 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

700 
(*NOT suitable for rewriting: the RHS has an instance of the LHS*) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

701 
lemma zdiv_zadd1_eq: 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

702 
"(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

703 
apply (case_tac "c = 0", simp) 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

704 
apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_div) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

705 
done 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

706 

29405
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

707 
instance int :: ring_div 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

708 
proof 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

709 
fix a b c :: int 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

710 
assume not0: "b \<noteq> 0" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

711 
show "(a + c * b) div b = c + a div b" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

712 
unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
30181  713 
by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq) 
30930  714 
next 
715 
fix a b c :: int 

716 
assume "a \<noteq> 0" 

717 
then show "(a * b) div (a * c) = b div c" 

718 
proof (cases "b \<noteq> 0 \<and> c \<noteq> 0") 

719 
case False then show ?thesis by auto 

720 
next 

721 
case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto 

722 
with `a \<noteq> 0` 

723 
have "\<And>q r. divmod_rel b c (q, r) \<Longrightarrow> divmod_rel (a * b) (a * c) (q, a * r)" 

724 
apply (auto simp add: divmod_rel_def) 

725 
apply (auto simp add: algebra_simps) 

726 
apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff) 

727 
apply (simp_all add: mult_less_cancel_left_disj mult_commute [of _ a]) 

728 
done 

729 
moreover with `c \<noteq> 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto 

730 
ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" . 

731 
moreover from `a \<noteq> 0` `c \<noteq> 0` have "a * c \<noteq> 0" by simp 

732 
ultimately show ?thesis by (rule divmod_rel_div) 

733 
qed 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

734 
qed auto 
25942  735 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

736 
lemma posDivAlg_div_mod: 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

737 
assumes "k \<ge> 0" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

738 
and "l \<ge> 0" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

739 
shows "posDivAlg k l = (k div l, k mod l)" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

740 
proof (cases "l = 0") 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

741 
case True then show ?thesis by (simp add: posDivAlg.simps) 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

742 
next 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

743 
case False with assms posDivAlg_correct 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

744 
have "divmod_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

745 
by simp 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

746 
from divmod_rel_div [OF this `l \<noteq> 0`] divmod_rel_mod [OF this `l \<noteq> 0`] 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

747 
show ?thesis by simp 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

748 
qed 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

749 

16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

750 
lemma negDivAlg_div_mod: 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

751 
assumes "k < 0" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

752 
and "l > 0" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

753 
shows "negDivAlg k l = (k div l, k mod l)" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

754 
proof  
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

755 
from assms have "l \<noteq> 0" by simp 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

756 
from assms negDivAlg_correct 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

757 
have "divmod_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

758 
by simp 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

759 
from divmod_rel_div [OF this `l \<noteq> 0`] divmod_rel_mod [OF this `l \<noteq> 0`] 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

760 
show ?thesis by simp 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

761 
qed 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

762 

23164  763 
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)" 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29045
diff
changeset

764 
by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) 
23164  765 

29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29045
diff
changeset

766 
(* REVISIT: should this be generalized to all semiring_div types? *) 
23164  767 
lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1] 
768 

23983  769 

23164  770 
subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *} 
771 

772 
(*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but 

773 
7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems 

774 
to cause particular problems.*) 

775 

776 
text{*first, four lemmas to bound the remainder for the cases b<0 and b>0 *} 

777 

778 
lemma zmult2_lemma_aux1: "[ (0::int) < c; b < r; r \<le> 0 ] ==> b*c < b*(q mod c) + r" 

779 
apply (subgoal_tac "b * (c  q mod c) < r * 1") 

29667  780 
apply (simp add: algebra_simps) 
23164  781 
apply (rule order_le_less_trans) 
29667  782 
apply (erule_tac [2] mult_strict_right_mono) 
783 
apply (rule mult_left_mono_neg) 

784 
using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps pos_mod_bound) 

785 
apply (simp) 

786 
apply (simp) 

23164  787 
done 
788 

789 
lemma zmult2_lemma_aux2: 

790 
"[ (0::int) < c; b < r; r \<le> 0 ] ==> b * (q mod c) + r \<le> 0" 

791 
apply (subgoal_tac "b * (q mod c) \<le> 0") 

792 
apply arith 

793 
apply (simp add: mult_le_0_iff) 

794 
done 

795 

796 
lemma zmult2_lemma_aux3: "[ (0::int) < c; 0 \<le> r; r < b ] ==> 0 \<le> b * (q mod c) + r" 

797 
apply (subgoal_tac "0 \<le> b * (q mod c) ") 

798 
apply arith 

799 
apply (simp add: zero_le_mult_iff) 

800 
done 

801 

802 
lemma zmult2_lemma_aux4: "[ (0::int) < c; 0 \<le> r; r < b ] ==> b * (q mod c) + r < b * c" 

803 
apply (subgoal_tac "r * 1 < b * (c  q mod c) ") 

29667  804 
apply (simp add: right_diff_distrib) 
23164  805 
apply (rule order_less_le_trans) 
29667  806 
apply (erule mult_strict_right_mono) 
807 
apply (rule_tac [2] mult_left_mono) 

808 
apply simp 

809 
using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps pos_mod_bound) 

810 
apply simp 

23164  811 
done 
812 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

813 
lemma zmult2_lemma: "[ divmod_rel a b (q, r); b \<noteq> 0; 0 < c ] 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

814 
==> divmod_rel a (b * c) (q div c, b*(q mod c) + r)" 
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

815 
by (auto simp add: mult_ac divmod_rel_def linorder_neq_iff 
23164  816 
zero_less_mult_iff right_distrib [symmetric] 
817 
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4) 

818 

819 
lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c" 

820 
apply (case_tac "b = 0", simp) 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

821 
apply (force simp add: divmod_rel_div_mod [THEN zmult2_lemma, THEN divmod_rel_div]) 
23164  822 
done 
823 

824 
lemma zmod_zmult2_eq: 

825 
"(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b" 

826 
apply (case_tac "b = 0", simp) 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

827 
apply (force simp add: divmod_rel_div_mod [THEN zmult2_lemma, THEN divmod_rel_mod]) 
23164  828 
done 
829 

830 

831 
subsection {*Splitting Rules for div and mod*} 

832 

833 
text{*The proofs of the two lemmas below are essentially identical*} 

834 

835 
lemma split_pos_lemma: 

836 
"0<k ==> 

837 
P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j > P i j)" 

838 
apply (rule iffI, clarify) 

839 
apply (erule_tac P="P ?x ?y" in rev_mp) 

29948  840 
apply (subst mod_add_eq) 
23164  841 
apply (subst zdiv_zadd1_eq) 
842 
apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial) 

843 
txt{*converse direction*} 

844 
apply (drule_tac x = "n div k" in spec) 

845 
apply (drule_tac x = "n mod k" in spec, simp) 

846 
done 

847 

848 
lemma split_neg_lemma: 

849 
"k<0 ==> 

850 
P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j > P i j)" 

851 
apply (rule iffI, clarify) 

852 
apply (erule_tac P="P ?x ?y" in rev_mp) 

29948  853 
apply (subst mod_add_eq) 
23164  854 
apply (subst zdiv_zadd1_eq) 
855 
apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial) 

856 
txt{*converse direction*} 

857 
apply (drule_tac x = "n div k" in spec) 

858 
apply (drule_tac x = "n mod k" in spec, simp) 

859 
done 

860 

861 
lemma split_zdiv: 

862 
"P(n div k :: int) = 

863 
((k = 0 > P 0) & 

864 
(0<k > (\<forall>i j. 0\<le>j & j<k & n = k*i + j > P i)) & 

865 
(k<0 > (\<forall>i j. k<j & j\<le>0 & n = k*i + j > P i)))" 

866 
apply (case_tac "k=0", simp) 

867 
apply (simp only: linorder_neq_iff) 

868 
apply (erule disjE) 

869 
apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"] 

870 
split_neg_lemma [of concl: "%x y. P x"]) 

871 
done 

872 

873 
lemma split_zmod: 

874 
"P(n mod k :: int) = 

875 
((k = 0 > P n) & 

876 
(0<k > (\<forall>i j. 0\<le>j & j<k & n = k*i + j > P j)) & 

877 
(k<0 > (\<forall>i j. k<j & j\<le>0 & n = k*i + j > P j)))" 

878 
apply (case_tac "k=0", simp) 

879 
apply (simp only: linorder_neq_iff) 

880 
apply (erule disjE) 

881 
apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"] 

882 
split_neg_lemma [of concl: "%x y. P y"]) 

883 
done 

884 

885 
(* Enable arith to deal with div 2 and mod 2: *) 

886 
declare split_zdiv [of _ _ "number_of k", simplified, standard, arith_split] 

887 
declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split] 

888 

889 

890 
subsection{*Speeding up the Division Algorithm with Shifting*} 

891 

892 
text{*computing div by shifting *} 

893 

894 
lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a" 

895 
proof cases 

896 
assume "a=0" 

897 
thus ?thesis by simp 

898 
next 

899 
assume "a\<noteq>0" and le_a: "0\<le>a" 

900 
hence a_pos: "1 \<le> a" by arith 

30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30517
diff
changeset

901 
hence one_less_a2: "1 < 2 * a" by arith 
23164  902 
hence le_2a: "2 * (1 + b mod a) \<le> 2 * a" 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30517
diff
changeset

903 
unfolding mult_le_cancel_left 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30517
diff
changeset

904 
by (simp add: add1_zle_eq add_commute [of 1]) 
23164  905 
with a_pos have "0 \<le> b mod a" by simp 
906 
hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)" 

907 
by (simp add: mod_pos_pos_trivial one_less_a2) 

908 
with le_2a 

909 
have "(1 mod (2*a) + 2*(b mod a)) div (2*a) = 0" 

910 
by (simp add: div_pos_pos_trivial le_addm mod_pos_pos_trivial one_less_a2 

911 
right_distrib) 

912 
thus ?thesis 

913 
by (subst zdiv_zadd1_eq, 

30930  914 
simp add: mod_mult_mult1 one_less_a2 
23164  915 
div_pos_pos_trivial) 
916 
qed 

917 

918 
lemma neg_zdiv_mult_2: "a \<le> (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a" 

919 
apply (subgoal_tac " (1 + 2* (b  1)) div (2 * (a)) = (b  1) div (a) ") 

920 
apply (rule_tac [2] pos_zdiv_mult_2) 

921 
apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib) 

922 
apply (subgoal_tac " (1  (2 * b)) =  (1 + (2 * b))") 

923 
apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric], 

924 
simp) 

925 
done 

926 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

927 
lemma zdiv_number_of_Bit0 [simp]: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

928 
"number_of (Int.Bit0 v) div number_of (Int.Bit0 w) = 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

929 
number_of v div (number_of w :: int)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

930 
by (simp only: number_of_eq numeral_simps) simp 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

931 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

932 
lemma zdiv_number_of_Bit1 [simp]: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

933 
"number_of (Int.Bit1 v) div number_of (Int.Bit0 w) = 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

934 
(if (0::int) \<le> number_of w 
23164  935 
then number_of v div (number_of w) 
936 
else (number_of v + (1::int)) div (number_of w))" 

937 
apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if) 

30930  938 
apply (simp add: pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac) 
23164  939 
done 
940 

941 

942 
subsection{*Computing mod by Shifting (proofs resemble those for div)*} 

943 

944 
lemma pos_zmod_mult_2: 

945 
"(0::int) \<le> a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)" 

946 
apply (case_tac "a = 0", simp) 

947 
apply (subgoal_tac "1 < a * 2") 

948 
prefer 2 apply arith 

949 
apply (subgoal_tac "2* (1 + b mod a) \<le> 2*a") 

950 
apply (rule_tac [2] mult_left_mono) 

951 
apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq 

952 
pos_mod_bound) 

29948  953 
apply (subst mod_add_eq) 
30930  954 
apply (simp add: mod_mult_mult2 mod_pos_pos_trivial) 
23164  955 
apply (rule mod_pos_pos_trivial) 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

956 
apply (auto simp add: mod_pos_pos_trivial ring_distribs) 
23164  957 
apply (subgoal_tac "0 \<le> b mod a", arith, simp) 
958 
done 

959 

960 
lemma neg_zmod_mult_2: 

961 
"a \<le> (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a)  1" 

962 
apply (subgoal_tac "(1 + 2* (b  1)) mod (2* (a)) = 

963 
1 + 2* ((b  1) mod (a))") 

964 
apply (rule_tac [2] pos_zmod_mult_2) 

30042  965 
apply (auto simp add: right_diff_distrib) 
23164  966 
apply (subgoal_tac " (1  (2 * b)) =  (1 + (2 * b))") 
967 
prefer 2 apply simp 

968 
apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric]) 

969 
done 

970 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

971 
lemma zmod_number_of_Bit0 [simp]: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

972 
"number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) = 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

973 
(2::int) * (number_of v mod number_of w)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

974 
apply (simp only: number_of_eq numeral_simps) 
30930  975 
apply (simp add: mod_mult_mult1 pos_zmod_mult_2 
29948  976 
neg_zmod_mult_2 add_ac) 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

977 
done 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

978 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

979 
lemma zmod_number_of_Bit1 [simp]: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

980 
"number_of (Int.Bit1 v) mod number_of (Int.Bit0 w) = 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

981 
(if (0::int) \<le> number_of w 
23164  982 
then 2 * (number_of v mod number_of w) + 1 
983 
else 2 * ((number_of v + (1::int)) mod number_of w)  1)" 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25961
diff
changeset

984 
apply (simp only: number_of_eq numeral_simps) 
30930  985 
apply (simp add: mod_mult_mult1 pos_zmod_mult_2 
29948  986 
neg_zmod_mult_2 add_ac) 
23164  987 
done 
988 

989 

990 
subsection{*Quotients of Signs*} 

991 

992 
lemma div_neg_pos_less0: "[ a < (0::int); 0 < b ] ==> a div b < 0" 

993 
apply (subgoal_tac "a div b \<le> 1", force) 

994 
apply (rule order_trans) 

995 
apply (rule_tac a' = "1" in zdiv_mono1) 

29948  996 
apply (auto simp add: div_eq_minus1) 
23164  997 
done 
998 

30323  999 
lemma div_nonneg_neg_le0: "[ (0::int) \<le> a; b < 0 ] ==> a div b \<le> 0" 
23164  1000 
by (drule zdiv_mono1_neg, auto) 
1001 

30323  1002 
lemma div_nonpos_pos_le0: "[ (a::int) \<le> 0; b > 0 ] ==> a div b \<le> 0" 
1003 
by (drule zdiv_mono1, auto) 

1004 

23164  1005 
lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)" 
1006 
apply auto 

1007 
apply (drule_tac [2] zdiv_mono1) 

1008 
apply (auto simp add: linorder_neq_iff) 

1009 
apply (simp (no_asm_use) add: linorder_not_less [symmetric]) 

1010 
apply (blast intro: div_neg_pos_less0) 

1011 
done 

1012 

1013 
lemma neg_imp_zdiv_nonneg_iff: 

1014 
"b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))" 

1015 
apply (subst zdiv_zminus_zminus [symmetric]) 

1016 
apply (subst pos_imp_zdiv_nonneg_iff, auto) 

1017 
done 

1018 

1019 
(*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*) 

1020 
lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)" 

1021 
by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff) 

1022 

1023 
(*Again the law fails for \<le>: consider a = 1, b = 2 when a div b = 0*) 

1024 
lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)" 

1025 
by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff) 

1026 

1027 

1028 
subsection {* The Divides Relation *} 

1029 

1030 
lemmas zdvd_iff_zmod_eq_0_number_of [simp] = 

30042  1031 
dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard] 
23164  1032 

1033 
lemma zdvd_anti_sym: 

1034 
"0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" 

1035 
apply (simp add: dvd_def, auto) 

1036 
apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff) 

1037 
done 

1038 

30042  1039 
lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a" 
23164  1040 
shows "\<bar>a\<bar> = \<bar>b\<bar>" 
1041 
proof 

30042  1042 
from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
1043 
from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 

23164  1044 
from k k' have "a = a*k*k'" by simp 
1045 
with mult_cancel_left1[where c="a" and b="k*k'"] 

30042  1046 
have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc) 
23164  1047 
hence "k = 1 \<and> k' = 1 \<or> k = 1 \<and> k' = 1" by (simp add: zmult_eq_1_iff) 
1048 
thus ?thesis using k k' by auto 

1049 
qed 

1050 

1051 
lemma zdvd_zdiffD: "k dvd m  n ==> k dvd n ==> k dvd (m::int)" 

1052 
apply (subgoal_tac "m = n + (m  n)") 

1053 
apply (erule ssubst) 

30042  1054 
apply (blast intro: dvd_add, simp) 
23164  1055 
done 
1056 

1057 
lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" 

30042  1058 
apply (rule iffI) 
1059 
apply (erule_tac [2] dvd_add) 

1060 
apply (subgoal_tac "n = (n + k * m)  k * m") 

1061 
apply (erule ssubst) 

1062 
apply (erule dvd_diff) 

1063 
apply(simp_all) 

1064 
done 

23164  1065 

1066 
lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n" 

30930  1067 
by (auto elim!: dvdE simp add: mod_mult_mult1) 
23164  1068 

1069 
lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)" 

1070 
apply (subgoal_tac "k dvd n * (m div n) + m mod n") 

1071 
apply (simp add: zmod_zdiv_equality [symmetric]) 

30042  1072 
apply (simp only: dvd_add dvd_mult2) 
23164  1073 
done 
1074 

1075 
lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)" 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1076 
apply (auto elim!: dvdE) 
23164  1077 
apply (subgoal_tac "0 < n") 
1078 
prefer 2 

1079 
apply (blast intro: order_less_trans) 

1080 
apply (simp add: zero_less_mult_iff) 

1081 
apply (subgoal_tac "n * k < n * 1") 

1082 
apply (drule mult_less_cancel_left [THEN iffD1], auto) 

1083 
done 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1084 

23164  1085 
lemma zmult_div_cancel: "(n::int) * (m div n) = m  (m mod n)" 
1086 
using zmod_zdiv_equality[where a="m" and b="n"] 

29667  1087 
by (simp add: algebra_simps) 
23164  1088 

1089 
lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m" 

1090 
apply (subgoal_tac "m mod n = 0") 

1091 
apply (simp add: zmult_div_cancel) 

30042  1092 
apply (simp only: dvd_eq_mod_eq_0) 
23164  1093 
done 
1094 

1095 
lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)" 

1096 
shows "m dvd n" 

1097 
proof 

1098 
from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast 

1099 
{assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp 

1100 
with h have False by (simp add: mult_assoc)} 

1101 
hence "n = m * h" by blast 

29410  1102 
thus ?thesis by simp 
23164  1103 
qed 
1104 

23969  1105 

23164  1106 
theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1107 
apply (simp split add: split_nat) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1108 
apply (rule iffI) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1109 
apply (erule exE) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1110 
apply (rule_tac x = "int x" in exI) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1111 
apply simp 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1112 
apply (erule exE) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1113 
apply (rule_tac x = "nat x" in exI) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1114 
apply (erule conjE) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1115 
apply (erule_tac x = "nat x" in allE) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1116 
apply simp 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1117 
done 
23164  1118 

23365  1119 
theorem zdvd_int: "(x dvd y) = (int x dvd int y)" 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1120 
proof  
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1121 
have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1122 
proof  
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1123 
fix k 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1124 
assume A: "int y = int x * k" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1125 
then show "x dvd y" proof (cases k) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1126 
case (1 n) with A have "y = x * n" by (simp add: zmult_int) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1127 
then show ?thesis .. 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1128 
next 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1129 
case (2 n) with A have "int y = int x * ( int (Suc n))" by simp 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1130 
also have "\<dots> =  (int x * int (Suc n))" by (simp only: mult_minus_right) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1131 
also have "\<dots> =  int (x * Suc n)" by (simp only: zmult_int) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1132 
finally have " int (x * Suc n) = int y" .. 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1133 
then show ?thesis by (simp only: negative_eq_positive) auto 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1134 
qed 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1135 
qed 
30042  1136 
then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult) 
29410  1137 
qed 
23164  1138 

1139 
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)" 

1140 
proof 

30042  1141 
assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp 
23164  1142 
hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int) 
1143 
hence "nat \<bar>x\<bar> = 1" by simp 

1144 
thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto) 

1145 
next 

1146 
assume "\<bar>x\<bar>=1" thus "x dvd 1" 

30042  1147 
by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0) 
23164  1148 
qed 
1149 
lemma zdvd_mult_cancel1: 

1150 
assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)" 

1151 
proof 

1152 
assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 

30042  1153 
by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff) 
23164  1154 
next 
1155 
assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp 

1156 
from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq) 

1157 
qed 

1158 

23365  1159 
lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" 
30042  1160 
unfolding zdvd_int by (cases "z \<ge> 0") simp_all 
23306
cdb027d0637e
add int_of_nat versions of lemmas about int::nat=>int
huffman
parents:
23164
diff
changeset

1161 

23365  1162 
lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" 
30042  1163 
unfolding zdvd_int by (cases "z \<ge> 0") simp_all 
23164  1164 

1165 
lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)" 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26507
diff
changeset

1166 
by (auto simp add: dvd_int_iff) 
23164  1167 

1168 
lemma zdvd_imp_le: "[ z dvd n; 0 < n ] ==> z \<le> (n::int)" 

23365  1169 
apply (rule_tac z=n in int_cases) 
1170 
apply (auto simp add: dvd_int_iff) 

1171 
apply (rule_tac z=z in int_cases) 

23307
2fe3345035c7
modify proofs to avoid referring to int::nat=>int
huffman
parents:
23306
diff
changeset

1172 
apply (auto simp add: dvd_imp_le) 
23164  1173 
done 
1174 

1175 
lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m" 

1176 
apply (induct "y", auto) 

1177 
apply (rule zmod_zmult1_eq [THEN trans]) 

1178 
apply (simp (no_asm_simp)) 

29948  1179 
apply (rule mod_mult_eq [symmetric]) 
23164  1180 
done 
1181 

23365  1182 
lemma zdiv_int: "int (a div b) = (int a) div (int b)" 
23164  1183 
apply (subst split_div, auto) 
1184 
apply (subst split_zdiv, auto) 

23365  1185 
apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient) 
29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

1186 
apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult) 
23164  1187 
done 
1188 

1189 
lemma zmod_int: "int (a mod b) = (int a) mod (int b)" 

23365  1190 
apply (subst split_mod, auto) 
1191 
apply (subst split_zmod, auto) 

1192 
apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 

1193 
in unique_remainder) 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

1194 
apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult) 
23365  1195 
done 
23164  1196 

30180  1197 
lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y" 
1198 
by (unfold dvd_def, cases "y=0", auto simp add: abs_mult) 

1199 

23164  1200 
text{*Suggested by Matthias Daum*} 
1201 
lemma int_power_div_base: 

1202 
"\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m  Suc 0)" 

30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30042
diff
changeset

1203 
apply (subgoal_tac "k ^ m = k ^ ((m  Suc 0) + Suc 0)") 
23164  1204 
apply (erule ssubst) 
1205 
apply (simp only: power_add) 

1206 
apply simp_all 

1207 
done 

1208 

23853  1209 
text {* by Brian Huffman *} 
1210 
lemma zminus_zmod: " ((x::int) mod m) mod m =  x mod m" 

29405
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

1211 
by (rule mod_minus_eq [symmetric]) 
23853  1212 

1213 
lemma zdiff_zmod_left: "(x mod m  y) mod m = (x  y) mod (m::int)" 

29405
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

1214 
by (rule mod_diff_left_eq [symmetric]) 
23853  1215 

1216 
lemma zdiff_zmod_right: "(x  y mod m) mod m = (x  y) mod (m::int)" 

29405
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

1217 
by (rule mod_diff_right_eq [symmetric]) 
23853  1218 

1219 
lemmas zmod_simps = 

30034  1220 
mod_add_left_eq [symmetric] 
1221 
mod_add_right_eq [symmetric] 

30930  1222 
zmod_zmult1_eq [symmetric] 
1223 
mod_mult_left_eq [symmetric] 

1224 
zpower_zmod 

23853  1225 
zminus_zmod zdiff_zmod_left zdiff_zmod_right 
1226 

29045
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1227 
text {* Distributive laws for function @{text nat}. *} 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1228 

3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1229 
lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y" 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1230 
apply (rule linorder_cases [of y 0]) 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1231 
apply (simp add: div_nonneg_neg_le0) 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1232 
apply simp 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1233 
apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int) 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1234 
done 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1235 

3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1236 
(*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*) 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1237 
lemma nat_mod_distrib: 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1238 
"\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y" 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1239 
apply (case_tac "y = 0", simp add: DIVISION_BY_ZERO) 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1240 
apply (simp add: nat_eq_iff zmod_int) 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1241 
done 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1242 

3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1243 
text{*Suggested by Matthias Daum*} 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1244 
lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)" 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1245 
apply (subgoal_tac "nat x div nat k < nat x") 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1246 
apply (simp (asm_lr) add: nat_div_distrib [symmetric]) 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1247 
apply (rule Divides.div_less_dividend, simp_all) 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1248 
done 
3c8f48333731
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
huffman
parents:
28562
diff
changeset

1249 

23853  1250 
text {* code generator setup *} 
23164  1251 

26507  1252 
context ring_1 
1253 
begin 

1254 

28562  1255 
lemma of_int_num [code]: 
26507  1256 
"of_int k = (if k = 0 then 0 else if k < 0 then 
1257 
 of_int ( k) else let 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

1258 
(l, m) = divmod k 2; 
26507  1259 
l' = of_int l 
1260 
in if m = 0 then l' + l' else l' + l' + 1)" 

1261 
proof  

1262 
have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow> 

1263 
of_int k = of_int (k div 2 * 2 + 1)" 

1264 
proof  

1265 
have "k mod 2 < 2" by (auto intro: pos_mod_bound) 

1266 
moreover have "0 \<le> k mod 2" by (auto intro: pos_mod_sign) 

1267 
moreover assume "k mod 2 \<noteq> 0" 

1268 
ultimately have "k mod 2 = 1" by arith 

1269 
moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp 

1270 
ultimately show ?thesis by auto 

1271 
qed 

1272 
have aux2: "\<And>x. of_int 2 * x = x + x" 

1273 
proof  

1274 
fix x 

1275 
have int2: "(2::int) = 1 + 1" by arith 

1276 
show "of_int 2 * x = x + x" 

1277 
unfolding int2 of_int_add left_distrib by simp 

1278 
qed 

1279 
have aux3: "\<And>x. x * of_int 2 = x + x" 

1280 
proof  

1281 
fix x 

1282 
have int2: "(2::int) = 1 + 1" by arith 

1283 
show "x * of_int 2 = x + x" 

1284 
unfolding int2 of_int_add right_distrib by simp 

1285 
qed 

29651
16a19466bf81
slightly adapted towards more uniformity with div/mod on nat
haftmann
parents:
29410
diff
changeset

1286 
from aux1 show ?thesis by (auto simp add: divmod_mod_div Let_def aux2 aux3) 
26507  1287 
qed 
1288 

1289 
end 

1290 

27667
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1291 
lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x  y" 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1292 
proof 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1293 
assume H: "x mod n = y mod n" 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1294 
hence "x mod n  y mod n = 0" by simp 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1295 
hence "(x mod n  y mod n) mod n = 0" by simp 
30034  1296 
hence "(x  y) mod n = 0" by (simp add: mod_diff_eq[symmetric]) 
30042  1297 
thus "n dvd x  y" by (simp add: dvd_eq_mod_eq_0) 
27667
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1298 
next 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1299 
assume H: "n dvd x  y" 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1300 
then obtain k where k: "xy = n*k" unfolding dvd_def by blast 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1301 
hence "x = n*k + y" by simp 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1302 
hence "x mod n = (n*k + y) mod n" by simp 
30034  1303 
thus "x mod n = y mod n" by (simp add: mod_add_left_eq) 
27667
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1304 
qed 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1305 

62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1306 
lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x" 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1307 
shows "\<exists>q. x = y + n * q" 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1308 
proof 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1309 
from xy have th: "int x  int y = int (x  y)" by simp 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1310 
from xyn have "int x mod int n = int y mod int n" 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1311 
by (simp add: zmod_int[symmetric]) 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1312 
hence "int n dvd int x  int y" by (simp only: zmod_eq_dvd_iff[symmetric]) 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1313 
hence "n dvd x  y" by (simp add: th zdvd_int) 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1314 
then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1315 
qed 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1316 

62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1317 
lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1318 
(is "?lhs = ?rhs") 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1319 
proof 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1320 
assume H: "x mod n = y mod n" 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1321 
{assume xy: "x \<le> y" 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1322 
from H have th: "y mod n = x mod n" by simp 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1323 
from nat_mod_eq_lemma[OF th xy] have ?rhs 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1324 
apply clarify apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)} 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1325 
moreover 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1326 
{assume xy: "y \<le> x" 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1327 
from nat_mod_eq_lemma[OF H xy] have ?rhs 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1328 
apply clarify apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)} 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1329 
ultimately show ?rhs using linear[of x y] by blast 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1330 
next 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1331 
assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1332 
hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1333 
thus ?lhs by simp 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1334 
qed 
62500b980749
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
chaieb
parents:
27651
diff
changeset

1335 

29936  1336 

30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30517
diff
changeset

1337 
subsection {* Simproc setup *} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30517
diff
changeset

1338 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30517
diff
changeset

1339 
use "Tools/int_factor_simprocs.ML" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30517
diff
changeset

1340 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30517
diff
changeset

1341 

29936  1342 
subsection {* Code generation *} 
1343 

1344 
definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where 

1345 
"pdivmod k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)" 

1346 

1347 
lemma pdivmod_posDivAlg [code]: 

1348 
"pdivmod k l = (if l = 0 then (0, \<bar>k\<bar>) else posDivAlg \<bar>k\<bar> \<bar>l\<bar>)" 

1349 
by (subst posDivAlg_div_mod) (simp_all add: pdivmod_def) 

1350 

1351 
lemma divmod_pdivmod: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else 

1352 
apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 

1353 
then pdivmod k l 

1354 
else (let (r, s) = pdivmod k l in 

1355 
if s = 0 then ( r, 0) else ( r  1, \<bar>l\<bar>  s))))" 

1356 
proof  

1357 
have aux: "\<And>q::int.  k = l * q \<longleftrightarrow> k = l *  q" by auto 

1358 
show ?thesis 

1359 
by (simp add: divmod_mod_div pdivmod_def) 

1360 
(auto simp add: aux not_less not_le zdiv_zminus1_eq_if 

1361 
zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if) 

1362 
qed 

1363 

1364 
lemma divmod_code [code]: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else 

1365 
apsnd ((op *) (sgn l)) (if sgn k = sgn l 

1366 
then pdivmod k l 

1367 
else (let (r, s) = pdivmod k l in 

1368 
if s = 0 then ( r, 0) else ( r  1, \<bar>l\<bar>  s))))" 

1369 
proof  

1370 
have "k \<noteq> 0 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 \<longleftrightarrow> sgn k = sgn l" 

1371 
by (auto simp add: not_less sgn_if) 

1372 
then show ?thesis by (simp add: divmod_pdivmod) 

1373 
qed 

1374 

23164  1375 
code_modulename SML 
1376 
IntDiv Integer 

1377 

1378 
code_modulename OCaml 

1379 
IntDiv Integer 

1380 

1381 
code_modulename Haskell 

24195  1382 
IntDiv Integer 
23164  1383 

1384 
end 