Theory Order_Relation_More

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

Basics on order-like relations.
*)

section ‹Basics on Order-Like Relations›

theory Order_Relation_More
  imports Main
begin

subsection ‹The upper and lower bounds operators›

lemma aboveS_subset_above: "aboveS r a  above r a"
  by(auto simp add: aboveS_def above_def)

lemma AboveS_subset_Above: "AboveS r A  Above r A"
  by(auto simp add: AboveS_def Above_def)

lemma UnderS_disjoint: "A Int (UnderS r A) = {}"
  by(auto simp add: UnderS_def)

lemma aboveS_notIn: "a  aboveS r a"
  by(auto simp add: aboveS_def)

lemma Refl_above_in: "Refl r; a  Field r  a  above r a"
  by(auto simp add: refl_on_def above_def)

lemma in_Above_under: "a  Field r  a  Above r (under r a)"
  by(auto simp add: Above_def under_def)

lemma in_Under_above: "a  Field r  a  Under r (above r a)"
  by(auto simp add: Under_def above_def)

lemma in_UnderS_aboveS: "a  Field r  a  UnderS r (aboveS r a)"
  by(auto simp add: UnderS_def aboveS_def)

lemma UnderS_subset_Under: "UnderS r A  Under r A"
  by(auto simp add: UnderS_def Under_def)

lemma subset_Above_Under: "B  Field r  B  Above r (Under r B)"
  by(auto simp add: Above_def Under_def)

lemma subset_Under_Above: "B  Field r  B  Under r (Above r B)"
  by(auto simp add: Under_def Above_def)

lemma subset_AboveS_UnderS: "B  Field r  B  AboveS r (UnderS r B)"
  by(auto simp add: AboveS_def UnderS_def)

lemma subset_UnderS_AboveS: "B  Field r  B  UnderS r (AboveS r B)"
  by(auto simp add: UnderS_def AboveS_def)

lemma Under_Above_Galois:
  "B  Field r; C  Field r  (B  Above r C) = (C  Under r B)"
  by(unfold Above_def Under_def, blast)

lemma UnderS_AboveS_Galois:
  "B  Field r; C  Field r  (B  AboveS r C) = (C  UnderS r B)"
  by(unfold AboveS_def UnderS_def, blast)

lemma Refl_above_aboveS:
  assumes REFL: "Refl r" and IN: "a  Field r"
  shows "above r a = aboveS r a  {a}"
proof(unfold above_def aboveS_def, auto)
  show "(a,a)  r" using REFL IN refl_on_def[of _ r] by blast
qed

lemma Linear_order_under_aboveS_Field:
  assumes LIN: "Linear_order r" and IN: "a  Field r"
  shows "Field r = under r a  aboveS r a"
proof(unfold under_def aboveS_def, auto)
  assume "a  Field r" "(a, a)  r"
  with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
  show False by auto
next
  fix b assume "b  Field r" "(b, a)  r"
  with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r]
  have "(a,b)  r  a = b" by blast
  thus "(a,b)  r"
    using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto
next
  fix b assume "(b, a)  r"
  thus "b  Field r"
    using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast
next
  fix b assume "b  a" "(a, b)  r"
  thus "b  Field r"
    using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
qed

lemma Linear_order_underS_above_Field:
  assumes LIN: "Linear_order r" and IN: "a  Field r"
  shows "Field r = underS r a  above r a"
proof(unfold underS_def above_def, auto)
  assume "a  Field r" "(a, a)  r"
  with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
  show False by metis
next
  fix b assume "b  Field r" "(a, b)  r"
  with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r]
  have "(b,a)  r  b = a" by blast
  thus "(b,a)  r"
    using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto
next
  fix b assume "b  a" "(b, a)  r"
  thus "b  Field r"
    using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast
next
  fix b assume "(a, b)  r"
  thus "b  Field r"
    using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
qed

lemma under_empty: "a  Field r  under r a = {}"
  unfolding Field_def under_def by auto

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

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

lemma above_Field: "above r a  Field r"
  by(unfold above_def Field_def, auto)

lemma aboveS_Field: "aboveS r a  Field r"
  by(unfold aboveS_def Field_def, auto)

lemma Above_Field: "Above r A  Field r"
  by(unfold Above_def Field_def, auto)

lemma Refl_under_Under:
  assumes REFL: "Refl r" and NE: "A  {}"
  shows "Under r A = (a  A. under r a)"
proof
  show "Under r A  (a  A. under r a)"
    by(unfold Under_def under_def, auto)
next
  show "(a  A. under r a)  Under r A"
  proof(auto)
    fix x
    assume *: "xa  A. x  under r xa"
    hence "xa  A. (x,xa)  r"
      by (simp add: under_def)
    moreover
    {from NE obtain a where "a  A" by blast
      with * have "x  under r a" by simp
      hence "x  Field r"
        using under_Field[of r a] by auto
    }
    ultimately show "x  Under r A"
      unfolding Under_def by auto
  qed
