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