*To*: Palle Raabjerg <palle.raabjerg at it.uu.se>*Subject*: Re: [isabelle] Structured induction with custom tactics*From*: Christian Urban <urbanc at in.tum.de>*Date*: Sat, 13 Feb 2010 12:37:55 +0100*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>*Reply-to*: urbanc at in.tum.de

Hi Palle, I am afraid I cannot give an answer to all your questions. Palle Raabjerg writes: > > 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. Sorry. Writing tutorials takes time and it is usually a thankless task (in terms of paper-counts etc). What I thought I will describe in this section is how to deal with manipulations of contexts. If I understood your original question correctly, this will not be of much help to you. > 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. Usually, if you want to set up a goal to be proved, then you need to use the function Goal.prove. For this you need a tactic that completely solves the goal. Not sure whether this is what you want. > What is the intention of Proof.theorem/theorem_i? The function theorem is for "outer layers" where the terms are given as strings. Theorem_i is the "internal" interface where parsing has been already done and terms are given as "real" terms. Having said that, forget this convention quickly, as it is already obsolete. I think today, functions for "outer layers" are called foo_cmd, while the internal functions are just called foo. To give more help, maybe it would be helpful if you describe exactly what you like to do. In your last email you described your problem in abstract terms. Judging from the absence of replies, it seems nobody was able to give an appropriate answer. Maybe a concrete example or even a small theory file would be more helpful....though no promises ;o) Best wishes, Christian

**Follow-Ups**:**Re: [isabelle] Structured induction with custom tactics***From:*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