Re: [isabelle] Proving cardinality



How about

  definition S :: "nat set" where
    "S ≡ {1,2}"

  lemma "card S > 1"
    by (simp add: S_def)

The same should work with your axiomatic version (but I don't see why you would use an axiom in this case). Just give the equation of the axiom an explicit name and supply it to simp.

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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.