--- a/src/HOL/HOLCF/Domain.thy Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Domain.thy Wed Dec 11 10:40:57 2024 +0100
@@ -112,6 +112,7 @@
end
+
subsection \<open>Proofs about take functions\<close>
text \<open>
@@ -173,6 +174,7 @@
with \<open>chain t\<close> \<open>(\<Squnion>n. t n) = ID\<close> show "P x" by (simp add: lub_distribs)
qed
+
subsection \<open>Finiteness\<close>
text \<open>
@@ -264,6 +266,7 @@
shows "(\<And>n. P (d n\<cdot>x)) \<Longrightarrow> P x"
using lub_ID_finite [OF assms] by metis
+
subsection \<open>Proofs about constructor functions\<close>
text \<open>Lemmas for proving nchotomy rule:\<close>
@@ -354,6 +357,7 @@
ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
deflation_strict deflation_ID ID1 cfcomp2
+
subsection \<open>ML setup\<close>
named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
@@ -416,6 +420,7 @@
unfolding abs_def rep_def
by (simp add: emb_prj_emb DEFL)
+
subsection \<open>Deflations as sets\<close>
definition defl_set :: "'a::bifinite defl \<Rightarrow> 'a set"
@@ -435,6 +440,7 @@
apply (auto simp add: cast.belowI cast.belowD)
done
+
subsection \<open>Proving a subtype is representable\<close>
text \<open>Temporarily relax type constraints.\<close>
@@ -509,6 +515,7 @@
ML_file \<open>Tools/domaindef.ML\<close>
+
subsection \<open>Isomorphic deflations\<close>
definition isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> udom defl \<Rightarrow> bool"
@@ -671,6 +678,7 @@
using isodefl_sfun [OF assms] unfolding isodefl_def
by (simp add: emb_cfun_def prj_cfun_def cfcomp1 encode_cfun_map)
+
subsection \<open>Setting up the domain package\<close>
named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"