[isabelle] Showing that type 'int' is infinite
John Matthews writes:
> 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)".
> What is the best way to prove this subgoal?
I think the best way is to use the facts that there is an
injection from nats to ints and that there are infinitely
many nats. My proof would go as follows
shows "infinite (UNIV::int set)"
have "inj int" by (rule inj_int)
then have "infinite (range int)" by (rule range_inj_infinite)
have "range int \<subseteq> (UNIV::int set)" by simp
ultimately show "infinite (UNIV::int set)" by (simp add: infinite_super)
This is what you are looking for as "infinite" is defined as
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and