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



Many thanks to all who responded to my query! I ended up with proving these lemmas:

  lemma infinite_UNIV:
    "inj (f::nat => 'a) ==> infinite (UNIV::'a set)"
  using range_inj_infinite finite_subset subset_UNIV
  by blast

  lemmas int_infinite[simp] = infinite_UNIV[OF inj_int]

-john

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?

Thanks,
-john







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