Re: [isabelle] Structured induction with custom tactics



On Fri, 12 Feb 2010, Palle Raabjerg wrote:

It occurs to me that I may not have been very clear or specific in my previous mail on this subject. I am also wondering: Would this be more appropriate for the [isabelle-dev] list, as we are dealing with Isabelle/ML?

Isabelle/ML is definitely part of the "user space" of Isabelle. As long as we speak about official releases for end-users, this is the correct mailing list.


If we look at the source files, it would seem that Pure/Isar/proof.ML
corresponds to "Proof commands", Pur/Isar/method.ML corresponds to
"Proof methods" and Pure/Isar/attrib.ML to "Attributes". And indeed,
many of the functions look interesting to me. I have been experimenting
a bit, but much of it still feels like a bit of a mystery.

But am I on the right track at least?
I may well be on the wrong track, in which case most of the questions
below are probably pointless.

I am impressed how far you've got in figuring out the sources. These modules implement the main concepts of the Isar proof language. Chapter 2 of the Isar reference manual provides some high-level explanations of all this. You do not need to understand all these details to implement advanced proof methods, though.


It seems clear that most of the functions in proof.ML manipulate a proof state. 'Proof.init @{context}' will give me a new (empty) proof state, which looks promising. I can populate the state with facts using Proof.put_facts and so on, but have so far been unable to give the state a goal.

Using 'Proof.theorem_i' as follows:
Proof.theorem_i NONE (K I) [[(@{prop "A ==> A"}, [])]] @{context}
seems to yield a state with a stack of 3 nodes, the _second_ node
including the goal "A ==> A", the other two empty. Puzzling. Maybe
theorem_i is not what I am looking for.

It is unlikely that you will need any of this. The proof state is already given by the user -- you can access it via Isar.state() in interactive ML.

The Proof.theorem_i function is the most basic entry point for producing a toplevel goal; the 'theorem' command does this in regular user space (with lots of extra sophistication). The stack implements Isar block structure -- just an internal detail.


How do we get an initial state with a goal we want to prove?

  lemma "A ==> A"
  ML_prf {* Isar.goal() *}

You can also say this:

  apply (tactic {* ... *})

but you need to give a closed ML expression of type tactic on the spot, so it is advisable to play around with ML_prf or ML_val first.


Is state-manipulation a recommended way of doing this in ML?

No, unless you want to come up with new primary Isar commands, which usually requires several years of intensive study of the machinery.


I am under the impression that the node stack corresponds to the levels (scopes) of an Isar proof. Is that correct?

Yes.  User code normally only needs the top-of-stack, though.


Moving on to possibly the most puzzling subject: Methods. Or Proof methods, as the implementation manual seems to call it. There are two prevalent Method types seen in method.ML and proof.ML: Method.method and Method.text

Method.method is what you need; the Method.text merely represents source text.


Are there functions for creating proof methods?

Method.METHOD etc. You should also grep for method_setup or Method.setup in the existing theory/ML sources to get an idea how it is usually done (but there are occasionally old forms that should not be copied blindly).

Wrapping up a tactic as a proof method involves some standard boiler plate, but the hard part is the logic behind the tactic itself. Maybe we should go back to some concrete examples from you nominal application.


Can Isar scripts be included in a Method.text element?

Not really. You can probably ignore Method.text altogether for your purposes.


	Makarius





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