# Theory Orders

Author:     Andreas Lochbihler
*)

section ‹Orders as predicates›

theory Orders
imports
Main
begin

subsection ‹Preliminaries›

text ‹transfer @{term "refl_on"} et al. from @{theory HOL.Relation} to predicates›

abbreviation refl_onP :: "'a set  ('a  'a  bool)  bool"
where "refl_onP A r  refl_on A {(x, y). r x y}"

abbreviation reflP :: "('a  'a  bool)  bool"
where "reflP == refl_onP UNIV"

abbreviation symP :: "('a  'a  bool)  bool"
where "symP r  sym {(x, y). r x y}"

abbreviation total_onP :: "'a set  ('a  'a  bool)  bool"
where "total_onP A r  total_on A {(x, y). r x y}"

abbreviation irreflP :: "('a  'a  bool)  bool"
where "irreflP r == irrefl {(x, y). r x y}"

definition irreflclp :: "('a  'a  bool)  'a  'a  bool" ("_" [1000] 1000)
where "r a b = (r a b  a  b)"

definition porder_on :: "'a set  ('a  'a  bool)  bool"
where "porder_on A r  refl_onP A r  transp r  antisymp r"

definition torder_on :: "'a set  ('a  'a  bool)  bool"
where "torder_on A r  porder_on A r  total_onP A r"

definition order_consistent :: "('a  'a  bool)  ('a  'a  bool)  bool"
where "order_consistent r s  (a a'. r a a'  s a' a  a = a')"

definition restrictP :: "('a  'a  bool)  'a set  'a  'a  bool" (infixl "|`" 110)
where "(r |` A) a b  r a b  a  A  b  A"

definition inv_imageP :: "('a  'a  bool)  ('b  'a)  'b  'b  bool"
where [iff]: "inv_imageP r f a b  r (f a) (f b)"

lemma refl_onPI: "(a a'. r a a'  a  A  a'  A)  (a. a : A  r a a)  refl_onP A r"
by(rule refl_onI)(auto)

lemma refl_onPD: "refl_onP A r ==> a : A ==> r a a"
by(drule (1) refl_onD)(simp)

lemma refl_onPD1: "refl_onP A r ==> r a b ==> a : A"
by(erule refl_onD1)(simp)

lemma refl_onPD2: "refl_onP A r ==> r a b ==> b : A"
by(erule refl_onD2)(simp)

lemma refl_onP_Int: "refl_onP A r ==> refl_onP B s ==> refl_onP (A  B) (λa a'. r a a'  s a a')"
by(drule (1) refl_on_Int)(simp add: split_def inf_fun_def inf_set_def)

lemma refl_onP_Un: "refl_onP A r ==> refl_onP B s ==> refl_onP (A  B) (λa a'. r a a'  s a a')"
by(drule (1) refl_on_Un)(simp add: split_def sup_fun_def sup_set_def)

lemma refl_onP_empty[simp]: "refl_onP {} (λa a'. False)"
unfolding split_def by simp

lemma refl_onP_tranclp:
assumes "refl_onP A r"
shows "refl_onP A r^++"
proof(rule refl_onPI)
fix a a'
assume "r^++ a a'"
thus "a  A  a'  A"
by(induct)(blast intro: refl_onPD1[OF assms] refl_onPD2[OF assms])+
next
fix a
assume "a  A"
from refl_onPD[OF assms this] show "r^++ a a" ..
qed

lemma irreflPI: "(a. ¬ r a a)  irreflP r"
unfolding irrefl_def by blast

lemma irreflPE:
assumes "irreflP r"
obtains "a. ¬ r a a"
using assms unfolding irrefl_def by blast

lemma irreflPD: " irreflP r; r a a   False"
unfolding irrefl_def by blast

lemma irreflclpD:
"r a b  r a b  a  b"

lemma irreflclpI [intro!]:
" r a b; a  b   r a b"

lemma irreflclpE [elim!]:
assumes "r a b"
obtains "r a b" "a  b"

lemma transPI: "(x y z.  r x y; r y z   r x z)  transp r"
by (fact transpI)

lemma transPD: "transp r; r x y; r y z   r x z"
by (fact transpD)

lemma transP_tranclp: "transp r^++"
by (fact trans_trancl [to_pred])

lemma antisymPI: "(x y.  r x y; r y x   x = y)  antisymp r"
by (fact antisympI)

lemma antisymPD: " antisymp r; r a b; r b a   a = b"
by (fact antisympD)

lemma antisym_subset:
" antisymp r; a a'. s a a'  r a a'   antisymp s"
by (blast intro: antisymp_less_eq [of s r])

