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