diff --git a/thys/Complete_Non_Orders/Kleene_Fixed_Point.thy b/thys/Complete_Non_Orders/Kleene_Fixed_Point.thy --- a/thys/Complete_Non_Orders/Kleene_Fixed_Point.thy +++ b/thys/Complete_Non_Orders/Kleene_Fixed_Point.thy @@ -1,291 +1,291 @@ theory Kleene_Fixed_Point imports Complete_Relations 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 \Scott Continuity, $\omega$-Completeness, $\omega$-Continuity\ text \In this Section, we formalize $\omega$-completeness, Scott continuity and $\omega$-continuity. We then prove that a Scott continuous map is $\omega$-continuous and that an $\omega$-continuous map is ``nearly'' monotone.\ context fixes A :: "'a set" and less_eq :: "'a \ 'a \ bool" (infix "\" 50) begin definition "omega_continuous f \ f ` A \ A \ (\c :: nat \ 'a. \ b \ A. range c \ A \ monotone (\) (\) c \ extreme_bound A (\) (range c) b \ extreme_bound A (\) (f ` range c) (f b))" lemmas omega_continuousI[intro?] = omega_continuous_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp, rule_format] lemmas omega_continuousDdom = omega_continuous_def[unfolded atomize_eq, THEN iffD1, unfolded conj_imp_eq_imp_imp, THEN conjunct1] lemmas omega_continuousD = omega_continuous_def[unfolded atomize_eq, THEN iffD1, unfolded conj_imp_eq_imp_imp, THEN conjunct2, rule_format] lemmas omega_continuousE[elim] = omega_continuous_def[unfolded atomize_eq, THEN iffD1, elim_format, unfolded conj_imp_eq_imp_imp, rule_format] lemma omega_continuous_imp_mono_refl: assumes cont: "omega_continuous f" and x: "x \ A" and y: "y \ A" and xy: "x \ y" and xx: "x \ x" and yy: "y \ y" shows "f x \ f y" proof- define c :: "nat \ 'a" where "c \ \i. if i = 0 then x else y" from x y xx xy yy have c: "range c \ A" "monotone (\) (\) c" by (auto simp: c_def intro!: monotoneI) have "extreme_bound A (\) (range c) y" using xy yy x y by (auto simp: c_def) then have fboy: "extreme_bound A (\) (f ` range c) (f y)" using c cont y by auto then show "f x \ f y" by (auto simp: c_def) qed definition "scott_continuous f \ f ` A \ A \ - (\X s. X \ A \ directed X (\) \ extreme_bound A (\) X s \ extreme_bound A (\) (f ` X) (f s))" + (\X s. X \ A \ directed X (\) \ X \ {} \ extreme_bound A (\) X s \ extreme_bound A (\) (f ` X) (f s))" lemmas scott_continuousI[intro?] = scott_continuous_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp, rule_format] -lemmas scott_continuousE[elim] = +lemmas scott_continuousE = scott_continuous_def[unfolded atomize_eq, THEN iffD1, elim_format, unfolded conj_imp_eq_imp_imp, rule_format] lemma scott_continuous_imp_mono_refl: assumes scott: "scott_continuous f" and x: "x \ A" and y: "y \ A" and xy: "x \ y" and yy: "y \ y" shows "f x \ f y" proof- define D where "D \ {x,y}" - from x y xy yy have dir_D: "D \ A" "directed D (\)" + from x y xy yy have dir_D: "D \ A" "directed D (\)" "D \ {}" by (auto simp: D_def intro!: bexI[of _ y] directedI) have "extreme_bound A (\) D y" using xy yy x y by (auto simp: D_def) - then have fboy: "extreme_bound A (\) (f ` D) (f y)" using dir_D scott by auto + then have fboy: "extreme_bound A (\) (f ` D) (f y)" using dir_D scott by (auto elim!: scott_continuousE) then show "f x \ f y" by (auto simp: D_def) qed lemma scott_continuous_imp_omega_continuous: assumes scott: "scott_continuous f" shows "omega_continuous f" proof - from scott show "f ` A \ A" by auto + from scott show "f ` A \ A" by (auto elim!: scott_continuousE) fix c :: "nat \ 'a" assume mono: "monotone (\) (\) c" and c: "range c \ A" from monotone_directed_image[OF mono[folded monotone_on_UNIV] order.directed] scott c show "extreme_bound A (\) (range c) b \ extreme_bound A (\) (f ` range c) (f b)" for b - by auto + by (auto elim!: scott_continuousE) qed end 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.\ (* no_notation power (infixr "^" 80) *) notation compower ("_^_"[1000,1000]1000) lemma mono_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_continuous A (\) f" begin interpretation less_eq_notations. 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 fn fn fnfn fnfn fnfn] show ?case by auto qed private lemma FnA: "Fn \ A" using fnA by auto private lemma 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 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 (unfold Fn) apply (rule omega_continuousD[OF cont]) using FnA fn_monotone q by (unfold Fn, 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!: exI[of _ "Suc n"]) then have "f ` Fn \ Fn" by auto from extreme_bound_mono[OF this fq q] show "f q \ q". qed lemma ex_kleene_qfp: assumes comp: "omega_complete A (\)" shows "\p. extreme_bound A (\) Fn p" using fn_monotone apply (intro comp[unfolded omega_complete_def, THEN completeD, OF FnA]) by fast 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_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_notations. theorem kleene_qfp_is_dual_extreme: assumes comp: "omega_complete A (\)" and cont: "omega_continuous 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 cont[THEN omega_continuousDdom] by (auto dest: sym_order_trans order_sym_trans) end corollary(in antisymmetric) kleene_fp: assumes cont: "omega_continuous 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 omega_continuousDdom] by (auto 2 3 intro!:antisym) no_notation compower ("_^_"[1000,1000]1000) end \ No newline at end of file