author  haftmann 
Sun, 16 Oct 2016 09:31:03 +0200  
changeset 64238  b60a9752b6d0 
parent 64164  38c407446400 
child 64240  eabf80376aab 
permissions  rwrr 
3366  1 
(* Title: HOL/Divides.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset

3 
Copyright 1999 University of Cambridge 
18154  4 
*) 
3366  5 

60758  6 
section \<open>The division operators div and mod\<close> 
3366  7 

15131  8 
theory Divides 
58778
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

9 
imports Parity 
15131  10 
begin 
3366  11 

60758  12 
subsection \<open>Abstract division in commutative semirings.\<close> 
25942  13 

64164
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64014
diff
changeset

14 
class semiring_div = semidom + semiring_modulo + 
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64014
diff
changeset

15 
assumes div_by_0: "a div 0 = 0" 
63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

16 
and div_0: "0 div a = 0" 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

17 
and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b" 
30930  18 
and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b" 
25942  19 
begin 
20 

60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

21 
subclass algebraic_semidom 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

22 
proof 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

23 
fix b a 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

24 
assume "b \<noteq> 0" 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

25 
then show "a * b div b = a" 
63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

26 
using div_mult_self1 [of b 0 a] by (simp add: ac_simps div_0) 
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

27 
qed (simp add: div_by_0) 
58953  28 

60867  29 
lemma div_by_1: 
30 
"a div 1 = a" 

31 
by (fact divide_1) 

32 

33 
lemma div_mult_self1_is_id: 

34 
"b \<noteq> 0 \<Longrightarrow> b * a div b = a" 

35 
by (fact nonzero_mult_divide_cancel_left) 

36 

37 
lemma div_mult_self2_is_id: 

38 
"b \<noteq> 0 \<Longrightarrow> a * b div b = a" 

39 
by (fact nonzero_mult_divide_cancel_right) 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

40 

63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

41 
text \<open>@{const divide} and @{const modulo}\<close> 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

42 

26062  43 
lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c" 
30934  44 
by (simp add: mod_div_equality) 
26062  45 

46 
lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c" 

30934  47 
by (simp add: mod_div_equality2) 
26062  48 

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

49 
lemma mod_by_0 [simp]: "a mod 0 = a" 
30934  50 
using mod_div_equality [of a zero] by simp 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

51 

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

52 
lemma mod_0 [simp]: "0 mod a = 0" 
30934  53 
using mod_div_equality [of zero a] div_0 by simp 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

54 

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

55 
lemma div_mult_self2 [simp]: 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

56 
assumes "b \<noteq> 0" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

57 
shows "(a + b * c) div b = c + a div b" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

58 
using assms div_mult_self1 [of b a c] by (simp add: mult.commute) 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

59 

54221  60 
lemma div_mult_self3 [simp]: 
61 
assumes "b \<noteq> 0" 

62 
shows "(c * b + a) div b = c + a div b" 

63 
using assms by (simp add: add.commute) 

64 

65 
lemma div_mult_self4 [simp]: 

66 
assumes "b \<noteq> 0" 

67 
shows "(b * c + a) div b = c + a div b" 

68 
using assms by (simp add: add.commute) 

69 

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

70 
lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

71 
proof (cases "b = 0") 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

72 
case True then show ?thesis by simp 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

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

74 
case False 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

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

76 
by (simp add: mod_div_equality) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

77 
also from False div_mult_self1 [of b a c] have 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

78 
"\<dots> = (c + a div b) * b + (a + c * b) mod b" 
29667  79 
by (simp add: algebra_simps) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

80 
finally have "a = a div b * b + (a + c * b) mod b" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

81 
by (simp add: add.commute [of a] add.assoc distrib_right) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

82 
then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

83 
by (simp add: mod_div_equality) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

84 
then show ?thesis by simp 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

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

86 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

87 
lemma mod_mult_self2 [simp]: 
54221  88 
"(a + b * c) mod b = a mod b" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

89 
by (simp add: mult.commute [of b]) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

90 

54221  91 
lemma mod_mult_self3 [simp]: 
92 
"(c * b + a) mod b = a mod b" 

93 
by (simp add: add.commute) 

94 

95 
lemma mod_mult_self4 [simp]: 

96 
"(b * c + a) mod b = a mod b" 

97 
by (simp add: add.commute) 

98 

60867  99 
lemma mod_mult_self1_is_0 [simp]: 
100 
"b * a mod b = 0" 

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

101 
using mod_mult_self2 [of 0 b a] by simp 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

102 

60867  103 
lemma mod_mult_self2_is_0 [simp]: 
104 
"a * b mod b = 0" 

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

105 
using mod_mult_self1 [of 0 a b] by simp 
26062  106 

60867  107 
lemma mod_by_1 [simp]: 
108 
"a mod 1 = 0" 

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

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

110 
from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

111 
then have "a + a mod 1 = a + 0" by simp 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

112 
then show ?thesis by (rule add_left_imp_eq) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

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

114 

60867  115 
lemma mod_self [simp]: 
116 
"a mod a = 0" 

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

117 
using mod_mult_self2_is_0 [of 1] by simp 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

118 

63499
9c9a59949887
Tuned looping simp rules in semiring_div
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset

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

120 
assumes "b \<noteq> 0" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

121 
shows "(b + a) div b = a div b + 1" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

122 
using assms div_mult_self1 [of b a 1] by (simp add: add.commute) 
26062  123 

63499
9c9a59949887
Tuned looping simp rules in semiring_div
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset

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

125 
assumes "b \<noteq> 0" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

126 
shows "(a + b) div b = a div b + 1" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

127 
using assms div_add_self1 [of b a] by (simp add: add.commute) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

128 

27676  129 
lemma mod_add_self1 [simp]: 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

130 
"(b + a) mod b = a mod b" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

131 
using mod_mult_self1 [of a 1 b] by (simp add: add.commute) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

132 

27676  133 
lemma mod_add_self2 [simp]: 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

134 
"(a + b) mod b = a mod b" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

135 
using mod_mult_self1 [of a 1 b] by simp 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset

136 

58834  137 
lemma dvd_imp_mod_0 [simp]: 
138 
assumes "a dvd b" 

139 
shows "b mod a = 0" 

140 
proof  

141 
from assms obtain c where "b = a * c" .. 

142 
then have "b mod a = a * c mod a" by simp 

143 
then show "b mod a = 0" by simp 

144 
qed 

58911
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

145 

2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

146 
lemma mod_eq_0_iff_dvd: 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

147 
"a mod b = 0 \<longleftrightarrow> b dvd a" 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

148 
proof 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

149 
assume "b dvd a" 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

150 
then show "a mod b = 0" by simp 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

151 
next 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

152 
assume "a mod b = 0" 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

153 
with mod_div_equality [of a b] have "a div b * b = a" by simp 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

154 
then have "a = b * (a div b)" by (simp add: ac_simps) 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

155 
then show "b dvd a" .. 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

156 
qed 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

157 

60867  158 
lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]: 
58834  159 
"a dvd b \<longleftrightarrow> b mod a = 0" 
58911
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

160 
by (simp add: mod_eq_0_iff_dvd) 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

161 

2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

162 
lemma mod_div_trivial [simp]: 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

163 
"a mod b div b = 0" 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

164 
proof (cases "b = 0") 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

165 
assume "b = 0" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

166 
thus ?thesis by simp 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

167 
next 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

168 
assume "b \<noteq> 0" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

169 
hence "a div b + a mod b div b = (a mod b + a div b * b) div b" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

170 
by (rule div_mult_self1 [symmetric]) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

171 
also have "\<dots> = a div b" 
64164
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64014
diff
changeset

