section ‹The Bourbaki-Witt tower construction for transfinite iteration›
theory Bourbaki_Witt_Fixpoint imports Main begin
lemma ChainsI [intro?]:
"(⋀a b. ⟦ a ∈ Y; b ∈ Y ⟧ ⟹ (a, b) ∈ r ∨ (b, a) ∈ r) ⟹ Y ∈ Chains r"
unfolding Chains_def by blast
lemma in_Chains_subset: "⟦ M ∈ Chains r; M' ⊆ M ⟧ ⟹ M' ∈ Chains r"
by(auto simp add: Chains_def)
lemma FieldI1: "(i, j) ∈ R ⟹ i ∈ Field R"
unfolding Field_def by auto
lemma Chains_FieldD: "⟦ M ∈ Chains r; x ∈ M ⟧ ⟹ x ∈ Field r"
by(auto simp add: Chains_def intro: FieldI1 FieldI2)
lemma in_Chains_conv_chain: "M ∈ Chains r ⟷ Complete_Partial_Order.chain (λx y. (x, y) ∈ r) M"
by(simp add: Chains_def chain_def)
lemma partial_order_on_trans:
"⟦ partial_order_on A r; (x, y) ∈ r; (y, z) ∈ r ⟧ ⟹ (x, z) ∈ r"
by(auto simp add: order_on_defs dest: transD)
locale bourbaki_witt_fixpoint =
fixes lub :: "'a set ⇒ 'a"
and leq :: "('a × 'a) set"
and f :: "'a ⇒ 'a"
assumes po: "Partial_order leq"
and lub_least: "⟦ M ∈ Chains leq; M ≠ {}; ⋀x. x ∈ M ⟹ (x, z) ∈ leq ⟧ ⟹ (lub M, z) ∈ leq"
and lub_upper: "⟦ M ∈ Chains leq; x ∈ M ⟧ ⟹ (x, lub M) ∈ leq"
and lub_in_Field: "⟦ M ∈ Chains leq; M ≠ {} ⟧ ⟹ lub M ∈ Field leq"
and increasing: "⋀x. x ∈ Field leq ⟹ (x, f x) ∈ leq"
begin
lemma leq_trans: "⟦ (x, y) ∈ leq; (y, z) ∈ leq ⟧ ⟹ (x, z) ∈ leq"
by(rule partial_order_on_trans[OF po])
lemma leq_refl: "x ∈ Field leq ⟹ (x, x) ∈ leq"
using po by(simp add: order_on_defs refl_on_def)
lemma leq_antisym: "⟦ (x, y) ∈ leq; (y, x) ∈ leq ⟧ ⟹ x = y"
using po by(simp add: order_on_defs antisym_def)
inductive_set iterates_above :: "'a ⇒ 'a set"
for a
where
base: "a ∈ iterates_above a"
| step: "x ∈ iterates_above a ⟹ f x ∈ iterates_above a"
| Sup: "⟦ M ∈ Chains leq; M ≠ {}; ⋀x. x ∈ M ⟹ x ∈ iterates_above a ⟧ ⟹ lub M ∈ iterates_above a"
definition fixp_above :: "'a ⇒ 'a"
where "fixp_above a = (if a ∈ Field leq then lub (iterates_above a) else a)"
lemma fixp_above_outside: "a ∉ Field leq ⟹ fixp_above a = a"
by(simp add: fixp_above_def)
lemma fixp_above_inside: "a ∈ Field leq ⟹ fixp_above a = lub (iterates_above a)"
by(simp add: fixp_above_def)
context
notes leq_refl [intro!, simp]
and base [intro]
and step [intro]
and Sup [intro]
and leq_trans [trans]
begin
lemma iterates_above_le_f: "⟦ x ∈ iterates_above a; a ∈ Field leq ⟧ ⟹ (x, f x) ∈ leq"
by(induction x rule: iterates_above.induct)(blast intro: increasing FieldI2 lub_in_Field)+
lemma iterates_above_Field: "⟦ x ∈ iterates_above a; a ∈ Field leq ⟧ ⟹ x ∈ Field leq"
by(drule (1) iterates_above_le_f)(rule FieldI1)
lemma iterates_above_ge:
assumes y: "y ∈ iterates_above a"
and a: "a ∈ Field leq"
shows "(a, y) ∈ leq"
using y by(induction)(auto intro: a increasing iterates_above_le_f leq_trans leq_trans[OF _ lub_upper])
lemma iterates_above_lub:
assumes M: "M ∈ Chains leq"
and nempty: "M ≠ {}"
and upper: "⋀y. y ∈ M ⟹ ∃z ∈ M. (y, z) ∈ leq ∧ z ∈ iterates_above a"
shows "lub M ∈ iterates_above a"
proof -
let ?M = "M ∩ iterates_above a"
from M have M': "?M ∈ Chains leq" by(rule in_Chains_subset)simp
have "?M ≠ {}" using nempty by(auto dest: upper)
with M' have "lub ?M ∈ iterates_above a" by(rule Sup) blast
also have "lub ?M = lub M" using nempty
by(intro leq_antisym)(blast intro!: lub_least[OF M] lub_least[OF M'] intro: lub_upper[OF M'] lub_upper[OF M] leq_trans dest: upper)+
finally show ?thesis .
qed
lemma iterates_above_successor:
assumes y: "y ∈ iterates_above a"
and a: "a ∈ Field leq"
shows "y = a ∨ y ∈ iterates_above (f a)"
using y
proof induction
case base thus ?case by simp
next
case (step x) thus ?case by auto
next
case (Sup M)
show ?case
proof(cases "∃x. M ⊆ {x}")
case True
with ‹M ≠ {}› obtain y where M: "M = {y}" by auto
have "lub M = y"
by(rule leq_antisym)(auto intro!: lub_upper Sup lub_least ChainsI simp add: a M Sup.hyps(3)[of y, THEN iterates_above_Field] dest: iterates_above_Field)
with Sup.IH[of y] M show ?thesis by simp
next
case False
from Sup(1-2) have "lub M ∈ iterates_above (f a)"
proof(rule iterates_above_lub)
fix y
assume y: "y ∈ M"
from Sup.IH[OF this] show "∃z∈M. (y, z) ∈ leq ∧ z ∈ iterates_above (f a)"
proof
assume "y = a"
from y False obtain z where z: "z ∈ M" and neq: "y ≠ z" by (metis insertI1 subsetI)
with Sup.IH[OF z] ‹y = a› Sup.hyps(3)[OF z]
show ?thesis by(auto dest: iterates_above_ge intro: a)
next
assume "y ∈ iterates_above (f a)"
moreover with increasing[OF a] have "y ∈ Field leq"
by(auto dest!: iterates_above_Field intro: FieldI2)
ultimately show ?thesis using y by(auto)
qed
qed
thus ?thesis by simp
qed
qed
lemma iterates_above_Sup_aux:
assumes M: "M ∈ Chains leq" "M ≠ {}"
and M': "M' ∈ Chains leq" "M' ≠ {}"
and comp: "⋀x. x ∈ M ⟹ x ∈ iterates_above (lub M') ∨ lub M' ∈ iterates_above x"
shows "(lub M, lub M') ∈ leq ∨ lub M ∈ iterates_above (lub M')"
proof(cases "∃x ∈ M. x ∈ iterates_above (lub M')")
case True
then obtain x where x: "x ∈ M" "x ∈ iterates_above (lub M')" by blast
have lub_M': "lub M' ∈ Field leq" using M' by(rule lub_in_Field)
have "lub M ∈ iterates_above (lub M')" using M
proof(rule iterates_above_lub)
fix y
assume y: "y ∈ M"
from comp[OF y] show "∃z∈M. (y, z) ∈ leq ∧ z ∈ iterates_above (lub M')"
proof
assume "y ∈ iterates_above (lub M')"
from this iterates_above_Field[OF this] y lub_M' show ?thesis by blast
next
assume "lub M' ∈ iterates_above y"
hence "(y, lub M') ∈ leq" using Chains_FieldD[OF M(1) y] by(rule iterates_above_ge)
also have "(lub M', x) ∈ leq" using x(2) lub_M' by(rule iterates_above_ge)
finally show ?thesis using x by blast
qed
qed
thus ?thesis ..
next
case False
have "(lub M, lub M') ∈ leq" using M
proof(rule lub_least)
fix x
assume x: "x ∈ M"
from comp[OF x] x False have "lub M' ∈ iterates_above x" by auto
moreover from M(1) x have "x ∈ Field leq" by(rule Chains_FieldD)
ultimately show "(x, lub M') ∈ leq" by(rule iterates_above_ge)
qed
thus ?thesis ..
qed
lemma iterates_above_triangle:
assumes x: "x ∈ iterates_above a"
and y: "y ∈ iterates_above a"
and a: "a ∈ Field leq"
shows "x ∈ iterates_above y ∨ y ∈ iterates_above x"
using x y
proof(induction arbitrary: y)
case base then show ?case by simp
next
case (step x) thus ?case using a
by(auto dest: iterates_above_successor intro: iterates_above_Field)
next
case x: (Sup M)
hence lub: "lub M ∈ iterates_above a" by blast
from ‹y ∈ iterates_above a› show ?case
proof(induction)
case base show ?case using lub by simp
next
case (step y) thus ?case using a
by(auto dest: iterates_above_successor intro: iterates_above_Field)
next
case y: (Sup M')
hence lub': "lub M' ∈ iterates_above a" by blast
have *: "x ∈ iterates_above (lub M') ∨ lub M' ∈ iterates_above x" if "x ∈ M" for x
using that lub' by(rule x.IH)
with x(1-2) y(1-2) have "(lub M, lub M') ∈ leq ∨ lub M ∈ iterates_above (lub M')"
by(rule iterates_above_Sup_aux)
moreover from y(1-2) x(1-2) have "(lub M', lub M) ∈ leq ∨ lub M' ∈ iterates_above (lub M)"
by(rule iterates_above_Sup_aux)(blast dest: y.IH)
ultimately show ?case by(auto 4 3 dest: leq_antisym)
qed
qed
lemma chain_iterates_above:
assumes a: "a ∈ Field leq"
shows "iterates_above a ∈ Chains leq" (is "?C ∈ _")
proof (rule ChainsI)
fix x y
assume "x ∈ ?C" "y ∈ ?C"
hence "x ∈ iterates_above y ∨ y ∈ iterates_above x" using a by(rule iterates_above_triangle)
moreover from ‹x ∈ ?C› a have "x ∈ Field leq" by(rule iterates_above_Field)
moreover from ‹y ∈ ?C› a have "y ∈ Field leq" by(rule iterates_above_Field)
ultimately show "(x, y) ∈ leq ∨ (y, x) ∈ leq" by(auto dest: iterates_above_ge)
qed
lemma fixp_iterates_above: "fixp_above a ∈ iterates_above a"
by(auto intro: chain_iterates_above simp add: fixp_above_def)
lemma fixp_above_Field: "a ∈ Field leq ⟹ fixp_above a ∈ Field leq"
using fixp_iterates_above by(rule iterates_above_Field)
lemma fixp_above_unfold:
assumes a: "a ∈ Field leq"
shows "fixp_above a = f (fixp_above a)" (is "?a = f ?a")
proof(rule leq_antisym)
show "(?a, f ?a) ∈ leq" using fixp_above_Field[OF a] by(rule increasing)
have "f ?a ∈ iterates_above a" using fixp_iterates_above by(rule iterates_above.step)
with chain_iterates_above[OF a] show "(f ?a, ?a) ∈ leq"
by(simp add: fixp_above_inside assms lub_upper)
qed
end
lemma fixp_induct [case_names adm base step]:
assumes adm: "ccpo.admissible lub (λx y. (x, y) ∈ leq) P"
and base: "P a"
and step: "⋀x. P x ⟹ P (f x)"
shows "P (fixp_above a)"
proof(cases "a ∈ Field leq")
case True
from adm chain_iterates_above[OF True]
show ?thesis unfolding fixp_above_inside[OF True] in_Chains_conv_chain
proof(rule ccpo.admissibleD)
have "a ∈ iterates_above a" ..
then show "iterates_above a ≠ {}" by(auto)
show "P x" if "x ∈ iterates_above a" for x using that
by induction(auto intro: base step simp add: in_Chains_conv_chain dest: ccpo.admissibleD[OF adm])
qed
qed(simp add: fixp_above_outside base)
end
end