Re: [isabelle] Problem with obtaining induction premises

On Mon, 18 Sep 2006, Vaidas Gasiunas wrote:

> I have tried following in my example:
> from Cons.hyps have "!!ys. [| length zs = length ys; a \<in> set zs |] 
> ==> !y. lookupEq zs ys a = Some y" .
> It does not work, "by auto" does not help here either.

You also need a type constraints "!!ys :: 'a list. ..." here.  Otherwise 
this closed formula will be syntactically unrelated to the context of the 

> At the end I proved the lemma without explicifying the hypothesis, just 
> by referring to the fact Cons.hyps by its name.

This is a good strategy.  It is usually easier (and more informative) to 
derive immediate conclusions from the induction hypotheses, rather than 
duplicate them literally.

> But I am still curious why "." or "apply" cannot deal with such 
> seemingly trivial step.

Note that 'apply' merely applies a proof method.  The "." abbreviates ``by 
this'', which can be expanded to ``apply this .'' The latter allows more 
fine-grained debugging.

The single step methods (notably "this" and "rule") insist on being able 
to apply all chained facts, without ignoring anything.  Thus providing 
excessive facts makes the method invocation fail.

This principle is important to achive some degree of robustness and 
predictability of structured proof checking.  In contrast, automated 
methods readily ignore irrelevant facts.  So it is easy to write proofs 
that tell the wrong story, e.g. like this:

  assume a: A
  assume b: B

  from a and b have C by auto

Here the ``auto'' step can ignore either a or b, or even worse ignore both 
and use different facts declared in the context.  The relevance of facts 
is a fundamental problem in most automated proof tools.

> If  I write
> have "[| length zs = length ys; a \<in> set zs |] ==> !y. lookupEq zs ys 
> a = Some y" .
> then it works, but
> have "!!ys. [| length zs = length ys; a \<in> set zs |] ==> !y. lookupEq 
> zs ys a = Some y" .
> does not work. But the latter is the hypothesis, which I see in the 
> context.

This is again a problem with unexpectedly general types.  The first form 
refers to the fixed variable ys of the context, i.e. gets the expected 
type.  The second is detached due to !! closure and gets a fresh type.


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