Theory Orders

(*  Title:      JinjaThreads/MM/Orders.thy
    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"
by(simp add: irreflclp_def)

lemma irreflclpI [intro!]:
  "⟦ r a b; a ≠ b ⟧ ⟹ r⇧≠⇧≠ a b"
by(simp add: irreflclp_def)

lemma irreflclpE [elim!]:
  assumes "r⇧≠⇧≠ a b"
  obtains "r a b" "a ≠ b"
using assms by(simp add: irreflclp_def)

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:
  "order_consistent r s ⟹ order_consistent s r"
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)
    with False show ?thesis by(contradiction)
  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)"
by(simp add: restrictP_def[abs_def])

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)"
by(simp add: refl_on_restrictPI)

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)"
by(simp add: porder_on_restrictPI)

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)"
by(simp add: total_on_restrictPI)

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)"
by(simp add: torder_on_restrictPI)

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"
by(simp add: restrictP_subsume1)

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 "semilattice (max_torder r)"
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)"
        by (auto simp add: max_torder_def)
      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_idem)
        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"
      by (simp add: max_torder_def)
  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:
  "semilattice_set (max_torder r)"
  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
    "semilattice_set.F (max_torder r) = Max_torder r"
    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
    "semilattice_set.F (max_torder r) = Max_torder r"
    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) ⟷ (∃a∈B. r x a)"
proof -
  interpret Max_torder: semilattice_set "max_torder r"
  rewrites
    "semilattice_set.F (max_torder r) = Max_torder r"
    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"
by(simp add: fun_eq_iff)

lemma inv_into_id [simp]: "a ∈ A ⟹ inv_into A id a = a"
by (metis f_inv_into_f id_apply image_id)

end