Theory Containers.Extend_Partial_Order

(* 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 "yS. xS. y  x  x = y"
  proof(rule Zorn_Lemma2[rule_format])
    fix c
    assume "c  chains S"
    hence "c  S" by(rule chainsD2)

    show "yS. xc. 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