172 
by (simp only: mod_div_equality3) 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

173 
also have "\<dots> = a div b + 0" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

174 
by simp 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

175 
finally show ?thesis 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

176 
by (rule add_left_imp_eq) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

177 
qed 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

178 

58911
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

179 
lemma mod_mod_trivial [simp]: 
2cf595ee508b
proper oriented equivalence of dvd predicate and mod
haftmann
parents:
58889
diff
changeset

180 
"a mod b mod b = a mod b" 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

181 
proof  
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

182 
have "a mod b mod b = (a mod b + a div b * b) mod b" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

183 
by (simp only: mod_mult_self1) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

184 
also have "\<dots> = a mod b" 
64164
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64014
diff
changeset

185 
by (simp only: mod_div_equality3) 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

186 
finally show ?thesis . 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

187 
qed 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

188 

58834  189 
lemma dvd_mod_imp_dvd: 
190 
assumes "k dvd m mod n" and "k dvd n" 

191 
shows "k dvd m" 

192 
proof  

193 
from assms have "k dvd (m div n) * n + m mod n" 

194 
by (simp only: dvd_add dvd_mult) 

195 
then show ?thesis by (simp add: mod_div_equality) 

196 
qed 

30078
beee83623cc9
move lemma dvd_mod_imp_dvd into class semiring_div
huffman
parents:
30052
diff
changeset

197 

60758  198 
text \<open>Addition respects modular equivalence.\<close> 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

199 

61799  200 
lemma mod_add_left_eq: \<comment> \<open>FIXME reorient\<close> 
60867  201 
"(a + b) mod c = (a mod c + b) mod c" 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

202 
proof  
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

203 
have "(a + b) mod c = (a div c * c + a mod c + b) mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

204 
by (simp only: mod_div_equality) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

205 
also have "\<dots> = (a mod c + b + a div c * c) mod c" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

206 
by (simp only: ac_simps) 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

207 
also have "\<dots> = (a mod c + b) mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

208 
by (rule mod_mult_self1) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

209 
finally show ?thesis . 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

210 
qed 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

211 

61799  212 
lemma mod_add_right_eq: \<comment> \<open>FIXME reorient\<close> 
60867  213 
"(a + b) mod c = (a + b mod c) mod c" 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

214 
proof  
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

215 
have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

216 
by (simp only: mod_div_equality) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

217 
also have "\<dots> = (a + b mod c + b div c * c) mod c" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

218 
by (simp only: ac_simps) 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

219 
also have "\<dots> = (a + b mod c) mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

220 
by (rule mod_mult_self1) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

221 
finally show ?thesis . 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

222 
qed 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

223 

61799  224 
lemma mod_add_eq: \<comment> \<open>FIXME reorient\<close> 
60867  225 
"(a + b) mod c = (a mod c + b mod c) mod c" 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

226 
by (rule trans [OF mod_add_left_eq mod_add_right_eq]) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

227 

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

228 
lemma mod_add_cong: 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

229 
assumes "a mod c = a' mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

230 
assumes "b mod c = b' mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

231 
shows "(a + b) mod c = (a' + b') mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

232 
proof  
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

233 
have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

234 
unfolding assms .. 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

235 
thus ?thesis 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

236 
by (simp only: mod_add_eq [symmetric]) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

237 
qed 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

238 

60758  239 
text \<open>Multiplication respects modular equivalence.\<close> 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

240 

61799  241 
lemma mod_mult_left_eq: \<comment> \<open>FIXME reorient\<close> 
60867  242 
"(a * b) mod c = ((a mod c) * b) mod c" 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

243 
proof  
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

244 
have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

245 
by (simp only: mod_div_equality) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

246 
also have "\<dots> = (a mod c * b + a div c * b * c) mod c" 
29667  247 
by (simp only: algebra_simps) 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

248 
also have "\<dots> = (a mod c * b) mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

249 
by (rule mod_mult_self1) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

250 
finally show ?thesis . 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

251 
qed 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

252 

61799  253 
lemma mod_mult_right_eq: \<comment> \<open>FIXME reorient\<close> 
60867  254 
"(a * b) mod c = (a * (b mod c)) mod c" 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

255 
proof  
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

256 
have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

257 
by (simp only: mod_div_equality) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

258 
also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c" 
29667  259 
by (simp only: algebra_simps) 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

260 
also have "\<dots> = (a * (b mod c)) mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

261 
by (rule mod_mult_self1) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

262 
finally show ?thesis . 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

263 
qed 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

264 

61799  265 
lemma mod_mult_eq: \<comment> \<open>FIXME reorient\<close> 
60867  266 
"(a * b) mod c = ((a mod c) * (b mod c)) mod c" 
29403
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

267 
by (rule trans [OF mod_mult_left_eq mod_mult_right_eq]) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

268 

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

269 
lemma mod_mult_cong: 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

270 
assumes "a mod c = a' mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

271 
assumes "b mod c = b' mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

272 
shows "(a * b) mod c = (a' * b') mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

273 
proof  
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

274 
have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c" 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

275 
unfolding assms .. 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

276 
thus ?thesis 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

277 
by (simp only: mod_mult_eq [symmetric]) 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

278 
qed 
fe17df4e4ab3
generalize some div/mod lemmas; remove typespecific proofs
huffman
parents:
29252
diff
changeset

279 

60758  280 
text \<open>Exponentiation respects modular equivalence.\<close> 
47164  281 

60867  282 
lemma power_mod: "(a mod b) ^ n mod b = a ^ n mod b" 
47164  283 
apply (induct n, simp_all) 
284 
apply (rule mod_mult_right_eq [THEN trans]) 

285 
apply (simp (no_asm_simp)) 

286 
apply (rule mod_mult_eq [symmetric]) 

287 
done 

288 

29404  289 
lemma mod_mod_cancel: 
290 
assumes "c dvd b" 

291 
shows "a mod b mod c = a mod c" 

292 
proof  

60758  293 
from \<open>c dvd b\<close> obtain k where "b = c * k" 
29404  294 
by (rule dvdE) 
295 
have "a mod b mod c = a mod (c * k) mod c" 

60758  296 
by (simp only: \<open>b = c * k\<close>) 
29404  297 
also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c" 
298 
by (simp only: mod_mult_self1) 

299 
also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c" 

58786  300 
by (simp only: ac_simps) 
29404  301 
also have "\<dots> = a mod c" 
302 
by (simp only: mod_div_equality) 

303 
finally show ?thesis . 

304 
qed 

305 

30930  306 
lemma div_mult_mult2 [simp]: 
307 
"c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

308 
by (drule div_mult_mult1) (simp add: mult.commute) 
30930  309 

310 
lemma div_mult_mult1_if [simp]: 

311 
"(c * a) div (c * b) = (if c = 0 then 0 else a div b)" 

312 
by simp_all 

30476  313 

30930  314 
lemma mod_mult_mult1: 
315 
"(c * a) mod (c * b) = c * (a mod b)" 

316 
proof (cases "c = 0") 

317 
case True then show ?thesis by simp 

318 
next 

319 
case False 

320 
from mod_div_equality 

321 
have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" . 

322 
with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b) 

323 
= c * a + c * (a mod b)" by (simp add: algebra_simps) 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

324 
with mod_div_equality show ?thesis by simp 
30930  325 
qed 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

326 

30930  327 
lemma mod_mult_mult2: 
328 
"(a * c) mod (b * c) = (a mod b) * c" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

329 
using mod_mult_mult1 [of c a b] by (simp add: mult.commute) 
30930  330 

47159  331 
lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)" 
332 
by (fact mod_mult_mult2 [symmetric]) 

