[isabelle-dev] IH in induction-wrapper

[Tobias Nipkow]

I am afraid this is a known limitation: inductions on proper terms rather than
just variables do not set up IH. We hope to generalise this one day...

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