--- 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.
--- 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)"
--- 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')) =
--- 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"
--- 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
--- 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