# HG changeset patch
# User wenzelm
# Date 1746648472 -7200
# Node ID b7148ee355f602ca94cf8d6b646027e9698ea850
# Parent  76262e8b53f7063ae9ff58e83ccf8818f42504c4# Parent  c1871d01355610071485c8e11f001a7470cf0035
merged

diff -r c1871d013556 -r b7148ee355f6 NEWS
--- a/NEWS	Wed May 07 22:06:49 2025 +0200
+++ b/NEWS	Wed May 07 22:07:52 2025 +0200
@@ -71,6 +71,8 @@
 yield false positives due to incomplete handling of polymorphism in certain
 situations; this is now corrected.
 
+* Theory "HOL.Nat": Added Kleene's Fixed Point Theorem for lfp.
+
 * Theory "HOL-Library.Code_Target_Bit_Shifts" incorporated into HOL-Main.
 Minor INCOMPATIBILITY.
 
diff -r c1871d013556 -r b7148ee355f6 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Wed May 07 22:06:49 2025 +0200
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Wed May 07 22:07:52 2025 +0200
@@ -1303,6 +1303,41 @@
   qed
 qed
 
+lemma Lim_left_bound:
+  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_bot} \<Rightarrow>
+    'b :: {linorder_topology, conditionally_complete_linorder}"
+  assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> b < x \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
+    and bnd: "\<And>b. b \<in> I \<Longrightarrow> b < x \<Longrightarrow> f b \<le> K"
+  shows "(f \<longlongrightarrow> Sup (f ` ({..<x} \<inter> I))) (at x within ({..<x} \<inter> I))"
+proof (cases "{..<x} \<inter> I = {}")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  show ?thesis
+  proof (rule order_tendstoI)
+    fix b
+    assume b: "Sup (f ` ({..<x} \<inter> I)) < b"
+    {
+      fix y
+      assume "y \<in> {..<x} \<inter> I"
+      with False bnd have "f y \<le> Sup (f ` ({..<x} \<inter> I))" by (auto intro!: cSup_upper bdd_aboveI2)
+      with b have "f y < b" by order
+    }
+    then show "eventually (\<lambda>x. f x < b) (at x within ({..<x} \<inter> I))"
+      by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
+  next
+    fix b
+    assume "b < Sup (f ` ({..<x} \<inter> I))"
+    from less_cSupD[OF _ this] False obtain y where y: "y < x" "y \<in> I" "b < f y" by auto
+    then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> b < f x) (at_left x)"
+      unfolding eventually_at_left[OF \<open>y < x\<close>] by (metis mono order_less_le order_less_le_trans)
+    then show "eventually (\<lambda>x. b < f x) (at x within ({..<x} \<inter> I))"
+      unfolding eventually_at_filter by eventually_elim simp
+  qed
+qed
+
+
 text\<open>These are special for limits out of the same topological space.\<close>
 
 lemma Lim_within_id: "(id \<longlongrightarrow> a) (at a within s)"
diff -r c1871d013556 -r b7148ee355f6 src/HOL/Library/datatype_records.ML
--- a/src/HOL/Library/datatype_records.ML	Wed May 07 22:06:49 2025 +0200
+++ b/src/HOL/Library/datatype_records.ML	Wed May 07 22:07:52 2025 +0200
@@ -173,7 +173,7 @@
       end
 
     fun define name t =