333 

334 
lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)" 

335 
by (fact mod_mult_mult1 [symmetric]) 

336 

31662
57f7ef0dba8e
generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
huffman
parents:
31661
diff
changeset

337 
lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)" 
57f7ef0dba8e
generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
huffman
parents:
31661
diff
changeset

338 
unfolding dvd_def by (auto simp add: mod_mult_mult1) 
57f7ef0dba8e
generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
huffman
parents:
31661
diff
changeset

339 

57f7ef0dba8e
generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
huffman
parents:
31661
diff
changeset

340 
lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m" 
57f7ef0dba8e
generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
huffman
parents:
31661
diff
changeset

341 
by (blast intro: dvd_mod_imp_dvd dvd_mod) 
57f7ef0dba8e
generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
huffman
parents:
31661
diff
changeset

342 

63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

343 
lemma div_div_eq_right: 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

344 
assumes "c dvd b" "b dvd a" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

345 
shows "a div (b div c) = a div b * c" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

346 
proof  
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

347 
from assms have "a div b * c = (a * c) div b" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

348 
by (subst dvd_div_mult) simp_all 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

349 
also from assms have "\<dots> = (a * c) div ((b div c) * c)" by simp 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

350 
also have "a * c div (b div c * c) = a div (b div c)" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

351 
by (cases "c = 0") simp_all 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

352 
finally show ?thesis .. 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

353 
qed 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

354 

ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

355 
lemma div_div_div_same: 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

356 
assumes "d dvd a" "d dvd b" "b dvd a" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

357 
shows "(a div d) div (b div d) = a div b" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

358 
using assms by (subst dvd_div_mult2_eq [symmetric]) simp_all 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

359 

31661
1e252b8b2334
move lemma div_power into semiring_div context; class ring_div inherits from idom
huffman
parents:
31009
diff
changeset

360 
end 
1e252b8b2334
move lemma div_power into semiring_div context; class ring_div inherits from idom
huffman
parents:
31009
diff
changeset

361 

59833
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59816
diff
changeset

362 
class ring_div = comm_ring_1 + semiring_div 
29405
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

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

364 

60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

365 
subclass idom_divide .. 
36634  366 

60758  367 
text \<open>Negation respects modular equivalence.\<close> 
29405
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

368 

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

369 
lemma mod_minus_eq: "( a) mod b = ( (a mod b)) mod b" 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

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

371 
have "( a) mod b = ( (a div b * b + a mod b)) mod b" 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

372 
by (simp only: mod_div_equality) 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

373 
also have "\<dots> = ( (a mod b) +  (a div b) * b) mod b" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

374 
by (simp add: ac_simps) 
29405
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

375 
also have "\<dots> = ( (a mod b)) mod b" 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

376 
by (rule mod_mult_self1) 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

377 
finally show ?thesis . 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

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

379 

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

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

381 
assumes "a mod b = a' mod b" 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

382 
shows "( a) mod b = ( a') mod b" 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

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

384 
have "( (a mod b)) mod b = ( (a' mod b)) mod b" 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

385 
unfolding assms .. 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

386 
thus ?thesis 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

387 
by (simp only: mod_minus_eq [symmetric]) 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

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

389 

60758  390 
text \<open>Subtraction respects modular equivalence.\<close> 
29405
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

391 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

392 
lemma mod_diff_left_eq: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

393 
"(a  b) mod c = (a mod c  b) mod c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

394 
using mod_add_cong [of a c "a mod c" " b" " b"] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

395 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

396 
lemma mod_diff_right_eq: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

397 
"(a  b) mod c = (a  b mod c) mod c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

398 
using mod_add_cong [of a c a " b" " (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

399 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

400 
lemma mod_diff_eq: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

401 
"(a  b) mod c = (a mod c  b mod c) mod c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

402 
using mod_add_cong [of a c "a mod c" " b" " (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp 
29405
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

403 

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

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

405 
assumes "a mod c = a' mod c" 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

406 
assumes "b mod c = b' mod c" 
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

407 
shows "(a  b) mod c = (a'  b') mod c" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

408 
using assms mod_add_cong [of a c a' " b" " b'"] mod_minus_cong [of b c "b'"] by simp 
29405
98ab21b14f09
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman
parents:
29404
diff
changeset

409 

30180  410 
lemma dvd_neg_div: "y dvd x \<Longrightarrow> x div y =  (x div y)" 
411 
apply (case_tac "y = 0") apply simp 

412 
apply (auto simp add: dvd_def) 

413 
apply (subgoal_tac "(y * k) = y *  k") 

57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
55440
diff
changeset

414 
apply (simp only:) 
30180  415 
apply (erule div_mult_self1_is_id) 
416 
apply simp 

417 
done 

418 

419 
lemma dvd_div_neg: "y dvd x \<Longrightarrow> x div y =  (x div y)" 

420 
apply (case_tac "y = 0") apply simp 

421 
apply (auto simp add: dvd_def) 

422 
apply (subgoal_tac "y * k = y * k") 

57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
55440
diff
changeset

423 
apply (erule ssubst, rule div_mult_self1_is_id) 
30180  424 
apply simp 
425 
apply simp 

426 
done 

427 

60867  428 
lemma div_diff [simp]: 
429 
"z dvd x \<Longrightarrow> z dvd y \<Longrightarrow> (x  y) div z = x div z  y div z" 

430 
using div_add [of _ _ " y"] by (simp add: dvd_neg_div) 

59380  431 

47159  432 
lemma div_minus_minus [simp]: "(a) div (b) = a div b" 
433 
using div_mult_mult1 [of " 1" a b] 

434 
unfolding neg_equal_0_iff_equal by simp 

435 

436 
lemma mod_minus_minus [simp]: "(a) mod (b) =  (a mod b)" 

437 
using mod_mult_mult1 [of " 1" a b] by simp 

438 

439 
lemma div_minus_right: "a div (b) = (a) div b" 

440 
using div_minus_minus [of "a" b] by simp 

441 

442 
lemma mod_minus_right: "a mod (b) =  ((a) mod b)" 

443 
using mod_minus_minus [of "a" b] by simp 

444 

47160  445 
lemma div_minus1_right [simp]: "a div (1) = a" 
446 
using div_minus_right [of a 1] by simp 

447 

448 
lemma mod_minus1_right [simp]: "a mod (1) = 0" 

449 
using mod_minus_right [of a 1] by simp 

450 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

451 
lemma minus_mod_self2 [simp]: 
54221  452 
"(a  b) mod b = a mod b" 
453 
by (simp add: mod_diff_right_eq) 

454 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

455 
lemma minus_mod_self1 [simp]: 
54221  456 
"(b  a) mod b =  a mod b" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54227
diff
changeset

457 
using mod_add_self2 [of " a" b] by simp 
54221  458 

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

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

460 

58778
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

461 

60758  462 
subsubsection \<open>Parity and division\<close> 
58778
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

463 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

464 
class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral + 
54226
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

465 
assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1" 
58786  466 
assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1" 
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58646
diff
changeset

467 
assumes zero_not_eq_two: "0 \<noteq> 2" 
54226
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

468 
begin 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

469 

e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

470 
lemma parity_cases [case_names even odd]: 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

471 
assumes "a mod 2 = 0 \<Longrightarrow> P" 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

472 
assumes "a mod 2 = 1 \<Longrightarrow> P" 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

473 
shows P 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

474 
using assms parity by blast 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

475 

58786  476 
lemma one_div_two_eq_zero [simp]: 
58778
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

477 
"1 div 2 = 0" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

478 
proof (cases "2 = 0") 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

479 
case True then show ?thesis by simp 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

480 
next 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

481 
case False 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

482 
from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" . 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

483 
with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp 
58953  484 
then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff) 
485 
then have "1 div 2 = 0 \<or> 2 = 0" by simp 

58778
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

486 
with False show ?thesis by auto 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

487 
qed 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

488 

58786  489 
lemma not_mod_2_eq_0_eq_1 [simp]: 
490 
"a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1" 

491 
by (cases a rule: parity_cases) simp_all 

492 

493 
lemma not_mod_2_eq_1_eq_0 [simp]: 

494 
"a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0" 

495 
by (cases a rule: parity_cases) simp_all 

496 

58778
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

497 
subclass semiring_parity 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

498 
proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1) 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

499 
show "1 mod 2 = 1" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

500 
by (fact one_mod_two_eq_one) 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

501 
next 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

502 
fix a b 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

503 
assume "a mod 2 = 1" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

504 
moreover assume "b mod 2 = 1" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

505 
ultimately show "(a + b) mod 2 = 0" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

506 
using mod_add_eq [of a b 2] by simp 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

507 
next 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

508 
fix a b 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

509 
assume "(a * b) mod 2 = 0" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

510 
then have "(a mod 2) * (b mod 2) = 0" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

511 
by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2]) 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

