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



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.

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). 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.)


	Makarius





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