Re: [isabelle] Problems with Logic.mk_implies + compose_tac



On Sun, 2011-07-10 at 20:16 +1000, Thomas Sewell wrote:
> Hi Matej,
> 
> Two interesting things have happened. The first is that Goal.prove has lifted your meta-quantified conclusion (/\s1 s2. P s1 s2) into a schematically quantified theorem (P ?s1 ?s2). The internal ==> implications within your conclusion sg2 are now treated together with the sg1 ==> sg2 implication as a group of assumptions. This may make compose_tac surprise you. You've told it you want to have only 1 new goal - if I recall correctly that will be the final assumption of the supplied theorem, so try rotating the sg1 assumption to the end.
> 
> If that fails, you could try to stop Goal.prove lifting your meta-quantification. Playing around with the (invisible) protect constant might help you - look up protectI or protectD, No promises. Alternatively you could sidestep Goal.prove entirely by creating Thm.trivial from sg1 ==> sg2 and applying your tactic to eliminate the first assumption.

Thank you very much Thomas. I will try both.

Do you think using 'Goal.protect' or 'Goal.conclude' would do the job?

> Can't be bothered firing up Isabelle on a weekend to test any of these strategies for you. Good luck.

Still, thank you very much for the pointers. :)

Best,
---
Matej

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.