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



Makarius wrote:
On Fri, 19 Feb 2010, Jeremy Dawson wrote:

Basically, it seems that methods can be combined in these sorts of ways, but it is hidden in the source code, which is essentially undocumented. erule is
Method.erule ;
val it = fn : int -> Thm.thm list -> Method.method

combining methods uses

Method.Then ;
val it = fn : Method.text list -> Method.text
Method.Try ;
val it = fn : Method.text -> Method.text
Method.Repeat1 ;
val it = fn : Method.text -> Method.text

You then have to work out how to get between a method and a Method.text

One way would use

Method.Basic ;
val it = fn : (ProofContext.context -> Method.method) -> Method.text

Method.text merely models the Isar source representation of method expressions. This is hardly useful in user-space.

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.

BTW, when reading the ML sources -- which are always written to be read by humans -- you need to look both bottom-up and top-down. In particular, checking for common uses of certain operations helps to infer their semantics (the sources themselve cannot say "this is used for blah blah" without violating modularity).
It's true that saying "this is used for blah blah" is one of the three aspects to documenting a function, and it is certainly true that it is a moot point as to where it should go. I've not come across the suggestion that as a consequence it should be omitted completely. In any case, the other two aspects of documenting a function are equally absent from most of the Isabelle source code.
If you grep for Method.Then for example, you will immediately see that only the Isar infrastructure itself ever uses it, so we can ignore it here.
Incidentally all the above code is Isabelle2007, some of it also changed to make some functions visible.
In Isabelle2009 I've cleaned up the main method_setup (and Method.setup) interfaces. If you just grep for either of these in the existing sources, you will get an idea how it is usually done. (These high-level entries are also covered in the manuals, with some minimal examples.)
As far as I can see, method_setup and Method.setup are relevant only when you already have the method you want to use. If I'm wrong it may be because I haven't spent any longer examining the sources. But examining (undocumented) sources is not the normal way to find out what a piece of software does.

Jeremy


    Makarius







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