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