Theory Fixed_Points
theory Fixed_Points
imports Complete_Relations Directedness
begin
section ‹Existence of Fixed Points in Complete Related Sets›
text ‹\label{sec:qfp-exists}›
text ‹The following proof is simplified and generalized from
Stouti--Maaden \cite{SM13}. We construct some set whose extreme bounds
-- if they exist, typically when the underlying related set is complete --
are fixed points of a monotone or inflationary function on any
related set. When the related set is attractive, those are actually the least fixed points.
This generalizes \cite{SM13}, relaxing reflexivity and antisymmetry.›
locale fixed_point_proof = related_set +
fixes f
assumes f: "f ` A ⊆ A"
begin
sublocale less_eq_asymmetrize.
definition AA where "AA ≡
{X. X ⊆ A ∧ f ` X ⊆ X ∧ (∀Y s. Y ⊆ X ⟶ extreme_bound A (⊑) Y s ⟶ s ∈ X)}"
lemma AA_I:
"X ⊆ A ⟹ f ` X ⊆ X ⟹ (⋀Y s. Y ⊆ X ⟹ extreme_bound A (⊑) Y s ⟹ s ∈ X) ⟹ X ∈ AA"
by (unfold AA_def, safe)
lemma AA_E:
"X ∈ AA ⟹
(X ⊆ A ⟹ f ` X ⊆ X ⟹ (⋀Y s. Y ⊆ X ⟹ extreme_bound A (⊑) Y s ⟹ s ∈ X) ⟹ thesis) ⟹ thesis"
by (auto simp: AA_def)
definition C where "C ≡ ⋂ AA"
lemma A_AA: "A ∈ AA" by (auto intro!:AA_I f)
lemma C_AA: "C ∈ AA"
proof (intro AA_I)
show "C ⊆ A" using C_def A_AA f by auto
show "f ` C ⊆ C" unfolding C_def AA_def by auto
fix B b assume B: "B ⊆ C" "extreme_bound A (⊑) B b"
{ fix X assume X: "X ∈ AA"
with B have "B ⊆ X" by (auto simp: C_def)
with X B have "b∈X" by (auto elim!: AA_E)
}
then show "b ∈ C" by (auto simp: C_def AA_def)
qed
lemma CA: "C ⊆ A" using A_AA by (auto simp: C_def)
lemma fC: "f ` C ⊆ C" using C_AA by (auto elim!: AA_E)
context
fixes c assumes Cc: "extreme_bound A (⊑) C c"
begin
private lemma cA: "c ∈ A" using Cc by auto
private lemma cC: "c ∈ C" using Cc C_AA by (blast elim!:AA_E)
private lemma fcC: "f c ∈ C" using cC AA_def C_AA by auto
private lemma fcA: "f c ∈ A" using fcC CA by auto
lemma qfp_as_extreme_bound:
assumes infl_mono: "∀x ∈ A. x ⊑ f x ∨ (∀y ∈ A. y ⊑ x ⟶ f y ⊑ f x)"
shows "f c ∼ c"
proof (intro conjI bexI sympartpI)
show "f c ⊑ c" using fcC Cc by auto
from infl_mono[rule_format, OF cA]
show "c ⊑ f c"
proof (safe)
text ‹Monotone case:›
assume mono: "∀b∈A. b ⊑ c ⟶ f b ⊑ f c"
define D where "D ≡ {x ∈ C. x ⊑ f c}"
have "D ∈ AA"
proof (intro AA_I)
show "D ⊆ A" unfolding D_def C_def using A_AA f by auto
have fxC: "x ∈ C ⟹ x ⊑ f c ⟹ f x ∈ C" for x using C_AA by (auto simp: AA_def)
show "f ` D ⊆ D"
proof (unfold D_def, safe intro!: fxC)
fix x assume xC: "x ∈ C"
have "x ⊑ c" "x ∈ A" using Cc xC CA by auto
then show "f x ⊑ f c" using mono by (auto dest:monotoneD)
qed
have DC: "D ⊆ C" unfolding D_def by auto
fix B b assume BD: "B ⊆ D" and Bb: "extreme_bound A (⊑) B b"
have "B ⊆ C" using DC BD by auto
then have bC: "b ∈ C" using C_AA Bb BD by (auto elim!: AA_E)
have bfc: "∀a∈B. a ⊑ f c" using BD unfolding D_def by auto
with f cA Bb
have "b ⊑ f c" by (auto simp: extreme_def image_subset_iff)
with bC show "b ∈ D" unfolding D_def by auto
qed
then have "C ⊆ D" unfolding C_def by auto
then show "c ⊑ f c" using cC unfolding D_def by auto
qed
qed
lemma extreme_qfp:
assumes attract: "∀q ∈ A. ∀x ∈ A. f q ∼ q ⟶ x ⊑ f q ⟶ x ⊑ q"
and mono: "monotone_on A (⊑) (⊑) f"
shows "extreme {q ∈ A. f q ∼ q ∨ f q = q} (⊒) c"
proof-
have fcc: "f c ∼ c"
apply (rule qfp_as_extreme_bound)
using mono by (auto elim!: monotone_onE)
define L where [simp]: "L ≡ {a ∈ A. ∀s ∈ A. (f s ∼ s ∨ f s = s) ⟶ a ⊑ s}"
have "L ∈ AA"
proof (unfold AA_def, intro CollectI conjI allI impI)
show XA: "L ⊆ A" by auto
show "f ` L ⊆ L"
proof safe
fix x assume xL: "x ∈ L"
show "f x ∈ L"
proof (unfold L_def, safe)
have xA: "x ∈ A" using xL by auto
then show fxA: "f x ∈ A" using f by auto
{ fix s assume sA: "s ∈ A" and sf: "f s ∼ s ∨ f s = s"
then have "x ⊑ s" using xL sA sf by auto
then have "f x ⊑ f s" using mono fxA sA xA by (auto elim!:monotone_onE)}
note fxfs = this
{ fix s assume sA: "s ∈ A" and sf: "f s ∼ s"
then show "f x ⊑ s" using fxfs attract mono sf fxA sA xA by (auto elim!:monotone_onE)
}
{ fix s assume sA: "s ∈ A" and sf: "f s = s"
with fxfs[OF sA] show "f x ⊑ s" by simp}
qed
qed
fix B b assume BL: "B ⊆ L" and b: "extreme_bound A (⊑) B b"
then have BA: "B ⊆ A" by auto
with BL b have bA: "b ∈ A" by auto
show "b ∈ L"
proof (unfold L_def, safe intro!: bA)
{ fix s assume sA: "s ∈ A" and sf: "f s ∼ s ∨ f s = s"
have "bound B (⊑) s" using sA BL b sf by auto
}
note Bs = this
{ fix s assume sA: "s ∈ A" and sf: "f s ∼ s"
with b sA Bs show "b ⊑ s" by auto
}
{ fix s assume sA: "s ∈ A" and sf: "f s = s"
with b sA Bs show "b ⊑ s" by auto
}
qed
qed
then have "C ⊆ L" by (simp add: C_def Inf_lower)
with cC have "c ∈ L" by auto
with L_def fcc
show ?thesis by auto
qed
end
lemma ex_qfp:
assumes comp: "CC-complete A (⊑)" and C: "CC C (⊑)"
and infl_mono: "∀a ∈ A. a ⊑ f a ∨ (∀b ∈ A. b ⊑ a ⟶ f b ⊑ f a)"
shows "∃s ∈ A. f s ∼ s"
using qfp_as_extreme_bound[OF _ infl_mono] completeD[OF comp CA, OF C] by auto
lemma ex_extreme_qfp_fp:
assumes comp: "CC-complete A (⊑)" and C: "CC C (⊑)"
and attract: "∀q ∈ A. ∀x ∈ A. f q ∼ q ⟶ x ⊑ f q ⟶ x ⊑ q"
and mono: "monotone_on A (⊑) (⊑) f"
shows "∃c. extreme {q ∈ A. f q ∼ q ∨ f q = q} (⊒) c"
using extreme_qfp[OF _ attract mono] completeD[OF comp CA, OF C] by auto
lemma ex_extreme_qfp:
assumes comp: "CC-complete A (⊑)" and C: "CC C (⊑)"
and attract: "∀q ∈ A. ∀x ∈ A. f q ∼ q ⟶ x ⊑ f q ⟶ x ⊑ q"
and mono: "monotone_on A (⊑) (⊑) f"
shows "∃c. extreme {q ∈ A. f q ∼ q} (⊒) c"
proof-
from completeD[OF comp CA, OF C]
obtain c where Cc: "extreme_bound A (⊑) C c" by auto
from extreme_qfp[OF Cc attract mono]
have Qc: "bound {q ∈ A. f q ∼ q} (⊒) c" by auto
have fcc: "f c ∼ c"
apply (rule qfp_as_extreme_bound[OF Cc])
using mono by (auto simp: monotone_onD)
from Cc CA have cA: "c ∈ A" by auto
from Qc fcc cA show ?thesis by (auto intro!: exI[of _ c])
qed
end
context
fixes less_eq :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50) and A :: "'a set" and f
assumes f: "f ` A ⊆ A"
begin
interpretation less_eq_symmetrize.
interpretation fixed_point_proof A "(⊑)" f using f by unfold_locales
theorem complete_infl_mono_imp_ex_qfp:
assumes comp: "⊤-complete A (⊑)" and infl_mono: "∀a∈A. a ⊑ f a ∨ (∀b∈A. b ⊑ a ⟶ f b ⊑ f a)"
shows "∃s∈A. f s ∼ s"
apply (rule ex_qfp[OF comp _ infl_mono]) by auto
end
corollary (in antisymmetric) complete_infl_mono_imp_ex_fp:
assumes comp: "⊤-complete A (⊑)" and f: "f ` A ⊆ A"
and infl_mono: "∀a∈A. a ⊑ f a ∨ (∀b∈A. b ⊑ a ⟶ f b ⊑ f a)"
shows "∃s ∈ A. f s = s"
proof-
interpret less_eq_symmetrize.
from complete_infl_mono_imp_ex_qfp[OF f comp infl_mono]
obtain s where sA: "s ∈ A" and fss: "f s ∼ s" by auto
from f sA have fsA: "f s ∈ A" by auto
have "f s = s" using antisym fsA sA fss by auto
with sA show ?thesis by auto
qed
context semiattractive begin
interpretation less_eq_symmetrize.
theorem complete_mono_imp_ex_extreme_qfp:
assumes comp: "⊤-complete A (⊑)" and f: "f ` A ⊆ A"
and mono: "monotone_on A (⊑) (⊑) f"
shows "∃s. extreme {p ∈ A. f p ∼ p} (⊑) s"
proof-
interpret dual: fixed_point_proof A "(⊒)" rewrites "dual.sym = (∼)"
using f by unfold_locales (auto intro!:ext)
show ?thesis
apply (rule dual.ex_extreme_qfp[OF complete_dual[OF comp] _ _ monotone_on_dual[OF mono]])
apply simp
using f sym_order_trans by blast
qed
end
corollary (in antisymmetric) complete_mono_imp_ex_extreme_fp:
assumes comp: "⊤-complete A (⊑)" and f: "f ` A ⊆ A"
and mono: "monotone_on A (⊑) (⊑) f"
shows "∃s. extreme {s ∈ A. f s = s} (⊑)⇧- s"
proof-
interpret less_eq_symmetrize.
interpret fixed_point_proof A "(⊑)" f using f by unfold_locales
have "∃c. extreme {q ∈ A. f q ∼ q ∨ f q = q} (⊒) c"
apply (rule ex_extreme_qfp_fp[OF comp _ _ mono])
using antisym f by (auto dest: order_sym_trans)
then obtain c where c: "extreme {q ∈ A. f q ∼ q ∨ f q = q} (⊒) c" by auto
then have "f c = c" using antisym f by blast
with c have "extreme {q ∈ A. f q = q} (⊒) c" by auto
then show ?thesis by auto
qed
section ‹Fixed Points in Well-Complete Antisymmetric Sets›
text ‹\label{sec:well-complete}›
text ‹In this section, we prove that an
inflationary or monotone map over a well-complete antisymmetric set
has a fixed point.
In order to formalize such a theorem in Isabelle,
we followed Grall's~\cite{grall10} elementary proof for Bourbaki--Witt and Markowsky's theorems.
His idea is to consider well-founded derivation trees over $A$,
where from a set $C \subseteq A$ of premises
one can derive $f\:(\bigsqcup C)$ if $C$ is a chain.
The main observation is as follows:
Let $D$ be the set of all the derivable elements; that is,
for each $d \in D$ there exists a well-founded derivation
whose root is $d$.
It is shown that $D$ is a chain,
and hence one can build a derivation yielding $f\:(\bigsqcup D)$,
and $f\:(\bigsqcup D)$ is shown to be a fixed point.›
lemma bound_monotone_on:
assumes mono: "monotone_on A r s f" and XA: "X ⊆ A" and aA: "a ∈ A" and rXa: "bound X r a"
shows "bound (f`X) s (f a)"
proof (safe)
fix x assume xX: "x ∈ X"
from rXa xX have "r x a" by auto
with xX XA mono aA show "s (f x) (f a)" by (auto elim!:monotone_onE)
qed
context fixed_point_proof begin
text ‹To avoid the usage of the axiom of choice, we carefully define derivations so that any derivable element
determines its lower set. This led to the following definition:›
definition "derivation X ≡ X ⊆ A ∧ well_ordered_set X (⊑) ∧
(∀x ∈ X. let Y = {y ∈ X. y ⊏ x} in
(∃y. extreme Y (⊑) y ∧ x = f y) ∨
f ` Y ⊆ Y ∧ extreme_bound A (⊑) Y x)"
lemma empty_derivation: "derivation {}" by (auto simp: derivation_def)
lemma assumes "derivation P"
shows derivation_A: "P ⊆ A" and derivation_well_ordered: "well_ordered_set P (⊑)"
using assms by (auto simp: derivation_def)
lemma derivation_cases[consumes 2, case_names suc lim]:
assumes "derivation X" and "x ∈ X"
and "⋀Y y. Y = {y ∈ X. y ⊏ x} ⟹ extreme Y (⊑) y ⟹ x = f y ⟹ thesis"
and "⋀Y. Y = {y ∈ X. y ⊏ x} ⟹ f ` Y ⊆ Y ⟹ extreme_bound A (⊑) Y x ⟹ thesis"
shows thesis
using assms unfolding derivation_def Let_def by auto
definition "derivable x ≡ ∃X. derivation X ∧ x ∈ X"
lemma derivableI[intro?]: "derivation X ⟹ x ∈ X ⟹ derivable x" by (auto simp: derivable_def)
lemma derivableE: "derivable x ⟹ (⋀P. derivation P ⟹ x ∈ P ⟹ thesis) ⟹ thesis"
by (auto simp: derivable_def)
lemma derivable_A: "derivable x ⟹ x ∈ A" by (auto elim: derivableE dest:derivation_A)
lemma UN_derivations_eq_derivable: "(⋃{P. derivation P}) = {x. derivable x}"
by (auto simp: derivable_def)
end
locale fixed_point_proof2 = fixed_point_proof + antisymmetric +
assumes derivation_infl: "∀X x y. derivation X ⟶ x ∈ X ⟶ y ∈ X ⟶ x ⊑ y ⟶ x ⊑ f y"
and derivation_f_refl: "∀X x. derivation X ⟶ x ∈ X ⟶ f x ⊑ f x"
begin
lemma derivation_lim:
assumes P: "derivation P" and fP: "f ` P ⊆ P" and Pp: "extreme_bound A (⊑) P p"
shows "derivation (P ∪ {p})"
proof (cases "p ∈ P")
case True
with P show ?thesis by (auto simp: insert_absorb)
next
case pP: False
interpret P: well_ordered_set P "(⊑)" using derivation_well_ordered[OF P].
have PA: "P ⊆ A" using derivation_A[OF P].
from Pp have pA: "p ∈ A" by auto
have bp: "bound P (⊑) p" using Pp by auto
then have pp: "p ⊑ p" using Pp by auto
have 1: "y ∈ P ⟶ {x. (x = p ∨ x ∈ P) ∧ x ⊏ y} = {x ∈ P. x ⊏ y}" for y
using Pp by (auto dest!: extreme_bound_imp_bound)
{ fix x assume xP: "x ∈ P" and px: "p ⊑ x"
from xP Pp have "x ⊑ p" by auto
with px have "p = x" using xP PA pA by (auto intro!: antisym)
with xP pP
have "False" by auto
}
note 2 = this
then have 3: "{x. (x = p ∨ x ∈ P) ∧ x ⊏ p} = P" using Pp by (auto intro!: asympartpI)
have wr: "well_ordered_set (P ∪ {p}) (⊑)"
apply (rule well_order_extend[OF P.well_ordered_set_axioms])
using pp bp pP 2 by auto
from P fP Pp
show "derivation (P ∪ {p})" by (auto simp: derivation_def pA wr[simplified] 1 3)
qed
lemma derivation_suc:
assumes P: "derivation P" and Pp: "extreme P (⊑) p" shows "derivation (P ∪ {f p})"
proof (cases "f p ∈ P")
case True
with P show ?thesis by (auto simp: insert_absorb)
next
case fpP: False
interpret P: well_ordered_set P "(⊑)" using derivation_well_ordered[OF P].
have PA: "P ⊆ A" using derivation_A[OF P].
with Pp have pP: "p ∈ P" and pA: "p ∈ A" by auto
with f have fpA: "f p ∈ A" by auto
from pP have pp: "p ⊑ p" by auto
from derivation_infl[rule_format, OF P pP pP pp] have "p ⊑ f p".
{ fix x assume xP: "x ∈ P"
then have xA: "x ∈ A" using PA by auto
have xp: "x ⊑ p" using xP Pp by auto
from derivation_infl[rule_format, OF P xP pP this]
have "x ⊑ f p".
}
note Pfp = this
then have bfp: "bound P (⊑) (f p)" by auto
{ fix y assume yP: "y ∈ P"
note yfp = Pfp[OF yP]
{ assume fpy: "f p ⊑ y"
with yfp have "f p = y" using yP PA pA fpA antisym by auto
with yP fpP have "False" by auto
}
with Pfp yP have "y ⊏ f p" by auto
}
note Pfp = this
have 1: "⋀y. y ∈ P ⟶ {x. (x = f p ∨ x ∈ P) ∧ x ⊏ y} = {x ∈ P. x ⊏ y}"
and 2: "{x. (x = f p ∨ x ∈ P) ∧ x ⊏ f p} = P" using Pfp by auto
have wr: "well_ordered_set (P ∪ {f p}) (⊑)"
apply (rule well_order_extend[OF P.well_ordered_set_axioms singleton_well_ordered])
using Pfp derivation_f_refl[rule_format, OF P pP] by auto
from P Pp
show "derivation (P ∪ {f p})" by (auto simp: derivation_def wr[simplified] 1 2 fpA)
qed
lemma derivable_closed:
assumes x: "derivable x" shows "derivable (f x)"
proof (insert x, elim derivableE)
fix P
assume P: "derivation P" and xP: "x ∈ P"
note PA = derivation_A[OF P]
then have xA: "x ∈ A" using xP by auto
interpret P: well_ordered_set P "(⊑)" using derivation_well_ordered[OF P].
interpret P.asympartp: transitive P "(⊏)" using P.asympartp_transitive.
define Px where "Px ≡ {y. y ∈ P ∧ y ⊏ x} ∪ {x}"
then have PxP: "Px ⊆ P" using xP by auto
have "x ⊑ x" using xP by auto
then have Pxx: "extreme Px (⊑) x" using xP PA by (auto simp: Px_def)
have wr: "well_ordered_set Px (⊑)" using P.well_ordered_subset[OF PxP].
{ fix z y assume zPx: "z ∈ Px" and yP: "y ∈ P" and yz: "y ⊏ z"
then have zP: "z ∈ P" using PxP by auto
have "y ⊏ x"
proof (cases "z = x")
case True
then show ?thesis using yz by auto
next
case False
then have zx: "z ⊏ x" using zPx by (auto simp: Px_def)
from P.asym.trans[OF yz zx yP zP xP] show ?thesis.
qed
}
then have 1: "⋀z. z ∈ Px ⟶ {y ∈ Px. y ⊏ z} = {y ∈ P. y ⊏ z}" using Px_def by blast
have Px: "derivation Px" using PxP PA P by (auto simp: wr derivation_def 1)
from derivation_suc[OF Px Pxx]
show ?thesis by (auto intro!: derivableI)
qed
text ‹The following lemma is derived from Grall's proof. We simplify the claim so that we
consider two elements from one derivation, instead of two derivations.›
lemma derivation_useful:
assumes X: "derivation X" and xX: "x ∈ X" and yX: "y ∈ X" and xy: "x ⊏ y"
shows "f x ⊑ y"
proof-
interpret X: well_ordered_set X "(⊑)" using derivation_well_ordered[OF X].
note XA = derivation_A[OF X]
{ fix x y assume xX: "x ∈ X" and yX: "y ∈ X"
from xX yX have "(x ⊏ y ⟶ f x ⊑ y ∧ f x ∈ X) ∧ (y ⊏ x ⟶ f y ⊑ x ∧ f y ∈ X)"
proof (induct x arbitrary: y)
case (less x)
note xX = ‹x ∈ X› and IHx = this(2)
with XA have xA: "x ∈ A" by auto
from ‹y ∈ X› show ?case
proof (induct y)
case (less y)
note yX = ‹y ∈ X› and IHy = this(2)
with XA have yA: "y ∈ A" by auto
show ?case
proof (rule conjI; intro impI)
assume xy: "x ⊏ y"
from X yX
show "f x ⊑ y ∧ f x ∈ X"
proof (cases rule:derivation_cases)
case (suc Z z)
with XA have zX: "z ∈ X" and zA: "z ∈ A" and zy: "z ⊏ y" and yfz: "y = f z" by auto
from xX zX show ?thesis
proof (cases rule: X.comparable_three_cases)
case xz: less
with IHy[OF zX zy] have fxz: "f x ⊑ z" and fxX: "f x ∈ X" by auto
from derivation_infl[rule_format, OF X fxX zX fxz] have "f x ⊑ y" by (auto simp: yfz)
with fxX show ?thesis by auto
next
case eq
with xX zX have "x = z" by auto
with yX yfz show ?thesis by auto
next
case zx: greater
with IHy[OF zX zy] yfz xy have False by auto
then show ?thesis by auto
qed
next
case (lim Z)
note Z = ‹Z = {z ∈ X. z ⊏ y}› and fZ = ‹f ` Z ⊆ Z›
from xX xy have "x ∈ Z" by (auto simp: Z)
with fZ have "f x ∈ Z" by auto
then have "f x ⊏ y" and "f x ∈ X" by (auto simp: Z)
then show ?thesis by auto
qed
next
assume yx: "y ⊏ x"
from X xX
show "f y ⊑ x ∧ f y ∈ X"
proof (cases rule:derivation_cases)
case (suc Z z)
with XA have zX: "z ∈ X" and zA: "z ∈ A" and zx: "z ⊏ x" and xfz: "x = f z" by auto
from yX zX show ?thesis
proof (cases rule: X.comparable_three_cases)
case yz: less
with IHx[OF zX zx yX] have fyz: "f y ⊑ z" and fyX: "f y ∈ X" by auto
from derivation_infl[rule_format, OF X fyX zX fyz] have "f y ⊑ x" by (auto simp: xfz)
with fyX show ?thesis by auto
next
case eq
with yX zX have "y = z" by auto
with xX xfz show ?thesis by auto
next
case greater
with IHx[OF zX zx yX] xfz yx have False by auto
then show ?thesis by auto
qed
next
case (lim Z)
note Z = ‹Z = {z ∈ X. z ⊏ x}› and fZ = ‹f ` Z ⊆ Z›
from yX yx have "y ∈ Z" by (auto simp: Z)
with fZ have "f y ∈ Z" by auto
then have "f y ⊏ x" and "f y ∈ X" by (auto simp: Z)
then show ?thesis by auto
qed
qed
qed
qed
}
with assms show "f x ⊑ y" by auto
qed
text ‹Next one is the main lemma of this section, stating that elements from two possibly different
derivations are comparable, and moreover the lower one is in the derivation of the upper one.
The latter claim, not found in Grall's proof, is crucial in proving that the union of all
derivations is well-related.›
lemma derivations_cross_compare:
assumes X: "derivation X" and Y: "derivation Y" and xX: "x ∈ X" and yY: "y ∈ Y"
shows "(x ⊏ y ∧ x ∈ Y) ∨ x = y ∨ (y ⊏ x ∧ y ∈ X)"
proof-
{ fix X Y x y
assume X: "derivation X" and Y: "derivation Y" and xX: "x ∈ X" and yY: "y ∈ Y"
interpret X: well_ordered_set X "(⊑)" using derivation_well_ordered[OF X].
interpret X.asympartp: transitive X "(⊏)" using X.asympartp_transitive.
interpret Y: well_ordered_set Y "(⊑)" using derivation_well_ordered[OF Y].
have XA: "X ⊆ A" using derivation_A[OF X].
then have xA: "x ∈ A" using xX by auto
with f have fxA: "f x ∈ A" by auto
have YA: "Y ⊆ A" using derivation_A[OF Y].
then have yA: "y ∈ A" using yY by auto
with f have fyA: "f y ∈ A" by auto
{ fix Z
assume Z: "Z = {z ∈ X. z ⊏ x}"
and fZ: "f ` Z ⊆ Z"
and Zx: "extreme_bound A (⊑) Z x"
and IHx: "∀z ∈ X. z ⊏ x ⟶ (z ⊏ y ∧ z ∈ Y) ∨ z = y ∨ (y ⊏ z ∧ y ∈ X)"
have "(y ⊏ x ∧ y ∈ X) ∨ x ⊑ y"
proof (cases "∃z ∈ Z. y ⊏ z")
case True
then obtain z where zZ: "z ∈ Z" and yz: "y ⊏ z" by auto
from zZ Z have zX: "z ∈ X" and zx: "z ⊏ x" by auto
from IHx[rule_format, OF zX zx] yz have yX: "y ∈ X" by auto
from X.asym.trans[OF yz zx yX zX xX] have "y ⊏ x".
with yX show ?thesis by auto
next
case False
have "bound Z (⊑) y"
proof
fix z assume "z ∈ Z"
then have zX: "z ∈ X" and zx: "z ⊏ x" and nyz: "¬ y ⊏ z" using Z False by auto
with IHx[rule_format, OF zX zx] X show "z ⊑ y" by auto
qed
with yA Zx have xy: "x ⊑ y" by auto
then show ?thesis by auto
qed
}
note lim_any = this
{ fix z Z
assume Z: "Z = {z ∈ X. z ⊏ x}"
and Zz: "extreme Z (⊑) z"
and xfz: "x = f z"
and IHx: "(z ⊏ y ∧ z ∈ Y) ∨ z = y ∨ (y ⊏ z ∧ y ∈ X)"
have zX: "z ∈ X" and zx: "z ⊏ x" using Zz Z by (auto simp: extreme_def)
then have zA: "z ∈ A" using XA by auto
from IHx have "(y ⊏ x ∧ y ∈ X) ∨ x ⊑ y"
proof (elim disjE conjE)
assume zy: "z ⊏ y" and zY: "z ∈ Y"
from derivation_useful[OF Y zY yY zy] xfz have xy: "x ⊑ y" by auto
then show ?thesis by auto
next
assume zy: "z = y"
then have "y ⊏ x" using zx by auto
with zy zX show ?thesis by auto
next
assume yz: "y ⊏ z" and yX: "y ∈ X"
from X.asym.trans[OF yz zx yX zX xX] have "y ⊏ x".
with yX show ?thesis by auto
qed
}
note lim_any this
}
note lim_any = this(1) and suc_any = this(2)
interpret X: well_ordered_set X "(⊑)" using derivation_well_ordered[OF X].
interpret Y: well_ordered_set Y "(⊑)" using derivation_well_ordered[OF Y].
have XA: "X ⊆ A" using derivation_A[OF X].
have YA: "Y ⊆ A" using derivation_A[OF Y].
from xX yY show ?thesis
proof (induct x arbitrary: y)
case (less x)
note xX = ‹x ∈ X› and IHx = this(2)
from xX XA f have xA: "x ∈ A" and fxA: "f x ∈ A" by auto
from ‹y ∈ Y›
show ?case
proof (induct y)
case (less y)
note yY = ‹y ∈ Y› and IHy = less(2)
from yY YA f have yA: "y ∈ A" and fyA: "f y ∈ A" by auto
from X xX show ?case
proof (cases rule: derivation_cases)
case (suc Z z)
note Z = ‹Z = {z ∈ X. z ⊏ x}› and Zz = ‹extreme Z (⊑) z› and xfz = ‹x = f z›
then have zx: "z ⊏ x" and zX: "z ∈ X" by auto
note IHz = IHx[OF zX zx yY]
have 1: "y ⊏ x ∧ y ∈ X ∨ x ⊑ y" using suc_any[OF X Y xX yY Z Zz xfz IHz] IHy by auto
from Y yY show ?thesis
proof (cases rule: derivation_cases)
case (suc W w)
note W = ‹W = {w ∈ Y. w ⊏ y}› and Ww = ‹extreme W (⊑) w› and yfw = ‹y = f w›
then have wY: "w ∈ Y" and wy: "w ⊏ y" by auto
have IHw: "w ⊏ x ∧ w ∈ X ∨ w = x ∨ x ⊏ w ∧ x ∈ Y" using IHy[OF wY wy] by auto
have "x ⊏ y ∧ x ∈ Y ∨ y ⊑ x" using suc_any[OF Y X yY xX W Ww yfw IHw] by auto
with 1 show ?thesis using antisym xA yA by auto
next
case (lim W)
note W = ‹W = {w ∈ Y. w ⊏ y}› and fW = ‹f ` W ⊆ W› and Wy = ‹extreme_bound A (⊑) W y›
have "x ⊏ y ∧ x ∈ Y ∨ y ⊑ x" using lim_any[OF Y X yY xX W fW Wy] IHy by auto
with 1 show ?thesis using antisym xA yA by auto
qed
next
case (lim Z)
note Z = ‹Z = {z ∈ X. z ⊏ x}› and fZ = ‹f ` Z ⊆ Z› and Zx = ‹extreme_bound A (⊑) Z x›
have 1: "y ⊏ x ∧ y ∈ X ∨ x ⊑ y" using lim_any[OF X Y xX yY Z fZ Zx] IHx[OF _ _ yY] by auto
from Y yY show ?thesis
proof (cases rule: derivation_cases)
case (suc W w)
note W = ‹W = {w ∈ Y. w ⊏ y}› and Ww = ‹extreme W (⊑) w› and yfw = ‹y = f w›
then have wY: "w ∈ Y" and wy: "w ⊏ y" by auto
have IHw: "w ⊏ x ∧ w ∈ X ∨ w = x ∨ x ⊏ w ∧ x ∈ Y" using IHy[OF wY wy] by auto
have "x ⊏ y ∧ x ∈ Y ∨ y ⊑ x" using suc_any[OF Y X yY xX W Ww yfw IHw] by auto
with 1 show ?thesis using antisym xA yA by auto
next
case (lim W)
note W = ‹W = {w ∈ Y. w ⊏ y}› and fW = ‹f ` W ⊆ W› and Wy = ‹extreme_bound A (⊑) W y›
have "x ⊏ y ∧ x ∈ Y ∨ y ⊑ x" using lim_any[OF Y X yY xX W fW Wy] IHy by auto
with 1 show ?thesis using antisym xA yA by auto
qed
qed
qed
qed
qed
sublocale derivable: well_ordered_set "{x. derivable x}" "(⊑)"
proof (rule well_ordered_set.intro)
show "antisymmetric {x. derivable x} (⊑)"
apply unfold_locales by (auto dest: derivable_A antisym)
show "well_related_set {x. derivable x} (⊑)"
apply (fold UN_derivations_eq_derivable)
apply (rule closed_UN_well_related)
by (auto dest: derivation_well_ordered derivations_cross_compare well_ordered_set.axioms)
qed
lemma pred_unique:
assumes X: "derivation X" and xX: "x ∈ X"
shows "{z ∈ X. z ⊏ x} = {z. derivable z ∧ z ⊏ x}"
proof
{ fix z assume "z ∈ X" and "z ⊏ x"
then have "derivable z ∧ z ⊏ x" using X by (auto simp: derivable_def)
}
then show "{z ∈ X. z ⊏ x} ⊆ {z. derivable z ∧ z ⊏ x}" by auto
{ fix z assume "derivable z" and zx: "z ⊏ x"
then obtain Y where Y: "derivation Y" and zY: "z ∈ Y" by (auto simp: derivable_def)
then have "z ∈ X" using derivations_cross_compare[OF X Y xX zY] zx by auto
}
then show "{z ∈ X. z ⊏ x} ⊇ {z. derivable z ∧ z ⊏ x}" by auto
qed
text ‹The set of all derivable elements is itself a derivation.›
lemma derivation_derivable: "derivation {x. derivable x}"
apply (unfold derivation_def)
apply (safe intro!: derivable_A derivable.well_ordered_set_axioms elim!: derivableE)
apply (unfold mem_Collect_eq pred_unique[symmetric])
by (auto simp: derivation_def)
text ‹Finally, if the set of all derivable elements admits a supremum, then it is a fixed point.›
context
fixes p
assumes p: "extreme_bound A (⊑) {x. derivable x} p"
begin
lemma sup_derivable_derivable: "derivable p"
using derivation_lim[OF derivation_derivable _ p] derivable_closed
by (auto intro: derivableI)
private lemmas sucp = sup_derivable_derivable[THEN derivable_closed]
lemma sup_derivable_prefixed: "f p ⊑ p" using sucp p by auto
lemma sup_derivable_postfixed: "p ⊑ f p"
apply (rule derivation_infl[rule_format, OF derivation_derivable])
using sup_derivable_derivable by auto
lemma sup_derivable_qfp: "f p ∼ p"
using sup_derivable_prefixed sup_derivable_postfixed by auto
lemma sup_derivable_fp: "f p = p"
using sup_derivable_derivable sucp
by (auto intro!: antisym sup_derivable_prefixed sup_derivable_postfixed simp: derivable_A)
end
end
text "The assumptions are satisfied by monotone functions."
context fixed_point_proof begin
context
assumes ord: "antisymmetric A (⊑)"
begin
interpretation antisymmetric using ord.
context
assumes mono: "monotone_on A (⊑) (⊑) f"
begin
interpretation fixed_point_proof2
proof
show mono_imp_derivation_infl:
"∀X x y. derivation X ⟶ x ∈ X ⟶ y ∈ X ⟶ x ⊑ y ⟶ x ⊑ f y"
proof (intro allI impI)
fix X x y
assume X: "derivation X" and xX: "x ∈ X" and yX: "y ∈ X" and xy: "x ⊑ y"
interpret X: well_ordered_set X "(⊑)" using derivation_well_ordered[OF X].
note XA = derivation_A[OF X]
from xX yX xy show "x ⊑ f y"
proof (induct x)
case (less x)
note IH = this(2) and xX = ‹x ∈ X› and yX = ‹y ∈ X› and xy = ‹x ⊑ y›
from xX yX XA have xA: "x ∈ A" and yA: "y ∈ A" by auto
from X xX show ?case
proof (cases rule: derivation_cases)
case (suc Z z)
then have zX: "z ∈ X" and zsx: "z ⊏ x" and xfz: "x = f z" by auto
then have zx: "z ⊑ x" by auto
from X.trans[OF zx xy zX xX yX] have zy: "z ⊑ y".
from zX XA have zA: "z ∈ A" by auto
from zy monotone_onD[OF mono] zA yA xfz show "x ⊑ f y" by auto
next
case (lim Z)
note Z = ‹Z = {z ∈ X. z ⊏ x}› and Zx = ‹extreme_bound A (⊑) Z x›
from f yA have fyA: "f y ∈ A" by auto
have "bound Z (⊑) (f y)"
proof
fix z assume zZ: "z ∈ Z"
with Z xX have zsx: "z ⊏ x" and zX: "z ∈ X" by auto
then have zx: "z ⊑ x" by auto
from X.trans[OF zx xy zX xX yX] have zy: "z ⊑ y".
from IH[OF zX zsx yX] zy show "z ⊑ f y" by auto
qed
with Zx fyA show ?thesis by auto
qed
qed
qed
show mono_imp_derivation_f_refl:
"∀X x. derivation X ⟶ x ∈ X ⟶ f x ⊑ f x"
proof (intro allI impI)
fix X x
assume X: "derivation X" and xX: "x ∈ X"
interpret X: well_ordered_set X "(⊑)" using derivation_well_ordered[OF X].
note XA = derivation_A[OF X]
from monotone_onD[OF mono] xX XA show "f x ⊑ f x" by auto
qed
qed
lemmas mono_imp_fixed_point_proof2 = fixed_point_proof2_axioms
corollary mono_imp_sup_derivable_fp:
assumes p: "extreme_bound A (⊑) {x. derivable x} p"
shows "f p = p"
by (simp add: sup_derivable_fp[OF p])
lemma mono_imp_sup_derivable_lfp:
assumes p: "extreme_bound A (⊑) {x. derivable x} p"
shows "extreme {q ∈ A. f q = q} (⊒) p"
proof (safe intro!: extremeI)
from p show "p ∈ A" by auto
from sup_derivable_fp[OF p]
show "f p = p".
fix q assume qA: "q ∈ A" and fqq: "f q = q"
have "bound {x. derivable x} (⊑) q"
proof (safe intro!: boundI elim!:derivableE)
fix x X
assume X: "derivation X" and xX: "x ∈ X"
from X interpret well_ordered_set X "(⊑)" by (rule derivation_well_ordered)
from xX show "x ⊑ q"
proof (induct x)
case (less x)
note xP = this(1) and IH = this(2)
with X show ?case
proof (cases rule: derivation_cases)
case (suc Z z)
with IH[of z] have zq: "z ⊑ q" and zX: "z ∈ X" by auto
from monotone_onD[OF mono _ qA zq] zX derivation_A[OF X]
show ?thesis by (auto simp: fqq suc)
next
case lim
with IH have "bound {z ∈ X. z ⊏ x} (⊑) q" by auto
with lim qA show ?thesis by auto
qed
qed
qed
with p qA show "p ⊑ q" by auto
qed
lemma mono_imp_ex_least_fp:
assumes comp: "well_related_set-complete A (⊑)"
shows "∃p. extreme {q ∈ A. f q = q} (⊒) p"
proof-
interpret fixed_point_proof using f by unfold_locales
have "∃p. extreme_bound A (⊑) {x. derivable x} p"
apply (rule completeD[OF comp])
using derivable_A derivable.well_related_set_axioms by auto
then obtain p where p: "extreme_bound A (⊑) {x. derivable x} p" by auto
from p mono_imp_sup_derivable_lfp[OF p] sup_derivable_qfp[OF p]
show ?thesis by auto
qed
end
end
end
text ‹Bourbaki-Witt Theorem on well-complete pseudo-ordered set:›
theorem (in pseudo_ordered_set) well_complete_infl'_imp_ex_fp:
assumes comp: "well_related_set-complete A (⊑)"
and f: "f ` A ⊆ A" and infl: "∀x ∈ A. ∀y ∈ A. x ⊑ y ⟶ x ⊑ f y"
shows "∃p ∈ A. f p = p"
proof-
interpret fixed_point_proof using f by unfold_locales
interpret fixed_point_proof2
proof
show dinfl: "∀X x y. derivation X ⟶ x ∈ X ⟶ y ∈ X ⟶ x ⊑ y ⟶ x ⊑ f y"
using infl by (auto dest!:derivation_A)
show drefl: "∀X x. derivation X ⟶ x ∈ X ⟶ f x ⊑ f x"
using f by (auto dest!: derivation_A)
qed
have "∃p. extreme_bound A (⊑) {x. derivable x} p"
apply (rule completeD[OF comp])
using derivable.well_related_set_axioms derivable_A by auto
with sup_derivable_fp
show ?thesis by auto
qed
text ‹Bourbaki-Witt Theorem on posets:›
corollary (in partially_ordered_set) well_complete_infl_imp_ex_fp:
assumes comp: "well_related_set-complete A (⊑)"
and f: "f ` A ⊆ A" and infl: "∀x ∈ A. x ⊑ f x"
shows "∃p ∈ A. f p = p"
proof (intro well_complete_infl'_imp_ex_fp[OF comp f] ballI impI)
fix x y assume x: "x ∈ A" and y: "y ∈ A" and xy: "x ⊑ y"
from y infl have "y ⊑ f y" by auto
from trans[OF xy this x y] f y show "x ⊑ f y" by auto
qed
section ‹Completeness of (Quasi-)Fixed Points›
text ‹We now prove that, under attractivity, the set of quasi-fixed points is complete.›
definition setwise where "setwise r X Y ≡ ∀x∈X. ∀y∈Y. r x y"
lemmas setwiseI[intro] = setwise_def[unfolded atomize_eq, THEN iffD2, rule_format]
lemmas setwiseE[elim] = setwise_def[unfolded atomize_eq, THEN iffD1, elim_format, rule_format]
context fixed_point_proof begin
abbreviation setwise_less_eq (infix "⊑⇧s" 50) where "(⊑⇧s) ≡ setwise (⊑)"
subsection ‹Least Quasi-Fixed Points for Attractive Relations.›
lemma attract_mono_imp_least_qfp:
assumes attract: "attractive A (⊑)"
and comp: "well_related_set-complete A (⊑)"
and mono: "monotone_on A (⊑) (⊑) f"
shows "∃c. extreme {p ∈ A. f p ∼ p ∨ f p = p} (⊒) c ∧ f c ∼ c"
proof-
interpret attractive using attract by auto
interpret sym: transitive A "(∼)" using sym_transitive.
define ecl ("[_]⇩∼") where "[x]⇩∼ ≡ {y ∈ A. x ∼ y} ∪ {x}" for x
define Q where "Q ≡ {[x]⇩∼ |. x ∈ A}"
{ fix X x assume XQ: "X ∈ Q" and xX: "x ∈ X"
then have XA: "X ⊆ A" by (auto simp: Q_def ecl_def)
then have xA: "x ∈ A" using xX by auto
obtain q where qA: "q ∈ A" and X: "X = [q]⇩∼" using XQ by (auto simp: Q_def)
have xqqx: "x ∼ q ∨ x = q" using X xX by (auto simp: ecl_def)
{fix y assume yX: "y ∈ X"
then have yA: "y ∈ A" using XA by auto
have "y ∼ q ∨ y = q" using yX X by (auto simp: ecl_def)
then have "x ∼ y ∨ y = x" using sym_order_trans xqqx xA qA yA by blast
}
then have 1: "X ⊆ [x]⇩∼" using X qA by (auto simp: ecl_def)
{ fix y assume "y ∈ A" and "x ∼ y ∨ y = x"
then have "q ∼ y ∨ y = q" using sym_order_trans xqqx xA qA by blast
}
then have 2: "X ⊇ [x]⇩∼" using X xX by (auto simp: ecl_def)
from 1 2 have "X = [x]⇩∼" by auto
}
then have XQx: "∀X ∈ Q. ∀x ∈ X. X = [x]⇩∼" by auto
have RSLE_eq: "X ∈ Q ⟹ Y ∈ Q ⟹ x ∈ X ⟹ y ∈ Y ⟹ x ⊑ y ⟹ X ⊑⇧s Y" for X Y x y
proof-
assume XQ: "X ∈ Q" and YQ: "Y ∈ Q" and xX: "x ∈ X" and yY: "y ∈ Y" and xy: "x ⊑ y"
then have XA: "X ⊆ A" and YA: "Y ⊆ A" by (auto simp: Q_def ecl_def)
then have xA: "x ∈ A" and yA: "y ∈ A" using xX yY by auto
{ fix xp yp assume xpX: "xp ∈ X" and ypY: "yp ∈ Y"
then have xpA: "xp ∈ A" and ypA: "yp ∈ A" using XA YA by auto
then have "xp ∼ x ∨ xp = x" using xpX XQx xX XQ by (auto simp: ecl_def)
then have xpy: "xp ⊑ y" using attract[OF _ _ xy xpA xA yA] xy by blast
have "yp ∼ y ∨ yp = y" using ypY XQx yY YQ by (auto simp: ecl_def)
then have "xp ⊑ yp" using dual.attract[OF _ _ xpy ypA yA xpA] xpy by blast
}
then show "X ⊑⇧s Y" using XQ YQ XA YA by auto
qed
have compQ: "well_related_set-complete Q (⊑⇧s)"
proof (intro completeI)
fix XX assume XXQ: "XX ⊆ Q" and XX: "well_related_set XX (⊑⇧s)"
have BA: "⋃XX ⊆ A" using XXQ by (auto simp: Q_def ecl_def)
from XX interpret XX: well_related_set XX "(⊑⇧s)".
interpret UXX: semiattractive "⋃XX" "(⊑)" by (rule semiattractive_subset[OF BA])
have "well_related_set (⋃XX) (⊑)"
proof(unfold_locales)
fix Y assume YXX: "Y ⊆ ⋃XX" and Y0: "Y ≠ {}"
have "{X ∈ XX. X ∩ Y ≠ {}} ≠ {}" using YXX Y0 by auto
from XX.nonempty_imp_ex_extreme[OF _ this]
obtain E where E: "extreme {X ∈ XX. X ∩ Y ≠ {}} (⊑⇧s)⇧- E" by auto
then have "E ∩ Y ≠ {}" by auto
then obtain e where eE: "e ∈ E" and eX: "e ∈ Y" by auto
have "extreme Y (⊒) e"
proof (intro extremeI eX)
fix x assume xY: "x ∈ Y"
with YXX obtain X where XXX: "X ∈ XX" and xX: "x ∈ X" by auto
with xY E XXX have "E ⊑⇧s X" by auto
with eE xX show "e ⊑ x" by auto
qed
then show "∃e. extreme Y (⊒) e" by auto
qed
with completeD[OF comp BA]
obtain b where extb: "extreme_bound A (⊑) (⋃XX) b" by auto
then have bb: "b ⊑ b" using extreme_def bound_def by auto
have bA: "b ∈ A" using extb extreme_def by auto
then have XQ: "[b]⇩∼ ∈ Q" using Q_def bA by auto
have bX: "b ∈ [b]⇩∼" by (auto simp: ecl_def)
have "extreme_bound Q (⊑⇧s) XX [b]⇩∼"
proof(intro extreme_boundI)
show "[b]⇩∼ ∈ Q" using XQ.
next
fix Y assume YXX: "Y ∈ XX"
then have YQ: "Y ∈ Q" using XXQ by auto
then obtain y where yA: "y ∈ A" and Yy: "Y = [y]⇩∼" by (auto simp: Q_def)
then have yY: "y ∈ Y" by (auto simp: ecl_def)
then have "y ∈ ⋃XX" using yY YXX by auto
then have "y ⊑ b" using extb by auto
then show "Y ⊑⇧s [b]⇩∼" using RSLE_eq[OF YQ XQ yY bX] by auto
next
fix Z assume boundZ: "bound XX (⊑⇧s) Z" and ZQ: "Z ∈ Q"
then obtain z where zA: "z ∈ A" and Zz: "Z = [z]⇩∼" by (auto simp: Q_def)
then have zZ: "z ∈ Z" by (auto simp: ecl_def)
{ fix y assume "y ∈ ⋃XX"
then obtain Y where yY: "y ∈ Y" and YXX: "Y ∈ XX" by auto
then have YA: "Y ⊆ A" using XXQ Q_def by (auto simp: ecl_def)
then have "Y ⊑⇧s Z" using YXX boundZ bound_def by auto
then have "y ⊑ z" using yY zZ by auto
}
then have "bound (⋃XX) (⊑) z" by auto
then have "b ⊑ z" using extb zA by auto
then show "[b]⇩∼ ⊑⇧s Z" using RSLE_eq[OF XQ ZQ bX zZ] by auto
qed
then show "Ex (extreme_bound Q (⊑⇧s) XX)" by auto
qed
interpret Q: antisymmetric Q "(⊑⇧s)"
proof
fix X Y assume XY: "X ⊑⇧s Y" and YX: "Y ⊑⇧s X" and XQ: "X ∈ Q" and YQ: "Y ∈ Q"
then obtain q where qA: "q ∈ A" and X: "X = [q]⇩∼" using Q_def by auto
then have qX: "q ∈ X" using X by (auto simp: ecl_def)
then obtain p where pA: "p ∈ A" and Y: "Y = [p]⇩∼" using YQ Q_def by auto
then have pY: "p ∈ Y" using X by (auto simp: ecl_def)
have pq: "p ⊑ q" using XQ YQ YX qX pY by auto
have "q ⊑ p" using XQ YQ XY qX pY by auto
then have "p ∈ X" using pq X pA by (auto simp: ecl_def)
then have "X = [p]⇩∼" using XQ XQx by auto
then show "X = Y" using Y by (auto simp: ecl_def)
qed
define F where "F X ≡ {y ∈ A. ∃x ∈ X. y ∼ f x} ∪ f ` X" for X
have XQFXQ: "⋀X. X ∈ Q ⟹ F X ∈ Q"
proof-
fix X assume XQ: "X ∈ Q"
then obtain x where xA: "x ∈ A" and X: "X = [x]⇩∼" using Q_def by auto
then have xX: "x ∈ X" by (auto simp: ecl_def)
have fxA: "f x ∈ A" using xA f by auto
have FXA: "F X ⊆ A" using f fxA X by (auto simp: F_def ecl_def)
have "F X = [f x]⇩∼"
proof (unfold X, intro equalityI subsetI)
fix z assume zFX: "z ∈ F [x]⇩∼"
then obtain y where yX: "y ∈ [x]⇩∼" and zfy: "z ∼ f y ∨ z = f y" by (auto simp: F_def)
have yA: "y ∈ A" using yX xA by (auto simp: ecl_def)
with f have fyA: "f y ∈ A" by auto
have zA: "z ∈ A" using zFX FXA by (auto simp: X)
have "y ∼ x ∨ y = x" using X yX by (auto simp: ecl_def)
then have "f y ∼ f x ∨ f y = f x" using mono xA yA by (auto simp: monotone_on_def)
then have "z ∼ f x ∨ z = f x" using zfy sym.trans[OF _ _ zA fyA fxA] by (auto simp:)
with zA show "z ∈ [f x]⇩∼" by (auto simp: ecl_def)
qed (auto simp: xX F_def ecl_def)
with FXA show "F X ∈ Q" by (auto simp: Q_def ecl_def)
qed
then have F: "F ` Q ⊆ Q" by auto
then interpret Q: fixed_point_proof Q "(⊑⇧s)" F by unfold_locales
have monoQ: "monotone_on Q (⊑⇧s) (⊑⇧s) F"
proof (intro monotone_onI)
fix X Y assume XQ: "X ∈ Q" and YQ: "Y ∈ Q" and XY: "X ⊑⇧s Y"
then obtain x y where xX: "x ∈ X" and yY: "y ∈ Y" using Q_def by (auto simp: ecl_def)
then have xA: "x ∈ A" and yA: "y ∈ A" using XQ YQ by (auto simp: Q_def ecl_def)
have "x ⊑ y" using XY xX yY by auto
then have fxfy: "f x ⊑ f y" using monotone_on_def[of A "(⊑)" "(⊑)" f] xA yA mono by auto
have fxgX: "f x ∈ F X" using xX F_def by blast
have fygY: "f y ∈ F Y" using yY F_def by blast
show "F X ⊑⇧s F Y" using RSLE_eq[OF XQFXQ[OF XQ] XQFXQ[OF YQ] fxgX fygY fxfy].
qed
have QdA: "{x. Q.derivable x} ⊆ Q" using Q.derivable_A by auto
interpret Q: fixed_point_proof2 Q "(⊑⇧s)" F
using Q.mono_imp_fixed_point_proof2[OF Q.antisymmetric_axioms monoQ].
from Q.mono_imp_ex_least_fp[OF Q.antisymmetric_axioms monoQ compQ]
obtain P where P: "extreme {q ∈ Q. F q = q} (⊑⇧s)⇧- P" by auto
then have PQ: "P ∈ Q" by (auto simp: extreme_def)
from P have FPP: "F P = P" using PQ by auto
with P have PP: "P ⊑⇧s P" by auto
from P obtain p where pA: "p ∈ A" and Pp: "P = [p]⇩∼" using Q_def by auto
then have pP: "p ∈ P" by (auto simp: ecl_def)
then have fpA: "f p ∈ A" using pA f by auto
have "f p ∈ F P" using pP F_def fpA by auto
then have "F P = [f p]⇩∼" using XQx XQFXQ[OF PQ] by auto
then have fp: "f p ∼ p ∨ f p = p" using pP FPP by (auto simp: ecl_def)
have "p ⊑ p" using PP pP by auto
with fp have fpp: "f p ∼ p" by auto
have e: "extreme {p ∈ A. f p ∼ p ∨ f p = p} (⊒) p"
proof (intro extremeI CollectI conjI pA fp, elim CollectE conjE)
fix q assume qA: "q ∈ A" and fq: "f q ∼ q ∨ f q = q"
define Z where "Z ≡ {z ∈ A. q ∼ z}∪{q}"
then have qZ: "q ∈ Z" using qA by auto
then have ZQ: "Z ∈ Q" using qA by (auto simp: Z_def Q_def ecl_def)
have fqA: "f q ∈ A" using qA f by auto
then have "f q ∈ Z" using fq by (auto simp: Z_def)
then have 1: "Z = [f q]⇩∼" using XQx ZQ by auto
then have "f q ∈ F Z" using qZ fqA by (auto simp: F_def)
then have "F Z = [f q]⇩∼" using XQx XQFXQ[OF ZQ] by auto
with 1 have "Z = F Z" by auto
then have "P ⊑⇧s Z" using P ZQ by auto
then show "p ⊑ q" using pP qZ by auto
qed
with fpp show ?thesis using e by auto
qed
subsection ‹General Completeness›
lemma attract_mono_imp_fp_qfp_complete:
assumes attract: "attractive A (⊑)"
and comp: "CC-complete A (⊑)"
and wr_CC: "∀C ⊆ A. well_related_set C (⊑) ⟶ CC C (⊑)"
and extend: "∀X Y. CC X (⊑) ⟶ CC Y (⊑) ⟶ X ⊑⇧s Y ⟶ CC (X ∪ Y) (⊑)"
and mono: "monotone_on A (⊑) (⊑) f"
and P: "P ⊆ {x ∈ A. f x = x}"
shows "CC-complete ({q ∈ A. f q ∼ q} ∪ P) (⊑)"
proof (intro completeI)
interpret attractive using attract.
fix X assume Xfix: "X ⊆ {q ∈ A. f q ∼ q} ∪ P" and XCC: "CC X (⊑)"
with P have XA: "X ⊆ A" by auto
define B where "B ≡ {b ∈ A. ∀a ∈ X. a ⊑ b}"
{ fix s a assume sA: "s ∈ A" and as: "∀a ∈ X. a ⊑ s" and aX: "a ∈ X"
then have aA: "a ∈ A" using XA by auto
then have fafs: "f a ⊑ f s" using mono f aX sA as by (auto elim!: monotone_onE)
have "a ⊑ f s"
proof (cases "f a = a")
case True
then show ?thesis using fafs by auto
next
case False
then have "a ∼ f a" using P aX Xfix by auto
also from fafs have "f a ⊑ f s" by auto
finally show ?thesis using f aA sA by auto
qed
}
with f have fBB: "f ` B ⊆ B" unfolding B_def by auto
have BA: "B ⊆ A" by (auto simp: B_def)
have compB: "CC-complete B (⊑)"
proof (unfold complete_def, intro allI impI)
fix Y assume YS: "Y ⊆ B" and YCC: "CC Y (⊑)"
with BA have YA: "Y ⊆ A" by auto
define C where "C ≡ X∪Y"
then have CA: "C ⊆ A" using XA YA C_def by auto
have XY: "X ⊑⇧s Y" using B_def YS by auto
then have CCC: "CC C (⊑)" using extend XA YA XCC YCC C_def by auto
then obtain s where s: "extreme_bound A (⊑) C s"
using completeD[OF comp CA, OF CCC] by auto
then have sA: "s ∈ A" by auto
show "Ex (extreme_bound B (⊑) Y)"
proof (intro exI extreme_boundI)
{ fix x assume "x ∈ X"
then have "x ⊑ s" using s C_def by auto
}
then show "s ∈ B" using sA B_def by auto
next
fix y assume "y ∈ Y"
then show "y ⊑ s" using s C_def using extremeD by auto
next
fix c assume cS: "c ∈ B" and "bound Y (⊑) c"
then have "bound C (⊑) c" using C_def B_def by auto
then show "s ⊑ c" using s BA cS by auto
qed
qed
from fBB interpret B: fixed_point_proof B "(⊑)" f by unfold_locales
from BA have *: "{x ∈ A. f x ∼ x} ∩ B = {x ∈ B. f x ∼ x}" by auto
have asB: "attractive B (⊑)" using attractive_subset[OF BA] by auto
have monoB: "monotone_on B (⊑) (⊑) f" using monotone_on_cmono[OF BA] mono by (auto dest!: le_funD)
have compB: "well_related_set-complete B (⊑)"
using wr_CC compB BA by (simp add: complete_def)
from B.attract_mono_imp_least_qfp[OF asB compB monoB]
obtain l where "extreme {p ∈ B. f p ∼ p ∨ f p = p} (⊒) l" and fll: "f l ∼ l" by auto
with P have l: "extreme ({p ∈ B. f p ∼ p} ∪ P ∩ B) (⊒) l" by auto
show "Ex (extreme_bound ({q ∈ A. f q ∼ q} ∪ P) (⊑) X)"
proof (intro exI extreme_boundI)
show "l ∈ {q ∈ A. f q ∼ q} ∪ P" using l BA by auto
fix a assume "a ∈ X"
with l show "a ⊑ l" by (auto simp: B_def)
next
fix c assume c: "bound X (⊑) c" and cfix: "c ∈ {q ∈ A. f q ∼ q} ∪ P"
with P have cA: "c ∈ A" by auto
with c have "c ∈ B" by (auto simp: B_def)
with cfix l show "l ⊑ c" by auto
qed
qed
lemma attract_mono_imp_qfp_complete:
assumes "attractive A (⊑)"
and "CC-complete A (⊑)"
and "∀C ⊆ A. well_related_set C (⊑) ⟶ CC C (⊑)"
and "∀X Y. CC X (⊑) ⟶ CC Y (⊑) ⟶ X ⊑⇧s Y ⟶ CC (X ∪ Y) (⊑)"
and "monotone_on A (⊑) (⊑) f"
shows "CC-complete {p ∈ A. f p ∼ p} (⊑)"
using attract_mono_imp_fp_qfp_complete[OF assms, of "{}"] by simp
lemma antisym_mono_imp_fp_complete:
assumes anti: "antisymmetric A (⊑)"
and comp: "CC-complete A (⊑)"
and wr_CC: "∀C ⊆ A. well_related_set C (⊑) ⟶ CC C (⊑)"
and extend: "∀X Y. CC X (⊑) ⟶ CC Y (⊑) ⟶ X ⊑⇧s Y ⟶ CC (X ∪ Y) (⊑)"
and mono: "monotone_on A (⊑) (⊑) f"
shows "CC-complete {p ∈ A. f p = p} (⊑)"
proof-
interpret antisymmetric using anti.
have *: "{q ∈ A. f q ∼ q} ⊆ {p ∈ A. f p = p}" using f by (auto intro!: antisym)
from * attract_mono_imp_fp_qfp_complete[OF attractive_axioms comp wr_CC extend mono, of "{p∈A. f p = p}"]
show ?thesis by (auto simp: subset_Un_eq)
qed
end
subsection ‹Instances›
subsubsection ‹Instances under attractivity›
context attractive begin
interpretation less_eq_symmetrize.
text ‹Full completeness›
theorem mono_imp_qfp_complete:
assumes comp: "⊤-complete A (⊑)" and f: "f ` A ⊆ A" and mono: "monotone_on A (⊑) (⊑) f"
shows "⊤-complete {p ∈ A. f p ∼ p} (⊑)"
apply (intro fixed_point_proof.attract_mono_imp_qfp_complete comp mono)
apply unfold_locales
by (auto simp: f)
text ‹Connex completeness›
theorem mono_imp_qfp_connex_complete:
assumes comp: "connex-complete A (⊑)"
and f: "f ` A ⊆ A" and mono: "monotone_on A (⊑) (⊑) f"
shows "connex-complete {p ∈ A. f p ∼ p} (⊑)"
apply (intro fixed_point_proof.attract_mono_imp_qfp_complete mono comp)
apply unfold_locales
by (auto simp: f intro: connex_union well_related_set.connex)
text ‹Directed completeness›
theorem mono_imp_qfp_directed_complete:
assumes comp: "directed-complete A (⊑)"
and f: "f ` A ⊆ A" and mono: "monotone_on A (⊑) (⊑) f"
shows "directed-complete {p ∈ A. f p ∼ p} (⊑)"
apply (intro fixed_point_proof.attract_mono_imp_qfp_complete mono comp)
apply unfold_locales
by (auto simp: f intro!: directed_extend intro: well_related_set.connex connex.directed)
text ‹Well Completeness›
theorem mono_imp_qfp_well_complete:
assumes comp: "well_related_set-complete A (⊑)"
and f: "f ` A ⊆ A" and mono: "monotone_on A (⊑) (⊑) f"
shows "well_related_set-complete {p ∈ A. f p ∼ p} (⊑)"
apply (intro fixed_point_proof.attract_mono_imp_qfp_complete mono comp)
apply unfold_locales
by (auto simp: f well_related_extend)
end
subsubsection ‹Usual instances under antisymmetry ›
context antisymmetric begin
text ‹Knaster--Tarski›
theorem mono_imp_fp_complete:
assumes comp: "⊤-complete A (⊑)"
and f: "f ` A ⊆ A" and mono: "monotone_on A (⊑) (⊑) f"
shows "⊤-complete {p ∈ A. f p = p} (⊑)"
proof-
interpret fixed_point_proof using f by unfold_locales
show ?thesis
apply (intro antisym_mono_imp_fp_complete mono antisymmetric_axioms comp)
by auto
qed
text ‹Markowsky 1976›
theorem mono_imp_fp_connex_complete:
assumes comp: "connex-complete A (⊑)"
and f: "f ` A ⊆ A" and mono: "monotone_on A (⊑) (⊑) f"
shows "connex-complete {p ∈ A. f p = p} (⊑)"
proof-
interpret fixed_point_proof using f by unfold_locales
show ?thesis
apply (intro antisym_mono_imp_fp_complete antisymmetric_axioms mono comp)
by (auto intro: connex_union well_related_set.connex)
qed
text ‹Pataraia›
theorem mono_imp_fp_directed_complete:
assumes comp: "directed-complete A (⊑)"
and f: "f ` A ⊆ A" and mono: "monotone_on A (⊑) (⊑) f"
shows "directed-complete {p ∈ A. f p = p} (⊑)"
proof-
interpret fixed_point_proof using f by unfold_locales
show ?thesis
apply (intro antisym_mono_imp_fp_complete mono antisymmetric_axioms comp)
by (auto intro: directed_extend connex.directed well_related_set.connex)
qed
text ‹Bhatta \& George 2011›
theorem mono_imp_fp_well_complete:
assumes comp: "well_related_set-complete A (⊑)"
and f: "f ` A ⊆ A" and mono: "monotone_on A (⊑) (⊑) f"
shows "well_related_set-complete {p ∈ A. f p = p} (⊑)"
proof-
interpret fixed_point_proof using f by unfold_locales
show ?thesis
apply (intro antisym_mono_imp_fp_complete mono antisymmetric_axioms comp)
by (auto intro!: antisym well_related_extend)
qed
end
end