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

• To: isabelle-users <isabelle-users at cl.cam.ac.uk>
• Subject: [isabelle] induct ... arbitrary: ...
• From: Christian Sternagel <christian.sternagel at uibk.ac.at>
• Date: Tue, 15 Mar 2011 13:02:44 +0100
• User-agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.13) Gecko/20101209 Fedora/3.1.7-0.35.b3pre.fc14 Lightning/1.0b3pre Thunderbird/3.1.7

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