*To*: Francois Pottier <Francois.Pottier at inria.fr>*Subject*: Re: [isabelle] Isabelle/Isar beginner questions on proofs by induction*From*: Makarius <makarius at sketis.net>*Date*: Tue, 11 Oct 2005 13:17:02 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20051010110007.GA26541@yquem.inria.fr>*References*: <20051010110007.GA26541@yquem.inria.fr>

On Mon, 10 Oct 2005, Francois Pottier wrote: > 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" > 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 The problem here is that your goal statement is not fully general wrt. to the induction principle, using an expression "subst x e2 e1" in place of an inductive variable. In order to make this work, one may reformulate the goal in terms of a local definition of that expression, then perform the induction, then unfold the definition in each inductive case: 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 "!!x e1 e2. e == subst x e2 e1 ==> (env2, e, t1) : judgments" using p proof (induct) case JVar then show ?case apply (simp only:) sorry next case JAbs then show ?case apply (simp only:) sorry next case JApp then show ?case apply (simp only:) sorry qed Note that the 'apply (simp only:)' above just demonstrate the machanics. A proper proof would spell this out differently. > * 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 ==>. !! ==> == instead of ALL --> = spare you 2 more bookeeping steps to get rid of the logical connectives in the goal and the final result. > What's the final word? An even better version of the 'induct' method, that is able to do generalizations and local definitions (induction over structured expressions) on the fly. I don't know if this will be the final word, but it would move even further from fiddling with connectives, emphasizing actual reasoning instead. Makarius

**References**:**[isabelle] Isabelle/Isar beginner questions on proofs by induction***From:*Francois Pottier

- Previous by Date: Re: [isabelle] subst question
- Next by Date: [isabelle] FMCO 2005: second call for participation
- Previous by Thread: [isabelle] Isabelle/Isar beginner questions on proofs by induction
- Next by Thread: [isabelle] subst question
- 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