--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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:
--- 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)"
--- 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>
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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