Re: [isabelle] Giving a name to a tactics-expression



On Mon, 22 Feb 2010, Jeremy Dawson wrote:

Well, that is useful information of a negative nature. It tells me how you _don't_ do the following:

val meth4 = EVERY [(TRY (REPEAT1 meth1)), meth2, meth3 ] ;

But the question is how _do_ you do it.

You don't, but go down to the basic tactics behind meth1, meth2, meth3. (All tools are supposed to export this ML view, apart from defining end-user method syntax.)

Isar methods are a more stylized way of refining structured goals than tactics, and things like fine-grained goal addressing is missing. This makes user space method expressions more digestible than old tactical ones -- you certainly know how proof scripts looked 10 years ago -- but on the other hand it is harder to define meaningful method combinations.

So just compose things as a tactic and then link it up with Isar via method_setup. There are plenty of examples in the sources -- most of them quite clean, because I've reworked these interfaces for Isabelle2009.


	Makarius






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