Re: [isabelle] Structured induction with custom tactics



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?

But in short, what I want to do is automate/manipulate Isar style
structured proofs in ML.

Since the last mail I have been looking around to find out more. The
Isabelle Programming Tutorial has a section intended for the subject of
structured proofs in ML. But that section is marked TBD, and there is
only a very short example on a single page.
The Isabelle/Isar Implementation Manual has a chapter intended for Isar
(supposedly to explain how to manipulate Isar style proofs on the ML
level). It contains the empty sections "Proof commands", "Proof methods"
and "Attributes".

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.

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.

So a few questions on this:
What is the intention of Proof.theorem/theorem_i?
How do we get an initial state with a goal we want to prove?
Is state-manipulation a recommended way of doing this in ML?
I am under the impression that the node stack corresponds to the levels
(scopes) of an Isar proof. Is that correct?

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

A Method.method is simply a function type: thm list -> cases_tactic
There are a number of basic methods in method.ML that seem to correspond
to some basic tactics (assumption, erule, drule...), and Method.text can
be a 'Basic of (Proof.context -> method) * Position.T'.
Method.text can also be 'Source of src', which seems to indicate that we
may be able to include Isar code in a Method.text.

Intuitively, it seems we should be able to use Proof.apply to apply
elements of type Method.text to states, and perform proofs that way. But
the 'Position.T' element indicates that this is not the whole story.

So a few more questions:
What are Method.method and Method.text really intended for?
Are there functions for creating proof methods?
Can Isar scripts be included in a Method.text element?

Best Regards,
The inquisitive
Palle Raabjerg





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