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


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> 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.