Information Technology Reference
In-Depth Information
provisos via incremental proofs. We also importantly preserve the general shape
of an extended refinement theorem during tactic applications. To illustrate this,
we consider the application of a refinement law. In the previous encoding these
laws were typically of the form
∀
v
1
:
T
1
;
...
;
v
n
:
T
n
|
P
[
v
1
,...,
v
n
]
•
A
[
v
1
,...,
v
n
]
B
[
v
1
,...,
v
n
]
with type provisos
v
1
:
T
1
,
v
2
:
T
2
, and so on. The notation
A
[
v
1
,...,
v
n
]isused
to emphasise that the variables
v
i
arefreein
A
. We now rephrase such laws as
∀
v
1
:
U
;
...
;
v
n
:
U
|
wd A
[
v
1
,...,
v
n
]
∧
P
[
v
1
,...,
v
n
]
•
A
[
v
1
,...,
v
n
]
B
[
v
1
,...,
v
n
]
∧
wd B
[
v
1
,...,
v
n
]
.
Here,
is the carrier set of a type that is dynamically inferred by the type
checker. It is maximal, and so only incurs trivial proof obligations. This new
version of the law can be proved from the former by rewriting the
wd
function on
both sides and extracting the type provisos. For example, if
A
is
v
1
∧
P
U
v
2
we have
that
wd
(
v
1
∧
P
v
2
)impliesthatboth
v
1
and
v
2
belong to
ALPHA PREDICATE
.
We observe that all type provisos have been absorbed into just one assertion
wd A
[
v
1
,...,
v
n
] that establishes well-definedness of the left-hand program. If we
apply the new law to an extended refinement theorem Γ
,
wd X
wd Y
,
the right-hand program
Y
is matched against the left-hand program
A
of the
law to instantiate the quantified variables. We then obtain an instantiation
P
,
wd Y
X
Y
∧
wd Y
after moving antecedents to the hypotheses.
The original extended refinement theorem and the instantiated law give rise
to the following four theorems (after eliminating the conjunction in the conclu-
sions): (1) Γ
,
wd X
Y
∧
Y
wd Y
;(3)
P
,
wd Y
Y
;
X
Y
;(2)Γ
,
wd X
Y
(4)
P
,
wd Y
wd Y
. We use (1), (3) and (4) to obtain
(5) Γ
,
P
,
wd X
,
wd Y
Y
∧
wd Y
X
by transitivity of refinement using (1) and (3), and conjunction using (4). The
transitivity model theorem is now recast as
wd p
1
∧
wd p
2
∧
wd p
3
•
p
1
p
2
∧
p
2
p
3
⇒
p
1
p
3
.
It is formulated in terms of
wd
theorems rather than type provisos.
The intermediate theorem (5) contains the surplus assumption
wd Y
,andour
goal is to eliminate it. This can be achieved by the cut rule together with (2). The
cut rule states that from Γ
1
Q
. All this
requires no real proof effort and can be done with the application of rules. (Rules
are theorem-generating functions in
ProofPower
, and their evaluation usually
requires less effort.) We then obtain the extended refinement theorem
P
and Γ
2
,
P
Q
we can derive Γ
1
,
Γ
2
(6) Γ
,
P
,
wd X
Y
∧
wd Y
X
with the desired shape. Apart from the
wd
assertion for the initial program and
provisos Γ, it only introduces the relevant proof obligations
P
of the law.
All this takes place as part of the mechanics of the implementation of law ap-
plications. It relies, however, on the model and law theorems having the correct
Search WWH ::
Custom Search