-      Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code]}),t))
+      Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code equation]}),t))
       #> apfst (apsnd snd)
 
     val (updates, (lthy'', lthy')) =
diff -r c1871d013556 -r b7148ee355f6 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed May 07 22:06:49 2025 +0200
+++ b/src/HOL/Nat.thy	Wed May 07 22:07:52 2025 +0200
@@ -2427,6 +2427,83 @@
   by (auto intro!: funpow_increasing simp: antimono_def)
 
 
+subsection \<open>Kleene's fixed point theorem for continuous functions\<close>
+
+text \<open>Kleene's fixed point theorem shows that the \<open>lfp\<close> of a omega-continuous function
+can be obtained as the supremum of an omega chain. It only requires an omega-complete partial order.
+We prove it here for complete lattices because the latter structures are not defined in Main
+but the theorem is also useful for complete lattices.\<close>
+
+definition omega_chain :: "(nat \<Rightarrow> ('a::complete_lattice)) \<Rightarrow> bool" where
+"omega_chain C = (\<forall>i. C i \<le> C(Suc i))"
+
+definition omega_cont :: "(('a::complete_lattice) \<Rightarrow> ('b::complete_lattice)) \<Rightarrow> bool" where
+"omega_cont f = (\<forall>C. omega_chain C \<longrightarrow> f(SUP n. C n) = (SUP n. f(C n)))"
+
+lemma omega_chain_mono: "omega_chain C \<Longrightarrow> i \<le> j \<Longrightarrow> C i \<le> C j"
+unfolding omega_chain_def using lift_Suc_mono_le[of C]  
+by(induction "j-i" arbitrary: i j)auto
+
+lemma mono_if_omega_cont: fixes f :: "('a::complete_lattice) \<Rightarrow> ('b::complete_lattice)"
+  assumes "omega_cont f" shows "mono f"
+proof
+  fix a b :: "'a" assume "a \<le> b"
+  let ?C = "\<lambda>n::nat. if n=0 then a else b"
+  have *: "omega_chain ?C" using \<open>a \<le> b\<close> by(auto simp: omega_chain_def)
+  have "f a \<le> sup (f a) (SUP n. f(?C n))" by(rule sup.cobounded1)
+  also have "\<dots> = sup (f(?C 0)) (SUP n. f(?C n))" by (simp)
+  also have "\<dots> = (SUP n. f (?C n))" using SUP_absorb[OF UNIV_I] .
+  also have "\<dots> = f (SUP n. ?C n)"
+    using assms * by (simp add: omega_cont_def del: if_image_distrib)
+  also have "f (SUP n. ?C n) = f b"
+    using \<open>a \<le> b\<close> by (auto simp add: gt_ex sup.absorb2 split: if_splits)
+  finally show "f a \<le> f b" .
+qed
+
+lemma omega_chain_iterates: fixes f :: "('a::complete_lattice) \<Rightarrow> 'a"
+  assumes "mono f" shows "omega_chain(\<lambda>n. (f^^n) bot)"
+proof-
+  have "(f ^^ n) bot \<le> (f ^^ Suc n) bot" for n
+  proof (induction n)
+    case 0 show ?case by simp
+  next
+    case (Suc n) thus ?case using assms by (auto simp: mono_def)
+  qed
+  thus ?thesis by(auto simp: omega_chain_def assms)
+qed
+
+theorem Kleene_lfp:
+  assumes "omega_cont f" shows "lfp f = (SUP n. (f^^n) bot)" (is "_ = ?U")
+proof(rule Orderings.antisym)
+  from assms mono_if_omega_cont
+  have mono: "(f ^^ n) bot \<le> (f ^^ Suc n) bot" for n
+    using funpow_decreasing [of n "Suc n"] by auto
+  show "lfp f \<le> ?U"
+  proof (rule lfp_lowerbound)
+    have "f ?U = (SUP n. (f^^Suc n) bot)"
+      using omega_chain_iterates[OF mono_if_omega_cont[OF assms]] assms
+      by(simp add: omega_cont_def)
+    also have "\<dots> = ?U" using mono by(blast intro: SUP_eq)
+    finally show "f ?U \<le> ?U" by simp
+  qed
+next
+  have "(f^^n) bot \<le> p" if "f p \<le> p" for n p
+  proof -
+    show ?thesis
+    proof(induction n)
+      case 0 show ?case by simp
+    next
+      case Suc
+      from monoD[OF mono_if_omega_cont[OF assms] Suc] \<open>f p \<le> p\<close>
+      show ?case by simp
+    qed
+  qed
+  thus "?U \<le> lfp f"
+    using lfp_unfold[OF mono_if_omega_cont[OF assms]]
+    by (simp add: SUP_le_iff)
+qed
+
+
 subsection \<open>The divides relation on \<^typ>\<open>nat\<close>\<close>
 
 lemma dvd_1_left [iff]: "Suc 0 dvd k"
diff -r c1871d013556 -r b7148ee355f6 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed May 07 22:06:49 2025 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed May 07 22:07:52 2025 +0200
@@ -308,7 +308,7 @@
               |> Thm.close_derivation \<^here>
               |> singleton (Variable.export transfer_ctxt lthy4)
             val lthy5 = lthy4
-              |> Local_Theory.note ((Binding.empty, @{attributes [code]}), [f_alt_def])
+              |> Local_Theory.note ((Binding.empty, @{attributes [code equation]}), [f_alt_def])
               |> snd
               (* if processing a mutual datatype (there is a cycle!) the corresponding quotient 
                  will be needed later and will be forgotten later *)
@@ -538,7 +538,7 @@
       |> singleton(Variable.export x_ctxt lthy6)
   in
     lthy6
-    |> snd o Local_Theory.note ((Binding.empty, @{attributes [code]}), [rep_isom_code])
+    |> snd o Local_Theory.note ((Binding.empty, @{attributes [code equation]}), [rep_isom_code])
     |> Lifting_Setup.lifting_forget pointer
     |> pair (selss, diss, rep_isom_code)
   end
diff -r c1871d013556 -r b7148ee355f6 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed May 07 22:06:49 2025 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed May 07 22:07:52 2025 +0200
@@ -230,7 +230,7 @@
   by (metis (no_types) open_UNIV not_open_singleton)
 
 
-subsection \<open>Generators for toplogies\<close>
+subsection \<open>Generators for topologies\<close>
 
 inductive generate_topology :: "'a set set \<Rightarrow> 'a set \<Rightarrow> bool" for S :: "'a set set"
   where