lemma symPI: "(x y. r x y  r y x)  symP r"
by(rule symI)(blast)

lemma symPD: " symP r; r x y   r y x"
by(blast dest: symD)

subsection ‹Easy properties›

lemma porder_onI:
" refl_onP A r; antisymp r; transp r   porder_on A r"
unfolding porder_on_def by blast

lemma porder_onE:
assumes "porder_on A r"
obtains "refl_onP A r" "antisymp r" "transp r"
using assms unfolding porder_on_def by blast

lemma torder_onI:
" porder_on A r; total_onP A r   torder_on A r"
unfolding torder_on_def by blast

lemma torder_onE:
assumes "torder_on A r"
obtains "porder_on A r" "total_onP A r"
using assms unfolding torder_on_def by blast

lemma total_onI:
"(x y.  x  A; y  A   (x, y)  r  x = y  (y, x)  r)  total_on A r"
unfolding total_on_def by blast

lemma total_onPI:
"(x y.  x  A; y  A   r x y  x = y  r y x)  total_onP A r"
by(rule total_onI) simp

lemma total_onD:
" total_on A r; x  A; y  A   (x, y)  r  x = y  (y, x)  r"
unfolding total_on_def by blast

lemma total_onPD:
" total_onP A r; x  A; y  A   r x y  x = y  r y x"
by(drule (2) total_onD) blast

subsection ‹Order consistency›

lemma order_consistentI:
"(a a'.  r a a'; s a' a   a = a')  order_consistent r s"
unfolding order_consistent_def by blast

lemma order_consistentD:
" order_consistent r s; r a a'; s a' a   a = a'"
unfolding order_consistent_def by blast

lemma order_consistent_subset:
" order_consistent r s; a a'. r' a a'  r a a'; a a'. s' a a'  s a a'   order_consistent r' s'"
by(blast intro: order_consistentI order_consistentD)

lemma order_consistent_sym:

by(blast intro: order_consistentI dest: order_consistentD)

lemma antisym_order_consistent_self:
"antisymp r  order_consistent r r"
by(rule order_consistentI)(erule antisympD, simp_all)

lemma total_on_refl_on_consistent_into:
assumes r: "total_onP A r" "refl_onP A r"
and consist: "order_consistent r s"
and x: "x  A" and y: "y  A" and s: "s x y"
shows "r x y"
proof(cases "x = y")
case True
with r x y show ?thesis by(blast intro: refl_onPD)
next
case False
with r x y have "r x y  r y x" by(blast dest: total_onD)
thus ?thesis
proof
assume "r y x"
with s consist have "x = y" by(blast dest: order_consistentD)
qed
qed

lemma porder_torder_tranclpE [consumes 5, case_names base step]:
assumes r: "porder_on A r"
and s: "torder_on B s"
and consist: "order_consistent r s"
and B_subset_A: "B  A"
and trancl: "(λa b. r a b  s a b)^++ x y"
obtains "r x y"
| u v where "r x u" "s u v" "r v y"
proof(atomize_elim)
from r have "refl_onP A r" "transp r" by(blast elim: porder_onE)+
from s have "refl_onP B s" "total_onP B s" "transp s"
by(blast elim: torder_onE porder_onE)+

from trancl show "r x y  (u v. r x u  s u v  r v y)"
proof(induct)
case (base y)
thus ?case
proof
assume "s x y"
with s have "x  B" "y  B"
by(blast elim: torder_onE porder_onE dest: refl_onPD1 refl_onPD2)+
with B_subset_A have "x  A" "y  A" by blast+
with refl_onPD[OF refl_onP A r, of x] refl_onPD[OF refl_onP A r, of y] s x y
show ?thesis by(iprover)
next
assume "r x y"
thus ?thesis ..
qed
next
case (step y z)
note IH = r x y  (u v. r x u  s u v  r v y)
from r y z  s y z show ?case
proof
assume "s y z"
with refl_onP B s have "y  B" "z  B"
by(blast dest: refl_onPD2 refl_onPD1)+
from IH show ?thesis
proof
assume "r x y"
moreover from z  B B_subset_A r have "r z z"
by(blast elim: porder_onE dest: refl_onPD)
ultimately show ?thesis using s y z by blast
next
assume "u v. r x u  s u v  r v y"
then obtain u v where "r x u" "s u v" "r v y" by blast
from refl_onP B s s u v have "v  B" by(rule refl_onPD2)
with total_onP B s refl_onP B s order_consistent_sym[OF consist]
have "s v y" using y  B r v y
by(rule total_on_refl_on_consistent_into)
with transp s have "s v z" using s y z by(rule transPD)
with transp s s u v have "s u z" by(rule transPD)
moreover from z  B B_subset_A have "z  A" ..
with refl_onP A r have "r z z" by(rule refl_onPD)
ultimately show ?thesis using r x u by blast
qed
next
assume "r y z"
with IH show ?thesis
by(blast intro: transPD[OF transp r])
qed
qed
qed

