Re: [isabelle] Structural induction with an assumption in Isar
Alternatively you can usually state and prove your implication directly:
... "Assumption S ==> P S"
Am 18/12/2012 10:23, schrieb Julian Brunner:
> 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.
> On Mon, Dec 17, 2012 at 11:07 PM, Edward Schwartz <edmcman at cmu.edu> wrote:
>> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and