David,
There is a reason why the ProofPower tutorials don't say much about the
forward proof tools you are trying to use.
I have given courses on ProofPower HOL and on ProofPower Z and wrote the
tutorials.
What I did in the courses was to teach just enough about forward proof
for the students to understand the basics of how proof in ProofPower
works, before teaching them how to use the goal package to accomplish
proofs.
Goal oriented proof is much easier in virtually all applications (though
it does often involve small fragments of forward proof).
Compared with using the goal package, contruction of forward proofs is
like pulling teeth.
The example given by Woodcock on page 42 can be proven using the goal
package by the following script:
set_goal([], %<%(%exists%x:'a%spot% %exists%y:'b%spot% P(x,y)) ´
(%exists%y:'b%spot% %exists%x:'a%spot% P(x,y))%>%);
a (REPEAT strip_tac);
a (%exists%_tac %<%y%>% THEN %exists%_tac %<%x%>% THEN strip_tac);
or just (not quite so easy to understand):
a (contr_tac THEN asm_fc_tac[]);
or even:
a (prove_tac[]);
(in a reasonable proof context such as "hol")
You might consider pointing your students to the Woodcock forward proof
and then showing them a ProofPower goal oriented proof, then they will
be learning a more intelligible and economic method of proof.
I could look closely at how to do this by forward proof and debug your
attempts, but I have never myself had occasion to do this kind of
forward proof, its not a necessary skill.
Of course, the forward proof facilities are used, but in rather
different ways, by the people who programmed the goal package, and by
people writing higher level proof facilities such as tactics, tacticals
etc., but for applications, the goal package makes things simpler both
to understand and to execute.
By way of further comment on why your proofs are not working, the term
required as a parameter to exists elim is one which matches just the
variable over which the existential quantifies, and so not a predicate.
It will only work one quantifier at a time (and %exists% x y %spot% is
two nested quantifiers), so you would have to do the proof in two stages
one for each of the quantified variables, unless you put them together
in the theorem as in %exists% (x,y) %spot%, which of course, is not
quite the same theorem.
So it really is a lot more complicated to do this by forward proof.
Roger
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
