Theory InfTypeClass

Up to index of Isabelle/HOL/Pi2

InfTypeClass = 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_in_inf_class:

  EX f. inj f