# Re: [isabelle] Problem with obtaining induction premises

On Sat, 16 Sep 2006, Vaidas Gasiunas wrote:
> I have problems when extracting the premises of the current inductive
> case, something like:
>
> lemma "?Q xs ==> ?P xs"
> proof (induct xs)
> case (Cons x xs) hence "?Q xs" by auto ...
>
> Sometimes I can extract the premises with ".", but in the most of cases I
> need to apply "auto".
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 "..." .
Another option is to retrieve premises out of the blue:
have "..." .
> 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 `...`
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.
Makarius

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