Re: [isabelle] A beginner's questionu



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



Attachment: Arith.thy
Description: Binary data



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