(* 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 \<leadsto> r'
lemma Under_incr:
"r \<le> r' \<Longrightarrow> Under r A \<le> Under r A"
unfolding Under_def by blast
lemma UnderS_incr:
"r \<le> r' \<Longrightarrow> UnderS r A \<le> UnderS r A"
unfolding UnderS_def by blast
lemma Under_incr_decr:
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> Under r A \<le> Under r A'"
unfolding Under_def by blast
lemma UnderS_incr_decr:
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> UnderS r A \<le> 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 \<le> r' \<Longrightarrow> Above r A \<le> Above r A"
unfolding Above_def by blast
lemma AboveS_incr:
"r \<le> r' \<Longrightarrow> AboveS r A \<le> AboveS r A"
unfolding AboveS_def by blast
lemma Above_incr_decr:
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> Above r A \<le> Above r A'"
unfolding Above_def by blast
lemma AboveS_incr_decr:
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> AboveS r A \<le> AboveS r A'"
unfolding AboveS_def by blast
*)
end
