[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.