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
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
\DOC RES_CANON
\TYPE {RES_CANON : (thm -> thm list)}
\SYNOPSIS
Put an implication into canonical form for resolution.
\KEYWORDS
rule, resolution, implication, canonical.
\DESCRIBE
All the HOL resolution tactics (e.g. {IMP_RES_TAC}) work by using modus ponens
to draw consequences from an implicative theorem and the assumptions of the
goal. Some of these tactics derive this implication from a theorem supplied
explicitly the user (or otherwise from `outside' the goal) and some obtain it
from the assumptions of the goal itself. But in either case, the supplied
theorem or assumption is first transformed into a list of implications in
`canonical' form by the function {RES_CANON}.
The theorem argument to {RES_CANON} should be either be an implication (which
can be universally quantified) or a theorem from which an implication can be
derived using the transformation rules discussed below. Given such a theorem,
{RES_CANON} returns a list of implications in canonical form. It is the
implications in this resulting list that are used by the various resolution
tactics to infer consequences from the assumptions of a goal.
The transformations done by {RES_CANON th} to the theorem {th} are as follows.
First, if {th} is a negation {A |- ~t}, this is converted to the implication
{A |- t ==> F}. The following inference rules are then applied
repeatedly, until no further rule applies. Conjunctions are split into their
components and equivalence (boolean equality) is split into implication in
both directions:
{
A |- t1 /\ t2 A |- t1 = t2
-------------------- ----------------------------------
A |- t1 A |- t2 A |- t1 ==> t2 A |- t2 ==> t1
}
\noindent Conjunctive antecedents are transformed by:
{
A |- (t1 /\ t2) ==> t
---------------------------------------------------
A |- t1 ==> (t2 ==> t) A |- t2 ==> (t1 ==> t)
}
\noindent and disjunctive antecedents by:
{
A |- (t1 \/ t2) ==> t
--------------------------------
A |- t1 ==> t A |- t2 ==> t
}
\noindent The scope of universal quantifiers is restricted, if possible:
{
A |- !x. t1 ==> t2
-------------------- [if x is not free in t1]
A |- t1 ==> !x. t2
}
\noindent and existentially-quantified antecedents are eliminated by:
{
A |- (?x. t1) ==> t2
--------------------------- [x' chosen so as not to be free in t2]
A |- !x'. t1[x'/x] ==> t2
}
\noindent Finally, when no further applications of the above rules are
possible, and the theorem is an implication:
{
A |- !x1...xn. t1 ==> t2
}
\noindent then the theorem {A u {{t1}} |- t2} is transformed by a recursive
application of {RES_CANON} to get a list of theorems:
{
[A u {{t1}} |- t21 ; ... ; A u {{t1}} |- t2n]
}
\noindent and the result of discharging {t1} from these theorems:
{
[A |- !x1...xn. t1 ==> t21 ; ... ; A |- !x1...xn. t1 ==> t2n]
}
\noindent is returned. That is, the transformation rules are recursively
applied to the conclusions of all implications.
\FAILURE
{RES_CANON th} fails if no implication(s) can be derived from {th} using the
transformation rules shown above.
\EXAMPLE
The uniqueness of the remainder {k MOD n} is expressed in HOL by the built-in
theorem {MOD_UNIQUE}:
{
|- !n k r. (?q. (k = (q * n) + r) /\ r < n) ==> (k MOD n = r)
}
\noindent For this theorem, the canonical list of implications returned by
{RES_CANON} is as follows:
{
#RES_CANON MOD_UNIQUE;;
[|- !k q n r. (k = (q * n) + r) ==> r < n ==> (k MOD n = r);
|- !r n. r < n ==> (!k q. (k = (q * n) + r) ==> (k MOD n = r))]
: thm list
}
\noindent The existentially-quantified, conjunctive, antecedent has given rise
to two implications, and the scope of universal quantifiers has been restricted
to the conclusions of the resulting implications wherever possible.
\USES
The primary use of {RES_CANON} is for the (internal) pre-processing phase of
the built-in resolution tactics {IMP_RES_TAC}, {IMP_RES_THEN}, {RES_TAC}, and
{RES_THEN}. But the function {RES_CANON} is also made available at top-level
so that users can call it to see the actual form of the implications used for
resolution in any particular case.
\SEEALSO
IMP_RES_TAC, IMP_RES_THEN, RES_TAC, RES_THEN.
\ENDDOC
|
