1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
(** {1 Number theory} *)
(** {2 Parity properties} *)
module Parity
use int.Int
predicate even (n: int) = exists k: int. n = 2 * k
predicate odd (n: int) = exists k: int. n = 2 * k + 1
lemma even_or_odd: forall n: int. even n \/ odd n
lemma even_not_odd: forall n: int. even n -> not (odd n)
lemma odd_not_even: forall n: int. odd n -> not (even n)
lemma even_odd: forall n: int. even n -> odd (n + 1)
lemma odd_even: forall n: int. odd n -> even (n + 1)
lemma even_even: forall n: int. even n -> even (n + 2)
lemma odd_odd: forall n: int. odd n -> odd (n + 2)
lemma even_2k: forall k: int. even (2 * k)
lemma odd_2k1: forall k: int. odd (2 * k + 1)
use int.ComputerDivision
lemma even_mod2 :
forall n:int. even n <-> mod n 2 = 0
end
(** {2 Divisibility} *)
module Divisibility
use export int.Int
use int.ComputerDivision
let predicate divides (d:int) (n:int)
ensures { result <-> exists q:int. n = q * d }
= if d = 0 then n = 0 else mod n d = 0
lemma divides_refl: forall n:int. divides n n
lemma divides_1_n : forall n:int. divides 1 n
lemma divides_0 : forall n:int. divides n 0
lemma divides_left : forall a b c: int. divides a b -> divides (c*a) (c*b)
lemma divides_right: forall a b c: int. divides a b -> divides (a*c) (b*c)
lemma divides_oppr: forall a b: int. divides a b -> divides a (-b)
lemma divides_oppl: forall a b: int. divides a b -> divides (-a) b
lemma divides_oppr_rev: forall a b: int. divides (-a) b -> divides a b
lemma divides_oppl_rev: forall a b: int. divides a (-b) -> divides a b
lemma divides_plusr:
forall a b c: int. divides a b -> divides a c -> divides a (b + c)
lemma divides_minusr:
forall a b c: int. divides a b -> divides a c -> divides a (b - c)
lemma divides_multl:
forall a b c: int. divides a b -> divides a (c * b)
lemma divides_multr:
forall a b c: int. divides a b -> divides a (b * c)
lemma divides_factorl: forall a b: int. divides a (b * a)
lemma divides_factorr: forall a b: int. divides a (a * b)
lemma divides_n_1: forall n: int. divides n 1 -> n = 1 \/ n = -1
lemma divides_antisym:
forall a b: int. divides a b -> divides b a -> a = b \/ a = -b
lemma divides_trans:
forall a b c: int. divides a b -> divides b c -> divides a c
use int.Abs
lemma divides_bounds:
forall a b: int. divides a b -> b <> 0 -> abs a <= abs b
use int.EuclideanDivision as ED
lemma mod_divides_euclidean:
forall a b: int. b <> 0 -> ED.mod a b = 0 -> divides b a
lemma divides_mod_euclidean:
forall a b: int. b <> 0 -> divides b a -> ED.mod a b = 0
use int.ComputerDivision as CD
lemma mod_divides_computer:
forall a b: int. b <> 0 -> CD.mod a b = 0 -> divides b a
lemma divides_mod_computer:
forall a b: int. b <> 0 -> divides b a -> CD.mod a b = 0
use Parity
lemma even_divides: forall a: int. even a <-> divides 2 a
lemma odd_divides: forall a: int. odd a <-> not (divides 2 a)
end
(** {2 Greateast Common Divisor} *)
module Gcd
use export int.Int
use Divisibility
function gcd int int : int
axiom gcd_nonneg: forall a b: int. 0 <= gcd a b
axiom gcd_def1 : forall a b: int. divides (gcd a b) a
axiom gcd_def2 : forall a b: int. divides (gcd a b) b
axiom gcd_def3 :
forall a b x: int. divides x a -> divides x b -> divides x (gcd a b)
axiom gcd_unique:
forall a b d: int.
0 <= d -> divides d a -> divides d b ->
(forall x: int. divides x a -> divides x b -> divides x d) ->
d = gcd a b
(* gcd is associative commutative *)
clone algebra.AC with type t = int, function op = gcd
lemma gcd_0_pos: forall a: int. 0 <= a -> gcd a 0 = a
lemma gcd_0_neg: forall a: int. a < 0 -> gcd a 0 = -a
lemma gcd_opp: forall a b: int. gcd a b = gcd (-a) b
lemma gcd_euclid: forall a b q: int. gcd a b = gcd a (b - q * a)
use int.ComputerDivision as CD
lemma Gcd_computer_mod:
forall a b: int [gcd b (CD.mod a b)].
b <> 0 -> gcd b (CD.mod a b) = gcd a b
use int.EuclideanDivision as ED
lemma Gcd_euclidean_mod:
forall a b: int [gcd b (ED.mod a b)].
b <> 0 -> gcd b (ED.mod a b) = gcd a b
lemma gcd_mult: forall a b c: int. 0 <= c -> gcd (c * a) (c * b) = c * gcd a b
end
(** {2 Prime numbers} *)
module Prime
use export int.Int
use Divisibility
predicate prime (p: int) =
2 <= p /\ forall n: int. 1 < n < p -> not (divides n p)
lemma not_prime_1: not (prime 1)
lemma prime_2 : prime 2
lemma prime_3 : prime 3
lemma prime_divisors:
forall p: int. prime p ->
forall d: int. divides d p -> d = 1 \/ d = -1 \/ d = p \/ d = -p
lemma small_divisors:
forall p: int. 2 <= p ->
(forall d: int. 2 <= d -> prime d -> 1 < d*d <= p -> not (divides d p)) ->
prime p
use Parity
lemma even_prime: forall p: int. prime p -> even p -> p = 2
lemma odd_prime: forall p: int. prime p -> p >= 3 -> odd p
end
(** {2 Coprime numbers} *)
module Coprime
use export int.Int
use Divisibility
use Gcd
predicate coprime (a b: int) = gcd a b = 1
use Prime
lemma prime_coprime:
forall p: int.
prime p <-> 2 <= p && forall n:int. 1 <= n < p -> coprime n p
lemma Gauss:
forall a b c:int. divides a (b*c) /\ coprime a b -> divides a c
lemma Euclid:
forall p a b:int.
prime p /\ divides p (a*b) -> divides p a \/ divides p b
lemma gcd_coprime:
forall a b c. coprime a b -> gcd a (b*c) = gcd a c
end
|
