Re: [isabelle] Proving cardinality



Thanks. Do you know why 'auto' wouldn't work even if S_def/ax1 is
already given as a fact?

John

On Wed, Jul 25, 2012 at 9:09 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
> 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.