Email Gateway (Aug 18 2022 at 14:33): Email Gateway (Aug 18 2022 at 14:33):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
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.methodcombining 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.textYou 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.textMethod.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
Email Gateway (Aug 18 2022 at 14:35):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 14:47):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all.
[Apologies if this question already was on this list some time ago]
Is there a way to give a short name to a complex tactic-expression. I
have, e.g., the following pattern that I frequently use.
apply (((erule (1) lemma1)+)?,erule lemma2,simp)+
Lemma1 and lemma2 are two (fixed) lemmas proven in my theory.
Instead, I would like to write something like:
define_method my_method = (((erule (1) lemma1)+)?,erule lemma2,simp)+
and later:
apply (my_method)
However, the only way I know is something like:
method_setup my_method = {* <Some scary ML-code, much more boilerplate
than the above tactics-expression, and much more complicated to read and
write if one does not know the ML-interface by heart> *} "..."
Is there a way without manually translating the above Tactics-expression
to ML code?
Regards and thanks,
Peter
Email Gateway (Aug 18 2022 at 14:47):From: Peter Lammich <peter.lammich@uni-muenster.de>
Peter Lammich schrieb:
Is there a way to give a short name to a complex tactic-expression. I
have, e.g., the following pattern that I frequently use.
apply (((erule (1) lemma1)+)?,erule lemma2,simp)+Trying to translate it to ML, I cannot find any ML-tactics equivalent
for "erule (1)". There is only etac, but this seems to have no number of
additional premises.
Regards & Thanks,
Peter
Lemma1 and lemma2 are two (fixed) lemmas proven in my theory.
Instead, I would like to write something like:
define_method my_method = (((erule (1) lemma1)+)?,erule lemma2,simp)+
and later:
apply (my_method)However, the only way I know is something like:
method_setup my_method = {* <Some scary ML-code, much more boilerplate
than the above tactics-expression, and much more complicated to read
and write if one does not know the ML-interface by heart> *} "..."Is there a way without manually translating the above
Tactics-expression to ML code?Regards and thanks,
Peter
Email Gateway (Aug 18 2022 at 14:47):From: Makarius <makarius@sketis.net>
On Thu, 18 Feb 2010, Peter Lammich wrote:
Is there a way without manually translating the above Tactics-expression
to ML code?
Not really. Isar was introduced to overcome adhoc "scripting" of proofs,
and there is a carefully chosen terminology to emphasize this ("proof
text" and "proof method", instead of the more primitive "proof script" and
"tactic"). This was just one further step to less operational detail
compared to old-style ML tactics of classic Isabelle/HOL, which was
already much more stylized in 1998 than original HOL with its huge numbers
of small tactics and tacticals.
Comparing formalizations from these different eras, my general impression
is that people now achieve more with the more abstract means of Isar, and
the results are checked faster and easier to maintain. Nonetheless, there
is still a lack of serious interactive proof development support, say some
kind of "prover IDE" that deserves this name.
Is there a way to give a short name to a complex tactic-expression. I have,
e.g., the following pattern that I frequently use.
apply (((erule (1) lemma1)+)?,erule lemma2,simp)+Lemma1 and lemma2 are two (fixed) lemmas proven in my theory.
Instead, I would like to write something like:
define_method my_method = (((erule (1) lemma1)+)?,erule lemma2,simp)+
and later:
apply (my_method)However, the only way I know is something like: method_setup my_method =
{* <Some scary ML-code, much more boilerplate than the above
tactics-expression, and much more complicated to read and write if one
does not know the ML-interface by heart> *} "..."
Designing (and implementing) Isar proof methods needs some care, this is
not for quick scripting.
First of all, in many situations, the intended goal refinement can be
achieve more declaratively, e.g. by deriving suitable compound rules, or
feeding certain rules to simp/fast/blast/auto etc. with intro/elim/iff
declarations.
If you really need to define a goal refinement macro, you can actually
give a name to a tactic (not a complex method expression as in the example
above). E.g. like this:
ML {* val my_tac = REPEAT o (rtac @{thm foo} THEN' (TRY o atac)) *}
and use it later via the "tactic" method, e.g. like this:
lemma True
apply (tactic {* my_tac 1 *})
This still looks a bit scary, but the overhead for argument parsing is
avoided.
If you explain your application more specifically, it is easier to say
what is really needed.
Makarius
Email Gateway (Aug 18 2022 at 14:47):From: Makarius <makarius@sketis.net>
The numbers merely specify additional assumption steps -- which used to be
a very common idiom in old-style tactic scripts. (In Isar, reasoning by
assumption is usually implicit in the proof structure, e.g. after closing
a 'by'.)
The low-level tactic is called assume_tac.
Makarius
Email Gateway (Aug 18 2022 at 14:47):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Peter Lammich wrote:
Hi all.
[Apologies if this question already was on this list some time ago]Is there a way to give a short name to a complex tactic-expression. I
have, e.g., the following pattern that I frequently use.
apply (((erule (1) lemma1)+)?,erule lemma2,simp)+Lemma1 and lemma2 are two (fixed) lemmas proven in my theory.
Instead, I would like to write something like:
define_method my_method = (((erule (1) lemma1)+)?,erule lemma2,simp)+
and later:
apply (my_method)However, the only way I know is something like:
method_setup my_method = {* <Some scary ML-code, much more boilerplate
than the above tactics-expression, and much more complicated to read
and write if one does not know the ML-interface by heart> *} "..."Is there a way without manually translating the above
Tactics-expression to ML code?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
The other way, it seems I never finished figuring it out (I looked at
this sort of stuff some years ago, and pretty much gave up on it, so I
decided to stick to using tactics directly - which are all described in
the Reference Manual).
The problem may be that a Method.text seems to be applied directly, not
by turning it into a method, see
Proof.apply ;
val it = fn : Method.text -> Proof.state -> Proof.state Seq.seq
(which uses
Method.apply ;
val it = fn : Method.method -> Thm.thm list -> RuleCases.tactic
but unfortunately not by creating a single compound method en route)
(Incidentally all the above code is Isabelle2007, some of it also
changed to make some functions visible).
If you can use a compound tactic, it would be much easier.
Method.erule is based on Tactic.eresolve_tac, plus some other stuff,
including doing something with facts. If you can do without the other
stuff, just use tactics and the tactic combinators - so then it would
look like
EVERY' [(TRY o REPEAT1 o eatac lemma1 1), etac lemma2, Simp_tac ] 1 ;
Jeremy
Regards and thanks,
Peter
Email Gateway (Aug 18 2022 at 14:47):From: Makarius <makarius@sketis.net>
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.methodcombining 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.textYou 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
Email Gateway (Aug 18 2022 at 14:48):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Peter Lammich wrote:
I was under the impression that erule (1) was just (erule,assumption)
which then would translate to "etac some_rule THEN' atac" in ML.
In any case, check out Christian's example from the Isabelle Developer
Workshop, where he shows an example translation from apply-style proof
script to ML method: http://tphols.in.tum.de/IDW/CU-Ex1.thy
And also look at Makarius's slides/examples on proof methods. Available
here:
http://tphols.in.tum.de/idw.html
I've found these practical examples have helped me much more than the
reference manual. Once I understood what the point of the exercise was,
the reference manual started to help instead of confuse.
Good luck!
Rafal Kolanski.
Last updated: Apr 26 2024 at 20:16 UTC