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.


Proofpower mailing list

Reply via email to