*To*: Andrei Popescu <uuomul at yahoo.com>*Subject*: Re: [isabelle] question concerning simplification basics*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 10 Jul 2009 14:56:28 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <802683.11722.qm@web56102.mail.re3.yahoo.com>*References*: <802683.11722.qm@web56102.mail.re3.yahoo.com>*User-agent*: Thunderbird 2.0.0.19 (X11/20081227)

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

**References**:**[isabelle] question concerning simplification basics***From:*Andrei Popescu

- Previous by Date: Re: [isabelle] question concerning simplification basics
- Next by Date: [isabelle] schematic variables and antiquotations
- Previous by Thread: Re: [isabelle] question concerning simplification basics
- Next by Thread: [isabelle] Record updates on applications
- Cl-isabelle-users July 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list