[isabelle-dev] IH in induction-wrapper
Christian Sternagel
c-sterna at jaist.ac.jp
Tue Apr 17 07:26:47 CEST 2012
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
More information about the isabelle-dev
mailing list