lemma torder_on_porder_on_consistent_tranclp_antisym:
assumes r: "porder_on A r"
and s: "torder_on B s"
and consist: "order_consistent r s"
and B_subset_A: "B  A"
shows "antisymp (λx y. r x y  s x y)^++"
proof(rule antisymPI)
fix x y
let ?rs = "λx y. r x y  s x y"
assume "?rs^++ x y" "?rs^++ y x"
from r have "antisymp r" "transp r" by(blast elim: porder_onE)+
from s have "total_onP B s" "refl_onP B s" "transp s" "antisymp s"
by(blast elim: torder_onE porder_onE)+

from r s consist B_subset_A ?rs^++ x y
show "x = y"
proof(cases rule: porder_torder_tranclpE)
case base
from r s consist B_subset_A ?rs^++ y x
show ?thesis
proof(cases rule: porder_torder_tranclpE)
case base
with antisymp r r x y show ?thesis by(rule antisymPD)
next
case (step u v)
from r v x r x y r y u have "r v u" by(blast intro: transPD[OF transp r])
with consist have "v = u" using s u v by(rule order_consistentD)
with r y u r v x have "r y x" by(blast intro: transPD[OF transp r])
with r x y show ?thesis by(rule antisymPD[OF antisymp r])
qed
next
case (step u v)
from r s consist B_subset_A ?rs^++ y x
show ?thesis
proof(cases rule: porder_torder_tranclpE)
case base
from r v y r y x r x u have "r v u" by(blast intro: transPD[OF transp r])
with order_consistent_sym[OF consist] s u v
have "u = v" by(rule order_consistentD)
with r v y r x u have "r x y" by(blast intro: transPD[OF transp r])
thus ?thesis using r y x by(rule antisymPD[OF antisymp r])
next
case (step u' v')
note r_into_s = total_on_refl_on_consistent_into[OF total_onP B s refl_onP B s order_consistent_sym[OF consist]]
from refl_onP B s s u v s u' v'
have "u  B" "v  B" "u'  B" "v'  B" by(blast dest: refl_onPD1 refl_onPD2)+
from r v' x r x u have "r v' u" by(rule transPD[OF transp r])
with v'  B u  B have "s v' u" by(rule r_into_s)
also note s u v
also (transPD[OF transp s])
from r v y r y u' have "r v u'" by(rule transPD[OF transp r])
with v  B u'  B have "s v u'" by(rule r_into_s)
finally (transPD[OF transp s])
have "v' = u'" using s u' v' by(rule antisymPD[OF antisymp s])
moreover with s v u' s v' u have "s v u" by(blast intro: transPD[OF transp s])
with s u v have "u = v" by(rule antisymPD[OF antisymp s])
ultimately have "r x y" "r y x" using r x u r v y r y u' r v' x
by(blast intro: transPD[OF transp r])+
thus ?thesis by(rule antisymPD[OF antisymp r])
qed
qed
qed

lemma porder_on_torder_on_tranclp_porder_onI:
assumes r: "porder_on A r"
and s: "torder_on B s"
and consist: "order_consistent r s"
and subset: "B  A"
shows "porder_on A (λa b. r a b  s a b)^++"
proof(rule porder_onI)
let ?rs = "λa b. r a b  s a b"
from r have "refl_onP A r" by(rule porder_onE)
moreover from s have "refl_onP B s" by(blast elim: torder_onE porder_onE)
ultimately have "refl_onP (A  B) ?rs" by(rule refl_onP_Un)
also from subset have "A  B = A" by blast
finally show "refl_onP A ?rs^++" by(rule refl_onP_tranclp)

show "transp ?rs^++" by(rule transP_tranclp)

from r s consist subset show "antisymp ?rs^++"
by (rule torder_on_porder_on_consistent_tranclp_antisym)
qed

