Up to index of Isabelle/HOL/PI

(* Title: InfClass.thy Author: Christine Roeckl InfClass contains all types which are at least countably infinite, e.g., the integers, or the real numbers. For every finite set of elements of any of these types, an element can be found which is not a member of the set. *) InfClass = Main + axclass inf_class < term inf_class "EX (f::nat=>'a). inj f" end

**theorem** *ex_dist1:*

EX b. a ~= b

**theorem** *ex_dist2:*

EX b. b ~= a

**theorem** *lemma:*

[| finite A; inj f |] ==> EX n. ALL a:A. ALL m. a = f m --> m <= n

**theorem** *ex_dist_set:*

finite A ==> EX b. b ~: A

**theorem** *ex_n_dist_set:*

finite A ==> EX B. card B = n & finite B & A Int B = {}

**theorem** *ex_dist_list:*

EX b. ¬ b mem xs

**theorem** *nat_ex_inj:*

EX f. inj f