Theory InfClass

Up to index of Isabelle/HOL/PI

theory InfClass = Main
files [InfClass.ML]:
(* 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