Theory ZFC_in_HOL.ZFC_Typeclasses

section ‹Type Classes for ZFC›

theory ZFC_Typeclasses
  imports ZFC_Cardinals Complex_Main

begin

subsection‹The class of embeddable types›

class embeddable =
  assumes ex_inj: "∃V_of :: 'a ⇒ V. inj V_of"

context countable
begin

subclass embeddable
proof -
  have "inj (ord_of_nat ∘ to_nat)" if "inj to_nat"
    for to_nat :: "'a ⇒ nat"
    using that by (simp add: inj_compose inj_ord_of_nat)
  then show "class.embeddable TYPE('a)"
    by intro_classes (meson local.ex_inj)
qed

end

instance unit :: embeddable ..
instance bool :: embeddable ..
instance nat :: embeddable ..
instance int :: embeddable ..
instance rat :: embeddable ..
instance char :: embeddable ..
instance String.literal :: embeddable ..
instance typerep :: embeddable ..


lemma embeddable_classI:
  fixes f :: "'a ⇒ V"
  assumes "⋀x y. f x = f y ⟹ x = y"
  shows "OFCLASS('a, embeddable_class)"
proof (intro_classes, rule exI)
  show "inj f"
    by (rule injI [OF assms]) assumption
qed

instance V :: embeddable
  by (intro_classes) (meson inj_on_id)

instance prod :: (embeddable,embeddable) embeddable
proof -
  have "inj (λ(x,y). ⟨V_of1 x, V_of2 y⟩)" if "inj V_of1" "inj V_of2"
    for V_of1 :: "'a ⇒ V" and V_of2 :: "'b ⇒ V"
    using that by (auto simp: inj_on_def)
  then show "OFCLASS('a × 'b, embeddable_class)"
    by intro_classes (meson embeddable_class.ex_inj)
qed

instance sum :: (embeddable,embeddable) embeddable
proof -
  have "inj (case_sum (Inl ∘ V_of1) (Inr ∘ V_of2))" if "inj V_of1" "inj V_of2"
    for V_of1 :: "'a ⇒ V" and V_of2 :: "'b ⇒ V"
    using that by (auto simp: inj_on_def split: sum.split_asm)
  then show "OFCLASS('a + 'b, embeddable_class)"
    by intro_classes (meson embeddable_class.ex_inj)
qed

instance option :: (embeddable) embeddable
proof -
  have "inj (case_option 0 (λx. ZFC_in_HOL.set{V_of x}))" if "inj V_of"
    for V_of :: "'a ⇒ V"
    using that by (auto simp: inj_on_def split: option.split_asm)
  then show "OFCLASS('a option, embeddable_class)"
    by intro_classes (meson embeddable_class.ex_inj)
qed

primrec V_of_list where
  "V_of_list V_of Nil = 0"
| "V_of_list V_of (x#xs) = ⟨V_of x, V_of_list V_of xs⟩"

lemma inj_V_of_list:
  assumes "inj V_of"
  shows "inj (V_of_list V_of)"
proof -
  note inj_eq [OF assms, simp]
  have "x = y" if "V_of_list V_of x = V_of_list V_of y" for x y
    using that
  proof (induction x arbitrary: y)
    case Nil
    then show ?case
      by (cases y) auto
  next
    case (Cons a x)
    then show ?case
      by (cases y) auto
  qed
  then show ?thesis
    by (auto simp: inj_on_def)
qed

instance list :: (embeddable) embeddable
proof -
  have "inj (rec_list 0 (λx xs r. ⟨V_of x, r⟩))" (is "inj ?f")
    if V_of: "inj V_of" for V_of :: "'a ⇒ V"
  proof -
    note inj_eq [OF V_of, simp]
    have "x = y" if "?f x = ?f y" for x y
      using that
    proof (induction x arbitrary: y)
      case Nil
      then show ?case
        by (cases y) auto
    next
      case (Cons a x)
      then show ?case
        by (cases y) auto
    qed
    then show ?thesis
      by (auto simp: inj_on_def)
  qed
  then show "OFCLASS('a list, embeddable_class)"
    by intro_classes (meson embeddable_class.ex_inj)
qed


subsection‹The class of small types›

