theory Quasi_Order
imports
Reduction_Pair
HOL.Complete_Lattices
"HOL-Library.Lattice_Syntax"
begin
section‹Convenient Relation-to-Set Conversion›
abbreviation rel_of where "rel_of f ≡ Collect (case_prod f)"
lemma mem_rel_ofI: "r1 x y ⟹ (x,y) ∈ rel_of r1" by simp
lemma rel_of:
shows rel_of_OO: "⋀r1 r2. rel_of (r1 OO r2) = rel_of r1 O rel_of r2"
and rel_of_sup: "⋀r1 r2. rel_of (r1 ⊔ r2) = rel_of r1 ∪ rel_of r2"
and rel_of_inf: "⋀r1 r2. rel_of (r1 ⊓ r2) = rel_of r1 ∩ rel_of r2"
and rel_of_tranclp: "⋀r. rel_of (r⇧+⇧+) = (rel_of r)⇧+"
and rel_of_rtranclp: "⋀r. rel_of (r⇧*⇧*) = (rel_of r)⇧*"
and rel_of_conversep: "⋀r. rel_of r¯¯ = (rel_of r)¯"
and le_by_rel_of: "⋀r1 r2. r1 ≤ r2 ⟷ rel_of r1 ⊆ rel_of r2"
and eq_by_rel_of: "⋀r1 r2. r1 = r2 ⟷ rel_of r1 = rel_of r2"
and wfP_by_rel_of: "⋀r. wfP r ⟷ wf (rel_of r)"
by (auto 0 4 simp add: trancl_def rtrancl_def wfP_def)
lemmas OO_mono1 = O_mono1[of "rel_of _" "rel_of _" "rel_of _", folded rel_of]
lemmas OO_mono2 = O_mono2[of "rel_of _" "rel_of _" "rel_of _", folded rel_of]
lemmas OO_assoc = O_assoc[of "rel_of _" "rel_of _" "rel_of _", folded rel_of]
lemma tranclp_mono: "r ≤ s ⟹ r⇧+⇧+ ≤ s⇧+⇧+"
by (simp add: rel_of subrelI trancl_mono)
lemma wf_O_comm: "wf (R O S) ⟷ wf (S O R)"
using SN_O_comm
by (metis SN_iff_wf converse_converse converse_relcomp)
lemma wf_relto_relcomp: "wf (relto R S) ⟷ wf (R O S⇧*)"
using SN_on_relto_relcomp[of "S¯" "R¯" UNIV]
by (simp add: rtrancl_converse converse_relcomp[symmetric] SN_iff_wf O_assoc)
context
fixes S R
assumes pull: "S O R ⊆ R⇧* O S"
begin
qualified lemma push: "R¯ O S¯ ⊆ S¯ O (R¯)⇧*"
by (metis pull converse_mono converse_relcomp rtrancl_converse)
lemma O_rtrancl_pull: "S O R⇧* ⊆ R⇧* O S"
using rtrancl_O_push[OF push]
by (metis converse_mono converse_relcomp rtrancl_converse)
lemma rtrancl_U_pull: "(S ∪ R)⇧* = R⇧* O S⇧*"
using rtrancl_U_push[OF push]
by (metis converse_Un converse_converse converse_relcomp rtrancl_converse sup_commute)
lemma wf_relto_pull: "wf (R⇧* O S O R⇧*) ⟷ wf S"
apply (rule iffI)
apply (rule wf_subset, force, force)
unfolding wf_relto_relcomp
using SN_on_O_push[OF push, of UNIV]
by (subst wf_O_comm, auto simp: O_rtrancl_pull wf_relcomp_compatible)
end
lemma wf_trancl_iff[simp]: "wf (R⇧+) ⟷ wf R"
by (intro iffI[OF wf_subset[of "R⇧+"] wf_trancl], auto)
context
fixes R S :: "('a × 'a) set"
assumes absorb: "R O S ⊆ R"
begin
lemma O_rtrancl_absorb_right: "R O S⇧* = R"
proof-
{ fix x y z
have "(y,z) ∈ S⇧* ⟹ (x,y) ∈ R ⟹ (x,z) ∈ R"
by (induct rule: rtrancl_induct, insert absorb, auto)
}
then show ?thesis by auto
qed
lemma rtrancl_U_absorb_right: "(S ∪ R)⇧* = S⇧* O R⇧*"
apply (subst Un_commute)
apply (rule rtrancl_U_pull)
using absorb by auto
lemma wf_relto_absorb_right: "wf (relto R S) ⟷ wf R"
apply (rule wf_relto_pull) using absorb by auto
end
section ‹Quasi-Orderings›
context ord begin
text ‹Extending @{class ord} with some more notations.›
definition equiv (infix "∼" 50) where [simp]: "x ∼ y ≡ x ≤ y ∧ y ≤ x"
lemma equiv_sym[sym]: "x ∼ y ⟹ y ∼ x" by auto
definition equiv_class ("[_]⇩∼") where "[x]⇩∼ ≡ { y. x ∼ y }"
lemma mem_equiv_class[simp]: "y ∈ [x]⇩∼ ⟷ x ∼ y" by (auto simp: equiv_class_def)
definition "Upper_Bounds X ≡ {b. ∀x ∈ X. b ≥ x}"
lemma mem_Upper_Bounds: "b ∈ Upper_Bounds X ⟷ (∀x ∈ X. b ≥ x)"
by (auto simp: Upper_Bounds_def)
lemma Upper_BoundsI[intro]: "(⋀x. x ∈ X ⟹ b ≥ x) ⟹ b ∈ Upper_Bounds X"
by (auto simp: Upper_Bounds_def)
lemma Upper_BoundsE[elim]: "b ∈ Upper_Bounds X ⟹ ((⋀x. x ∈ X ⟹ b ≥ x) ⟹ thesis) ⟹ thesis"
by (auto simp: Upper_Bounds_def)
lemma Upper_Bounds_empty[simp]: "Upper_Bounds {} = UNIV" by auto
lemma Upper_Bounds_insert: "Upper_Bounds (insert x X) = {b. b ≥ x} ∩ Upper_Bounds X" by auto
lemma Upper_Bounds_singleton[simp]: "Upper_Bounds {x} = {b. b ≥ x}" by auto
lemma Upper_Bounds_cmono: assumes "X ⊆ Y" shows "Upper_Bounds X ⊇ Upper_Bounds Y"
using assms by (auto simp: Upper_Bounds_def)
definition "Leasts X ≡ { b ∈ X. ∀c ∈ X. b ≤ c }"
lemma LeastsI[intro]: "b ∈ X ⟹ (⋀x. x ∈ X ⟹ b ≤ x) ⟹ b ∈ Leasts X"
and LeastsD: "x ∈ Leasts X ⟹ y ∈ X ⟹ x ≤ y"
and LeastsE[elim]: "b ∈ Leasts X ⟹ (b ∈ X ⟹ (⋀x. x ∈ X ⟹ b ≤ x) ⟹ thesis) ⟹ thesis"
by (auto simp: Leasts_def)
lemma Least_Upper_Bounds_mono:
assumes XY: "X ⊆ Y" and bX: "bX ∈ Leasts (Upper_Bounds X)" and bY: "bY ∈ Leasts (Upper_Bounds Y)"
shows "bX ≤ bY"
proof-
have "bY ∈ Upper_Bounds X" using XY bY by force
with bX show ?thesis by auto
qed
lemma Leasts_equiv: "x ∈ Leasts X ⟹ y ∈ Leasts X ⟹ x ∼ y" by auto
end
text ‹This is a trick to make a class available also as a locale›
locale ord_syntax = ord less_eq less for less_eq less :: "'a ⇒ 'a ⇒ bool"
begin
notation less_eq (infix "⊑" 50)
notation less (infix "⊏" 50)
abbreviation(input) greater_eq_syntax (infix "⊒" 50) where "greater_eq_syntax ≡ ord.greater_eq less_eq"
abbreviation(input) greater_syntax (infix "⊐" 50) where "greater_syntax ≡ ord.greater less"
abbreviation equiv_syntax (infix "≃" 50) where "equiv_syntax ≡ ord.equiv less_eq"
abbreviation equiv_class_syntax ("[_]⇩≃") where "equiv_class_syntax ≡ ord.equiv_class less_eq"
end
class quasi_order = ord +
assumes order_refl[iff]: "x ≤ x"
and order_trans[trans]: "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
and le_less_trans[trans]: "x ≤ y ⟹ y < z ⟹ x < z"
and less_le_trans[trans]: "x < y ⟹ y ≤ z ⟹ x < z"
and less_imp_le: "x < y ⟹ x ≤ y"
begin
lemma eq_imp_le: "x = y ⟹ x ≤ y" by auto
lemma less_trans[trans]: "x < y ⟹ y < z ⟹ x < z"
using le_less_trans[OF less_imp_le].
text ‹
Class @{class quasi_order} is incomparable with HOL class @{class preorder}, as the latter
fixes $<$ as the "strict part" (which is not nice, e.g., for comparing polynomials)
while we already assume compatibility (@{thm le_less_trans}).
›
lemma equiv_trans[trans]:
"x ∼ y ⟹ y ∼ z ⟹ x ∼ z"
"x ∼ y ⟹ y ≤ z ⟹ x ≤ z"
"x ≤ y ⟹ y ∼ z ⟹ x ≤ z"
"x ∼ y ⟹ y < z ⟹ x < z"
"x < y ⟹ y ∼ z ⟹ x < z"
by (auto dest: order_trans le_less_trans less_le_trans)
lemma chainp_le_mono:
assumes ch: "chainp (≤) seq" and ij: "i ≤ j" shows "seq i ≤ seq j"
by (insert ij, induct rule: inc_induct, insert ch, auto dest: order_trans)
lemma chainp_less_mono: assumes ch: "chainp (<) seq" and ij: "i < j" shows "seq i < seq j"
by (insert ij, induct rule:strict_inc_induct, insert ch, auto dest: less_trans)
lemma Leasts_singleton[simp]: "Leasts {a} = {a}"
by auto
lemma Least_Upper_Bounds_singleton: "Leasts ({b. b ≥ x}) = [x]⇩∼"
by (auto intro!: LeastsI dest: order_trans)
lemma Least_Upper_Bounds_equiv_class:
assumes bX: "b ∈ Leasts (Upper_Bounds X)" shows "Leasts (Upper_Bounds X) = [b]⇩∼"
proof(intro equalityI subsetI, unfold mem_equiv_class)
from bX have bX: "b ∈ Upper_Bounds X" and leastb: "⋀x. x ∈ Upper_Bounds X ⟹ b ≤ x" by auto
{ fix c assume "c ∈ Leasts (Upper_Bounds X)"
then have cUpper_Bounds: "c ∈ Upper_Bounds X" and leastc: "⋀b. b ∈ Upper_Bounds X ⟹ c ≤ b" by auto
from leastb[OF cUpper_Bounds] leastc[OF bX] show "b ∼ c" by auto
}
{ fix c assume bc: "b ∼ c"
show "c ∈ Leasts (Upper_Bounds X)"
proof(intro LeastsI Upper_BoundsI)
fix x assume "x ∈ X"
with bX have "x ≤ b" by auto
with bc show "x ≤ c" by (auto dest: order_trans)
next
fix x assume "x ∈ Upper_Bounds X"
from leastb[OF this] bc show "c ≤ x" by (auto dest: order_trans)
qed
}
qed
sublocale order_pair "rel_of (>)" "rel_of (≥)"
apply (unfold_locales, fold transp_trans)
using le_less_trans less_le_trans
by (auto intro: refl_onI transpI[OF less_trans] transpI[OF order_trans])
end
subsection ‹Weakly ordered domain: where antisymmetry holds›
class weak_order = quasi_order + assumes antisym[dest]: "a ≤ b ⟹ b ≤ a ⟹ a = b"
begin
lemma equiv_is_eq[simp]: "(∼) = (=)" by (intro ext, auto)
lemma equiv_class_singleton[simp]: "[a]⇩∼ = {a}" by auto
lemma Least_Upper_Bound_singleton[simp]: "Leasts (Upper_Bounds {a}) = {a}" by auto
end
declare equiv_def[simp del]
subclass(in order) weak_order by(unfold_locales, auto)
subsection ‹Well-founded quasi-ordered domain›
class wf_order = quasi_order +
assumes less_induct[case_names less]: "⋀P a. (⋀x. (⋀y. y < x ⟹ P y) ⟹ P x) ⟹ P a"
begin
lemma wf: "wf (rel_of (<))" unfolding wf_def by(auto intro:less_induct)
sublocale SN_order_pair "rel_of (>)" "rel_of (≥)"
by (unfold_locales, auto simp: SN_iff_wf converse_def conversep.simps intro: wf)
lemma chainp_ends_nonstrict:
assumes 0: "chainp (≥) seq" shows "∃n. ∀i ≥ n. ¬ seq (Suc i) < seq i"
proof (rule ccontr, insert 0, induct "seq 0" arbitrary: seq rule: less_induct)
case (less seq)
from less.prems
obtain n where 1: "seq n > seq (Suc n)" by auto
define seq' where "⋀i. seq' i = seq (Suc n + i)"
show False
proof (rule less.hyps)
from less.prems show "chainp (≥) seq'" by (auto simp: seq'_def)
note 1
also have "seq 0 ≥ seq n" using less.prems by (induct n, auto dest: order_trans)
finally show "seq 0 > seq' 0" by (auto simp: seq'_def)
show "∄n. ∀i≥n. ¬ seq' (Suc i) < seq' i"
proof (unfold not_ex, intro allI notI)
fix m
assume 2: "∀i≥m. ¬ seq' (Suc i) < seq' i"
from less.prems(1)[simplified, rule_format, of "m+n+1"]
obtain i where "i ≥ m + n + 1" and "seq (Suc i) < seq i" by auto
then have "i - n - 1 ≥ m" and "seq' (Suc (i-n-1)) < seq' (i-n-1)" by (auto simp: seq'_def)
with 2 show False by auto
qed
qed
qed
end
text ‹@{class wellorder} is a @{class wf_order}.›
context wellorder begin
subclass wf_order by (unfold_locales; (fact less_induct | simp))
lemma chainp_ends_eq:
assumes 1: "chainp (≥) seq" shows "∃n. ∀i≥n. seq i = seq n"
proof-
from chainp_ends_nonstrict[OF 1] 1
obtain n where 2: "⋀i. i ≥ n ⟹ seq (Suc i) = seq i" by (auto simp: not_less)
show ?thesis
proof (intro exI allI impI)
show "n ≤ i ⟹ seq i = seq n" for i by (induct rule:dec_induct, auto simp: 2)
qed
qed
end
text ‹@{type nat} is a @{class wf_order}.›
instance nat :: wf_order ..
text ‹The next one turns a well-founded relation into a well-founded order pair.›
locale wf_order_seed =
fixes w s :: "'a ⇒ 'a ⇒ bool"
assumes wf: "wfP s"
and weak_compatp: "s OO w ≤ s⇧+⇧+"
begin
definition less (infix "⊏" 50) where "less ≡ (w⇧*⇧* OO s)⇧+⇧+"
definition less_eq (infix "⊑" 50) where "less_eq ≡ (w ⊔ s)⇧*⇧*"
lemma absorb: "s⇧+⇧+ OO w ≤ s⇧+⇧+"
proof-
have "s⇧+⇧+ x y ⟹ w y z ⟹ s⇧+⇧+ x z" for x y z
by (induct rule: tranclp_induct, insert weak_compatp, auto)
then show ?thesis by auto
qed
sublocale wf_order where less_eq = less_eq and less = less
proof (unfold_locales)
have [trans]: "⋀x y z. less x y ⟹ less y z ⟹ less x z" by (auto simp: less_def)
have "less ≤ less_eq" by (unfold less_def less_eq_def rel_of, regexp)
then show "⋀x y. x ⊏ y ⟹ x ⊑ y" by auto
show [trans]: "⋀x y z. x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z" by (auto simp: less_eq_def)
have 1: "less_eq OO less ≤ less" by (unfold rel_of less_eq_def less_def, regexp)
then show "⋀x y z. x ⊑ y ⟹ y ⊏ z ⟹ x ⊏ z" by auto
have "less OO w ≤ (w⇧*⇧* OO s)⇧*⇧* OO w⇧*⇧* OO s⇧+⇧+"
apply (unfold less_def)
apply (subst trancl_unfold_right[of "rel_of _", unfolded rel_of[symmetric]])
using OO_mono1[OF weak_compatp, of "(w⇧*⇧* OO s)⇧*⇧* OO w⇧*⇧*"]
by (simp add: OO_assoc)
also have "... ≤ less" by (unfold less_def rel_of, regexp)
finally have "less OO w ≤ less".
moreover have "less OO s ≤ less" by (unfold less_def rel_of, regexp)
ultimately have "less OO (w ⊔ s) ≤ less" by auto
then have 2: "less OO less_eq = less"
by (simp add: less_eq_def rel_of O_rtrancl_absorb_right)
from eq_imp_le[OF this] show "⋀x y z. x ⊏ y ⟹ y ⊑ z ⟹ x ⊏ z" by force
have less: "less = (w⇧*⇧* OO s⇧+⇧+ OO w⇧*⇧*)⇧+⇧+"
apply (subst 2[symmetric])
apply (unfold less_eq_def less_def rel_of)
apply regexp
done
have "wf (rel_of less)"
apply (unfold less rel_of wf_trancl_iff)
apply (subst wf_relto_absorb_right) using absorb wf
by (auto simp: rel_of)
then show "⋀P a. (⋀x. (⋀y. y ⊏ x ⟹ P y) ⟹ P x) ⟹ P a"
by (auto simp: wf_def)
qed (auto simp: less_eq_def)
end
class quasi_order_sup = quasi_order + sup +
assumes sup_ge1 [intro!]: "x ≤ x ⊔ y"
and sup_ge2 [intro!]: "y ≤ x ⊔ y"
begin
lemma sup_trans1: assumes "x ≤ y" shows "x ≤ y ⊔ z"
proof-
note assms also note sup_ge1 finally show ?thesis by auto
qed
lemma sup_trans2: assumes "x ≤ z" shows "x ≤ y ⊔ z"
proof-
note assms also note sup_ge2 finally show ?thesis by auto
qed
lemma finite_set_has_Upper_Bounds: "finite X ⟹ ∃b. b ∈ Upper_Bounds X"
by (unfold Upper_Bounds_def, induct X rule:finite_induct, auto dest: sup_trans1)
lemma finite_set_is_bounded:
assumes "finite X" and "x ∈ X" shows "x ≤ (SOME b. b ∈ Upper_Bounds X)"
using finite_set_has_Upper_Bounds[OF assms(1), folded some_eq_ex] assms(2) by auto
end
class quasi_semilattice_sup = quasi_order_sup +
assumes sup_least: "y ≤ x ⟹ z ≤ x ⟹ y ⊔ z ≤ x"
begin
lemma finite_set_has_Least_Upper_Bounds: "finite X ⟹ X ≠ {} ⟹ ∃b. b ∈ Leasts (Upper_Bounds X)"
proof(induct X rule:finite_induct)
case empty then show ?case by auto
next
case IH: (insert x X)
show ?case
proof(cases "X = {}")
case True
with Least_Upper_Bounds_singleton have "Leasts (Upper_Bounds (insert x X)) = [x]⇩∼" by auto
then show ?thesis by auto
next
case False
with IH have "Leasts (Upper_Bounds X) ≠ {}" by auto
then obtain b where bX: "b ∈ Leasts (Upper_Bounds X)" by auto
then have "sup x b ∈ Leasts (Upper_Bounds (insert x X))"
by (auto intro: sup_trans2 sup_least intro!: LeastsI Upper_BoundsI simp: Upper_Bounds_insert)
then show ?thesis by auto
qed
qed
end
subclass (in semilattice_sup) quasi_semilattice_sup by (unfold_locales, auto)
class quasi_order_bot = quasi_order + bot +
assumes bot_least: "⊥ ≤ a"
text ‹A class where the @{const Sup} operator is defined, which is valid only if it is definable.›
class quasi_order_Sup = quasi_order + Sup +
assumes Sup_in_Least_Upper_Bounds: "Leasts (Upper_Bounds X) ≠ {} ⟹ ⨆X ∈ Leasts (Upper_Bounds X)"
begin
lemma Sup_upper: assumes LUB: "Leasts (Upper_Bounds X) ≠ {}" and xX: "x ∈ X" shows "x ≤ ⨆X"
using Sup_in_Least_Upper_Bounds[OF LUB] xX by auto
lemma Sup_least: assumes LUB: "Leasts (Upper_Bounds X) ≠ {}" shows "(⋀x. x ∈ X ⟹ x ≤ y) ⟹ ⨆X ≤ y"
using Sup_in_Least_Upper_Bounds[OF LUB] by (auto simp: Upper_Bounds_def)
lemma Sup_equiv_Least_Upper_Bounds: assumes bX: "b ∈ Leasts (Upper_Bounds X)" shows "⨆X ∼ b"
proof-
have "Leasts (Upper_Bounds X) ≠ {}" using bX by auto
from Sup_in_Least_Upper_Bounds[OF this] show ?thesis using bX by auto
qed
lemma Sup_singleton: "⨆{x} ∼ x" by (rule Sup_equiv_Least_Upper_Bounds, auto)
lemma Sup_mono:
assumes X: "Leasts (Upper_Bounds X) ≠ {}" and Y: "Leasts (Upper_Bounds Y) ≠ {}" and XY: "X ⊆ Y"
shows "⨆X ≤ ⨆Y"
by (auto intro: Least_Upper_Bounds_mono[OF XY] Sup_in_Least_Upper_Bounds[OF X] Sup_in_Least_Upper_Bounds[OF Y])
end
text ‹Upward complete quasi-semilattices -- where @{const Sup} is always defined.›
class quasi_semilattice_Sup = quasi_order_Sup + sup + bot +
assumes Least_Upper_Bounds: "Leasts (Upper_Bounds X) ≠ {}"
and sup_Sup: "x ⊔ y = ⨆{x,y}"
and bot_Sup: "⊥ = ⨆{}"
begin
lemmas Sup_in_Least_Upper_Bounds = Sup_in_Least_Upper_Bounds[OF Least_Upper_Bounds]
lemmas Sup_upper = Sup_upper[OF Least_Upper_Bounds]
lemmas Sup_least = Sup_least[OF Least_Upper_Bounds]
lemmas Sup_mono = Sup_mono[OF Least_Upper_Bounds]
subclass quasi_semilattice_sup
by (unfold_locales, auto intro: Sup_upper Sup_least simp: sup_Sup)
subclass quasi_order_bot
proof(unfold_locales)
fix x
have "⊥ ≤ ⨆{x}" by (unfold bot_Sup, rule Sup_mono, auto)
also have "… ∼ x" by (rule Sup_singleton)
finally show "⊥ ≤ x".
qed
end
subsection ‹@{term inv_imagep}›
locale quasi_order_inv_imagep = base: quasi_order
begin
sublocale quasi_order "inv_imagep less_eq f" "inv_imagep less f"
by (unfold_locales, unfold in_inv_imagep;
fact base.order_refl base.order_trans base.less_trans base.less_le_trans base.le_less_trans base.less_imp_le)
end
locale wf_order_inv_imagep = base: wf_order
begin
interpretation quasi_order_inv_imagep..
sublocale wf_order "inv_imagep less_eq f" "inv_imagep less f"
apply (unfold_locales)
apply (unfold in_inv_imagep)
using wf_inv_image[OF base.wf, unfolded wf_def] by auto
end
end