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
> 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
>> I use the build of 2006 Sep 12.
> In that case you might want to read the NEWS file, which explains a
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and