*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Isabelle/Isar beginner questions on proofs by induction*From*: Francois Pottier <Francois.Pottier at inria.fr>*Date*: Mon, 10 Oct 2005 13:00:07 +0200*Reply-to*: Francois.Pottier at inria.fr*User-agent*: Mutt/1.5.9i

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"

**Follow-Ups**:

- Previous by Date: [isabelle] isabelle help
- Next by Date: [isabelle] subst question
- Previous by Thread: [isabelle] isabelle help
- Next by Thread: Re: [isabelle] Isabelle/Isar beginner questions on proofs by induction
- Cl-isabelle-users October 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list