# [isabelle] question concerning simplification basics

Hello,
In the scripts below, why does lemma "try" succeed whilst lemma "try2" fails? ("try2" fails not only with force, but also with auto and blast, not to mention simp).
Thank you in advance,
Andrei Popescu
consts P::"'a => bool"
definition Q :: "'a => bool"
where "Q = P"
lemma try:
"P x ==> Q x"
proof-
assume "P x"
thus "Q x" by (simp add: Q_def)
qed
lemma try2:
"P x ==> Q x"
proof-
assume "P x"
thus "Q x" using Q_def by force (* THIS FAILS *)
qed
--- On Wed, 7/8/09, Andrei Popescu <uuomul at yahoo.com> wrote:
From: Andrei Popescu <uuomul at yahoo.com>
Subject: set comprehension with pairs
To: cl-isabelle-users at lists.cam.ac.uk
Date: Wednesday, July 8, 2009, 3:21 AM
Hello,
Given P :: 'a => 'b => bool,
I would like to know what does the expression
{(x,y). P x y}
*precisely* stand for.
Is it something like
{z. EX x y. z = (x,y) /\ P x y} ?
Knowing this would help me deal more easily with some trivial set theory that seems reluctant to blasting. I would also appreciate if someone showed me not only the answer to this, but also the way I could have found out myself looking at the online libraries.
Thank you in advance,
Andrei Popescu

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