Re: [isabelle] Problem with obtaining induction premises



> Here the facts stemming from the Cons case consist of several things
> simultaneously.  The auto method silently ignores unused facts, while
> single-step methods insist on being more thourough.  This means a "."
> proof has to be able to apply all given facts, which fails in the 
> above
> application.
>
> You can try something like this to specify facts more precisely:
>
>  from Cons.hyps have "..." .

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. At the end I 
proved the lemma without explicifying the hypothesis, just by referring 
to the fact  Cons.hyps by its name. But I am still curious why "." or 
"apply" cannot deal with such seemingly trivial step.

> Another option is to retrieve premises out of the blue:
>
>  have "..." .

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.

>
>> I use the build of 2006 Sep 12.
>
> In that case you might want to read the NEWS file, which explains a 
> few
> additions to the induction setup, including common proof patterns.  In
> particular, the above from/have/. invocation can be replaced by
>
>  from `...`

Thanks, this can be very useful to make the proof more readable, because 
now I invent a lot of fancy names to refer to the known facts.

> Note that your example in Test.thy will need a type constraint of
> "!!ys :: 'a list. ..." here.  This may change eventually, when the 
> `...`
> notation becomes polymorphic.

I don't know, but I somehow proved it without additional type 
annotations.

Thanks,
Vaidas 







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