*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Proving cardinality*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Wed, 25 Jul 2012 17:09:22 +0900*In-reply-to*: <CAP0k5J7mOyzTK0HSkzseihyrrho7_L6kJw-bGmDbP3PCDnNJ_g@mail.gmail.com>*References*: <CAP0k5J7mOyzTK0HSkzseihyrrho7_L6kJw-bGmDbP3PCDnNJ_g@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:14.0) Gecko/20120717 Thunderbird/14.0

How about definition S :: "nat set" where "S ≡ {1,2}" lemma "card S > 1" by (simp add: S_def)

Maybe a nicer way to state S would be context fixes S :: "nat set" assumes S_def: "S = {1, 2}" begin lemma "card S > 1" by (simp add: S_def) end cheers chris On 07/25/2012 08:55 AM, John Munroe wrote:

Hi, I'm trying to prove the cardinality of the set {1,2} being greater than 1, but I seem to be able to only prove that the cardinality is greater than 0: axiomatization S :: "nat set" where ax1 : "S = {1,2}" lemma "card S > 0" using ax1 by (metis card_eq_0_iff finite.emptyI finite.insertI gr0I insert_not_empty) Now I'm trying to prove: lemma "card S > 1" sledgehammer but sledgehammer can't seem to find a proof. Could someone please help? Thanks a lot for your time. John

**Follow-Ups**:**Re: [isabelle] Proving cardinality***From:*John Munroe

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

- Previous by Date: Re: [isabelle] Unicode tokens in jedit
- Next by Date: Re: [isabelle] sloccount for .thy files?
- Previous by Thread: [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