natural_hol.fcl 17.4 KB
Newer Older
1
2
3
4
open "basics";;
open "naturals";;
open "natural_instantiation";;

5
6
7
8
9
10
11
12
13
14
15
16
17
18
(* This file is very sensible to the numbering of theorems performed
   by Holide.

   If the numbering changes for whatever reason, we can use the Emacs
   Lisp script update-thm-numbers.el.

   In Emacs, this can be done by hitting C-x C-e with point at the end
   of the following expression:

   (let ((load-path '(".")))
   (when (load "update-thm-numbers") (update-all-thm-numbers)))

*)

19
20
21
22
23
24
25
26
(* We instantiate the species hierarchy defined in nat.fcl
   using the definitions of OpenTheory.
   We proceed species by species. *)

(* NatDecl *)

type hnat = internal
  external
Raphael Cauderlier's avatar
Raphael Cauderlier committed
27
  | dedukti -> {* HolNaturals.Number_2ENatural_2Enatural *};;
28
29
30

let hzero = internal hnat
  external
Raphael Cauderlier's avatar
Raphael Cauderlier committed
31
  | dedukti -> {* HolNaturals.Number_2ENatural_2Ezero *};;
32
33
34

let hsucc (n : hnat) = internal hnat
  external
Raphael Cauderlier's avatar
Raphael Cauderlier committed
35
  | dedukti -> {* HolNaturals.Number_2ENatural_2Esuc n *};;
36
37

theorem hol_induction :
38
39
40
  all p : hnat -> bool,
      (p(hzero) /\ (all n : hnat, p(n) -> p(hsucc(n)))) ->
      (all n : hnat, p(n))
41
42
proof = dedukti proof {* HolNaturals.thm_1239. *};;
(* (update-thm-number-on-previous-line "((p zero) /\\ (∀n, (p n) ==> (p (suc n)))) ==> (∀n, p n)")
Raphael Cauderlier's avatar
Raphael Cauderlier committed
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

species HolNatDecl =
  inherit NatDecl;
  representation = hnat;

  let zero = hzero;
  let succ(n : hnat) = hsucc(n);

  proof of ind =
  dedukti proof
    definition of zero, succ
    {* (p : (cc.eT abst_T -> cc.eT hol.bool) =>
        H0 : hol.proof (p abst_zero) =>
        HS : (n : cc.eT abst_T ->
              hol.proof (p n) ->
              hol.proof (p (abst_succ n))) =>
        hol_induction p
          (hol.and_intro
             (p abst_zero)
             (hol.forall abst_T (n : hol.term abst_T => hol.imp (p n) (p (abst_succ n))))
             H0 HS)). *};

  proof of zero_succ =
  <1>1 assume m : Self,
       prove ~ (succ(m) = zero)
       dedukti proof definition of zero, succ
Raphael Cauderlier's avatar
Raphael Cauderlier committed
70
         {* HolNaturals.thm_106 m *}
71
         (* (update-thm-number-on-previous-line "∀n, ~ ((suc n) = zero)") *)
72
73
74
75
76
77
  <1>f conclude;

  proof of succ_inj =
  <1>1 assume m n : Self,
       prove (succ(m) = succ(n)) <-> (m = n)
       dedukti proof definition of succ
Raphael Cauderlier's avatar
Raphael Cauderlier committed
78
         {* HolNaturals.thm_107 m n *}
79
         (* (update-thm-number-on-previous-line "∀m n, ((suc m) = (suc n)) <=> (m = n)") *)
80
81
82
83
84
85
86
87
  <1>f conclude;
end;;

collection HolNatDeclColl = implement HolNatDecl; end;;


(* NatIter *)

Raphael Cauderlier's avatar
Raphael Cauderlier committed
88
89
90
91
92
93
94
95
96
97
(* let id(x : 'a) = x;; *)
let id =
  internal 'a -> 'a
  external
  | dedukti -> {* HolNaturals.Function_2Eid (hol.arr __var_a __var_a).
                  axiom_id : a : hol.type -> x : hol.term a -> hol.proof (hol.eq a (id a x) x)
                *};;

theorem id_x : all x : 'a, id @ x = x
proof = dedukti proof {* axiom_id. *};;
98
99
100
101

let ( ^ ) =
  internal ('a -> 'a) -> hnat -> ('a -> 'a)
  external
Raphael Cauderlier's avatar
Raphael Cauderlier committed
102
  | dedukti -> {* HolNaturals.Function_2E_5E __var_a *};;
103
104
105
106
107

theorem power_zero : all f : 'a -> 'a,
  f ^ hzero = id
proof =
dedukti proof
Raphael Cauderlier's avatar
Raphael Cauderlier committed
108
  {* HolNaturals.thm_109. *};;
109
  (* (update-thm-number-on-previous-line "∀f, (f ^ zero) = id") *)
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125

species HolNatIter =
  inherit NatIter, HolNatDecl;

  let iter(f, z, n) = (f ^ n) @ z;
  proof of iter_zero =
  <1>1 assume f : Self -> Self,
       assume z : Self,
       prove iter(f, z, zero) = z
       <2>1 prove iter(f, z, zero) = (f ^ zero) @ z
            by definition of iter
       <2>2 prove f ^ zero = id
            dedukti proof
              definition of zero
                {* power_zero abst_T f *}
       <2>3 prove id @ z = z
Raphael Cauderlier's avatar
Raphael Cauderlier committed
126
              dedukti proof {* id_x abst_T z *}
127
128
129
130
131
132
133
134
       <2>f conclude
  <1>f conclude;

  proof of iter_succ =
  <1>1 assume f : Self -> Self,
       assume z : Self,
       assume n : Self,
       prove iter(f, z, succ(n)) = f @ iter(f, z, n)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
135
       dedukti proof definition of iter, succ {* HolNaturals.thm_6414 abst_T f n z *}
136
       (* (update-thm-number-on-previous-line "∀f n x, (f ^ (suc n) x) = (f (f ^ n x))") *)
137
138
139
140
141
142
143
144
145
146
  <1>f conclude;
end;;

collection HolNatIterColl = implement HolNatIter; end;;

(* NatPlus *)

let hol_plus =
  internal hnat -> hnat -> hnat
  external
Raphael Cauderlier's avatar
Raphael Cauderlier committed
147
  | dedukti -> {* HolNaturals.Number_2ENatural_2E_2B *};;
148
149
150
151
152
153
154
155
156

species HolPlus =
  inherit HolNatIter, NatPlus;

  (* Redefine plus as in OpenTheory. *)
  let plus(a, b) = hol_plus(a, b);
  proof of zero_plus =
  dedukti proof
    definition of plus, zero
Raphael Cauderlier's avatar
Raphael Cauderlier committed
157
    {* HolNaturals.thm_144. *};
158
    (* (update-thm-number-on-previous-line "∀n, (zero + n) = n") *)
159
160
161
162

  proof of succ_plus =
  dedukti proof
    definition of plus, succ
Raphael Cauderlier's avatar
Raphael Cauderlier committed
163
    {* HolNaturals.thm_147. *};
164
    (* (update-thm-number-on-previous-line "∀m n, ((suc m) + n) = (suc (m + n))") *)
165
166
167
168
169
170
171
172
173
end;;

collection HolPlusColl = implement HolPlus; end;;

(* NatTimes *)

let hol_times (p : hnat, q : hnat) : hnat =
  internal hnat
  external
Raphael Cauderlier's avatar
Raphael Cauderlier committed
174
  | dedukti -> {* HolNaturals.Number_2ENatural_2E_2A p q *};;
175
176

theorem hol_times_zero : all n : hnat, hol_times(hzero, n) = hzero
Raphael Cauderlier's avatar
Raphael Cauderlier committed
177
proof = dedukti proof {* HolNaturals.thm_117. *};;
178
(* (update-thm-number-on-previous-line "∀n, (zero * n) = zero") *)
179
180

theorem hol_times_succ : all m n : hnat, hol_times(hsucc(m), n) = hol_plus(hol_times(m, n), n)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
181
proof = dedukti proof {* HolNaturals.thm_157. *};;
182
(* (update-thm-number-on-previous-line "∀m n, ((suc m) * n) = ((m * n) + n)") *)
183
184
185

theorem hol_times_commute : all m n : hnat,
  hol_times (m, n) = hol_times (n, m)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
186
proof = dedukti proof {* HolNaturals.thm_143. *};;
187
(* (update-thm-number-on-previous-line "∀m n, (m * n) = (n * m)") *)
188
189
190

theorem hol_plus_commute : all m n : hnat,
  hol_plus (m, n) = hol_plus (n, m)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
191
proof = dedukti proof {* HolNaturals.thm_129. *};;
192
(* (update-thm-number-on-previous-line "∀m n, (m + n) = (n + m)") *)
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215

species HolTimes =
  inherit NatTimes, HolPlus;
  let times (p, q) = hol_times(p, q);
  proof of zero_times = by definition of zero, times property hol_times_zero;
  proof of succ_times =
  <1>1 assume m n : Self,
       prove times(succ(m), n) = plus(n, times(m, n))
       <2>1 prove times(succ(m), n) = plus(times(m, n), n)
            by definition of succ, times, plus
               property hol_times_succ
       <2>2 prove plus(times(m, n), n) = plus(n, times(m, n))
            by definition of plus property hol_plus_commute
       <2>f conclude
  <1>f conclude;
end;;

collection HolTimesColl = implement HolTimes; end;;

(* NatLe *)

let hol_le (m : hnat, n : hnat) =
  internal bool
Raphael Cauderlier's avatar
Raphael Cauderlier committed
216
  external | dedukti -> {* HolNaturals.Number_2ENatural_2E_3C_3D m n *};;
217
218

theorem hol_le_plus : all m n : hnat, hol_le(m, n) <-> ex d : hnat, n = hol_plus(m, d)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
219
proof = dedukti proof {* HolNaturals.thm_132. *};;
220
(* (update-thm-number-on-previous-line "∀m n, (m <= n) <=> (∃d, n = (m + d))") *)
221
222
223
224
225
226
227
228
229
230
231
232
233
234

species HolLe =
  inherit NatLe, HolPlus;
  logical let le (m, n) = hol_le(m, n);
  proof of le_plus = by definition of le, plus property hol_le_plus;
end;;

collection HolLeColl = implement HolLe; end;;

(* NatDivides *)

let hol_divides (p : hnat, q : hnat) : bool =
  internal bool
  external
Raphael Cauderlier's avatar
Raphael Cauderlier committed
235
  | dedukti -> {* HolNaturals.Number_2ENatural_2Edivides p q *};;
236
237
238

theorem hol_divides_times1 : all m n : hnat,
  hol_divides (m, n) <-> (ex p : hnat, hol_times(p, m) = n)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
239
proof = dedukti proof {* HolNaturals.thm_241. *};;
240
(* (update-thm-number-on-previous-line "∀a b, (divides a b) <=> (∃c, (c * a) = b)") *)
241
242
243
244
245
246
247
248
249
250

theorem hol_divides_times2 : all m n : hnat,
  hol_divides (m, n) <-> (ex p : hnat, hol_times(m, p) = n)
proof = by property hol_divides_times1, hol_times_commute;;

(* NatLt *)

let hol_lt(m : hnat, n : hnat) =
  internal bool
  external
Raphael Cauderlier's avatar
Raphael Cauderlier committed
251
  | dedukti -> {* HolNaturals.Number_2ENatural_2E_3C m n *};;
252
253

theorem hol_lt_le : all m n : hnat, hol_le(hsucc(m), n) <-> hol_lt(m, n)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
254
proof = dedukti proof {* HolNaturals.thm_189. *};;
255
(* (update-thm-number-on-previous-line "∀m n, ((suc m) <= n) <=> (m < n)") *)
256
257

theorem hol_lt_zero : all m : hnat, ~(hol_lt(m, hzero))
Raphael Cauderlier's avatar
Raphael Cauderlier committed
258
proof = dedukti proof {* HolNaturals.thm_104. *};;
259
(* (update-thm-number-on-previous-line "∀m, ~ (m < zero)") *)
260
261

theorem hol_le_zero : all n : hnat, hol_le(hzero, n)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
262
proof = dedukti proof {* HolNaturals.thm_1348. *};;
263
(* (update-thm-number-on-previous-line "∀n, zero <= n") *)
264
265

theorem hol_le_lt : all m n : hnat, hol_le(m, n) <-> (hol_lt(m, n) \/ m = n)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
266
proof = dedukti proof {* HolNaturals.thm_2162. *};;
267
(* (update-thm-number-on-previous-line "∀m n, (m <= n) <=> ((m < n) \\/ (m = n))") *)
268
269
270
271
272

theorem hol_lt_one : all m : hnat, (m = hzero \/ (m = hsucc(hzero) \/ hol_lt(hsucc(hzero), m)))
proof = by property hol_le_zero, hol_le_lt, hol_lt_le;;

theorem hol_lt_irrefl : all n : hnat, ~(hol_lt(n, n))
Raphael Cauderlier's avatar
Raphael Cauderlier committed
273
proof = dedukti proof {* HolNaturals.thm_201. *};;
274
(* (update-thm-number-on-previous-line "∀n, ~ (n < n)") *)
275
276
277
278
279
280
281
282
283
284
285

species HolLt =
  inherit NatLt, HolLe;
  logical let lt(m, n) = hol_lt(m, n);
  proof of lt_spec = by definition of lt, le, succ
                        property hol_lt_le;
end;;

collection HolLtColl = implement HolLt; end;;

theorem hol_divides_le : all m n : hnat, (~(n = hzero) /\ hol_divides(m, n)) -> hol_le(m, n)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
286
proof = dedukti proof {* HolNaturals.thm_232. *};;
287
(* (update-thm-number-on-previous-line "∀a b, ((~ (b = zero)) /\\ (divides a b)) ==> (a <= b)") *)
288
289
290
291
292
293

species HolDiv =
  inherit NatDivides, HolTimes, HolLt;
  logical let divides (p, q) = hol_divides(p, q);
  proof of divides_times = by definition of divides, times property hol_divides_times2;

294
295
  theorem divides_le : all m n : Self, divides(m, n) -> le(succ(succ(zero)), n) -> le(m, n)
  proof =
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
  <1>1 assume m n : Self,
       hypothesis H1 : divides(m, n),
       hypothesis H2 : le(succ(succ(zero)), n),
       prove le(m, n)
       <2>1 prove ((~ n = zero) /\ divides(m, n)) -> le(m, n)
            by property hol_divides_le definition of zero, divides, le
       <2>2 prove divides(m, n) by hypothesis H1
       <2>3 hypothesis H3 : n = zero,
            prove false
            <3>1 prove lt(succ(zero), zero)
                 by property lt_spec hypothesis H2, H3
            <3>2 prove ~ lt(succ(zero), zero)
                 by definition of lt, zero
                    property hol_lt_zero
            <3>f conclude
       <2>f conclude
  <1>f conclude;
end;;

(* Dummy implementation to check that the species HolDiv is full. *)
collection HolDivColl = implement HolDiv; end;;

(* NatPrime *)

let hol_prime (p : hnat) : bool =
  internal bool
  external
Raphael Cauderlier's avatar
Raphael Cauderlier committed
323
  | dedukti -> {* HolNaturals.Number_2ENatural_2Eprime p *};;
324
325
326
327
328
329
330
331

(* The definition of prime in OpenTheory refers to the constant 1
   written in binary so we first need to import it and prove it is
   indeed equal to succ(zero). *)

(* Adding a zero in binary (mulitplication by 2) *)
let b0 (n : hnat) =
  internal hnat
Raphael Cauderlier's avatar
Raphael Cauderlier committed
332
  external | dedukti -> {* HolNaturals.Number_2ENatural_2Ebit0 n *};;
333
334

theorem b0_zero : b0(hzero) = hzero
Raphael Cauderlier's avatar
Raphael Cauderlier committed
335
proof = dedukti proof {* HolNaturals.thm_112. *};;
336
(* (update-thm-number-on-previous-line "(bit0 zero) = zero") *)
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351

(* Adding a one in binary (n => 2*n + 1) *)
let b1 (n : hnat) = hsucc (b0(n));;

(* The binary constant one *)
let hol_one = b1 (hzero);;

(* One is the successor of zero *)
theorem hol_one_succ : hol_one = hsucc (hzero)
proof = by property b0_zero definition of b1, hol_one;;

theorem hol_prime_def : all p : hnat,
        hol_prime(p) <->
          ((~(p = hol_one)) /\
           all n : hnat, hol_divides(n, p) -> (n = hol_one \/ n = p))
Raphael Cauderlier's avatar
Raphael Cauderlier committed
352
proof = dedukti proof {* HolNaturals.thm_227. *};;
353
(* (update-thm-number-on-previous-line "∀p, (prime p) <=> ((~ (p = (bit1 zero))) /\\ (∀n, (divides n p) ==> ((n = (bit1 zero)) \\/ (n = p))))") *)
354
355

theorem hol_prime_zero : ~(hol_prime(hzero))
Raphael Cauderlier's avatar
Raphael Cauderlier committed
356
proof = dedukti proof {* HolNaturals.thm_14422. *};;
357
(* (update-thm-number-on-previous-line "~ (prime zero)") *)
358
359

theorem hol_prime_one : ~(hol_prime(hol_one))
Raphael Cauderlier's avatar
Raphael Cauderlier committed
360
proof = dedukti proof {* HolNaturals.thm_14428. *};;
361
(* (update-thm-number-on-previous-line "~ (prime (bit1 zero))") *)
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498

species HolPrime =
  inherit NatPrime, HolDiv, HolLt;
  logical let prime (p) = hol_prime(p);
  proof of prime_1 =
  <1>1 assume p : Self,
       hypothesis H1 : prime(p),
       prove lt(succ(zero), p)
       <2>1 hypothesis H : p = zero,
            prove false
            by definition of zero, succ, prime
               hypothesis H, H1
               property hol_prime_zero
       <2>2 hypothesis H : p = succ(zero),
            prove false
            by definition of zero, succ, prime
               hypothesis H, H1
               property hol_prime_one, hol_one_succ
       <2>3 prove (p = zero \/ (p = succ(zero) \/ lt(succ(zero), p)))
            dedukti proof
               definition of lt, succ, zero
               {* hol_lt_one p *}
       <2>4 prove (p = succ(zero) \/ lt(succ(zero), p))
            by step <2>1, <2>3
       <2>f conclude
  <1>f conclude;
  proof of prime_sd =
  <1>1 assume p d : Self,
       hypothesis Hp : prime(p),
       hypothesis Hd : sd(d, p),
       prove false
       <2>1 prove divides(d, p)
            by property sd_divides hypothesis Hd
       <2>2 prove (d = hol_one \/ d = p)
            by property hol_prime_def
               definition of prime, divides
               hypothesis Hp step <2>1
       <2>3 hypothesis H1 : d = hol_one,
            prove false
            <3>1 prove lt(succ(zero), d)
                 by property sd_1 hypothesis Hd
            <3>2 prove lt(succ(zero), hol_one)
                 by step <3>1 hypothesis H1
            <3>3 prove lt(succ(zero), succ(zero))
                 by step <3>2
                    property hol_one_succ
                    definition of succ, zero
            <3>4 qed by step <3>3
                        property hol_lt_irrefl
                        definition of lt
       <2>4 hypothesis H1 : d = p,
            prove false
            <3>1 prove lt(d, p)
                 by property sd_lt hypothesis Hd
            <3>2 prove lt(p, p)
                 by step <3>1 hypothesis H1
            <3>3 prove ~(lt(p, p))
                 by property hol_lt_irrefl
                    definition of lt
            <3>f conclude
       <2>f conclude
   <1>f conclude;
  proof of prime_intro =
  <1>1 assume p : Self,
       hypothesis H1 : lt(succ(zero), p),
       hypothesis Hd : all d : Self, ~(sd(d, p)),
       prove prime(p)
       <2>1 hypothesis Hp1 : p = hol_one,
            prove false
            <3>1 prove lt(succ(zero), hol_one)
                 by hypothesis H1, Hp1
            <3>2 prove lt(hol_one, hol_one)
                 by step <3>1 property hol_one_succ definition of succ, zero
            <3>3 prove ~(lt(hol_one, hol_one))
                 by property hol_lt_irrefl definition of lt
            <3>f conclude
       <2>2 assume n : Self,
            hypothesis Hn : divides(n, p),
            prove (n = hol_one \/ n = p)
            <3>1 prove ~(sd(n, p))
                 by hypothesis Hd
            <3>2 hypothesis Hnot : ~(n = hol_one),
                 hypothesis Hp : ~(n = p),
                 prove false
                 <4>a hypothesis Hpz : p = zero,
                      prove false
                      <5>1 prove lt(succ(zero), zero)
                           by hypothesis H1, Hpz
                      <5>2 prove ~(lt(succ(zero), zero))
                           by property hol_lt_zero
                           definition of zero, lt
                      <5>f conclude
                 <4>0 prove le(n, p)
                      by property hol_divides_le
                         hypothesis Hn
                         step <4>a
                         definition of le, divides, zero
                 <4>1 prove lt(n, p)
                      by hypothesis Hp step <4>0
                         property hol_le_lt
                         definition of le, lt
                 <4>2 hypothesis H0 : n = zero,
                      prove false
                      <5>1 prove ex k : Self, times(zero, k) = p
                           by property divides_times hypothesis H0, Hn
                      <5>2 prove zero = p
                           by step <5>1 property zero_times
                      <5>f qed by step <5>2, <4>a
                 <4>3 prove lt(succ(zero), n)
                      by property hol_lt_one, hol_one_succ
                         definition of succ, zero, lt
                         hypothesis Hnot
                         step <4>2
                 <4>4 prove sd(n, p)
                      by property sd_intro
                         hypothesis Hn
                         step <4>3, <4>1
                 <4>f qed by step <4>4, <3>1
             <3>f conclude
       <2>3 prove
          ((~(p = hol_one)) /\
           all n : hnat, divides(n, p) -> (n = hol_one \/ n = p))
           by step <2>1, <2>2
       <2>f qed by step <2>3 property hol_prime_def definition of divides, prime
   <1>f conclude;
end;;

collection HolPrimeColl =
  implement HolPrime;
end;;


(* Retrieving our theorem from OpenTheory. *)

theorem hol_prime_divisor :
  all n : hnat,
  (~(n = hol_one)) -> ex p : hnat, hol_prime(p) /\ hol_divides(p, n)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
499
proof = dedukti proof {* HolNaturals.thm_14683. *};;
500
(* (update-thm-number-on-previous-line "∀n, (~ (n = (bit1 zero))) ==> (∃p, (prime p) /\\ (divides p n))") *)
501

502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
(* species HolPrimeDiv = *)
(*   inherit NatPrimeDiv, HolPrime; *)
(*   proof of prime_divisor = *)
(*   by property hol_prime_divisor, hol_one_succ *)
(*      definition of prime, divides, succ, zero; *)

(*   let primediv_pred (n : hnat, p : hnat) = internal bool *)
(*   external | dedukti -> {* hol.and (hol_prime p) (hol_divides p n) *}; *)
(*   proof of primediv_pred_spec = *)
(*   <1>1 assume n p : Self, *)
(*        prove (primediv_pred(n, p) <-> (prime(p) /\ divides(p, n))) *)
(*        dedukti proof definition of primediv_pred, prime, divides *)
(*          {* hol.REFL hol.bool (abst_primediv_pred n p) *} *)
(*   <1>f conclude; *)
(* end;; *)

(* collection HolPrimeDivColl = *)
(*   implement HolPrimeDiv; *)
(* end;; *)