Re: [isabelle] induct ... arbitrary: ...
On Tue, Mar 15, 2011 at 5:02 AM, Christian Sternagel
<christian.sternagel at uibk.ac.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)
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and