class small =
  assumes small: "small (UNIV::'a set)"
begin

subclass embeddable
  by intro_classes (meson local.small small_def)

lemma TC_small [iff]:
  fixes A :: "'a set"
  shows "small A"
  using small smaller_than_small by blast

end

context countable
begin

subclass small
proof -
  have *: "inj (ord_of_nat ∘ to_nat)" if "inj to_nat"
    for to_nat :: "'a ⇒ nat"
    using that by (simp add: inj_compose inj_ord_of_nat)
  then show "class.small TYPE('a)"
    by intro_classes (metis small_image_nat local.ex_inj the_inv_into_onto)
qed

end

lemma lepoll_UNIV_imp_small: "X ≲ (UNIV::'a::small set) ⟹ small X"
  by (meson lepoll_iff replacement small smaller_than_small)

lemma lepoll_imp_small:
  fixes A :: "'a::small set"
  assumes "X ≲ A"
  shows "small X"
  by (metis lepoll_UNIV_imp_small UNIV_I assms lepoll_def subsetI)

instance unit :: small ..
instance bool :: small ..
instance nat :: small ..
instance int :: small ..
instance rat :: small ..
instance char :: small ..
instance String.literal :: small ..
instance typerep :: small ..

instance prod :: (small,small) small
proof -
  have "inj (λ(x,y). ⟨V_of1 x, V_of2 y⟩)"
       "range (λ(x,y). ⟨V_of1 x, V_of2 y⟩) ≤ elts (VSigma A (λx. B))"
    if "inj V_of1" "inj V_of2" "range V_of1 ≤ elts A" "range V_of2 ≤ elts B"
    for V_of1 :: "'a ⇒ V" and V_of2 :: "'b ⇒ V" and A B
    using that by (auto simp: inj_on_def)
  with small [where 'a='a] small [where 'a='b]
  show "OFCLASS('a × 'b, small_class)"
    by intro_classes (smt (verit) down_raw f_inv_into_f set_eq_subset small_def)
qed

instance sum :: (small,small) small
proof -
  have "inj (case_sum (Inl ∘ V_of1) (Inr ∘ V_of2))"
       "range (case_sum (Inl ∘ V_of1) (Inr ∘ V_of2)) ≤ elts (A ⨄ B)"
    if "inj V_of1" "inj V_of2" "range V_of1 ≤ elts A" "range V_of2 ≤ elts B"
    for V_of1 :: "'a ⇒ V" and V_of2 :: "'b ⇒ V" and A B
    using that by (force simp: inj_on_def split: sum.split)+
  with small [where 'a='a] small [where 'a='b]
  show "OFCLASS('a + 'b, small_class)"
    by intro_classes (metis down_raw replacement set_eq_subset small_def small_iff)
qed

instance option :: (small) small
proof -
  have "inj (λx. case x of None ⇒ 0 | Some x ⇒ ZFC_in_HOL.set {V_of x})"
       "range (λx. case x of None ⇒ 0 | Some x ⇒ ZFC_in_HOL.set {V_of x}) ≤ insert 0 (elts (VPow A))"
    if "inj V_of" "range V_of ≤ elts A"
    for V_of :: "'a ⇒ V" and A
    using that  by (auto simp: inj_on_def split: option.split_asm)
  with small [where 'a='a]
  show "OFCLASS('a option, small_class)"
    by intro_classes (smt (verit) down order.refl ex_inj small_iff small_image_iff small_insert)
qed

instance list :: (small) small
proof -
  have "small (range (V_of_list V_of))"
    if "inj V_of" "range V_of ≤ elts A"
    for V_of :: "'a ⇒ V" and A
  proof -
    have "range (V_of_list V_of) ≈ (UNIV :: 'a list set)"
      using that by (simp add: inj_V_of_list)
    also have "… ≈ lists (UNIV :: 'a set)"
      by simp
    also have "… ≲ (UNIV :: 'a set) × (UNIV :: nat set)"
    proof (cases "finite (range (V_of::'a ⇒ V))")
      case True
      then have "lists (UNIV :: 'a set) ≲ (UNIV :: nat set)"
        using countable_iff_lepoll countable_image_inj_on that(1) uncountable_infinite by blast
      then show ?thesis
        by (blast intro: lepoll_trans [OF _ lepoll_times2])
    next
      case False
      then have "lists (UNIV :: 'a set) ≲ (UNIV :: 'a set)"
        using ‹infinite (range V_of)› eqpoll_imp_lepoll infinite_eqpoll_lists by blast
      then show ?thesis
        using lepoll_times1 lepoll_trans by fastforce
    qed
    finally show ?thesis
      by (simp add: lepoll_imp_small)
  qed
  with small [where 'a='a]
  show "OFCLASS('a list, small_class)"
    by intro_classes (metis inj_V_of_list order.refl small_def small_iff small_iff_range)