512 
then show "a mod 2 = 0 \<or> b mod 2 = 0" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

513 
by (rule divisors_zero) 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

514 
next 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

515 
fix a 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

516 
assume "a mod 2 = 1" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

517 
then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

518 
then show "\<exists>b. a = b + 1" .. 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

519 
qed 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

520 

e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

521 
lemma even_iff_mod_2_eq_zero: 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

522 
"even a \<longleftrightarrow> a mod 2 = 0" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

523 
by (fact dvd_eq_mod_eq_0) 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

524 

64014  525 
lemma odd_iff_mod_2_eq_one: 
526 
"odd a \<longleftrightarrow> a mod 2 = 1" 

527 
by (auto simp add: even_iff_mod_2_eq_zero) 

528 

58778
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

529 
lemma even_succ_div_two [simp]: 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

530 
"even a \<Longrightarrow> (a + 1) div 2 = a div 2" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

531 
by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero) 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

532 

e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

533 
lemma odd_succ_div_two [simp]: 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

534 
"odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

535 
by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc) 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

536 

e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

537 
lemma even_two_times_div_two: 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

538 
"even a \<Longrightarrow> 2 * (a div 2) = a" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

539 
by (fact dvd_mult_div_cancel) 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

540 

58834  541 
lemma odd_two_times_div_two_succ [simp]: 
58778
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

542 
"odd a \<Longrightarrow> 2 * (a div 2) + 1 = a" 
e29cae8eab1f
even further downshift of theory Parity in the hierarchy
haftmann
parents:
58710
diff
changeset

543 
using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero) 
60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60867
diff
changeset

544 

54226
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

545 
end 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

546 

25942  547 

60758  548 
subsection \<open>Generic numeral division with a pragmatic type class\<close> 
549 

550 
text \<open> 

53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

551 
The following type class contains everything necessary to formulate 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

552 
a division algorithm in ring structures with numerals, restricted 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

553 
to its positive segments. This is its primary motiviation, and it 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

554 
could surely be formulated using a more finegrained, more algebraic 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

555 
and less technical class hierarchy. 
60758  556 
\<close> 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

557 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

558 
class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom + 
59816
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59807
diff
changeset

559 
assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0" 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

560 
and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

561 
and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

562 
and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

563 
and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

564 
and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

565 
and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

566 
and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

567 
assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b" 
61275
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

568 
fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a" 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

569 
and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a" 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

570 
assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)" 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

571 
and divmod_step_def: "divmod_step l qr = (let (q, r) = qr 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

572 
in if r \<ge> numeral l then (2 * q + 1, r  numeral l) 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

573 
else (2 * q, r))" 
61799  574 
\<comment> \<open>These are conceptually definitions but force generated code 
61275
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

575 
to be monomorphic wrt. particular instances of this class which 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

576 
yields a significant speedup.\<close> 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

577 

53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

578 
begin 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

579 

59816
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59807
diff
changeset

580 
lemma mult_div_cancel: 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59807
diff
changeset

581 
"b * (a div b) = a  a mod b" 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59807
diff
changeset

582 
proof  
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59807
diff
changeset

583 
have "b * (a div b) + a mod b = a" 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59807
diff
changeset

584 
using mod_div_equality [of a b] by (simp add: ac_simps) 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59807
diff
changeset

585 
then have "b * (a div b) + a mod b  a mod b = a  a mod b" 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59807
diff
changeset

586 
by simp 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59807
diff
changeset

587 
then show ?thesis 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59807
diff
changeset

588 
by simp 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59807
diff
changeset

589 
qed 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

590 

54226
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

591 
subclass semiring_div_parity 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

592 
proof 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

593 
fix a 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

594 
show "a mod 2 = 0 \<or> a mod 2 = 1" 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

595 
proof (rule ccontr) 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

596 
assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)" 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

597 
then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

598 
have "0 < 2" by simp 
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

599 
with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all 
60758  600 
with \<open>a mod 2 \<noteq> 0\<close> have "0 < a mod 2" by simp 
54226
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

601 
with discrete have "1 \<le> a mod 2" by simp 
60758  602 
with \<open>a mod 2 \<noteq> 1\<close> have "1 < a mod 2" by simp 
54226
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

603 
with discrete have "2 \<le> a mod 2" by simp 
60758  604 
with \<open>a mod 2 < 2\<close> show False by simp 
54226
e3df2a4e02fc
explicit type class for modelling even/odd parity
haftmann
parents:
54221
diff
changeset

605 
qed 
58646
cd63a4b12a33
specialized specification: avoid trivial instances
haftmann
parents:
58511
diff
changeset

606 
next 
cd63a4b12a33
specialized specification: avoid trivial instances
haftmann
parents:
58511
diff
changeset

607 
show "1 mod 2 = 1" 
cd63a4b12a33
specialized specification: avoid trivial instances
haftmann
parents:
58511
diff
changeset

608 
by (rule mod_less) simp_all 
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58646
diff
changeset

609 
next 
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58646
diff
changeset

610 
show "0 \<noteq> 2" 
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58646
diff
changeset

611 
by simp 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

612 
qed 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

613 

ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

614 
lemma divmod_digit_1: 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

615 
assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

616 
shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P") 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

617 
and "a mod (2 * b)  b = a mod b" (is "?Q") 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

618 
proof  
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

619 
from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

620 
by (auto intro: trans) 
60758  621 
with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive) 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

622 
then have [simp]: "1 \<le> a div b" by (simp add: discrete) 
60758  623 
with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound) 
63040  624 
define w where "w = a div b mod 2" 
625 
with parity have w_exhaust: "w = 0 \<or> w = 1" by auto 

53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

626 
have mod_w: "a mod (2 * b) = a mod b + b * w" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

627 
by (simp add: w_def mod_mult2_eq ac_simps) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

628 
from assms w_exhaust have "w = 1" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

629 
by (auto simp add: mod_w) (insert mod_less, auto) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

630 
with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

631 
have "2 * (a div (2 * b)) = a div b  w" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

632 
by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps) 
60758  633 
with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b  1" by simp 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

634 
then show ?P and ?Q 
60867  635 
by (simp_all add: div mod add_implies_diff [symmetric]) 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

636 
qed 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

637 

ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

638 
lemma divmod_digit_0: 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

639 
assumes "0 < b" and "a mod (2 * b) < b" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

