Theory Infinity

(******************************************************************************)
(* Project: Isabelle/UTP Toolkit                                              *)
(* File: Infinity.thy                                                         *)
(* Authors: Frank Zeyda and Simon Foster (University of York, UK)             *)
(* Emails: frank.zeyda@york.ac.uk and simon.foster@york.ac.uk                 *)
(******************************************************************************)

section ‹ Infinity Supplement ›

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

text ‹
  This theory introduces a type class ‹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 ‹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