*To*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Subject*: Re: [isabelle] induct ... arbitrary: ...*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 15 Mar 2011 06:28:20 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4D7F5564.9010403@uibk.ac.at>*References*: <4D7F5564.9010403@uibk.ac.at>*Sender*: huffman.brian.c at gmail.com

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) > 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? Christian, 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

**References**:**[isabelle] induct ... arbitrary: ...***From:*Christian Sternagel

- Previous by Date: [isabelle] induct ... arbitrary: ...
- Next by Date: [isabelle] Theorem-proving for a Bayesian model compiler
- Previous by Thread: [isabelle] induct ... arbitrary: ...
- Next by Thread: [isabelle] Theorem-proving for a Bayesian model compiler
- Cl-isabelle-users March 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list