# [isabelle] A beginner's questionu

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

theory Arith
imports Main
begin
datatype arith =
Z
| Succ "arith"
| Pred "arith"
(*
datatype val =
V_Z
| V_Succ "val"
*)
value "Z"
value "Pred Z"
value "Succ (Pred Z)"
inductive isvalue :: "arith \<Rightarrow> bool" where
v_z : "isvalue Z" |
v_s : "isvalue M ==> isvalue (Succ M)"
inductive step :: "arith \<Rightarrow> arith \<Rightarrow> bool" ("_\<down>_") where
s_succ : "m \<down> m' ==> (Succ m) \<down> (Succ m')" |
s_pred_zero : "(Pred Z) \<down> Z" |
s_pred : "m \<down> m' ==> (Pred m) \<down> (Pred m')" |
s_pred_succ : "isvalue v ==> (Pred(Succ v)) \<down> v" |
(* I add these rules because I don't know how to
proove the theorem that values don't step, so
values have to step to themselves *)
s_z [simp] : "Z \<down> Z"
(* s_val : "isvalue v ==> v \<down> v" *)
theorem det: shows "(step m n_1) \<and> (step m n_2) ==> (n_1 = n_2)"
(* apply (rule step.induct) \<leftarrow> this doesn't do what I expected *)
sorry
end

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