qed

lemma Refl_underS_UnderS:
  assumes REFL: "Refl r" and NE: "A  {}"
  shows "UnderS r A = (a  A. underS r a)"
proof
  show "UnderS r A  (a  A. underS r a)"
    by(unfold UnderS_def underS_def, auto)
next
  show "(a  A. underS r a)  UnderS r A"
  proof(auto)
    fix x
    assume *: "xa  A. x  underS r xa"
    hence "xa  A. x  xa  (x,xa)  r"
      by (auto simp add: underS_def)
    moreover
    {from NE obtain a where "a  A" by blast
      with * have "x  underS r a" by simp
      hence "x  Field r"
        using underS_Field[of _ r a] by auto
    }
    ultimately show "x  UnderS r A"
      unfolding UnderS_def by auto
  qed
qed

lemma Refl_above_Above:
  assumes REFL: "Refl r" and NE: "A  {}"
  shows "Above r A = (a  A. above r a)"
proof
  show "Above r A  (a  A. above r a)"
    by(unfold Above_def above_def, auto)
next
  show "(a  A. above r a)  Above r A"
  proof(auto)
    fix x
    assume *: "xa  A. x  above r xa"
    hence "xa  A. (xa,x)  r"
      by (simp add: above_def)
    moreover
    {from NE obtain a where "a  A" by blast
      with * have "x  above r a" by simp
      hence "x  Field r"
        using above_Field[of r a] by auto
    }
    ultimately show "x  Above r A"
      unfolding Above_def by auto
  qed
qed

lemma Refl_aboveS_AboveS:
  assumes REFL: "Refl r" and NE: "A  {}"
  shows "AboveS r A = (a  A. aboveS r a)"
proof
  show "AboveS r A  (a  A. aboveS r a)"
    by(unfold AboveS_def aboveS_def, auto)
next
  show "(a  A. aboveS r a)  AboveS r A"
  proof(auto)
    fix x
    assume *: "xa  A. x  aboveS r xa"
    hence "xa  A. xa  x  (xa,x)  r"
      by (auto simp add: aboveS_def)
    moreover
    {from NE obtain a where "a  A" by blast
      with * have "x  aboveS r a" by simp
      hence "x  Field r"
        using aboveS_Field[of r a] by auto
    }
    ultimately show "x  AboveS r A"
      unfolding AboveS_def by auto
  qed
qed

lemma under_Under_singl: "under r a = Under r {a}"
  by(unfold Under_def under_def, auto simp add: Field_def)

lemma underS_UnderS_singl: "underS r a = UnderS r {a}"
  by(unfold UnderS_def underS_def, auto simp add: Field_def)

lemma above_Above_singl: "above r a = Above r {a}"
  by(unfold Above_def above_def, auto simp add: Field_def)

lemma aboveS_AboveS_singl: "aboveS r a = AboveS r {a}"
  by(unfold AboveS_def aboveS_def, auto simp add: Field_def)

lemma Under_decr: "A  B  Under r B  Under r A"
  by(unfold Under_def, auto)

lemma UnderS_decr: "A  B  UnderS r B  UnderS r A"
  by(unfold UnderS_def, auto)

lemma Above_decr: "A  B  Above r B  Above r A"
  by(unfold Above_def, auto)

lemma AboveS_decr: "A  B  AboveS r B  AboveS r A"
  by(unfold AboveS_def, auto)

lemma under_incl_iff:
  assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a  Field r"
  shows "(under r a  under r b) = ((a,b)  r)"
proof
  assume "(a,b)  r"
  thus "under r a  under r b" using TRANS
    by (auto simp add: under_incr)
next
  assume "under r a  under r b"
  moreover
  have "a  under r a" using REFL IN
    by (auto simp add: Refl_under_in)
  ultimately show "(a,b)  r"
    by (auto simp add: under_def)
qed

lemma above_decr:
  assumes TRANS: "trans r" and REL: "(a,b)  r"
  shows "above r b  above r a"
proof(unfold above_def, auto)
  fix x assume "(b,x)  r"
  with REL TRANS trans_def[of r]
  show "(a,x)  r" by blast
qed

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

lemma under_trans:
  assumes TRANS: "trans r" and
    IN1: "a  under r b" and IN2: "b  under r c"
  shows "a  under r c"
proof-
  have "(a,b)  r  (b,c)  r"
    using IN1 IN2 under_def by fastforce
  hence "(a,c)  r"
    using TRANS trans_def[of r] by blast
  thus ?thesis unfolding under_def by simp
qed

