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
|
(in-package "ACL2")
(include-book "generic-partial")
(include-book "misc/defpun" :dir :system)
(local (include-book "arithmetic/top-with-meta" :dir :system))
;; I do the obvious thing, namely define the function clock with the
;; tail-recursive equation so that it drives us to the first moment at
;; which we reach an exitpoint.
(defpun clock-fn-tail (s i)
(if (exitpoint s) i
(clock-fn-tail (step-fn s) (1+ i))))
(defun clock-fn (s)
(clock-fn-tail s 0))
;; Now I know how to prove theorems about these tail-recursive
;; equations. So I just go through them.
(local
(defun cutpoint-induction (k steps s)
(if (zp k) (list k steps s)
(cutpoint-induction (1- k) (1+ steps) (step-fn s)))))
(local
(encapsulate
()
(local
(defthmd clock-fn-tail-inv
(implies (and (exitpoint (run-fn s k))
(natp steps))
(let* ((result (clock-fn-tail s steps))
(exitpoint-steps (- result steps)))
(and (natp result)
(natp exitpoint-steps)
(implies (natp k)
(<= exitpoint-steps k))
(exitpoint (run-fn s exitpoint-steps)))))
:hints (("Goal"
:in-theory (enable natp)
:induct (cutpoint-induction k steps s)))))
(defthm clock-fn-is-natp
(implies (exitpoint (run-fn s k))
(natp (clock-fn s)))
:rule-classes (:rewrite
; :forward-chaining ;fcd/Satriani v3.7 Moore
:type-prescription)
:hints (("Goal"
:use ((:instance clock-fn-tail-inv
(steps 0))))))
(defthm clock-fn-provide-exitpoint
(implies (exitpoint (run-fn s k))
(exitpoint (run-fn s (clock-fn s))))
:hints (("Goal"
:use ((:instance clock-fn-tail-inv
(steps 0))))))
(defthm clock-fn-is-minimal
(implies (and (exitpoint (run-fn s k))
(natp k))
(<= (clock-fn s)
k))
:rule-classes :linear
:hints (("Goal"
:use ((:instance clock-fn-tail-inv
(steps 0))))))))
(local (in-theory (disable clock-fn)))
;; Now I prove that the first thing to reach an exitpoint is the clock
;; function.
(local
(defthm n-is-first-reduces-to-clock
(implies (and (n-is-first s n)
(exitpoint (run-fn s n))
(natp n)
(pre s))
(equal (clock-fn s) n))
:hints (("Goal"
:use ((:instance n-is-first-necc
(m (clock-fn s))))))))
;; And finally I just prove the desired clock function theorems.
(defthm |clock fn is natp|
(implies (and (pre s)
(exitpoint (run-fn s n)))
(natp (clock-fn s)))
:rule-classes :type-prescription)
(defthm |clock fn is minimal|
(implies (and (pre s)
(natp n)
(exitpoint (run-fn s n)))
(<= (clock-fn s) n))
:rule-classes :linear)
(defthm |clock fn produces exitpoint|
(implies (and (pre s)
(exitpoint (run-fn s n)))
(exitpoint (run-fn s (clock-fn s)))))
(defthm |clock fn produces postcondition|
(implies (and (pre s)
(exitpoint (run-fn s n)))
(post (run-fn s (clock-fn s)))))
|