lemma porder_on_sub_torder_on_tranclp_porder_onI:
assumes r: "porder_on A r"
and s: "torder_on B s"
and consist: "order_consistent r s"
and t: "x y. t x y  s x y"
and subset: "B  A"
shows "porder_on A (λx y. r x y  t x y)^++"
proof(rule porder_onI)
let ?rt = "λx y. r x y  t x y"
let ?rs = "λx y. r x y  s x y"
from r s consist subset have "antisymp ?rs^++"
by(rule torder_on_porder_on_consistent_tranclp_antisym)
thus "antisymp ?rt^++"
proof(rule antisym_subset)
fix x y
assume "?rt^++ x y" thus "?rs^++ x y"
by(induct)(blast intro: tranclp.r_into_trancl t tranclp.trancl_into_trancl t)+
qed

from s have "refl_onP B s" by(blast elim: porder_onE torder_onE)
{ fix x y
assume "t x y"
hence "s x y" by(rule t)
hence "x  B" "y  B"
by(blast dest: refl_onPD1[OF refl_onP B s] refl_onPD2[OF refl_onP B s])+
with subset have "x  A" "y  A" by blast+ }
note t_reflD = this

from r have "refl_onP A r" by(rule porder_onE)
show "refl_onP A ?rt^++"
proof(rule refl_onPI)
fix a a'
assume "?rt^++ a a'"
thus "a  A  a'  A"
by(induct)(auto dest: refl_onPD1[OF refl_onP A r] refl_onPD2[OF refl_onP A r] t_reflD)
next
fix a
assume "a  A"
with refl_onP A r have "r a a" by(rule refl_onPD)
thus "?rt^++ a a" by(blast intro: tranclp.r_into_trancl)
qed

show "transp ?rt^++" by(rule transP_tranclp)
qed

subsection ‹Order restrictions›

lemma restrictPI [intro!, simp]:
" r a b; a  A; b  A   (r |` A) a b"
unfolding restrictP_def by simp

lemma restrictPE [elim!]:
assumes "(r |` A) a b"
obtains "r a b" "a  A" "b  A"
using assms unfolding restrictP_def by simp

lemma restrictP_empty [simp]: "R |` {} = (λ_ _. False)"

lemma refl_on_restrictPI:
"refl_onP A r  refl_onP (A  B) (r |` B)"
by(rule refl_onPI)(blast dest: refl_onPD1 refl_onPD2 refl_onPD)+

lemma refl_on_restrictPI':
" refl_onP A r; B = A  C   refl_onP B (r |` C)"

lemma antisym_restrictPI:
"antisymp r  antisymp (r |` A)"
by(rule antisymPI)(blast dest: antisymPD)

lemma trans_restrictPI:
"transp r  transp (r |` A)"
by(rule transPI)(blast dest: transPD)

lemma porder_on_restrictPI:
"porder_on A r  porder_on (A  B) (r |` B)"
by(blast elim: porder_onE intro: refl_on_restrictPI antisym_restrictPI trans_restrictPI porder_onI)

lemma porder_on_restrictPI':
" porder_on A r; B = A  C   porder_on B (r |` C)"

lemma total_on_restrictPI:
"total_onP A r  total_onP (A  B) (r |` B)"
by(blast intro: total_onPI dest: total_onPD)

lemma total_on_restrictPI':
" total_onP A r; B = A  C   total_onP B (r |` C)"

lemma torder_on_restrictPI:
"torder_on A r  torder_on (A  B) (r |` B)"
by(blast elim: torder_onE intro: torder_onI porder_on_restrictPI total_on_restrictPI)

lemma torder_on_restrictPI':
" torder_on A r; B = A  C   torder_on B (r |` C)"

lemma restrictP_commute:
fixes r :: "'a  'a  bool"
shows "r |` A |` B = r |` B |` A"
by(blast intro!: ext)

lemma restrictP_subsume1:
fixes r :: "'a  'a  bool"
assumes "A  B"
shows "r |` A |` B = r |` A"
using assms by(blast intro!: ext)

lemma restrictP_subsume2:
fixes r :: "'a  'a  bool"
assumes "B  A"
shows "r |` A |` B = r |` B"
using assms by(blast intro!: ext)

lemma restrictP_idem [simp]:
fixes r :: "'a  'a  bool"
shows "r |` A |` A = r |` A"

subsection ‹Maximal elements w.r.t. a total order›

definition max_torder :: "('a  'a  bool)  'a  'a  'a"
where "max_torder r a b = (if Domainp r a  Domainp r b then if r a b then b else a
else if a = b then a else SOME a. ¬ Domainp r a)"

lemma refl_on_DomainD: "refl_on A r  A = Domain r"
by(auto simp add: Domain_unfold dest: refl_onD refl_onD1)

lemma refl_onP_DomainPD: "refl_onP A r  A = {a. Domainp r a}"
by(drule refl_on_DomainD) auto

