# [isabelle] Isabelle/Isar beginner questions on proofs by induction

```Hello,

I am trying to gain an initial understanding of both Isabelle/HOL
and the Isar structured proof language. My main sources are the
Isabelle/HOL tutorial and Markus Wenzel's PhD thesis. I have some

I have been trying to write a few simple proofs about simply-typed
lambda-calculus. Here is a typical statement, a substitution lemma:

lemma substitution:
assumes p: "(env1, e1, t1) : judgments"
assumes q: "(env2, e2, t2) : judgments"
assumes e: "ALL y. y ~= x --> env1 y = env2 y"
assumes f: "env1 x = t2"
shows      "(env2, subst x e2 e1, t1) : judgments"

(For reference, I include the definitions that lead up to this lemma
at the end of this message.) (For simplicity, my environments are
total functions from variable names to types.)

If I try to attack a proof of this statement by saying

using p proof (induct)

then Isabelle presents me with new subgoals that are plain wrong.
The first of these, for instance, is

1. !!env xa. (env2, subst x e2 (EVar xa), env xa) : judgments

I can understand how these subgoals appear. The induction principle for
judgments (judgments.induct) involves a schematic variable ?P that must
satisfy the equation

?P env1 e1 t1 = ((env2, subst x e2 e1, t1) : judgments)

(This equation is obtained by considering the fact p and the statement's final
"shows" clause. The facts q, e, and f are apparently ignored in this process.)

?P = %env1 e1 t1. ((env2, subst x e2 e1, t1) : judgments)

which is inappropriate.

My questions are,

* how should I reformulate the statement (or the proof) so that appropriate
sub-goals arise? should I explicitly provide a value for the variable ?P in
the proof script? or should I modify the statement so that the hypotheses q,
e, and f are moved into the shows clause, using explicit implications?

* the Isabelle tutorial suggests that this kind of induction
requires a strengthened statement, typically making use of
the object-level quantifiers ALL and -->. However, Wenzel's
thesis suggests that this is no longer necessary in Isabelle/Isar,
and that it is possible to stick with the meta-level quantifiers
!! and ==>. What's the final word?

I will of course continue to explore on my own, but any help would be warmly
welcome. Pointers to Isabelle/Isar developments that perform proofs by
induction with multiple hypotheses or multiple parameters, like above, would
also be very interesting to me.

Best regards,

--
François Pottier
Francois.Pottier at inria.fr

theory Lambda = Main:

types
name = nat

datatype lambda =
EVar name
| EAbs name lambda
| EApp lambda lambda

datatype type =
TBase name
| TArrow type type

consts
judgments :: "((name => type) * lambda * type) set"

inductive judgments
intros
JVar: "(env, EVar x, env x) : judgments"
JAbs: "(env(x := t1), e, t2) : judgments ==>
(env, EAbs x e, TArrow t1 t2) : judgments"
JApp: "(env, e1, TArrow t1 t2) : judgments ==>
(env, e2, t1) : judgments ==>
(env, EApp e1 e2, t2) : judgments"

consts
subst :: "name => lambda => lambda => lambda"

primrec
"subst x e (EVar y) = (if x = y then e else EVar y)"
"subst x e (EAbs y e1) = (if x = y then EAbs y e1 else EAbs y (subst x e e1))"
"subst x e (EApp e1 e2) = EApp (subst x e e1) (subst x e e2)"

lemma substitution:
assumes p: "(env1, e1, t1) : judgments"
assumes q: "(env2, e2, t2) : judgments"
assumes e: "ALL y. y ~= x --> env1 y = env2 y"
shows      "(env2, subst x e2 e1, t1) : judgments"

```

• Follow-Ups:

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