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
|
\DOC associate_restriction
\TYPE {associate_restriction : ((string # string) -> void)}
\SYNOPSIS
Associates a restriction semantics with a binder.
\DESCRIBE
If {B} is a binder and {RES_B} a constant then
{
associate_restriction(`B`, `RES_B`)
}
\noindent will cause the parser and pretty-printer to support:
{
---- parse ---->
Bv::P. B RES_B P (\v. B)
<---- print ----
}
Anything can be written between the binder and {`::`} that could be
written between the binder and {`.`} in the old notation. See the
examples below.
Associations between user defined binders and their restrictions are not
stored in the theory, so they have to be set up for each hol session
(e.g. with a {hol-init.ml} file).
The flag {`print_restrict`} has default {true}, but if set to {false} will
disable the pretty printing. This is useful for seeing what the
semantics of particular restricted abstractions are.
The following associations are predefined:
{
\v::P. B <----> RES_ABSTRACT P (\v. B)
!v::P. B <----> RES_FORALL P (\v. B)
?v::P. B <----> RES_EXISTS P (\v. B)
@v::P. B <----> RES_SELECT P (\v. B)
}
Where the constants {RES_ABSTRACT}, {RES_FORALL}, {RES_EXISTS} and
{RES_SELECT} are defined in the theory {`bool`} by:
{
|- RES_ABSTRACT P B = \x:*. (P x => B x | ARB:**)
|- RES_FORALL P B = !x:*. P x ==> B x
|- RES_EXISTS P B = ?x:*. P x /\ B x
|- RES_SELECT P B = @x:*. P x /\ B x
}
where {ARB} is defined in the theory {`bool`} by:
{
|- ARB = @x:*. T
}
\FAILURE
Never fails.
\EXAMPLE
{
#new_binder_definition(`DURING`, "DURING(p:num#num->bool) = $!p");;
|- !p. $DURING p = $! p
#"DURING x::(m,n). p x";;
no restriction constant associated with DURING
skipping: x " ;; parse failed
#new_definition
# (`RES_DURING`, "RES_DURING(m,n)p = !x. m<=x /\ x<=n ==> p x");;
|- !m n p. RES_DURING(m,n)p = (!x. m <= x /\ x <= n ==> p x)
#associate_restriction(`DURING`,`RES_DURING`);;
() : void
#"DURING x::(m,n). p x";;
"DURING x :: (m,n). p x" : term
#set_flag(`print_restrict`,false);;
true : bool
#"DURING x::(m,n). p x";;
"RES_DURING(m,n)(\x. p x)" : term
}
\ENDDOC
|
