author  berghofe 
Tue, 25 Mar 2003 09:56:01 +0100  
changeset 13882  2266550ab316 
parent 13517  42efec18f5b2 
child 14131  a4fc8b1af5e7 
permissions  rwrr 
3366  1 
(* Title: HOL/Divides.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

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

4 
Copyright 1999 University of Cambridge 
3366  5 

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

7 
*) 

8 

13152  9 
theory Divides = NatArith files("Divides_lemmas.ML"): 
3366  10 

8902  11 
(*We use the same class for div and mod; 
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset

12 
moreover, dvd is defined whenever multiplication is*) 
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset

13 
axclass 
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
10789
diff
changeset

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

15 

13152  16 
instance nat :: div .. 
17 
instance nat :: plus_ac0 

18 
proof qed (rule add_commute add_assoc add_0)+ 

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

19 

3366  20 
consts 
13152  21 
div :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a" (infixl 70) 
22 
mod :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a" (infixl 70) 

23 
dvd :: "'a::times \<Rightarrow> 'a \<Rightarrow> bool" (infixl 50) 

3366  24 

25 

26 
defs 

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

27 

13152  28 
mod_def: "m mod n == wfrec (trancl pred_nat) 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
6865
diff
changeset

29 
(%f j. if j<n  n=0 then j else f (jn)) m" 
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset

30 

13152  31 
div_def: "m div n == wfrec (trancl pred_nat) 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
6865
diff
changeset

32 
(%f j. if j<n  n=0 then 0 else Suc (f (jn))) m" 
3366  33 

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

34 
(*The definition of dvd is polymorphic!*) 
13152  35 
dvd_def: "m dvd n == EX k. n = m*k" 
3366  36 

10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset

37 
(*This definition helps prove the harder properties of div and mod. 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset

38 
It is copied from IntDiv.thy; should it be overloaded?*) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset

39 
constdefs 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset

40 
quorem :: "(nat*nat) * (nat*nat) => bool" 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset

41 
"quorem == %((a,b), (q,r)). 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset

42 
a = b*q + r & 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset

43 
(if 0<b then 0<=r & r<b else b<r & r <=0)" 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset

44 

13152  45 
use "Divides_lemmas.ML" 
46 

47 
lemma split_div: 

13189
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

48 
"P(n div k :: nat) = 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

49 
((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

50 
(is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))") 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

51 
proof 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

52 
assume P: ?P 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

53 
show ?Q 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

54 
proof (cases) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

55 
assume "k = 0" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

56 
with P show ?Q by(simp add:DIVISION_BY_ZERO_DIV) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

57 
next 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

58 
assume not0: "k \<noteq> 0" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

59 
thus ?Q 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

60 
proof (simp, intro allI impI) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

61 
fix i j 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

62 
assume n: "n = k*i + j" and j: "j < k" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

63 
show "P i" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

64 
proof (cases) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

65 
assume "i = 0" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

66 
with n j P show "P i" by simp 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

67 
next 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

68 
assume "i \<noteq> 0" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

69 
with not0 n j P show "P i" by(simp add:add_ac) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

70 
qed 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

71 
qed 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

72 
qed 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

73 
next 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

74 
assume Q: ?Q 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

75 
show ?P 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

76 
proof (cases) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

77 
assume "k = 0" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

78 
with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

79 
next 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

80 
assume not0: "k \<noteq> 0" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

81 
with Q have R: ?R by simp 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

82 
from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"] 
13517  83 
show ?P by simp 
13189
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

84 
qed 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

85 
qed 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

86 

13882  87 
lemma split_div_lemma: 
88 
"0 < n \<Longrightarrow> (n * q <= m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))" 

89 
apply (rule iffI) 

90 
apply (rule_tac a=m and r = "m  n * q" and r' = "m mod n" in unique_quotient) 

91 
apply (simp_all add: quorem_def) 

92 
apply arith 

93 
apply (rule conjI) 

94 
apply (rule_tac P="%x. n * (m div n) \<le> x" in 

95 
subst [OF mod_div_equality [of _ n]]) 

96 
apply (simp only: add: mult_ac) 

97 
apply (rule_tac P="%x. x < n + n * (m div n)" in 

98 
subst [OF mod_div_equality [of _ n]]) 

99 
apply (simp only: add: mult_ac add_ac) 

100 
apply (rule add_less_mono1) 

101 
apply simp 

102 
done 

103 

104 
theorem split_div': 

105 
"P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or> 

106 
(\<exists>q. (n * q <= m \<and> m < n * (Suc q)) \<and> P q))" 

107 
apply (case_tac "0 < n") 

108 
apply (simp only: add: split_div_lemma) 

109 
apply (simp_all add: DIVISION_BY_ZERO_DIV) 

110 
done 

111 

13189
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

112 
lemma split_mod: 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

113 
"P(n mod k :: nat) = 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

114 
((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

115 
(is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))") 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

116 
proof 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

117 
assume P: ?P 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

118 
show ?Q 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

119 
proof (cases) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

120 
assume "k = 0" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

121 
with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

122 
next 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

123 
assume not0: "k \<noteq> 0" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

124 
thus ?Q 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

125 
proof (simp, intro allI impI) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

126 
fix i j 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

127 
assume "n = k*i + j" "j < k" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

128 
thus "P j" using not0 P by(simp add:add_ac mult_ac) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

129 
qed 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

130 
qed 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

131 
next 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

132 
assume Q: ?Q 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

133 
show ?P 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

134 
proof (cases) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

135 
assume "k = 0" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

136 
with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

137 
next 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

138 
assume not0: "k \<noteq> 0" 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

139 
with Q have R: ?R by simp 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

140 
from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"] 
13517  141 
show ?P by simp 
13189
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

142 
qed 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

143 
qed 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

144 

13882  145 
theorem mod_div_equality': "(m::nat) mod n = m  (m div n) * n" 
146 
apply (rule_tac P="%x. m mod n = x  (m div n) * n" in 

147 
subst [OF mod_div_equality [of _ n]]) 

148 
apply arith 

149 
done 

150 

13189
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

151 
(* 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

152 
lemma split_div: 
13152  153 
assumes m: "m \<noteq> 0" 
154 
shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)" 

155 
(is "?P = ?Q") 

156 
proof 

157 
assume P: ?P 

158 
show ?Q 

159 
proof (intro allI impI) 

160 
fix i j 

161 
assume n: "n = m*i + j" and j: "j < m" 

162 
show "P i" 

163 
proof (cases) 

164 
assume "i = 0" 

165 
with n j P show "P i" by simp 

166 
next 

167 
assume "i \<noteq> 0" 

168 
with n j P show "P i" by (simp add:add_ac div_mult_self1) 

169 
qed 

170 
qed 

171 
next 

172 
assume Q: ?Q 

173 
from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"] 

13517  174 
show ?P by simp 
13152  175 
qed 
176 

177 
lemma split_mod: 

178 
assumes m: "m \<noteq> 0" 

179 
shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)" 

180 
(is "?P = ?Q") 

181 
proof 

182 
assume P: ?P 

183 
show ?Q 

184 
proof (intro allI impI) 

185 
fix i j 

186 
assume "n = m*i + j" "j < m" 

187 
thus "P j" using m P by(simp add:add_ac mult_ac) 

188 
qed 

189 
next 

190 
assume Q: ?Q 

191 
from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"] 

13517  192 
show ?P by simp 
13152  193 
qed 
13189
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

194 
*) 
3366  195 
end 