Theory Kleene_Fixed_Point

theory Kleene_Fixed_Point
  imports Complete_Relations Continuity
begin


section ‹Iterative Fixed Point Theorem›

text ‹Kleene's fixed-point theorem states that,
for a pointed directed complete partial order $\tp{A,\SLE}$
and a Scott-continuous map $f: A \to A$,
the supremum of $\set{f^n(\bot) \mid n\in\Nat}$ exists in $A$ and is a least 
fixed point.
Mashburn \cite{mashburn83} generalized the result so that
$\tp{A,\SLE}$ is a $\omega$-complete partial order
and $f$ is $\omega$-continuous.

In this section we further generalize the result and show that
for $\omega$-complete relation $\tp{A,\SLE}$
and for every bottom element $\bot \in A$,
the set $\set{f^n(\bot) \mid n\in\Nat}$ has suprema (not necessarily unique, of 
course) and, 
they are quasi-fixed points.
Moreover, if $(\SLE)$ is attractive, then the suprema are precisely the least 
quasi-fixed points.›

subsection ‹Existence of Iterative Fixed Points›

text ‹The first part of Kleene's theorem demands to prove that the set 
$\set{f^n(\bot) \mid n \in \Nat}$ has a supremum and 
that all such are quasi-fixed points. We prove this claim without assuming 
anything on the relation $\SLE$ besides $\omega$-completeness and one bottom element.›

notation compower (‹_^_›[1000,1000]1000)

lemma monotone_on_funpow: assumes f: "f ` A ⊆ A" and mono: "monotone_on A r r f"
  shows "monotone_on A r r (f^n)"
proof (induct n)
  case 0
  show ?case using monotone_on_id by (auto simp: id_def)
next
  case (Suc n)
  with funpow_dom[OF f] show ?case
    by (auto intro!: monotone_onI monotone_onD[OF mono] elim!:monotone_onE)
qed

no_notation bot (‹⊥›)

context
  fixes A and less_eq (infix ‹⊑› 50) and bot (‹⊥›) and f
  assumes bot: "⊥ ∈ A" "∀q ∈ A. ⊥ ⊑ q"
  assumes cont: "omega_chain-continuous A (⊑) A (⊑) f"
begin

interpretation less_eq_symmetrize.

private lemma f: "f ` A ⊆ A" using cont by auto

private abbreviation(input) "Fn ≡ {f^n ⊥ |. n :: nat}"

private lemma fn_ref: "f^n ⊥ ⊑ f^n ⊥" and fnA: "f^n ⊥ ∈ A"
proof (atomize(full), induct n)
  case 0
  from bot show ?case by simp
next
  case (Suc n)
  then have fn: "f^n ⊥ ∈ A" and fnfn: "f^n ⊥ ⊑ f^n ⊥" by auto
  from f fn omega_continuous_imp_mono_refl[OF cont fnfn fnfn fnfn]
  show ?case by auto
qed

private lemma FnA: "Fn ⊆ A" using fnA by auto

private lemma Fn_chain: "omega_chain Fn (⊑)"
proof (intro omega_chainI)
  show fn_monotone: "monotone (≤) (⊑) (λn. f^n ⊥)"
  proof
    fix n m :: nat
    assume "n ≤ m"
    from le_Suc_ex[OF this] obtain k where m: "m = n + k" by auto
    from bot fn_ref fnA omega_continuous_imp_mono_refl[OF cont]
    show "f^n ⊥ ⊑ f^m ⊥" by (unfold m, induct n, auto)
  qed
qed auto

private lemma Fn: "Fn = range (λn. f^n ⊥)" by auto

theorem kleene_qfp:
  assumes q: "extreme_bound A (⊑) Fn q"
  shows "f q ∼ q"
proof
  have fq: "extreme_bound A (⊑) (f ` Fn) (f q)"
    apply (rule continuousD[OF cont _ _ FnA q])
    using Fn_chain by auto
  with bot have nq: "f^n ⊥ ⊑ f q" for n by (induct n, auto simp: extreme_bound_iff)
  then show "q ⊑ f q" using f q by blast
  have "f (f^n ⊥) ∈ Fn" for n by (auto intro!: range_eqI[of _ _ "Suc n"])
  then have "f ` Fn ⊆ Fn" by auto
  from extreme_bound_subset[OF this fq q]
  show "f q ⊑ q".
qed

lemma ex_kleene_qfp:
  assumes comp: "omega_chain-complete A (⊑)"
  shows "∃p. extreme_bound A (⊑) Fn p"
  apply (intro comp[THEN completeD, OF FnA])
  using Fn_chain
  by auto

