1+ (*
2+ This file is a part of IsarMathLib -
3+ a library of formalized mathematics for Isabelle/Isar.
4+
5+ Copyright (C) 2008-2025 Slawomir Kolodynski
6+
7+ This program is free software; Redistribution and use in source and binary forms,
8+ with or without modification, are permitted provided that the following conditions are met:
9+
10+ 1. Redistributions of source code must retain the above copyright notice,
11+ this list of conditions and the following disclaimer.
12+ 2. Redistributions in binary form must reproduce the above copyright notice,
13+ this list of conditions and the following disclaimer in the documentation and/or
14+ other materials provided with the distribution.
15+ 3. The name of the author may not be used to endorse or promote products
16+ derived from this software without specific prior written permission.
17+
18+ THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED
19+ WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
20+ MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
21+ IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
22+ SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
23+ PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
24+ OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
25+ WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
26+ OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
27+ EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28+
29+ *)
30+
31+ section \<open>Finite choice and order relations\<close>
32+
33+ theory FinOrd_ZF_1 imports FinOrd_ZF Cardinal_ZF
34+
35+ begin
36+
37+ text \<open>In this theory we continue the subject of finite sets and order relation
38+ from \<open>FinOrd_ZF\<close> with some consequences of finite choice for down - directed sets. \<close>
39+
40+ subsection \<open>Finte choice and preorders\<close>
41+
42+ text \<open>In the \<open>Order_ZF\<close> theory we define what it means that a relation $r $ down - directs a set $X $:
43+ each two elements of $X $ have a common lower bound in $X $. If the relation is a preorder
44+ ( i.e. is reflexive and transitive ) and it down - directs $X $ we say that $X $ is a down - directed
45+ set ( by the relation $r $) . \<close>
46+
47+ text \<open>The next lemma states that each finite subset of a down-directed set
48+ has a lower bound in $X$.\<close>
49+
50+ lemma fin_dir_set_bounded :
51+ assumes "IsDownDirectedSet(X,r)" and "B\<in>FinPow(X)"
52+ shows "\<exists>x\<in>X.\<forall>t\<in>B. \<langle>x,t\<rangle>\<in>r"
53+ proof -
54+ from assms ( 1 ) have "\<exists>x\<in>X.\<forall>t\<in>\<emptyset>. \<langle>x,t\<rangle>\<in>r"
55+ unfolding IsDownDirectedSet_def DownDirects_def by auto
56+ moreover have
57+ "\<forall>A\<in>FinPow(X). (\<exists>x\<in>X.\<forall>t\<in>A. \<langle>x,t\<rangle>\<in>r)\<longrightarrow>(\<forall>a\<in>X. \<exists>m\<in>X.\<forall>t\<in>A\<union>{a}. \<langle>m,t\<rangle>\<in>r)"
58+ proof -
59+ { fix A assume "A\<in>FinPow(X)" and I : "\<exists>x\<in>X.\<forall>t\<in>A. \<langle>x,t\<rangle>\<in>r"
60+ { fix a assume "a\<in>X"
61+ from I obtain x where "x\<in>X" and II : "\<forall>t\<in>A. \<langle>x,t\<rangle>\<in>r" by auto
62+ from assms ( 1 ) \<open>a\<in>X\<close> \<open>x\<in>X\<close> obtain m where
63+ "m\<in>X" "\<langle>m,a\<rangle>\<in>r" "\<langle>m,x\<rangle>\<in>r"
64+ unfolding IsDownDirectedSet_def DownDirects_def by auto
65+ with assms ( 1 ) II have "\<exists>m\<in>X.\<forall>t\<in>A\<union>{a}. \<langle>m,t\<rangle>\<in>r"
66+ unfolding IsDownDirectedSet_def IsPreorder_def trans_def
67+ by blast
68+ } hence "\<forall>a\<in>X. \<exists>x\<in>X.\<forall>t\<in>A\<union>{a}. \<langle>x,t\<rangle>\<in>r" by blast
69+ } thus ?thesis by simp
70+ qed
71+ moreover note assms ( 2 )
72+ ultimately show ?thesis by ( rule FinPow_induct )
73+ qed
74+
75+ text \<open>Suppose $Y$ is a set down-directed by a (preorder) relation $r$
76+ and $f,g$ are funtions defined on two finite subsets $A,B$, resp., of $X$, valued in Y
77+ (i.e.$f:A\rightarrow Y$, $f:B\rightarrow Y$ and $A,B$ are finite subsets of $X$).
78+ Then there exist a function $h:A\cup B\rightarrow Y$ that is a lower bound for
79+ $f$ on $A$ and for $g$ on $B$.\<close>
80+
81+ lemma two_fun_low_bound :
82+ assumes "IsDownDirectedSet(Y,r)" "A\<in>FinPow(X)" "B\<in>FinPow(X)" "f:A\<rightarrow>Y" "g:B\<rightarrow>Y"
83+ shows "\<exists>h\<in>A\<union>B\<rightarrow>Y. (\<forall>x\<in>A. \<langle>h`(x),f`(x)\<rangle>\<in>r) \<and> (\<forall>x\<in>B. \<langle>h`(x),g`(x)\<rangle>\<in>r)"
84+ proof -
85+ from assms ( 2 , 3 ) have "Finite(A\<union>B)" using union_finpow
86+ unfolding FinPow_def by simp
87+ { fix x assume "x\<in>A\<union>B"
88+ from assms ( 4 , 5 ) have "f``{x}\<union>g``{x} \<in> FinPow(Y)"
89+ using image_singleton_fin union_finpow by simp
90+ with assms ( 1 ) have "\<exists>y\<in>Y.\<forall>t\<in>(f``{x}\<union>g``{x}). \<langle>y,t\<rangle>\<in>r"
91+ using fin_dir_set_bounded by simp
92+ } hence "\<forall>x\<in>A\<union>B. \<exists>y\<in>Y.\<forall>t\<in>(f``{x}\<union>g``{x}). \<langle>y,t\<rangle>\<in>r" by auto
93+ with \<open>Finite(A\<union>B)\<close> have
94+ "\<exists>h\<in>A\<union>B\<rightarrow>Y. \<forall>x\<in>A\<union>B. \<forall>t\<in>(f``{x}\<union>g``{x}). \<langle>h`(x),t\<rangle>\<in>r"
95+ by ( rule finite_choice_fun )
96+ then obtain h where "h\<in>A\<union>B\<rightarrow>Y" and
97+ "\<forall>x\<in>A\<union>B. \<forall>t\<in>(f``{x}\<union>g``{x}). \<langle>h`(x),t\<rangle>\<in>r"
98+ by auto
99+ with assms ( 4 , 5 ) have
100+ "\<forall>x\<in>A. \<langle>h`(x),f`(x)\<rangle>\<in>r" and "\<forall>x\<in>B. \<langle>h`(x),g`(x)\<rangle>\<in>r"
101+ using func_imagedef by simp_all
102+ with \<open>h\<in>A\<union>B\<rightarrow>Y\<close> show ?thesis by auto
103+ qed
104+
105+ end
0 commit comments