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


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
questions about proofs by induction.

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.)
This leads to the candidate

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

  name = nat

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

datatype type =
  TBase name
| TArrow type type

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

inductive judgments
    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"

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

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

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