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
|
\DOC new_infix_prim_rec_definition
\TYPE {new_infix_prim_rec_definition : ((string # term) -> thm)}
\SYNOPSIS
Defines an infix primitive recursive function over the type {num}.
\DESCRIBE
The function {new_infix_prim_rec_definition} provides the facility for defining
primitive recursive functions with infix status on the type {num}. 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_infix_prim_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 {num_Axiom}:
{
|- !e f. ?! fn. (fn 0 = e) /\ (!n. fn(SUC n) = f(fn n)n)
}
\noindent Evaluating
{
new_infix_prim_rec_definition
(`fun_DEF`,
"(fun 0 x = f_1[x]) /\
(fun (SUC n) x = f_2[fun n x', n, x])");;
}
\noindent where all the free variables in the term {x'} are
contained in {{{n, x}}}, automatically proves the theorem:
{
|- ?fun. !x. fun 0 x = f_1[x] /\
!x. fun (SUC n) x = f_2[fun n x', n, x]
}
\noindent and then declares a new constant {fun} with this property and infix
status as its specification. This constant specification is returned as a
theorem and is saved with name {fun_DEF} in the current theory segment.
The ML function {new_infix_prim_rec_definition} is, in fact, slightly more
general than is indicated above. In particular, a curried primitive recursive
function can be defined by primitive recursion on either one of its arguments
using this ML function. The ML function {new_infix_prim_rec_definition} also
allows the user to partially specify the value of a function defined (possibly
recursively) on the natural numbers by giving its value for only one of {0} or
{SUC n}.
\FAILURE
Failure occurs if HOL cannot prove there is a function satisfying the
specification (ie. if the term supplied to {new_prim_rec_definition} is not a
well-formed primitive recursive definition); if the type of {fun} is not of the
form {ty_1->ty_2->ty_3}, or if any other condition for making a constant
specification is violated (see the failure conditions for {new_specification}).
\EXAMPLE
Here is the recursive definition of the constant {+} used by the system:
{
new_infix_prim_rec_definition
(`ADD`,
"($+ 0 n = n) /\
($+ (SUC m) n = SUC($+ m n))")
}
\noindent The {$}'s are there (as documentation) to indicate that the constant
{+} is being declared to be an infix. Evaluating this ML expression will
create the following constant specification in the current theory segment:
{
ADD = |- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n))
}
\SEEALSO
new_definition, new_infix_definition, new_infix_list_rec_definition,
new_prim_rec_definition, new_list_rec_definition, new_recursive_definition,
new_type_definition, new_specification, num_Axiom.
\ENDDOC
|
