*To*: cl-isabelle-users at lists.cam.ac.uk, Christian Urban <urbanc at in.tum.de>*Subject*: Re: [isabelle] A beginner's questionu*From*: Francisco Ferreira <ferrerif at iro.umontreal.ca>*Date*: Tue, 23 Nov 2010 23:26:25 -0500*In-reply-to*: <20101123172838.10421xy6e31ub0za@mailbroy.informatik.tu-muenchen.de>*References*: <4CEAF770.1000304@iro.umontreal.ca> <20101123172838.10421xy6e31ub0za@mailbroy.informatik.tu-muenchen.de>

Thank you! That was really helpful! But I am still having problems, I've checked the tutorial and the reference manual, but in the tutorial the Proof commands are not discussed, and I find the reference manual a bit too advanced, is there a tutorial on the proof command? Regarding my example I eliminated the problematic rule, and now when I reach the proof of the Pred(Z) rule, I don't know how I prove that Z↓m' is not possible as no rule matches Z Sorry for the continuos questions, and thanks again for your help, Francisco

**Attachment:
Arith2.thy**

On 2010-11-23, at 11:28 AM, Christian Urban wrote: > Hi Francisco, > > Below I have started your proof in the style > of Isabelle/Isar. Maybe this is of help for how > approaching this kind of proofs. However, once > I attempted the second case, I found out that > the lemma for your definition is not true. You > added a rule to Pierce's rules, which breaks the > property you are after. The counter example is > also included. > > Hope this helps, > Christian > > > > > Quoting Francisco Ferreira <ferrerif at iro.umontreal.ca>: > >> Hello all, >> >> I am just starting with Isabelle, my intention is to prove some simple theorems of simply-typed lambda (from Pierce's TAPL book) calculus using Nominal Isabelle. >> I am using the tutorial and the isar reference as guides (and the nominal_datatype_reference too) >> I am starting nice and easy trying to do the determinism proof for a very simple language of arithmetic expressions. >> So far I have defined my datatype and the step by step semantics relation, and I have formulated my theorem (I've attached the code as I have it so far). >> >> On my paper proof, I would proceed by induction on the structure of the step relation but I don't know how to proceed in this case (apply (rule step.induct) confuses me). >> >> What I need is some help to start, and hopefully be able to keep the momentum going. >> How do I approach this proof? (are there any examples that I should check?) >> >> Thanks in advance, >> Francisco >> > > > <Arith.thy>

**Follow-Ups**:**Re: [isabelle] A beginner's questionu***From:*Lars Noschinski

**Re: [isabelle] A beginner's questionu***From:*Lars Noschinski

**References**:**[isabelle] A beginner's questionu***From:*Francisco Ferreira

**Re: [isabelle] A beginner's questionu***From:*Christian Urban

- Previous by Date: Re: [isabelle] Pattern Matching Problem
- Next by Date: Re: [isabelle] A beginner's questionu
- Previous by Thread: Re: [isabelle] A beginner's questionu
- Next by Thread: Re: [isabelle] A beginner's questionu
- Cl-isabelle-users November 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