Re: [isabelle] question concerning simplification basics



This is a tricky one to do with types. If you write "using <thms>" then
these thms become part of the proof state, namely new assumptions. But
the simplifier does not instantiate ?-Variables in the proof state -
this is not equivalence preserving. This includes type variables. In
your example one of your assumptions is now "(Q::?'a => bool) = (P::?'a
=> bool)" and this ?'a does not get instantiated with 'a to allow
rewriting the conclusion "Q(x::'a)". If you write "(simp add:thms)"
instead, the simplifier is perfectly happy to instantiate the ?-type
variables as required because they are no longer part of the proof state.

The only time I add simplification rules via "using" is if they need to
be simplified themselves. Otherwise "simp add:" is preferable.

Best
Tobias

Andrei Popescu wrote:
> 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.