Quelle  Infinity.thy

section ‹ Infinity Supplement ›

theory Infinity
imports HOL.Real
  "HOL-Library.Infinite_Set"
  "Optics.Two"
begin

text ‹
 This theory introduces a type class @{text infinite} that guarantees that the
 underlying universe of the type is infinite. It also provides useful theorems
 to prove infinity of the universes for various HOL types.
 ›

subsection ‹ Type class @{text infinite} ›

text ‹
 The type class postulates that the universe (carrier) of a type is infinite.
 ›

class infinite =
  assumes infinite_UNIV [simp]: "infinite (UNIV :: 'a set)"

subsection ‹ Infinity Theorems ›

text ‹ Useful theorems to prove that a type's @{const UNIV} is infinite. ›

text ‹
 Note that @{thm [source] infinite_UNIV_nat} is already a simplification rule
 by default.
 ›

lemmas infinite_UNIV_int [simp]

theorem infinite_UNIV_real [simp]:
"infinite (UNIV :: real set)"
  by (rule infinite_UNIV_char_0)

theorem infinite_UNIV_fun1 [simp]:
"infinite (UNIV :: 'a set) ==>
 card (UNIV :: 'b set) ≠ Suc 0 ==>
 infinite (UNIV :: ('a ==> 'b) set)"
  apply (erule contrapos_nn)
  apply (erule finite_fun_UNIVD1)
  apply (assumption)
  done

theorem infinite_UNIV_fun2 [simp]:
"infinite (UNIV :: 'b set) ==>
 infinite (UNIV :: ('a ==> 'b) set)"
  apply (erule contrapos_nn)
  apply (erule finite_fun_UNIVD2)
  done

theorem infinite_UNIV_set [simp]:
"infinite (UNIV :: 'a set) ==>
 infinite (UNIV :: 'a set set)"
  apply (erule contrapos_nn)
  apply (simp add: Finite_Set.finite_set)
  done

theorem infinite_UNIV_prod1 [simp]:
"infinite (UNIV :: 'a set) ==>
 infinite (UNIV :: ('a × 'b) set)"
  apply (erule contrapos_nn)
  apply (simp add: finite_prod)
  done

theorem infinite_UNIV_prod2 [simp]:
"infinite (UNIV :: 'b set) ==>
 infinite (UNIV :: ('a × 'b) set)"
  apply (erule contrapos_nn)
  apply (simp add: finite_prod)
  done

theorem infinite_UNIV_sum1 [simp]:
"infinite (UNIV :: 'a set) ==>
 infinite (UNIV :: ('a + 'b) set)"
  apply (erule contrapos_nn)
  apply (simp)
  done

theorem infinite_UNIV_sum2 [simp]:
"infinite (UNIV :: 'b set) ==>
 infinite (UNIV :: ('a + 'b) set)"
  apply (erule contrapos_nn)
  apply (simp)
  done

theorem infinite_UNIV_list [simp]:
"infinite (UNIV :: 'a list set)"
  apply (rule infinite_UNIV_listI)
  done

theorem infinite_UNIV_option [simp]:
"infinite (UNIV :: 'a set) ==>
 infinite (UNIV :: 'a option set)"
  apply (erule contrapos_nn)
  apply (simp)
  done

theorem infinite_image [intro]:
"infinite A ==> inj_on f A ==> infinite (f ` A)"
  apply (metis finite_imageD)
  done

theorem infinite_transfer (*[intro]*) :
"infinite B ==> B ⊆ f ` A ==> infinite A"
  using infinite_super
  apply (blast)
  done

subsection ‹ Instantiations ›

text ‹
 The instantiations for product and sum types have stronger caveats than in
 principle needed. Namely, it would be sufficient for one type of a product
 or sum to be infinite. A corresponding rule, however, cannot be formulated
 using type classes. Generally, classes are not entirely adequate for the
 purpose of deriving the infinity of HOL types, which is perhaps why a class
 such as @{class infinite} was omitted from the Isabelle/HOL library.
 ›

instance nat :: infinite by (intro_classes, simp)
instance int :: infinite by (intro_classes, simp)
instance real :: infinite by (intro_classes, simp)
instance "fun" :: (type, infinite) infinite by (intro_classes, simp)
instance set :: (infinite) infinite by (intro_classes, simp)
instance prod :: (infinite, infinite) infinite by (intro_classes, simp)
instance sum :: (infinite, infinite) infinite by (intro_classes, simp)
instance list :: (type) infinite by (intro_classes, simp)
instance option :: (infinite) infinite by (intro_classes, simp)

subclass (in infinite) two  by (intro_classes, auto)
    
end