1.1 --- a/src/HOL/Cardinals/Order_Relation_More_Base.thy Thu Dec 05 17:52:12 2013 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,286 +0,0 @@
1.4 -(* Title: HOL/Cardinals/Order_Relation_More_Base.thy
1.5 - Author: Andrei Popescu, TU Muenchen
1.6 - Copyright 2012
1.7 -
1.8 -Basics on order-like relations (base).
1.9 -*)
1.10 -
1.11 -header {* Basics on Order-Like Relations (Base) *}
1.12 -
1.13 -theory Order_Relation_More_Base
1.14 -imports "~~/src/HOL/Library/Order_Relation"
1.15 -begin
1.16 -
1.17 -
1.18 -text{* In this section, we develop basic concepts and results pertaining
1.19 -to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
1.20 -total relations. The development is placed on top of the definitions
1.21 -from the theory @{text "Order_Relation"}. We also
1.22 -further define upper and lower bounds operators. *}
1.23 -
1.24 -
1.25 -locale rel = fixes r :: "'a rel"
1.26 -
1.27 -text{* The following context encompasses all this section, except
1.28 -for its last subsection. In other words, for the rest of this section except its last
1.29 -subsection, we consider a fixed relation @{text "r"}. *}
1.30 -
1.31 -context rel
1.32 -begin
1.33 -
1.34 -
1.35 -subsection {* Auxiliaries *}
1.36 -
1.37 -
1.38 -lemma refl_on_domain:
1.39 -"\<lbrakk>refl_on A r; (a,b) : r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
1.40 -by(auto simp add: refl_on_def)
1.41 -
1.42 -
1.43 -corollary well_order_on_domain:
1.44 -"\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
1.45 -by(simp add: refl_on_domain order_on_defs)
1.46 -
1.47 -
1.48 -lemma well_order_on_Field:
1.49 -"well_order_on A r \<Longrightarrow> A = Field r"
1.50 -by(auto simp add: refl_on_def Field_def order_on_defs)
1.51 -
1.52 -
1.53 -lemma well_order_on_Well_order:
1.54 -"well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
1.55 -using well_order_on_Field by simp
1.56 -
1.57 -
1.58 -lemma Total_subset_Id:
1.59 -assumes TOT: "Total r" and SUB: "r \<le> Id"
1.60 -shows "r = {} \<or> (\<exists>a. r = {(a,a)})"
1.61 -proof-
1.62 - {assume "r \<noteq> {}"
1.63 - then obtain a b where 1: "(a,b) \<in> r" by fast
1.64 - hence "a = b" using SUB by blast
1.65 - hence 2: "(a,a) \<in> r" using 1 by simp
1.66 - {fix c d assume "(c,d) \<in> r"
1.67 - hence "{a,c,d} \<le> Field r" using 1 unfolding Field_def by blast
1.68 - hence "((a,c) \<in> r \<or> (c,a) \<in> r \<or> a = c) \<and>
1.69 - ((a,d) \<in> r \<or> (d,a) \<in> r \<or> a = d)"
1.70 - using TOT unfolding total_on_def by blast
1.71 - hence "a = c \<and> a = d" using SUB by blast
1.72 - }
1.73 - hence "r \<le> {(a,a)}" by auto
1.74 - with 2 have "\<exists>a. r = {(a,a)}" by blast
1.75 - }
1.76 - thus ?thesis by blast
1.77 -qed
1.78 -
1.79 -
1.80 -lemma Linear_order_in_diff_Id:
1.81 -assumes LI: "Linear_order r" and
1.82 - IN1: "a \<in> Field r" and IN2: "b \<in> Field r"
1.83 -shows "((a,b) \<in> r) = ((b,a) \<notin> r - Id)"
1.84 -using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force
1.85 -
1.86 -
1.87 -subsection {* The upper and lower bounds operators *}
1.88 -
1.89 -
1.90 -text{* Here we define upper (``above") and lower (``below") bounds operators.
1.91 -We think of @{text "r"} as a {\em non-strict} relation. The suffix ``S"
1.92 -at the names of some operators indicates that the bounds are strict -- e.g.,
1.93 -@{text "underS a"} is the set of all strict lower bounds of @{text "a"} (w.r.t. @{text "r"}).
1.94 -Capitalization of the first letter in the name reminds that the operator acts on sets, rather
1.95 -than on individual elements. *}
1.96 -
1.97 -definition under::"'a \<Rightarrow> 'a set"
1.98 -where "under a \<equiv> {b. (b,a) \<in> r}"
1.99 -
1.100 -definition underS::"'a \<Rightarrow> 'a set"
1.101 -where "underS a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
1.102 -
1.103 -definition Under::"'a set \<Rightarrow> 'a set"
1.104 -where "Under A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
1.105 -
1.106 -definition UnderS::"'a set \<Rightarrow> 'a set"
1.107 -where "UnderS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
1.108 -
1.109 -definition above::"'a \<Rightarrow> 'a set"
1.110 -where "above a \<equiv> {b. (a,b) \<in> r}"
1.111 -
1.112 -definition aboveS::"'a \<Rightarrow> 'a set"
1.113 -where "aboveS a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
1.114 -
1.115 -definition Above::"'a set \<Rightarrow> 'a set"
1.116 -where "Above A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
1.117 -
1.118 -definition AboveS::"'a set \<Rightarrow> 'a set"
1.119 -where "AboveS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
1.120 -(* *)
1.121 -
1.122 -text{* Note: In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
1.123 - we bounded comprehension by @{text "Field r"} in order to properly cover
1.124 - the case of @{text "A"} being empty. *}
1.125 -
1.126 -
1.127 -lemma UnderS_subset_Under: "UnderS A \<le> Under A"
1.128 -by(auto simp add: UnderS_def Under_def)
1.129 -
1.130 -
1.131 -lemma underS_subset_under: "underS a \<le> under a"
1.132 -by(auto simp add: underS_def under_def)
1.133 -
1.134 -
1.135 -lemma underS_notIn: "a \<notin> underS a"
1.136 -by(simp add: underS_def)
1.137 -
1.138 -
1.139 -lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under a"
1.140 -by(simp add: refl_on_def under_def)
1.141 -
1.142 -
1.143 -lemma AboveS_disjoint: "A Int (AboveS A) = {}"
1.144 -by(auto simp add: AboveS_def)
1.145 -
1.146 -
1.147 -lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS (underS a)"
1.148 -by(auto simp add: AboveS_def underS_def)
1.149 -
1.150 -
1.151 -lemma Refl_under_underS:
1.152 -assumes "Refl r" "a \<in> Field r"
1.153 -shows "under a = underS a \<union> {a}"
1.154 -unfolding under_def underS_def
1.155 -using assms refl_on_def[of _ r] by fastforce
1.156 -
1.157 -
1.158 -lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS a = {}"
1.159 -by (auto simp: Field_def underS_def)
1.160 -
1.161 -
1.162 -lemma under_Field: "under a \<le> Field r"
1.163 -by(unfold under_def Field_def, auto)
1.164 -
1.165 -
1.166 -lemma underS_Field: "underS a \<le> Field r"
1.167 -by(unfold underS_def Field_def, auto)
1.168 -
1.169 -
1.170 -lemma underS_Field2:
1.171 -"a \<in> Field r \<Longrightarrow> underS a < Field r"
1.172 -using assms underS_notIn underS_Field by blast
1.173 -
1.174 -
1.175 -lemma underS_Field3:
1.176 -"Field r \<noteq> {} \<Longrightarrow> underS a < Field r"
1.177 -by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)
1.178 -
1.179 -
1.180 -lemma Under_Field: "Under A \<le> Field r"
1.181 -by(unfold Under_def Field_def, auto)
1.182 -
1.183 -
1.184 -lemma UnderS_Field: "UnderS A \<le> Field r"
1.185 -by(unfold UnderS_def Field_def, auto)
1.186 -
1.187 -
1.188 -lemma AboveS_Field: "AboveS A \<le> Field r"
1.189 -by(unfold AboveS_def Field_def, auto)
1.190 -
1.191 -
1.192 -lemma under_incr:
1.193 -assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
1.194 -shows "under a \<le> under b"
1.195 -proof(unfold under_def, auto)
1.196 - fix x assume "(x,a) \<in> r"
1.197 - with REL TRANS trans_def[of r]
1.198 - show "(x,b) \<in> r" by blast
1.199 -qed
1.200 -
1.201 -
1.202 -lemma underS_incr:
1.203 -assumes TRANS: "trans r" and ANTISYM: "antisym r" and
1.204 - REL: "(a,b) \<in> r"
1.205 -shows "underS a \<le> underS b"
1.206 -proof(unfold underS_def, auto)
1.207 - assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
1.208 - with ANTISYM antisym_def[of r] REL
1.209 - show False by blast
1.210 -next
1.211 - fix x assume "x \<noteq> a" "(x,a) \<in> r"
1.212 - with REL TRANS trans_def[of r]
1.213 - show "(x,b) \<in> r" by blast
1.214 -qed
1.215 -
1.216 -
1.217 -lemma underS_incl_iff:
1.218 -assumes LO: "Linear_order r" and
1.219 - INa: "a \<in> Field r" and INb: "b \<in> Field r"
1.220 -shows "(underS a \<le> underS b) = ((a,b) \<in> r)"
1.221 -proof
1.222 - assume "(a,b) \<in> r"
1.223 - thus "underS a \<le> underS b" using LO
1.224 - by (simp add: order_on_defs underS_incr)
1.225 -next
1.226 - assume *: "underS a \<le> underS b"
1.227 - {assume "a = b"
1.228 - hence "(a,b) \<in> r" using assms
1.229 - by (simp add: order_on_defs refl_on_def)
1.230 - }
1.231 - moreover
1.232 - {assume "a \<noteq> b \<and> (b,a) \<in> r"
1.233 - hence "b \<in> underS a" unfolding underS_def by blast
1.234 - hence "b \<in> underS b" using * by blast
1.235 - hence False by (simp add: underS_notIn)
1.236 - }
1.237 - ultimately
1.238 - show "(a,b) \<in> r" using assms
1.239 - order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
1.240 -qed
1.241 -
1.242 -
1.243 -lemma under_Under_trans:
1.244 -assumes TRANS: "trans r" and
1.245 - IN1: "a \<in> under b" and IN2: "b \<in> Under C"
1.246 -shows "a \<in> Under C"
1.247 -proof-
1.248 - have "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)"
1.249 - using IN1 IN2 under_def Under_def by blast
1.250 - hence "\<forall>c \<in> C. (a,c) \<in> r"
1.251 - using TRANS trans_def[of r] by blast
1.252 - moreover
1.253 - have "a \<in> Field r" using IN1 unfolding Field_def under_def by blast
1.254 - ultimately
1.255 - show ?thesis unfolding Under_def by blast
1.256 -qed
1.257 -
1.258 -
1.259 -lemma under_UnderS_trans:
1.260 -assumes TRANS: "trans r" and ANTISYM: "antisym r" and
1.261 - IN1: "a \<in> under b" and IN2: "b \<in> UnderS C"
1.262 -shows "a \<in> UnderS C"
1.263 -proof-
1.264 - from IN2 have "b \<in> Under C"
1.265 - using UnderS_subset_Under[of C] by blast
1.266 - with assms under_Under_trans
1.267 - have "a \<in> Under C" by blast
1.268 - (* *)
1.269 - moreover
1.270 - have "a \<notin> C"
1.271 - proof
1.272 - assume *: "a \<in> C"
1.273 - have 1: "(a,b) \<in> r"
1.274 - using IN1 under_def[of b] by auto
1.275 - have "\<forall>c \<in> C. b \<noteq> c \<and> (b,c) \<in> r"
1.276 - using IN2 UnderS_def[of C] by blast
1.277 - with * have "b \<noteq> a \<and> (b,a) \<in> r" by blast
1.278 - with 1 ANTISYM antisym_def[of r]
1.279 - show False by blast
1.280 - qed
1.281 - (* *)
1.282 - ultimately
1.283 - show ?thesis unfolding UnderS_def Under_def by fast
1.284 -qed
1.285 -
1.286 -
1.287 -end (* context rel *)
1.288 -
1.289 -end