[ProofPower] type variables in subgoal package

[Roger Bishop Jones]

On Thursday 23 September 2004 11:01 am, Philip Clayton wrote:
> There appear to be some restrictions when reasoning involves
> type variables in the subgoal package.  Is there a succinct
> way to sum up these restrictions?
>
> For example, it appears that it is not possible to rewrite
> with an assumption if the assumption requires type
> instantiation.

Its a restriction of the logic that when you instantiate
type variables you must do this over the entire sequent.
When you use an assumption in the goal package what happens
is equivalent to doing asm_rule on the assumption and then
reasoning forward from that theorem.
The theorem you get is  A |- A where A is the relevant
assumption. You can't instantiate type variables in the
conclusion without doing so in the assumptions, but
if you do that you will be reasoning from something
which isn't in the assumptions, so your proof would not
hang together.

The reason why the logic does not allow instantiation
of the conclusion without instantiation of the assumptions
is because it is not sound. If you could you would be
able to derive a contradiction by starting with 
asm_rule of "there is exactly one object of type 'a"
then instantiate 'a in the conclusion to BOOL and prove
that the conclusion is False, then discard the
assumption and instantiate 'a to "one"
and prove that the hypothesis is true, yielding
a proof of T => F, which is false, from which all
else follows.

So there is no fix to this problem, you just have to
remember not to put things in the assumptions if
you want to type instantiate them.
If you really need a polymorphic lemma, then you
have to prove it as a separate theorem rather than
use "lemma_tac" (or else you have to do lemma_tac
for every instance you need).

It is a feature of ProofPower's subgoal package
(unlike the other HOL's) that it works out the
proofs as it goes along and the entire current
state of the goal package is coded up as a theorem
which asserts that the desired goal is a consequence
of the outstanding subgoals.
This is to avoid the possibility (which might arise
from incorrectly coded tactics) that you get to the
end of your proof and the subgoal package finds it
can't actually sew it together and get the theorem
you thought you had proved.  (this did happen
occasionally with classic HOL, it doesn't any more
because they use "mk_thm" covertly behind the scenes
to check the partial proof even though the subgoals
haven't been proved).
Thinking about this might give some insight into
what the goal package can't do. 
It does explain why you can't generalise the type of
a subgoal, taken alongside my earlier remarks about
the logic.
As far as I am aware there is nothing
(sound) which the ProofPower goal package disallows
but which is allowed by the other HOLs.

In relation to your comments to Steve about losing
the assumptions on things you strip into the assumptions,
this is not correct.
I think it is another original feature of the ProofPower
subgoal package that it handles the use of theorems
with assumptions better than previous goal packages.
If you use a theorem which has assumptions, either
by stripping it into the assumptions or for any other
purpose in a goal package proof, then the extra assumptions
are added into the subgoal list.  This is what it takes
to make the proof hang together.
Try it with asm_tac (asm_rule %<%F%>%).

Yes, the tutorials should mention that you can't type
instantiate assumptions.
The tutorials really only scratch the surface, and they don't
seem to mention type instantiation at all (which I
suppose is a testimonial to how much you can do without
worrying about type instantiation).

Roger Jones