Quelle  Orders.thy

(*  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^\<noteq>^\<noteq> a b = (r a b ∧ a ≠ b)"

definition porder_on :: "'a set ==> ('a ==> 'a ==> bool) ==> bool"
  where "porder_on A r ⟷
    (∀a a'. r a a' ⟶ a ∈ A ∧ a' ∈ A) ∧ 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 : 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_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
  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^\<noteq>^\<noteq> a b ==> r a b ∧ a ≠ b"
by(simp add: irreflclp_def)

lemma irreflclpI [intro!]:
  "[ r a b; a ≠ b ] ==> r^\<noteq>^\<noteq> a b"
by(simp add: irreflclp_def)

lemma irreflclpE [elim!]:
  assumes "r^\<noteq>^\<noteq> 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:
  "[(∧a a'. r a a' ==> a ∈ A ∧ a' ∈ A); 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 "∀a a'. r a a' ⟶ a ∈ A ∧ a' ∈ A" "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"
        unfolding atomize_conj
        by (simp add: porder_on_def torder_on_def)
      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"
        unfolding atomize_conj
        by (metis porder_on_def s torder_on_def)
      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 ‹s u v› have "v ∈ B"
          by (metis porder_on_def s torder_on_def)
        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 ‹s u v› ‹s u' v'›
      have "u ∈ B" "v ∈ B" "u' ∈ B" "v' ∈ B"
        unfolding atomize_conj
        by (metis porder_on_def s torder_on_def)
      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"
  show "∧a a'. ?rs⁺⁺ a a' ==> a ∈ A ∧ a' ∈ A"
    using consist porder_on_def[of A r] porder_torder_tranclpE[of A r B s] r s
      subset by blast
  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"

  show "∧a a'. ?rt⁺⁺ a a' ==> a ∈ A ∧ a' ∈ A"
    by (smt (verit, del_insts) converse_tranclpE in_mono porder_on_def r s subset t
        torder_onE tranclp.cases)

  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"
      unfolding atomize_conj
      by (metis porder_on_def s torder_on_def)
    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
    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_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 (smt (verit, ccfv_SIG) IntI antisym_restrictPI porder_on_def
      refl_on_restrictPI restrictP_def trans_restrictPI)

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 semilattice_max_torder:
  assumes tot: "torder_on A r"
  shows "semilattice (max_torder r)"
proof -
  from tot have r_domain_range: "∀a a'. r a a' ⟶ a ∈ A ∧ a' ∈ A"
    and 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)

  have "{a. Domainp r a} = A"
    using r_domain_range
    by (metis (mono_tags, opaque_lifting) Domainp.simps local.refl mem_Collect_eq
        refl_onPD subset_antisym subset_iff)

  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 a ∈ A ∧ b ∈ A then
        if r a b then b else a else SOME a. a ∉ A)"
        by (auto simp add: max_torder_def "domain")

      show ?thesis
      proof (cases "x ∈ A"; cases "y ∈ A"; cases "z ∈ A")
        show "x ∈ A ==> y ∈ A ==> z ∈ A ==> ?thesis"
          using True
          by (simp add: *) (metis trans[THEN transpD] to[THEN total_onPD])
      next
        show "x ∈ A ==> y ∈ A ==> z ∉ A ==> ?thesis"
          using True
          by (simp add: *) (metis "*" someI_ex)
      next
        show "x ∈ A ==> y ∉ A ==> z ∈ A ==> ?thesis"
          using True
          by (simp add: *) (metis (no_types, lifting) "*" someI_ex)
      next
        show "x ∈ A ==> y ∉ A ==> z ∉ A ==> ?thesis"
          using True
          by (simp add: *) (metis (no_types, lifting) "*" max_torder_def someI_ex)
      next
        show "x ∉ A ==> y ∈ A ==> z ∈ A ==> ?thesis"
          using True
          by (simp add: *) (metis "*" someI_ex)
      next
        show "x ∉ A ==> y ∈ A ==> z ∉ A ==> ?thesis"
          using True
          by (simp add: * domain max_torder_def)
      next
        show "x ∉ A ==> y ∉ A ==> z ∈ A ==> ?thesis"
          using True
          by (simp add: *) (metis (no_types, lifting) "*" max_torder_def some_eq_imp)
      next
        show "x ∉ A ==> y ∉ A ==> z ∉ A ==> ?thesis"
          using True
          by (simp add: * domain max_torder_def)
      qed
    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 r_domain_range: "∀a a'. r a a' ⟶ a ∈ A ∧ a' ∈ A"
    and 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)
  have "{a. Domainp r a} = A"
    using r_domain_range
    by (metis (mono_tags, lifting) Domainp.simps local.refl mem_Collect_eq
        refl_onPD subset_antisym subset_iff)
  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 (smt (verit, ccfv_threshold) Domainp.simps mem_Collect_eq porder_on_def
        refl_onPD subset_antisym subset_iff torder_onE)
  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