[isabelle] induct ... arbitrary: ...



Hi there!

I'm a bit puzzled by the behavior of arbitrary for induct. After the initial proof part

lemma success_sequenceI:
  assumes "!!m s. m : set ms ==> success m s"
  shows "success (sequence ms) s"
using assms proof (induct ms arbitrary: s)
  case Nil thus ?case by (auto intro!: success_intros)
next

I have to prove

!!a ms x.
  [|!!x. (!!m x. m : set ms ==> success m x)
      ==> success (sequence ms) x;
    !!m x. m : set (a # ms) ==> success m x|]
  ==> success (sequence (a # ms)) x

which is as expected (note the nested bindings of x). However, after the further step

case (Cons m ms)

I obtain the facts (this:)

  (!!m x. m : set ms ==> success m x) ==> success (sequence ms) ?x
  ?m : set (m # ms) ==> success ?m ?x

So the x's which where originally different are now required to be the same. Do I miss something here?

PS: I only succeeded in the proof after transforming the lemma into:

assumes "!!m s. m : set ms ==> success m s"
shows "ALL s. success (sequence ms) s"

cheers

chris





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