640 
shows "2 * (a div (2 * b)) = a div b" (is "?P") 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

641 
and "a mod (2 * b) = a mod b" (is "?Q") 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

642 
proof  
63040  643 
define w where "w = a div b mod 2" 
644 
with parity have w_exhaust: "w = 0 \<or> w = 1" by auto 

53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

645 
have mod_w: "a mod (2 * b) = a mod b + b * w" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

646 
by (simp add: w_def mod_mult2_eq ac_simps) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

647 
moreover have "b \<le> a mod b + b" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

648 
proof  
60758  649 
from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

650 
then have "0 + b \<le> a mod b + b" by (rule add_right_mono) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

651 
then show ?thesis by simp 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

652 
qed 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

653 
moreover note assms w_exhaust 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

654 
ultimately have "w = 0" by auto 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

655 
with mod_w have mod: "a mod (2 * b) = a mod b" by simp 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

656 
have "2 * (a div (2 * b)) = a div b  w" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

657 
by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps) 
60758  658 
with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

659 
then show ?P and ?Q 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

660 
by (simp_all add: div mod) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

661 
qed 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

662 

60867  663 
lemma fst_divmod: 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

664 
"fst (divmod m n) = numeral m div numeral n" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

665 
by (simp add: divmod_def) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

666 

60867  667 
lemma snd_divmod: 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

668 
"snd (divmod m n) = numeral m mod numeral n" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

669 
by (simp add: divmod_def) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

670 

60758  671 
text \<open> 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

672 
This is a formulation of one step (referring to one digit position) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

673 
in schoolmethod division: compare the dividend at the current 
53070  674 
digit position with the remainder from previous division steps 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

675 
and evaluate accordingly. 
60758  676 
\<close> 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

677 

61275
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

678 
lemma divmod_step_eq [simp]: 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

679 
"divmod_step l (q, r) = (if numeral l \<le> r 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

680 
then (2 * q + 1, r  numeral l) else (2 * q, r))" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

681 
by (simp add: divmod_step_def) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

682 

60758  683 
text \<open> 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

684 
This is a formulation of schoolmethod division. 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

685 
If the divisor is smaller than the dividend, terminate. 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

686 
If not, shift the dividend to the right until termination 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

687 
occurs and then reiterate single division steps in the 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

688 
opposite direction. 
60758  689 
\<close> 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

690 

60867  691 
lemma divmod_divmod_step: 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

692 
"divmod m n = (if m < n then (0, numeral m) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

693 
else divmod_step n (divmod m (Num.Bit0 n)))" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

694 
proof (cases "m < n") 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

695 
case True then have "numeral m < numeral n" by simp 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

696 
then show ?thesis 
60867  697 
by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod) 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

698 
next 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

699 
case False 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

700 
have "divmod m n = 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

701 
divmod_step n (numeral m div (2 * numeral n), 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

702 
numeral m mod (2 * numeral n))" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

703 
proof (cases "numeral n \<le> numeral m mod (2 * numeral n)") 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

704 
case True 
60867  705 
with divmod_step_eq 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

706 
have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) = 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

707 
(2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n)  numeral n)" 
60867  708 
by simp 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

709 
moreover from True divmod_digit_1 [of "numeral m" "numeral n"] 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

710 
have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

711 
and "numeral m mod (2 * numeral n)  numeral n = numeral m mod numeral n" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

712 
by simp_all 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

713 
ultimately show ?thesis by (simp only: divmod_def) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

714 
next 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

715 
case False then have *: "numeral m mod (2 * numeral n) < numeral n" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

716 
by (simp add: not_le) 
60867  717 
with divmod_step_eq 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

718 
have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) = 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

719 
(2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))" 
60867  720 
by auto 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

721 
moreover from * divmod_digit_0 [of "numeral n" "numeral m"] 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

722 
have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

723 
and "numeral m mod (2 * numeral n) = numeral m mod numeral n" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

724 
by (simp_all only: zero_less_numeral) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

725 
ultimately show ?thesis by (simp only: divmod_def) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

726 
qed 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

727 
then have "divmod m n = 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

728 
divmod_step n (numeral m div numeral (Num.Bit0 n), 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

729 
numeral m mod numeral (Num.Bit0 n))" 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

730 
by (simp only: numeral.simps distrib mult_1) 
53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

731 
then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))" 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

732 
by (simp add: divmod_def) 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

733 
with False show ?thesis by simp 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

734 
qed 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

735 

61799  736 
text \<open>The division rewrite proper  first, trivial results involving \<open>1\<close>\<close> 
60867  737 

61275
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

738 
lemma divmod_trivial [simp]: 
60867  739 
"divmod Num.One Num.One = (numeral Num.One, 0)" 
740 
"divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)" 

741 
"divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)" 

742 
"divmod num.One (num.Bit0 n) = (0, Numeral1)" 

743 
"divmod num.One (num.Bit1 n) = (0, Numeral1)" 

744 
using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def) 

745 

746 
text \<open>Division by an even number is a rightshift\<close> 

58953  747 

61275
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

748 
lemma divmod_cancel [simp]: 
53069
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
53068
diff
changeset

749 
"divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P) 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
53068
diff
changeset

750 
"divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q) 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
53068
diff
changeset

751 
proof  
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
53068
diff
changeset

752 
have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q" 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
53068
diff
changeset

753 
"\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1" 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
53068
diff
changeset

754 
by (simp_all only: numeral_mult numeral.simps distrib) simp_all 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
53068
diff
changeset

755 
have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less) 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
53068
diff
changeset

756 
then show ?P and ?Q 
60867  757 
by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1 
758 
div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] 

759 
add.commute del: numeral_times_numeral) 

58953  760 
qed 
761 

60867  762 
text \<open>The really hard work\<close> 
763 

61275
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

764 
lemma divmod_steps [simp]: 
60867  765 
"divmod (num.Bit0 m) (num.Bit1 n) = 
766 
(if m \<le> n then (0, numeral (num.Bit0 m)) 

767 
else divmod_step (num.Bit1 n) 

768 
(divmod (num.Bit0 m) 

769 
(num.Bit0 (num.Bit1 n))))" 

770 
"divmod (num.Bit1 m) (num.Bit1 n) = 

771 
(if m < n then (0, numeral (num.Bit1 m)) 

772 
else divmod_step (num.Bit1 n) 

773 
(divmod (num.Bit1 m) 

774 
(num.Bit0 (num.Bit1 n))))" 

775 
by (simp_all add: divmod_divmod_step) 

776 

61275
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

777 
lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

778 

60758  779 
text \<open>Special case: divisibility\<close> 
58953  780 

781 
definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool" 

782 
where 

783 
"divides_aux qr \<longleftrightarrow> snd qr = 0" 

784 

785 
lemma divides_aux_eq [simp]: 

786 
"divides_aux (q, r) \<longleftrightarrow> r = 0" 

787 
by (simp add: divides_aux_def) 

788 

789 
lemma dvd_numeral_simp [simp]: 

790 
"numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)" 

791 
by (simp add: divmod_def mod_eq_0_iff_dvd) 

53069
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
53068
diff
changeset

792 

60867  793 
text \<open>Generic computation of quotient and remainder\<close> 
794 

795 
lemma numeral_div_numeral [simp]: 

796 
"numeral k div numeral l = fst (divmod k l)" 

797 
by (simp add: fst_divmod) 

798 

799 
lemma numeral_mod_numeral [simp]: 

800 
"numeral k mod numeral l = snd (divmod k l)" 

801 
by (simp add: snd_divmod) 

802 

803 
lemma one_div_numeral [simp]: 

804 
"1 div numeral n = fst (divmod num.One n)" 

