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
|
; (certify-book "equisort2")
; Suppose sortfn1 and sortfn2 are two arbitrary unary functions that return
; ordered results that preserve the how-many property for every object e. Then
; they are equal.
; I constrain sortfn1 and sortfn2 and then prove this. Thus, when one
; functionally instantiates sortfn1-is-sortfn2 below, replacing the two generic
; names by specific sorting functions, nice proof obligations are produced:
; each sorting function must return an ordered list that preserves the how-many
; property.
(in-package "ACL2")
(include-book "perm")
(include-book "ordered-perms")
(include-book "convert-perm-to-how-many")
(encapsulate ((sorthyp (x) t)
(sortfn1 (x) t)
(sortfn2 (x) t))
(local (defun sorthyp (x) (true-listp x)))
(local (defun sortfn1-insert (e x)
(if (endp x)
(cons e x)
(if (lexorder e (car x))
(cons e x)
(cons (car x)
(sortfn1-insert e (cdr x)))))))
(local (defun sortfn1 (x)
(if (endp x)
nil
(sortfn1-insert (car x)
(sortfn1 (cdr x))))))
(local (defun sortfn2 (x) (sortfn1 x)))
(defthm orderedp-sortfn1
(orderedp (sortfn1 x)))
(defthm true-listp-sortfn1
(implies (sorthyp x)
(true-listp (sortfn1 x))))
(defthm orderedp-sortfn2
(orderedp (sortfn2 x)))
(defthm true-listp-sortfn2
(implies (sorthyp x)
(true-listp (sortfn2 x))))
(defthm how-many-sortfn1
(equal (how-many e (sortfn1 x))
(how-many e x)))
(defthm how-many-sortfn2
(equal (how-many e (sortfn2 x))
(how-many e x))))
(defthm sortfn1-is-sortfn2
(implies (sorthyp x)
(equal (sortfn1 x) (sortfn2 x)))
:rule-classes nil
:hints (("Goal" :use (:instance ordered-perms
(a (sortfn1 x))
(b (sortfn2 x))))))
|
