*To*: Palle Raabjerg <palle.raabjerg at it.uu.se>*Subject*: Re: [isabelle] Structured induction with custom tactics*From*: Makarius <makarius at sketis.net>*Date*: Sat, 13 Feb 2010 13:18:08 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4B758038.9070606@it.uu.se>*References*: <4B715D77.1040107@it.uu.se> <4B758038.9070606@it.uu.se>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Fri, 12 Feb 2010, Palle Raabjerg wrote:

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

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 proofstate. 'Proof.init @{context}' will give me a new (empty) proof state,which looks promising. I can populate the state with facts usingProof.put_facts and so on, but have so far been unable to give the statea 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.

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 {* ... *})

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?

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

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

Are there functions for creating proof methods?

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

Makarius

**References**:**[isabelle] Structured induction with custom tactics***From:*Palle Raabjerg

**Re: [isabelle] Structured induction with custom tactics***From:*Palle Raabjerg

- Previous by Date: Re: [isabelle] Structured induction with custom tactics
- Next by Date: Re: [isabelle] Structured induction with custom tactics
- Previous by Thread: Re: [isabelle] Structured induction with custom tactics
- Next by Thread: Re: [isabelle] Structured induction with custom tactics
- Cl-isabelle-users February 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list