*To*: John Munroe <munddr at gmail.com>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Proving cardinality*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Thu, 26 Jul 2012 11:13:31 +0900*In-reply-to*: <CAP0k5J67dNeCMK07VETaMZtFkiiE0m0TWgHQGjQANg5oqEuUvA@mail.gmail.com>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:14.0) Gecko/20120717 Thunderbird/14.0

Dear John,

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-February/msg00019.html

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

**Follow-Ups**:**Re: [isabelle] Proving cardinality***From:*Tobias Nipkow

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

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

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

- Previous by Date: [isabelle] skip_proofs in Isabelle2012
- Next by Date: [isabelle] Sledgehammer and Nitpick from the command line?
- Previous by Thread: Re: [isabelle] Proving cardinality
- Next by Thread: Re: [isabelle] Proving cardinality
- 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