# HG changeset patch
# User wenzelm
# Date 1733910057 -3600
# Node ID a712bf5ccab09998fb603f55e2224de5778d6377
# Parent  0a01bec9bc1370196681f01cbfabebee6fee421d
tuned whitespace;

diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Algebraic.thy
--- a/src/HOL/HOLCF/Algebraic.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Algebraic.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -10,6 +10,7 @@
 
 default_sort bifinite
 
+
 subsection \<open>Type constructor for finite deflations\<close>
 
 typedef 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
@@ -72,6 +73,7 @@
 using finite_deflation_Rep_fin_defl
 by (rule finite_deflation_imp_compact)
 
+
 subsection \<open>Defining algebraic deflations by ideal completion\<close>
 
 typedef 'a defl = "{S::'a fin_defl set. below.ideal S}"
@@ -147,6 +149,7 @@
 lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
 by (rule defl_minimal [THEN bottomI, symmetric])
 
+
 subsection \<open>Applying algebraic deflations\<close>
 
 definition
@@ -215,6 +218,7 @@
 lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
 by (rule cast.below [THEN bottomI])
 
+
 subsection \<open>Deflation combinators\<close>
 
 definition
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Bifinite.thy
--- a/src/HOL/HOLCF/Bifinite.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -10,6 +10,7 @@
 
 default_sort cpo
 
+
 subsection \<open>Chains of finite deflations\<close>
 
 locale approx_chain =
@@ -43,6 +44,7 @@
 
 end
 
+
 subsection \<open>Omega-profinite and bifinite domains\<close>
 
 class bifinite = pcpo +
@@ -51,6 +53,7 @@
 class profinite = cpo +
   assumes profinite: "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
 
+
 subsection \<open>Building approx chains\<close>
 
 lemma approx_chain_iso:
@@ -155,6 +158,7 @@
 using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
 by (rule approx_chain.intro)
 
+
 subsection \<open>Class instance proofs\<close>
 
 instance bifinite \<subseteq> profinite
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Compact_Basis.thy
--- a/src/HOL/HOLCF/Compact_Basis.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -10,6 +10,7 @@
 
 default_sort bifinite
 
+
 subsection \<open>A compact basis for powerdomains\<close>
 
 definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
@@ -40,6 +41,7 @@
   (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
 qed
 
+
 subsection \<open>Unit and plus constructors\<close>
 
 definition
@@ -91,6 +93,7 @@
 apply (rule PDUnit, erule PDPlus [OF PDUnit])
 done
 
+
 subsection \<open>Fold operator\<close>
 
 definition
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Completion.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -128,6 +128,7 @@
 apply (erule (1) below_trans)
 done
 
+
 subsection \<open>Lemmas about least upper bounds\<close>
 
 lemma is_ub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
@@ -184,6 +185,7 @@
   "\<forall>i. Y i \<preceq> Y (Suc i) \<Longrightarrow> chain (\<lambda>i. principal (Y i))"
 by (simp add: chainI principal_mono)
 
+
 subsubsection \<open>Principal ideals approximate all elements\<close>
 
 lemma compact_principal [simp]: "compact (principal a)"
@@ -296,6 +298,7 @@
 apply (drule (2) admD2, fast, simp)
 done
 
+
 subsection \<open>Defining functions in terms of basis elements\<close>
 
 definition
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -466,6 +466,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
+
 subsection \<open>Convex powerdomain is bifinite\<close>
 
 lemma approx_chain_convex_map:
@@ -481,6 +482,7 @@
     by (fast intro!: approx_chain_convex_map)
 qed
 
+
 subsection \<open>Join\<close>
 
 definition
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Cpo.thy
--- a/src/HOL/HOLCF/Cpo.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Cpo.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -558,6 +558,7 @@
 
 end
 
+
 subsection \<open>Discrete cpos\<close>
 
 class discrete_cpo = below +
@@ -799,10 +800,12 @@
   apply simp
   done
 
+
 section \<open>Admissibility and compactness\<close>
 
 default_sort cpo
 
+
 subsection \<open>Definitions\<close>
 
 definition adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool"
@@ -969,6 +972,7 @@
   adm_below adm_eq adm_not_below
   adm_compact_not_below adm_compact_neq adm_neq_compact
 
+
 section \<open>Class instances for the full function space\<close>
 
 subsection \<open>Full function space is a partial order\<close>
@@ -1109,6 +1113,7 @@
   for S :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo"
   by (simp add: lub_fun ch2ch_lambda)
 
+
 section \<open>The cpo of cartesian products\<close>
 
 subsection \<open>Unit type is a pcpo\<close>
@@ -1401,6 +1406,7 @@
   apply (case_tac "\<Squnion>i. Y i", simp)
   done
 
+
 section \<open>Discrete cpo types\<close>
 
 datatype 'a discr = Discr "'a :: type"
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Deflation.thy
--- a/src/HOL/HOLCF/Deflation.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Deflation.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -313,6 +313,7 @@
 
 end
 
+
 subsection \<open>Uniqueness of ep-pairs\<close>
 
 lemma ep_pair_unique_e_lemma:
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Domain.thy
--- 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)"
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -285,6 +285,7 @@
   "succeed\<cdot>x \<noteq> fail" "fail \<noteq> succeed\<cdot>x"
 by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject)
 
