Re: [isabelle] A beginner's questionu

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,


Attachment: Arith2.thy
Description: Binary data

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>:
>> 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>

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