(* Title: HF_SetCat Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2020 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) chapter "The Category of Hereditarily Finite Sets" theory HF_SetCat imports CategoryWithFiniteLimits CartesianClosedCategory HereditarilyFinite.HF begin text‹ This theory constructs a category whose objects are in bijective correspondence with the hereditarily finite sets and whose arrows correspond to the functions between such sets. We show that this category is cartesian closed and has finite limits. Note that up to this point we have not constructed any other interpretation for the @{locale cartesian_closed_category} locale, but it is important to have one to ensure that the locale assumptions are consistent. › section "Preliminaries" text‹ We begin with some preliminary definitions and facts about hereditarily finite sets, which are better targeted toward what we are trying to do here than what already exists in @{theory HereditarilyFinite.HF}. › text‹ The following defines when a hereditarily finite set ‹F› represents a function from a hereditarily finite set ‹B› to a hereditarily finite set ‹C›. Specifically, ‹F› must be a relation from ‹B› to ‹C›, whose domain is ‹B›, whose range is contained in ‹C›, and which is single-valued on its domain. › definition hfun where "hfun B C F ≡ F ≤ B * C ∧ hfunction F ∧ hdomain F = B ∧ hrange F ≤ C" lemma hfunI [intro]: assumes "F ≤ A * B" and "⋀X. X ❙∈A ⟹ ∃!Y. ⟨X, Y⟩ ❙∈F" and "⋀X Y. ⟨X, Y⟩ ❙∈F ⟹ Y ❙∈B" shows "hfun A B F" unfolding hfun_def using assms hfunction_def hrelation_def is_hpair_def hrange_def hconverse_def hdomain_def apply (intro conjI) apply auto by fast lemma hfunE [elim]: assumes "hfun B C F" and "(⋀Y. Y ❙∈B ⟹ (∃!Z. ⟨Y, Z⟩ ❙∈F) ∧ (∀Z. ⟨Y, Z⟩ ❙∈F ⟶ Z ❙∈C)) ⟹ T" shows T proof - have "⋀Y. Y ❙∈B ⟹ (∃!Z. ⟨Y, Z⟩ ❙∈F) ∧ (∀Z. ⟨Y, Z⟩ ❙∈F ⟶ Z ❙∈C)" proof (intro allI impI conjI) fix Y assume Y: "Y ❙∈B" show "∃!Z. ⟨Y, Z⟩ ❙∈F" proof - have "∃Z. ⟨Y, Z⟩ ❙∈F" using assms Y hfun_def hdomain_def by auto moreover have "⋀Z Z'. ⟦ ⟨Y, Z⟩ ❙∈F; ⟨Y, Z'⟩ ❙∈F ⟧ ⟹ Z = Z'" using assms hfun_def hfunction_def by simp ultimately show ?thesis by blast qed show "⋀Z. ⟨Y, Z⟩ ❙∈F ⟹ Z ❙∈C" using assms Y hfun_def by auto qed thus ?thesis using assms(2) by simp qed text‹ The hereditarily finite set ‹hexp B C› represents the collection of all functions from ‹B› to ‹C›. › definition hexp where "hexp B C = ⦃F ❙∈HPow (B * C). hfun B C F⦄" lemma hfun_in_hexp: assumes "hfun B C F" shows "F ❙∈hexp B C" using assms by (simp add: hexp_def hfun_def) text‹ The function ‹happ› applies a function ‹F› from ‹B› to ‹C› to an element of ‹B›, yielding an element of ‹C›. › abbreviation happ where "happ ≡ app" lemma happ_mapsto: assumes "F ❙∈hexp B C" and "Y ❙∈B" shows "happ F Y ❙∈C" and "happ F Y ❙∈hrange F" proof - show "happ F Y ❙∈C" using assms app_def hexp_def app_equality hdomain_def hfun_def by auto show "happ F Y ❙∈hrange F" proof - have "⟨Y, happ F Y⟩ ❙∈F" using assms app_def hexp_def app_equality hdomain_def hfun_def by auto thus ?thesis using hdomain_def hrange_def hconverse_def by auto qed qed lemma happ_expansion: assumes "hfun B C F" shows "F = ⦃XY ❙∈B * C. hsnd XY = happ F (hfst XY)⦄" proof fix XY show "XY ❙∈F ⟷ XY ❙∈⦃XY ❙∈B * C. hsnd XY = happ F (hfst XY)⦄" proof show "XY ❙∈F ⟹ XY ❙∈⦃XY ❙∈B * C. hsnd XY = happ F (hfst XY)⦄" proof - assume XY: "XY ❙∈F" have "XY ❙∈B * C" using assms XY hfun_def by auto moreover have "hsnd XY = happ F (hfst XY)" using assms XY hfunE app_def [of F "hfst XY"] the1_equality [of "λy. ⟨hfst XY, y⟩ ❙∈F"] calculation by auto ultimately show "XY ❙∈⦃XY ❙∈B * C. hsnd XY = happ F (hfst XY)⦄" by simp qed show "XY ❙∈⦃XY ❙∈B * C. hsnd XY = happ F (hfst XY)⦄ ⟹ XY ❙∈F" proof - assume XY: "XY ❙∈⦃XY ❙∈B * C. hsnd XY = happ F (hfst XY)⦄" show "XY ❙∈F" using assms XY app_def [of F "hfst XY"] the1_equality [of "λy. ⟨hfst XY, y⟩ ❙∈F"] by fastforce qed qed qed text‹ Function ‹hlam› takes a function ‹F› from ‹A * B› to ‹C› to a function ‹hlam F› from ‹A› to ‹hexp B C›. › definition hlam where "hlam A B C F = ⦃XG ❙∈A * hexp B C. ∀YZ. YZ ❙∈hsnd XG ⟷ is_hpair YZ ∧ ⟨⟨hfst XG, hfst YZ⟩, hsnd YZ⟩ ❙∈F⦄" lemma hfun_hlam: assumes "hfun (A * B) C F" shows "hfun A (hexp B C) (hlam A B C F)" proof show "hlam A B C F ≤ A * hexp B C" using assms hlam_def by auto show "⋀X. X ❙∈A ⟹ ∃!Y. ⟨X, Y⟩ ❙∈hlam A B C F" proof fix X assume X: "X ❙∈A" let ?G = "⦃YZ ❙∈B * C. ⟨⟨X, hfst YZ⟩, hsnd YZ⟩ ❙∈F⦄" have 1: "?G ❙∈hexp B C" using assms X hexp_def by fastforce show "⟨X, ?G⟩ ❙∈hlam A B C F" using assms X 1 is_hpair_def hfun_def hlam_def by auto fix Y assume XY: "⟨X, Y⟩ ❙∈hlam A B C F" show "Y = ?G" using assms X XY hlam_def hexp_def by fastforce qed show "⋀X Y. ⟨X, Y⟩ ❙∈hlam A B C F ⟹ Y ❙∈hexp B C" using assms hlam_def hexp_def by simp qed lemma happ_hlam: assumes "X ❙∈A" and "hfun (A * B) C F" shows "∃!G. ⟨X, G⟩ ❙∈hlam A B C F" and "happ (hlam A B C F) X = (THE G. ⟨X, G⟩ ❙∈hlam A B C F)" and "happ (hlam A B C F) X = ⦃yz ❙∈B * C. ⟨⟨X, hfst yz⟩, hsnd yz⟩ ❙∈F⦄" and "Y ❙∈B ⟹ happ (happ (hlam A B C F) X) Y = happ F ⟨X, Y⟩" proof - show 1: "∃!G. ⟨X, G⟩ ❙∈hlam A B C F" using assms(1,2) hfun_hlam hfunE by (metis (full_types)) show 2: "happ (hlam A B C F) X = (THE G. ⟨X, G⟩ ❙∈hlam A B C F)" using assms app_def by simp show "happ (happ (hlam A B C F) X) Y = happ F ⟨X, Y⟩" proof - have 3: "⟨X, happ (hlam A B C F) X⟩ ❙∈hlam A B C F" using assms(1) 1 2 theI' [of "λG. ⟨X, G⟩ ❙∈hlam A B C F"] by simp hence "∃!Z. happ (happ (hlam A B C F) X) = Z" by simp moreover have "happ (happ (hlam A B C F) X) Y = happ F ⟨X, Y⟩" using assms(1-2) 3 hlam_def is_hpair_def app_def by simp ultimately show ?thesis by simp qed show "happ (hlam A B C F) X = ⦃YZ ❙∈B * C. ⟨⟨X, hfst YZ⟩, hsnd YZ⟩ ❙∈F⦄" proof - let ?G = "⦃YZ ❙∈B * C. ⟨⟨X, hfst YZ⟩, hsnd YZ⟩ ❙∈F⦄" have 4: "hfun B C ?G" proof show "⦃YZ ❙∈B * C. ⟨⟨X, hfst YZ⟩, hsnd YZ⟩ ❙∈F⦄ ≤ B * C" using assms by auto show "⋀Y. Y ❙∈B ⟹ ∃!Z. ⟨Y, Z⟩ ❙∈⦃YZ ❙∈B * C. ⟨⟨X, hfst YZ⟩, hsnd YZ⟩ ❙∈F⦄" proof - fix Y assume Y: "Y ❙∈B" have XY: "⟨X, Y⟩ ❙∈A * B" using assms Y by simp hence 1: "∃!Z. ⟨⟨X, Y⟩, Z⟩ ❙∈F" using assms XY hfunE [of "A * B" C F] by metis obtain Z where Z: "⟨⟨X, Y⟩, Z⟩ ❙∈F" using 1 by auto have "∃Z. ⟨Y, Z⟩ ❙∈⦃YZ ❙∈B * C. ⟨⟨X, hfst YZ⟩, hsnd YZ⟩ ❙∈F⦄" proof - have "⟨Y, Z⟩ ❙∈B * C" using assms Y Z by blast moreover have "⟨⟨X, hfst ⟨Y, Z⟩⟩, hsnd ⟨Y, Z⟩⟩ ❙∈F" using assms Y Z by simp ultimately show ?thesis by auto qed moreover have "⋀Z Z'. ⟦⟨Y, Z⟩ ❙∈⦃YZ ❙∈B * C. ⟨⟨X, hfst YZ⟩, hsnd YZ⟩ ❙∈F⦄; ⟨Y, Z'⟩ ❙∈⦃YZ ❙∈B * C. ⟨⟨X, hfst YZ⟩, hsnd YZ⟩ ❙∈F⦄⟧ ⟹ Z = Z'" using assms Y by auto ultimately show "∃!Z. ⟨Y, Z⟩ ❙∈⦃YZ ❙∈B * C. ⟨⟨X, hfst YZ⟩, hsnd YZ⟩ ❙∈F⦄" by auto qed show "⋀Y Z. ⟨Y, Z⟩ ❙∈⦃YZ ❙∈B * C. ⟨⟨X, hfst YZ⟩, hsnd YZ⟩ ❙∈F⦄ ⟹ Z ❙∈C" using assms by simp qed have "⟨X, ?G⟩ ❙∈hlam A B C F" proof - have "⟨X, ?G⟩ ❙∈A * hexp B C" using assms 4 by (simp add: hfun_in_hexp) moreover have "∀YZ. YZ ❙∈?G ⟷ is_hpair YZ ∧ ⟨⟨X, hfst YZ⟩, hsnd YZ⟩ ❙∈F" using assms 1 is_hpair_def hfun_def by auto ultimately show ?thesis using assms 1 hlam_def by simp qed thus "happ (hlam A B C F) X = ?G" using assms 2 4 app_equality hfun_def hfun_hlam by auto qed qed section "Construction of the Category" locale hfsetcat begin text‹ We construct the category of hereditarily finite sets and functions simply by applying the generic ``set category'' construction, using the hereditarily finite sets as the universe, and constraining the collections of such sets that determine objects of the category to those that are finite. › interpretation setcat ‹TYPE(hf)› finite using finite_subset by unfold_locales blast+ interpretation set_category comp ‹λA. A ⊆ Collect terminal ∧ finite (elem_of ` A)› using is_set_category by blast lemma set_ide_char: shows "A ∈ set ` Collect ide ⟷ A ⊆ Univ ∧ finite A" proof assume A: "A ∈ set ` Collect ide" show "A ⊆ Univ ∧ finite A" proof show "A ⊆ Univ" using A setp_set' by auto obtain a where a: "ide a ∧ A = set a" using A by blast have "finite (elem_of ` set a)" using a setp_set_ide by blast moreover have "inj_on elem_of (set a)" proof - have "inj_on elem_of Univ" using bij_elem_of bij_betw_imp_inj_on by auto moreover have "set a ⊆ Univ" using a setp_set' [of a] by blast ultimately show ?thesis using inj_on_subset by auto qed ultimately show "finite A" using a A finite_imageD [of elem_of "set a"] by blast qed next assume A: "A ⊆ Univ ∧ finite A" have "ide (mkIde A)" using A ide_mkIde by simp moreover have "set (mkIde A) = A" using A finite_imp_setp set_mkIde by presburger ultimately show "A ∈ set ` Collect ide" by blast qed lemma set_ideD: assumes "ide a" shows "set a ⊆ Univ" and "finite (set a)" using assms set_ide_char by auto lemma ide_mkIdeI [intro]: assumes "A ⊆ Univ" and "finite A" shows "ide (mkIde A)" and "set (mkIde A) = A" using assms ide_mkIde set_mkIde by auto interpretation category_with_terminal_object comp using terminal_unity by unfold_locales auto text‹ We verify that the objects of HF are indeed in bijective correspondence with the hereditarily finite sets. › definition ide_to_hf where "ide_to_hf a = HF (elem_of ` set a)" definition hf_to_ide where "hf_to_ide x = mkIde (arr_of ` hfset x)" lemma ide_to_hf_mapsto: shows "ide_to_hf ∈ Collect ide → UNIV" by simp lemma hf_to_ide_mapsto: shows "hf_to_ide ∈ UNIV → Collect ide" proof fix x :: hf have "finite (arr_of ` hfset x)" by simp moreover have "arr_of ` hfset x ⊆ Univ" by (metis (mono_tags, lifting) UNIV_I bij_arr_of bij_betw_def imageE image_eqI subsetI) ultimately have "ide (mkIde (arr_of ` hfset x))" using finite_imp_setp ide_mkIde by presburger thus "hf_to_ide x ∈ Collect ide" using hf_to_ide_def by simp qed lemma hf_to_ide_ide_to_hf: assumes "a ∈ Collect ide" shows "hf_to_ide (ide_to_hf a) = a" proof - have "hf_to_ide (ide_to_hf a) = mkIde (arr_of ` hfset (HF (elem_of ` set a)))" using hf_to_ide_def ide_to_hf_def by simp also have "... = a" proof - have "mkIde (arr_of ` hfset (HF (elem_of ` set a))) = mkIde (arr_of ` elem_of ` set a)" proof - have "finite (set a)" using assms set_ide_char by blast hence "finite (elem_of ` set a)" by simp hence "hfset (HF (elem_of ` set a)) = elem_of ` set a" using hfset_HF [of "elem_of ` set a"] by simp thus ?thesis by simp qed also have "... = a" proof - have "set a ⊆ Univ" using assms set_ide_char by blast hence "⋀x. x ∈ set a ⟹ arr_of (elem_of x) = x" using assms by auto hence "arr_of ` elem_of ` set a = set a" by force thus ?thesis using assms ide_char mkIde_set by simp qed finally show ?thesis by blast qed finally show "hf_to_ide (ide_to_hf a) = a" by blast qed lemma ide_to_hf_hf_to_ide: assumes "x ∈ UNIV" shows "ide_to_hf (hf_to_ide x) = x" proof - have "HF (elem_of ` set (mkIde (arr_of ` hfset x))) = x" proof - have "HF (elem_of ` set (mkIde (arr_of ` hfset x))) = HF (elem_of ` arr_of ` hfset x)" using assms set_mkIde [of "arr_of ` hfset x"] arr_of_mapsto mkIde_def by auto also have "... = HF (hfset x)" proof - have "⋀A. elem_of ` arr_of ` A = A" using elem_of_arr_of by force thus ?thesis by metis qed also have "... = x" by simp finally show ?thesis by blast qed thus ?thesis using assms ide_to_hf_def hf_to_ide_def by simp qed lemma bij_betw_ide_hf_set: shows "bij_betw ide_to_hf (Collect ide) (UNIV :: hf set)" using ide_to_hf_mapsto hf_to_ide_mapsto ide_to_hf_hf_to_ide hf_to_ide_ide_to_hf by (intro bij_betwI) auto lemma ide_implies_finite_set: assumes "ide a" shows "finite (set a)" and "finite (hom unity a)" proof - show 1: "finite (set a)" using assms set_ide_char by blast show "finite (hom unity a)" using assms 1 bij_betw_points_and_set finite_imageD inj_img set_def by auto qed text‹ We establish the connection between the membership relation defined for hereditarily finite sets and the corresponding membership relation associated with the set category. › lemma arr_of_membI [intro]: assumes "x ❙∈ide_to_hf a" shows "arr_of x ∈ set a" proof - let ?X = "inv_into (set a) elem_of x" have "x = elem_of ?X ∧ ?X ∈ set a" using assms by (simp add: f_inv_into_f ide_to_hf_def inv_into_into) thus ?thesis by (metis (no_types, lifting) arr_of_elem_of elem_set_implies_incl_in elem_set_implies_set_eq_singleton incl_in_def mem_Collect_eq terminal_char2) qed lemma elem_of_membI [intro]: assumes "ide a" and "x ∈ set a" shows "elem_of x ❙∈ide_to_hf a" proof - have "finite (elem_of ` set a)" using assms ide_implies_finite_set [of a] by simp hence "elem_of x ∈ hfset (ide_to_hf a)" using assms ide_to_hf_def hfset_HF [of "elem_of ` set a"] by simp thus ?thesis using hmem_def by blast qed text‹ We show that each hom-set ‹hom a b› is in bijective correspondence with the elements of the hereditarily finite set ‹hfun (ide_to_hf a) (ide_to_hf b)›. › definition arr_to_hfun where "arr_to_hfun f = ⦃XY ❙∈ide_to_hf (dom f) * ide_to_hf (cod f). hsnd XY = elem_of (Fun f (arr_of (hfst XY)))⦄" definition hfun_to_arr where "hfun_to_arr B C F = mkArr (arr_of ` hfset B) (arr_of ` hfset C) (λx. arr_of (happ F (elem_of x)))" lemma hfun_arr_to_hfun: assumes "arr f" shows "hfun (ide_to_hf (dom f)) (ide_to_hf (cod f)) (arr_to_hfun f)" proof show "arr_to_hfun f ≤ ide_to_hf (dom f) * ide_to_hf (cod f)" using assms arr_to_hfun_def by auto show "⋀X. X ❙∈ide_to_hf (dom f) ⟹ ∃!Y. ⟨X, Y⟩ ❙∈arr_to_hfun f" proof fix X assume X: "X ❙∈ide_to_hf (dom f)" show "⟨X, elem_of (Fun f (arr_of X))⟩ ❙∈arr_to_hfun f" proof - have "⟨X, elem_of (Fun f (arr_of X))⟩ ❙∈⦃XY ❙∈ide_to_hf (dom f) * ide_to_hf (cod f). hsnd XY = elem_of (Fun f (arr_of (hfst XY)))⦄" proof - have "hsnd ⟨X, elem_of (Fun f (arr_of X))⟩ = elem_of (Fun f (arr_of (hfst ⟨X, elem_of (Fun f (arr_of X))⟩)))" using assms X by simp moreover have "⟨X, elem_of (Fun f (arr_of X))⟩ ❙∈ide_to_hf (dom f) * ide_to_hf (cod f)" proof - have "elem_of (Fun f (arr_of X)) ❙∈ide_to_hf (cod f)" proof (intro elem_of_membI) show "ide (cod f)" using assms ide_cod by simp show "Fun f (arr_of X) ∈ Cod f" using assms X Fun_mapsto arr_of_membI by auto qed thus ?thesis using X by simp qed ultimately show ?thesis by simp qed thus ?thesis using arr_to_hfun_def by simp qed fix Y assume XY: "⟨X, Y⟩ ❙∈arr_to_hfun f" show "Y = elem_of (Fun f (arr_of X))" using assms X XY arr_to_hfun_def by auto qed show "⋀X Y. ⟨X, Y⟩ ❙∈arr_to_hfun f ⟹ Y ❙∈ide_to_hf (cod f)" using assms arr_to_hfun_def ide_to_hf_def ‹arr_to_hfun f ≤ ide_to_hf (dom f) * ide_to_hf (cod f)› by blast qed lemma arr_to_hfun_in_hexp: assumes "arr f" shows "arr_to_hfun f ❙∈hexp (ide_to_hf (dom f)) (ide_to_hf (cod f))" using assms arr_to_hfun_def hfun_arr_to_hfun hexp_def by auto lemma hfun_to_arr_in_hom: assumes "hfun B C F" shows "«hfun_to_arr B C F : hf_to_ide B → hf_to_ide C»" proof let ?f = "mkArr (arr_of ` hfset B) (arr_of ` hfset C) (λx. arr_of (happ F (elem_of x)))" have 0: "arr ?f" proof - have "arr_of ` hfset B ⊆ Univ ∧ arr_of ` hfset C ⊆ Univ" using arr_of_mapsto by auto moreover have "(λx. arr_of (happ F (elem_of x))) ∈ arr_of ` hfset B → arr_of ` hfset C" proof fix x assume x: "x ∈ arr_of ` hfset B" have "happ F (elem_of x) ∈ hfset C" using assms x happ_mapsto hfun_in_hexp by (metis elem_of_arr_of HF_hfset finite_hfset hmem_HF_iff imageE) thus "arr_of (happ F (elem_of x)) ∈ arr_of ` hfset C" by simp qed ultimately show ?thesis using arr_mkArr by (meson finite_hfset finite_iff_ordLess_natLeq finite_imageI) qed show 1: "arr (hfun_to_arr B C F)" using 0 hfun_to_arr_def by simp show "dom (hfun_to_arr B C F) = hf_to_ide B" using 1 hfun_to_arr_def hf_to_ide_def dom_mkArr by auto show "cod (hfun_to_arr B C F) = hf_to_ide C" using 1 hfun_to_arr_def hf_to_ide_def cod_mkArr by auto qed text‹ The comprehension notation from @{theory HereditarilyFinite.HF} interferes in an unfortunate way with the restriction notation from @{theory "HOL-Library.FuncSet"}, making it impossible to use both in the present context. › lemma Fun_char: assumes "arr f" shows "Fun f = restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f)" proof fix x show "Fun f x = restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f) x" proof (cases "x ∈ Dom f") show "x ∉ Dom f ⟹ ?thesis" using assms Fun_mapsto Fun_def restrict_apply by simp show "x ∈ Dom f ⟹ ?thesis" proof - assume x: "x ∈ Dom f" have 1: "hfun (ide_to_hf (dom f)) (ide_to_hf (cod f)) (arr_to_hfun f)" using assms app_def arr_to_hfun_def hfun_arr_to_hfun the1_equality [of "λy. ⟨elem_of x, y⟩ ❙∈arr_to_hfun f" "elem_of (Fun f x)"] by simp have 2: "∃!Y. ⟨elem_of x, Y⟩ ❙∈arr_to_hfun f" using assms x 1 hfunE elem_of_membI ide_dom by (metis (no_types, lifting)) have "Fun f x = arr_of (elem_of (Fun f x))" proof - have "Fun f x ∈ Univ" using assms x ide_cod Fun_mapsto [of f] set_ide_char by blast thus ?thesis using arr_of_elem_of by simp qed also have "... = arr_of (happ (arr_to_hfun f) (elem_of x))" proof - have "⟨elem_of x, elem_of (Fun f x)⟩ ❙∈arr_to_hfun f" proof - have "⟨elem_of x, elem_of (Fun f x)⟩ ❙∈ide_to_hf (dom f) * ide_to_hf (cod f)" using assms x ide_dom ide_cod Fun_mapsto by fast moreover have "elem_of (Fun f x) = elem_of (Fun f (arr_of (elem_of x)))" by (metis (no_types, lifting) arr_of_elem_of setp_set_ide assms ide_dom subsetD x) ultimately show ?thesis using arr_to_hfun_def by auto qed moreover have "⟨elem_of x, happ (arr_to_hfun f) (elem_of x)⟩ ❙∈arr_to_hfun f" using assms x 1 2 app_equality hfun_def by blast ultimately show ?thesis using 2 by fastforce qed also have "... = restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f) x" using assms x ide_dom by auto finally show ?thesis by simp qed qed qed lemma Fun_hfun_to_arr: assumes "hfun B C F" shows "Fun (hfun_to_arr B C F) = restrict (λx. arr_of (happ F (elem_of x))) (arr_of ` hfset B)" proof - have "arr (hfun_to_arr B C F)" using assms hfun_to_arr_in_hom by blast hence "arr (mkArr (arr_of ` hfset B) (arr_of ` hfset C) (λx. arr_of (happ F (elem_of x))))" using hfun_to_arr_def by simp thus ?thesis using assms hfun_to_arr_def Fun_mkArr by simp qed lemma arr_of_img_hfset_ide_to_hf: assumes "ide a" shows "arr_of ` hfset (ide_to_hf a) = set a" proof - have "arr_of ` hfset (ide_to_hf a) = arr_of ` hfset (HF (elem_of ` set a))" using ide_to_hf_def by simp also have "... = arr_of ` elem_of ` set a" using assms ide_implies_finite_set(1) ide_char by auto also have "... = set a" proof - have "⋀x. x ∈ set a ⟹ arr_of (elem_of x) = x" using assms ide_char arr_of_elem_of setp_set_ide by blast thus ?thesis by force qed finally show ?thesis by blast qed lemma hfun_to_arr_arr_to_hfun: assumes "arr f" shows "hfun_to_arr (ide_to_hf (dom f)) (ide_to_hf (cod f)) (arr_to_hfun f) = f" proof - have 0: "hfun_to_arr (ide_to_hf (dom f)) (ide_to_hf (cod f)) (arr_to_hfun f) = mkArr (arr_of ` hfset (ide_to_hf (dom f))) (arr_of ` hfset (ide_to_hf (cod f))) (λx. arr_of (happ (arr_to_hfun f) (elem_of x)))" unfolding hfun_to_arr_def by blast also have "... = mkArr (Dom f) (Cod f) (restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f))" proof (intro mkArr_eqI) show 1: "arr_of ` hfset (ide_to_hf (dom f)) = Dom f" using assms arr_of_img_hfset_ide_to_hf ide_dom by simp show 2: "arr_of ` hfset (ide_to_hf (cod f)) = Cod f" using assms arr_of_img_hfset_ide_to_hf ide_cod by simp show "arr (mkArr (arr_of ` hfset (ide_to_hf (dom f))) (arr_of ` hfset (ide_to_hf (cod f))) (λx. arr_of (happ (arr_to_hfun f) (elem_of x))))" using 0 1 2 by (metis (no_types, lifting) arrI assms hfun_arr_to_hfun hfun_to_arr_in_hom) show "⋀x. x ∈ arr_of ` hfset (ide_to_hf (dom f)) ⟹ arr_of (happ (arr_to_hfun f) (elem_of x)) = restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f) x" using assms 1 by simp qed also have "... = mkArr (Dom f) (Cod f) (Fun f)" using assms Fun_char mkArr_eqI by simp also have "... = f" using assms mkArr_Fun by blast finally show ?thesis by simp qed lemma arr_to_hfun_hfun_to_arr: assumes "hfun B C F" shows "arr_to_hfun (hfun_to_arr B C F) = F" proof - have "arr_to_hfun (hfun_to_arr B C F) = ⦃XY ❙∈ide_to_hf (dom (hfun_to_arr B C F)) * ide_to_hf (cod (hfun_to_arr B C F)). hsnd XY = elem_of (Fun (hfun_to_arr B C F) (arr_of (hfst XY)))⦄" unfolding arr_to_hfun_def by blast also have "... = ⦃XY ❙∈ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)). hsnd XY = elem_of (Fun (hfun_to_arr B C F) (arr_of (hfst XY)))⦄" using assms hfun_to_arr_in_hom [of B C F] hf_to_ide_def by (metis (no_types, lifting) in_homE) also have "... = ⦃XY ❙∈ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)). hsnd XY = elem_of (restrict (λx. arr_of (happ F (elem_of x))) (arr_of ` hfset B) (arr_of (hfst XY)))⦄" using assms Fun_hfun_to_arr by simp also have "... = ⦃XY ❙∈ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)). hsnd XY = elem_of (arr_of (happ F (elem_of (arr_of (hfst XY)))))⦄" proof - have 1: "⋀XY. XY ❙∈ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)) ⟹ arr_of (hfst XY) ∈ arr_of ` hfset B" proof - fix XY assume XY: "XY ❙∈ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C))" have "hfst XY ❙∈ide_to_hf (mkIde (arr_of ` hfset B))" using XY by auto thus "arr_of (hfst XY) ∈ arr_of ` hfset B" using assms arr_of_membI [of "hfst XY" "mkIde (arr_of ` hfset B)"] set_mkIde by (metis (mono_tags, lifting) arrI arr_mkArr hfun_to_arr_def hfun_to_arr_in_hom) qed show ?thesis proof - have "⋀XY. (XY ❙∈ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)) ∧ hsnd XY = elem_of (restrict (λx. arr_of (happ F (elem_of x))) (arr_of ` hfset B) (arr_of (hfst XY)))) ⟷ (XY ❙∈ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)) ∧ hsnd XY = elem_of (arr_of (happ F (elem_of (arr_of (hfst XY))))))" using 1 by auto thus ?thesis by blast qed qed also have "... = ⦃XY ❙∈ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)). hsnd XY = happ F (hfst XY)⦄" by simp also have "... = ⦃XY ❙∈B * C. hsnd XY = happ F (hfst XY)⦄" using assms hf_to_ide_def ide_to_hf_hf_to_ide by force also have "... = F" using assms happ_expansion by simp finally show ?thesis by simp qed lemma bij_betw_hom_hfun: assumes "ide a" and "ide b" shows "bij_betw arr_to_hfun (hom a b) {F. hfun (ide_to_hf a) (ide_to_hf b) F}" proof (intro bij_betwI) show "arr_to_hfun ∈ hom a b → {F. hfun (ide_to_hf a) (ide_to_hf b) F}" using assms arr_to_hfun_in_hexp hexp_def hfun_arr_to_hfun by blast show "hfun_to_arr (ide_to_hf a) (ide_to_hf b) ∈ {F. hfun (ide_to_hf a) (ide_to_hf b) F} → hom a b" using assms hfun_to_arr_in_hom by (metis (no_types, lifting) Pi_I hf_to_ide_ide_to_hf mem_Collect_eq) show "⋀x. x ∈ hom a b ⟹ hfun_to_arr (ide_to_hf a) (ide_to_hf b) (arr_to_hfun x) = x" using assms hfun_to_arr_arr_to_hfun by blast show "⋀y. y ∈ {F. hfun (ide_to_hf a) (ide_to_hf b) F} ⟹ arr_to_hfun (hfun_to_arr (ide_to_hf a) (ide_to_hf b) y) = y" using assms arr_to_hfun_hfun_to_arr by simp qed text‹ We next relate composition of arrows in the category to the corresponding operation on hereditarily finite sets. › definition hcomp where "hcomp G F = ⦃XZ ❙∈hdomain F * hrange G. hsnd XZ = happ G (happ F (hfst XZ))⦄" lemma hfun_hcomp: assumes "hfun A B F" and "hfun B C G" shows "hfun A C (hcomp G F)" proof show "hcomp G F ≤ A * C" using assms hcomp_def hfun_def by auto show "⋀X. X ❙∈A ⟹ ∃!Y. ⟨X, Y⟩ ❙∈hcomp G F" proof fix X assume X: "X ❙∈A" show "⟨X, happ G (happ F X)⟩ ❙∈hcomp G F" unfolding hcomp_def using assms X hfunE happ_mapsto hfun_in_hexp by (metis (mono_tags, lifting) HCollect_iff hfst_conv hfun_def hsnd_conv timesI) show "⋀X Y. ⟦X ❙∈A; ⟨X, Y⟩ ❙∈hcomp G F⟧ ⟹ Y = happ G (happ F X)" unfolding hcomp_def by simp qed show "⋀X Y. ⟨X, Y⟩ ❙∈hcomp G F ⟹ Y ❙∈C" unfolding hcomp_def using assms hfunE happ_mapsto hfun_in_hexp by (metis HCollectE hfun_def hsubsetCE timesD2) qed lemma arr_to_hfun_comp: assumes "seq g f" shows "arr_to_hfun (comp g f) = hcomp (arr_to_hfun g) (arr_to_hfun f)" proof - have 1: "hdomain (arr_to_hfun f) = ide_to_hf (dom f)" using assms hfun_arr_to_hfun hfun_def by blast have "arr_to_hfun (comp g f) = ⦃XZ ❙∈ide_to_hf (dom f) * ide_to_hf (cod g). hsnd XZ = elem_of (Fun (comp g f) (arr_of (hfst XZ)))⦄" unfolding arr_to_hfun_def comp_def using assms by fastforce also have "... = ⦃XZ ❙∈hdomain (arr_to_hfun f) * hrange (arr_to_hfun g). hsnd XZ = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))⦄" proof fix XZ have "hfst XZ ❙∈hdomain (arr_to_hfun f) ⟹ hsnd XZ ❙∈ide_to_hf (cod g) ∧ hsnd XZ = elem_of (Fun (comp g f) (arr_of (hfst XZ))) ⟷ hsnd XZ ❙∈hrange (arr_to_hfun g) ∧ hsnd XZ = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))" proof assume XZ: "hfst XZ ❙∈hdomain (arr_to_hfun f)" have 2: "arr_of (hfst XZ) ∈ Dom f" using XZ 1 hfsetcat.arr_of_membI by auto have 3: "arr_of (happ (arr_to_hfun f) (hfst XZ)) ∈ Dom g" using assms XZ 2 by (metis (no_types, lifting) "1" happ_mapsto(1) hfsetcat.arr_of_membI arr_to_hfun_in_hexp seqE) have 4: "elem_of (Fun (comp g f) (arr_of (hfst XZ))) = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))" proof - have "elem_of (Fun (comp g f) (arr_of (hfst XZ))) = elem_of (restrict (Fun g o Fun f) (Dom f) (arr_of (hfst XZ)))" using assms Fun_comp Fun_char by simp also have "... = elem_of ((Fun g o Fun f) (arr_of (hfst XZ)))" using XZ 2 by auto also have "... = elem_of (Fun g (Fun f (arr_of (hfst XZ))))" by simp also have "... = elem_of (Fun g (restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f) (arr_of (hfst XZ))))" proof - have "Fun f = restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f)" using assms Fun_char [of f] by blast thus ?thesis by simp qed also have "... = elem_of (Fun g (arr_of (happ (arr_to_hfun f) (hfst XZ))))" using 2 by simp also have "... = elem_of (restrict (λx. arr_of (happ (arr_to_hfun g) (elem_of x))) (Dom g) (arr_of (happ (arr_to_hfun f) (hfst XZ))))" proof - have "Fun g = restrict (λx. arr_of (happ (arr_to_hfun g) (elem_of x))) (Dom g)" using assms Fun_char [of g] by blast thus ?thesis by simp qed also have "... = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))" using 3 by simp finally show ?thesis by blast qed have 5: "elem_of (Fun (comp g f) (arr_of (hfst XZ))) ❙∈hrange (arr_to_hfun g)" proof - have "happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ)) ❙∈hrange (arr_to_hfun g)" using assms 1 3 XZ hfun_arr_to_hfun happ_mapsto arr_to_hfun_in_hexp arr_to_hfun_def by (metis (no_types, lifting) seqE) thus ?thesis using XZ 4 by simp qed show "hsnd XZ ❙∈ide_to_hf (cod g) ∧ hsnd XZ = elem_of (Fun (comp g f) (arr_of (hfst XZ))) ⟹ hsnd XZ ❙∈hrange (arr_to_hfun g) ∧ hsnd XZ = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))" using XZ 4 5 by simp show "hsnd XZ ❙∈hrange (arr_to_hfun g) ∧ hsnd XZ = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ)) ⟹ hsnd XZ ❙∈ide_to_hf (cod g) ∧ hsnd XZ = elem_of (Fun (comp g f) (arr_of (hfst XZ)))" using assms XZ 1 4 by (metis (no_types, lifting) arr_to_hfun_in_hexp happ_mapsto(1) seqE) qed thus "XZ ❙∈⦃XZ ❙∈ide_to_hf (dom f) * ide_to_hf (cod g). hsnd XZ = elem_of (Fun (comp g f) (arr_of (hfst XZ)))⦄ ⟷ XZ ❙∈⦃XZ ❙∈hdomain (arr_to_hfun f) * hrange (arr_to_hfun g). hsnd XZ = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))⦄" using 1 is_hpair_def by auto qed also have "... = hcomp (arr_to_hfun g) (arr_to_hfun f)" using assms arr_to_hfun_def hcomp_def by simp finally show ?thesis by simp qed lemma hfun_to_arr_hcomp: assumes "hfun A B F" and "hfun B C G" shows "hfun_to_arr A C (hcomp G F) = comp (hfun_to_arr B C G) (hfun_to_arr A B F)" proof - have 1: "arr_to_hfun (hfun_to_arr A C (hcomp G F)) = arr_to_hfun (comp (hfun_to_arr B C G) (hfun_to_arr A B F))" proof - have "arr_to_hfun (comp (hfun_to_arr B C G) (hfun_to_arr A B F)) = hcomp (arr_to_hfun (hfun_to_arr B C G)) (arr_to_hfun (hfun_to_arr A B F))" using assms arr_to_hfun_comp hfun_to_arr_in_hom by blast also have "... = hcomp G F" using assms by (simp add: arr_to_hfun_hfun_to_arr) also have "... = arr_to_hfun (hfun_to_arr A C (hcomp G F))" proof - have "hfun A C (hcomp G F)" using assms hfun_hcomp by simp thus ?thesis by (simp add: arr_to_hfun_hfun_to_arr) qed finally show ?thesis by simp qed show ?thesis proof - have "hfun_to_arr A C (hcomp G F) ∈ hom (hf_to_ide A) (hf_to_ide C)" using assms hfun_hcomp hf_to_ide_def hfun_to_arr_in_hom by auto moreover have "comp (hfun_to_arr B C G) (hfun_to_arr A B F) ∈ hom (hf_to_ide A) (hf_to_ide C)" using assms hfun_to_arr_in_hom hf_to_ide_def by (metis (no_types, lifting) comp_in_homI mem_Collect_eq) moreover have "inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))" proof - have "ide (hf_to_ide A) ∧ ide (hf_to_ide C)" using assms hf_to_ide_mapsto by auto thus ?thesis using bij_betw_hom_hfun [of "hf_to_ide A" "hf_to_ide C"] bij_betw_imp_inj_on by auto qed ultimately show ?thesis using 1 inj_on_def [of arr_to_hfun "hom (hf_to_ide A) (hf_to_ide C)"] by simp qed qed section "Binary Products" text‹ The category of hereditarily finite sets has binary products, given by cartesian product of sets in the usual way. › definition prod where "prod a b = hf_to_ide (ide_to_hf a * ide_to_hf b)" definition pr0 where "pr0 a b = (if ide a ∧ ide b then mkArr (set (prod a b)) (set b) (λx. arr_of (hsnd (elem_of x))) else null)" definition pr1 where "pr1 a b = (if ide a ∧ ide b then mkArr (set (prod a b)) (set a) (λx. arr_of (hfst (elem_of x))) else null)" definition tuple where "tuple f g = mkArr (set (dom f)) (set (prod (cod f) (cod g))) (λx. arr_of (hpair (elem_of (Fun f x)) (elem_of (Fun g x))))" lemma ide_prod: assumes "ide a" and "ide b" shows "ide (prod a b)" using assms prod_def hf_to_ide_mapsto ide_to_hf_mapsto by auto lemma pr1_in_hom [intro]: assumes "ide a" and "ide b" shows "«pr1 a b : prod a b → a»" proof show 0: "arr (pr1 a b)" proof - have "set (prod a b) ⊆ Univ ∧ finite (set (prod a b))" using assms ide_implies_finite_set(1) set_ideD(1) ide_prod by presburger moreover have "set a ⊆ Univ ∧ finite (set a)" using assms ide_char set_ide_char by blast moreover have "(λx. arr_of (hfst (elem_of x))) ∈ set (prod a b) → set a" proof (unfold prod_def) show "(λx. arr_of (hfst (elem_of x))) ∈ set (hf_to_ide (ide_to_hf a * ide_to_hf b)) → set a" proof fix x assume x: "x ∈ set (hf_to_ide (ide_to_hf a * ide_to_hf b))" have "elem_of x ∈ hfset (ide_to_hf a * ide_to_hf b)" using assms ide_char x by (metis (no_types, lifting) prod_def elem_of_membI HF_hfset UNIV_I hmem_HF_iff ide_prod ide_to_hf_hf_to_ide) hence "hfst (elem_of x) ❙∈ide_to_hf a" by (metis HF_hfset finite_hfset hfst_conv hmem_HF_iff timesE) thus "arr_of (hfst (elem_of x)) ∈ set a" using arr_of_membI by simp qed qed ultimately show ?thesis unfolding pr1_def using assms arr_mkArr finite_imp_setp by presburger qed show "dom (pr1 a b) = prod a b" using assms 0 ide_char ide_prod dom_mkArr by (metis (no_types, lifting) mkIde_set pr1_def) show "cod (pr1 a b) = a" using assms 0 ide_char ide_prod cod_mkArr by (metis (no_types, lifting) mkIde_set pr1_def) qed lemma pr1_simps [simp]: assumes "ide a" and "ide b" shows "arr (pr1 a b)" and "dom (pr1 a b) = prod a b" and "cod (pr1 a b) = a" using assms pr1_in_hom by blast+ lemma pr0_in_hom [intro]: assumes "ide a" and "ide b" shows "«pr0 a b : prod a b → b»" proof show 0: "arr (pr0 a b)" proof - have "set (prod a b) ⊆ Univ ∧ finite (set (prod a b))" using setp_set_ide assms ide_implies_finite_set(1) ide_prod by presburger moreover have "set b ⊆ Univ ∧ finite (set b)" using assms ide_char set_ide_char by blast moreover have "(λx. arr_of (hsnd (elem_of x))) ∈ set (prod a b) → set b" proof (unfold prod_def) show "(λx. arr_of (hsnd (elem_of x))) ∈ set (hf_to_ide (ide_to_hf a * ide_to_hf b)) → set b" proof fix x assume x: "x ∈ set (hf_to_ide (ide_to_hf a * ide_to_hf b))" have "elem_of x ∈ hfset (ide_to_hf a * ide_to_hf b)" using assms ide_char x by (metis (no_types, lifting) prod_def elem_of_membI HF_hfset UNIV_I hmem_HF_iff ide_prod ide_to_hf_hf_to_ide) hence "hsnd (elem_of x) ❙∈ide_to_hf b" by (metis HF_hfset finite_hfset hsnd_conv hmem_HF_iff timesE) thus "arr_of (hsnd (elem_of x)) ∈ set b" using arr_of_membI by simp qed qed ultimately show ?thesis unfolding pr0_def using assms arr_mkArr finite_imp_setp by presburger qed show "dom (pr0 a b) = prod a b" using assms 0 ide_char ide_prod dom_mkArr by (metis (no_types, lifting) mkIde_set pr0_def) show "cod (pr0 a b) = b" using assms 0 ide_char ide_prod cod_mkArr by (metis (no_types, lifting) mkIde_set pr0_def) qed lemma pr0_simps [simp]: assumes "ide a" and "ide b" shows "arr (pr0 a b)" and "dom (pr0 a b) = prod a b" and "cod (pr0 a b) = b" using assms pr0_in_hom by blast+ lemma arr_of_tuple_elem_of_membI: assumes "span f g" and "x ∈ Dom f" shows "arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩ ∈ set (prod (cod f) (cod g))" proof - have "Fun f x ∈ set (cod f)" using assms Fun_mapsto by blast moreover have "Fun g x ∈ set (cod g)" using assms Fun_mapsto by auto ultimately have "⟨elem_of (Fun f x), elem_of (Fun g x)⟩ ❙∈ide_to_hf (cod f) * ide_to_hf (cod g)" using assms ide_cod by auto moreover have "set (prod (cod f) (cod g)) ⊆ Univ" using setp_set_ide assms(1) ide_cod ide_prod by presburger ultimately show ?thesis using prod_def arr_of_membI ide_to_hf_hf_to_ide by auto qed lemma tuple_in_hom [intro]: assumes "span f g" shows "«tuple f g : dom f → prod (cod f) (cod g)»" proof show 1: "arr (tuple f g)" proof - have "Dom f ⊆ Univ ∧ finite (Dom f)" using assms set_ideD(1) ide_dom ide_implies_finite_set(1) by presburger moreover have "set (prod (cod f) (cod g)) ⊆ Univ ∧ finite (set (prod (cod f) (cod g)))" using assms set_ideD(1) ide_cod ide_prod ide_implies_finite_set(1) by presburger moreover have "(λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩) ∈ Dom f → set (prod (cod f) (cod g))" using assms arr_of_tuple_elem_of_membI by simp ultimately show ?thesis using assms ide_prod tuple_def arr_mkArr ide_dom ide_cod by simp qed show "dom (tuple f g) = dom f" using assms 1 dom_mkArr ide_dom mkIde_set tuple_def by auto show "cod (tuple f g) = prod (cod f) (cod g)" using assms 1 cod_mkArr ide_cod mkIde_set tuple_def ide_prod by auto qed lemma tuple_simps [simp]: assumes "span f g" shows "arr (tuple f g)" and "dom (tuple f g) = dom f" and "cod (tuple f g) = prod (cod f) (cod g)" using assms tuple_in_hom by blast+ lemma Fun_pr1: assumes "ide a" and "ide b" shows "Fun (pr1 a b) = restrict (λx. arr_of (hfst (elem_of x))) (set (prod a b))" using assms pr1_def Fun_mkArr arr_char pr1_simps(1) by presburger lemma Fun_pr0: assumes "ide a" and "ide b" shows "Fun (pr0 a b) = restrict (λx. arr_of (hsnd (elem_of x))) (set (prod a b))" using assms pr0_def Fun_mkArr arr_char pr0_simps(1) by presburger lemma Fun_tuple: assumes "span f g" shows "Fun (tuple f g) = restrict (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩) (Dom f)" proof - have "arr (tuple f g)" using assms tuple_in_hom by blast thus ?thesis using assms tuple_def Fun_mkArr by simp qed lemma pr1_tuple: assumes "span f g" shows "comp (pr1 (cod f) (cod g)) (tuple f g) = f" proof (intro arr_eqI⇩_{S}⇩_{C}) have pr1: "«pr1 (cod f) (cod g) : prod (cod f) (cod g) → cod f»" using assms ide_cod by blast have tuple: "«tuple f g : dom f → prod (cod f) (cod g)»" using assms by blast show par: "par (comp (pr1 (cod f) (cod g)) (tuple f g)) f" using assms pr1_in_hom tuple_in_hom by (metis (no_types, lifting) comp_in_homI' ide_cod in_homE) show "Fun (comp (pr1 (cod f) (cod g)) (tuple f g)) = Fun f" proof - have seq: "seq (pr1 (cod f) (cod g)) (tuple f g)" using par by blast have "Fun (comp (pr1 (cod f) (cod g)) (tuple f g)) = restrict (Fun (pr1 (cod f) (cod g)) ∘ Fun (tuple f g)) (Dom (tuple f g))" using pr1 tuple seq Fun_comp by simp also have "... = restrict (Fun (mkArr (set (prod (cod f) (cod g))) (Cod f) (λx. arr_of (hfst (elem_of x)))) ∘ Fun (mkArr (Dom f) (set (prod (cod f) (cod g))) (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩))) (Dom (tuple f g))" unfolding pr1_def tuple_def using assms ide_cod by presburger also have "... = restrict (restrict (λx. arr_of (hfst (elem_of x))) (set (prod (cod f) (cod g))) o restrict (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩) (Dom f)) (Dom f)" proof - have "Fun (mkArr (set (prod (cod f) (cod g))) (Cod f) (λx. arr_of (hfst (elem_of x)))) = restrict (λx. arr_of (hfst (elem_of x))) (set (prod (cod f) (cod g)))" using assms Fun_mkArr ide_prod pr1 by (metis (no_types, lifting) arrI ide_cod pr1_def) moreover have "Fun (mkArr (Dom f) (set (prod (cod f) (cod g))) (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩)) = restrict (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩) (Dom f)" using assms Fun_mkArr ide_prod ide_cod tuple_def tuple arrI by simp ultimately show ?thesis using assms tuple_simps(2) by simp qed also have "... = restrict ((λx. arr_of (hfst (elem_of x))) o (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩)) (Dom f)" using assms tuple tuple_def arr_of_tuple_elem_of_membI by auto also have "... = restrict (Fun f) (Dom f)" proof fix x have "restrict ((λx. arr_of (hfst (elem_of x))) o (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩)) (Dom f) x = restrict (λx. arr_of (elem_of (Fun f x))) (Dom f) x" by simp also have "... = restrict (Fun f) (Dom f) x" proof (cases "x ∈ Dom f") show "x ∉ Dom f ⟹ ?thesis" by simp assume x: "x ∈ Dom f" have "Fun f x ∈ Cod f" using assms x Fun_mapsto arr_char by blast moreover have "Cod f ⊆ Univ" using setp_set_ide assms ide_cod by blast ultimately show ?thesis using assms arr_of_elem_of Fun_mapsto by auto qed finally show "restrict ((λx. arr_of (hfst (elem_of x))) ∘ (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩)) (Dom f) x = restrict (Fun f) (Dom f) x" by blast qed also have "... = Fun f" using assms par Fun_mapsto Fun_mkArr mkArr_Fun by (metis (no_types, lifting)) finally show ?thesis by blast qed qed lemma pr0_tuple: assumes "span f g" shows "comp (pr0 (cod f) (cod g)) (tuple f g) = g" proof (intro arr_eqI⇩_{S}⇩_{C}) have pr0: "«pr0 (cod f) (cod g) : prod (cod f) (cod g) → cod g»" using assms ide_cod by blast have tuple: "«tuple f g : dom f → prod (cod f) (cod g)»" using assms by blast show par: "par (comp (pr0 (cod f) (cod g)) (tuple f g)) g" using assms pr0_in_hom tuple_in_hom by (metis (no_types, lifting) comp_in_homI' ide_cod in_homE) show "Fun (comp (pr0 (cod f) (cod g)) (tuple f g)) = Fun g" proof - have seq: "seq (pr0 (cod f) (cod g)) (tuple f g)" using par by blast have "Fun (comp (pr0 (cod f) (cod g)) (tuple f g)) = restrict (Fun (pr0 (cod f) (cod g)) ∘ Fun (tuple f g)) (Dom (tuple f g))" using pr0 tuple seq Fun_comp by simp also have "... = restrict (Fun (mkArr (set (prod (cod f) (cod g))) (Cod g) (λx. arr_of (hsnd (elem_of x)))) ∘ Fun (mkArr (Dom f) (set (prod (cod f) (cod g))) (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩))) (Dom (tuple f g))" unfolding pr0_def tuple_def using assms ide_cod by presburger also have "... = restrict (restrict (λx. arr_of (hsnd (elem_of x))) (set (prod (cod f) (cod g))) o restrict (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩) (Dom g)) (Dom g)" proof - have "Fun (mkArr (set (prod (cod f) (cod g))) (Cod g) (λx. arr_of (hsnd (elem_of x)))) = restrict (λx. arr_of (hsnd (elem_of x))) (set (prod (cod f) (cod g)))" using assms Fun_mkArr ide_prod arrI by (metis (no_types, lifting) ide_cod pr0 pr0_def) moreover have "Fun (mkArr (Dom f) (set (prod (cod f) (cod g))) (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩)) = restrict (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩) (Dom f)" using assms Fun_mkArr ide_prod ide_cod tuple_def tuple arrI by simp ultimately show ?thesis using assms tuple_simps(2) by simp qed also have "... = restrict ((λx. arr_of (hsnd (elem_of x))) o (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩)) (Dom g)" using assms tuple tuple_def arr_of_tuple_elem_of_membI by auto also have "... = restrict (Fun g) (Dom g)" proof fix x have "restrict ((λx. arr_of (hsnd (elem_of x))) o (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩)) (Dom g) x = restrict (λx. arr_of (elem_of (Fun g x))) (Dom g) x" by simp also have "... = restrict (Fun g) (Dom g) x" proof (cases "x ∈ Dom g") show "x ∉ Dom g ⟹ ?thesis" by simp assume x: "x ∈ Dom g" have "Fun g x ∈ Cod g" using assms x Fun_mapsto arr_char by blast moreover have "Cod g ⊆ Univ" using assms set_ideD(1) ide_cod by blast ultimately show ?thesis using assms arr_of_elem_of Fun_mapsto by auto qed finally show "restrict ((λx. arr_of (hsnd (elem_of x))) ∘ (λx. arr_of ⟨elem_of (Fun f x), elem_of (Fun g x)⟩)) (Dom g) x = restrict (Fun g) (Dom g) x" by blast qed also have "... = Fun g" using assms par Fun_mapsto Fun_mkArr mkArr_Fun by (metis (no_types, lifting)) finally show ?thesis by blast qed qed lemma tuple_pr: assumes "ide a" and "ide b" and "«h : dom h → prod a b»" shows "tuple (comp (pr1 a b) h) (comp (pr0 a b) h) = h" proof (intro arr_eqI⇩_{S}⇩_{C}) have pr0: "«pr0 a b : prod a b → b»" using assms pr0_in_hom ide_cod by blast have pr1: "«pr1 a b : prod a b → a»" using assms pr1_in_hom ide_cod by blast have tuple: "«tuple (comp (pr1 a b) h) (comp (pr0 a b) h) : dom h → prod a b»" using assms pr0 pr1 by (metis (no_types, lifting) cod_comp dom_comp pr0_simps(3) pr1_simps(3) seqI' tuple_in_hom) show par: "par (tuple (comp (pr1 a b) h) (comp (pr0 a b) h)) h" using assms tuple by (metis (no_types, lifting) in_homE) show "Fun (tuple (comp (pr1 a b) h) (comp (pr0 a b) h)) = Fun h" proof - have 1: "Fun (comp (pr1 a b) h) = restrict (restrict (λx. arr_of (hfst (elem_of x))) (set (prod a b)) ∘ Fun h) (Dom h)" using assms pr1 Fun_comp Fun_pr1 seqI' by auto have 2: "Fun (comp (pr0 a b) h) = restrict (restrict (λx. arr_of (hsnd (elem_of x))) (set (prod a b)) ∘ Fun h) (Dom h)" using assms pr0 Fun_comp Fun_pr0 seqI' by auto have "Fun (tuple (comp (pr1 a b) h) (comp (pr0 a b) h)) = restrict (λx. arr_of ⟨elem_of (restrict (restrict (λx. arr_of (hfst (elem_of x))) (set (prod a b)) ∘ Fun h) (Dom h) x), elem_of (restrict (restrict (λx. arr_of (hsnd (elem_of x))) (set (prod a b)) ∘ Fun h) (Dom h) x)⟩) (Dom h)" proof - have "Dom (comp (pr1 a b) h) = Dom h" using assms pr1_in_hom by (metis (no_types, lifting) in_homE dom_comp seqI) moreover have "arr (mkArr (Dom (comp (pr1 a b) h)) (set (prod (cod (comp (pr1 a b) h)) (cod (comp (pr0 a b) h)))) (λx. arr_of ⟨elem_of (Fun (comp (pr1 a b) h) x), elem_of (Fun (comp (pr0 a b) h) x)⟩))" using tuple unfolding tuple_def by blast ultimately show ?thesis using 1 2 tuple tuple_def Fun_mkArr [of "Dom (comp (pr1 a b) h)" "set (prod (cod (comp (pr1 a b) h)) (cod (comp (pr0 a b) h)))" "λx. arr_of ⟨elem_of (Fun (comp (pr1 a b) h) x), elem_of (Fun (comp (pr0 a b) h) x)⟩"] by simp qed also have "... = Fun h" proof let ?f = "..." fix x show "?f x = Fun h x" proof - have "x ∉ Dom h ⟹ ?f x = Fun h x" proof - assume x: "x ∉ Dom h" have "restrict ?f (Dom h) x = undefined" using assms x restrict_apply by auto also have "... = Fun h x" proof - have "arr h" using assms by blast thus ?thesis using assms x Fun_mapsto [of h] extensional_arb [of "Fun h" "Dom h" x] by simp qed finally show ?thesis by auto qed moreover have "x ∈ Dom h ⟹ ?f x = Fun h x" proof - assume x: "x ∈ Dom h" have 1: "Fun h x ∈ set (prod a b)" proof - have "Fun h x ∈ Cod h" using assms x Fun_mapsto [of h] by blast moreover have "Cod h = set (prod a b)" using assms ide_prod by (metis (no_types, lifting) in_homE) ultimately show ?thesis by fast qed have "?f x = arr_of ⟨hfst (elem_of (Fun h x)), hsnd (elem_of (Fun h x))⟩" using x 1 by simp also have "... = arr_of (elem_of (Fun h x))" proof - have "elem_of (Fun h x) ❙∈ide_to_hf a * ide_to_hf b" using assms x 1 par by (metis (no_types, lifting) prod_def elem_of_membI UNIV_I ide_prod ide_to_hf_hf_to_ide) thus ?thesis using x is_hpair_def by auto qed also have "... = Fun h x" using 1 arr_of_elem_of assms set_ideD(1) ide_prod by blast finally show ?thesis by blast qed ultimately show ?thesis by blast qed qed finally show ?thesis by blast qed qed interpretation HF': elementary_category_with_binary_products comp pr0 pr1 proof show "⋀a b. ⟦ide a; ide b⟧ ⟹ span (pr1 a b) (pr0 a b)" using pr0_simps(1) pr0_simps(2) pr1_simps(1) pr1_simps(2) by auto show "⋀a b. ⟦ide a; ide b⟧ ⟹ cod (pr0 a b) = b" using pr0_simps(1-3) by blast show "⋀a b. ⟦ide a; ide b⟧ ⟹ cod (pr1 a b) = a" using pr1_simps(1-3) by blast show "⋀f g. span f g ⟹ ∃!l. comp (pr1 (cod f) (cod g)) l = f ∧ comp (pr0 (cod f) (cod g)) l = g" proof fix f g assume fg: "span f g" show "comp (pr1 (cod f) (cod g)) (tuple f g) = f ∧ comp (pr0 (cod f) (cod g)) (tuple f g) = g" using fg pr0_simps pr1_simps tuple_simps pr0_tuple pr1_tuple by presburger show "⋀l. ⟦comp (pr1 (cod f) (cod g)) l = f ∧ comp (pr0 (cod f) (cod g)) l = g⟧ ⟹ l = tuple f g " proof - fix l assume l: "comp (pr1 (cod f) (cod g)) l = f ∧ comp (pr0 (cod f) (cod g)) l = g" show "l = tuple f g" using fg l tuple_pr by (metis (no_types, lifting) arr_iff_in_hom ide_cod seqE pr0_simps(2)) qed qed qed text‹ For reasons of economy of locale parameters, the notion ‹prod› is a defined notion of the @{locale elementary_category_with_binary_products} locale. However, we need to be able to relate this notion to that of cartesian product of hereditarily finite sets, which we have already used to give a definition of ‹prod›. The locale assumptions for @{locale elementary_cartesian_closed_category} refer specifically to ‹HF'.prod›, even though in the end the notion itself does not depend on that choice. To be able to show that the locale assumptions of @{locale elementary_cartesian_closed_category} are satisfied, we need to use a choice of products that we can relate to the cartesian product of hereditarily finite sets. We therefore need to show that our previously defined ‹prod› coincides (on objects) with the one defined in the @{locale elementary_category_with_binary_products} locale; \emph{i.e.}~‹HF'.prod›. Note that the latter is defined for all arrows, not just identity arrows, so we need to use that for the subsequent definitions and proofs. › lemma prod_ide_eq: assumes "ide a" and "ide b" shows "prod a b = HF'.prod a b" using assms prod_def HF'.pr_simps(2) HF'.prod_def pr0_simps(2) by presburger lemma tuple_span_eq: assumes "span f g" shows "tuple f g = HF'.tuple f g" using assms tuple_def HF'.tuple_def by (metis (no_types, lifting) HF'.tuple_eqI ide_cod pr0_tuple pr1_tuple) section "Exponentials" text‹ We now turn our attention to exponentials. › definition exp where "exp b c = hf_to_ide (hexp (ide_to_hf b) (ide_to_hf c))" definition eval where "eval b c = mkArr (set (HF'.prod (exp b c) b)) (set c) (λx. arr_of (happ (hfst (elem_of x)) (hsnd (elem_of x))))" definition Λ where "Λ a b c f = mkArr (set a) (set (exp b c)) (λx. arr_of (happ (hlam (ide_to_hf a) (ide_to_hf b) (ide_to_hf c) (arr_to_hfun f)) (elem_of x)))" lemma ide_exp: assumes "ide b" and "ide c" shows "ide (exp b c)" using assms exp_def hf_to_ide_mapsto ide_to_hf_mapsto by auto lemma hfset_ide_to_hf: assumes "ide a" shows "hfset (ide_to_hf a) = elem_of ` set a" using assms ide_to_hf_def ide_implies_finite_set(1) by auto lemma eval_in_hom [intro]: assumes "ide b" and "ide c" shows "in_hom (eval b c) (HF'.prod (exp b c) b) c" proof show 1: "arr (eval b c)" proof (unfold eval_def arr_mkArr, intro conjI) show "set (HF'.prod (exp b c) b) ⊆ Univ" using HF'.ide_prod assms set_ideD(1) ide_exp by presburger show "set c ⊆ Univ" using assms set_ideD(1) by blast show "(λx. arr_of (happ (hfst (elem_of x)) (hsnd (elem_of x)))) ∈ set (HF'.prod (exp b c) b) → set c" proof fix x assume "x ∈ set (HF'.prod (exp b c) b)" hence x: "x ∈ set (prod (exp b c) b)" using assms prod_ide_eq ide_exp by auto show "arr_of (happ (hfst (elem_of x)) (hsnd (elem_of x))) ∈ set c" proof (intro arr_of_membI) show "happ (hfst (elem_of x)) (hsnd (elem_of x)) ❙∈ide_to_hf c" proof - have 1: "elem_of x ❙∈ide_to_hf (exp b c) * ide_to_hf b" proof - have "elem_of x ❙∈ide_to_hf (prod (exp b c) b)" using assms x elem_of_membI ide_prod ide_exp by simp thus ?thesis using assms x prod_def ide_to_hf_hf_to_ide by auto qed have "hfst (elem_of x) ❙∈hexp (ide_to_hf b) (ide_to_hf c)" using assms 1 x exp_def ide_to_hf_hf_to_ide by auto moreover have "hsnd (elem_of x) ❙∈ide_to_hf b" using assms 1 by auto ultimately show ?thesis using happ_mapsto [of "hfst (elem_of x)" "ide_to_hf b" "ide_to_hf c" "hsnd (elem_of x)"] by simp qed qed qed show "finite (elem_of ` set (HF'.prod (exp b c) b))" using HF'.ide_prod setp_set_ide assms ide_exp by presburger show "finite (elem_of ` set c)" using setp_set_ide assms(2) by blast qed show "dom (eval b c) = HF'.prod (exp b c) b" using assms 1 ide_char HF'.ide_prod ide_exp dom_mkArr eval_def by (metis (no_types, lifting) mkIde_set) show "cod (eval b c) = c" using assms 1 ide_char cod_mkArr eval_def by (metis (no_types, lifting) mkIde_set) qed lemma eval_simps [simp]: assumes "ide b" and "ide c" shows "arr (eval b c)" and "dom (eval b c) = HF'.prod (exp b c) b" and "cod (eval b c) = c" using assms eval_in_hom by blast+ lemma hlam_arr_to_hfun_in_hexp: assumes "ide a" and "ide b" and "ide c" and "in_hom f (prod a b) c" shows "hlam (ide_to_hf a) (ide_to_hf b) (ide_to_hf c) (arr_to_hfun f) ❙∈hexp (ide_to_hf a) (ide_to_hf (exp b c))" using assms hfun_in_hexp hfun_hlam by (metis (no_types, lifting) prod_def HCollect_iff in_homE UNIV_I arr_to_hfun_in_hexp exp_def hexp_def ide_to_hf_hf_to_ide) lemma lam_in_hom [intro]: assumes "ide a" and "ide b" and "ide c" and "in_hom f (prod a b) c" shows "in_hom (Λ a b c f) a (exp b c)" proof show 1: "arr (Λ a b c f)" proof (unfold Λ_def arr_mkArr, intro conjI) show "set a ⊆ Univ" using assms(1) set_ideD(1) by blast show "set (exp b c) ⊆ Univ" using assms(2-3) set_ideD(1) ide_exp ide_char by blast show "finite (elem_of ` set a)" using assms(1) set_ideD(1) setp_set_ide by presburger show "finite (elem_of ` set (exp b c))" using assms(2-3) set_ideD(1) setp_set_ide ide_exp by presburger show "(λx. arr_of (happ (hlam (ide_to_hf a) (ide_to_hf b) (ide_to_hf c) (arr_to_hfun f)) (elem_of x))) ∈ set a → set (exp b c)" proof fix x assume x: "x ∈ set a" show "arr_of (happ (hlam (ide_to_hf a) (ide_to_hf b) (ide_to_hf c) (arr_to_hfun f)) (elem_of x)) ∈ set (exp b c)" using assms x hlam_arr_to_hfun_in_hexp ide_to_hf_def elem_of_membI happ_mapsto arr_of_membI by meson qed qed show "dom (Λ a b c f) = a" using assms(1) 1 Λ_def ide_char dom_mkArr mkIde_set by auto show "cod (Λ a b c f) = exp b c" using assms(2-3) 1 Λ_def cod_mkArr ide_exp mkIde_set by auto qed lemma lam_simps [simp]: assumes "ide a" and "ide b" and "ide c" and "in_hom f (prod a b) c" shows "arr (Λ a b c f)" and "dom (Λ a b c f) = a" and "cod (Λ a b c f) = exp b c" using assms lam_in_hom by blast+ lemma Fun_lam: assumes "ide a" and "ide b" and "ide c" and "in_hom f (prod a b) c" shows "Fun (Λ a b c f) = restrict (λx. arr_of (happ (hlam (ide_to_hf a) (ide_to_hf b) (ide_to_hf c) (arr_to_hfun f)) (elem_of x))) (set a)" using assms arr_char lam_simps(1) Λ_def Fun_mkArr by simp lemma Fun_eval: assumes "ide b" and "ide c" shows "Fun (eval b c) = restrict (λx. arr_of (happ (hfst (elem_of x)) (hsnd (elem_of x)))) (set (HF'.prod (exp b c) b))" using assms arr_char eval_simps(1) eval_def Fun_mkArr by force lemma Fun_prod: assumes "arr f" and "arr g" and "x ∈ set (prod (dom f) (dom g))" shows "Fun (HF'.prod f g) x = arr_of ⟨elem_of (Fun f (arr_of (hfst (elem_of x)))), elem_of (Fun g (arr_of (hsnd (elem_of x))))⟩" proof - have 1: "span (comp f (pr1 (dom f) (dom g))) (comp g (pr0 (dom f) (dom g)))" using assms by (metis (no_types, lifting) HF'.prod_def HF'.prod_simps(1) HF'.tuple_ext not_arr_null) have 2: "Dom (comp f (pr1 (dom f) (dom g))) = set (prod (dom f) (dom g))" using assms by (metis (mono_tags, lifting) 1 dom_comp ide_dom pr0_simps(2)) have 3: "Dom (comp g (pr0 (dom f) (dom g))) = set (prod (dom f) (dom g))" using assms 1 2 by force have "Fun (HF'.prod f g) x = Fun (HF'.tuple (comp f (pr1 (dom f) (dom g))) (comp g (pr0 (dom f) (dom g)))) x" using assms(3) HF'.prod_def by simp also have "... = restrict (λx. arr_of ⟨elem_of (Fun (comp f (pr1 (dom f) (dom g))