+
 subsubsection \<open>Run operator\<close>
 
 definition
@@ -305,6 +306,7 @@
 unfolding run_def succeed_def
 by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)
 
+
 subsubsection \<open>Monad plus operator\<close>
 
 definition
@@ -335,6 +337,7 @@
 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
 by (cases x, simp_all)
 
+
 subsection \<open>Match functions for built-in types\<close>
 
 default_sort pcpo
@@ -431,6 +434,7 @@
   "match_FF\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_FF_def)
 
+
 subsection \<open>Mutual recursion\<close>
 
 text \<open>
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Lift.thy
--- a/src/HOL/HOLCF/Lift.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Lift.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -19,6 +19,7 @@
   Def :: "'a \<Rightarrow> 'a lift" where
   "Def x = Abs_lift (up\<cdot>(Discr x))"
 
+
 subsection \<open>Lift as a datatype\<close>
 
 lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
@@ -70,6 +71,7 @@
     by (induct x) auto
 qed
 
+
 subsection \<open>Continuity of \<^const>\<open>case_lift\<close>\<close>
 
 lemma case_lift_eq: "case_lift \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
@@ -82,6 +84,7 @@
   "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. case_lift \<bottom> (f x) (g x))"
 unfolding case_lift_eq by (simp add: cont_Rep_lift)
 
+
 subsection \<open>Further operations\<close>
 
 definition
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -459,6 +459,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
+
 subsection \<open>Lower powerdomain is bifinite\<close>
 
 lemma approx_chain_lower_map:
@@ -474,6 +475,7 @@
     by (fast intro!: approx_chain_lower_map)
 qed
 
+
 subsection \<open>Join\<close>
 
 definition
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Powerdomains.thy
--- a/src/HOL/HOLCF/Powerdomains.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Powerdomains.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -31,6 +31,7 @@
   unfolding convex_emb_def convex_prj_def
   by (simp add: ep_pair_udom approx_chain_convex_map)
 
+
 subsection \<open>Deflation combinators\<close>
 
 definition upper_defl :: "udom defl \<rightarrow> udom defl"
@@ -57,6 +58,7 @@
 using ep_pair_convex finite_deflation_convex_map
 unfolding convex_defl_def by (rule cast_defl_fun1)
 
+
 subsection \<open>Domain class instances\<close>
 
 instantiation upper_pd :: ("domain") "domain"
@@ -167,6 +169,7 @@
 lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
 by (rule defl_convex_pd_def)
 
+
 subsection \<open>Isomorphic deflations\<close>
 
 lemma isodefl_upper:
@@ -193,6 +196,7 @@
 apply (simp add: convex_map_map)
 done
 
+
 subsection \<open>Domain package setup for powerdomains\<close>
 
 lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Representable.thy
--- a/src/HOL/HOLCF/Representable.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Representable.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -10,6 +10,7 @@
 
 default_sort cpo
 
+
 subsection \<open>Class of representable domains\<close>
 
 text \<open>
@@ -88,6 +89,7 @@
 lemmas emb_strict = domain.e_strict
 lemmas prj_strict = domain.p_strict
 
+
 subsection \<open>Domains are bifinite\<close>
 
 lemma approx_chain_ep_cast:
