Theory BNF_Wellorder_Relation
section ‹Well-Order Relations as Needed by Bounded Natural Functors›
theory BNF_Wellorder_Relation
imports Order_Relation
begin
text‹In this section, we develop basic concepts and results pertaining
to well-order relations. Note that we consider well-order relations
as {\em non-strict relations},
i.e., as containing the diagonals of their fields.›
locale wo_rel =
fixes r :: "'a rel"
assumes WELL: "Well_order r"
begin
text‹The following context encompasses all this section. In other words,
for the whole section, we consider a fixed well-order relation \<^term>‹r›.›
abbreviation under where "under ≡ Order_Relation.under r"
abbreviation underS where "underS ≡ Order_Relation.underS r"
abbreviation Under where "Under ≡ Order_Relation.Under r"
abbreviation UnderS where "UnderS ≡ Order_Relation.UnderS r"
abbreviation above where "above ≡ Order_Relation.above r"
abbreviation aboveS where "aboveS ≡ Order_Relation.aboveS r"
abbreviation Above where "Above ≡ Order_Relation.Above r"
abbreviation AboveS where "AboveS ≡ Order_Relation.AboveS r"
abbreviation ofilter where "ofilter ≡ Order_Relation.ofilter r"
lemmas ofilter_def = Order_Relation.ofilter_def[of r]
subsection ‹Auxiliaries›
lemma REFL: "Refl r"
using WELL order_on_defs[of _ r] by auto
lemma TRANS: "trans r"
using WELL order_on_defs[of _ r] by auto
lemma ANTISYM: "antisym r"
using WELL order_on_defs[of _ r] by auto
lemma TOTAL: "Total r"
using WELL order_on_defs[of _ r] by auto
lemma TOTALS: "∀a ∈ Field r. ∀b ∈ Field r. (a,b) ∈ r ∨ (b,a) ∈ r"
using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force
lemma LIN: "Linear_order r"
using WELL well_order_on_def[of _ r] by auto
lemma WF: "wf (r - Id)"
using WELL well_order_on_def[of _ r] by auto
lemma cases_Total:
"⋀ phi a b. ⟦{a,b} <= Field r; ((a,b) ∈ r ⟹ phi a b); ((b,a) ∈ r ⟹ phi a b)⟧
⟹ phi a b"
using TOTALS by auto
lemma cases_Total3:
"⋀ phi a b. ⟦{a,b} ≤ Field r; ((a,b) ∈ r - Id ∨ (b,a) ∈ r - Id ⟹ phi a b);
(a = b ⟹ phi a b)⟧ ⟹ phi a b"
using TOTALS by auto
subsection ‹Well-founded induction and recursion adapted to non-strict well-order relations›
text‹Here we provide induction and recursion principles specific to {\em non-strict}
well-order relations.
Although minor variations of those for well-founded relations, they will be useful
for doing away with the tediousness of
having to take out the diagonal each time in order to switch to a well-founded relation.›
lemma well_order_induct:
assumes IND: "⋀x. ∀y. y ≠ x ∧ (y, x) ∈ r ⟶ P y ⟹ P x"
shows "P a"
proof-
have "⋀x. ∀y. (y, x) ∈ r - Id ⟶ P y ⟹ P x"
using IND by blast
thus "P a" using WF wf_induct[of "r - Id" P a] by blast
qed
definition
worec :: "(('a ⇒ 'b) ⇒ 'a ⇒ 'b) ⇒ 'a ⇒ 'b"
where
"worec F ≡ wfrec (r - Id) F"
definition
adm_wo :: "(('a ⇒ 'b) ⇒ 'a ⇒ 'b) ⇒ bool"
where
"adm_wo H ≡ ∀f g x. (∀y ∈ underS x. f y = g y) ⟶ H f x = H g x"
lemma worec_fixpoint:
assumes ADM: "adm_wo H"
shows "worec H = H (worec H)"
proof-
let ?rS = "r - Id"
have "adm_wf (r - Id) H"
unfolding adm_wf_def
using ADM adm_wo_def[of H] underS_def[of r] by auto
hence "wfrec ?rS H = H (wfrec ?rS H)"
using WF wfrec_fixpoint[of ?rS H] by simp
thus ?thesis unfolding worec_def .
qed
subsection ‹The notions of maximum, minimum, supremum, successor and order filter›
text‹
We define the successor {\em of a set}, and not of an element (the latter is of course
a particular case). Also, we define the maximum {\em of two elements}, ‹max2›,
and the minimum {\em of a set}, ‹minim› -- we chose these variants since we
consider them the most useful for well-orders. The minimum is defined in terms of the
auxiliary relational operator ‹isMinim›. Then, supremum and successor are
defined in terms of minimum as expected.
The minimum is only meaningful for non-empty sets, and the successor is only
meaningful for sets for which strict upper bounds exist.
Order filters for well-orders are also known as ``initial segments".›
definition max2 :: "'a ⇒ 'a ⇒ 'a"
where "max2 a b ≡ if (a,b) ∈ r then b else a"
definition isMinim :: "'a set ⇒ 'a ⇒ bool"
where "isMinim A b ≡ b ∈ A ∧ (∀a ∈ A. (b,a) ∈ r)"
definition minim :: "'a set ⇒ 'a"
where "minim A ≡ THE b. isMinim A b"
definition supr :: "'a set ⇒ 'a"
where "supr A ≡ minim (Above A)"
definition suc :: "'a set ⇒ 'a"
where "suc A ≡ minim (AboveS A)"
subsubsection ‹Properties of max2›
lemma max2_greater_among:
assumes "a ∈ Field r" and "b ∈ Field r"
shows "(a, max2 a b) ∈ r ∧ (b, max2 a b) ∈ r ∧ max2 a b ∈ {a,b}"
proof-
{assume "(a,b) ∈ r"
hence ?thesis using max2_def assms REFL refl_on_def
by (auto simp add: refl_on_def)
}
moreover
{assume "a = b"
hence "(a,b) ∈ r" using REFL assms
by (auto simp add: refl_on_def)
}
moreover
{assume *: "a ≠ b ∧ (b,a) ∈ r"
hence "(a,b) ∉ r" using ANTISYM
by (auto simp add: antisym_def)
hence ?thesis using * max2_def assms REFL refl_on_def
by (auto simp add: refl_on_def)
}
ultimately show ?thesis using assms TOTAL
total_on_def[of "Field r" r] by blast
qed
lemma max2_greater:
assumes "a ∈ Field r" and "b ∈ Field r"
shows "(a, max2 a b) ∈ r ∧ (b, max2 a b) ∈ r"
using assms by (auto simp add: max2_greater_among)
lemma max2_among:
assumes "a ∈ Field r" and "b ∈ Field r"
shows "max2 a b ∈ {a, b}"
using assms max2_greater_among[of a b] by simp
lemma max2_equals1:
assumes "a ∈ Field r" and "b ∈ Field r"
shows "(max2 a b = a) = ((b,a) ∈ r)"
using assms ANTISYM unfolding antisym_def using TOTALS
by(auto simp add: max2_def max2_among)
lemma max2_equals2:
assumes "a ∈ Field r" and "b ∈ Field r"
shows "(max2 a b = b) = ((a,b) ∈ r)"
using assms ANTISYM unfolding antisym_def using TOTALS
unfolding max2_def by auto
lemma in_notinI:
assumes "(j,i) ∉ r ∨ j = i" and "i ∈ Field r" and "j ∈ Field r"
shows "(i,j) ∈ r" using assms max2_def max2_greater_among by fastforce
subsubsection ‹Existence and uniqueness for isMinim and well-definedness of minim›
lemma isMinim_unique:
assumes "isMinim B a" "isMinim B a'"
shows "a = a'"
using assms ANTISYM antisym_def[of r] by (auto simp: isMinim_def)
lemma Well_order_isMinim_exists:
assumes SUB: "B ≤ Field r" and NE: "B ≠ {}"
shows "∃b. isMinim B b"
proof-
from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
*: "b ∈ B ∧ (∀b'. b' ≠ b ∧ (b',b) ∈ r ⟶ b' ∉ B)" by auto
have "∀b'. b' ∈ B ⟶ (b, b') ∈ r"
proof
fix b'
show "b' ∈ B ⟶ (b, b') ∈ r"
proof
assume As: "b' ∈ B"
hence **: "b ∈ Field r ∧ b' ∈ Field r" using As SUB * by auto
from As * have "b' = b ∨ (b',b) ∉ r" by auto
moreover have "b' = b ⟹ (b, b') ∈ r"
using ** REFL by (auto simp add: refl_on_def)
moreover have "b' ≠ b ∧ (b',b) ∉ r ⟹ (b,b') ∈ r"
using ** TOTAL by (auto simp add: total_on_def)
ultimately show "(b,b') ∈ r" by blast
qed
qed
then show ?thesis
unfolding isMinim_def using * by auto
qed
lemma minim_isMinim:
assumes SUB: "B ≤ Field r" and NE: "B ≠ {}"
shows "isMinim B (minim B)"
proof-
let ?phi = "(λ b. isMinim B b)"
from assms Well_order_isMinim_exists
obtain b where *: "?phi b" by blast
moreover
have "⋀ b'. ?phi b' ⟹ b' = b"
using isMinim_unique * by auto
ultimately show ?thesis
unfolding minim_def using theI[of ?phi b] by blast
qed
subsubsection‹Properties of minim›
lemma minim_in:
assumes "B ≤ Field r" and "B ≠ {}"
shows "minim B ∈ B"
using assms minim_isMinim[of B] by (auto simp: isMinim_def)
lemma minim_inField:
assumes "B ≤ Field r" and "B ≠ {}"
shows "minim B ∈ Field r"
proof-
have "minim B ∈ B" using assms by (simp add: minim_in)
thus ?thesis using assms by blast
qed
lemma minim_least:
assumes SUB: "B ≤ Field r" and IN: "b ∈ B"
shows "(minim B, b) ∈ r"
proof-
from minim_isMinim[of B] assms
have "isMinim B (minim B)" by auto
thus ?thesis by (auto simp add: isMinim_def IN)
qed
lemma equals_minim:
assumes SUB: "B ≤ Field r" and IN: "a ∈ B" and
LEAST: "⋀ b. b ∈ B ⟹ (a,b) ∈ r"
shows "a = minim B"
proof-
from minim_isMinim[of B] assms
have "isMinim B (minim B)" by auto
moreover have "isMinim B a" using IN LEAST isMinim_def by auto
ultimately show ?thesis
using isMinim_unique by auto
qed
subsubsection‹Properties of successor›
lemma suc_AboveS:
assumes SUB: "B ≤ Field r" and ABOVES: "AboveS B ≠ {}"
shows "suc B ∈ AboveS B"
proof(unfold suc_def)
have "AboveS B ≤ Field r"
using AboveS_Field[of r] by auto
thus "minim (AboveS B) ∈ AboveS B"
using assms by (simp add: minim_in)
qed
lemma suc_greater:
assumes SUB: "B ≤ Field r" and ABOVES: "AboveS B ≠ {}" and IN: "b ∈ B"
shows "suc B ≠ b ∧ (b,suc B) ∈ r"
using IN AboveS_def[of r] assms suc_AboveS by auto
lemma suc_least_AboveS:
assumes ABOVES: "a ∈ AboveS B"
shows "(suc B,a) ∈ r"
using assms minim_least AboveS_Field[of r] by (auto simp: suc_def)
lemma suc_inField:
assumes "B ≤ Field r" and "AboveS B ≠ {}"
shows "suc B ∈ Field r"
using suc_AboveS assms AboveS_Field[of r] by auto
lemma equals_suc_AboveS:
assumes "B ≤ Field r" and "a ∈ AboveS B" and "⋀ a'. a' ∈ AboveS B ⟹ (a,a') ∈ r"
shows "a = suc B"
using assms equals_minim AboveS_Field[of r B] by (auto simp: suc_def)
lemma suc_underS:
assumes IN: "a ∈ Field r"
shows "a = suc (underS a)"
proof-
have "underS a ≤ Field r"
using underS_Field[of r] by auto
moreover
have "a ∈ AboveS (underS a)"
using in_AboveS_underS IN by fast
moreover
have "∀a' ∈ AboveS (underS a). (a,a') ∈ r"
proof(clarify)
fix a'
assume *: "a' ∈ AboveS (underS a)"
hence **: "a' ∈ Field r"
using AboveS_Field by fast
{assume "(a,a') ∉ r"
hence "a' = a ∨ (a',a) ∈ r"
using TOTAL IN ** by (auto simp add: total_on_def)
moreover
{assume "a' = a"
hence "(a,a') ∈ r"
using REFL IN ** by (auto simp add: refl_on_def)
}
moreover
{assume "a' ≠ a ∧ (a',a) ∈ r"
hence "a' ∈ underS a"
unfolding underS_def by simp
hence "a' ∉ AboveS (underS a)"
using AboveS_disjoint by fast
with * have False by simp
}
ultimately have "(a,a') ∈ r" by blast
}
thus "(a, a') ∈ r" by blast
qed
ultimately show ?thesis
using equals_suc_AboveS by auto
qed
subsubsection ‹Properties of order filters›
lemma under_ofilter: "ofilter (under a)"
using TRANS by (auto simp: ofilter_def under_def Field_iff trans_def)
lemma underS_ofilter: "ofilter (underS a)"
unfolding ofilter_def underS_def under_def
proof safe
fix b assume "(a, b) ∈ r" "(b, a) ∈ r" and DIFF: "b ≠ a"
thus False
using ANTISYM antisym_def[of r] by blast
next
fix b x
assume "(b,a) ∈ r" "b ≠ a" "(x,b) ∈ r"
thus "(x,a) ∈ r"
using TRANS trans_def[of r] by blast
next
fix x
assume "x ≠ a" and "(x, a) ∈ r"
then show "x ∈ Field r"
unfolding Field_def
by auto
qed
lemma Field_ofilter:
"ofilter (Field r)"
by(unfold ofilter_def under_def, auto simp add: Field_def)
lemma ofilter_underS_Field:
"ofilter A = ((∃a ∈ Field r. A = underS a) ∨ (A = Field r))"
proof
assume "(∃a∈Field r. A = underS a) ∨ A = Field r"
thus "ofilter A"
by (auto simp: underS_ofilter Field_ofilter)
next
assume *: "ofilter A"
let ?One = "(∃a∈Field r. A = underS a)"
let ?Two = "(A = Field r)"
show "?One ∨ ?Two"
proof(cases ?Two)
let ?B = "(Field r) - A"
let ?a = "minim ?B"
assume "A ≠ Field r"
moreover have "A ≤ Field r" using * ofilter_def by simp
ultimately have 1: "?B ≠ {}" by blast
hence 2: "?a ∈ Field r" using minim_inField[of ?B] by blast
have 3: "?a ∈ ?B" using minim_in[of ?B] 1 by blast
hence 4: "?a ∉ A" by blast
have 5: "A ≤ Field r" using * ofilter_def by auto
moreover
have "A = underS ?a"
proof
show "A ≤ underS ?a"
proof
fix x assume **: "x ∈ A"
hence 11: "x ∈ Field r" using 5 by auto
have 12: "x ≠ ?a" using 4 ** by auto
have 13: "under x ≤ A" using * ofilter_def ** by auto
{assume "(x,?a) ∉ r"
hence "(?a,x) ∈ r"
using TOTAL total_on_def[of "Field r" r]
2 4 11 12 by auto
hence "?a ∈ under x" using under_def[of r] by auto
hence "?a ∈ A" using ** 13 by blast
with 4 have False by simp
}
then have "(x,?a) ∈ r" by blast
thus "x ∈ underS ?a"
unfolding underS_def by (auto simp add: 12)
qed
next
show "underS ?a ≤ A"
proof
fix x
assume **: "x ∈ underS ?a"
hence 11: "x ∈ Field r"
using Field_def unfolding underS_def by fastforce
{assume "x ∉ A"
hence "x ∈ ?B" using 11 by auto
hence "(?a,x) ∈ r" using 3 minim_least[of ?B x] by blast
hence False
using ANTISYM antisym_def[of r] ** unfolding underS_def by auto
}
thus "x ∈ A" by blast
qed
qed
ultimately have ?One using 2 by blast
thus ?thesis by simp
next
assume "A = Field r"
then show ?thesis
by simp
qed
qed
lemma ofilter_UNION:
"(⋀ i. i ∈ I ⟹ ofilter(A i)) ⟹ ofilter (⋃i ∈ I. A i)"
unfolding ofilter_def by blast
lemma ofilter_under_UNION:
assumes "ofilter A"
shows "A = (⋃a ∈ A. under a)"
proof
have "∀a ∈ A. under a ≤ A"
using assms ofilter_def by auto
thus "(⋃a ∈ A. under a) ≤ A" by blast
next
have "∀a ∈ A. a ∈ under a"
using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
thus "A ≤ (⋃a ∈ A. under a)" by blast
qed
subsubsection‹Other properties›
lemma ofilter_linord:
assumes OF1: "ofilter A" and OF2: "ofilter B"
shows "A ≤ B ∨ B ≤ A"
proof(cases "A = Field r")
assume Case1: "A = Field r"
hence "B ≤ A" using OF2 ofilter_def by auto
thus ?thesis by simp
next
assume Case2: "A ≠ Field r"
with ofilter_underS_Field OF1 obtain a where
1: "a ∈ Field r ∧ A = underS a" by auto
show ?thesis
proof(cases "B = Field r")
assume Case21: "B = Field r"
hence "A ≤ B" using OF1 ofilter_def by auto
thus ?thesis by simp
next
assume Case22: "B ≠ Field r"
with ofilter_underS_Field OF2 obtain b where
2: "b ∈ Field r ∧ B = underS b" by auto
have "a = b ∨ (a,b) ∈ r ∨ (b,a) ∈ r"
using 1 2 TOTAL total_on_def[of _ r] by auto
moreover
{assume "a = b" with 1 2 have ?thesis by auto
}
moreover
{assume "(a,b) ∈ r"
with underS_incr[of r] TRANS ANTISYM 1 2
have "A ≤ B" by auto
hence ?thesis by auto
}
moreover
{assume "(b,a) ∈ r"
with underS_incr[of r] TRANS ANTISYM 1 2
have "B ≤ A" by auto
hence ?thesis by auto
}
ultimately show ?thesis by blast
qed
qed
lemma ofilter_AboveS_Field:
assumes "ofilter A"
shows "A ∪ (AboveS A) = Field r"
proof
show "A ∪ (AboveS A) ≤ Field r"
using assms ofilter_def AboveS_Field[of r] by auto
next
{fix x assume *: "x ∈ Field r" and **: "x ∉ A"
{fix y assume ***: "y ∈ A"
with ** have 1: "y ≠ x" by auto
{assume "(y,x) ∉ r"
moreover
have "y ∈ Field r" using assms ofilter_def *** by auto
ultimately have "(x,y) ∈ r"
using 1 * TOTAL total_on_def[of _ r] by auto
with *** assms ofilter_def under_def[of r] have "x ∈ A" by auto
with ** have False by contradiction
}
hence "(y,x) ∈ r" by blast
with 1 have "y ≠ x ∧ (y,x) ∈ r" by auto
}
with * have "x ∈ AboveS A" unfolding AboveS_def by auto
}
thus "Field r ≤ A ∪ (AboveS A)" by blast
qed
lemma suc_ofilter_in:
assumes OF: "ofilter A" and ABOVE_NE: "AboveS A ≠ {}" and
REL: "(b,suc A) ∈ r" and DIFF: "b ≠ suc A"
shows "b ∈ A"
proof-
have *: "suc A ∈ Field r ∧ b ∈ Field r"
using WELL REL well_order_on_domain[of "Field r"] by auto
{assume **: "b ∉ A"
hence "b ∈ AboveS A"
using OF * ofilter_AboveS_Field by auto
hence "(suc A, b) ∈ r"
using suc_least_AboveS by auto
hence False using REL DIFF ANTISYM *
by (auto simp add: antisym_def)
}
thus ?thesis by blast
qed
end
end