Email Gateway (Aug 18 2022 at 17:21): Email Gateway (Aug 18 2022 at 17:21):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
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
Email Gateway (Aug 18 2022 at 17:22):From: Brian Huffman <brianh@cs.pdx.edu>
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.
Last updated: Apr 19 2024 at 08:19 UTC