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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
