Re: [isabelle] Structural induction with an assumption in Isar


I just wanted to follow-up in case anyone finds this thread in the archive.
 I spoke too quickly.  Julian's solution *does* ensure that the Assumption
S fact is available during the induction.  However, S still remains
unconnected to Foo arg, the current induction form. Because of this, I
cannot show Assumption (Foo arg).

I was able to get the proof to work by including the assumption as part of
the induction hypothesis, as Tobias suggested.  I had tried this before,
actually, but was running into trouble because I did not use the next
command between induction cases.  This was very confusing to me, because I
normally don't need to use next.  I guess it matters here because each
induction case will add to the assumptions, and so it needs to be reset.

Thank you to both Julian and Tobias for the help.


On Tue, Dec 18, 2012 at 10:05 AM, Edward Schwartz <edmcman at> wrote:

> Thank you!  In retrospect, this makes perfect sense.
> On Tue, Dec 18, 2012 at 4:23 AM, Julian Brunner <julianbrunner at>wrote:
>> Hello,
>> You'll want to change your proof to something like
>> proof -
>>   assume Asm: "Assumption S"
>>   from Asm have "P S"
>>   proof (induct S)
>>   case (Foo arg) from Foo show ?case by simp
>> That way, your assumption is included in the induction and will
>> reappear as part of Foo.
>> Cheers,
>>  Julian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.