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.

Michael.





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