# Re: [isabelle] extending well-founded partial orders to total well-founded orders

```Dear Christian,

```
I haven't seen a formalisation of that proof, but I have formalised a proof that every partial order can be extended to a total order (in the appendix, works with Isabelle2012). A preliminary version thereof is part of JinjaThreads in the AFP (theory MM/Orders), but I have already removed that from the development version, because I no longer need it. As you can see there, it is not necessary to modify Zorn.thy from Isabelle's library, because you can encode the carrier set in the relation.
```
```
For the case of well-foundedness, I found the following informal proof in a blog, though I haven't checked whether it is correct:
```http://tylerneylon.com/blog/2007/06/every-well-founded-partial-order-can-be.html
```
It uses the existence of a well-ordering on any set. I don't know whether that has been proven in Isabelle before. Andrei might have done so in his Cardinals development; he might tell you more.
```
Andreas

On 01/17/2013 07:55 AM, Christian Sternagel wrote:
```
```Dear all,

```
is anybody aware of an Isabelle formalization of the (apparently well-known) fact that every well-founded partial order can be extended to a total well-founded order (in particular a well-partial-order)?
```
If not, any pointers to "informal" proofs (i.e., papers or textbooks ;)).

cheers

chris

```
```
```
```header {* Every partial order can be extended to a total order *}

theory Extend_Partial_Order
imports
"~~/src/HOL/Library/Zorn"
begin

lemma ChainD: "\<lbrakk> x \<in> C; C \<in> Chain r; y \<in> C \<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r"

lemma Chain_Field: "\<lbrakk> C \<in> Chain r; x \<in> C \<rbrakk> \<Longrightarrow> x \<in> Field r"

lemma total_onD:
"\<lbrakk> total_on A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> x = y \<or> (y, x) \<in> r"
unfolding total_on_def by blast

lemma linear_order_imp_linorder: "linear_order {(A, B). leq A B} \<Longrightarrow> class.linorder leq (\<lambda>x y. leq x y \<and> \<not> 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 \<le> 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 \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"
where "order_consistent r s \<longleftrightarrow> (\<forall>a a'. (a, a') \<in> r \<longrightarrow> (a', a) \<in> s \<longrightarrow> a = a')"

lemma order_consistent_sym:
"order_consistent r s \<Longrightarrow> order_consistent s r"

lemma antisym_order_consistent_self:
"antisym r \<Longrightarrow> 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) \<in> r^+"
thus "a \<in> A \<and> b \<in> 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 \<in> A" and y: "y \<in> A" and s: "(x, y) \<in> s"
shows "(x, y) \<in> r"
proof(cases "x = y")
case False
with r x y have "(x, y) \<in> r \<or> (y, x) \<in> r" unfolding total_on_def by blast
thus ?thesis
proof
assume "(y, x) \<in> 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 \<subseteq> A"
and trancl: "(x, y) \<in> (r \<union> s)^+"
obtains "(x, y) \<in> r"
| u v where "(x, u) \<in> r" "(u, v) \<in> s" "(v, y) \<in> 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"

from trancl show "(x, y) \<in> r \<or> (\<exists>u v. (x, u) \<in> r \<and> (u, v) \<in> s \<and> (v, y) \<in> r)"
proof(induction)
case (base y)
thus ?case
proof
assume "(x, y) \<in> s"
with `refl_on B s` have "x \<in> B" "y \<in> B"
by(blast dest: refl_onD1 refl_onD2)+
with B_subset_A have "x \<in> A" "y \<in> A" by blast+
hence "(x, x) \<in> r" "(y, y) \<in> r"
using `refl_on A r` by(blast intro: refl_onD)+
with `(x, y) \<in> s` show ?thesis by blast
qed(simp)
next
case (step y z)
from `(y, z) \<in> r \<union> s` show ?case
proof
assume "(y, z) \<in> s"
with `refl_on B s` have "y \<in> B" "z \<in> B"
by(blast dest: refl_onD2 refl_onD1)+
from step.IH show ?thesis
proof
assume "(x, y) \<in> r"
moreover from `z \<in> B` B_subset_A `refl_on A r`
have "(z, z) \<in> r" by(blast dest: refl_onD)
ultimately show ?thesis using `(y, z) \<in> s` by blast
next
assume "\<exists>u v. (x, u) \<in> r \<and> (u, v) \<in> s \<and> (v, y) \<in> r"
then obtain u v where "(x, u) \<in> r" "(u, v) \<in> s" "(v, y) \<in> r" by blast
from `refl_on B s` `(u, v) \<in> s` have "v \<in> B" by(rule refl_onD2)
with `total_on B s` `refl_on B s` order_consistent_sym[OF consist]
have "(v, y) \<in> s" using `y \<in> B` `(v, y) \<in> r`
by(rule total_on_refl_on_consistent_into)
with `trans s` have "(v, z) \<in> s" using `(y, z) \<in> s` by(rule transD)
with `trans s` `(u, v) \<in> s` have "(u, z) \<in> s" by(rule transD)
moreover from `z \<in> B` B_subset_A have "z \<in> A" ..
with `refl_on A r` have "(z, z) \<in> r" by(rule refl_onD)
ultimately show ?thesis using `(x, u) \<in> r` by blast
qed
next
assume "(y, z) \<in> 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 \<subseteq> A"
shows "antisym ((r \<union> s)^+)"
proof(rule antisymI)
fix x y
let ?rs = "(r \<union> s)^+"
assume "(x, y) \<in> ?rs" "(y, x) \<in> ?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"

from r s consist B_subset_A `(x, y) \<in> ?rs`
show "x = y"
proof(cases rule: porder_linorder_tranclpE)
case base
from r s consist B_subset_A `(y, x) \<in> ?rs`
show ?thesis
proof(cases rule: porder_linorder_tranclpE)
case base
with `antisym r` `(x, y) \<in> r` show ?thesis by(rule antisymD)
next
case (step u v)
from `(v, x) \<in> r` `(x, y) \<in> r` `(y, u) \<in> r` have "(v, u) \<in> r"
by(blast intro: transD[OF `trans r`])
with consist have "v = u" using `(u, v) \<in> s`
with `(y, u) \<in> r` `(v, x) \<in> r` have "(y, x) \<in> r"
by(blast intro: transD[OF `trans r`])
with `antisym r` `(x, y) \<in> r` show ?thesis by(rule antisymD)
qed
next
case (step u v)
from r s consist B_subset_A `(y, x) \<in> ?rs`
show ?thesis
proof(cases rule: porder_linorder_tranclpE)
case base
from `(v, y) \<in> r` `(y, x) \<in> r` `(x, u) \<in> r` have "(v, u) \<in> r"
by(blast intro: transD[OF `trans r`])
with consist `(u, v) \<in> s`
have "u = v" by(auto simp add: order_consistent_def)
with `(v, y) \<in> r` `(x, u) \<in> r` have "(x, y) \<in> r"
by(blast intro: transD[OF `trans r`])
with `antisym r` show ?thesis using `(y, x) \<in> 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) \<in> s` `(u', v') \<in> s`
have "u \<in> B" "v \<in> B" "u' \<in> B" "v' \<in> B" by(blast dest: refl_onD1 refl_onD2)+
from `trans r` `(v', x) \<in> r` `(x, u) \<in> r` have "(v', u) \<in> r" by(rule transD)
with `v' \<in> B` `u \<in> B` have "(v', u) \<in> s" by(rule r_into_s)
also note `(u, v) \<in> s` also (transD[OF `trans s`])
from `trans r` `(v, y) \<in> r` `(y, u') \<in> r` have "(v, u') \<in> r" by(rule transD)
with `v \<in> B` `u' \<in> B` have "(v, u') \<in> s" by(rule r_into_s)
finally (transD[OF `trans s`])
have "v' = u'" using `(u', v') \<in> s` by(rule antisymD[OF `antisym s`])
moreover with `(v, u') \<in> s` `(v', u) \<in> s` have "(v, u) \<in> s"
by(blast intro: transD[OF `trans s`])
with `antisym s` `(u, v) \<in> s` have "u = v" by(rule antisymD)
ultimately have "(x, y) \<in> r" "(y, x) \<in> r"
using `(x, u) \<in> r` `(v, y) \<in> r` `(y, u') \<in> r` `(v', x) \<in> 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 \<subseteq> A"
shows "partial_order_on A ((r \<union> s)^+)"
unfolding partial_order_on_def preorder_on_def
proof(intro conjI)
let ?rs = "r \<union> 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"
ultimately have "refl_on (A \<union> B) ?rs" by(rule refl_on_Un)
also from subset have "A \<union> 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)
def S \<equiv> "{s. partial_order_on A s \<and> r \<subseteq> s}"
from r have r_in_S: "r \<in> S" unfolding S_def by auto

have "\<exists>y\<in>S. \<forall>x\<in>S. y \<subseteq> x \<longrightarrow> y = x"
proof(rule Zorn_Lemma2[rule_format])
fix c
assume "c \<in> chain S"
hence "c \<subseteq> S" by(rule chainD2)

show "\<exists>y\<in>S. \<forall>x\<in>c. x \<subseteq> y"
proof(cases "c = {}")
case True
with r_in_S show ?thesis by blast
next
case False
then obtain s where "s \<in> c" by blast
hence s: "partial_order_on A s"
and r_in_s: "r \<subseteq> s"
using `c \<subseteq> S` unfolding S_def by blast+

have "partial_order_on A (\<Union>c)"
unfolding partial_order_on_def preorder_on_def
proof(intro conjI)
show "refl_on A (\<Union>c)"
proof(rule refl_onI[OF subsetI])
fix x
assume "x \<in> \<Union>c"
then obtain X where "X \<in> c" and "x \<in> X" by blast
from `X \<in> c` `c \<subseteq> S` have "X \<in> S" ..
hence "partial_order_on A X" unfolding S_def by simp
with `x \<in> X` show "x \<in> A \<times> A"
by(cases x)(auto simp add: partial_order_on_def preorder_on_def dest: refl_onD1 refl_onD2)
next
fix x
assume "x \<in> A"
with s have "(x, x) \<in> s" unfolding partial_order_on_def preorder_on_def
by(blast dest: refl_onD)
with `s \<in> c` show "(x, x) \<in> \<Union>c" by(rule UnionI)
qed

show "antisym (\<Union>c)"
proof(rule antisymI)
fix x y
assume "(x, y) \<in> \<Union>c" "(y, x) \<in> \<Union>c"
then obtain X Y where "X \<in> c" "Y \<in> c" "(x, y) \<in> X" "(y, x) \<in> Y" by blast
from `X \<in> c` `Y \<in> c` `c \<subseteq> S` have "antisym X" "antisym Y"
unfolding S_def by(auto simp add: partial_order_on_def)
moreover from `c \<in> chain S` `X \<in> c` `Y \<in> c`
have "X \<subseteq> Y \<or> Y \<subseteq> X" by(rule chainD)
ultimately show "x = y" using `(x, y) \<in> X` `(y, x) \<in> Y`
by(auto dest: antisymD)
qed

show "trans (\<Union>c)"
proof(rule transI)
fix x y z
assume "(x, y) \<in> \<Union>c" "(y, z) \<in> \<Union>c"
then obtain X Y where "X \<in> c" "Y \<in> c" "(x, y) \<in> X" "(y, z) \<in> Y" by blast
from `X \<in> c` `Y \<in> c` `c \<subseteq> S` have "trans X" "trans Y"
unfolding S_def by(auto simp add: partial_order_on_def preorder_on_def)
from `c \<in> chain S` `X \<in> c` `Y \<in> c`
have "X \<subseteq> Y \<or> Y \<subseteq> X" by(rule chainD)
thus "(x, z) \<in> \<Union>c"
proof
assume "X \<subseteq> Y"
with `trans Y` `(x, y) \<in> X` `(y, z) \<in> Y`
have "(x, z) \<in> Y" by(blast dest: transD)
with `Y \<in> c` show ?thesis by(rule UnionI)
next
assume "Y \<subseteq> X"
with `trans X` `(x, y) \<in> X` `(y, z) \<in> Y`
have "(x, z) \<in> X" by(blast dest: transD)
with `X \<in> c` show ?thesis by(rule UnionI)
qed
qed
qed
moreover
have "r \<subseteq> \<Union>c" using r_in_s `s \<in> c` by blast
ultimately have "\<Union>c \<in> S" unfolding S_def by simp
thus ?thesis by blast
qed
qed
then obtain s where "s \<in> S" and y_max: "\<And>t. \<lbrakk> t \<in> S; s \<subseteq> t \<rbrakk> \<Longrightarrow> s = t" by blast

have "partial_order_on A s" using `s \<in> S`
unfolding S_def by simp
moreover
have r_in_s: "r \<subseteq> s" using `s \<in> S` unfolding S_def by blast

have "total_on A s"
unfolding total_on_def
proof(intro strip)
fix x y
assume "x \<in> A" "y \<in> A" "x \<noteq> y"
show "(x, y) \<in> s \<or> (y, x) \<in> s"
proof(rule ccontr)
assume "\<not> ?thesis"
hence xy: "(x, y) \<notin> s" "(y, x) \<notin> s" by simp_all

def s' \<equiv> "{(a, b). a = x \<and> (b = y \<or> b = x) \<or> a = y \<and> b = y}"
let ?s' = "(s \<union> 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} \<subseteq> A" using `x \<in> A` `y \<in> A` by blast
ultimately have "partial_order_on A ?s'"
by(rule porder_on_linorder_on_tranclp_porder_onI)
moreover have "r \<subseteq> ?s'" using r_in_s by auto
ultimately have "?s' \<in> S" unfolding S_def by simp
moreover have "s \<subseteq> ?s'" by auto
ultimately have "s = ?s'" by(rule y_max)
moreover have "(x, y) \<in> ?s'" by(auto simp add: s'_def)
ultimately show False using `(x, y) \<notin> 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') \<in> r" "(a', a) \<in> s"
from `(a, a') \<in> r` have "(a, a') \<in> s" using r_in_s by blast
with `partial_order_on A s` `(a', a) \<in> s`
show "a = a'" unfolding partial_order_on_def by(blast dest: antisymD)
qed
ultimately show "\<exists>s. linear_order_on A s \<and> order_consistent r s" by blast
qed

end```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.