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



Alternatively you can usually state and prove your implication directly:

...  "Assumption S ==> P S"
proof(induct S)

Regards
Tobias

Am 18/12/2012 10:23, schrieb Julian Brunner:
> 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
> 
> On Mon, Dec 17, 2012 at 11:07 PM, Edward Schwartz <edmcman at cmu.edu> wrote:
>> Hi,
>>
>> I am trying to prove a fairly straight-forward property in Isar:
>>
>> Assumption S ==> P S
>>
>> I am trying to prove P by induction on S.
>>
>> proof -
>>   assume Asm: "Assumption S"
>>   have "P S"
>>   proof (induct S)
>>   case (Foo arg) from Asm show ?case by simp
>>
>> And here is where the problem occurs.  Asm refers to S.  But all of the
>> current proof goals and assumptions are in terms of Foo arg.  There doesn't
>> seem to be any fact that says S = Foo arg.
>>
>> How can I structure my proof so this works?
>>
>> Thanks,
>> Ed





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