Well this was just a stripped-down version of my real proof, in which
the term seems to be necessary. Here is a less stripped-down version.
notepad
begin
fix P :: "bool" and Q :: "(nat ⇒ 'a set) ⇒ bool"
fix f :: "nat => 'a set" and n :: nat
assume "finite (f n)" and "Q f"
hence "P"
proof (induction "f n" arbitrary: f rule: finite_psubset_induct)
case (psubset g)
thm psubset.IH (* this fact does not exist *)
show ?case sorry
qed
end
If I drop the "f n", then in the fact psubset I have
?B ⊂ g ⟹ Q ?f ⟹ P (i.e., ?B and ?f are not related)
Otherwise I have
?f n ⊂ g n ⟹ Q ?f ⟹ P
cheers
chris
On 04/17/2012 04:44 PM, Tobias Nipkow wrote:
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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
