Theory Extend_Partial_Order

theory Extend_Partial_Order
imports Main
(* Title:      Containers/Extend_Partial_Order.thy
   Author:     Andreas Lochbihler, KIT *)

theory Extend_Partial_Order
imports Main
begin

section ‹Every partial order can be extended to a total order›

lemma ChainsD: "⟦ x ∈ C; C ∈ Chains r; y ∈ C ⟧ ⟹ (x, y) ∈ r ∨ (y, x) ∈ r"
by(simp add: Chains_def)

lemma Chains_Field: "⟦ C ∈ Chains r; x ∈ C ⟧ ⟹ x ∈ Field r"
by(auto simp add: Chains_def Field_def)

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 linear_order_imp_linorder: "linear_order {(A, B). leq A B} ⟹ class.linorder leq (λx y. leq x y ∧ ¬ leq y x)"
by(unfold_locales)(auto 4 4 simp add: linear_order_on_def partial_order_on_def preorder_on_def dest: refl_onD antisymD transD total_onD)

lemma (in linorder) linear_order: "linear_order {(A, B). A ≤ B}"
by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def total_on_def intro: refl_onI antisymI transI)


definition order_consistent :: "('a × 'a) set ⇒ ('a × 'a) set ⇒ bool"
where "order_consistent r s ⟷ (∀a a'. (a, a') ∈ r ⟶ (a', a) ∈ s ⟶ a = a')"

lemma order_consistent_sym:
  "order_consistent r s ⟹ order_consistent s r"
by(auto simp add: order_consistent_def)

lemma antisym_order_consistent_self:
  "antisym r ⟹ order_consistent r r"
by(auto simp add: order_consistent_def dest: antisymD)


lemma refl_on_trancl:
  assumes "refl_on A r"
  shows "refl_on A (r^+)"
proof(rule refl_onI, safe del: conjI)
  fix a b
  assume "(a, b) ∈ r^+"
  thus "a ∈ A ∧ b ∈ A"
    by induct(blast intro: refl_onD1[OF assms] refl_onD2[OF assms])+
qed(blast dest: refl_onD[OF assms])

lemma total_on_refl_on_consistent_into:
  assumes r: "total_on A r" "refl_on A r"
  and consist: "order_consistent r s"
  and x: "x ∈ A" and y: "y ∈ A" and s: "(x, y) ∈ s"
  shows "(x, y) ∈ r"
proof(cases "x = y")
  case False
  with r x y have "(x, y) ∈ r ∨ (y, x) ∈ r" unfolding total_on_def by blast
  thus ?thesis
  proof
    assume "(y, x) ∈ r"
    with s consist have "x = y" unfolding order_consistent_def by blast
    with False show ?thesis by contradiction
  qed
qed(blast intro: refl_onD r x y)

lemma porder_linorder_tranclpE [consumes 5, case_names base step]:
  assumes r: "partial_order_on A r"
  and s: "linear_order_on B s"
  and consist: "order_consistent r s"
  and B_subset_A: "B ⊆ A"
  and trancl: "(x, y) ∈ (r ∪ s)^+"
  obtains "(x, y) ∈ r"
        | u v where "(x, u) ∈ r" "(u, v) ∈ s" "(v, y) ∈ r"