lemma semilattice_max_torder:
assumes tot: "torder_on A r"
shows
proof -
from tot have as: "antisymp r"
and to: "total_onP A r"
and trans: "transp r"
and refl: "refl_onP A r"
by(auto elim: torder_onE porder_onE)
from refl have "{a. Domainp r a} = A" by (rule refl_onP_DomainPD[symmetric])
from this [symmetric] have "domain": "a. Domainp r a  a  A" by simp
show ?thesis
proof
fix x y z
show "max_torder r (max_torder r x y) z = max_torder r x (max_torder r y z)"
proof (cases "x  y  x  z  y  z")
case True
have *: "a b. a  b  max_torder r a b = (if Domainp r a  Domainp r b then
if r a b then b else a else SOME a. ¬ Domainp r a)"
with True show ?thesis
apply (simp only: max_torder_def "domain")
apply (auto split!: if_splits)
apply (blast dest: total_onPD [OF to] transPD [OF trans] antisymPD [OF as] refl_onPD1 [OF refl] refl_onPD2 [OF refl] someI [where P="λa. a  A"])+
done
next
have max_torder_idem: "a. max_torder r a a = a" by (simp add: max_torder_def)
case False then show ?thesis
apply (auto simp add: max_torder_def "domain" dest: someI [where P="λa. a  A"])
done
qed
next
fix x y
show "max_torder r x y = max_torder r y x"
by (auto simp add: max_torder_def "domain" dest: total_onPD [OF to] antisymPD [OF as])
next
fix x
show "max_torder r x x = x"
qed
qed

lemma max_torder_ge_conv_disj:
assumes tot: "torder_on A r" and x: "x  A" and y: "y  A"
shows "r z (max_torder r x y)  r z x  r z y"
proof -
from tot have as: "antisymp r"
and to: "total_onP A r"
and trans: "transp r"
and refl: "refl_onP A r"
by(auto elim: torder_onE porder_onE)
from refl have "{a. Domainp r a} = A" by (rule refl_onP_DomainPD[symmetric])
from this [symmetric] have "domain": "a. Domainp r a  a  A" by simp
show ?thesis using x y
by(simp add: max_torder_def "domain")(blast dest: total_onPD[OF to] transPD[OF trans])
qed

definition Max_torder :: "('a  'a  bool)  'a set  'a"
where
"Max_torder r = semilattice_set.F (max_torder r)"

context
fixes A r
assumes tot: "torder_on A r"
begin

lemma semilattice_set:

by (rule semilattice_set.intro, rule semilattice_max_torder) (fact tot)

lemma domain:
"Domainp r a  a  A"
proof -
from tot have "{a. Domainp r a} = A"
by (auto elim: torder_onE porder_onE dest: refl_onP_DomainPD [symmetric])
from this [symmetric] show ?thesis by simp
qed

lemma Max_torder_in_Domain:
assumes B: "finite B" "B  {}" "B  A"
shows "Max_torder r B  A"
proof -
interpret Max_torder: semilattice_set "max_torder r"
rewrites

by (fact semilattice_set Max_torder_def [symmetric])+
show ?thesis using B
by (induct rule: finite_ne_induct) (simp_all add: max_torder_def "domain")
qed

lemma Max_torder_in_set:
assumes B: "finite B" "B  {}" "B  A"
shows "Max_torder r B  B"
proof -
interpret Max_torder: semilattice_set "max_torder r"
rewrites

by (fact semilattice_set Max_torder_def [symmetric])+
show ?thesis using B
by (induct rule: finite_ne_induct) (auto simp add: max_torder_def "domain")
qed

lemma Max_torder_above_iff:
assumes B: "finite B" "B  {}" "B  A"
shows "r x (Max_torder r B)  (aB. r x a)"
proof -
interpret Max_torder: semilattice_set "max_torder r"
rewrites

by (fact semilattice_set Max_torder_def [symmetric])+
from B show ?thesis
by (induct rule: finite_ne_induct) (simp_all add: max_torder_ge_conv_disj [OF tot] Max_torder_in_Domain)
qed

end

lemma Max_torder_above:
assumes tot: "torder_on A r"
and "finite B" "a  B" "B  A"
shows "r a (Max_torder r B)"
proof -
from tot have refl: "refl_onP A r" by(auto elim: torder_onE porder_onE)
with a  B B  A have "r a a" by(blast dest: refl_onPD[OF refl])
from a  B have "B  {}" by auto
from Max_torder_above_iff [OF tot finite B this B  A, of a] r a a a  B
show ?thesis by blast
qed

lemma inv_imageP_id [simp]: "inv_imageP R id = R"