Theory Order_Relation_More_Base

(*  Title:      HOL/Cardinals/Order_Relation_More_Base.thy
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2012

Basics on order-like relations (base).
*)

header {* Basics on Order-Like Relations (Base) *}

theory Order_Relation_More_Base
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:
"[|refl_on A r; (a,b) : r|] ==> a ∈ A ∧ b ∈ A"
by(auto simp add: refl_on_def)


corollary well_order_on_domain:
"[|well_order_on A r; (a,b) ∈ r|] ==> a ∈ A ∧ b ∈ A"
by(simp add: refl_on_domain order_on_defs)


lemma well_order_on_Field:
"well_order_on A r ==> 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 ==> A = Field r ∧ Well_order r"
using well_order_on_Field by simp


lemma Total_Id_Field:
assumes TOT: "Total r" and NID: "¬ (r <= Id)"
shows "Field r = Field(r - Id)"
using mono_Field[of "r - Id" r] Diff_subset[of r Id]
proof(auto)
  have "r ≠ {}" using NID by fast
  then obtain b and c where "b ≠ c ∧ (b,c) ∈ r" using NID by fast
  hence 1: "b ≠ c ∧ {b,c} ≤ Field r" by (auto simp: Field_def)
  (*  *)
  fix a assume *: "a ∈ Field r"
  obtain d where 2: "d ∈ Field r" and 3: "d ≠ a"
  using * 1 by blast
  hence "(a,d) ∈ r ∨ (d,a) ∈ r" using * TOT
  by (simp add: total_on_def)
  thus "a ∈ Field(r - Id)" using 3 unfolding Field_def by blast
qed


