--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Cardinals/Order_Relation_More_FP.thy Mon Nov 18 18:04:45 2013 +0100
@@ -0,0 +1,230 @@
+(* Title: HOL/Cardinals/Order_Relation_More_FP.thy
+ Author: Andrei Popescu, TU Muenchen
+ Copyright 2012
+
+Basics on order-like relations (FP).
+*)
+
+header {* Basics on Order-Like Relations (FP) *}
+
+theory Order_Relation_More_FP
+imports "~~/src/HOL/Library/Order_Relation"
+begin
+
+
+text{* In this section, we develop basic concepts and results pertaining
+to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
+total relations. The development is placed on top of the definitions
+from the theory @{text "Order_Relation"}. We also
+further define upper and lower bounds operators. *}
+
+
+locale rel = fixes r :: "'a rel"
+
+text{* The following context encompasses all this section, except
+for its last subsection. In other words, for the rest of this section except its last
+subsection, we consider a fixed relation @{text "r"}. *}
+
+context rel
+begin
+
+
+subsection {* Auxiliaries *}
+
+
+lemma refl_on_domain:
+"\<lbrakk>refl_on A r; (a,b) : r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
+by(auto simp add: refl_on_def)
+
+
+corollary well_order_on_domain:
+"\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
+by(simp add: refl_on_domain order_on_defs)
+
+
+lemma well_order_on_Field:
+"well_order_on A r \<Longrightarrow> A = Field r"
+by(auto simp add: refl_on_def Field_def order_on_defs)
+
+
+lemma well_order_on_Well_order:
+"well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
+using well_order_on_Field by simp
+
+
+lemma Total_subset_Id:
+assumes TOT: "Total r" and SUB: "r \<le> Id"
+shows "r = {} \<or> (\<exists>a. r = {(a,a)})"
+proof-
+ {assume "r \<noteq> {}"
+ then obtain a b where 1: "(a,b) \<in> r" by fast
+ hence "a = b" using SUB by blast
+ hence 2: "(a,a) \<in> r" using 1 by simp
+ {fix c d assume "(c,d) \<in> r"
+ hence "{a,c,d} \<le> Field r" using 1 unfolding Field_def by blast
+ hence "((a,c) \<in> r \<or> (c,a) \<in> r \<or> a = c) \<and>
+ ((a,d) \<in> r \<or> (d,a) \<in> r \<or> a = d)"
+ using TOT unfolding total_on_def by blast
+ hence "a = c \<and> a = d" using SUB by blast
+ }
+ hence "r \<le> {(a,a)}" by auto
+ with 2 have "\<exists>a. r = {(a,a)}" by blast
+ }
+ thus ?thesis by blast
+qed
+
+
+lemma Linear_order_in_diff_Id:
+assumes LI: "Linear_order r" and
+ IN1: "a \<in> Field r" and IN2: "b \<in> Field r"
+shows "((a,b) \<in> r) = ((b,a) \<notin> r - Id)"
+using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force
+
+
+subsection {* The upper and lower bounds operators *}
+
+
+text{* Here we define upper (``above") and lower (``below") bounds operators.
+We think of @{text "r"} as a {\em non-strict} relation. The suffix ``S"
+at the names of some operators indicates that the bounds are strict -- e.g.,
+@{text "underS a"} is the set of all strict lower bounds of @{text "a"} (w.r.t. @{text "r"}).
+Capitalization of the first letter in the name reminds that the operator acts on sets, rather
+than on individual elements. *}
+
+definition under::"'a \<Rightarrow> 'a set"
+where "under a \<equiv> {b. (b,a) \<in> r}"
+
+definition underS::"'a \<Rightarrow> 'a set"
+where "underS a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
+
+definition Under::"'a set \<Rightarrow> 'a set"
+where "Under A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
+
+definition UnderS::"'a set \<Rightarrow> 'a set"
+where "UnderS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
+
+definition above::"'a \<Rightarrow> 'a set"
+where "above a \<equiv> {b. (a,b) \<in> r}"
+
+definition aboveS::"'a \<Rightarrow> 'a set"
+where "aboveS a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
+
+definition Above::"'a set \<Rightarrow> 'a set"
+where "Above A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
+
+definition AboveS::"'a set \<Rightarrow> 'a set"
+where "AboveS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
+(* *)
+
+text{* Note: In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
+ we bounded comprehension by @{text "Field r"} in order to properly cover
+ the case of @{text "A"} being empty. *}
+
+
+lemma underS_subset_under: "underS a \<le> under a"
+by(auto simp add: underS_def under_def)
+
+
+lemma underS_notIn: "a \<notin> underS a"
+by(simp add: underS_def)
+
+
+lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under a"
+by(simp add: refl_on_def under_def)
+
+
+lemma AboveS_disjoint: "A Int (AboveS A) = {}"
+by(auto simp add: AboveS_def)
+
+
+lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS (underS a)"
+by(auto simp add: AboveS_def underS_def)
+
+
+lemma Refl_under_underS:
+assumes "Refl r" "a \<in> Field r"
+shows "under a = underS a \<union> {a}"
+unfolding under_def underS_def
+using assms refl_on_def[of _ r] by fastforce
+
+
+lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS a = {}"
+by (auto simp: Field_def underS_def)
+
+
+lemma under_Field: "under a \<le> Field r"
+by(unfold under_def Field_def, auto)
+
+
+lemma underS_Field: "underS a \<le> Field r"
+by(unfold underS_def Field_def, auto)
+
+
+lemma underS_Field2:
+"a \<in> Field r \<Longrightarrow> underS a < Field r"
+using assms underS_notIn underS_Field by blast
+
+
+lemma underS_Field3:
+"Field r \<noteq> {} \<Longrightarrow> underS a < Field r"
+by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)
+
+
+lemma AboveS_Field: "AboveS A \<le> Field r"
+by(unfold AboveS_def Field_def, auto)
+
+
+lemma under_incr:
+assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
+shows "under a \<le> under b"
+proof(unfold under_def, auto)
+ fix x assume "(x,a) \<in> r"
+ with REL TRANS trans_def[of r]
+ show "(x,b) \<in> r" by blast
+qed
+
+
+lemma underS_incr:
+assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ REL: "(a,b) \<in> r"
+shows "underS a \<le> underS b"
+proof(unfold underS_def, auto)
+ assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
+ with ANTISYM antisym_def[of r] REL
+ show False by blast
+next
+ fix x assume "x \<noteq> a" "(x,a) \<in> r"
+ with REL TRANS trans_def[of r]
+ show "(x,b) \<in> r" by blast
+qed
+
+
+lemma underS_incl_iff:
+assumes LO: "Linear_order r" and
+ INa: "a \<in> Field r" and INb: "b \<in> Field r"
+shows "(underS a \<le> underS b) = ((a,b) \<in> r)"
+proof
+ assume "(a,b) \<in> r"
+ thus "underS a \<le> underS b" using LO
+ by (simp add: order_on_defs underS_incr)
+next
+ assume *: "underS a \<le> underS b"
+ {assume "a = b"
+ hence "(a,b) \<in> r" using assms
+ by (simp add: order_on_defs refl_on_def)
+ }
+ moreover
+ {assume "a \<noteq> b \<and> (b,a) \<in> r"
+ hence "b \<in> underS a" unfolding underS_def by blast
+ hence "b \<in> underS b" using * by blast
+ hence False by (simp add: underS_notIn)
+ }
+ ultimately
+ show "(a,b) \<in> r" using assms
+ order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
+qed
+
+
+end (* context rel *)
+
+end