*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Proving cardinality*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 26 Jul 2012 08:54:09 +0200*In-reply-to*: <5010A7CB.1020603@jaist.ac.jp>*References*: <CAP0k5J7mOyzTK0HSkzseihyrrho7_L6kJw-bGmDbP3PCDnNJ_g@mail.gmail.com> <500FA9B2.5070809@jaist.ac.jp> <CAP0k5J6jbDE43YB3PFk8A9dQozCMFazyTNXs0ft4_oRU2-H7nQ@mail.gmail.com> <501087D5.8010505@jaist.ac.jp> <CAP0k5J67dNeCMK07VETaMZtFkiiE0m0TWgHQGjQANg5oqEuUvA@mail.gmail.com> <5010A7CB.1020603@jaist.ac.jp>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:14.0) Gecko/20120713 Thunderbird/14.0

Am 26/07/2012 04:13, schrieb Christian Sternagel: > Dear John, > > I can reproduce your problem but do not have an explanation. There is a thread > about "using" in the mailing list archives: > > > https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-February/msg00019.html > > which is interesting, but does not give an explanation for your case (since S is > not polymorphic). > > To make it easier for others to follow, here is the problem again: > > definition S :: "nat set" where "S == {1, 2, 3}" > lemma "card S > 1" by (auto simp: S_def) (*this works*) > lemma "card S > 1" using S_def apply auto (*leaves the goal*) > 1. S = {Suc 0, 2, 3} ⟹ Suc 0 < card S This is the result of a simplifier heuristic: if it finds an equation "constant = term" among the assumptions, it turns it around. Otherwise the following frequently happens: an equation like "0 = x" is produced in the middle of simplification and then 0 is replaced by x everywhere - not a good idea. The heuristic does not apply to equation that are added to the simplifier explicitly. Tobias > cheers > > chris > > On 07/26/2012 10:06 AM, John Munroe wrote: >> I gave it with 'using S_def'. Do you know why 'using S_def; by auto' >> wouldn't work? > >> On Thu, Jul 26, 2012 at 12:57 AM, Christian Sternagel wrote: >>> For me, by (auto simp: S_def) did the job. So how did you give S_def/ax1 as >>> fact? >

**References**:**[isabelle] Proving cardinality***From:*John Munroe

**Re: [isabelle] Proving cardinality***From:*Christian Sternagel

**Re: [isabelle] Proving cardinality***From:*John Munroe

**Re: [isabelle] Proving cardinality***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] HOLCF equality type class
- Next by Date: [isabelle] Some more project announcements
- Previous by Thread: Re: [isabelle] Proving cardinality
- Next by Thread: [isabelle] sloccount for .thy files?
- Cl-isabelle-users July 2012 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