Re: [isabelle] Showing that type 'int' is infinite
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?
Show by finite-induction that any finite non-empty set of integers has
a greatest/least element.
This archive was generated by a fusion of
Pipermail (Mailman edition) and