lemma Total_subset_Id:
assumes TOT: "Total r" and SUB: "r ≤ Id"
shows "r = {} ∨ (∃a. r = {(a,a)})"
proof-
  {assume "r ≠ {}"
   then obtain a b where 1: "(a,b) ∈ r" by fast
   hence "a = b" using SUB by blast
   hence 2: "(a,a) ∈ r" using 1 by simp
   {fix c d assume "(c,d) ∈ r"
    hence "{a,c,d} ≤ Field r" using 1 unfolding Field_def by blast
    hence "((a,c) ∈ r ∨ (c,a) ∈ r ∨ a = c) ∧
           ((a,d) ∈ r ∨ (d,a) ∈ r ∨ a = d)"
    using TOT unfolding total_on_def by blast
    hence "a = c ∧ a = d" using SUB by blast
   }
   hence "r ≤ {(a,a)}" by auto
   with 2 have "∃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 ∈ Field r" and IN2: "b ∈ Field r"
shows "((a,b) ∈ r) = ((b,a) ∉ 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 => 'a set"
where "under a ≡ {b. (b,a) ∈ r}"

definition underS::"'a => 'a set"
where "underS a ≡ {b. b ≠ a ∧ (b,a) ∈ r}"

definition Under::"'a set => 'a set"
where "Under A ≡ {b ∈ Field r. ∀a ∈ A. (b,a) ∈ r}"

definition UnderS::"'a set => 'a set"
where "UnderS A ≡ {b ∈ Field r. ∀a ∈ A. b ≠ a ∧ (b,a) ∈ r}"

definition above::"'a => 'a set"
where "above a ≡ {b. (a,b) ∈ r}"

definition aboveS::"'a => 'a set"
where "aboveS a ≡ {b. b ≠ a ∧ (a,b) ∈ r}"

definition Above::"'a set => 'a set"
where "Above A ≡ {b ∈ Field r. ∀a ∈ A. (a,b) ∈ r}"

definition AboveS::"'a set => 'a set"
where "AboveS A ≡ {b ∈ Field r. ∀a ∈ A. b ≠ a ∧ (a,b) ∈ 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 ≤ Under A"
by(auto simp add: UnderS_def Under_def)


lemma underS_subset_under: "underS a ≤ under a"
by(auto simp add: underS_def under_def)


lemma underS_notIn: "a ∉ underS a"
by(simp add: underS_def)


lemma Refl_under_in: "[|Refl r; a ∈ Field r|] ==> a ∈ 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 ∈ Field r ==> a ∈ AboveS (underS a)"
by(auto simp add: AboveS_def underS_def)


lemma Refl_under_underS:
assumes "Refl r" "a ∈ Field r"
shows "under a = underS a ∪ {a}"
unfolding under_def underS_def
using assms refl_on_def[of _ r] by fastforce


lemma underS_empty: "a ∉ Field r ==> underS a = {}"
by (auto simp: Field_def underS_def)


lemma under_Field: "under a ≤ Field r"
by(unfold under_def Field_def, auto)


lemma underS_Field: "underS a ≤ Field r"
by(unfold underS_def Field_def, auto)


lemma underS_Field2:
"a ∈ Field r ==> underS a < Field r"
using assms underS_notIn underS_Field by blast


lemma underS_Field3:
"Field r ≠ {} ==> underS a < Field r"
by(cases "a ∈ Field r", simp add: underS_Field2, auto simp add: underS_empty)


lemma Under_Field: "Under A ≤ Field r"
by(unfold Under_def Field_def, auto)


lemma UnderS_Field: "UnderS A ≤ Field r"
by(unfold UnderS_def Field_def, auto)


lemma AboveS_Field: "AboveS A ≤ Field r"
by(unfold AboveS_def Field_def, auto)


lemma under_incr:
assumes TRANS: "trans r" and REL: "(a,b) ∈ r"
shows "under a ≤ under b"
proof(unfold under_def, auto)
  fix x assume "(x,a) ∈ r"
  with REL TRANS trans_def[of r]
  show "(x,b) ∈ r" by blast
qed


lemma underS_incr:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
        REL: "(a,b) ∈ r"
shows "underS a ≤ underS b"
proof(unfold underS_def, auto)
  assume *: "b ≠ a" and **: "(b,a) ∈ r"
  with ANTISYM antisym_def[of r] REL
  show False by blast
next
  fix x assume "x ≠ a" "(x,a) ∈ r"
  with REL TRANS trans_def[of r]
  show "(x,b) ∈ r" by blast
qed


lemma underS_incl_iff:
assumes LO: "Linear_order r" and
        INa: "a ∈ Field r" and INb: "b ∈ Field r"
shows "(underS a ≤ underS b) = ((a,b) ∈ r)"
proof
  assume "(a,b) ∈ r"
  thus "underS a ≤ underS b" using LO
  by (simp add: order_on_defs underS_incr)
next
  assume *: "underS a ≤ underS b"
  {assume "a = b"
   hence "(a,b) ∈ r" using assms
   by (simp add: order_on_defs refl_on_def)
  }
  moreover
  {assume "a ≠ b ∧ (b,a) ∈ r"
   hence "b ∈ underS a" unfolding underS_def by blast
   hence "b ∈ underS b" using * by blast
   hence False by (simp add: underS_notIn)
  }
  ultimately
  show "(a,b) ∈ r" using assms
  order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
qed


lemma under_Under_trans:
assumes TRANS: "trans r" and
        IN1: "a ∈ under b" and IN2: "b ∈ Under C"
shows "a ∈ Under C"
proof-
  have "(a,b) ∈ r ∧ (∀c ∈ C. (b,c) ∈ r)"
  using IN1 IN2 under_def Under_def by blast
  hence "∀c ∈ C. (a,c) ∈ r"
  using TRANS trans_def[of r] by blast
  moreover
  have "a ∈ Field r" using IN1 unfolding Field_def under_def by blast
  ultimately
  show ?thesis unfolding Under_def by blast
qed


lemma under_UnderS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
        IN1: "a ∈ under b" and IN2: "b ∈ UnderS C"
shows "a ∈ UnderS C"
proof-
  from IN2 have "b ∈ Under C"
  using UnderS_subset_Under[of C] by blast
  with assms under_Under_trans
  have "a ∈ Under C" by blast
  (*  *)
  moreover
  have "a ∉ C"
  proof
    assume *: "a ∈ C"
    have 1: "(a,b) ∈ r"
    using IN1 under_def[of b] by auto
    have "∀c ∈ C. b ≠ c ∧ (b,c) ∈ r"
    using IN2 UnderS_def[of C] by blast
    with * have "b ≠ a ∧ (b,a) ∈ r" by blast
    with 1 ANTISYM antisym_def[of r]
    show False by blast
  qed
  (*  *)
  ultimately
  show ?thesis unfolding UnderS_def Under_def by fast
qed


end  (* context rel *)

end