[isabelle-dev] IH in induction-wrapper

[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