[isabelle] Structural induction with an assumption in Isar



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.