@@ -126,6 +128,7 @@
 instance predomain \<subseteq> profinite
 by standard (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
 
+
 subsection \<open>Universal domain ep-pairs\<close>
 
 definition "u_emb = udom_emb (\<lambda>i. u_map\<cdot>(udom_approx i))"
@@ -163,6 +166,7 @@
   unfolding sfun_emb_def sfun_prj_def
   by (simp add: ep_pair_udom approx_chain_sfun_map)
 
+
 subsection \<open>Type combinators\<close>
 
 definition u_defl :: "udom defl \<rightarrow> udom defl"
@@ -223,6 +227,7 @@
 by (rule cast_eq_imp_eq)
    (simp add: cast_u_liftdefl cast_liftdefl_of cast_u_defl)
 
+
 subsection \<open>Class instance proofs\<close>
 
 subsubsection \<open>Universal domain\<close>
@@ -267,6 +272,7 @@
 
 end
 
+
 subsubsection \<open>Lifted cpo\<close>
 
 instantiation u :: (predomain) "domain"
@@ -304,6 +310,7 @@
 lemma DEFL_u: "DEFL('a::predomain u) = u_liftdefl\<cdot>LIFTDEFL('a)"
 by (rule defl_u_def)
 
+
 subsubsection \<open>Strict function space\<close>
 
 instantiation sfun :: ("domain", "domain") "domain"
@@ -342,6 +349,7 @@
   "DEFL('a::domain \<rightarrow>! 'b::domain) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 by (rule defl_sfun_def)
 
+
 subsubsection \<open>Continuous function space\<close>
 
 instantiation cfun :: (predomain, "domain") "domain"
@@ -382,6 +390,7 @@
   "DEFL('a::predomain \<rightarrow> 'b::domain) = DEFL('a u \<rightarrow>! 'b)"
 by (rule defl_cfun_def)
 
+
 subsubsection \<open>Strict product\<close>
 
 instantiation sprod :: ("domain", "domain") "domain"
@@ -420,6 +429,7 @@
   "DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 by (rule defl_sprod_def)
 
+
 subsubsection \<open>Cartesian product\<close>
 
 definition prod_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
@@ -508,6 +518,7 @@
     prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
 by (rule liftdefl_prod_def)
 
+
 subsubsection \<open>Unit type\<close>
 
 instantiation unit :: "domain"
@@ -541,6 +552,7 @@
 
 end
 
+
 subsubsection \<open>Discrete cpo\<close>
 
 instantiation discr :: (countable) predomain
@@ -586,6 +598,7 @@
 
 end
 
+
 subsubsection \<open>Strict sum\<close>
 
 instantiation ssum :: ("domain", "domain") "domain"
@@ -624,6 +637,7 @@
   "DEFL('a::domain \<oplus> 'b::domain) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 by (rule defl_ssum_def)
 
+
 subsubsection \<open>Lifted HOL type\<close>
 
 instantiation lift :: (countable) "domain"
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -10,6 +10,7 @@
 
 no_notation binomial  (infix \<open>choose\<close> 64)
 
+
 subsection \<open>Basis for universal domain\<close>
 
 subsubsection \<open>Basis datatype\<close>
@@ -79,6 +80,7 @@
  apply (simp add: 2 node_gt1 node_gt2)
 done
 
+
 subsubsection \<open>Basis ordering\<close>
 
 inductive
@@ -105,6 +107,7 @@
 apply (erule (1) ubasis_le_trans)
 done
 
+
 subsubsection \<open>Generic take function\<close>
 
 function
@@ -275,6 +278,7 @@
   approx_chain approx for approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
 begin
 
+
 subsubsection \<open>Choosing a maximal element from a finite set\<close>
 
 lemma finite_has_maximal:
@@ -389,6 +393,7 @@
  apply (simp add: choose_pos.simps)
 done
 
+
 subsubsection \<open>Compact basis take function\<close>
 
 primrec
@@ -443,6 +448,7 @@
 apply (rule inj_onI, simp add: Rep_compact_basis_inject)
 done
 
+
 subsubsection \<open>Rank of basis elements\<close>
 
 definition
@@ -522,6 +528,7 @@
 lemma rank_lt_Un_rank_eq: "rank_lt x \<union> rank_eq x = rank_le x"
 unfolding rank_lt_def rank_eq_def rank_le_def by auto
 
+
 subsubsection \<open>Sequencing basis elements\<close>
 
 definition
@@ -571,6 +578,7 @@
 lemma inj_place: "inj place"
 by (rule inj_onI, erule place_eqD)
 
+
 subsubsection \<open>Embedding and projection on basis elements\<close>
 
 definition
@@ -831,6 +839,7 @@
     by (rule bifinite_approx_chain.ideal_completion)
 qed
 
+
 subsubsection \<open>EP-pair from any bifinite domain into \emph{udom}\<close>
 
 context bifinite_approx_chain begin
@@ -879,6 +888,7 @@
 lemmas ep_pair_udom =
   bifinite_approx_chain.ep_pair_udom [unfolded bifinite_approx_chain_def]
 
+
 subsection \<open>Chain of approx functions for type \emph{udom}\<close>
 
 definition
diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -452,6 +452,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
+
 subsection \<open>Upper powerdomain is bifinite\<close>
 
 lemma approx_chain_upper_map:
@@ -467,6 +468,7 @@
     by (fast intro!: approx_chain_upper_map)
 qed
 
+
 subsection \<open>Join\<close>
 
 definition