From ba1a7cc8ac745855566a6682fc300f7c0c70cc5f Mon Sep 17 00:00:00 2001 From: SKolodynski Date: Sun, 16 Feb 2025 20:31:52 +0100 Subject: [PATCH] another form of finite choice --- IsarMathLib/Cardinal_ZF.thy | 210 +++++++++++++++++++++--------------- IsarMathLib/Finite_ZF.thy | 5 + IsarMathLib/func1.thy | 2 +- 3 files changed, 127 insertions(+), 90 deletions(-) diff --git a/IsarMathLib/Cardinal_ZF.thy b/IsarMathLib/Cardinal_ZF.thy index af5e1a8..2972665 100644 --- a/IsarMathLib/Cardinal_ZF.thy +++ b/IsarMathLib/Cardinal_ZF.thy @@ -28,7 +28,7 @@ EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section \Cardinal numbers\ -theory Cardinal_ZF imports ZF.CardinalArith func1 +theory Cardinal_ZF imports ZF.CardinalArith Finite_ZF func1 begin @@ -408,6 +408,105 @@ definition AxiomCardinalChoiceGen ("{the axiom of}_{choice holds}") where "{the axiom of} Q {choice holds} \ Card(Q) \ (\ M N. (M \Q \ (\t\M. N`t\0)) \ (\f. f:Pi(M,\t. N`t) \ (\t\M. f`t\N`t)))" + +text\The axiom of choice holds if and only if the \AxiomCardinalChoice\ + holds for every couple of a cardinal \Q\ and a set \K\.\ + +lemma choice_subset_imp_choice: + shows "{the axiom of} Q {choice holds} \ (\ K. {the axiom of} Q {choice holds for subsets}K)" + unfolding AxiomCardinalChoice_def AxiomCardinalChoiceGen_def by blast + +text\A choice axiom for greater cardinality implies one for +smaller cardinality\ + +lemma greater_choice_imp_smaller_choice: + assumes "Q\Q1" "Card(Q)" + shows "{the axiom of} Q1 {choice holds} \ ({the axiom of} Q {choice holds})" using assms + AxiomCardinalChoiceGen_def lepoll_trans by auto + +text\If we have a surjective function from a set which is injective to a set + of ordinals, then we can find an injection which goes the other way.\ + +lemma surj_fun_inv: + assumes "f \ surj(A,B)" "A\Q" "Ord(Q)" + shows "B\A" +proof- + let ?g = "{\m,\ j. j\A \ f`(j)=m\. m\B}" + have "?g:B\range(?g)" using lam_is_fun_range by simp + then have fun: "?g:B\?g``(B)" using range_image_domain by simp + from assms(2,3) have OA: "\j\A. Ord(j)" using lt_def Ord_in_Ord by auto + { + fix x + assume "x\?g``(B)" + then have "x\range(?g)" and "\y\B. \y,x\\?g" by auto + then obtain y where T: "x=(\ j. j\A\ f`(j)=y)" and "y\B" by auto + with assms(1) OA obtain z where P: "z\A \ f`(z)=y" "Ord(z)" unfolding surj_def + by auto + with T have "x\A \ f`(x)=y" using LeastI by simp + hence "x\A" by simp + } + then have "?g``(B) \ A" by auto + with fun have fun2: "?g:B\A" using fun_weaken_type by auto + then have "?g\inj(B,A)" + proof - + { + fix w x + assume AS: "?g`w=?g`x" "w\B" "x\B" + from assms(1) OA AS(2,3) obtain wz xz where + P1: "wz\A \ f`(wz)=w" "Ord(wz)" and P2: "xz\A \ f`(xz)=x" "Ord(xz)" + unfolding surj_def by blast + from P1 have "(\ j. j\A\ f`j=w) \ A \ f`(\ j. j\A\ f`j=w)=w" + by (rule LeastI) + moreover from P2 have "(\ j. j\A\ f`j=x) \ A \ f`(\ j. j\A\ f`j=x)=x" + by (rule LeastI) + ultimately have R: "f`(\ j. j\A\ f`j=w)=w" "f`(\ j. j\A\ f`j=x)=x" + by auto + from AS have "(\ j. j\A\ f`(j)=w)=(\ j. j\A \ f`(j)=x)" + using apply_equality fun2 by auto + hence "f`(\ j. j\A \ f`(j)=w) = f`(\ j. j\A \ f`(j)=x)" by auto + with R(1) have "w = f`(\ j. j\A\ f`j=x)" by auto + with R(2) have "w=x" by auto + } + hence "\w\B. \x\B. ?g`(w) = ?g`(x) \ w = x" + by auto + with fun2 show "?g\inj(B,A)" unfolding inj_def by auto + qed + then show ?thesis unfolding lepoll_def by auto +qed + +text\The difference with the previous result is that in this one +\A\ is not a subset of an ordinal, it is only injective +with one.\ + +theorem surj_fun_inv_2: + assumes "f:surj(A,B)" "A\Q" "Ord(Q)" + shows "B\A" +proof- + from assms(2) obtain h where h_def: "h\inj(A,Q)" using lepoll_def by auto + then have bij: "h\bij(A,range(h))" using inj_bij_range by auto + then obtain h1 where "h1\bij(range(h),A)" using bij_converse_bij by auto + then have "h1 \ surj(range(h),A)" using bij_def by auto + with assms(1) have "(f O h1)\surj(range(h),B)" using comp_surj by auto + moreover + { + fix x + assume p: "x\range(h)" + from bij have "h\surj(A,range(h))" using bij_def by auto + with p obtain q where "q\A" and "h`(q)=x" using surj_def by auto + then have "x\Q" using h_def inj_def by auto + } + then have "range(h)\Q" by auto + ultimately have "B\range(h)" using surj_fun_inv assms(3) by auto + moreover have "range(h)\A" using bij eqpoll_def eqpoll_sym by blast + ultimately show "B\A" using lepoll_eq_trans by auto +qed + +subsection\Finite choice\ + +text\In ZF every finite collection of non-empty sets has a choice function, i.e. a function that + selects one element from each set of the collection. In this section we prove various forms of + that claim.\ + text\The axiom of finite choice always holds.\ theorem finite_choice: @@ -497,97 +596,30 @@ proof - ultimately show ?thesis by (rule nat_induct) qed -text\The axiom of choice holds if and only if the \AxiomCardinalChoice\ -holds for every couple of a cardinal \Q\ and a set \K\.\ - -lemma choice_subset_imp_choice: - shows "{the axiom of} Q {choice holds} \ (\ K. {the axiom of} Q {choice holds for subsets}K)" - unfolding AxiomCardinalChoice_def AxiomCardinalChoiceGen_def by blast - -text\A choice axiom for greater cardinality implies one for -smaller cardinality\ +text\The choice functions of a collection $\mathcal{A}$ are functions $f$ defined on + $\mathcal{A}$ and valued in $\bigcup \mathcal{A}$ such that $f(A)\in A$ + for every $A\in \mathcal{A}$.\ -lemma greater_choice_imp_smaller_choice: - assumes "Q\Q1" "Card(Q)" - shows "{the axiom of} Q1 {choice holds} \ ({the axiom of} Q {choice holds})" using assms - AxiomCardinalChoiceGen_def lepoll_trans by auto - -text\If we have a surjective function from a set which is injective to a set - of ordinals, then we can find an injection which goes the other way.\ - -lemma surj_fun_inv: - assumes "f \ surj(A,B)" "A\Q" "Ord(Q)" - shows "B\A" -proof- - let ?g = "{\m,\ j. j\A \ f`(j)=m\. m\B}" - have "?g:B\range(?g)" using lam_is_fun_range by simp - then have fun: "?g:B\?g``(B)" using range_image_domain by simp - from assms(2,3) have OA: "\j\A. Ord(j)" using lt_def Ord_in_Ord by auto - { - fix x - assume "x\?g``(B)" - then have "x\range(?g)" and "\y\B. \y,x\\?g" by auto - then obtain y where T: "x=(\ j. j\A\ f`(j)=y)" and "y\B" by auto - with assms(1) OA obtain z where P: "z\A \ f`(z)=y" "Ord(z)" unfolding surj_def - by auto - with T have "x\A \ f`(x)=y" using LeastI by simp - hence "x\A" by simp - } - then have "?g``(B) \ A" by auto - with fun have fun2: "?g:B\A" using fun_weaken_type by auto - then have "?g\inj(B,A)" - proof - - { - fix w x - assume AS: "?g`w=?g`x" "w\B" "x\B" - from assms(1) OA AS(2,3) obtain wz xz where - P1: "wz\A \ f`(wz)=w" "Ord(wz)" and P2: "xz\A \ f`(xz)=x" "Ord(xz)" - unfolding surj_def by blast - from P1 have "(\ j. j\A\ f`j=w) \ A \ f`(\ j. j\A\ f`j=w)=w" - by (rule LeastI) - moreover from P2 have "(\ j. j\A\ f`j=x) \ A \ f`(\ j. j\A\ f`j=x)=x" - by (rule LeastI) - ultimately have R: "f`(\ j. j\A\ f`j=w)=w" "f`(\ j. j\A\ f`j=x)=x" - by auto - from AS have "(\ j. j\A\ f`(j)=w)=(\ j. j\A \ f`(j)=x)" - using apply_equality fun2 by auto - hence "f`(\ j. j\A \ f`(j)=w) = f`(\ j. j\A \ f`(j)=x)" by auto - with R(1) have "w = f`(\ j. j\A\ f`j=x)" by auto - with R(2) have "w=x" by auto - } - hence "\w\B. \x\B. ?g`(w) = ?g`(x) \ w = x" - by auto - with fun2 show "?g\inj(B,A)" unfolding inj_def by auto - qed - then show ?thesis unfolding lepoll_def by auto -qed +definition + "ChoiceFunctions(\) \ {f\\\\\. \A\\. f`(A)\A}" -text\The difference with the previous result is that in this one -\A\ is not a subset of an ordinal, it is only injective -with one.\ +text\For finite collections of non-empty sets the set of choice functions is non-empty.\ -theorem surj_fun_inv_2: - assumes "f:surj(A,B)" "A\Q" "Ord(Q)" - shows "B\A" -proof- - from assms(2) obtain h where h_def: "h\inj(A,Q)" using lepoll_def by auto - then have bij: "h\bij(A,range(h))" using inj_bij_range by auto - then obtain h1 where "h1\bij(range(h),A)" using bij_converse_bij by auto - then have "h1 \ surj(range(h),A)" using bij_def by auto - with assms(1) have "(f O h1)\surj(range(h),B)" using comp_surj by auto - moreover - { - fix x - assume p: "x\range(h)" - from bij have "h\surj(A,range(h))" using bij_def by auto - with p obtain q where "q\A" and "h`(q)=x" using surj_def by auto - then have "x\Q" using h_def inj_def by auto - } - then have "range(h)\Q" by auto - ultimately have "B\range(h)" using surj_fun_inv assms(3) by auto - moreover have "range(h)\A" using bij eqpoll_def eqpoll_sym by blast - ultimately show "B\A" using lepoll_eq_trans by auto +theorem finite_choice1: assumes "Finite(\)" and "\A\\. A\\" + shows "ChoiceFunctions(\) \ \" +proof - + let ?N = "id(\)" + let ?\ = "(\t. ?N`(t))" + from assms(1) obtain n where "n\nat" and "\\n" + unfolding Finite_def by auto + from assms(2) \\\n\ have "\\n" and "\A\\. ?N`(A)\\" + using eqpoll_imp_lepoll by simp_all + with \n\nat\ obtain f where "f\Pi(\,?\)" + using finite_choice unfolding AxiomCardinalChoiceGen_def by blast + have "Pi(\,?\) = {f\\\(\A\\. ?\(A)). \A\\. f`(A)\?\(A)}" + by (rule pi_fun_space) + with \f\Pi(\,?\)\ show ?thesis + unfolding ChoiceFunctions_def by auto qed - end diff --git a/IsarMathLib/Finite_ZF.thy b/IsarMathLib/Finite_ZF.thy index 3120ca4..f767ff3 100644 --- a/IsarMathLib/Finite_ZF.thy +++ b/IsarMathLib/Finite_ZF.thy @@ -64,6 +64,11 @@ lemma card_fin_is_nat: assumes "A \ FinPow(X)" using assms FinPow_def Finite_def cardinal_cong nat_into_Card Card_cardinal_eq by auto +text\The cardinality of a finite set is a natural number.\ + +lemma card_fin_is_nat1: assumes "Finite(A)" shows "|A| \ nat" + using assms card_fin_is_nat(1) unfolding FinPow_def by auto + text\A reformulation of \card_fin_is_nat\: for a finit set $A$ there is a bijection between $|A|$ and $A$.\ diff --git a/IsarMathLib/func1.thy b/IsarMathLib/func1.thy index 62d8194..d35f7dc 100755 --- a/IsarMathLib/func1.thy +++ b/IsarMathLib/func1.thy @@ -955,7 +955,7 @@ qed subsection\Dependent function space\ text\The standard Isabelle/ZF \ZF_Base\ theory defines a general notion of - a dependent function space $\text{Pi}(X,N)$, where $X$ wher $X$ is any set and + a dependent function space \Pi(X,N)\, where $X$ is any set and $N$ is a collection of sets indexed by $X$. We rarely use that notion in IsarMathLib. The facts shown in this section provide information on how to interpret the dependent function space notion in terms of a regular space of functions defined on $X$