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.