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.

Thanks,
Vaidas

----- 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. 
> Otherwise
> this closed formula will be syntactically unrelated to the context of 
> the
> problem.
>
>
>> 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.
>
>
> Makarius 







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