Re: [isabelle] Showing that type 'int' is infinite



On 01/02/2007, at 12:38 PM, John Matthews wrote:

I have a subgoal of the form

  1. "~ (finite (UNIV :: int set))"

However, I can't find a corresponding theorem using find_theorems in Isabelle/HOL. Nor was find_theorems produce successful on the terms "card (UNIV :: int set)" or "setsum ?f (UNIV :: int set)".

In my humbling experience you want to avoid "card" for anything involving (possibly) infinite sets - "card (UNIV :: nat set) = 0". IIRC setsum only works properly for finite sets, hence this strange property. Of course "card" has no business having "nat" as a codomain.

With Gerwin's help I cooked up a "has" library, where we can uniformly say "this set has (at least) this many elements, and here are the witnesses." It was cheaper than trying to talk about cardinals. I can polish it up if anyone is interested.

What is the best way to prove this subgoal?

I'm not going to claim this is the best but it does the job in Isabelle2005:

lemma "infinite (UNIV :: int set)"
  using infinite_iff_countable_subset[symmetric] inj_int
  by blast

cheers
peter





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