805 
by (simp add: fst_divmod) 

806 

807 
lemma one_mod_numeral [simp]: 

808 
"1 mod numeral n = snd (divmod num.One n)" 

809 
by (simp add: snd_divmod) 

810 

53067
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

811 
end 
ee0b7c2315d2
type class for generic division algorithm on numerals
haftmann
parents:
53066
diff
changeset

812 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

813 

60758  814 
subsection \<open>Division on @{typ nat}\<close> 
815 

61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

816 
context 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

817 
begin 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

818 

60758  819 
text \<open> 
63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

820 
We define @{const divide} and @{const modulo} on @{typ nat} by means 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

821 
of a characteristic relation with two input arguments 
61076  822 
@{term "m::nat"}, @{term "n::nat"} and two output arguments 
823 
@{term "q::nat"}(uotient) and @{term "r::nat"}(emainder). 

60758  824 
\<close> 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

825 

33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

826 
definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where 
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

827 
"divmod_nat_rel m n qr \<longleftrightarrow> 
30923
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

828 
m = fst qr * n + snd qr \<and> 
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

829 
(if n = 0 then fst qr = 0 else if n > 0 then 0 \<le> snd qr \<and> snd qr < n else n < snd qr \<and> snd qr \<le> 0)" 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

830 

60758  831 
text \<open>@{const divmod_nat_rel} is total:\<close> 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

832 

61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

833 
qualified lemma divmod_nat_rel_ex: 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

834 
obtains q r where "divmod_nat_rel m n (q, r)" 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

835 
proof (cases "n = 0") 
30923
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

836 
case True with that show thesis 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

837 
by (auto simp add: divmod_nat_rel_def) 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

838 
next 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

839 
case False 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

840 
have "\<exists>q r. m = q * n + r \<and> r < n" 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

841 
proof (induct m) 
60758  842 
case 0 with \<open>n \<noteq> 0\<close> 
61076  843 
have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

844 
then show ?case by blast 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

845 
next 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

846 
case (Suc m) then obtain q' r' 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

847 
where m: "m = q' * n + r'" and n: "r' < n" by auto 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

848 
then show ?case proof (cases "Suc r' < n") 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

849 
case True 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

850 
from m n have "Suc m = q' * n + Suc r'" by simp 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

851 
with True show ?thesis by blast 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

852 
next 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

853 
case False then have "n \<le> Suc r'" by auto 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

854 
moreover from n have "Suc r' \<le> n" by auto 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

855 
ultimately have "n = Suc r'" by auto 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

856 
with m have "Suc m = Suc q' * n + 0" by simp 
60758  857 
with \<open>n \<noteq> 0\<close> show ?thesis by blast 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

858 
qed 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

859 
qed 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

860 
with that show thesis 
60758  861 
using \<open>n \<noteq> 0\<close> by (auto simp add: divmod_nat_rel_def) 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

862 
qed 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

863 

60758  864 
text \<open>@{const divmod_nat_rel} is injective:\<close> 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

865 

61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

866 
qualified lemma divmod_nat_rel_unique: 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

867 
assumes "divmod_nat_rel m n qr" 
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

868 
and "divmod_nat_rel m n qr'" 
30923
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

869 
shows "qr = qr'" 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

870 
proof (cases "n = 0") 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

871 
case True with assms show ?thesis 
30923
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

872 
by (cases qr, cases qr') 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

873 
(simp add: divmod_nat_rel_def) 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

874 
next 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

875 
case False 
61076  876 
have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q::nat)" 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

877 
apply (rule leI) 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

878 
apply (subst less_iff_Suc_add) 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

879 
apply (auto simp add: add_mult_distrib) 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

880 
done 
60758  881 
from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'" 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

882 
by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym) 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53199
diff
changeset

883 
with assms have "snd qr = snd qr'" 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

884 
by (simp add: divmod_nat_rel_def) 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53199
diff
changeset

885 
with * show ?thesis by (cases qr, cases qr') simp 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

886 
qed 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

887 

60758  888 
text \<open> 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

889 
We instantiate divisibility on the natural numbers by 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

890 
means of @{const divmod_nat_rel}: 
60758  891 
\<close> 
25942  892 

61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

893 
qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where 
37767  894 
"divmod_nat m n = (THE qr. divmod_nat_rel m n qr)" 
30923
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

895 

61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

896 
qualified lemma divmod_nat_rel_divmod_nat: 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

897 
"divmod_nat_rel m n (divmod_nat m n)" 
30923
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

898 
proof  
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

899 
from divmod_nat_rel_ex 
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

900 
obtain qr where rel: "divmod_nat_rel m n qr" . 
30923
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

901 
then show ?thesis 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

902 
by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique) 
30923
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

903 
qed 
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

904 

61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

905 
qualified lemma divmod_nat_unique: 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

906 
assumes "divmod_nat_rel m n qr" 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

907 
shows "divmod_nat m n = qr" 
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

908 
using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat) 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

909 

61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

910 
qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)" 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

911 
by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def) 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

912 

a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

913 
qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)" 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

914 
by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def) 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

915 

a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

916 
qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)" 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

917 
by (simp add: divmod_nat_unique divmod_nat_rel_def) 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

918 

a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

919 
qualified lemma divmod_nat_step: 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

920 
assumes "0 < n" and "n \<le> m" 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

921 
shows "divmod_nat m n = apfst Suc (divmod_nat (m  n) n)" 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

922 
proof (rule divmod_nat_unique) 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

923 
have "divmod_nat_rel (m  n) n (divmod_nat (m  n) n)" 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

924 
by (fact divmod_nat_rel_divmod_nat) 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

925 
then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m  n) n))" 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

926 
unfolding divmod_nat_rel_def using assms by auto 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

927 
qed 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

928 

a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

929 
end 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

930 

60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60353
diff
changeset

931 
instantiation nat :: semiring_div 
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

932 
begin 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

933 

d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

934 
definition divide_nat where 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

935 
div_nat_def: "m div n = fst (Divides.divmod_nat m n)" 
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

936 

63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

937 
definition modulo_nat where 
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

938 
mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)" 
46551
866bce5442a3
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
huffman
parents:
46026
diff
changeset

939 

866bce5442a3
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
huffman
parents:
46026
diff
changeset

940 
lemma fst_divmod_nat [simp]: 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

941 
"fst (Divides.divmod_nat m n) = m div n" 
46551
866bce5442a3
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
huffman
parents:
46026
diff
changeset

942 
by (simp add: div_nat_def) 
866bce5442a3
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
huffman
parents:
46026
diff
changeset

943 

866bce5442a3
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
huffman
parents:
46026
diff
changeset

944 
lemma snd_divmod_nat [simp]: 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

945 
"snd (Divides.divmod_nat m n) = m mod n" 
46551
866bce5442a3
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
huffman
parents:
46026
diff
changeset

946 
by (simp add: mod_nat_def) 
866bce5442a3
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
huffman
parents:
46026
diff
changeset

947 

33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

948 
lemma divmod_nat_div_mod: 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

949 
"Divides.divmod_nat m n = (m div n, m mod n)" 
46551
866bce5442a3
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
huffman
parents:
46026
diff
changeset

950 
by (simp add: prod_eq_iff) 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

951 

47135
fb67b596067f
rename lemmas {div,mod}_eq > {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
huffman
parents:
47134
diff
changeset

952 
lemma div_nat_unique: 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

953 
assumes "divmod_nat_rel m n (q, r)" 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

954 
shows "m div n = q" 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

955 
using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff) 
47135
fb67b596067f
rename lemmas {div,mod}_eq > {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
huffman
parents:
47134
diff
changeset

956 

fb67b596067f
rename lemmas {div,mod}_eq > {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
huffman
parents:
47134
diff
changeset

957 
lemma mod_nat_unique: 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

958 
assumes "divmod_nat_rel m n (q, r)" 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

959 
shows "m mod n = r" 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

960 
using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff) 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25162
diff
changeset

961 

33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

962 
lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)" 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

