[ProofPower] type variables in subgoal package

[Philip Clayton]

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.  I have 
convinced myself why this is the case --- see attached example, 
originally sent to Steve Brackin.  (Did I miss something there?)  This 
appears to be a common problem when people are learning to use ProofPower.

Also, is is possible to generalize the types of a subgoal such that the 
old subgoal is a type instance of the new subgoal?  I've seen examples 
where more specific types prevent prove_tac from working with ?_ext pcs 
because e.g. tuple components are considered separately --- see attached 
example type_vars_eg.  Consider the scenario: a 
more-type-specific-than-necessary lemma is introduced to avoid the 
rewriting problem above but then to simplify proof of the lemma with 
prove_tac, the user would like to generalize this lemma first.  Is there 
a way to do this or is it necessary to prove a separate theorem?

Thanks
Phil

-------------- next part --------------
A non-text attachment was scrubbed...
Name: forstevebrackin20040922.ML.gz
Type: application/x-gzip
Size: 1666 bytes
Desc: not available
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040923/d8b1cbb7/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: type_vars_eg.ML.gz
Type: application/x-gzip
Size: 342 bytes
Desc: not available
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040923/d8b1cbb7/attachment-0001.bin>