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
|
\DOC new_list_rec_definition
\TYPE {new_list_rec_definition : ((string # term) -> thm)}
\SYNOPSIS
Defines a primitive recursive function over the type of lists.
\DESCRIBE
The function {new_list_rec_definition} provides the facility for defining
primitive recursive functions on the type of lists. It takes a pair argument,
consisting of the name under which the resulting definition will be saved in
the current theory segment, and a term giving the desired definition. The
value returned by {new_list_rec_definition} is a theorem which states the
definition requested by the user. This theorem is derived by formal proof from
an instance of the theorem {list_Axiom}:
{
|- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t)
}
Evaluating
{
new_list_rec_definition
(`fun_DEF`,
"(fun x_1 ... [] ... x_i = f_1[x_1, ..., x_i]) /\
(fun x_1 ... (CONS h t) ... x_i =
f_2[fun t_1 ... t ... t_i, x_1, ..., h, t, ..., x_i])");;
}
\noindent where all the free variables in the terms {t_1}, ..., {t_i} are
contained in {{{h,t,x_1,...,x_i}}}, automatically proves the theorem:
{
|- ?fun. !x_1 ... x_i. fun x_1 ... [] ... x_i = f_1[x_1, ..., x_i] /\
!x_1 ... x_i. fun (CONS h t) x_1 ... x_i =
f_2[fun t_1 ... t ... t_i, x_1, ..., h, t, ...,x_i]
}
\noindent and then declares a new constant {fun} with this property as its
specification. This constant specification is returned as a theorem by
{new_list_rec_definition} and is saved with name {fun_DEF} in the
current theory segment.
The ML function {new_list_rec_definition} also allows the user to
partially specify the value of a function defined (possibly recursively) on
lists by giving its value for only one of {[]} or {CONS h t}. See the
examples below.
\FAILURE
Failure occurs if HOL cannot prove there is a function satisfying the
specification (ie. if the term supplied to ml{new_list_rec_definition}
is not a well-formed primitive recursive definition), or if
any other condition for making a constant specification is violated
(see the failure conditions for {new_specification}).
\EXAMPLE
The HOL system defines a length function, {LENGTH}, on lists by the
primitive recursive definition on lists shown below:
{
new_list_rec_definition
(`LENGTH`,
"(LENGTH NIL = 0) /\
(!h:*. !t. LENGTH (CONS h t) = SUC (LENGTH t))")
}
\noindent When this ML expression is evaluated, HOL uses {list_Axiom}
to prove existence of a function that satisfies the given primitive
recursive definition, introduces a constant to name this function
using a constant specification, and stores the resulting theorem:
{
LENGTH |- (LENGTH[] = 0) /\ (!h t. LENGTH(CONS h t) = SUC(LENGTH t))
}
\noindent in the current theory segment (in this case, the theory {list}).
Using {new_list_rec_definition}, the predicate {NULL} and the
selectors {HD} and {TL} are defined
in the theory {list} by the
specifications:
{
NULL |- NULL[] /\ (!h t. ~NULL(CONS h t))
HD |- !(h:*) t. HD(CONS h t) = h
TL |- !(h:*) t. TL(CONS h t) = t
}
\SEEALSO
new_definition, new_infix_definition, new_infix_list_rec_definition,
new_infix_prim_rec_definition, new_prim_rec_definition,
new_recursive_definition, new_type_definition, new_specification, list_Axiom.
\ENDDOC
|