proof(atomize_elim)
  from r have "refl_on A r" "trans r" by(simp_all add: partial_order_on_def preorder_on_def)
  from s have "refl_on B s" "total_on B s" "trans s"
    by(simp_all add: partial_order_on_def preorder_on_def linear_order_on_def)

  from trancl show "(x, y) ∈ r ∨ (∃u v. (x, u) ∈ r ∧ (u, v) ∈ s ∧ (v, y) ∈ r)"
  proof(induction)
    case (base y)
    thus ?case
    proof
      assume "(x, y) ∈ s"
      with ‹refl_on B s› have "x ∈ B" "y ∈ B"
        by(blast dest: refl_onD1 refl_onD2)+
      with B_subset_A have "x ∈ A" "y ∈ A" by blast+
      hence "(x, x) ∈ r" "(y, y) ∈ r"
        using ‹refl_on A r› by(blast intro: refl_onD)+
      with ‹(x, y) ∈ s› show ?thesis by blast
    qed(simp)
  next
    case (step y z)
    from ‹(y, z) ∈ r ∪ s› show ?case
    proof
      assume "(y, z) ∈ s"
      with ‹refl_on B s› have "y ∈ B" "z ∈ B"
        by(blast dest: refl_onD2 refl_onD1)+
      from step.IH show ?thesis
      proof
        assume "(x, y) ∈ r"
        moreover from ‹z ∈ B› B_subset_A ‹refl_on A r› 
        have "(z, z) ∈ r" by(blast dest: refl_onD)
        ultimately show ?thesis using ‹(y, z) ∈ s› by blast
      next
        assume "∃u v. (x, u) ∈ r ∧ (u, v) ∈ s ∧ (v, y) ∈ r"
        then obtain u v where "(x, u) ∈ r" "(u, v) ∈ s" "(v, y) ∈ r" by blast
        from ‹refl_on B s› ‹(u, v) ∈ s› have "v ∈ B" by(rule refl_onD2)
        with ‹total_on B s› ‹refl_on B s› order_consistent_sym[OF consist]
        have "(v, y) ∈ s" using ‹y ∈ B› ‹(v, y) ∈ r›
          by(rule total_on_refl_on_consistent_into)
        with ‹trans s› have "(v, z) ∈ s" using ‹(y, z) ∈ s› by(rule transD)
        with ‹trans s› ‹(u, v) ∈ s› have "(u, z) ∈ s" by(rule transD)
        moreover from ‹z ∈ B› B_subset_A have "z ∈ A" ..
        with ‹refl_on A r› have "(z, z) ∈ r" by(rule refl_onD)
        ultimately show ?thesis using ‹(x, u) ∈ r› by blast
      qed
    next
      assume "(y, z) ∈ r"
      with step.IH show ?thesis
        by(blast intro: transD[OF ‹trans r›])
    qed
  qed
qed

lemma porder_on_consistent_linorder_on_trancl_antisym:
  assumes r: "partial_order_on A r"
  and s: "linear_order_on B s"
  and consist: "order_consistent r s"
  and B_subset_A: "B ⊆ A"
  shows "antisym ((r ∪ s)^+)"
proof(rule antisymI)
  fix x y
  let ?rs = "(r ∪ s)^+"
  assume "(x, y) ∈ ?rs" "(y, x) ∈ ?rs"
  from r have "antisym r" "trans r" by(simp_all add: partial_order_on_def preorder_on_def)
  from s have "total_on B s" "refl_on B s" "trans s" "antisym s"
    by(simp_all add: partial_order_on_def preorder_on_def linear_order_on_def)

  from r s consist B_subset_A ‹(x, y) ∈ ?rs›
  show "x = y"
  proof(cases rule: porder_linorder_tranclpE)
    case base
    from r s consist B_subset_A ‹(y, x) ∈ ?rs›
    show ?thesis
    proof(cases rule: porder_linorder_tranclpE)
      case base
      with ‹antisym r› ‹(x, y) ∈ r› show ?thesis by(rule antisymD)
    next
      case (step u v)
      from ‹(v, x) ∈ r› ‹(x, y) ∈ r› ‹(y, u) ∈ r› have "(v, u) ∈ r"
        by(blast intro: transD[OF ‹trans r›])
      with consist have "v = u" using ‹(u, v) ∈ s› 
        by(simp add: order_consistent_def) 
      with ‹(y, u) ∈ r› ‹(v, x) ∈ r› have "(y, x) ∈ r"
        by(blast intro: transD[OF ‹trans r›])
      with ‹antisym r› ‹(x, y) ∈ r› show ?thesis by(rule antisymD)
    qed
  next
    case (step u v)
    from r s consist B_subset_A ‹(y, x) ∈ ?rs›
    show ?thesis
    proof(cases rule: porder_linorder_tranclpE)
      case base
      from ‹(v, y) ∈ r› ‹(y, x) ∈ r› ‹(x, u) ∈ r› have "(v, u) ∈ r"
        by(blast intro: transD[OF ‹trans r›])
      with consist ‹(u, v) ∈ s›
      have "u = v" by(auto simp add: order_consistent_def)
      with ‹(v, y) ∈ r› ‹(x, u) ∈ r› have "(x, y) ∈ r"
        by(blast intro: transD[OF ‹trans r›])
      with ‹antisym r› show ?thesis using ‹(y, x) ∈ r› by(rule antisymD)
    next
      case (step u' v')
      note r_into_s = total_on_refl_on_consistent_into[OF ‹total_on B s› ‹refl_on B s› order_consistent_sym[OF consist]]
      from ‹refl_on B s› ‹(u, v) ∈ s› ‹(u', v') ∈ s›
      have "u ∈ B" "v ∈ B" "u' ∈ B" "v' ∈ B" by(blast dest: refl_onD1 refl_onD2)+
      from ‹trans r› ‹(v', x) ∈ r› ‹(x, u) ∈ r› have "(v', u) ∈ r" by(rule transD)
      with ‹v' ∈ B› ‹u ∈ B› have "(v', u) ∈ s" by(rule r_into_s)
      also note ‹(u, v) ∈ s› also (transD[OF ‹trans s›])
      from ‹trans r› ‹(v, y) ∈ r› ‹(y, u') ∈ r› have "(v, u') ∈ r" by(rule transD)
      with ‹v ∈ B› ‹u' ∈ B› have "(v, u') ∈ s" by(rule r_into_s)
      finally (transD[OF ‹trans s›])
      have "v' = u'" using ‹(u', v') ∈ s› by(rule antisymD[OF ‹antisym s›])
      moreover with ‹(v, u') ∈ s› ‹(v', u) ∈ s› have "(v, u) ∈ s"
        by(blast intro: transD[OF ‹trans s›])
      with ‹antisym s› ‹(u, v) ∈ s› have "u = v" by(rule antisymD)
      ultimately have "(x, y) ∈ r" "(y, x) ∈ r"
        using ‹(x, u) ∈ r› ‹(v, y) ∈ r› ‹(y, u') ∈ r› ‹(v', x) ∈ r›
        by(blast intro: transD[OF ‹trans r›])+
      with ‹antisym r› show ?thesis by(rule antisymD)
    qed
  qed
qed

lemma porder_on_linorder_on_tranclp_porder_onI:
  assumes r: "partial_order_on A r"
  and s: "linear_order_on B s" 
  and consist: "order_consistent r s"
  and subset: "B ⊆ A"
  shows "partial_order_on A ((r ∪ s)^+)"
  unfolding partial_order_on_def preorder_on_def
proof(intro conjI)
  let ?rs = "r ∪ s"
  from r have "refl_on A r" by(simp add: partial_order_on_def preorder_on_def)
  moreover from s have "refl_on B s"
    by(simp add: linear_order_on_def partial_order_on_def preorder_on_def)
  ultimately have "refl_on (A ∪ B) ?rs" by(rule refl_on_Un)
  also from subset have "A ∪ B = A" by blast
  finally show "refl_on A (?rs^+)" by(rule refl_on_trancl)

  show "trans (?rs^+)" by(rule trans_trancl)

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

lemma porder_extend_to_linorder:
  assumes r: "partial_order_on A r"
  obtains s where "linear_order_on A s" "order_consistent r s"
proof(atomize_elim)
  define S where "S = {s. partial_order_on A s ∧ r ⊆ s}"
  from r have r_in_S: "r ∈ S" unfolding S_def by auto

  have "∃y∈S. ∀x∈S. y ⊆ x ⟶ x = y"
  proof(rule Zorn_Lemma2[rule_format])
    fix c
    assume "c ∈ chains S"
    hence "c ⊆ S" by(rule chainsD2)

    show "∃y∈S. ∀x∈c. x ⊆ y"
    proof(cases "c = {}")
      case True
      with r_in_S show ?thesis by blast
    next
      case False
      then obtain s where "s ∈ c" by blast
      hence s: "partial_order_on A s"
        and r_in_s: "r ⊆ s"
        using ‹c ⊆ S› unfolding S_def by blast+

      have "partial_order_on A (⋃c)"
        unfolding partial_order_on_def preorder_on_def
      proof(intro conjI)
        show "refl_on A (⋃c)"
        proof(rule refl_onI[OF subsetI])
          fix x
          assume "x ∈ ⋃c"
          then obtain X where "X ∈ c" and "x ∈ X" by blast
          from ‹X ∈ c› ‹c ⊆ S› have "X ∈ S" ..
          hence "partial_order_on A X" unfolding S_def by simp
          with ‹x ∈ X› show "x ∈ A × A"
            by(cases x)(auto simp add: partial_order_on_def preorder_on_def dest: refl_onD1 refl_onD2)
        next
          fix x
          assume "x ∈ A"
          with s have "(x, x) ∈ s" unfolding partial_order_on_def preorder_on_def
            by(blast dest: refl_onD)
          with ‹s ∈ c› show "(x, x) ∈ ⋃c" by(rule UnionI)
        qed

        show "antisym (⋃c)"
        proof(rule antisymI)
          fix x y
          assume "(x, y) ∈ ⋃c" "(y, x) ∈ ⋃c"
          then obtain X Y where "X ∈ c" "Y ∈ c" "(x, y) ∈ X" "(y, x) ∈ Y" by blast
          from ‹X ∈ c› ‹Y ∈ c› ‹c ⊆ S› have "antisym X" "antisym Y"
            unfolding S_def by(auto simp add: partial_order_on_def)
          moreover from ‹c ∈ chains S› ‹X ∈ c› ‹Y ∈ c› 
          have "X ⊆ Y ∨ Y ⊆ X" by(rule chainsD)
          ultimately show "x = y" using ‹(x, y) ∈ X› ‹(y, x) ∈ Y› 
            by(auto dest: antisymD)
        qed

        show "trans (⋃c)"
        proof(rule transI)
          fix x y z
          assume "(x, y) ∈ ⋃c" "(y, z) ∈ ⋃c"
          then obtain X Y where "X ∈ c" "Y ∈ c" "(x, y) ∈ X" "(y, z) ∈ Y" by blast
          from ‹X ∈ c› ‹Y ∈ c› ‹c ⊆ S› have "trans X" "trans Y"
            unfolding S_def by(auto simp add: partial_order_on_def preorder_on_def)
          from ‹c ∈ chains S› ‹X ∈ c› ‹Y ∈ c› 
          have "X ⊆ Y ∨ Y ⊆ X" by(rule chainsD)
          thus "(x, z) ∈ ⋃c"
          proof
            assume "X ⊆ Y"
            with ‹trans Y› ‹(x, y) ∈ X› ‹(y, z) ∈ Y›
            have "(x, z) ∈ Y" by(blast dest: transD)
            with ‹Y ∈ c› show ?thesis by(rule UnionI)
          next
            assume "Y ⊆ X"
            with ‹trans X› ‹(x, y) ∈ X› ‹(y, z) ∈ Y›
            have "(x, z) ∈ X" by(blast dest: transD)
            with ‹X ∈ c› show ?thesis by(rule UnionI)
          qed
        qed
      qed
      moreover
      have "r ⊆ ⋃c" using r_in_s ‹s ∈ c› by blast
      ultimately have "⋃c ∈ S" unfolding S_def by simp
      thus ?thesis by blast
    qed
  qed
  then obtain s where "s ∈ S" and y_max: "⋀t. ⟦ t ∈ S; s ⊆ t ⟧ ⟹ s = t" by blast

  have "partial_order_on A s" using ‹s ∈ S›
    unfolding S_def by simp
  moreover
  have r_in_s: "r ⊆ s" using ‹s ∈ S› unfolding S_def by blast

  have "total_on A s"
    unfolding total_on_def
  proof(intro strip)
    fix x y
    assume "x ∈ A" "y ∈ A" "x ≠ y" 
    show "(x, y) ∈ s ∨ (y, x) ∈ s"
    proof(rule ccontr)
      assume "¬ ?thesis"
      hence xy: "(x, y) ∉ s" "(y, x) ∉ s" by simp_all

      define s' where "s' = {(a, b). a = x ∧ (b = y ∨ b = x) ∨ a = y ∧ b = y}"
      let ?s' = "(s ∪ s')^+"
      note ‹partial_order_on A s›
      moreover have "linear_order_on {x, y} s'" unfolding s'_def
        by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def total_on_def intro: refl_onI transI antisymI)
      moreover have "order_consistent s s'"
        unfolding s'_def using xy unfolding order_consistent_def by blast
      moreover have "{x, y} ⊆ A" using ‹x ∈ A› ‹y ∈ A› by blast
      ultimately have "partial_order_on A ?s'"
        by(rule porder_on_linorder_on_tranclp_porder_onI)
      moreover have "r ⊆ ?s'" using r_in_s by auto
      ultimately have "?s' ∈ S" unfolding S_def by simp
      moreover have "s ⊆ ?s'" by auto
      ultimately have "s = ?s'" by(rule y_max)
      moreover have "(x, y) ∈ ?s'" by(auto simp add: s'_def)
      ultimately show False using ‹(x, y) ∉ s› by simp
    qed
  qed
  ultimately have "linear_order_on A s" by(simp add: linear_order_on_def)
  moreover have "order_consistent r s" unfolding order_consistent_def
  proof(intro strip)
    fix a a'
    assume "(a, a') ∈ r" "(a', a) ∈ s"
    from ‹(a, a') ∈ r› have "(a, a') ∈ s" using r_in_s by blast
    with ‹partial_order_on A s› ‹(a', a) ∈ s›
    show "a = a'" unfolding partial_order_on_def by(blast dest: antisymD)
  qed
  ultimately show "∃s. linear_order_on A s ∧ order_consistent r s" by blast
qed

end