1\DOC Hol_defn
2
3\TYPE {Hol_defn : string -> term quotation -> defn}
4
5\SYNOPSIS
6General-purpose function definition facility.
7
8\KEYWORDS
9definition, recursive definition.
10
11
12
13\DESCRIBE
14{Hol_defn} allows one to define functions, recursive functions in
15particular, while deferring termination issues.  {Hol_defn} should be
16used when {Define} or {xDefine} fails, or when the context required by
17{Define} or {xDefine} is too much.
18
19{Hol_defn} takes the same arguments as {xDefine}.
20
21{Hol_defn s q} automatically constructs termination constraints for the
22function specified by {q}, defines the function, derives the specified
23equations, and proves an induction theorem. All these results are
24packaged up in the returned {defn} value. The {defn} type is best
25thought of as an intermediate step in the process of deriving the
26unconstrained equations and induction theorem for the function.
27
28The termination conditions constructed by {Hol_defn} are for a function
29that takes a single tuple as an argument. This is an artifact of the
30way that recursive functions are modelled.
31
32A prettyprinter, which prints out a summary of the known information on
33the results of {Hol_defn}, has been installed in the interactive system.
34
35{Hol_defn} may be found in {bossLib} and also in {Defn}.
36
37
38
39\FAILURE
40{Hol_defn s q} fails if {s} is not an alphanumeric identifier.
41
42{Hol_defn s q} fails if {q} fails to parse or typecheck.
43
44{Hol_defn} may extract unsatisfiable termination conditions when asked
45to define a higher-order recursion involving a higher-order function
46that the termination condition extraction mechanism of {Hol_defn} is
47unaware of.
48
49
50
51\EXAMPLE
52Here we attempt to define a quick-sort function {qsort}:
53{
54   - Hol_defn "qsort"
55         `(qsort ___ [] = []) /\
56          (qsort ord (x::rst) =
57             APPEND (qsort ord (FILTER ($~ o ord x) rst))
58               (x :: qsort ord (FILTER (ord x) rst)))`;
59
60   <<HOL message: inventing new type variable names: 'a>>
61   > val it =
62       HOL function definition (recursive)
63
64       Equation(s) :
65        [...]
66       |- (qsort v0 [] = []) /\
67          (qsort ord (x::rst) =
68           APPEND (qsort ord (FILTER ($~ o ord x) rst))
69             (x::qsort ord (FILTER (ord x) rst)))
70
71       Induction :
72        [...]
73       |- !P.
74            (!v0. P v0 []) /\
75            (!ord x rst.
76               P ord (FILTER ($~ o ord x) rst) /\
77               P ord (FILTER (ord x) rst) ==> P ord (x::rst))
78              ==> !v v1. P v v1
79
80       Termination conditions :
81         0. WF R
82         1. !rst x ord. R (ord,FILTER ($~ o ord x) rst) (ord,x::rst)
83         2. !rst x ord. R (ord,FILTER (ord x) rst) (ord,x::rst)
84}
85In the following we give an example of how to use {Hol_defn} to define a
86nested recursion.  In processing this definition, an auxiliary function
87{N_aux} is defined.  The termination conditions of {N} are phrased in
88terms of {N_aux} for technical reasons.
89{
90   - Hol_defn "ninety1"
91       `N x = if x>100 then x-10
92                       else N(N(x+11))`;
93
94   > val it =
95       HOL function definition (nested recursion)
96
97       Equation(s) :
98        [...] |- N x = (if x > 100 then x - 10 else N (N (x + 11)))
99
100       Induction :
101        [...]
102       |- !P.
103            (!x. (~(x > 100) ==> P (x + 11)) /\
104                 (~(x > 100) ==> P (N (x + 11))) ==> P x)
105            ==>
106             !v. P v
107
108       Termination conditions :
109         0. WF R
110         1. !x. ~(x > 100) ==> R (x + 11) x
111         2. !x. ~(x > 100) ==> R (N_aux R (x + 11)) x
112}
113
114\COMMENTS
115An invocation of {Hol_defn} is usually the first step in a multi-step
116process that ends with unconstrained recursion equations for a
117function, along with an induction theorem. {Hol_defn} is used to
118construct the function and synthesize its termination conditions;
119next, one invokes {tgoal} to set up a goal to prove termination of the
120function.  The termination proof usually starts with an invocation of
121{WF_REL_TAC}. After the proof is over, the desired recursion equations
122and induction theorem are available for further use.
123
124It is occasionally important to understand, at least in part, how
125{Hol_defn} constructs termination constraints. In some cases, it is
126necessary for users to influence this process in order to have correct
127termination constraints extracted. The process is driven by so-called
128congruence theorems for particular HOL constants. For example, suppose
129we were interested in defining a `destructor-style` version of the
130factorial function over natural numbers:
131{
132   fact n = if n=0 then 1 else n * fact (n-1).
133}
134
135In the absence of a congruence theorem for the `if-then-else` construct,
136{Hol_defn} would extract the termination constraints
137{
138   0. WF R
139   1. !n. R (n - 1) n
140}
141
142which are unprovable, because the context of the recursive call has not
143been taken account of. This example is in fact not a problem for HOL,
144since the following congruence theorem is known to {Hol_defn}:
145{
146   |- !b b' x x' y y'.
147         (b = b') /\
148         (b' ==> (x = x')) /\
149         (~b' ==> (y = y')) ==>
150         ((if b then x else y) = (if b' then x' else y'))
151}
152
153This theorem is interpreted by {Hol_defn} as an ordered sequence of
154instructions to follow when the termination condition extractor hits an
155`if-then-else`. The theorem is read as follows:
156{
157   When an instance `if B then X else Y` is encountered while the
158   extractor traverses the function definition, do the following:
159
160     1. Go into B and extract termination conditions TCs(B) from
161        any recursive calls in it. This returns a theorem
162        TCs(B) |- B = B'.
163
164     2. Assume B' and extract termination conditions from any
165        recursive calls in X. This returns a theorem
166        TCs(X) |- X = X'. Each element of TCs(X) will have
167        the form "B' ==> M".
168
169     3. Assume ~B' and extract termination conditions from any
170        recursive calls in Y. This returns a theorem
171        TCs(Y) |- Y = Y'. Each element of TCs(Y) will have
172        the form "~B' ==> M".
173
174     4. By equality reasoning with (1), (2), and (3), derive
175
176            TCs(B) u TCs(X) u TCs(Y)
177             |-
178            (if B then X else Y) = (if B' then X' else Y')
179
180     5. Replace "if B then X else Y" by "if B' then X' else Y'".
181}
182
183The accumulated termination conditions are propagated until the
184extraction process finishes, and appear as hypotheses in the final
185result. In our example, context is properly accounted for in recursive
186calls under either branch of an `if-then-else`. Thus the extracted
187termination conditions for {fact} are
188{
189   0. WF R
190   1. !n. ~(n = 0) ==> R (n - 1) n
191}
192and are easy to prove.
193
194Now we discuss congruence theorems for higher-order functions. A
195`higher-order` recursion is one in which a higher-order function is
196used to apply the recursive function to arguments. In order for the
197correct termination conditions to be proved for such a recursion,
198congruence rules for the higher order function must be known to
199the termination condition extraction mechanism. Congruence rules for
200common higher-order functions, e.g., {MAP}, {EVERY}, and {EXISTS} for
201lists, are already known to the mechanism. However, at times, one must
202manually prove and install a congruence theorem for a higher-order
203function.
204
205For example, suppose we define a higher-order function {SIGMA} for
206summing the results of a function in a list. We then use {SIGMA} in
207the definition of a function for summing the results of a function
208in an arbitrarily (finitely) branching tree.
209{
210   - Define `(SIGMA f [] = 0) /\
211             (SIGMA f (h::t) = f h + SIGMA f t)`;
212
213
214   - Hol_datatype `ltree = Node of 'a => ltree list`;
215   > val it = () : unit
216
217   - Defn.Hol_defn
218        "ltree_sigma"     (* higher order recursion *)
219        `ltree_sigma f (Node v tl) = f v + SIGMA (ltree_sigma f) tl`;
220
221   > val it =
222     HOL function definition (recursive)
223
224       Equation(s) :
225        [..] |- ltree_sigma f (Node v tl)
226                  = f v + SIGMA (\a. ltree_sigma f a) tl
227
228       Induction :
229        [..] |- !P. (!f v tl. (!a. P f a) ==> P f (Node v tl))
230                    ==> !v v1. P v v1
231
232       Termination conditions :
233         0. WF R
234         1. !tl v f a. R (f,a) (f,Node v tl) : defn
235}
236The termination conditions for {ltree_sigma} seem to require finding a
237well-founded relation {R} such that the pair {(f,a)} is {R}-less than
238{(f, Node v tl)}. However, this is a hopeless task, since there is no
239relation between {a} and {Node v tl}, besides the fact that they are
240both {ltree}s. The termination condition extractor has not performed
241properly, because it didn't know a congruence rule for {SIGMA}. Such a
242congruence theorem is the following:
243{
244   SIGMA_CONG =
245    |- !l1 l2 f g.
246         (l1=l2) /\ (!x. MEM x l2 ==> (f x = g x)) ==>
247         (SIGMA f l1 = SIGMA g l2)
248}
249Once {Hol_defn} has been told about this theorem, via {write_congs}, the
250termination conditions extracted for the definition are provable,
251since {a} is a proper subterm of {Node v tl}.
252{
253   - local open DefnBase
254     in
255     val _ = write_congs (SIGMA_CONG::read_congs())
256     end;
257
258   - Defn.Hol_defn
259        "ltree_sigma"
260        `ltree_sigma f (Node v tl) = f v + SIGMA (ltree_sigma f) tl`;
261
262   > val it =
263       HOL function definition (recursive)
264
265       Equation(s) :  ...  (* as before *)
266       Induction :    ...  (* as before *)
267
268       Termination conditions :
269         0. WF R
270         1. !v f tl a. MEM a tl ==> R (f,a) (f,Node v tl)
271}
272
273One final point : for every HOL datatype defined by application of
274{Hol_datatype}, a congruence theorem is automatically proved for the
275`case' constant for that type, and stored in the {TypeBase}. For example,
276the following congruence theorem for {num_case} is stored in the {TypeBase}:
277{
278    |- !f' f b' b M' M.
279         (M = M') /\
280         ((M' = 0) ==> (b = b')) /\
281         (!n. (M' = SUC n) ==> (f n = f' n))
282        ==>
283         (num_case b f M = num_case b' f' M')
284}
285This allows the contexts of recursive calls in branches of
286`case' expressions to be tracked.
287
288\SEEALSO
289Defn.tgoal, Defn.tprove, bossLib.WF_REL_TAC, bossLib.Define,
290bossLib.xDefine, bossLib.Hol_datatype.
291
292\ENDDOC
293