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

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"





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