qed

instance "fun" :: (small,embeddable) embeddable
proof -
  have "inj (λf. VLambda A (λx. V_of2 (f (inv V_of1 x))))"
    if *: "inj V_of1" "inj V_of2" "range V_of1 ≤ elts A"
    for V_of1 :: "'a ⇒ V" and V_of2 :: "'b ⇒ V" and A
  proof -
    have "f u = f' u"
      if "VLambda A (λu. V_of2 (f (inv V_of1 u))) = VLambda A (λx. V_of2 (f' (inv V_of1 x)))"
      for f f' :: "'a ⇒ 'b" and u
      by (metis inv_f_f rangeI subsetD VLambda_eq_D2 [OF that, of "V_of1 u"] *)
    then show ?thesis
      by (auto simp: inj_on_def)
  qed
  then show "OFCLASS('a ⇒ 'b, embeddable_class)"
    by intro_classes (metis embeddable_class.ex_inj small order_refl replacement small_iff)
qed

instance "fun" :: (small,small) small
proof -
  have "inj (λf. VLambda A (λx. V_of2 (f (inv V_of1 x))))"   (is "inj ?φ")
       "range (λf. VLambda A (λx. V_of2 (f (inv V_of1 x)))) ≤ elts (VPi A (λx. B))"
    if *: "inj V_of1" "inj V_of2" "range V_of1 ≤ elts A" and "range V_of2 ≤ elts B"
    for V_of1 :: "'a ⇒ V" and V_of2 :: "'b ⇒ V" and A B
  proof -
    have "f u = f' u"
      if "VLambda A (λu. V_of2 (f (inv V_of1 u))) = VLambda A (λx. V_of2 (f' (inv V_of1 x)))"
      for f f' :: "'a ⇒ 'b" and u
      by (metis inv_f_f rangeI subsetD VLambda_eq_D2 [OF that, of "V_of1 u"] *)
    then show "inj ?φ"
      by (auto simp: inj_on_def)
    show "range ?φ ≤ elts (VPi A (λx. B))"
      using that by (simp add: VPi_I subset_eq)
  qed
  with small [where 'a='a] small [where 'a='b]
  show "OFCLASS('a ⇒ 'b, small_class)"
    by intro_classes (smt (verit, best) down_raw order_refl imageE small_def)
qed

instance set :: (small) small 
proof -
  have 1: "inj (λx. ZFC_in_HOL.set (V_of ` x))"
    if "inj V_of" for V_of :: "'a ⇒ V" 
    by (simp add: inj_on_def inj_image_eq_iff [OF that])
  have 2: "range (λx. ZFC_in_HOL.set (V_of ` x)) ≤ elts (VPow A)"
    if "range V_of ≤ elts A" for V_of :: "'a ⇒ V" and A
    using that by (auto simp: inj_on_def image_subset_iff)
  from small [where 'a='a]
  show "OFCLASS('a set, small_class)"
    by intro_classes (metis 1 2 down_raw imageE small_def order_refl)
qed

instance real :: small 
proof -
  have "small (range (Rep_real))"
    by simp
  then show "OFCLASS(real, small_class)"
    by intro_classes (metis Rep_real_inverse image_inv_f_f inj_on_def replacement)
qed

instance complex :: small 
proof -
  have "⋀c. c ∈ range (λ(x,y). Complex x y)"
    by (metis case_prod_conv complex.exhaust_sel rangeI)
  then show "OFCLASS(complex, small_class)"
    by intro_classes (meson TC_small replacement smaller_than_small subset_eq)
qed

end