lemma under_underS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a  under r b" and IN2: "b  underS r c"
  shows "a  underS r c"
proof-
  have 0: "(a,b)  r  (b,c)  r"
    using IN1 IN2 under_def underS_def by fastforce
  hence 1: "(a,c)  r"
    using TRANS trans_def[of r] by blast
  have 2: "b  c" using IN2 underS_def by force
  have 3: "a  c"
  proof
    assume "a = c" with 0 2 ANTISYM antisym_def[of r]
    show False by auto
  qed
  from 1 3 show ?thesis unfolding underS_def by simp
qed

lemma underS_under_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a  underS r b" and IN2: "b  under r c"
  shows "a  underS r c"
proof-
  have 0: "(a,b)  r  (b,c)  r"
    using IN1 IN2 under_def underS_def by fast
  hence 1: "(a,c)  r"
    using TRANS trans_def[of r] by fast
  have 2: "a  b" using IN1 underS_def by force
  have 3: "a  c"
  proof
    assume "a = c" with 0 2 ANTISYM antisym_def[of r]
    show False by auto
  qed
  from 1 3 show ?thesis unfolding underS_def by simp
qed

lemma underS_underS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a  underS r b" and IN2: "b  underS r c"
  shows "a  underS r c"
proof-
  have "a  under r b"
    using IN1 underS_subset_under by fast
  with assms under_underS_trans show ?thesis by fast
qed

lemma above_trans:
  assumes TRANS: "trans r" and
    IN1: "b  above r a" and IN2: "c  above r b"
  shows "c  above r a"
proof-
  have "(a,b)  r  (b,c)  r"
    using IN1 IN2 above_def by fast
  hence "(a,c)  r"
    using TRANS trans_def[of r] by blast
  thus ?thesis unfolding above_def by simp
qed

lemma above_aboveS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "b  above r a" and IN2: "c  aboveS r b"
  shows "c  aboveS r a"
proof-
  have 0: "(a,b)  r  (b,c)  r"
    using IN1 IN2 above_def aboveS_def by fast
  hence 1: "(a,c)  r"
    using TRANS trans_def[of r] by blast
  have 2: "b  c" using IN2 aboveS_def by force
  have 3: "a  c"
  proof
    assume "a = c" with 0 2 ANTISYM antisym_def[of r]
    show False by auto
  qed
  from 1 3 show ?thesis unfolding aboveS_def by simp
qed

lemma aboveS_above_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "b  aboveS r a" and IN2: "c  above r b"
  shows "c  aboveS r a"
proof-
  have 0: "(a,b)  r  (b,c)  r"
    using IN1 IN2 above_def aboveS_def by fast
  hence 1: "(a,c)  r"
    using TRANS trans_def[of r] by blast
  have 2: "a  b" using IN1 aboveS_def by force
  have 3: "a  c"
  proof
    assume "a = c" with 0 2 ANTISYM antisym_def[of r]
    show False by auto
  qed
  from 1 3 show ?thesis unfolding aboveS_def by simp
qed

lemma aboveS_aboveS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "b  aboveS r a" and IN2: "c  aboveS r b"
  shows "c  aboveS r a"
proof-
  have "b  above r a"
    using IN1 aboveS_subset_above by fast
  with assms above_aboveS_trans show ?thesis by fast
qed

lemma under_Under_trans:
  assumes TRANS: "trans r" and
    IN1: "a  under r b" and IN2: "b  Under r C"
  shows "a  Under r C"
proof-
  have "b  {u  Field r. x. x  C  (u, x)  r}"
    using IN2 Under_def by force
  hence "(a,b)  r  (c  C. (b,c)  r)"
    using IN1 under_def by fast
  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 underS_Under_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a  underS r b" and IN2: "b  Under r C"
  shows "a  UnderS r C"
proof-
  from IN1 have "a  under r b"
    using underS_subset_under[of r b] by fast
  with assms under_Under_trans
  have "a  Under r C" by fast
      (*  *)
  moreover
  have "a  C"
  proof
    assume *: "a  C"
    have 1: "b  a  (a,b)  r"
      using IN1 underS_def[of r b] by auto
    have "c  C. (b,c)  r"
      using IN2 Under_def[of r C] by auto
    with * have "(b,a)  r" by simp
    with 1 ANTISYM antisym_def[of r]
    show False by blast
  qed
    (*  *)
  ultimately
  show ?thesis unfolding UnderS_def
    using Under_def by force
qed

lemma underS_UnderS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a  underS r b" and IN2: "b  UnderS r C"
  shows "a  UnderS r C"
proof-
  from IN2 have "b  Under r C"
    using UnderS_subset_Under[of r C] by blast
  with underS_Under_trans assms
  show ?thesis by force
qed

