Re: [isabelle] Proving cardinality



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

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?






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