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