[isabelle-dev] IH in induction-wrapper

[Christian Sternagel]

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