Re: [isabelle] Showing that type 'int' is infinite
Many thanks to all who responded to my query! I ended up with proving
"inj (f::nat => 'a) ==> infinite (UNIV::'a set)"
using range_inj_infinite finite_subset subset_UNIV
lemmas int_infinite[simp] = infinite_UNIV[OF inj_int]
On Jan 31, 2007, at 5: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)".
What is the best way to prove this subgoal?
This archive was generated by a fusion of
Pipermail (Mailman edition) and