[isabelle-dev] IH in induction-wrapper

[Tobias Nipkow]

Revised answer.

I was a bit surprised that it did not work and tried to get to the bottom of it
with some tracing, but everything seemed to be fine. Then I realised that your
inductions are overkill: your inductions are over a predicate, you do not need
to give a variable or term as well. If you drop "f 0" below, everything works fine.

Best regards
Tobias

Am 17/04/2012 07:26, schrieb Christian Sternagel:
> Hi all,
> 
> I think the possibility to refer to the induction hypothesis via, e.g., Suc.IH
> (for natural numbers) is a nice feature offered by the "induction"-wrapper
> around "induct". I was wondering if there is an inherent problem in the
> following example, or if the "induction"-wrapper could be adapted to deal with it?
> 
> notepad
> begin
>   fix A :: "'a set" and P :: "bool"
>   assume "finite A"
>   hence "P"
>   proof (induction A rule: finite_psubset_induct)
>     case (psubset B)
>     thm psubset.IH (* as expected *)
>     show ?case sorry
>   qed
>   fix f :: "nat => 'a set"
>   assume "finite (f 0)"
>   hence "P"
>   proof (induction "f 0" arbitrary: f rule: finite_psubset_induct)
>     case (psubset g)
>     thm psubset.IH (* this fact does not exist *)
>     show ?case sorry
>   qed
> end
> 
> cheers
> 
> chris
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev