[isabelle-dev] IH in induction-wrapper
Christian Sternagel
c-sterna at jaist.ac.jp
Tue Apr 17 10:09:53 CEST 2012
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
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
More information about the isabelle-dev
mailing list