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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev