# Theory Order_Relation

theory Order_Relation
imports Wfrec
(*  Title:      HOL/Order_Relation.thy
Author:     Tobias Nipkow
Author:     Andrei Popescu, TU Muenchen
*)

section ‹Orders as Relations›

theory Order_Relation
imports Wfrec
begin

subsection ‹Orders on a set›

definition "preorder_on A r ≡ refl_on A r ∧ trans r"

definition "partial_order_on A r ≡ preorder_on A r ∧ antisym r"

definition "linear_order_on A r ≡ partial_order_on A r ∧ total_on A r"

definition "strict_linear_order_on A r ≡ trans r ∧ irrefl r ∧ total_on A r"

definition "well_order_on A r ≡ linear_order_on A r ∧ wf(r - Id)"

lemmas order_on_defs =
preorder_on_def partial_order_on_def linear_order_on_def
strict_linear_order_on_def well_order_on_def

lemma preorder_on_empty[simp]: "preorder_on {} {}"

lemma partial_order_on_empty[simp]: "partial_order_on {} {}"

lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"

lemma well_order_on_empty[simp]: "well_order_on {} {}"

lemma preorder_on_converse[simp]: "preorder_on A (r¯) = preorder_on A r"

lemma partial_order_on_converse[simp]: "partial_order_on A (r¯) = partial_order_on A r"

lemma linear_order_on_converse[simp]: "linear_order_on A (r¯) = linear_order_on A r"

lemma strict_linear_order_on_diff_Id: "linear_order_on A r ⟹ strict_linear_order_on A (r - Id)"

lemma linear_order_on_singleton [simp]: "linear_order_on {x} {(x, x)}"

lemma linear_order_on_acyclic:
assumes "linear_order_on A r"
shows "acyclic (r - Id)"
using strict_linear_order_on_diff_Id[OF assms]
by (auto simp add: acyclic_irrefl strict_linear_order_on_def)

lemma linear_order_on_well_order_on:
assumes "finite r"
shows "linear_order_on A r ⟷ well_order_on A r"
unfolding well_order_on_def
using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast

subsection ‹Orders on the field›

abbreviation "Refl r ≡ refl_on (Field r) r"

abbreviation "Preorder r ≡ preorder_on (Field r) r"

abbreviation "Partial_order r ≡ partial_order_on (Field r) r"

abbreviation "Total r ≡ total_on (Field r) r"

abbreviation "Linear_order r ≡ linear_order_on (Field r) r"

abbreviation "Well_order r ≡ well_order_on (Field r) r"

lemma subset_Image_Image_iff:
"Preorder r ⟹ A ⊆ Field r ⟹ B ⊆ Field r ⟹
r `` A ⊆ r `` B ⟷ (∀a∈A.∃b∈B. (b, a) ∈ r)"
apply (simp add: preorder_on_def refl_on_def Image_def subset_eq)
apply (simp only: trans_def)
apply fast
done

lemma subset_Image1_Image1_iff:
"Preorder r ⟹ a ∈ Field r ⟹ b ∈ Field r ⟹ r `` {a} ⊆ r `` {b} ⟷ (b, a) ∈ r"

lemma Refl_antisym_eq_Image1_Image1_iff:
assumes "Refl r"
and as: "antisym r"
and abf: "a ∈ Field r" "b ∈ Field r"
shows "r `` {a} = r `` {b} ⟷ a = b"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
then have *: "⋀x. (a, x) ∈ r ⟷ (b, x) ∈ r"
have "(a, a) ∈ r" "(b, b) ∈ r" using ‹Refl r› abf by (simp_all add: refl_on_def)
then have "(a, b) ∈ r" "(b, a) ∈ r" using *[of a] *[of b] by simp_all
then show ?rhs
using ‹antisym r›[unfolded antisym_def] by blast
next
assume ?rhs
then show ?lhs by fast
qed

lemma Partial_order_eq_Image1_Image1_iff:
"Partial_order r ⟹ a ∈ Field r ⟹ b ∈ Field r ⟹ r `` {a} = r `` {b} ⟷ a = b"
by (auto simp: order_on_defs Refl_antisym_eq_Image1_Image1_iff)

lemma Total_Id_Field:
assumes "Total r"
and not_Id: "¬ r ⊆ Id"
shows "Field r = Field (r - Id)"
using mono_Field[of "r - Id" r] Diff_subset[of r Id]
proof auto
fix a assume *: "a ∈ Field r"
from not_Id have "r ≠ {}" by fast
with not_Id obtain b and c where "b ≠ c ∧ (b,c) ∈ r" by auto
then have "b ≠ c ∧ {b, c} ⊆ Field r" by (auto simp: Field_def)
with * obtain d where "d ∈ Field r" "d ≠ a" by auto
with * ‹Total r› have "(a, d) ∈ r ∨ (d, a) ∈ r" by (simp add: total_on_def)
with ‹d ≠ a› show "a ∈ Field (r - Id)" unfolding Field_def by blast
qed

subsection ‹Orders on a type›

abbreviation "strict_linear_order ≡ strict_linear_order_on UNIV"

abbreviation "linear_order ≡ linear_order_on UNIV"

abbreviation "well_order ≡ well_order_on UNIV"

subsection ‹Order-like relations›

text ‹
In this subsection, 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. We also further define upper and lower bounds operators.
›

subsubsection ‹Auxiliaries›

lemma refl_on_domain: "refl_on A r ⟹ (a, b) ∈ r ⟹ a ∈ A ∧ b ∈ A"

corollary well_order_on_domain: "well_order_on A r ⟹ (a, b) ∈ r ⟹ a ∈ A ∧ b ∈ A"
by (auto 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 [of A] by auto

lemma Total_subset_Id:
assumes "Total r"
and "r ⊆ Id"
shows "r = {} ∨ (∃a. r = {(a, a)})"
proof -
have "∃a. r = {(a, a)}" if "r ≠ {}"
proof -
from that obtain a b where ab: "(a, b) ∈ r" by fast
with ‹r ⊆ Id› have "a = b" by blast
with ab have aa: "(a, a) ∈ r" by simp
have "a = c ∧ a = d" if "(c, d) ∈ r" for c d
proof -
from that have "{a, c, d} ⊆ Field r"
using ab unfolding Field_def by blast
then have "((a, c) ∈ r ∨ (c, a) ∈ r ∨ a = c) ∧ ((a, d) ∈ r ∨ (d, a) ∈ r ∨ a = d)"
using ‹Total r› unfolding total_on_def by blast
with ‹r ⊆ Id› show ?thesis by blast
qed
then have "r ⊆ {(a, a)}" by auto
with aa show ?thesis by blast
qed
then show ?thesis by blast
qed

lemma Linear_order_in_diff_Id:
assumes "Linear_order r"
and "a ∈ Field r"
and "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

subsubsection ‹The upper and lower bounds operators›

text ‹
Here we define upper (``above") and lower (``below") bounds operators. We
think of ‹r› as a ∗‹non-strict› relation. The suffix ‹S› at the names of
some operators indicates that the bounds are strict -- e.g., ‹underS a› is
the set of all strict lower bounds of ‹a› (w.r.t. ‹r›). Capitalization of
the first letter in the name reminds that the operator acts on sets, rather
than on individual elements.
›

definition under :: "'a rel ⇒ 'a ⇒ 'a set"
where "under r a ≡ {b. (b, a) ∈ r}"

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

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

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

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

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

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

definition AboveS :: "'a rel ⇒ 'a set ⇒ 'a set"
where "AboveS r A ≡ {b ∈ Field r. ∀a ∈ A. b ≠ a ∧ (a, b) ∈ r}"

definition ofilter :: "'a rel ⇒ 'a set ⇒ bool"
where "ofilter r A ≡ A ⊆ Field r ∧ (∀a ∈ A. under r a ⊆ A)"

text ‹
Note: In the definitions of ‹Above[S]› and ‹Under[S]›, we bounded
comprehension by ‹Field r› in order to properly cover the case of ‹A› being
empty.
›

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

lemma underS_notIn: "a ∉ underS r a"

lemma Refl_under_in: "Refl r ⟹ a ∈ Field r ⟹ a ∈ under r a"

lemma AboveS_disjoint: "A ∩ (AboveS r A) = {}"

lemma in_AboveS_underS: "a ∈ Field r ⟹ a ∈ AboveS r (underS r a)"
by (auto simp add: AboveS_def underS_def)

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

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

lemma under_Field: "under r a ⊆ Field r"
by (auto simp: under_def Field_def)

lemma underS_Field: "underS r a ⊆ Field r"
by (auto simp: underS_def Field_def)

lemma underS_Field2: "a ∈ Field r ⟹ underS r a ⊂ Field r"
using underS_notIn underS_Field by fast

lemma underS_Field3: "Field r ≠ {} ⟹ underS r a ⊂ Field r"
by (cases "a ∈ Field r") (auto simp: underS_Field2 underS_empty)

lemma AboveS_Field: "AboveS r A ⊆ Field r"
by (auto simp: AboveS_def Field_def)

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

lemma underS_incr:
assumes "trans r"
and "antisym r"
and ab: "(a, b) ∈ r"
shows "underS r a ⊆ underS r b"
unfolding underS_def
proof auto
assume *: "b ≠ a" and **: "(b, a) ∈ r"
with ‹antisym r› antisym_def[of r] ab show False
by blast
next
fix x assume "x ≠ a" "(x, a) ∈ r"
with ab ‹trans r› 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 r a ⊆ underS r b ⟷ (a, b) ∈ r"
(is "?lhs ⟷ ?rhs")
proof
assume ?rhs
with ‹Linear_order r› show ?lhs
next
assume *: ?lhs
have "(a, b) ∈ r" if "a = b"
using assms that by (simp add: order_on_defs refl_on_def)
moreover have False if "a ≠ b" "(b, a) ∈ r"
proof -
from that have "b ∈ underS r a" unfolding underS_def by blast
with * have "b ∈ underS r b" by blast
then show ?thesis by (simp add: underS_notIn)
qed
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 finite_Linear_order_induct[consumes 3, case_names step]:
assumes "Linear_order r"
and "x ∈ Field r"
and "finite r"
and step: "⋀x. x ∈ Field r ⟹ (⋀y. y ∈ aboveS r x ⟹ P y) ⟹ P x"
shows "P x"
using assms(2)
proof (induct rule: wf_induct[of "r¯ - Id"])
case 1
from assms(1,3) show "wf (r¯ - Id)"
using linear_order_on_well_order_on linear_order_on_converse
unfolding well_order_on_def by blast
next
case prems: (2 x)
show ?case
by (rule step) (use prems in ‹auto simp: aboveS_def intro: FieldI2›)
qed

subsection ‹Variations on Well-Founded Relations›

text ‹
This subsection contains some variations of the results from @{theory Wellfounded}:
▪ means for slightly more direct definitions by well-founded recursion;
▪ variations of well-founded induction;
▪ means for proving a linear order to be a well-order.
›

subsubsection ‹Characterizations of well-foundedness›

text ‹
A transitive relation is well-founded iff it is ``locally'' well-founded,
i.e., iff its restriction to the lower bounds of of any element is
well-founded.
›

lemma trans_wf_iff:
assumes "trans r"
shows "wf r ⟷ (∀a. wf (r ∩ (r¯``{a} × r¯``{a})))"
proof -
define R where "R a = r ∩ (r¯``{a} × r¯``{a})" for a
have "wf (R a)" if "wf r" for a
using that R_def wf_subset[of r "R a"] by auto
moreover
have "wf r" if *: "∀a. wf(R a)"
unfolding wf_def
proof clarify
fix phi a
assume **: "∀a. (∀b. (b, a) ∈ r ⟶ phi b) ⟶ phi a"
define chi where "chi b ⟷ (b, a) ∈ r ⟶ phi b" for b
with * have "wf (R a)" by auto
then have "(∀b. (∀c. (c, b) ∈ R a ⟶ chi c) ⟶ chi b) ⟶ (∀b. chi b)"
unfolding wf_def by blast
also have "∀b. (∀c. (c, b) ∈ R a ⟶ chi c) ⟶ chi b"
proof (auto simp add: chi_def R_def)
fix b
assume "(b, a) ∈ r" and "∀c. (c, b) ∈ r ∧ (c, a) ∈ r ⟶ phi c"
then have "∀c. (c, b) ∈ r ⟶ phi c"
using assms trans_def[of r] by blast
with ** show "phi b" by blast
qed
finally have  "∀b. chi b" .
with ** chi_def show "phi a" by blast
qed
ultimately show ?thesis unfolding R_def by blast
qed

text‹A transitive relation is well-founded if all initial segments are finite.›
corollary wf_finite_segments:
assumes "irrefl r" and "trans r" and "⋀x. finite {y. (y, x) ∈ r}"
shows "wf (r)"
proof (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
fix a
have "trans (r ∩ ({x. (x, a) ∈ r} × {x. (x, a) ∈ r}))"
using assms unfolding trans_def Field_def by blast
then show "acyclic (r ∩ {x. (x, a) ∈ r} × {x. (x, a) ∈ r})"
using assms acyclic_def assms irrefl_def by fastforce
qed

text ‹The next lemma is a variation of ‹wf_eq_minimal› from Wellfounded,
allowing one to assume the set included in the field.›

lemma wf_eq_minimal2: "wf r ⟷ (∀A. A ⊆ Field r ∧ A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a', a) ∉ r))"
proof-
let ?phi = "λA. A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a',a) ∉ r)"
have "wf r ⟷ (∀A. ?phi A)"
apply (auto simp: ex_in_conv [THEN sym])
apply (erule wfE_min)
apply assumption
apply blast
apply (rule wfI_min)
apply fast
done
also have "(∀A. ?phi A) ⟷ (∀B ⊆ Field r. ?phi B)"
proof
assume "∀A. ?phi A"
then show "∀B ⊆ Field r. ?phi B" by simp
next
assume *: "∀B ⊆ Field r. ?phi B"
show "∀A. ?phi A"
proof clarify
fix A :: "'a set"
assume **: "A ≠ {}"
define B where "B = A ∩ Field r"
show "∃a ∈ A. ∀a' ∈ A. (a', a) ∉ r"
proof (cases "B = {}")
case True
with ** obtain a where a: "a ∈ A" "a ∉ Field r"
unfolding B_def by blast
with a have "∀a' ∈ A. (a',a) ∉ r"
unfolding Field_def by blast
with a show ?thesis by blast
next
case False
have "B ⊆ Field r" unfolding B_def by blast
with False * obtain a where a: "a ∈ B" "∀a' ∈ B. (a', a) ∉ r"
by blast
have "(a', a) ∉ r" if "a' ∈ A" for a'
proof
assume a'a: "(a', a) ∈ r"
with that have "a' ∈ B" unfolding B_def Field_def by blast
with a a'a show False by blast
qed
with a show ?thesis unfolding B_def by blast
qed
qed
qed
finally show ?thesis by blast
qed

subsubsection ‹Characterizations of well-foundedness›

text ‹
The next lemma and its corollary enable one to prove that a linear order is
a well-order in a way which is more standard than via well-foundedness of
the strict version of the relation.
›

lemma Linear_order_wf_diff_Id:
assumes "Linear_order r"
shows "wf (r - Id) ⟷ (∀A ⊆ Field r. A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r))"
proof (cases "r ⊆ Id")
case True
then have *: "r - Id = {}" by blast
have "wf (r - Id)" by (simp add: *)
moreover have "∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r"
if *: "A ⊆ Field r" and **: "A ≠ {}" for A
proof -
from ‹Linear_order r› True
obtain a where a: "r = {} ∨ r = {(a, a)}"
unfolding order_on_defs using Total_subset_Id [of r] by blast
with * ** have "A = {a} ∧ r = {(a, a)}"
unfolding Field_def by blast
with a show ?thesis by blast
qed
ultimately show ?thesis by blast
next
case False
with ‹Linear_order r› have Field: "Field r = Field (r - Id)"
unfolding order_on_defs using Total_Id_Field [of r] by blast
show ?thesis
proof
assume *: "wf (r - Id)"
show "∀A ⊆ Field r. A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r)"
proof clarify
fix A
assume **: "A ⊆ Field r" and ***: "A ≠ {}"
then have "∃a ∈ A. ∀a' ∈ A. (a',a) ∉ r - Id"
using Field * unfolding wf_eq_minimal2 by simp
moreover have "∀a ∈ A. ∀a' ∈ A. (a, a') ∈ r ⟷ (a', a) ∉ r - Id"
using Linear_order_in_diff_Id [OF ‹Linear_order r›] ** by blast
ultimately show "∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r" by blast
qed
next
assume *: "∀A ⊆ Field r. A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r)"
show "wf (r - Id)"
unfolding wf_eq_minimal2
proof clarify
fix A
assume **: "A ⊆ Field(r - Id)" and ***: "A ≠ {}"
then have "∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r"
using Field * by simp
moreover have "∀a ∈ A. ∀a' ∈ A. (a, a') ∈ r ⟷ (a', a) ∉ r - Id"
using Linear_order_in_diff_Id [OF ‹Linear_order r›] ** mono_Field[of "r - Id" r] by blast
ultimately show "∃a ∈ A. ∀a' ∈ A. (a',a) ∉ r - Id"
by blast
qed
qed
qed

corollary Linear_order_Well_order_iff:
"Linear_order r ⟹
Well_order r ⟷ (∀A ⊆ Field r. A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r))"
unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast

end