subsection ‹Iterative Fixed Points are Least.›
text ‹Kleene's theorem also states that the quasi-fixed point found this way is a least one.
Again, attractivity is needed to prove this statement.›

lemma kleene_qfp_is_least:
  assumes attract: "∀q ∈ A. ∀x ∈ A. f q ∼ q ⟶ x ⊑ f q ⟶ x ⊑ q"
  assumes q: "extreme_bound A (⊑) Fn q"
  shows "extreme {s ∈ A. f s ∼ s} (⊒) q"
proof(safe intro!: extremeI kleene_qfp[OF q])
  from q
  show "q ∈ A" by auto
  fix c assume c: "c ∈ A" and cqfp: "f c ∼ c"
  {
    fix n::nat
    have "f^n ⊥ ⊑ c"
    proof(induct n)
      case 0
      show ?case using bot c by auto
    next
      case IH: (Suc n)
      have "c ⊑ c" using attract cqfp c by auto
      with IH have "f^(Suc n) ⊥ ⊑ f c"
        using omega_continuous_imp_mono_refl[OF cont] fn_ref fnA c by auto
      then show ?case using attract cqfp c fnA by blast
    qed
  }
  then show "q ⊑ c" using q c by auto
qed

lemma kleene_qfp_iff_least:
  assumes comp: "omega_chain-complete A (⊑)"
  assumes attract: "∀q ∈ A. ∀x ∈ A. f q ∼ q ⟶ x ⊑ f q ⟶ x ⊑ q"
  assumes dual_attract: "∀p ∈ A. ∀q ∈ A. ∀x ∈ A. p ∼ q ⟶ q ⊑ x ⟶ p ⊑ x"
  shows "extreme_bound A (⊑) Fn = extreme {s ∈ A. f s ∼ s} (⊒)"
proof (intro ext iffI kleene_qfp_is_least[OF attract])
  fix q
  assume q: "extreme {s ∈ A. f s ∼ s} (⊒) q"
  from q have qA: "q ∈ A" by auto
  from q have qq: "q ⊑ q" by auto
  from q have fqq: "f q ∼ q" by auto
  from ex_kleene_qfp[OF comp]
  obtain k where k: "extreme_bound A (⊑) Fn k" by auto
  have qk: "q ∼ k"
  proof
    from kleene_qfp[OF k] q k
    show "q ⊑ k" by auto
    from kleene_qfp_is_least[OF _ k] q attract
    show "k ⊑ q" by blast
  qed
  show "extreme_bound A (⊑) Fn q"
  proof (intro extreme_boundI,safe)
    fix n
    show "f^n ⊥ ⊑ q"
    proof (induct n)
      case 0
      from bot q show ?case by auto 
    next
      case S:(Suc n)
      from fnA f have fsnbA: "f (f^n ⊥) ∈ A" by auto
      have fnfn: "f^n ⊥ ⊑ f^n ⊥" using fn_ref by auto
      have "f (f^n ⊥) ⊑ f q"
        using omega_continuous_imp_mono_refl[OF cont] fnA qA S fnfn qq by auto
      then show ?case using fsnbA qA attract fqq by auto
    qed
  next
    fix x
    assume "bound Fn (⊑) x" and x: "x ∈ A"
    with k have kx: "k ⊑ x" by auto
    with dual_attract[rule_format, OF _ _ x qk] q k
    show "q ⊑ x" by auto
  next
    from q show "q ∈ A" by auto
  qed
qed

end

context attractive begin

interpretation less_eq_dualize + less_eq_symmetrize.

theorem kleene_qfp_is_dual_extreme:
  assumes comp: "omega_chain-complete A (⊑)"
    and cont: "omega_chain-continuous A (⊑) A (⊑) f" and bA: "b ∈ A" and bot: "∀x ∈ A. b ⊑ x"
  shows "extreme_bound A (⊑) {f^n b |. n :: nat} = extreme {s ∈ A. f s ∼ s} (⊒)"
  apply (rule kleene_qfp_iff_least[OF bA bot cont comp])
  using continuous_carrierD[OF cont]
  by (auto dest: sym_order_trans order_sym_trans)

end

corollary(in antisymmetric) kleene_fp:
  assumes cont: "omega_chain-continuous A (⊑) A (⊑) f"
    and b: "b ∈ A" "∀x ∈ A. b ⊑ x"
    and p: "extreme_bound A (⊑) {f^n b |. n :: nat} p"
  shows "f p = p"
  using kleene_qfp[OF b cont] p cont[THEN continuous_carrierD]
  by (auto 2 3 intro!:antisym)

no_notation compower (‹_^_›[1000,1000]1000)

end