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

On Tue, Mar 15, 2011 at 5:02 AM, Christian Sternagel
<christian.sternagel at> wrote:
> 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?


Those '?x's are not required to be the same. You are not seeing two
occurrences of ?x in the same goal state here; those are two
completely separate local theorems. At this point in your proof, you
can say the following to instantiate them differently:

thm Cons.hyps [where x=a]
thm Cons.prems [where x=b]

Here's another unrelated hint about using induct/arbitrary in
structured proofs: You can fix the name of the generalized variables
by using the "case" command with an extra name:

using assms proof (induct ms arbitrary: s)
case (Nil s)
case (Cons m ms s)

Otherwise in your case this variable defaults to the name "x", which I
suppose is a bit less meaningful. Look at "Isabelle > Show Me > Cases"
in Proof General for details.

- Brian

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