author | wenzelm |
Tue, 16 Jul 2002 18:41:50 +0200 | |
changeset 13377 | cc8245843abc |
parent 13189 | 81ed5c6de890 |
child 13517 | 42efec18f5b2 |
permissions | -rw-r--r-- |
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 (j-n)) 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 (j-n))) 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 |