[isabelle] Eliminating two quantifiers in structural proof



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.