4 Copyright 1999 University of Cambridge |
4 Copyright 1999 University of Cambridge |
5 |
5 |
6 The division operators div, mod and the divides relation "dvd" |
6 The division operators div, mod and the divides relation "dvd" |
7 *) |
7 *) |
8 |
8 |
9 Divides = NatArith + |
9 theory Divides = NatArith files("Divides_lemmas.ML"): |
10 |
10 |
11 (*We use the same class for div and mod; |
11 (*We use the same class for div and mod; |
12 moreover, dvd is defined whenever multiplication is*) |
12 moreover, dvd is defined whenever multiplication is*) |
13 axclass |
13 axclass |
14 div < type |
14 div < type |
15 |
15 |
16 instance nat :: div |
16 instance nat :: div .. |
17 instance nat :: plus_ac0 (add_commute,add_assoc,add_0) |
17 instance nat :: plus_ac0 |
|
18 proof qed (rule add_commute add_assoc add_0)+ |
18 |
19 |
19 consts |
20 consts |
20 div :: ['a::div, 'a] => 'a (infixl 70) |
21 div :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a" (infixl 70) |
21 mod :: ['a::div, 'a] => 'a (infixl 70) |
22 mod :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a" (infixl 70) |
22 dvd :: ['a::times, 'a] => bool (infixl 50) |
23 dvd :: "'a::times \<Rightarrow> 'a \<Rightarrow> bool" (infixl 50) |
23 |
24 |
24 |
25 |
25 (*Remainder and quotient are defined here by algorithms and later proved to |
|
26 satisfy the traditional definition (theorem mod_div_equality) |
|
27 *) |
|
28 defs |
26 defs |
29 |
27 |
30 mod_def "m mod n == wfrec (trancl pred_nat) |
28 mod_def: "m mod n == wfrec (trancl pred_nat) |
31 (%f j. if j<n | n=0 then j else f (j-n)) m" |
29 (%f j. if j<n | n=0 then j else f (j-n)) m" |
32 |
30 |
33 div_def "m div n == wfrec (trancl pred_nat) |
31 div_def: "m div n == wfrec (trancl pred_nat) |
34 (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" |
32 (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" |
35 |
33 |
36 (*The definition of dvd is polymorphic!*) |
34 (*The definition of dvd is polymorphic!*) |
37 dvd_def "m dvd n == EX k. n = m*k" |
35 dvd_def: "m dvd n == EX k. n = m*k" |
38 |
36 |
39 (*This definition helps prove the harder properties of div and mod. |
37 (*This definition helps prove the harder properties of div and mod. |
40 It is copied from IntDiv.thy; should it be overloaded?*) |
38 It is copied from IntDiv.thy; should it be overloaded?*) |
41 constdefs |
39 constdefs |
42 quorem :: "(nat*nat) * (nat*nat) => bool" |
40 quorem :: "(nat*nat) * (nat*nat) => bool" |
43 "quorem == %((a,b), (q,r)). |
41 "quorem == %((a,b), (q,r)). |
44 a = b*q + r & |
42 a = b*q + r & |
45 (if 0<b then 0<=r & r<b else b<r & r <=0)" |
43 (if 0<b then 0<=r & r<b else b<r & r <=0)" |
46 |
44 |
|
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: |
|
53 assumes m: "m \<noteq> 0" |
|
54 shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)" |
|
55 (is "?P = ?Q") |
|
56 proof |
|
57 assume P: ?P |
|
58 show ?Q |
|
59 proof (intro allI impI) |
|
60 fix i j |
|
61 assume n: "n = m*i + j" and j: "j < m" |
|
62 show "P i" |
|
63 proof (cases) |
|
64 assume "i = 0" |
|
65 with n j P show "P i" by simp |
|
66 next |
|
67 assume "i \<noteq> 0" |
|
68 with n j P show "P i" by (simp add:add_ac div_mult_self1) |
|
69 qed |
|
70 qed |
|
71 next |
|
72 assume Q: ?Q |
|
73 from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"] |
|
74 show ?P by(simp add:mod_div_equality2) |
|
75 qed |
|
76 |
|
77 lemma split_mod: |
|
78 assumes m: "m \<noteq> 0" |
|
79 shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)" |
|
80 (is "?P = ?Q") |
|
81 proof |
|
82 assume P: ?P |
|
83 show ?Q |
|
84 proof (intro allI impI) |
|
85 fix i j |
|
86 assume "n = m*i + j" "j < m" |
|
87 thus "P j" using m P by(simp add:add_ac mult_ac) |
|
88 qed |
|
89 next |
|
90 assume Q: ?Q |
|
91 from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"] |
|
92 show ?P by(simp add:mod_div_equality2) |
|
93 qed |
|
94 |
47 end |
95 end |