Up to index of Isabelle/HOL/Free-Groups
theory Order_Relation_More(* Title: HOL/Cardinals/Order_Relation_More.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
Basics on order-like relations.
*)
header {* Basics on Order-Like Relations *}
theory Order_Relation_More
imports Order_Relation_More_Base
begin
subsection {* The upper and lower bounds operators *}
lemma (in rel) aboveS_subset_above: "aboveS a ≤ above a"
by(auto simp add: aboveS_def above_def)
lemma (in rel) AboveS_subset_Above: "AboveS A ≤ Above A"
by(auto simp add: AboveS_def Above_def)
lemma (in rel) UnderS_disjoint: "A Int (UnderS A) = {}"
by(auto simp add: UnderS_def)
lemma (in rel) aboveS_notIn: "a ∉ aboveS a"
by(auto simp add: aboveS_def)
lemma (in rel) Refl_above_in: "[|Refl r; a ∈ Field r|] ==> a ∈ above a"
by(auto simp add: refl_on_def above_def)
lemma (in rel) in_Above_under: "a ∈ Field r ==> a ∈ Above (under a)"
by(auto simp add: Above_def under_def)
lemma (in rel) in_Under_above: "a ∈ Field r ==> a ∈ Under (above a)"
by(auto simp add: Under_def above_def)
lemma (in rel) in_UnderS_aboveS: "a ∈ Field r ==> a ∈ UnderS (aboveS a)"
by(auto simp add: UnderS_def aboveS_def)
lemma (in rel) subset_Above_Under: "B ≤ Field r ==> B ≤ Above (Under B)"
by(auto simp add: Above_def Under_def)
lemma (in rel) subset_Under_Above: "B ≤ Field r ==> B ≤ Under (Above B)"
by(auto simp add: Under_def Above_def)
lemma (in rel) subset_AboveS_UnderS: "B ≤ Field r ==> B ≤ AboveS (UnderS B)"
by(auto simp add: AboveS_def UnderS_def)
lemma (in rel) subset_UnderS_AboveS: "B ≤ Field r ==> B ≤ UnderS (AboveS B)"
by(auto simp add: UnderS_def AboveS_def)
lemma (in rel) Under_Above_Galois:
"[|B ≤ Field r; C ≤ Field r|] ==> (B ≤ Above C) = (C ≤ Under B)"
by(unfold Above_def Under_def, blast)
lemma (in rel) UnderS_AboveS_Galois:
"[|B ≤ Field r; C ≤ Field r|] ==> (B ≤ AboveS C) = (C ≤ UnderS B)"
by(unfold AboveS_def UnderS_def, blast)
lemma (in rel) Refl_above_aboveS:
assumes REFL: "Refl r" and IN: "a ∈ Field r"
shows "above a = aboveS 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 (in rel) Linear_order_under_aboveS_Field:
assumes LIN: "Linear_order r" and IN: "a ∈ Field r"
shows "Field r = under a ∪ aboveS 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 (in rel) Linear_order_underS_above_Field:
assumes LIN: "Linear_order r" and IN: "a ∈ Field r"
shows "Field r = underS a ∪ above 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 auto
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 (in rel) under_empty: "a ∉ Field r ==> under a = {}"
unfolding Field_def under_def by auto
lemma (in rel) above_Field: "above a ≤ Field r"
by(unfold above_def Field_def, auto)
lemma (in rel) aboveS_Field: "aboveS a ≤ Field r"
by(unfold aboveS_def Field_def, auto)
lemma (in rel) Above_Field: "Above A ≤ Field r"
by(unfold Above_def Field_def, auto)
lemma (in rel) Refl_under_Under:
assumes REFL: "Refl r" and NE: "A ≠ {}"
shows "Under A = (\<Inter> a ∈ A. under a)"
proof
show "Under A ⊆ (\<Inter> a ∈ A. under a)"
by(unfold Under_def under_def, auto)
next
show "(\<Inter> a ∈ A. under a) ⊆ Under A"
proof(auto)
fix x
assume *: "∀xa ∈ A. x ∈ under 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 a" by simp
hence "x ∈ Field r"
using under_Field[of a] by auto
}
ultimately show "x ∈ Under A"
unfolding Under_def by auto
qed
qed
lemma (in rel) Refl_underS_UnderS:
assumes REFL: "Refl r" and NE: "A ≠ {}"
shows "UnderS A = (\<Inter> a ∈ A. underS a)"
proof
show "UnderS A ⊆ (\<Inter> a ∈ A. underS a)"
by(unfold UnderS_def underS_def, auto)
next
show "(\<Inter> a ∈ A. underS a) ⊆ UnderS A"
proof(auto)
fix x
assume *: "∀xa ∈ A. x ∈ underS 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 a" by simp
hence "x ∈ Field r"
using underS_Field[of a] by auto
}
ultimately show "x ∈ UnderS A"
unfolding UnderS_def by auto
qed
qed
lemma (in rel) Refl_above_Above:
assumes REFL: "Refl r" and NE: "A ≠ {}"
shows "Above A = (\<Inter> a ∈ A. above a)"
proof
show "Above A ⊆ (\<Inter> a ∈ A. above a)"
by(unfold Above_def above_def, auto)
next
show "(\<Inter> a ∈ A. above a) ⊆ Above A"
proof(auto)
fix x
assume *: "∀xa ∈ A. x ∈ above 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 a" by simp
hence "x ∈ Field r"
using above_Field[of a] by auto
}
ultimately show "x ∈ Above A"
unfolding Above_def by auto
qed
qed
lemma (in rel) Refl_aboveS_AboveS:
assumes REFL: "Refl r" and NE: "A ≠ {}"
shows "AboveS A = (\<Inter> a ∈ A. aboveS a)"
proof
show "AboveS A ⊆ (\<Inter> a ∈ A. aboveS a)"
by(unfold AboveS_def aboveS_def, auto)
next
show "(\<Inter> a ∈ A. aboveS a) ⊆ AboveS A"
proof(auto)
fix x
assume *: "∀xa ∈ A. x ∈ aboveS 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 a" by simp
hence "x ∈ Field r"
using aboveS_Field[of a] by auto
}
ultimately show "x ∈ AboveS A"
unfolding AboveS_def by auto
qed
qed
lemma (in rel) under_Under_singl: "under a = Under {a}"
by(unfold Under_def under_def, auto simp add: Field_def)
lemma (in rel) underS_UnderS_singl: "underS a = UnderS {a}"
by(unfold UnderS_def underS_def, auto simp add: Field_def)
lemma (in rel) above_Above_singl: "above a = Above {a}"
by(unfold Above_def above_def, auto simp add: Field_def)
lemma (in rel) aboveS_AboveS_singl: "aboveS a = AboveS {a}"
by(unfold AboveS_def aboveS_def, auto simp add: Field_def)
lemma (in rel) Under_decr: "A ≤ B ==> Under B ≤ Under A"
by(unfold Under_def, auto)
lemma (in rel) UnderS_decr: "A ≤ B ==> UnderS B ≤ UnderS A"
by(unfold UnderS_def, auto)
lemma (in rel) Above_decr: "A ≤ B ==> Above B ≤ Above A"
by(unfold Above_def, auto)
lemma (in rel) AboveS_decr: "A ≤ B ==> AboveS B ≤ AboveS A"
by(unfold AboveS_def, auto)
lemma (in rel) under_incl_iff:
assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a ∈ Field r"
shows "(under a ≤ under b) = ((a,b) ∈ r)"
proof
assume "(a,b) ∈ r"
thus "under a ≤ under b" using TRANS
by (auto simp add: under_incr)
next
assume "under a ≤ under b"
moreover
have "a ∈ under a" using REFL IN
by (auto simp add: Refl_under_in)
ultimately show "(a,b) ∈ r"
by (auto simp add: under_def)
qed
lemma (in rel) above_decr:
assumes TRANS: "trans r" and REL: "(a,b) ∈ r"
shows "above b ≤ above 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 (in rel) aboveS_decr:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
REL: "(a,b) ∈ r"
shows "aboveS b ≤ aboveS 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 (in rel) 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 ∧ (b,c) ∈ r"
using IN1 IN2 under_def by auto
hence "(a,c) ∈ r"
using TRANS trans_def[of r] by blast
thus ?thesis unfolding under_def by simp
qed
lemma (in rel) 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-
have 0: "(a,b) ∈ r ∧ (b,c) ∈ r"
using IN1 IN2 under_def underS_def by auto
hence 1: "(a,c) ∈ r"
using TRANS trans_def[of r] by blast
have 2: "b ≠ c" using IN2 underS_def by auto
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 (in rel) underS_under_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
IN1: "a ∈ underS b" and IN2: "b ∈ under c"
shows "a ∈ underS c"
proof-
have 0: "(a,b) ∈ r ∧ (b,c) ∈ r"
using IN1 IN2 under_def underS_def by auto
hence 1: "(a,c) ∈ r"
using TRANS trans_def[of r] by blast
have 2: "a ≠ b" using IN1 underS_def by auto
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 (in rel) underS_underS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
IN1: "a ∈ underS b" and IN2: "b ∈ underS c"
shows "a ∈ underS c"
proof-
have "a ∈ under b"
using IN1 underS_subset_under by auto
with assms under_underS_trans show ?thesis by auto
qed
lemma (in rel) above_trans:
assumes TRANS: "trans r" and
IN1: "b ∈ above a" and IN2: "c ∈ above b"
shows "c ∈ above a"
proof-
have "(a,b) ∈ r ∧ (b,c) ∈ r"
using IN1 IN2 above_def by auto
hence "(a,c) ∈ r"
using TRANS trans_def[of r] by blast
thus ?thesis unfolding above_def by simp
qed
lemma (in rel) above_aboveS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
IN1: "b ∈ above a" and IN2: "c ∈ aboveS b"
shows "c ∈ aboveS a"
proof-
have 0: "(a,b) ∈ r ∧ (b,c) ∈ r"
using IN1 IN2 above_def aboveS_def by auto
hence 1: "(a,c) ∈ r"
using TRANS trans_def[of r] by blast
have 2: "b ≠ c" using IN2 aboveS_def by auto
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 (in rel) aboveS_above_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
IN1: "b ∈ aboveS a" and IN2: "c ∈ above b"
shows "c ∈ aboveS a"
proof-
have 0: "(a,b) ∈ r ∧ (b,c) ∈ r"
using IN1 IN2 above_def aboveS_def by auto
hence 1: "(a,c) ∈ r"
using TRANS trans_def[of r] by blast
have 2: "a ≠ b" using IN1 aboveS_def by auto
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 (in rel) aboveS_aboveS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
IN1: "b ∈ aboveS a" and IN2: "c ∈ aboveS b"
shows "c ∈ aboveS a"
proof-
have "b ∈ above a"
using IN1 aboveS_subset_above by auto
with assms above_aboveS_trans show ?thesis by auto
qed
lemma (in rel) underS_Under_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
IN1: "a ∈ underS b" and IN2: "b ∈ Under C"
shows "a ∈ UnderS C"
proof-
from IN1 have "a ∈ under b"
using underS_subset_under[of b] by blast
with assms under_Under_trans
have "a ∈ Under C" by auto
(* *)
moreover
have "a ∉ C"
proof
assume *: "a ∈ C"
have 1: "b ≠ a ∧ (a,b) ∈ r"
using IN1 underS_def[of b] by auto
have "∀c ∈ C. (b,c) ∈ r"
using IN2 Under_def[of 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 auto
qed
lemma (in rel) underS_UnderS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
IN1: "a ∈ underS 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 underS_Under_trans assms
show ?thesis by auto
qed
lemma (in rel) above_Above_trans:
assumes TRANS: "trans r" and
IN1: "a ∈ above b" and IN2: "b ∈ Above C"
shows "a ∈ Above C"
proof-
have "(b,a) ∈ r ∧ (∀c ∈ C. (c,b) ∈ r)"
using IN1 IN2 above_def Above_def by auto
hence "∀c ∈ C. (c,a) ∈ r"
using TRANS trans_def[of r] by blast
moreover
have "a ∈ Field r" using IN1 Field_def above_def by force
ultimately
show ?thesis unfolding Above_def by auto
qed
lemma (in rel) aboveS_Above_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
IN1: "a ∈ aboveS b" and IN2: "b ∈ Above C"
shows "a ∈ AboveS C"
proof-
from IN1 have "a ∈ above b"
using aboveS_subset_above[of b] by blast
with assms above_Above_trans
have "a ∈ Above C" by auto
(* *)
moreover
have "a ∉ C"
proof
assume *: "a ∈ C"
have 1: "b ≠ a ∧ (b,a) ∈ r"
using IN1 aboveS_def[of b] by auto
have "∀c ∈ C. (c,b) ∈ r"
using IN2 Above_def[of 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 auto
qed
lemma (in rel) above_AboveS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
IN1: "a ∈ above b" and IN2: "b ∈ AboveS C"
shows "a ∈ AboveS C"
proof-
from IN2 have "b ∈ Above C"
using AboveS_subset_Above[of C] by blast
with assms above_Above_trans
have "a ∈ Above C" by auto
(* *)
moreover
have "a ∉ C"
proof
assume *: "a ∈ C"
have 1: "(b,a) ∈ r"
using IN1 above_def[of b] by auto
have "∀c ∈ C. b ≠ c ∧ (c,b) ∈ r"
using IN2 AboveS_def[of 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 auto
qed
lemma (in rel) aboveS_AboveS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
IN1: "a ∈ aboveS b" and IN2: "b ∈ AboveS C"
shows "a ∈ AboveS C"
proof-
from IN2 have "b ∈ Above C"
using AboveS_subset_Above[of C] by blast
with aboveS_Above_trans assms
show ?thesis by auto
qed
subsection {* Properties depending on more than one relation *}
abbreviation "under ≡ rel.under"
abbreviation "underS ≡ rel.underS"
abbreviation "Under ≡ rel.Under"
abbreviation "UnderS ≡ rel.UnderS"
abbreviation "above ≡ rel.above"
abbreviation "aboveS ≡ rel.aboveS"
abbreviation "Above ≡ rel.Above"
abbreviation "AboveS ≡ rel.AboveS"
lemma under_incr2:
"r ≤ r' ==> under r a ≤ under r' a"
unfolding rel.under_def by blast
lemma underS_incr2:
"r ≤ r' ==> underS r a ≤ underS r' a"
unfolding rel.underS_def by blast
lemma Under_incr:
"r ≤ r' ==> Under r A ≤ Under r A"
unfolding rel.Under_def by blast
lemma UnderS_incr:
"r ≤ r' ==> UnderS r A ≤ UnderS r A"
unfolding rel.UnderS_def by blast
lemma Under_incr_decr:
"[|r ≤ r'; A' ≤ A|] ==> Under r A ≤ Under r A'"
unfolding rel.Under_def by blast
lemma UnderS_incr_decr:
"[|r ≤ r'; A' ≤ A|] ==> UnderS r A ≤ UnderS r A'"
unfolding rel.UnderS_def by blast
lemma above_incr2:
"r ≤ r' ==> above r a ≤ above r' a"
unfolding rel.above_def by blast
lemma aboveS_incr2:
"r ≤ r' ==> aboveS r a ≤ aboveS r' a"
unfolding rel.aboveS_def by blast
lemma Above_incr:
"r ≤ r' ==> Above r A ≤ Above r A"
unfolding rel.Above_def by blast
lemma AboveS_incr:
"r ≤ r' ==> AboveS r A ≤ AboveS r A"
unfolding rel.AboveS_def by blast
lemma Above_incr_decr:
"[|r ≤ r'; A' ≤ A|] ==> Above r A ≤ Above r A'"
unfolding rel.Above_def by blast
lemma AboveS_incr_decr:
"[|r ≤ r'; A' ≤ A|] ==> AboveS r A ≤ AboveS r A'"
unfolding rel.AboveS_def by blast
end