*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Structured induction with custom tactics*From*: Palle Raabjerg <palle.raabjerg at it.uu.se>*Date*: Fri, 12 Feb 2010 17:22:16 +0100*In-reply-to*: <4B715D77.1040107@it.uu.se>*References*: <4B715D77.1040107@it.uu.se>*User-agent*: Thunderbird 2.0.0.19 (X11/20090123)

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

**Follow-Ups**:**Re: [isabelle] Structured induction with custom tactics***From:*Christian Urban

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

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

- Previous by Date: [isabelle] Modifying latex rule output
- Next by Date: Re: [isabelle] Structured induction with custom tactics
- Previous by Thread: [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