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
lemma "infinite (UNIV :: int set)"
using infinite_iff_countable_subset[symmetric] inj_int
This archive was generated by a fusion of
Pipermail (Mailman edition) and