Re: [isabelle] Eliminating two quantifiers in structural proof

Try to use the meta-quantifier !! instead of \<forall> whenever you can, and in
your examples you can. Now if you have an assumption A: "!!x y. P x y" you can
instantiate the quantifiers very easily: just write A[of "t1" "t2"]. Then it is
hardly more verbose than Coq. Note that the instantiation order is not the order
of quantification but the order in which x and y occur in P (from left to
right). In fact, if you inspect A in the proof (eg via command thm) you see that
the !! have disappeared and x/y became ?x/?y.

Unfortunately the "of" operator only works for !!, and !! can only occur at the
"outermost" level, ie not inside HOL formulas. But in many situations that suffices.


Am 15/09/2012 22:15, schrieb Edward Schwartz:
> Hi,
> I am new to Isabelle, and am stuck on a fairly trivial part of my
> proof.  I have an assumption "\forall x y. P x y".  I'd simply like to
> show (P a b) for two terms I have (a and b).  Surprisingly, I am
> having trouble doing this in a structural way.
> With one quantified variable, there is no problem:
> lemma single_proof : "(\<forall>x. P x) \<Longrightarrow> P a"
> proof (erule allE)
>   fix c
>   assume A: "P c"
>   from A show "P c" by assumption
> qed
> My understanding of what is happening is that allE removes the
> quantifier, and so we really just prove /\ c. P c ==> P c.  It seems
> like a better proof would be of /\ c. P ?c ==> P c.  Is there any way
> to do this instead?
> lemma double : "(\<forall>x y. P x y) \<Longrightarrow> P a b"
> apply (erule allE, erule allE)
> apply assumption
> done
> Here is a way to do the proof with tactics.  Unfortunately, in my
> larger proof, the erule commands do not find the correct assumption,
> and so I must specify P manually, which is *very* ugly.
> lemma double_proof : "(\<forall>x y. P x y) \<Longrightarrow> P a b"
> proof (erule allE)
>   fix c
>   assume "\<forall>y. P c y"
>   have "P c b"
>   proof (erule allE) (* error: proof command failed *)
> Finally, I try to do a structural proof, eliminating one quantifier at
> a time, and fail.  I've tried many variations, but can't seem to
> understand how to do this.  If someone could show how to finish this
> proof, and explain why it works, I would greatly appreciate it.
> Overall, Isabelle/HOL seems to make it very difficult to instantiate
> free variables in foralls.  In Coq, this is very easy, since \forall
> x. P x is actually a function that accepts a variable v and returns
> proof that (P v).  What am I missing?
> Thanks,
> Ed

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