963 
using Divides.divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod) 
25942  964 

63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

965 
text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close> 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

966 

fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

967 
lemma div_less [simp]: 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

968 
fixes m n :: nat 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

969 
assumes "m < n" 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

970 
shows "m div n = 0" 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

971 
using assms Divides.divmod_nat_base by (simp add: prod_eq_iff) 
25942  972 

26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

973 
lemma le_div_geq: 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

974 
fixes m n :: nat 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

975 
assumes "0 < n" and "n \<le> m" 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

976 
shows "m div n = Suc ((m  n) div n)" 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

977 
using assms Divides.divmod_nat_step by (simp add: prod_eq_iff) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

978 

26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

979 
lemma mod_less [simp]: 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

980 
fixes m n :: nat 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

981 
assumes "m < n" 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

982 
shows "m mod n = m" 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

983 
using assms Divides.divmod_nat_base by (simp add: prod_eq_iff) 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

984 

fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

985 
lemma le_mod_geq: 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

986 
fixes m n :: nat 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

987 
assumes "n \<le> m" 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

988 
shows "m mod n = (m  n) mod n" 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

989 
using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

990 

47136  991 
instance proof 
992 
fix m n :: nat 

993 
show "m div n * n + m mod n = m" 

994 
using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def) 

995 
next 

996 
fix m n q :: nat 

997 
assume "n \<noteq> 0" 

998 
then show "(q + m * n) div n = m + q div n" 

999 
by (induct m) (simp_all add: le_div_geq) 

1000 
next 

1001 
fix m n q :: nat 

1002 
assume "m \<noteq> 0" 

1003 
hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)" 

1004 
unfolding divmod_nat_rel_def 

62390  1005 
by (auto split: if_split_asm, simp_all add: algebra_simps) 
47136  1006 
moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" . 
1007 
ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" . 

1008 
thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique) 

1009 
next 

1010 
fix n :: nat show "n div 0 = 0" 

61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

1011 
by (simp add: div_nat_def Divides.divmod_nat_zero) 
47136  1012 
next 
1013 
fix n :: nat show "0 div n = 0" 

61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

1014 
by (simp add: div_nat_def Divides.divmod_nat_zero_left) 
25942  1015 
qed 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1016 

25942  1017 
end 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1018 

60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1019 
instantiation nat :: normalization_semidom 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1020 
begin 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1021 

cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1022 
definition normalize_nat 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1023 
where [simp]: "normalize = (id :: nat \<Rightarrow> nat)" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1024 

cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1025 
definition unit_factor_nat 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1026 
where "unit_factor n = (if n = 0 then 0 else 1 :: nat)" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1027 

cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1028 
lemma unit_factor_simps [simp]: 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1029 
"unit_factor 0 = (0::nat)" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1030 
"unit_factor (Suc n) = 1" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1031 
by (simp_all add: unit_factor_nat_def) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1032 

cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1033 
instance 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1034 
by standard (simp_all add: unit_factor_nat_def) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1035 

cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1036 
end 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60562
diff
changeset

1037 

61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

1038 
lemma divmod_nat_if [code]: 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

1039 
"Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else 
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset

1040 
let (q, r) = Divides.divmod_nat (m  n) n in (Suc q, r))" 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55172
diff
changeset

1041 
by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq) 
33361
1f18de40b43f
combined former theories Divides and IntDiv to one theory Divides
haftmann
parents:
33340
diff
changeset

1042 

63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

1043 
text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close> 
25942  1044 

51299
30b014246e21
proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);
wenzelm
parents:
51173
diff
changeset

1045 
ML_file "~~/src/Provers/Arith/cancel_div_mod.ML" 
30b014246e21
proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);
wenzelm
parents:
51173
diff
changeset

1046 

60758  1047 
ML \<open> 
43594  1048 
structure Cancel_Div_Mod_Nat = Cancel_Div_Mod 
41550  1049 
( 
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1050 
val div_name = @{const_name divide}; 
63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

1051 
val mod_name = @{const_name modulo}; 
30934  1052 
val mk_binop = HOLogic.mk_binop; 
48561
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1053 
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1054 
val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1055 
fun mk_sum [] = HOLogic.zero 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1056 
 mk_sum [t] = t 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1057 
 mk_sum (t :: ts) = mk_plus (t, mk_sum ts); 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1058 
fun dest_sum tm = 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1059 
if HOLogic.is_zero tm then [] 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1060 
else 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1061 
(case try HOLogic.dest_Suc tm of 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1062 
SOME t => HOLogic.Suc_zero :: dest_sum t 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1063 
 NONE => 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1064 
(case try dest_plus tm of 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1065 
SOME (t, u) => dest_sum t @ dest_sum u 
12aa0cb2b447
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman
parents:
47268
diff
changeset

1066 
 NONE => [tm])); 
25942  1067 

30934  1068 
val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]; 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1069 

30934  1070 
val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

1071 
(@{thm add_0_left} :: @{thm add_0_right} :: @{thms ac_simps})) 
41550  1072 
) 
60758  1073 
\<close> 
1074 

1075 
simproc_setup cancel_div_mod_nat ("(m::nat) + n") = \<open>K Cancel_Div_Mod_Nat.proc\<close> 

1076 

1077 

1078 
subsubsection \<open>Quotient\<close> 

26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1079 

fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1080 
lemma div_geq: "0 < n \<Longrightarrow> \<not> m < n \<Longrightarrow> m div n = Suc ((m  n) div n)" 
29667  1081 
by (simp add: le_div_geq linorder_not_less) 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1082 

fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1083 
lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m  n) div n))" 
29667  1084 
by (simp add: div_geq) 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1085 

fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1086 
lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)" 
29667  1087 
by simp 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1088 

fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1089 
lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)" 
29667  1090 
by simp 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1091 

53066  1092 
lemma div_positive: 
1093 
fixes m n :: nat 

1094 
assumes "n > 0" 

1095 
assumes "m \<ge> n" 

1096 
shows "m div n > 0" 

1097 
proof  

60758  1098 
from \<open>m \<ge> n\<close> obtain q where "m = n + q" 
53066  1099 
by (auto simp add: le_iff_add) 
63499
9c9a59949887
Tuned looping simp rules in semiring_div
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset

1100 
with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1) 
53066  1101 
qed 
1102 

59000  1103 
lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0" 
1104 
by (metis div_less div_positive div_by_0 gr0I less_numeral_extra(3) not_less) 

25942  1105 

60758  1106 
subsubsection \<open>Remainder\<close> 
25942  1107 

26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1108 
lemma mod_less_divisor [simp]: 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1109 
fixes m n :: nat 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1110 
assumes "n > 0" 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1111 
shows "m mod n < (n::nat)" 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

1112 
using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def by auto 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1113 

51173  1114 
lemma mod_Suc_le_divisor [simp]: 
1115 
"m mod Suc n \<le> n" 

1116 
using mod_less_divisor [of "Suc n" m] by arith 

1117 

26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1118 
lemma mod_less_eq_dividend [simp]: 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1119 
fixes m n :: nat 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1120 
shows "m mod n \<le> m" 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1121 
proof (rule add_leD2) 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1122 
from mod_div_equality have "m div n * n + m mod n = m" . 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1123 
then show "m div n * n + m mod n \<le> m" by auto 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1124 
qed 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1125 