lemma above_Above_trans:
  assumes TRANS: "trans r" and
    IN1: "a  above r b" and IN2: "b  Above r C"
  shows "a  Above r C"
proof-
  have "(b,a)  r  (c  C. (c,b)  r)"
    using IN1[unfolded above_def] IN2[unfolded Above_def] by simp
  hence "c  C. (c,a)  r"
    using TRANS trans_def[of r] by blast
  moreover
  have "a  Field r" using IN1[unfolded above_def] Field_def by fast
  ultimately
  show ?thesis unfolding Above_def by auto
qed

lemma aboveS_Above_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a  aboveS r b" and IN2: "b  Above r C"
  shows "a  AboveS r C"
proof-
  from IN1 have "a  above r b"
    using aboveS_subset_above[of r b] by blast
  with assms above_Above_trans
  have "a  Above r C" by fast
      (*  *)
  moreover
  have "a  C"
  proof
    assume *: "a  C"
    have 1: "b  a  (b,a)  r"
      using IN1 aboveS_def[of r b] by auto
    have "c  C. (c,b)  r"
      using IN2 Above_def[of r C] by auto
    with * have "(a,b)  r" by simp
    with 1 ANTISYM antisym_def[of r]
    show False by blast
  qed
    (*  *)
  ultimately
  show ?thesis unfolding AboveS_def
    using Above_def by force
qed

lemma above_AboveS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a  above r b" and IN2: "b  AboveS r C"
  shows "a  AboveS r C"
proof-
  from IN2 have "b  Above r C"
    using AboveS_subset_Above[of r C] by blast
  with assms above_Above_trans
  have "a  Above r C" by force
      (*  *)
  moreover
  have "a  C"
  proof
    assume *: "a  C"
    have 1: "(b,a)  r"
      using IN1 above_def[of r b] by auto
    have "c  C. b  c  (c,b)  r"
      using IN2 AboveS_def[of r C] by auto
    with * have "b  a  (a,b)  r" by simp
    with 1 ANTISYM antisym_def[of r]
    show False by blast
  qed
    (*  *)
  ultimately
  show ?thesis unfolding AboveS_def
    using Above_def by force
qed

lemma aboveS_AboveS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a  aboveS r b" and IN2: "b  AboveS r C"
  shows "a  AboveS r C"
proof-
  from IN2 have "b  Above r C"
    using AboveS_subset_Above[of r C] by blast
  with aboveS_Above_trans assms
  show ?thesis by force
qed

lemma under_UnderS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a  under r b" and IN2: "b  UnderS r C"
  shows "a  UnderS r C"
proof-
  from IN2 have "b  Under r C"
    using UnderS_subset_Under[of r C] by blast
  with assms under_Under_trans
  have "a  Under r C" by force
      (*  *)
  moreover
  have "a  C"
  proof
    assume *: "a  C"
    have 1: "(a,b)  r"
      using IN1 under_def[of r b] by auto
    have "c  C. b  c  (b,c)  r"
      using IN2 UnderS_def[of r 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


subsection ‹Properties depending on more than one relation›

lemma under_incr2:
  "r  r'  under r a  under r' a"
  unfolding under_def by blast

lemma underS_incr2:
  "r  r'  underS r a  underS r' a"
  unfolding underS_def by blast

(* FIXME: r ↝ r'
lemma Under_incr:
"r ≤ r' ⟹ Under r A ≤ Under r A"
unfolding Under_def by blast

lemma UnderS_incr:
"r ≤ r' ⟹ UnderS r A ≤ UnderS r A"
unfolding UnderS_def by blast

lemma Under_incr_decr:
"⟦r ≤ r'; A' ≤ A⟧  ⟹ Under r A ≤ Under r A'"
unfolding Under_def by blast

lemma UnderS_incr_decr:
"⟦r ≤ r'; A' ≤ A⟧  ⟹ UnderS r A ≤ UnderS r A'"
unfolding UnderS_def by blast
*)

lemma above_incr2:
  "r  r'  above r a  above r' a"
  unfolding above_def by blast

lemma aboveS_incr2:
  "r  r'  aboveS r a  aboveS r' a"
  unfolding aboveS_def by blast

(* FIXME
lemma Above_incr:
"r ≤ r' ⟹ Above r A ≤ Above r A"
unfolding Above_def by blast

lemma AboveS_incr:
"r ≤ r' ⟹ AboveS r A ≤ AboveS r A"
unfolding AboveS_def by blast

lemma Above_incr_decr:
"⟦r ≤ r'; A' ≤ A⟧ ⟹ Above r A ≤ Above r A'"
unfolding Above_def by blast

lemma AboveS_incr_decr:
"⟦r ≤ r'; A' ≤ A⟧ ⟹ AboveS r A ≤ AboveS r A'"
unfolding AboveS_def by blast
*)

end