Re: [isabelle] Problem with obtaining induction premises
Indeed, when I write
from Cons.hyps have "!!(ys::'a list). [| length zs = length ys; a \<in>
set zs |] ==> !y. lookupEq zs ys a = Some y" .
then it works. Now I will know how to deal with such cases.
----- Original Message -----
From: "Makarius" <makarius at sketis.net>
To: "Vaidas Gasiunas" <gasiunas at informatik.tu-darmstadt.de>
Cc: <isabelle-users at cl.cam.ac.uk>
Sent: Tuesday, September 19, 2006 2:05 PM
Subject: 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.
> this closed formula will be syntactically unrelated to the context of
>> At the end I proved the lemma without explicifying the hypothesis,
>> by referring to the fact Cons.hyps by its name.
> This is a good strategy. It is usually easier (and more informative)
> derive immediate conclusions from the induction hypotheses, rather
> 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
> this'', which can be expanded to ``apply this .'' The latter allows
> fine-grained debugging.
> The single step methods (notably "this" and "rule") insist on being
> 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
> 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
> and use different facts declared in the context. The relevance of
> is a fundamental problem in most automated proof tools.
>> If I write
>> have "[| length zs = length ys; a \<in> set zs |] ==> !y. lookupEq zs
>> a = Some y" .
>> then it works, but
>> have "!!ys. [| length zs = length ys; a \<in> set zs |] ==> !y.
>> 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
> 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