author  nipkow 
Fri, 31 May 2002 07:53:37 +0200  
changeset 13189  81ed5c6de890 
parent 13152  2a54f99b44b3 
child 13517  42efec18f5b2 
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 mod_div_equality2: "n * (m div n) + m mod n = (m::nat)" 

48 
apply(insert mod_div_equality[of m n]) 

49 
apply(simp only:mult_ac) 

50 
done 

51 

52 
lemma split_div: 

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

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

54 
((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

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

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

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

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

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

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

61 
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

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

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

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

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

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

67 
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

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

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

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

71 
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

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

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

74 
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

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

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

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

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

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

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

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

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

83 
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

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

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

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

87 
from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"] 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

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

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

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

91 

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

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

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

94 
((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

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

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

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

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

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

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

101 
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

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

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

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

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

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

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

108 
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

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

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

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

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

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

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

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

116 
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

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

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

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

120 
from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"] 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13152
diff
changeset

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

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

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

124 

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

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

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

129 
(is "?P = ?Q") 

130 
proof 

131 
assume P: ?P 

132 
show ?Q 

133 
proof (intro allI impI) 

134 
fix i j 

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

136 
show "P i" 

137 
proof (cases) 

138 
assume "i = 0" 

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

140 
next 

141 
assume "i \<noteq> 0" 

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

143 
qed 

144 
qed 

145 
next 

146 
assume Q: ?Q 

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

148 
show ?P by(simp add:mod_div_equality2) 

149 
qed 

150 

151 
lemma split_mod: 

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

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

154 
(is "?P = ?Q") 

155 
proof 

156 
assume P: ?P 

157 
show ?Q 

158 
proof (intro allI impI) 

159 
fix i j 

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

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

162 
qed 

163 
next 

164 
assume Q: ?Q 

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

166 
show ?P by(simp add:mod_div_equality2) 

167 
qed 

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

168 
*) 
3366  169 
end 