61076  1126 
lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m  n) mod n" 
29667  1127 
by (simp add: le_mod_geq linorder_not_less) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1128 

61076  1129 
lemma mod_if: "m mod (n::nat) = (if m < n then m else (m  n) mod n)" 
29667  1130 
by (simp add: le_mod_geq) 
26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26072
diff
changeset

1131 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1132 
lemma mod_1 [simp]: "m mod Suc 0 = 0" 
29667  1133 
by (induct m) (simp_all add: mod_geq) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1134 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1135 
(* a simple rearrangement of mod_div_equality: *) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1136 
lemma mult_div_cancel: "(n::nat) * (m div n) = m  (m mod n)" 
47138  1137 
using mod_div_equality2 [of n m] by arith 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1138 

15439  1139 
lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)" 
22718  1140 
apply (drule mod_less_divisor [where m = m]) 
1141 
apply simp 

1142 
done 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1143 

60758  1144 
subsubsection \<open>Quotient and Remainder\<close> 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1145 

33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

1146 
lemma divmod_nat_rel_mult1_eq: 
46552  1147 
"divmod_nat_rel b c (q, r) 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

1148 
\<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)" 
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

1149 
by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1150 

30923
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

1151 
lemma div_mult1_eq: 
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

1152 
"(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)" 
47135
fb67b596067f
rename lemmas {div,mod}_eq > {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
huffman
parents:
47134
diff
changeset

1153 
by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1154 

33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

1155 
lemma divmod_nat_rel_add1_eq: 
46552  1156 
"divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br) 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

1157 
\<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)" 
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

1158 
by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1159 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1160 
(*NOT suitable for rewriting: the RHS has an instance of the LHS*) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1161 
lemma div_add1_eq: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1162 
"(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)" 
47135
fb67b596067f
rename lemmas {div,mod}_eq > {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
huffman
parents:
47134
diff
changeset

1163 
by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1164 

33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

1165 
lemma divmod_nat_rel_mult2_eq: 
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1166 
assumes "divmod_nat_rel a b (q, r)" 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1167 
shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)" 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1168 
proof  
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

1169 
{ assume "r < b" and "0 < c" 
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1170 
then have "b * (q mod c) + r < b * c" 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1171 
apply (cut_tac m = q and n = c in mod_less_divisor) 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1172 
apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto) 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1173 
apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst) 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1174 
apply (simp add: add_mult_distrib2) 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1175 
done 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1176 
then have "r + b * (q mod c) < b * c" 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1177 
by (simp add: ac_simps) 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1178 
} with assms show ?thesis 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1179 
by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric]) 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59833
diff
changeset

1180 
qed 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60517
diff
changeset

1181 

55085
0e8e4dc55866
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
54489
diff
changeset

1182 
lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)" 
47135
fb67b596067f
rename lemmas {div,mod}_eq > {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
huffman
parents:
47134
diff
changeset

1183 
by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique]) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1184 

55085
0e8e4dc55866
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
54489
diff
changeset

1185 
lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

1186 
by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique]) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1187 

61275
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1188 
instantiation nat :: semiring_numeral_div 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1189 
begin 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1190 

053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1191 
definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat" 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1192 
where 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1193 
divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)" 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1194 

053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1195 
definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat" 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1196 
where 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1197 
"divmod_step_nat l qr = (let (q, r) = qr 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1198 
in if r \<ge> numeral l then (2 * q + 1, r  numeral l) 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1199 
else (2 * q, r))" 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1200 

053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1201 
instance 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1202 
by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq) 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1203 

053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1204 
end 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1205 

053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1206 
declare divmod_algorithm_code [where ?'a = nat, code] 
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
61201
diff
changeset

1207 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1208 

60758  1209 
subsubsection \<open>Further Facts about Quotient and Remainder\<close> 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1210 

58786  1211 
lemma div_1 [simp]: 
1212 
"m div Suc 0 = m" 

1213 
using div_by_1 [of m] by simp 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1214 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1215 
(* Monotonicity of div in first argument *) 
30923
2697a1d1d34a
more coherent developement in Divides.thy and IntDiv.thy
haftmann
parents:
30840
diff
changeset

1216 
lemma div_le_mono [rule_format (no_asm)]: 
22718  1217 
"\<forall>m::nat. m \<le> n > (m div k) \<le> (n div k)" 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1218 
apply (case_tac "k=0", simp) 
15251  1219 
apply (induct "n" rule: nat_less_induct, clarify) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1220 
apply (case_tac "n<k") 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1221 
(* 1 case n<k *) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1222 
apply simp 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1223 
(* 2 case n >= k *) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1224 
apply (case_tac "m<k") 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1225 
(* 2.1 case m<k *) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1226 
apply simp 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1227 
(* 2.2 case m>=k *) 
15439  1228 
apply (simp add: div_geq diff_le_mono) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1229 
done 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1230 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1231 
(* Antimonotonicity of div in second argument *) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1232 
lemma div_le_mono2: "!!m::nat. [ 0<m; m\<le>n ] ==> (k div n) \<le> (k div m)" 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1233 
apply (subgoal_tac "0<n") 
22718  1234 
prefer 2 apply simp 
15251  1235 
apply (induct_tac k rule: nat_less_induct) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1236 
apply (rename_tac "k") 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1237 
apply (case_tac "k<n", simp) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1238 
apply (subgoal_tac "~ (k<m) ") 
22718  1239 
prefer 2 apply simp 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1240 
apply (simp add: div_geq) 
15251  1241 
apply (subgoal_tac "(kn) div n \<le> (km) div n") 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1242 
prefer 2 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1243 
apply (blast intro: div_le_mono diff_le_mono2) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1244 
apply (rule le_trans, simp) 
15439  1245 
apply (simp) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1246 
done 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1247 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1248 
lemma div_le_dividend [simp]: "m div n \<le> (m::nat)" 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1249 
apply (case_tac "n=0", simp) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1250 
apply (subgoal_tac "m div n \<le> m div 1", simp) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1251 
apply (rule div_le_mono2) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1252 
apply (simp_all (no_asm_simp)) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1253 
done 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1254 

22718  1255 
(* Similar for "less than" *) 
47138  1256 
lemma div_less_dividend [simp]: 
1257 
"\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m" 

1258 
apply (induct m rule: nat_less_induct) 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1259 
apply (rename_tac "m") 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1260 
apply (case_tac "m<n", simp) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1261 
apply (subgoal_tac "0<n") 
22718  1262 
prefer 2 apply simp 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1263 
apply (simp add: div_geq) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1264 
apply (case_tac "n<m") 
15251  1265 
apply (subgoal_tac "(mn) div n < (mn) ") 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1266 
apply (rule impI less_trans_Suc)+ 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1267 
apply assumption 
15439  1268 
apply (simp_all) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1269 
done 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1270 

60758  1271 
text\<open>A fact for the mutilated chess board\<close> 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1272 
lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))" 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1273 
apply (case_tac "n=0", simp) 
15251  1274 
apply (induct "m" rule: nat_less_induct) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1275 
apply (case_tac "Suc (na) <n") 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1276 
(* case Suc(na) < n *) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1277 
apply (frule lessI [THEN less_trans], simp add: less_not_refl3) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1278 
(* case n \<le> Suc(na) *) 
16796  1279 
apply (simp add: linorder_not_less le_Suc_eq mod_geq) 
15439  1280 
apply (auto simp add: Suc_diff_le le_mod_geq) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1281 
done 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1282 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14208
diff
changeset

1283 
lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)" 
29667  1284 
by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) 
17084
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
16796
diff
changeset

1285 