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

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