--- a/NEWS Thu Jun 10 11:21:57 2021 +0200
+++ b/NEWS Thu Jun 10 11:54:14 2021 +0200
@@ -34,6 +34,12 @@
*** Document preparation ***
+* More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (LaTeX package
+"pifont").
+
+* High-quality blackboard-bold symbols from font "txmia" (LaTeX package
+"pxfonts"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>.
+
* Document antiquotations for ML text have been refined: "def" and "ref"
variants support index entries, e.g. @{ML} (no entry) vs. @{ML_def}
(bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit
@@ -97,16 +103,23 @@
no longer required.
+*** Pure ***
+
+* "global_interpretation" is applicable in instantiation and overloading
+targets and in any nested target built on top of a target supporting
+"global_interpretation".
+
+
*** HOL ***
-* Theory Multiset: dedicated predicate "multiset" is gone, use
-explict expression instead. Minor INCOMPATIBILITY.
-
-* Theory Multiset: consolidated abbreviations Mempty, Melem, not_Melem
-to empty_mset, member_mset, not_member_mset respectively. Minor
-INCOMPATIBILITY.
-
-* Theory Multiset: consolidated operation and fact names:
+* Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,
+use explict expression instead. Minor INCOMPATIBILITY.
+
+* Theory "HOL-Library.Multiset": consolidated abbreviations Mempty,
+Melem, not_Melem to empty_mset, member_mset, not_member_mset
+respectively. Minor INCOMPATIBILITY.
+
+* Theory "HOL-Library.Multiset": consolidated operation and fact names:
inf_subset_mset ~> inter_mset
sup_subset_mset ~> union_mset
multiset_inter_def ~> inter_mset_def
@@ -114,52 +127,52 @@
multiset_inter_count ~> count_inter_mset
sup_subset_mset_count ~> count_union_mset
-* Theory Multiset: syntax precendence for membership operations has been
-adjusted to match the corresponding precendences on sets. Rare
-INCOMPATIBILITY.
-
-* HOL-Analysis/HOL-Probability: indexed products of discrete
-distributions, negative binomial distribution, Hoeffding's inequality,
-Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some
-more small lemmas. Some theorems that were stated awkwardly before were
-corrected. Minor INCOMPATIBILITY.
+* Theory "HOL-Library.Multiset": syntax precendence for membership
+operations has been adjusted to match the corresponding precendences on
+sets. Rare INCOMPATIBILITY.
+
+* Session "HOL-Analysis" and "HOL-Probability": indexed products of
+discrete distributions, negative binomial distribution, Hoeffding's
+inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral,
+and some more small lemmas. Some theorems that were stated awkwardly
+before were corrected. Minor INCOMPATIBILITY.
* Theorems "antisym" and "eq_iff" in class "order" have been renamed to
"order.antisym" and "order.eq_iff", to coexist locally with "antisym"
-and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant
+and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant
potential for change can be avoided if interpretations of type class
"order" are replaced or augmented by interpretations of locale
"ordering".
-* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor
+* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor
INCOMPATIBILITY; note that for most applications less elementary lemmas
exists.
-* Dedicated session HOL-Combinatorics. INCOMPATIBILITY: theories
+* Theory "HOL-Library.Permutation" has been renamed to the more specific
+"HOL-Library.List_Permutation". Note that most notions from that theory
+are already present in theory "HOL-Combinatorics.Permutations".
+INCOMPATIBILITY.
+
+* Dedicated session "HOL-Combinatorics". INCOMPATIBILITY: theories
"Permutations", "List_Permutation" (formerly "Permutation"), "Stirling",
"Multiset_Permutations", "Perm" have been moved there from session
HOL-Library.
-* Theory "Permutation" in HOL-Library has been renamed to the more
-specific "List_Permutation". Note that most notions from that
-theory are already present in theory "Permutations". INCOMPATIBILITY.
-
-* Lemma "permutes_induct" has been given stronger
-hypotheses and named premises. INCOMPATIBILITY.
-
-* Theory "Transposition" in HOL-Combinatorics provides elementary
-swap operation "transpose".
-
-* Combinator "Fun.swap" resolved into a mere input abbreviation
-in separate theory "Transposition" in HOL-Combinatorics.
-INCOMPATIBILITY.
+* Theory "HOL-Combinatorics.Transposition" provides elementary swap
+operation "transpose".
+
+* Lemma "permutes_induct" has been given stronger hypotheses and named
+premises. INCOMPATIBILITY.
+
+* Combinator "Fun.swap" resolved into a mere input abbreviation in
+separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY.
* Bit operations set_bit, unset_bit and flip_bit are now class
-operations. INCOMPATIBILITY.
+operations. INCOMPATIBILITY.
* Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
-"setBit", "clearBit". See there further the changelog in theory Guide.
+"setBit", "clearBit". See there further the changelog in theory Guide.
INCOMPATIBILITY.
@@ -231,10 +244,27 @@
*** System ***
+* ML profiling has been updated and reactivated, after some degration in
+Isabelle2021:
+
+ - "isabelle build -o threads=1 -o profiling=..." works properly
+ within the PIDE session context;
+
+ - "isabelle profiling_report" now uses the session build database
+ (like "isabelle log");
+
+ - output uses non-intrusive tracing messages, instead of warnings.
+
* System option "system_log" specifies an optional log file for internal
-messages produced by Output.system_message in Isabelle/ML; "-" refers to
-console progress of the build job. This works for "isabelle build" or
-any derivative of it.
+messages produced by Output.system_message in Isabelle/ML; the value
+"true" refers to console progress of the build job. This works for
+"isabelle build" or any derivative of it.
+
+* System options of type string may be set to "true" using the short
+notation of type bool. E.g. "isabelle build -o system_log".
+
+* System option "document=true" is an alias for "document=pdf" and thus
+can be used in the short form. E.g. "isabelle build -o document".
* Command-line tool "isabelle version" supports repository archives
(without full .hg directory). More options.
@@ -991,12 +1021,6 @@
*** Document preparation ***
-* More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (package
-"pifont").
-
-* High-quality blackboard-bold symbols from font "txmia" (package
-"pxfonts"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>.
-
* Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that
are stripped from document output: the effect is to modify the semantic
presentation context or to emit markup to the PIDE document. Some
--- a/etc/options Thu Jun 10 11:21:57 2021 +0200
+++ b/etc/options Thu Jun 10 11:54:14 2021 +0200
@@ -6,7 +6,7 @@
-- "generate theory browser information"
option document : string = ""
- -- "build document in given format: pdf, dvi, false"
+ -- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")"
option document_output : string = ""
-- "document output directory"
option document_variants : string = "document"
@@ -132,7 +132,7 @@
-- "ML profiling (possible values: time, allocations)"
option system_log : string = ""
- -- "output for system messages (log file or \"-\" for console progress)"
+ -- "output for system messages (log file or \"true\" for console progress)"
option system_heaps : bool = false
-- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS"
@@ -305,10 +305,10 @@
section "Phabricator"
-option phabricator_version_arcanist : string = "7af9846f994a8d0a1fc89af996e3ddd81f01765e"
+option phabricator_version_arcanist : string = "cdae0ac68f1fed138323fa3dbb299ef3b287723c"
-- "repository version for arcanist"
-option phabricator_version_phabricator : string = "2afedad61c5181bb4f832cea27b9b59df19f3fd5"
+option phabricator_version_phabricator : string = "4f70fcffa8a5393e210d64f237ffdaa256256d6a"
-- "repository version for phabricator"
--- a/src/Doc/Isar_Ref/Spec.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Thu Jun 10 11:54:14 2021 +0200
@@ -738,6 +738,9 @@
free variable whose name is already bound in the context --- for example,
because a constant of that name exists --- add it to the \<^theory_text>\<open>for\<close> clause.
+ When used in a nested target, resulting declarations are propagated
+ through the whole target stack.
+
\<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs\<close> interprets \<open>expr\<close>
into the locale \<open>name\<close>. A proof that the specification of \<open>name\<close> implies the
specification of \<open>expr\<close> is required. As in the localized version of the
--- a/src/Doc/System/Presentation.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Doc/System/Presentation.thy Thu Jun 10 11:54:14 2021 +0200
@@ -47,9 +47,9 @@
reported by the above verbose invocation of the build process.
Many Isabelle sessions (such as \<^session>\<open>HOL-Library\<close> in
- \<^dir>\<open>~~/src/HOL/Library\<close>) also provide printable documents in PDF. These are
+ \<^dir>\<open>~~/src/HOL/Library\<close>) also provide theory documents in PDF. These are
prepared automatically as well if enabled like this:
- @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
+ @{verbatim [display] \<open>isabelle build -o browser_info -o document -v -c HOL-Library\<close>}
Enabling both browser info and document preparation simultaneously causes an
appropriate ``document'' link to be included in the HTML index. Documents
--- a/src/Doc/System/Sessions.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Doc/System/Sessions.thy Thu Jun 10 11:54:14 2021 +0200
@@ -201,8 +201,9 @@
info, see also \secref{sec:info}.
\<^item> @{system_option_def "document"} controls document output for a
- particular session or theory; \<^verbatim>\<open>document=pdf\<close> means enabled,
- \<^verbatim>\<open>document=false\<close> means disabled (especially for particular theories).
+ particular session or theory; \<^verbatim>\<open>document=pdf\<close> or \<^verbatim>\<open>document=true\<close> means
+ enabled, \<^verbatim>\<open>document=""\<close> or \<^verbatim>\<open>document=false\<close> means disabled (especially
+ for particular theories).
\<^item> @{system_option_def "document_output"} specifies an alternative
directory for generated output of the document preparation system; the
@@ -278,7 +279,8 @@
\<^item> @{system_option_def system_log} specifies an optional log file for
low-level messages produced by \<^ML>\<open>Output.system_message\<close> in
- Isabelle/ML; ``\<^verbatim>\<open>-\<close>'' refers to console progress of the build job.
+ Isabelle/ML; the value ``\<^verbatim>\<open>true\<close>'' refers to console progress of the build
+ job.
\<^item> @{system_option_def "system_heaps"} determines the directories for
session heap images: \<^path>\<open>$ISABELLE_HEAPS\<close> is the user directory and
@@ -410,11 +412,12 @@
The build process depends on additional options
(\secref{sec:system-options}) that are passed to the prover eventually. The
settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
- additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>.
- Moreover, the environment of system build options may be augmented on the
- command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>, which abbreviates
- \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on
- the command-line are applied in the given order.
+ additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf
+ threads=4"\<close>. Moreover, the environment of system build options may be
+ augmented on the command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>,
+ which abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean or string options.
+ Multiple occurrences of \<^verbatim>\<open>-o\<close> on the command-line are applied in the given
+ order.
\<^medskip>
Option \<^verbatim>\<open>-P\<close> enables PDF/HTML presentation in the given directory, where
@@ -496,7 +499,7 @@
\<^smallskip>
Build all sessions with HTML browser info and PDF document preparation:
- @{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>}
+ @{verbatim [display] \<open>isabelle build -a -o browser_info -o document\<close>}
\<^smallskip>
Build all sessions with a maximum of 8 parallel prover processes and 4
@@ -539,6 +542,7 @@
-U output Unicode symbols
-m MARGIN margin for pretty printing (default: 76.0)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -v print all messages, including information etc.
Print messages from the build database of the given session, without any
checks against current sources: results from a failed build can be
@@ -563,8 +567,8 @@
symbols. The default is for an old-fashioned ASCII terminal at 80 characters
per line (76 + 4 characters to prefix warnings or errors).
- \<^medskip> Option \<^verbatim>\<open>-v\<close> prints all messages from the session database, including
- extra information and tracing messages etc.
+ \<^medskip> Option \<^verbatim>\<open>-v\<close> prints all messages from the session database that are
+ normally inlined into the source text, including information messages etc.
\<close>
subsubsection \<open>Examples\<close>
--- a/src/HOL/Finite_Set.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Finite_Set.thy Thu Jun 10 11:54:14 2021 +0200
@@ -710,21 +710,23 @@
subsection \<open>A basic fold functional for finite sets\<close>
-text \<open>The intended behaviour is
- \<open>fold f z {x\<^sub>1, \<dots>, x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)\<close>
- if \<open>f\<close> is ``left-commutative'':
+text \<open>
+ The intended behaviour is \<open>fold f z {x\<^sub>1, \<dots>, x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)\<close>
+ if \<open>f\<close> is ``left-commutative''.
+ The commutativity requirement is relativised to the carrier set \<open>S\<close>:
\<close>
-locale comp_fun_commute =
+locale comp_fun_commute_on =
+ fixes S :: "'a set"
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
- assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
+ assumes comp_fun_commute_on: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
begin
-lemma fun_left_comm: "f y (f x z) = f x (f y z)"
- using comp_fun_commute by (simp add: fun_eq_iff)
+lemma fun_left_comm: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f y (f x z) = f x (f y z)"
+ using comp_fun_commute_on by (simp add: fun_eq_iff)
-lemma commute_left_comp: "f y \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> g)"
- by (simp add: o_assoc comp_fun_commute)
+lemma commute_left_comp: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f y \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> g)"
+ by (simp add: o_assoc comp_fun_commute_on)
end
@@ -776,7 +778,7 @@
by (subst fold_graph_closed_eq[where B=B and g=g]) (auto simp: that)
text \<open>
- A tempting alternative for the definiens is
+ A tempting alternative for the definition is
\<^term>\<open>if finite A then THE y. fold_graph f z A y else e\<close>.
It allows the removal of finiteness assumptions from the theorems
\<open>fold_comm\<close>, \<open>fold_reindex\<close> and \<open>fold_distrib\<close>.
@@ -789,7 +791,7 @@
subsubsection \<open>From \<^const>\<open>fold_graph\<close> to \<^term>\<open>fold\<close>\<close>
-context comp_fun_commute
+context comp_fun_commute_on
begin
lemma fold_graph_finite:
@@ -798,7 +800,10 @@
using assms by induct simp_all
lemma fold_graph_insertE_aux:
- "fold_graph f z A y \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_graph f z (A - {a}) y'"
+ assumes "A \<subseteq> S"
+ assumes "fold_graph f z A y" "a \<in> A"
+ shows "\<exists>y'. y = f a y' \<and> fold_graph f z (A - {a}) y'"
+ using assms(2-,1)
proof (induct set: fold_graph)
case emptyI
then show ?case by simp
@@ -812,8 +817,9 @@
case False
then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'"
using insertI by auto
- have "f x y = f a (f x y')"
- unfolding y by (rule fun_left_comm)
+ from insertI have "x \<in> S" "a \<in> S" by auto
+ then have "f x y = f a (f x y')"
+ unfolding y by (intro fun_left_comm; simp)
moreover have "fold_graph f z (insert x A - {a}) (f x y')"
using y' and \<open>x \<noteq> a\<close> and \<open>x \<notin> A\<close>
by (simp add: insert_Diff_if fold_graph.insertI)
@@ -823,35 +829,41 @@
qed
lemma fold_graph_insertE:
+ assumes "insert x A \<subseteq> S"
assumes "fold_graph f z (insert x A) v" and "x \<notin> A"
obtains y where "v = f x y" and "fold_graph f z A y"
- using assms by (auto dest: fold_graph_insertE_aux [OF _ insertI1])
+ using assms by (auto dest: fold_graph_insertE_aux[OF \<open>insert x A \<subseteq> S\<close> _ insertI1])
-lemma fold_graph_determ: "fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x"
+lemma fold_graph_determ:
+ assumes "A \<subseteq> S"
+ assumes "fold_graph f z A x" "fold_graph f z A y"
+ shows "y = x"
+ using assms(2-,1)
proof (induct arbitrary: y set: fold_graph)
case emptyI
then show ?case by fast
next
case (insertI x A y v)
- from \<open>fold_graph f z (insert x A) v\<close> and \<open>x \<notin> A\<close>
+ from \<open>insert x A \<subseteq> S\<close> and \<open>fold_graph f z (insert x A) v\<close> and \<open>x \<notin> A\<close>
obtain y' where "v = f x y'" and "fold_graph f z A y'"
by (rule fold_graph_insertE)
- from \<open>fold_graph f z A y'\<close> have "y' = y"
- by (rule insertI)
+ from \<open>fold_graph f z A y'\<close> insertI have "y' = y"
+ by simp
with \<open>v = f x y'\<close> show "v = f x y"
by simp
qed
-lemma fold_equality: "fold_graph f z A y \<Longrightarrow> fold f z A = y"
+lemma fold_equality: "A \<subseteq> S \<Longrightarrow> fold_graph f z A y \<Longrightarrow> fold f z A = y"
by (cases "finite A") (auto simp add: fold_def intro: fold_graph_determ dest: fold_graph_finite)
lemma fold_graph_fold:
+ assumes "A \<subseteq> S"
assumes "finite A"
shows "fold_graph f z A (fold f z A)"
proof -
- from assms have "\<exists>x. fold_graph f z A x"
+ from \<open>finite A\<close> have "\<exists>x. fold_graph f z A x"
by (rule finite_imp_fold_graph)
- moreover note fold_graph_determ
+ moreover note fold_graph_determ[OF \<open>A \<subseteq> S\<close>]
ultimately have "\<exists>!x. fold_graph f z A x"
by (rule ex_ex1I)
then have "fold_graph f z A (The (fold_graph f z A))"
@@ -871,12 +883,13 @@
text \<open>The various recursion equations for \<^const>\<open>fold\<close>:\<close>
lemma fold_insert [simp]:
+ assumes "insert x A \<subseteq> S"
assumes "finite A" and "x \<notin> A"
shows "fold f z (insert x A) = f x (fold f z A)"
-proof (rule fold_equality)
+proof (rule fold_equality[OF \<open>insert x A \<subseteq> S\<close>])
fix z
- from \<open>finite A\<close> have "fold_graph f z A (fold f z A)"
- by (rule fold_graph_fold)
+ from \<open>insert x A \<subseteq> S\<close> \<open>finite A\<close> have "fold_graph f z A (fold f z A)"
+ by (blast intro: fold_graph_fold)
with \<open>x \<notin> A\<close> have "fold_graph f z (insert x A) (f x (fold f z A))"
by (rule fold_graph.insertI)
then show "fold_graph f z (insert x A) (f x (fold f z A))"
@@ -886,20 +899,33 @@
declare (in -) empty_fold_graphE [rule del] fold_graph.intros [rule del]
\<comment> \<open>No more proofs involve these.\<close>
-lemma fold_fun_left_comm: "finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
+lemma fold_fun_left_comm:
+ assumes "insert x A \<subseteq> S" "finite A"
+ shows "f x (fold f z A) = fold f (f x z) A"
+ using assms(2,1)
proof (induct rule: finite_induct)
case empty
then show ?case by simp
next
- case insert
- then show ?case
- by (simp add: fun_left_comm [of x])
+ case (insert y F)
+ then have "fold f (f x z) (insert y F) = f y (fold f (f x z) F)"
+ by simp
+ also have "\<dots> = f x (f y (fold f z F))"
+ using insert by (simp add: fun_left_comm[where ?y=x])
+ also have "\<dots> = f x (fold f z (insert y F))"
+ proof -
+ from insert have "insert y F \<subseteq> S" by simp
+ from fold_insert[OF this] insert show ?thesis by simp
+ qed
+ finally show ?case ..
qed
-lemma fold_insert2: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
+lemma fold_insert2:
+ "insert x A \<subseteq> S \<Longrightarrow> finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
by (simp add: fold_fun_left_comm)
lemma fold_rec:
+ assumes "A \<subseteq> S"
assumes "finite A" and "x \<in> A"
shows "fold f z A = f x (fold f z (A - {x}))"
proof -
@@ -908,11 +934,12 @@
then have "fold f z A = fold f z (insert x (A - {x}))"
by simp
also have "\<dots> = f x (fold f z (A - {x}))"
- by (rule fold_insert) (simp add: \<open>finite A\<close>)+
+ by (rule fold_insert) (use assms in \<open>auto\<close>)
finally show ?thesis .
qed
lemma fold_insert_remove:
+ assumes "insert x A \<subseteq> S"
assumes "finite A"
shows "fold f z (insert x A) = f x (fold f z (A - {x}))"
proof -
@@ -921,20 +948,77 @@
moreover have "x \<in> insert x A"
by auto
ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))"
- by (rule fold_rec)
+ using \<open>insert x A \<subseteq> S\<close> by (blast intro: fold_rec)
then show ?thesis
by simp
qed
lemma fold_set_union_disj:
+ assumes "A \<subseteq> S" "B \<subseteq> S"
assumes "finite A" "finite B" "A \<inter> B = {}"
shows "Finite_Set.fold f z (A \<union> B) = Finite_Set.fold f (Finite_Set.fold f z A) B"
- using assms(2,1,3) by induct simp_all
+ using \<open>finite B\<close> assms(1,2,3,5)
+proof induct
+ case (insert x F)
+ have "fold f z (A \<union> insert x F) = f x (fold f (fold f z A) F)"
+ using insert by auto
+ also have "\<dots> = fold f (fold f z A) (insert x F)"
+ using insert by (blast intro: fold_insert[symmetric])
+ finally show ?case .
+qed simp
+
end
text \<open>Other properties of \<^const>\<open>fold\<close>:\<close>
+lemma fold_graph_image:
+ assumes "inj_on g A"
+ shows "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"
+proof
+ fix w
+ show "fold_graph f z (g ` A) w = fold_graph (f o g) z A w"
+ proof
+ assume "fold_graph f z (g ` A) w"
+ then show "fold_graph (f \<circ> g) z A w"
+ using assms
+ proof (induct "g ` A" w arbitrary: A)
+ case emptyI
+ then show ?case by (auto intro: fold_graph.emptyI)
+ next
+ case (insertI x A r B)
+ from \<open>inj_on g B\<close> \<open>x \<notin> A\<close> \<open>insert x A = image g B\<close> obtain x' A'
+ where "x' \<notin> A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'"
+ by (rule inj_img_insertE)
+ from insertI.prems have "fold_graph (f \<circ> g) z A' r"
+ by (auto intro: insertI.hyps)
+ with \<open>x' \<notin> A'\<close> have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)"
+ by (rule fold_graph.insertI)
+ then show ?case
+ by simp
+ qed
+ next
+ assume "fold_graph (f \<circ> g) z A w"
+ then show "fold_graph f z (g ` A) w"
+ using assms
+ proof induct
+ case emptyI
+ then show ?case
+ by (auto intro: fold_graph.emptyI)
+ next
+ case (insertI x A r)
+ from \<open>x \<notin> A\<close> insertI.prems have "g x \<notin> g ` A"
+ by auto
+ moreover from insertI have "fold_graph f z (g ` A) r"
+ by simp
+ ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)"
+ by (rule fold_graph.insertI)
+ then show ?case
+ by simp
+ qed
+ qed
+qed
+
lemma fold_image:
assumes "inj_on g A"
shows "fold f z (g ` A) = fold (f \<circ> g) z A"
@@ -944,70 +1028,26 @@
by (auto dest: finite_imageD simp add: fold_def)
next
case True
- have "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"
- proof
- fix w
- show "fold_graph f z (g ` A) w \<longleftrightarrow> fold_graph (f \<circ> g) z A w" (is "?P \<longleftrightarrow> ?Q")
- proof
- assume ?P
- then show ?Q
- using assms
- proof (induct "g ` A" w arbitrary: A)
- case emptyI
- then show ?case by (auto intro: fold_graph.emptyI)
- next
- case (insertI x A r B)
- from \<open>inj_on g B\<close> \<open>x \<notin> A\<close> \<open>insert x A = image g B\<close> obtain x' A'
- where "x' \<notin> A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'"
- by (rule inj_img_insertE)
- from insertI.prems have "fold_graph (f \<circ> g) z A' r"
- by (auto intro: insertI.hyps)
- with \<open>x' \<notin> A'\<close> have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)"
- by (rule fold_graph.insertI)
- then show ?case
- by simp
- qed
- next
- assume ?Q
- then show ?P
- using assms
- proof induct
- case emptyI
- then show ?case
- by (auto intro: fold_graph.emptyI)
- next
- case (insertI x A r)
- from \<open>x \<notin> A\<close> insertI.prems have "g x \<notin> g ` A"
- by auto
- moreover from insertI have "fold_graph f z (g ` A) r"
- by simp
- ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)"
- by (rule fold_graph.insertI)
- then show ?case
- by simp
- qed
- qed
- qed
- with True assms show ?thesis
- by (auto simp add: fold_def)
+ then show ?thesis
+ by (auto simp add: fold_def fold_graph_image[OF assms])
qed
lemma fold_cong:
- assumes "comp_fun_commute f" "comp_fun_commute g"
- and "finite A"
+ assumes "comp_fun_commute_on S f" "comp_fun_commute_on S g"
+ and "A \<subseteq> S" "finite A"
and cong: "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
and "s = t" and "A = B"
shows "fold f s A = fold g t B"
proof -
have "fold f s A = fold g s A"
- using \<open>finite A\<close> cong
+ using \<open>finite A\<close> \<open>A \<subseteq> S\<close> cong
proof (induct A)
case empty
then show ?case by simp
next
case insert
- interpret f: comp_fun_commute f by (fact \<open>comp_fun_commute f\<close>)
- interpret g: comp_fun_commute g by (fact \<open>comp_fun_commute g\<close>)
+ interpret f: comp_fun_commute_on S f by (fact \<open>comp_fun_commute_on S f\<close>)
+ interpret g: comp_fun_commute_on S g by (fact \<open>comp_fun_commute_on S g\<close>)
from insert show ?case by simp
qed
with assms show ?thesis by simp
@@ -1016,14 +1056,15 @@
text \<open>A simplified version for idempotent functions:\<close>
-locale comp_fun_idem = comp_fun_commute +
- assumes comp_fun_idem: "f x \<circ> f x = f x"
+locale comp_fun_idem_on = comp_fun_commute_on +
+ assumes comp_fun_idem_on: "x \<in> S \<Longrightarrow> f x \<circ> f x = f x"
begin
-lemma fun_left_idem: "f x (f x z) = f x z"
- using comp_fun_idem by (simp add: fun_eq_iff)
+lemma fun_left_idem: "x \<in> S \<Longrightarrow> f x (f x z) = f x z"
+ using comp_fun_idem_on by (simp add: fun_eq_iff)
lemma fold_insert_idem:
+ assumes "insert x A \<subseteq> S"
assumes fin: "finite A"
shows "fold f z (insert x A) = f x (fold f z A)"
proof cases
@@ -1031,33 +1072,42 @@
then obtain B where "A = insert x B" and "x \<notin> B"
by (rule set_insert)
then show ?thesis
- using assms by (simp add: comp_fun_idem fun_left_idem)
+ using assms by (simp add: comp_fun_idem_on fun_left_idem)
next
assume "x \<notin> A"
then show ?thesis
- using assms by simp
+ using assms by auto
qed
declare fold_insert [simp del] fold_insert_idem [simp]
-lemma fold_insert_idem2: "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
+lemma fold_insert_idem2: "insert x A \<subseteq> S \<Longrightarrow> finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
by (simp add: fold_fun_left_comm)
end
-subsubsection \<open>Liftings to \<open>comp_fun_commute\<close> etc.\<close>
-
-lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f \<circ> g)"
- by standard (simp_all add: comp_fun_commute)
+subsubsection \<open>Liftings to \<open>comp_fun_commute_on\<close> etc.\<close>
+
+lemma (in comp_fun_commute_on) comp_comp_fun_commute_on:
+ "range g \<subseteq> S \<Longrightarrow> comp_fun_commute_on R (f \<circ> g)"
+ by standard (force intro: comp_fun_commute_on)
-lemma (in comp_fun_idem) comp_comp_fun_idem: "comp_fun_idem (f \<circ> g)"
- by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales)
- (simp_all add: comp_fun_idem)
+lemma (in comp_fun_idem_on) comp_comp_fun_idem_on:
+ assumes "range g \<subseteq> S"
+ shows "comp_fun_idem_on R (f \<circ> g)"
+proof
+ interpret f_g: comp_fun_commute_on R "f o g"
+ by (fact comp_comp_fun_commute_on[OF \<open>range g \<subseteq> S\<close>])
+ show "x \<in> R \<Longrightarrow> y \<in> R \<Longrightarrow> (f \<circ> g) y \<circ> (f \<circ> g) x = (f \<circ> g) x \<circ> (f \<circ> g) y" for x y
+ by (fact f_g.comp_fun_commute_on)
+qed (use \<open>range g \<subseteq> S\<close> in \<open>force intro: comp_fun_idem_on\<close>)
-lemma (in comp_fun_commute) comp_fun_commute_funpow: "comp_fun_commute (\<lambda>x. f x ^^ g x)"
+lemma (in comp_fun_commute_on) comp_fun_commute_on_funpow:
+ "comp_fun_commute_on S (\<lambda>x. f x ^^ g x)"
proof
- show "f y ^^ g y \<circ> f x ^^ g x = f x ^^ g x \<circ> f y ^^ g y" for x y
+ fix x y assume "x \<in> S" "y \<in> S"
+ show "f y ^^ g y \<circ> f x ^^ g x = f x ^^ g x \<circ> f y ^^ g y"
proof (cases "x = y")
case True
then show ?thesis by simp
@@ -1082,8 +1132,8 @@
by auto
from Suc h_def have "g y = Suc (h y)"
by simp
- then show ?case
- by (simp add: comp_assoc hyp) (simp add: o_assoc comp_fun_commute)
+ with \<open>x \<in> S\<close> \<open>y \<in> S\<close> show ?case
+ by (simp add: comp_assoc hyp) (simp add: o_assoc comp_fun_commute_on)
qed
define h where "h z = (if z = x then g x - 1 else g z)" for z
with Suc have "n = h x"
@@ -1101,6 +1151,67 @@
qed
+subsubsection \<open>\<^term>\<open>UNIV\<close> as carrier set\<close>
+
+locale comp_fun_commute =
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
+begin
+
+lemma (in -) comp_fun_commute_def': "comp_fun_commute f = comp_fun_commute_on UNIV f"
+ unfolding comp_fun_commute_def comp_fun_commute_on_def by blast
+
+text \<open>
+ We abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that
+ result from instantiating the carrier set to \<^term>\<open>UNIV\<close>.
+\<close>
+sublocale comp_fun_commute_on UNIV f
+ rewrites "\<And>X. (X \<subseteq> UNIV) \<equiv> True"
+ and "\<And>x. x \<in> UNIV \<equiv> True"
+ and "\<And>P. (True \<Longrightarrow> P) \<equiv> Trueprop P"
+ and "\<And>P Q. (True \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> True \<Longrightarrow> PROP Q)"
+proof -
+ show "comp_fun_commute_on UNIV f"
+ by standard (simp add: comp_fun_commute)
+qed simp_all
+
+end
+
+lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f o g)"
+ unfolding comp_fun_commute_def' by (fact comp_comp_fun_commute_on)
+
+lemma (in comp_fun_commute) comp_fun_commute_funpow: "comp_fun_commute (\<lambda>x. f x ^^ g x)"
+ unfolding comp_fun_commute_def' by (fact comp_fun_commute_on_funpow)
+
+locale comp_fun_idem = comp_fun_commute +
+ assumes comp_fun_idem: "f x o f x = f x"
+begin
+
+lemma (in -) comp_fun_idem_def': "comp_fun_idem f = comp_fun_idem_on UNIV f"
+ unfolding comp_fun_idem_on_def comp_fun_idem_def comp_fun_commute_def'
+ unfolding comp_fun_idem_axioms_def comp_fun_idem_on_axioms_def
+ by blast
+
+text \<open>
+ Again, we abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that
+ result from instantiating the carrier set to \<^term>\<open>UNIV\<close>.
+\<close>
+sublocale comp_fun_idem_on UNIV f
+ rewrites "\<And>X. (X \<subseteq> UNIV) \<equiv> True"
+ and "\<And>x. x \<in> UNIV \<equiv> True"
+ and "\<And>P. (True \<Longrightarrow> P) \<equiv> Trueprop P"
+ and "\<And>P Q. (True \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> True \<Longrightarrow> PROP Q)"
+proof -
+ show "comp_fun_idem_on UNIV f"
+ by standard (simp_all add: comp_fun_idem comp_fun_commute)
+qed simp_all
+
+end
+
+lemma (in comp_fun_idem) comp_comp_fun_idem: "comp_fun_idem (f o g)"
+ unfolding comp_fun_idem_def' by (fact comp_comp_fun_idem_on)
+
+
subsubsection \<open>Expressing set operations via \<^const>\<open>fold\<close>\<close>
lemma comp_fun_commute_const: "comp_fun_commute (\<lambda>_. f)"
@@ -1150,8 +1261,12 @@
assumes "finite A"
shows "Set.filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A"
using assms
- by induct
- (auto simp add: Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
+proof -
+ interpret commute_insert: comp_fun_commute "(\<lambda>x A'. if P x then Set.insert x A' else A')"
+ by (fact comp_fun_commute_filter_fold)
+ from \<open>finite A\<close> show ?thesis
+ by induct (auto simp add: Set.filter_def)
+qed
lemma inter_Set_filter:
assumes "finite B"
@@ -1190,7 +1305,7 @@
qed
lemma comp_fun_commute_Pow_fold: "comp_fun_commute (\<lambda>x A. A \<union> Set.insert x ` A)"
- by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast (* somewhat slow *)
+ by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast
lemma Pow_fold:
assumes "finite A"
@@ -1219,9 +1334,12 @@
lemma product_fold:
assumes "finite A" "finite B"
shows "A \<times> B = fold (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B) {} A"
- using assms unfolding Sigma_def
- by (induct A)
- (simp_all add: comp_fun_commute.fold_insert[OF comp_fun_commute_product_fold] fold_union_pair)
+proof -
+ interpret commute_product: comp_fun_commute "(\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B)"
+ by (fact comp_fun_commute_product_fold[OF \<open>finite B\<close>])
+ from assms show ?thesis unfolding Sigma_def
+ by (induct A) (simp_all add: fold_union_pair)
+qed
context complete_lattice
begin
@@ -1309,61 +1427,67 @@
subsubsection \<open>The natural case\<close>
-locale folding =
+locale folding_on =
+ fixes S :: "'a set"
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: "'b"
- assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
+ assumes comp_fun_commute_on: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f y o f x = f x o f y"
begin
-interpretation fold?: comp_fun_commute f
- by standard (use comp_fun_commute in \<open>simp add: fun_eq_iff\<close>)
+interpretation fold?: comp_fun_commute_on S f
+ by standard (simp add: comp_fun_commute_on)
definition F :: "'a set \<Rightarrow> 'b"
- where eq_fold: "F A = fold f z A"
+ where eq_fold: "F A = Finite_Set.fold f z A"
-lemma empty [simp]:"F {} = z"
+lemma empty [simp]: "F {} = z"
by (simp add: eq_fold)
lemma infinite [simp]: "\<not> finite A \<Longrightarrow> F A = z"
by (simp add: eq_fold)
lemma insert [simp]:
- assumes "finite A" and "x \<notin> A"
+ assumes "insert x A \<subseteq> S" and "finite A" and "x \<notin> A"
shows "F (insert x A) = f x (F A)"
proof -
from fold_insert assms
- have "fold f z (insert x A) = f x (fold f z A)" by simp
+ have "Finite_Set.fold f z (insert x A)
+ = f x (Finite_Set.fold f z A)"
+ by simp
with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff)
qed
lemma remove:
- assumes "finite A" and "x \<in> A"
+ assumes "A \<subseteq> S" and "finite A" and "x \<in> A"
shows "F A = f x (F (A - {x}))"
proof -
from \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B"
by (auto dest: mk_disjoint_insert)
moreover from \<open>finite A\<close> A have "finite B" by simp
- ultimately show ?thesis by simp
+ ultimately show ?thesis
+ using \<open>A \<subseteq> S\<close> by auto
qed
-lemma insert_remove: "finite A \<Longrightarrow> F (insert x A) = f x (F (A - {x}))"
- by (cases "x \<in> A") (simp_all add: remove insert_absorb)
+lemma insert_remove:
+ assumes "insert x A \<subseteq> S" and "finite A"
+ shows "F (insert x A) = f x (F (A - {x}))"
+ using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
end
subsubsection \<open>With idempotency\<close>
-locale folding_idem = folding +
- assumes comp_fun_idem: "f x \<circ> f x = f x"
+locale folding_idem_on = folding_on +
+ assumes comp_fun_idem_on: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f x \<circ> f x = f x"
begin
declare insert [simp del]
-interpretation fold?: comp_fun_idem f
- by standard (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
+interpretation fold?: comp_fun_idem_on S f
+ by standard (simp_all add: comp_fun_commute_on comp_fun_idem_on)
lemma insert_idem [simp]:
- assumes "finite A"
+ assumes "insert x A \<subseteq> S" and "finite A"
shows "F (insert x A) = f x (F A)"
proof -
from fold_insert_idem assms
@@ -1373,6 +1497,57 @@
end
+subsubsection \<open>\<^term>\<open>UNIV\<close> as the carrier set\<close>
+
+locale folding =
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: "'b"
+ assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
+begin
+
+lemma (in -) folding_def': "folding f = folding_on UNIV f"
+ unfolding folding_def folding_on_def by blast
+
+text \<open>
+ Again, we abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that
+ result from instantiating the carrier set to \<^term>\<open>UNIV\<close>.
+\<close>
+sublocale folding_on UNIV f
+ rewrites "\<And>X. (X \<subseteq> UNIV) \<equiv> True"
+ and "\<And>x. x \<in> UNIV \<equiv> True"
+ and "\<And>P. (True \<Longrightarrow> P) \<equiv> Trueprop P"
+ and "\<And>P Q. (True \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> True \<Longrightarrow> PROP Q)"
+proof -
+ show "folding_on UNIV f"
+ by standard (simp add: comp_fun_commute)
+qed simp_all
+
+end
+
+locale folding_idem = folding +
+ assumes comp_fun_idem: "f x \<circ> f x = f x"
+begin
+
+lemma (in -) folding_idem_def': "folding_idem f = folding_idem_on UNIV f"
+ unfolding folding_idem_def folding_def' folding_idem_on_def
+ unfolding folding_idem_axioms_def folding_idem_on_axioms_def
+ by blast
+
+text \<open>
+ Again, we abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that
+ result from instantiating the carrier set to \<^term>\<open>UNIV\<close>.
+\<close>
+sublocale folding_idem_on UNIV f
+ rewrites "\<And>X. (X \<subseteq> UNIV) \<equiv> True"
+ and "\<And>x. x \<in> UNIV \<equiv> True"
+ and "\<And>P. (True \<Longrightarrow> P) \<equiv> Trueprop P"
+ and "\<And>P Q. (True \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> True \<Longrightarrow> PROP Q)"
+proof -
+ show "folding_idem_on UNIV f"
+ by standard (simp add: comp_fun_idem)
+qed simp_all
+
+end
+
subsection \<open>Finite cardinality\<close>
@@ -1384,7 +1559,7 @@
\<close>
global_interpretation card: folding "\<lambda>_. Suc" 0
- defines card = "folding.F (\<lambda>_. Suc) 0"
+ defines card = "folding_on.F (\<lambda>_. Suc) 0"
by standard rule
lemma card_insert_disjoint: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> card (insert x A) = Suc (card A)"
--- a/src/HOL/Library/AList.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Library/AList.thy Thu Jun 10 11:54:14 2021 +0200
@@ -423,6 +423,9 @@
finally show ?thesis .
qed
+lemma graph_map_of: "Map.graph (map_of al) = set (clearjunk al)"
+ by (metis distinct_clearjunk graph_map_of_if_distinct_ran map_of_clearjunk)
+
lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)"
by (induct al rule: clearjunk.induct) (simp_all add: delete_update)
--- a/src/HOL/Library/AList_Mapping.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Library/AList_Mapping.thy Thu Jun 10 11:54:14 2021 +0200
@@ -34,6 +34,25 @@
"Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
+lemma entries_Mapping [code]:
+ "Mapping.entries (Mapping xs) = set (AList.clearjunk xs)"
+ by transfer (fact graph_map_of)
+
+lemma ordered_entries_Mapping [code]:
+ "Mapping.ordered_entries (Mapping xs) = sort_key fst (AList.clearjunk xs)"
+proof -
+ have distinct: "distinct (sort_key fst (AList.clearjunk xs))"
+ using distinct_clearjunk distinct_map distinct_sort by blast
+ note folding_Map_graph.idem_if_sorted_distinct[where ?m="map_of xs", OF _ sorted_sort_key distinct]
+ then show ?thesis
+ unfolding ordered_entries_def
+ by (transfer fixing: xs) (auto simp: graph_map_of)
+qed
+
+lemma fold_Mapping [code]:
+ "Mapping.fold f (Mapping xs) a = List.fold (case_prod f) (sort_key fst (AList.clearjunk xs)) a"
+ by (simp add: Mapping.fold_def ordered_entries_Mapping)
+
lemma size_Mapping [code]: "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
--- a/src/HOL/Library/FSet.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Library/FSet.thy Thu Jun 10 11:54:14 2021 +0200
@@ -726,7 +726,8 @@
"\<And>x. x |\<in>| A \<Longrightarrow> f x = g x"
and "s = t" and "A = B"
shows "ffold f s A = ffold g t B"
-using assms by transfer (metis Finite_Set.fold_cong)
+ using assms[unfolded comp_fun_commute_def']
+ by transfer (meson Finite_Set.fold_cong subset_UNIV)
context comp_fun_idem
begin
--- a/src/HOL/Library/Finite_Lattice.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Library/Finite_Lattice.thy Thu Jun 10 11:54:14 2021 +0200
@@ -170,15 +170,36 @@
context finite_distrib_lattice_complete
begin
subclass finite_distrib_lattice
- apply standard
- apply (simp_all add: Inf_def Sup_def bot_def top_def)
- apply (metis (mono_tags) insert_UNIV local.Sup_fin.eq_fold local.bot_def local.finite_UNIV local.top_def)
- apply (simp add: comp_fun_idem.fold_insert_idem local.comp_fun_idem_inf)
- apply (metis (mono_tags) insert_UNIV local.Inf_fin.eq_fold local.finite_UNIV)
- apply (simp add: comp_fun_idem.fold_insert_idem local.comp_fun_idem_sup)
- apply (metis (mono_tags) insert_UNIV local.Inf_fin.eq_fold local.finite_UNIV)
- apply (metis (mono_tags) insert_UNIV local.Sup_fin.eq_fold local.finite_UNIV)
- done
+proof -
+ show "class.finite_distrib_lattice Inf Sup inf (\<le>) (<) sup bot top"
+ proof
+ show "bot = Inf UNIV"
+ unfolding bot_def top_def Inf_def
+ using Inf_fin.eq_fold Inf_fin.insert inf.absorb2 by force
+ next
+ show "top = Sup UNIV"
+ unfolding bot_def top_def Sup_def
+ using Sup_fin.eq_fold Sup_fin.insert by force
+ next
+ show "Inf {} = Sup UNIV"
+ unfolding Inf_def Sup_def bot_def top_def
+ using Sup_fin.eq_fold Sup_fin.insert by force
+ next
+ show "Sup {} = Inf UNIV"
+ unfolding Inf_def Sup_def bot_def top_def
+ using Inf_fin.eq_fold Inf_fin.insert inf.absorb2 by force
+ next
+ interpret comp_fun_idem_inf: comp_fun_idem inf
+ by (fact comp_fun_idem_inf)
+ show "Inf (insert a A) = inf a (Inf A)" for a A
+ using comp_fun_idem_inf.fold_insert_idem Inf_def finite by simp
+ next
+ interpret comp_fun_idem_sup: comp_fun_idem sup
+ by (fact comp_fun_idem_sup)
+ show "Sup (insert a A) = sup a (Sup A)" for a A
+ using comp_fun_idem_sup.fold_insert_idem Sup_def finite by simp
+ qed
+qed
end
instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice ..
--- a/src/HOL/Library/Lexord.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Library/Lexord.thy Thu Jun 10 11:54:14 2021 +0200
@@ -194,8 +194,6 @@
apply (auto simp add: dvd_strict_def)
done
-print_theorems
-
global_interpretation lex_dvd: preordering lex_dvd lex_dvd_strict
by (fact dvd.preordering)
--- a/src/HOL/Library/Mapping.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Library/Mapping.thy Thu Jun 10 11:54:14 2021 +0200
@@ -5,7 +5,7 @@
section \<open>An abstract view on maps for code generation.\<close>
theory Mapping
-imports Main
+imports Main AList
begin
subsection \<open>Parametricity transfer rules\<close>
@@ -43,6 +43,16 @@
shows "((A ===> rel_option B) ===> rel_set A) dom dom"
unfolding dom_def [abs_def] Option.is_none_def [symmetric] by transfer_prover
+lemma graph_parametric:
+ assumes "bi_total A"
+ shows "((A ===> rel_option B) ===> rel_set (rel_prod A B)) Map.graph Map.graph"
+proof
+ fix f g assume "(A ===> rel_option B) f g"
+ with assms[unfolded bi_total_def] show "rel_set (rel_prod A B) (Map.graph f) (Map.graph g)"
+ unfolding graph_def rel_set_def rel_fun_def
+ by auto (metis option_rel_Some1 option_rel_Some2)+
+qed
+
lemma map_of_parametric [transfer_rule]:
assumes [transfer_rule]: "bi_unique R1"
shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
@@ -129,6 +139,9 @@
lift_definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set"
is dom parametric dom_parametric .
+lift_definition entries :: "('a, 'b) mapping \<Rightarrow> ('a \<times> 'b) set"
+ is Map.graph parametric graph_parametric .
+
lift_definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping"
is "\<lambda>ks f. (map_of (List.map (\<lambda>k. (k, f k)) ks))" parametric tabulate_parametric .
@@ -166,6 +179,13 @@
definition ordered_keys :: "('a::linorder, 'b) mapping \<Rightarrow> 'a list"
where "ordered_keys m = (if finite (keys m) then sorted_list_of_set (keys m) else [])"
+definition ordered_entries :: "('a::linorder, 'b) mapping \<Rightarrow> ('a \<times> 'b) list"
+ where "ordered_entries m = (if finite (entries m) then sorted_key_list_of_set fst (entries m)
+ else [])"
+
+definition fold :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> 'c \<Rightarrow> 'c"
+ where "fold f m a = List.fold (case_prod f) (ordered_entries m) a"
+
definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool"
where "is_empty m \<longleftrightarrow> keys m = {}"
@@ -462,7 +482,13 @@
by transfer rule
lemma keys_empty [simp]: "keys empty = {}"
- by transfer simp
+ by transfer (fact dom_empty)
+
+lemma in_keysD: "k \<in> keys m \<Longrightarrow> \<exists>v. lookup m k = Some v"
+ by transfer (fact domD)
+
+lemma in_entriesI: "lookup m k = Some v \<Longrightarrow> (k, v) \<in> entries m"
+ by transfer (fact in_graphI)
lemma keys_update [simp]: "keys (update k v m) = insert k (keys m)"
by transfer simp
@@ -515,7 +541,7 @@
"finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow>
ordered_keys (update k v m) = insort k (ordered_keys m)"
by (simp_all add: ordered_keys_def)
- (auto simp only: sorted_list_of_set_insert [symmetric] insert_absorb)
+ (auto simp only: sorted_list_of_set_insert_remove[symmetric] insert_absorb)
lemma ordered_keys_delete [simp]: "ordered_keys (delete k m) = remove1 k (ordered_keys m)"
proof (cases "finite (keys m)")
@@ -559,14 +585,14 @@
lemma ordered_keys_bulkload [simp]: "ordered_keys (bulkload ks) = [0..<length ks]"
by (simp add: ordered_keys_def)
-lemma tabulate_fold: "tabulate xs f = fold (\<lambda>k m. update k (f k) m) xs empty"
+lemma tabulate_fold: "tabulate xs f = List.fold (\<lambda>k m. update k (f k) m) xs empty"
proof transfer
fix f :: "'a \<Rightarrow> 'b" and xs
have "map_of (List.map (\<lambda>k. (k, f k)) xs) = foldr (\<lambda>k m. m(k \<mapsto> f k)) xs Map.empty"
by (simp add: foldr_map comp_def map_of_foldr)
- also have "foldr (\<lambda>k m. m(k \<mapsto> f k)) xs = fold (\<lambda>k m. m(k \<mapsto> f k)) xs"
+ also have "foldr (\<lambda>k m. m(k \<mapsto> f k)) xs = List.fold (\<lambda>k m. m(k \<mapsto> f k)) xs"
by (rule foldr_fold) (simp add: fun_eq_iff)
- ultimately show "map_of (List.map (\<lambda>k. (k, f k)) xs) = fold (\<lambda>k m. m(k \<mapsto> f k)) xs Map.empty"
+ ultimately show "map_of (List.map (\<lambda>k. (k, f k)) xs) = List.fold (\<lambda>k m. m(k \<mapsto> f k)) xs Map.empty"
by simp
qed
@@ -647,10 +673,262 @@
end
+subsubsection \<open>@{term [source] entries}, @{term [source] ordered_entries},
+ and @{term [source] fold}\<close>
+
+context linorder
+begin
+
+sublocale folding_Map_graph: folding_insort_key "(\<le>)" "(<)" "Map.graph m" fst for m
+ by unfold_locales (fact inj_on_fst_graph)
+
+end
+
+lemma sorted_fst_list_of_set_insort_Map_graph[simp]:
+ assumes "finite (dom m)" "fst x \<notin> dom m"
+ shows "sorted_key_list_of_set fst (insert x (Map.graph m))
+ = insort_key fst x (sorted_key_list_of_set fst (Map.graph m))"
+proof(cases x)
+ case (Pair k v)
+ with \<open>fst x \<notin> dom m\<close> have "Map.graph m \<subseteq> Map.graph (m(k \<mapsto> v))"
+ by(auto simp: graph_def)
+ moreover from Pair \<open>fst x \<notin> dom m\<close> have "(k, v) \<notin> Map.graph m"
+ using graph_domD by fastforce
+ ultimately show ?thesis
+ using Pair assms folding_Map_graph.sorted_key_list_of_set_insert[where ?m="m(k \<mapsto> v)"]
+ by auto
+qed
+
+lemma sorted_fst_list_of_set_insort_insert_Map_graph[simp]:
+ assumes "finite (dom m)" "fst x \<notin> dom m"
+ shows "sorted_key_list_of_set fst (insert x (Map.graph m))
+ = insort_insert_key fst x (sorted_key_list_of_set fst (Map.graph m))"
+proof(cases x)
+ case (Pair k v)
+ with \<open>fst x \<notin> dom m\<close> have "Map.graph m \<subseteq> Map.graph (m(k \<mapsto> v))"
+ by(auto simp: graph_def)
+ with assms Pair show ?thesis
+ unfolding sorted_fst_list_of_set_insort_Map_graph[OF assms] insort_insert_key_def
+ using folding_Map_graph.set_sorted_key_list_of_set in_graphD by (fastforce split: if_splits)
+qed
+
+lemma linorder_finite_Map_induct[consumes 1, case_names empty update]:
+ fixes m :: "'a::linorder \<rightharpoonup> 'b"
+ assumes "finite (dom m)"
+ assumes "P Map.empty"
+ assumes "\<And>k v m. \<lbrakk> finite (dom m); k \<notin> dom m; (\<And>k'. k' \<in> dom m \<Longrightarrow> k' \<le> k); P m \<rbrakk>
+ \<Longrightarrow> P (m(k \<mapsto> v))"
+ shows "P m"
+proof -
+ let ?key_list = "\<lambda>m. sorted_list_of_set (dom m)"
+ from assms(1,2) show ?thesis
+ proof(induction "length (?key_list m)" arbitrary: m)
+ case 0
+ then have "sorted_list_of_set (dom m) = []"
+ by auto
+ with \<open>finite (dom m)\<close> have "m = Map.empty"
+ by auto
+ with \<open>P Map.empty\<close> show ?case by simp
+ next
+ case (Suc n)
+ then obtain x xs where x_xs: "sorted_list_of_set (dom m) = xs @ [x]"
+ by (metis append_butlast_last_id length_greater_0_conv zero_less_Suc)
+ have "sorted_list_of_set (dom (m(x := None))) = xs"
+ proof -
+ have "distinct (xs @ [x])"
+ by (metis sorted_list_of_set.distinct_sorted_key_list_of_set x_xs)
+ then have "remove1 x (xs @ [x]) = xs"
+ by (simp add: remove1_append)
+ with \<open>finite (dom m)\<close> x_xs show ?thesis
+ by (simp add: sorted_list_of_set_remove)
+ qed
+ moreover have "k \<le> x" if "k \<in> dom (m(x := None))" for k
+ proof -
+ from x_xs have "sorted (xs @ [x])"
+ by (metis sorted_list_of_set.sorted_sorted_key_list_of_set)
+ moreover from \<open>k \<in> dom (m(x := None))\<close> have "k \<in> set xs"
+ using \<open>finite (dom m)\<close> \<open>sorted_list_of_set (dom (m(x := None))) = xs\<close>
+ by auto
+ ultimately show "k \<le> x"
+ by (simp add: sorted_append)
+ qed
+ moreover from \<open>finite (dom m)\<close> have "finite (dom (m(x := None)))" "x \<notin> dom (m(x := None))"
+ by simp_all
+ moreover have "P (m(x := None))"
+ using Suc \<open>sorted_list_of_set (dom (m(x := None))) = xs\<close> x_xs by auto
+ ultimately show ?case
+ using assms(3)[where ?m="m(x := None)"] by (metis fun_upd_triv fun_upd_upd not_Some_eq)
+ qed
+qed
+
+lemma delete_insort_fst[simp]: "AList.delete k (insort_key fst (k, v) xs) = AList.delete k xs"
+ by (induction xs) simp_all
+
+lemma insort_fst_delete: "\<lbrakk> fst x \<noteq> k2; sorted (List.map fst xs) \<rbrakk>
+ \<Longrightarrow> insort_key fst x (AList.delete k2 xs) = AList.delete k2 (insort_key fst x xs)"
+ by (induction xs) (fastforce simp add: insort_is_Cons order_trans)+
+
+lemma sorted_fst_list_of_set_Map_graph_fun_upd_None[simp]:
+ "sorted_key_list_of_set fst (Map.graph (m(k := None)))
+ = AList.delete k (sorted_key_list_of_set fst (Map.graph m))"
+proof(cases "finite (Map.graph m)")
+ assume "finite (Map.graph m)"
+ from this[unfolded finite_graph_iff_finite_dom] show ?thesis
+ proof(induction rule: finite_Map_induct)
+ let ?list_of="sorted_key_list_of_set fst"
+ case (update k2 v2 m)
+ note [simp] = \<open>k2 \<notin> dom m\<close> \<open>finite (dom m)\<close>
+
+ have right_eq: "AList.delete k (?list_of (Map.graph (m(k2 \<mapsto> v2))))
+ = AList.delete k (insort_key fst (k2, v2) (?list_of (Map.graph m)))"
+ by simp
+
+ show ?case
+ proof(cases "k = k2")
+ case True
+ then have "?list_of (Map.graph ((m(k2 \<mapsto> v2))(k := None)))
+ = AList.delete k (insort_key fst (k2, v2) (?list_of (Map.graph m)))"
+ using fst_graph_eq_dom update.IH by auto
+ then show ?thesis
+ using right_eq by metis
+ next
+ case False
+ then have "AList.delete k (insort_key fst (k2, v2) (?list_of (Map.graph m)))
+ = insort_key fst (k2, v2) (?list_of (Map.graph (m(k := None))))"
+ by (auto simp add: insort_fst_delete update.IH
+ folding_Map_graph.sorted_sorted_key_list_of_set[OF subset_refl])
+ also have "\<dots> = ?list_of (insert (k2, v2) (Map.graph (m(k := None))))"
+ by auto
+ also from False \<open>k2 \<notin> dom m\<close> have "\<dots> = ?list_of (Map.graph ((m(k2 \<mapsto> v2))(k := None)))"
+ by (metis graph_map_upd domIff fun_upd_triv fun_upd_twist)
+ finally show ?thesis using right_eq by metis
+ qed
+ qed simp
+qed simp
+
+lemma entries_lookup: "entries m = Map.graph (lookup m)"
+ by transfer rule
+
+lemma entries_empty[simp]: "entries empty = {}"
+ by transfer (fact graph_empty)
+
+lemma finite_entries_iff_finite_keys[simp]:
+ "finite (entries m) = finite (keys m)"
+ by transfer (fact finite_graph_iff_finite_dom)
+
+lemma entries_update[simp]:
+ "entries (update k v m) = insert (k, v) (entries (delete k m))"
+ by transfer (fact graph_map_upd)
+
+lemma Mapping_delete_if_notin_keys[simp]:
+ "k \<notin> Mapping.keys m \<Longrightarrow> delete k m = m"
+ by transfer simp
+
+lemma entries_delete:
+ "entries (delete k m) = {e \<in> entries m. fst e \<noteq> k}"
+ by transfer (fact graph_fun_upd_None)
+
+lemma entries_of_alist[simp]:
+ "distinct (List.map fst xs) \<Longrightarrow> entries (of_alist xs) = set xs"
+ by transfer (fact graph_map_of_if_distinct_ran)
+
+lemma entries_keysD:
+ "x \<in> entries m \<Longrightarrow> fst x \<in> keys m"
+ by transfer (fact graph_domD)
+
+lemma finite_keys_entries[simp]:
+ "finite (keys (update k v m)) = finite (keys m)"
+ by transfer simp
+
+lemma set_ordered_entries[simp]:
+ "finite (Mapping.keys m) \<Longrightarrow> set (ordered_entries m) = entries m"
+ unfolding ordered_entries_def
+ by transfer (auto simp: folding_Map_graph.set_sorted_key_list_of_set[OF subset_refl])
+
+lemma distinct_ordered_entries[simp]: "distinct (List.map fst (ordered_entries m))"
+ unfolding ordered_entries_def
+ by transfer (simp add: folding_Map_graph.distinct_sorted_key_list_of_set[OF subset_refl])
+
+lemma sorted_ordered_entries[simp]: "sorted (List.map fst (ordered_entries m))"
+ unfolding ordered_entries_def
+ by transfer (auto intro: folding_Map_graph.sorted_sorted_key_list_of_set)
+
+lemma ordered_entries_infinite[simp]:
+ "\<not> finite (Mapping.keys m) \<Longrightarrow> ordered_entries m = []"
+ by (simp add: ordered_entries_def)
+
+lemma ordered_entries_empty[simp]: "ordered_entries empty = []"
+ by (simp add: ordered_entries_def)
+
+lemma ordered_entries_update[simp]:
+ assumes "finite (keys m)"
+ shows "ordered_entries (update k v m)
+ = insort_insert_key fst (k, v) (AList.delete k (ordered_entries m))"
+proof -
+ let ?list_of="sorted_key_list_of_set fst" and ?insort="insort_insert_key fst"
+
+ have *: "?list_of (insert (k, v) (Map.graph (m(k := None))))
+ = ?insort (k, v) (AList.delete k (?list_of (Map.graph m)))" if "finite (dom m)" for m
+ proof -
+ from \<open>finite (dom m)\<close> have "?list_of (insert (k, v) (Map.graph (m(k := None))))
+ = ?insort (k, v) (?list_of (Map.graph (m(k := None))))"
+ by (intro sorted_fst_list_of_set_insort_insert_Map_graph) (simp_all add: subset_insertI)
+ then show ?thesis by simp
+ qed
+ from assms show ?thesis
+ unfolding ordered_entries_def
+ apply (transfer fixing: k v) using "*" by auto
+qed
+
+lemma ordered_entries_delete[simp]:
+ "ordered_entries (delete k m) = AList.delete k (ordered_entries m)"
+ unfolding ordered_entries_def by transfer auto
+
+lemma fold_empty[simp]: "fold f empty a = a"
+ unfolding fold_def by simp
+
+lemma insort_key_is_snoc_if_sorted_and_distinct:
+ assumes "sorted (List.map f xs)" "f y \<notin> f ` set xs" "\<forall>x \<in> set xs. f x \<le> f y"
+ shows "insort_key f y xs = xs @ [y]"
+ using assms by (induction xs) (auto dest!: insort_is_Cons)
+
+lemma fold_update:
+ assumes "finite (keys m)"
+ assumes "k \<notin> keys m" "\<And>k'. k' \<in> keys m \<Longrightarrow> k' \<le> k"
+ shows "fold f (update k v m) a = f k v (fold f m a)"
+proof -
+ from assms have k_notin_entries: "k \<notin> fst ` set (ordered_entries m)"
+ using entries_keysD by fastforce
+ with assms have "ordered_entries (update k v m)
+ = insort_insert_key fst (k, v) (ordered_entries m)"
+ by simp
+ also from k_notin_entries have "\<dots> = ordered_entries m @ [(k, v)]"
+ proof -
+ from assms have "\<forall>x \<in> set (ordered_entries m). fst x \<le> fst (k, v)"
+ unfolding ordered_entries_def
+ by transfer (fastforce simp: folding_Map_graph.set_sorted_key_list_of_set[OF order_refl]
+ dest: graph_domD)
+ from insort_key_is_snoc_if_sorted_and_distinct[OF _ _ this] k_notin_entries show ?thesis
+ unfolding insort_insert_key_def by auto
+ qed
+ finally show ?thesis unfolding fold_def by simp
+qed
+
+lemma linorder_finite_Mapping_induct[consumes 1, case_names empty update]:
+ fixes m :: "('a::linorder, 'b) mapping"
+ assumes "finite (keys m)"
+ assumes "P empty"
+ assumes "\<And>k v m.
+ \<lbrakk> finite (keys m); k \<notin> keys m; (\<And>k'. k' \<in> keys m \<Longrightarrow> k' \<le> k); P m \<rbrakk>
+ \<Longrightarrow> P (update k v m)"
+ shows "P m"
+ using assms by transfer (simp add: linorder_finite_Map_induct)
+
subsection \<open>Code generator setup\<close>
hide_const (open) empty is_empty rep lookup lookup_default filter update delete ordered_keys
keys size replace default map_entry map_default tabulate bulkload map map_values combine of_alist
+ entries ordered_entries fold
end
--- a/src/HOL/Library/Multiset.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Jun 10 11:54:14 2021 +0200
@@ -1610,7 +1610,7 @@
by (simp add: not_in_iff)
from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (add_mset x M) y) s (set_mset M) =
Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_mset M)"
- by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
+ by (auto intro!: Finite_Set.fold_cong comp_fun_commute_on_funpow)
with False * show ?thesis
by (simp add: fold_mset_def del: count_add_mset)
next
@@ -1619,7 +1619,7 @@
from N_def True have *: "set_mset M = insert x N" "x \<notin> N" "finite N" by auto
then have "Finite_Set.fold (\<lambda>y. f y ^^ count (add_mset x M) y) s N =
Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
- by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
+ by (auto intro!: Finite_Set.fold_cong comp_fun_commute_on_funpow)
with * show ?thesis by (simp add: fold_mset_def del: count_add_mset) simp
qed
qed
@@ -1984,7 +1984,7 @@
by (induct xs) simp_all
global_interpretation mset_set: folding add_mset "{#}"
- defines mset_set = "folding.F add_mset {#}"
+ defines mset_set = "folding_on.F add_mset {#}"
by standard (simp add: fun_eq_iff)
lemma sum_multiset_singleton [simp]: "sum (\<lambda>n. {#n#}) A = mset_set A"
--- a/src/HOL/Library/RBT.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Library/RBT.thy Thu Jun 10 11:54:14 2021 +0200
@@ -196,6 +196,9 @@
lemma distinct_entries: "distinct (List.map fst (entries t))"
by transfer (simp add: distinct_entries)
+lemma sorted_entries: "sorted (List.map fst (entries t))"
+ by (transfer) (simp add: rbt_sorted_entries)
+
lemma non_empty_keys: "t \<noteq> empty \<Longrightarrow> keys t \<noteq> []"
by transfer (simp add: non_empty_rbt_keys)
--- a/src/HOL/Library/RBT_Mapping.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Library/RBT_Mapping.thy Thu Jun 10 11:54:14 2021 +0200
@@ -57,6 +57,24 @@
unfolding ordered_keys_def
by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique)
+lemma Map_graph_lookup: "Map.graph (RBT.lookup t) = set (RBT.entries t)"
+ by (metis RBT.distinct_entries RBT.map_of_entries graph_map_of_if_distinct_ran)
+
+lemma entries_Mapping [code]: "Mapping.entries (Mapping t) = set (RBT.entries t)"
+ by (transfer fixing: t) (fact Map_graph_lookup)
+
+lemma ordered_entries_Mapping [code]: "Mapping.ordered_entries (Mapping t) = RBT.entries t"
+proof -
+ note folding_Map_graph.idem_if_sorted_distinct[
+ where ?m="RBT.lookup t", OF _ _ folding_Map_graph.distinct_if_distinct_map]
+ then show ?thesis
+ unfolding ordered_entries_def
+ by (transfer fixing: t) (auto simp: Map_graph_lookup distinct_entries sorted_entries)
+qed
+
+lemma fold_Mapping [code]: "Mapping.fold f (Mapping t) a = RBT.fold f t a"
+ by (simp add: Mapping.fold_def fold_fold ordered_entries_Mapping)
+
lemma Mapping_size_card_keys: (*FIXME*)
"Mapping.size m = card (Mapping.keys m)"
unfolding size_def by transfer simp
@@ -100,7 +118,7 @@
lemma equal_Mapping [code]:
"HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> RBT.entries t1 = RBT.entries t2"
- by (transfer fixing: t1 t2) (simp add: entries_lookup)
+ by (transfer fixing: t1 t2) (simp add: RBT.entries_lookup)
lemma [code nbe]:
"HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
--- a/src/HOL/Library/RBT_Set.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Library/RBT_Set.thy Thu Jun 10 11:54:14 2021 +0200
@@ -58,6 +58,8 @@
assumes "comp_fun_commute f"
shows "Finite_Set.fold f A (set (RBT.entries t)) = RBT.fold (curry f) t A"
proof -
+ interpret comp_fun_commute: comp_fun_commute f
+ by (fact assms)
have *: "remdups (RBT.entries t) = RBT.entries t"
using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
--- a/src/HOL/Lifting_Set.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Lifting_Set.thy Thu Jun 10 11:54:14 2021 +0200
@@ -329,4 +329,44 @@
shows "rel_set R (\<Union>(f ` A)) (\<Union>(g ` B))"
by transfer_prover
+context
+ includes lifting_syntax
+begin
+
+lemma fold_graph_transfer[transfer_rule]:
+ assumes "bi_unique R" "right_total R"
+ shows "((R ===> (=) ===> (=)) ===> (=) ===> rel_set R ===> (=) ===> (=)) fold_graph fold_graph"
+proof(intro rel_funI)
+ fix f1 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c" and f2 :: "'b \<Rightarrow> 'c \<Rightarrow> 'c"
+ assume rel_f: "(R ===> (=) ===> (=)) f1 f2"
+ fix z1 z2 :: 'c assume [simp]: "z1 = z2"
+ fix A1 A2 assume rel_A: "rel_set R A1 A2"
+ fix y1 y2 :: 'c assume [simp]: "y1 = y2"
+
+ from \<open>bi_unique R\<close> \<open>right_total R\<close> have The_y: "\<forall>y. \<exists>!x. R x y"
+ unfolding bi_unique_def right_total_def by auto
+ define r where "r \<equiv> \<lambda>y. THE x. R x y"
+
+ from The_y have r_y: "R (r y) y" for y
+ unfolding r_def using the_equality by fastforce
+ with assms rel_A have "inj_on r A2" "A1 = r ` A2"
+ unfolding r_def rel_set_def inj_on_def bi_unique_def
+ apply(auto simp: image_iff) by metis+
+ with \<open>bi_unique R\<close> rel_f r_y have "(f1 o r) y = f2 y" for y
+ unfolding bi_unique_def rel_fun_def by auto
+ then have "(f1 o r) = f2"
+ by blast
+ then show "fold_graph f1 z1 A1 y1 = fold_graph f2 z2 A2 y2"
+ by (fastforce simp: fold_graph_image[OF \<open>inj_on r A2\<close>] \<open>A1 = r ` A2\<close>)
+qed
+
+lemma fold_transfer[transfer_rule]:
+ assumes [transfer_rule]: "bi_unique R" "right_total R"
+ shows "((R ===> (=) ===> (=)) ===> (=) ===> rel_set R ===> (=)) Finite_Set.fold Finite_Set.fold"
+ unfolding Finite_Set.fold_def
+ by transfer_prover
+
end
+
+
+end
--- a/src/HOL/List.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/List.thy Thu Jun 10 11:54:14 2021 +0200
@@ -3124,13 +3124,16 @@
text \<open>\<^const>\<open>Finite_Set.fold\<close> and \<^const>\<open>fold\<close>\<close>
-lemma (in comp_fun_commute) fold_set_fold_remdups:
- "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
- by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm insert_absorb)
-
-lemma (in comp_fun_idem) fold_set_fold:
- "Finite_Set.fold f y (set xs) = fold f xs y"
- by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm)
+lemma (in comp_fun_commute_on) fold_set_fold_remdups:
+ assumes "set xs \<subseteq> S"
+ shows "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
+ by (rule sym, use assms in \<open>induct xs arbitrary: y\<close>)
+ (simp_all add: insert_absorb fold_fun_left_comm)
+
+lemma (in comp_fun_idem_on) fold_set_fold:
+ assumes "set xs \<subseteq> S"
+ shows "Finite_Set.fold f y (set xs) = fold f xs y"
+ by (rule sym, use assms in \<open>induct xs arbitrary: y\<close>) (simp_all add: fold_fun_left_comm)
lemma union_set_fold [code]: "set xs \<union> A = fold Set.insert xs A"
proof -
@@ -5785,6 +5788,10 @@
lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
by(induct xs)(auto simp: set_insort_key)
+lemma distinct_insort_key:
+ "distinct (map f (insort_key f x xs)) = (f x \<notin> f ` set xs \<and> (distinct (map f xs)))"
+by (induct xs) (auto simp: set_insort_key)
+
lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
by (induct xs) (simp_all add: distinct_insort)
@@ -5897,8 +5904,8 @@
"filter P (sort_key f xs) = sort_key f (filter P xs)"
by (induct xs) (simp_all add: filter_insort_triv filter_insort)
-lemma remove1_insort [simp]:
- "remove1 x (insort x xs) = xs"
+lemma remove1_insort_key [simp]:
+ "remove1 x (insort_key f x xs) = xs"
by (induct xs) simp_all
end
@@ -6087,98 +6094,149 @@
qed
-subsubsection \<open>\<open>sorted_list_of_set\<close>\<close>
-
-text\<open>This function maps (finite) linearly ordered sets to sorted
-lists. Warning: in most cases it is not a good idea to convert from
-sets to lists but one should convert in the other direction (via
-\<^const>\<open>set\<close>).\<close>
-
-context linorder
+subsubsection \<open>\<open>sorted_key_list_of_set\<close>\<close>
+
+text\<open>
+ This function maps (finite) linearly ordered sets to sorted lists.
+ The linear order is obtained by a key function that maps the elements of the set to a type
+ that is linearly ordered.
+ Warning: in most cases it is not a good idea to convert from
+ sets to lists but one should convert in the other direction (via \<^const>\<open>set\<close>).
+
+ Note: this is a generalisation of the older \<open>sorted_list_of_set\<close> that is obtained by setting
+ the key function to the identity. Consequently, new theorems should be added to the locale
+ below. They should also be aliased to more convenient names for use with \<open>sorted_list_of_set\<close>
+ as seen further below.
+\<close>
+
+definition (in linorder) sorted_key_list_of_set :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'b list"
+ where "sorted_key_list_of_set f \<equiv> folding_on.F (insort_key f) []"
+
+locale folding_insort_key = lo?: linorder "less_eq :: 'a \<Rightarrow> 'a \<Rightarrow> bool" less
+ for less_eq (infix "\<preceq>" 50) and less (infix "\<prec>" 50) +
+ fixes S
+ fixes f :: "'b \<Rightarrow> 'a"
+ assumes inj_on: "inj_on f S"
begin
-definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
- "sorted_list_of_set = folding.F insort []"
-
-sublocale sorted_list_of_set: folding insort Nil
-rewrites
- "folding.F insort [] = sorted_list_of_set"
+lemma insort_key_commute:
+ "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> insort_key f y o insort_key f x = insort_key f x o insort_key f y"
+proof(rule ext, goal_cases)
+ case (1 xs)
+ with inj_on show ?case by (induction xs) (auto simp: inj_onD)
+qed
+
+sublocale fold_insort_key: folding_on S "insort_key f" "[]"
+ rewrites "folding_on.F (insort_key f) [] = sorted_key_list_of_set f"
proof -
- interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
- show "folding insort" by standard (fact comp_fun_commute)
- show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def)
-qed
-
-lemma sorted_list_of_set_empty:
- "sorted_list_of_set {} = []"
- by (fact sorted_list_of_set.empty)
-
-lemma sorted_list_of_set_insert [simp]:
- "finite A \<Longrightarrow> sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
- by (fact sorted_list_of_set.insert_remove)
-
-lemma sorted_list_of_set_eq_Nil_iff [simp]:
- "finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
- by (auto simp: sorted_list_of_set.remove)
-
-lemma set_sorted_list_of_set [simp]:
- "finite A \<Longrightarrow> set (sorted_list_of_set A) = A"
- by(induct A rule: finite_induct) (simp_all add: set_insort_key)
-
-lemma sorted_sorted_list_of_set [simp]: "sorted (sorted_list_of_set A)"
+ show "folding_on S (insort_key f)"
+ by standard (simp add: insort_key_commute)
+qed (simp add: sorted_key_list_of_set_def)
+
+lemma idem_if_sorted_distinct:
+ assumes "set xs \<subseteq> S" and "sorted (map f xs)" "distinct xs"
+ shows "sorted_key_list_of_set f (set xs) = xs"
+proof(cases "S = {}")
+ case True
+ then show ?thesis using \<open>set xs \<subseteq> S\<close> by auto
+next
+ case False
+ with assms show ?thesis
+ proof(induction xs)
+ case (Cons a xs)
+ with Cons show ?case by (cases xs) auto
+ qed simp
+qed
+
+lemma sorted_key_list_of_set_empty:
+ "sorted_key_list_of_set f {} = []"
+ by (fact fold_insort_key.empty)
+
+lemma sorted_key_list_of_set_insert:
+ assumes "insert x A \<subseteq> S" and "finite A" "x \<notin> A"
+ shows "sorted_key_list_of_set f (insert x A)
+ = insort_key f x (sorted_key_list_of_set f A)"
+ using assms by (fact fold_insort_key.insert)
+
+lemma sorted_key_list_of_set_insert_remove [simp]:
+ assumes "insert x A \<subseteq> S" and "finite A"
+ shows "sorted_key_list_of_set f (insert x A)
+ = insort_key f x (sorted_key_list_of_set f (A - {x}))"
+ using assms by (fact fold_insort_key.insert_remove)
+
+lemma sorted_key_list_of_set_eq_Nil_iff [simp]:
+ assumes "A \<subseteq> S" and "finite A"
+ shows "sorted_key_list_of_set f A = [] \<longleftrightarrow> A = {}"
+ using assms by (auto simp: fold_insort_key.remove)
+
+lemma set_sorted_key_list_of_set [simp]:
+ assumes "A \<subseteq> S" and "finite A"
+ shows "set (sorted_key_list_of_set f A) = A"
+ using assms(2,1)
+ by (induct A rule: finite_induct) (simp_all add: set_insort_key)
+
+lemma sorted_sorted_key_list_of_set [simp]:
+ assumes "A \<subseteq> S"
+ shows "sorted (map f (sorted_key_list_of_set f A))"
proof (cases "finite A")
- case True thus ?thesis by(induction A) (simp_all add: sorted_insort)
+ case True thus ?thesis using \<open>A \<subseteq> S\<close>
+ by (induction A) (simp_all add: sorted_insort_key)
next
case False thus ?thesis by simp
qed
-lemma distinct_sorted_list_of_set [simp]: "distinct (sorted_list_of_set A)"
+lemma distinct_if_distinct_map: "distinct (map f xs) \<Longrightarrow> distinct xs"
+ using inj_on by (simp add: distinct_map)
+
+lemma distinct_sorted_key_list_of_set [simp]:
+ assumes "A \<subseteq> S"
+ shows "distinct (map f (sorted_key_list_of_set f A))"
proof (cases "finite A")
- case True thus ?thesis by(induction A) (simp_all add: distinct_insort)
-next
+ case True thus ?thesis using \<open>A \<subseteq> S\<close> inj_on
+ by (induction A) (force simp: distinct_insort_key dest: inj_onD)+
+ next
case False thus ?thesis by simp
qed
-lemma length_sorted_list_of_set [simp]: "length (sorted_list_of_set A) = card A"
+lemma length_sorted_key_list_of_set [simp]:
+ assumes "A \<subseteq> S"
+ shows "length (sorted_key_list_of_set f A) = card A"
proof (cases "finite A")
case True
- then show ?thesis
- by(metis distinct_card distinct_sorted_list_of_set set_sorted_list_of_set)
+ with assms inj_on show ?thesis
+ using distinct_card[symmetric, OF distinct_sorted_key_list_of_set]
+ by (auto simp: subset_inj_on intro!: card_image)
qed auto
-lemmas sorted_list_of_set = set_sorted_list_of_set sorted_sorted_list_of_set distinct_sorted_list_of_set
-
-lemma sorted_list_of_set_sort_remdups [code]:
- "sorted_list_of_set (set xs) = sort (remdups xs)"
-proof -
- interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
- show ?thesis by (simp add: sorted_list_of_set.eq_fold sort_conv_fold fold_set_fold_remdups)
-qed
-
-lemma sorted_list_of_set_remove:
- assumes "finite A"
- shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
+lemmas sorted_key_list_of_set =
+ set_sorted_key_list_of_set sorted_sorted_key_list_of_set distinct_sorted_key_list_of_set
+
+lemma sorted_key_list_of_set_remove:
+ assumes "insert x A \<subseteq> S" and "finite A"
+ shows "sorted_key_list_of_set f (A - {x}) = remove1 x (sorted_key_list_of_set f A)"
proof (cases "x \<in> A")
- case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
+ case False with assms have "x \<notin> set (sorted_key_list_of_set f A)" by simp
with False show ?thesis by (simp add: remove1_idem)
next
case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
with assms show ?thesis by simp
qed
-lemma strict_sorted_list_of_set [simp]: "sorted_wrt (<) (sorted_list_of_set A)"
- by (simp add: strict_sorted_iff)
+lemma strict_sorted_key_list_of_set [simp]:
+ "A \<subseteq> S \<Longrightarrow> sorted_wrt (\<prec>) (map f (sorted_key_list_of_set f A))"
+ by (cases "finite A") (auto simp: strict_sorted_iff subset_inj_on[OF inj_on])
lemma finite_set_strict_sorted:
- assumes "finite A"
- obtains l where "sorted_wrt (<) l" "set l = A" "length l = card A"
- by (metis assms distinct_card distinct_sorted_list_of_set set_sorted_list_of_set strict_sorted_list_of_set)
-
-lemma strict_sorted_equal:
+ assumes "A \<subseteq> S" and "finite A"
+ obtains l where "sorted_wrt (\<prec>) (map f l)" "set l = A" "length l = card A"
+ using assms
+ by (meson length_sorted_key_list_of_set set_sorted_key_list_of_set strict_sorted_key_list_of_set)
+
+lemma (in linorder) strict_sorted_equal:
assumes "sorted_wrt (<) xs"
- and "sorted_wrt (<) ys"
- and "set ys = set xs"
- shows "ys = xs"
+ and "sorted_wrt (<) ys"
+ and "set ys = set xs"
+ shows "ys = xs"
using assms
proof (induction xs arbitrary: ys)
case (Cons x xs)
@@ -6197,22 +6255,73 @@
using local.Cons by blast
qed
qed auto
-
-lemma strict_sorted_equal_Uniq: "\<exists>\<^sub>\<le>\<^sub>1xs. sorted_wrt (<) xs \<and> set xs = A"
+
+lemma (in linorder) strict_sorted_equal_Uniq: "\<exists>\<^sub>\<le>\<^sub>1xs. sorted_wrt (<) xs \<and> set xs = A"
by (simp add: Uniq_def strict_sorted_equal)
-lemma sorted_list_of_set_inject:
- assumes "sorted_list_of_set A = sorted_list_of_set B" "finite A" "finite B"
+lemma sorted_key_list_of_set_inject:
+ assumes "A \<subseteq> S" "B \<subseteq> S"
+ assumes "sorted_key_list_of_set f A = sorted_key_list_of_set f B" "finite A" "finite B"
shows "A = B"
- using assms set_sorted_list_of_set by fastforce
-
-lemma sorted_list_of_set_unique:
- assumes "finite A"
- shows "sorted_wrt (<) l \<and> set l = A \<and> length l = card A \<longleftrightarrow> sorted_list_of_set A = l"
- using assms strict_sorted_equal by force
+ using assms set_sorted_key_list_of_set by metis
+
+lemma sorted_key_list_of_set_unique:
+ assumes "A \<subseteq> S" and "finite A"
+ shows "sorted_wrt (\<prec>) (map f l) \<and> set l = A \<and> length l = card A
+ \<longleftrightarrow> sorted_key_list_of_set f A = l"
+ using assms
+ by (auto simp: strict_sorted_iff card_distinct idem_if_sorted_distinct)
end
+context linorder
+begin
+
+definition "sorted_list_of_set \<equiv> sorted_key_list_of_set (\<lambda>x::'a. x)"
+
+text \<open>
+ We abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that result
+ from instantiating the key function to the identity.
+\<close>
+sublocale sorted_list_of_set: folding_insort_key "(\<le>)" "(<)" UNIV "(\<lambda>x. x)"
+ rewrites "sorted_key_list_of_set (\<lambda>x. x) = sorted_list_of_set"
+ and "\<And>xs. map (\<lambda>x. x) xs \<equiv> xs"
+ and "\<And>X. (X \<subseteq> UNIV) \<equiv> True"
+ and "\<And>x. x \<in> UNIV \<equiv> True"
+ and "\<And>P. (True \<Longrightarrow> P) \<equiv> Trueprop P"
+ and "\<And>P Q. (True \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> True \<Longrightarrow> PROP Q)"
+proof -
+ show "folding_insort_key (\<le>) (<) UNIV (\<lambda>x. x)"
+ by standard simp
+qed (simp_all add: sorted_list_of_set_def)
+
+text \<open>Alias theorems for backwards compatibility and ease of use.\<close>
+lemmas sorted_list_of_set = sorted_list_of_set.sorted_key_list_of_set and
+ sorted_list_of_set_empty = sorted_list_of_set.sorted_key_list_of_set_empty and
+ sorted_list_of_set_insert = sorted_list_of_set.sorted_key_list_of_set_insert and
+ sorted_list_of_set_insert_remove = sorted_list_of_set.sorted_key_list_of_set_insert_remove and
+ sorted_list_of_set_eq_Nil_iff = sorted_list_of_set.sorted_key_list_of_set_eq_Nil_iff and
+ set_sorted_list_of_set = sorted_list_of_set.set_sorted_key_list_of_set and
+ sorted_sorted_list_of_set = sorted_list_of_set.sorted_sorted_key_list_of_set and
+ distinct_sorted_list_of_set = sorted_list_of_set.distinct_sorted_key_list_of_set and
+ length_sorted_list_of_set = sorted_list_of_set.length_sorted_key_list_of_set and
+ sorted_list_of_set_remove = sorted_list_of_set.sorted_key_list_of_set_remove and
+ strict_sorted_list_of_set = sorted_list_of_set.strict_sorted_key_list_of_set and
+ sorted_list_of_set_inject = sorted_list_of_set.sorted_key_list_of_set_inject and
+ sorted_list_of_set_unique = sorted_list_of_set.sorted_key_list_of_set_unique and
+ finite_set_strict_sorted = sorted_list_of_set.finite_set_strict_sorted
+
+lemma sorted_list_of_set_sort_remdups [code]:
+ "sorted_list_of_set (set xs) = sort (remdups xs)"
+proof -
+ interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
+ show ?thesis
+ by (simp add: sorted_list_of_set.fold_insort_key.eq_fold sort_conv_fold fold_set_fold_remdups)
+qed
+
+end
+
+
lemma sorted_list_of_set_range [simp]:
"sorted_list_of_set {m..<n} = [m..<n]"
by (rule sorted_distinct_set_unique) simp_all
@@ -6228,7 +6337,8 @@
lemma sorted_list_of_set_nonempty:
assumes "finite A" "A \<noteq> {}"
shows "sorted_list_of_set A = Min A # sorted_list_of_set (A - {Min A})"
- using assms by (auto simp: less_le simp flip: sorted_list_of_set_unique intro: Min_in)
+ using assms
+ by (auto simp: less_le simp flip: sorted_list_of_set.sorted_key_list_of_set_unique intro: Min_in)
lemma sorted_list_of_set_greaterThanLessThan:
assumes "Suc i < j"
--- a/src/HOL/Map.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Map.thy Thu Jun 10 11:54:14 2021 +0200
@@ -42,6 +42,10 @@
"ran m = {b. \<exists>a. m a = Some b}"
definition
+ graph :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<times> 'b) set" where
+ "graph m = {(a, b) | a b. m a = Some b}"
+
+definition
map_le :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix "\<subseteq>\<^sub>m" 50) where
"(m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2) \<longleftrightarrow> (\<forall>a \<in> dom m\<^sub>1. m\<^sub>1 a = m\<^sub>2 a)"
@@ -660,6 +664,9 @@
unfolding ran_def
by force
+lemma fun_upd_None_if_notin_dom[simp]: "k \<notin> dom m \<Longrightarrow> m(k := None) = m"
+ by auto
+
lemma ran_map_add:
assumes "dom m1 \<inter> dom m2 = {}"
shows "ran (m1 ++ m2) = ran m1 \<union> ran m2"
@@ -710,6 +717,62 @@
lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
by (auto simp add: ran_def)
+subsection \<open>@{term [source] graph}\<close>
+
+lemma graph_empty[simp]: "graph empty = {}"
+ unfolding graph_def by simp
+
+lemma in_graphI: "m k = Some v \<Longrightarrow> (k, v) \<in> graph m"
+ unfolding graph_def by blast
+
+lemma in_graphD: "(k, v) \<in> graph m \<Longrightarrow> m k = Some v"
+ unfolding graph_def by blast
+
+lemma graph_map_upd[simp]: "graph (m(k \<mapsto> v)) = insert (k, v) (graph (m(k := None)))"
+ unfolding graph_def by (auto split: if_splits)
+
+lemma graph_fun_upd_None: "graph (m(k := None)) = {e \<in> graph m. fst e \<noteq> k}"
+ unfolding graph_def by (auto split: if_splits)
+
+lemma graph_restrictD:
+ assumes "(k, v) \<in> graph (m |` A)"
+ shows "k \<in> A" and "m k = Some v"
+ using assms unfolding graph_def
+ by (auto simp: restrict_map_def split: if_splits)
+
+lemma graph_map_comp[simp]: "graph (m1 \<circ>\<^sub>m m2) = graph m2 O graph m1"
+ unfolding graph_def by (auto simp: map_comp_Some_iff relcomp_unfold)
+
+lemma graph_map_add: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> graph (m1 ++ m2) = graph m1 \<union> graph m2"
+ unfolding graph_def using map_add_comm by force
+
+lemma graph_eq_to_snd_dom: "graph m = (\<lambda>x. (x, the (m x))) ` dom m"
+ unfolding graph_def dom_def by force
+
+lemma fst_graph_eq_dom: "fst ` graph m = dom m"
+ unfolding graph_eq_to_snd_dom by force
+
+lemma graph_domD: "x \<in> graph m \<Longrightarrow> fst x \<in> dom m"
+ using fst_graph_eq_dom by (metis imageI)
+
+lemma snd_graph_ran: "snd ` graph m = ran m"
+ unfolding graph_def ran_def by force
+
+lemma graph_ranD: "x \<in> graph m \<Longrightarrow> snd x \<in> ran m"
+ using snd_graph_ran by (metis imageI)
+
+lemma finite_graph_map_of: "finite (graph (map_of al))"
+ unfolding graph_eq_to_snd_dom finite_dom_map_of
+ using finite_dom_map_of by blast
+
+lemma graph_map_of_if_distinct_ran: "distinct (map fst al) \<Longrightarrow> graph (map_of al) = set al"
+ unfolding graph_def by auto
+
+lemma finite_graph_iff_finite_dom[simp]: "finite (graph m) = finite (dom m)"
+ by (metis graph_eq_to_snd_dom finite_imageI fst_graph_eq_dom)
+
+lemma inj_on_fst_graph: "inj_on fst (graph m)"
+ unfolding graph_def inj_on_def by force
subsection \<open>\<open>map_le\<close>\<close>
@@ -857,6 +920,23 @@
qed
qed
-hide_const (open) Map.empty
+lemma finite_Map_induct[consumes 1, case_names empty update]:
+ assumes "finite (dom m)"
+ assumes "P Map.empty"
+ assumes "\<And>k v m. finite (dom m) \<Longrightarrow> k \<notin> dom m \<Longrightarrow> P m \<Longrightarrow> P (m(k \<mapsto> v))"
+ shows "P m"
+ using assms(1)
+proof(induction "dom m" arbitrary: m rule: finite_induct)
+ case empty
+ then show ?case using assms(2) unfolding dom_def by simp
+next
+ case (insert x F)
+ then have "finite (dom (m(x:=None)))" "x \<notin> dom (m(x:=None))" "P (m(x:=None))"
+ by (metis Diff_insert_absorb dom_fun_upd)+
+ with assms(3)[OF this] show ?case
+ by (metis fun_upd_triv fun_upd_upd option.exhaust)
+qed
+
+hide_const (open) Map.empty Map.graph
end
--- a/src/HOL/Relation.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Relation.thy Thu Jun 10 11:54:14 2021 +0200
@@ -1242,9 +1242,12 @@
assumes "finite R" "finite S"
shows "R O S = Finite_Set.fold
(\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R"
- using assms
- by (induct R)
- (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
- cong: if_cong)
+proof -
+ interpret commute_relcomp_fold: comp_fun_commute
+ "(\<lambda>(x, y) A. Finite_Set.fold (\<lambda>(w, z) A'. if y = w then insert (x, z) A' else A') A S)"
+ by (fact comp_fun_commute_relcomp_fold[OF \<open>finite S\<close>])
+ from assms show ?thesis
+ by (induct R) (auto simp: comp_fun_commute_relcomp_fold insert_relcomp_fold cong: if_cong)
+qed
end
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Thu Jun 10 11:54:14 2021 +0200
@@ -177,7 +177,8 @@
val name = Toplevel.name_of tr;
val pos = Toplevel.pos_of tr;
in
- if can (Proof.assert_backward o Toplevel.proof_of) st andalso
+ if Context.proper_subthy (\<^theory>, thy) andalso
+ can (Proof.assert_backward o Toplevel.proof_of) st andalso
member (op =) whitelist name andalso check_thy pos
then SOME {theory_index = thy_index, name = name, pos = pos,
pre = Toplevel.proof_of st, post = st'}
--- a/src/HOL/Topological_Spaces.thy Thu Jun 10 11:21:57 2021 +0200
+++ b/src/HOL/Topological_Spaces.thy Thu Jun 10 11:54:14 2021 +0200
@@ -35,7 +35,7 @@
using open_Union [of "B ` A"] by simp
lemma open_Inter [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
- by (induct set: finite) auto
+ by (induction set: finite) auto
lemma open_INT [continuous_intros, intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
using open_Inter [of "B ` A"] by simp
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Interpretation_in_nested_targets.thy Thu Jun 10 11:54:14 2021 +0200
@@ -0,0 +1,36 @@
+theory Interpretation_in_nested_targets
+ imports Main
+begin
+
+locale injection =
+ fixes f :: \<open>'a \<Rightarrow> 'b\<close>
+ assumes eqI: \<open>f x = f y \<Longrightarrow> x = y\<close>
+begin
+
+lemma eq_iff:
+ \<open>x = y \<longleftrightarrow> f x = f y\<close>
+ by (auto intro: eqI)
+
+lemma inv_apply:
+ \<open>inv f (f x) = x\<close>
+ by (rule inv_f_f) (simp add: eqI injI)
+
+end
+
+context
+ fixes f :: \<open>'a::linorder \<Rightarrow> 'b::linorder\<close>
+ assumes \<open>strict_mono f\<close>
+begin
+
+global_interpretation strict_mono: injection f
+ by standard (simp add: \<open>strict_mono f\<close> strict_mono_eq)
+
+thm strict_mono.eq_iff
+thm strict_mono.inv_apply
+
+end
+
+thm strict_mono.eq_iff
+thm strict_mono.inv_apply
+
+end
--- a/src/Pure/General/output.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/General/output.ML Thu Jun 10 11:54:14 2021 +0200
@@ -10,9 +10,6 @@
val tracing: string -> unit
val warning: string -> unit
val legacy_feature: string -> unit
- val profile_time: ('a -> 'b) -> 'a -> 'b
- val profile_time_thread: ('a -> 'b) -> 'a -> 'b
- val profile_allocations: ('a -> 'b) -> 'a -> 'b
end;
signature OUTPUT =
@@ -158,40 +155,6 @@
fun protocol_message props body = ! protocol_message_fn props body;
fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => ();
-
-(* profiling *)
-
-local
-
-fun output_profile title entries =
- let
- val body = entries
- |> sort (int_ord o apply2 fst)
- |> map (fn (count, name) =>
- let
- val c = string_of_int count;
- val prefix = replicate_string (Int.max (0, 10 - size c)) " ";
- in prefix ^ c ^ " " ^ name end);
- val total = fold (curry (op +) o fst) entries 0;
- in
- if total = 0 then ()
- else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total])))
- end;
-
-in
-
-fun profile_time f x =
- ML_Profiling.profile_time (output_profile "time profile:") f x;
-
-fun profile_time_thread f x =
- ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x;
-
-fun profile_allocations f x =
- ML_Profiling.profile_allocations (output_profile "allocations profile:") f x;
-
-end;
-
-
end;
structure Output: OUTPUT = Private_Output;
--- a/src/Pure/Isar/class.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Isar/class.ML Thu Jun 10 11:54:14 2021 +0200
@@ -493,7 +493,7 @@
val add_dependency =
(case some_dep_morph of
SOME dep_morph =>
- Locale.add_dependency sub
+ Generic_Target.locale_dependency sub
{inst = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)),
mixin = NONE, export = export}
| NONE => I);
@@ -667,7 +667,7 @@
fun registration thy_ctxt {inst, mixin, export} lthy =
lthy
- |> Locale.add_registration_theory
+ |> Generic_Target.theory_registration
{inst = inst,
mixin = mixin,
export = export $> Proof_Context.export_morphism lthy thy_ctxt}
--- a/src/Pure/Isar/class_declaration.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Isar/class_declaration.ML Thu Jun 10 11:54:14 2021 +0200
@@ -331,10 +331,10 @@
|-> (fn (param_map, params, assm_axiom) =>
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)
#-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
- Locale.add_registration_theory'
+ Context.theory_map (Locale.add_registration
{inst = (class, base_morph),
mixin = Option.map (rpair true) eq_morph,
- export = export_morph}
+ export = export_morph})
#> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
#> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
|> snd
--- a/src/Pure/Isar/generic_target.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML Thu Jun 10 11:54:14 2021 +0200
@@ -29,6 +29,8 @@
(morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
+ val local_interpretation: Locale.registration ->
+ local_theory -> local_theory
(*lifting target primitives to local theory operations*)
val define: (((binding * typ) * mixfix) * (binding * term) ->
@@ -54,6 +56,7 @@
val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
local_theory -> (term * term) * local_theory
val theory_declaration: declaration -> local_theory -> local_theory
+ val theory_registration: Locale.registration -> local_theory -> local_theory
(*locale target primitives*)
val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list ->
@@ -71,6 +74,8 @@
local_theory -> local_theory
val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
+ val locale_dependency: string -> Locale.registration ->
+ local_theory -> local_theory
end
structure Generic_Target: GENERIC_TARGET =
@@ -230,6 +235,15 @@
fun standard_const pred prmode ((b, mx), rhs) =
standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
+fun standard_registration pred registration lthy =
+ Local_Theory.map_contexts (fn level =>
+ if pred (Local_Theory.level lthy, level)
+ then Context.proof_map (Locale.add_registration registration)
+ else I) lthy;
+
+val local_interpretation = standard_registration (fn (n, level) => level = n - 1);
+
+
(** lifting target primitives to local theory operations **)
@@ -393,6 +407,16 @@
fun theory_declaration decl =
background_declaration decl #> standard_declaration (K true) decl;
+fun target_registration lthy {inst, mixin, export} =
+ {inst = inst, mixin = mixin,
+ export = export $> Proof_Context.export_morphism lthy (Local_Theory.target_of lthy)};
+
+fun theory_registration registration lthy =
+ lthy
+ |> (Local_Theory.raw_theory o Context.theory_map)
+ (Locale.add_registration (target_registration lthy registration))
+ |> standard_registration (K true) registration;
+
(** locale target primitives **)
@@ -424,6 +448,11 @@
locale_target_const locale (K true) prmode ((b, mx), rhs)
#> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
+fun locale_dependency loc registration lthy =
+ lthy
+ |> Local_Theory.raw_theory (Locale.add_dependency loc registration)
+ |> standard_registration (K true) registration;
+
(** locale abbreviations **)
--- a/src/Pure/Isar/interpretation.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Isar/interpretation.ML Thu Jun 10 11:54:14 2021 +0200
@@ -140,11 +140,16 @@
(fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
"interpret" propss eqns goal_ctxt state;
+fun add_registration_proof registration ctxt = ctxt
+ |> Proof_Context.set_stmt false
+ |> Context.proof_map (Locale.add_registration registration)
+ |> Proof_Context.restore_stmt ctxt;
+
fun gen_interpret prep_interpretation expression state =
Proof.assert_forward_or_chain state
|> Proof.context_of
|> generic_interpretation prep_interpretation (setup_proof state)
- Attrib.local_notes Locale.add_registration_proof expression [];
+ Attrib.local_notes add_registration_proof expression [];
in
@@ -157,7 +162,7 @@
(* interpretation in local theories *)
val add_registration_local_theory =
- Named_Target.revoke_reinitializability oo Locale.add_registration_local_theory;
+ Named_Target.revoke_reinitializability oo Generic_Target.local_interpretation;
fun interpretation expression =
generic_interpretation cert_interpretation Element.witness_proof_eqs
--- a/src/Pure/Isar/local_theory.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Isar/local_theory.ML Thu Jun 10 11:54:14 2021 +0200
@@ -253,6 +253,7 @@
val operations_of = #operations o top_of;
fun operation f lthy = f (operations_of lthy) lthy;
+fun operation1 f x = operation (fn ops => f ops x);
fun operation2 f x y = operation (fn ops => f ops x y);
@@ -264,10 +265,9 @@
val define_internal = operation2 #define true;
val notes_kind = operation2 #notes;
val declaration = operation2 #declaration;
-fun theory_registration registration =
- assert_bottom #> operation (fn ops => #theory_registration ops registration);
+val theory_registration = operation1 #theory_registration;
fun locale_dependency registration =
- assert_bottom #> operation (fn ops => #locale_dependency ops registration);
+ assert_bottom #> operation1 #locale_dependency registration;
(* theorems *)
--- a/src/Pure/Isar/locale.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Isar/locale.ML Thu Jun 10 11:54:14 2021 +0200
@@ -79,13 +79,8 @@
type registration = {inst: string * morphism, mixin: (morphism * bool) option, export: morphism}
val amend_registration: registration -> Context.generic -> Context.generic
val add_registration: registration -> Context.generic -> Context.generic
- val add_registration_theory': registration -> theory -> theory
- val add_registration_theory: registration -> local_theory -> local_theory
- val add_registration_local_theory: registration -> local_theory -> local_theory
- val add_registration_proof: registration -> Proof.context -> Proof.context
val registrations_of: Context.generic -> string -> (string * morphism) list
- val add_dependency': string -> registration -> theory -> theory
- val add_dependency: string -> registration -> local_theory -> local_theory
+ val add_dependency: string -> registration -> theory -> theory
(* Diagnostic *)
val get_locales: theory -> string list
@@ -611,21 +606,6 @@
|> activate_facts (SOME export) (name, mix_morph $> pos_morph)
end;
-val add_registration_theory' = Context.theory_map o add_registration;
-
-val add_registration_theory = Local_Theory.raw_theory o add_registration_theory';
-
-fun add_registration_local_theory registration lthy =
- let val n = Local_Theory.level lthy in
- lthy
- |> Local_Theory.map_contexts (fn level =>
- level = n - 1 ? Context.proof_map (add_registration registration))
- end;
-
-fun add_registration_proof registration ctxt = ctxt
- |> Proof_Context.set_stmt false
- |> Context.proof_map (add_registration registration)
- |> Proof_Context.restore_stmt ctxt;
(*** Dependencies ***)
@@ -637,7 +617,7 @@
|> map (fn (name, (base, export)) =>
(name, base $> (collect_mixins context (name, base $> export)) $> export));
-fun add_dependency' loc {inst = (name, morph), mixin, export} thy =
+fun add_dependency loc {inst = (name, morph), mixin, export} thy =
let
val dep = make_dep (name, (morph, export));
val add_dep =
@@ -649,13 +629,10 @@
fold_rev (roundup thy' cons export)
(registrations_of context' loc) (Idents.get context', []);
in
- fold_rev (fn inst => add_registration_theory' {inst = inst, mixin = NONE, export = export})
+ fold_rev (fn inst => Context.theory_map (add_registration {inst = inst, mixin = NONE, export = export}))
regs thy'
end;
-fun add_dependency loc registration =
- Local_Theory.raw_theory (add_dependency' loc registration)
- #> add_registration_local_theory registration;
(*** Storing results ***)
--- a/src/Pure/Isar/named_target.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Isar/named_target.ML Thu Jun 10 11:54:14 2021 +0200
@@ -94,7 +94,7 @@
notes = Generic_Target.notes Generic_Target.theory_target_notes,
abbrev = Generic_Target.theory_abbrev,
declaration = fn _ => Generic_Target.theory_declaration,
- theory_registration = Locale.add_registration_theory,
+ theory_registration = Generic_Target.theory_registration,
locale_dependency = fn _ => error "Not possible in theory target",
pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]}
@@ -104,7 +104,7 @@
abbrev = Generic_Target.locale_abbrev locale,
declaration = Generic_Target.locale_declaration locale,
theory_registration = fn _ => error "Not possible in locale target",
- locale_dependency = Locale.add_dependency locale,
+ locale_dependency = Generic_Target.locale_dependency locale,
pretty = fn ctxt => [Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale]}
| operations (Class class) =
{define = Generic_Target.define (class_foundation class),
@@ -112,7 +112,7 @@
abbrev = Class.abbrev class,
declaration = Generic_Target.locale_declaration class,
theory_registration = fn _ => error "Not possible in class target",
- locale_dependency = Locale.add_dependency class,
+ locale_dependency = Generic_Target.locale_dependency class,
pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class};
fun setup_context Theory = Proof_Context.init_global
--- a/src/Pure/Isar/overloading.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Isar/overloading.ML Thu Jun 10 11:54:14 2021 +0200
@@ -210,7 +210,7 @@
notes = Generic_Target.notes Generic_Target.theory_target_notes,
abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
declaration = K Generic_Target.theory_declaration,
- theory_registration = Locale.add_registration_theory,
+ theory_registration = Generic_Target.theory_registration,
locale_dependency = fn _ => error "Not possible in overloading target",
pretty = pretty}
end;
--- a/src/Pure/Isar/runtime.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Isar/runtime.ML Thu Jun 10 11:54:14 2021 +0200
@@ -194,7 +194,8 @@
f |> debugging1 opt_context |> debugging2 opt_context;
fun controlled_execution opt_context f x =
- (f |> debugging opt_context |> Future.interruptible_task) x;
+ (f |> debugging opt_context |> Future.interruptible_task
+ |> ML_Profiling.profile (Options.default_string "profiling")) x;
fun toplevel_error output_exn f x = f x
handle exn =>
--- a/src/Pure/ML/ml_profiling.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/ML/ml_profiling.ML Thu Jun 10 11:54:14 2021 +0200
@@ -1,26 +1,76 @@
(* Title: Pure/ML/ml_profiling.ML
Author: Makarius
-ML profiling.
+ML profiling (via Poly/ML run-time system).
*)
+signature BASIC_ML_PROFILING =
+sig
+ val profile_time: ('a -> 'b) -> 'a -> 'b
+ val profile_time_thread: ('a -> 'b) -> 'a -> 'b
+ val profile_allocations: ('a -> 'b) -> 'a -> 'b
+end;
+
signature ML_PROFILING =
sig
- val profile_time: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
- val profile_time_thread: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
- val profile_allocations: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
+ val check_mode: string -> unit
+ val profile: string -> ('a -> 'b) -> 'a -> 'b
+ include BASIC_ML_PROFILING
end;
structure ML_Profiling: ML_PROFILING =
struct
-fun profile_time pr f x =
- PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
+(* mode *)
+
+val modes =
+ Symtab.make
+ [("time", PolyML.Profiling.ProfileTime),
+ ("time_thread", PolyML.Profiling.ProfileTimeThisThread),
+ ("allocations", PolyML.Profiling.ProfileAllocations)];
+
+fun get_mode kind =
+ (case Symtab.lookup modes kind of
+ SOME mode => mode
+ | NONE => error ("Bad profiling mode: " ^ quote kind));
+
+fun check_mode "" = ()
+ | check_mode kind = ignore (get_mode kind);
+
+
+(* profile *)
-fun profile_time_thread pr f x =
- PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
+fun print_entry count name =
+ let
+ val c = string_of_int count;
+ val prefix = Symbol.spaces (Int.max (0, 12 - size c));
+ in prefix ^ c ^ " " ^ name end;
-fun profile_allocations pr f x =
- PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
+fun profile "" f x = f x
+ | profile kind f x =
+ let
+ val mode = get_mode kind;
+ fun output entries =
+ (case fold (curry (op +) o fst) entries 0 of
+ 0 => ()
+ | total =>
+ let
+ val body = entries
+ |> sort (int_ord o apply2 fst)
+ |> map (fn (count, name) =>
+ let val markup = Markup.ML_profiling_entry {name = name, count = count}
+ in XML.Elem (markup, [XML.Text (print_entry count name ^ "\n")]) end);
+ val head = XML.Text ("profile_" ^ kind ^ ":\n");
+ val foot = XML.Text (print_entry total "TOTAL");
+ val msg = XML.Elem (Markup.ML_profiling kind, head :: body @ [foot]);
+ in tracing (YXML.string_of msg) end);
+ in PolyML.Profiling.profileStream output mode f x end;
+
+fun profile_time f = profile "time" f;
+fun profile_time_thread f = profile "time_thread" f;
+fun profile_allocations f = profile "allocations" f;
end;
+
+structure Basic_ML_Profiling: BASIC_ML_PROFILING = ML_Profiling;
+open Basic_ML_Profiling;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_profiling.scala Thu Jun 10 11:54:14 2021 +0200
@@ -0,0 +1,49 @@
+/* Title: Pure/ML/ml_profiling.scala
+ Author: Makarius
+
+ML profiling (via Poly/ML run-time system).
+*/
+
+package isabelle
+
+
+import java.util.Locale
+
+import scala.collection.immutable.SortedMap
+
+
+object ML_Profiling
+{
+ sealed case class Entry(name: String, count: Long)
+ {
+ def clean_name: Entry = copy(name = """-?\(\d+\).*$""".r.replaceAllIn(name, ""))
+
+ def print: String =
+ String.format(Locale.ROOT, "%12d %s",
+ count.asInstanceOf[AnyRef], name.asInstanceOf[AnyRef])
+ }
+
+ sealed case class Report(kind: String, entries: List[Entry])
+ {
+ def clean_name: Report = copy(entries = entries.map(_.clean_name))
+
+ def total: Entry = Entry("TOTAL", entries.iterator.map(_.count).sum)
+
+ def print: String =
+ ("profile_" + kind + ":\n") + cat_lines((entries ::: List(total)).map(_.print))
+ }
+
+ def account(reports: List[Report]): List[Report] =
+ {
+ val empty = SortedMap.empty[String, Long].withDefaultValue(0L)
+ var results = SortedMap.empty[String, SortedMap[String, Long]].withDefaultValue(empty)
+ for (report <- reports) {
+ val kind = report.kind
+ val map = report.entries.foldLeft(results(kind))(
+ (m, e) => m + (e.name -> (e.count + m(e.name))))
+ results = results + (kind -> map)
+ }
+ for ((kind, map) <- results.toList)
+ yield Report(kind, for ((name, count) <- map.toList.sortBy(_._2)) yield Entry(name, count))
+ }
+}
--- a/src/Pure/PIDE/markup.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/PIDE/markup.ML Thu Jun 10 11:54:14 2021 +0200
@@ -202,6 +202,11 @@
val no_reportN: string val no_report: T
val badN: string val bad: unit -> T
val intensifyN: string val intensify: T
+ val countN: string
+ val ML_profiling_entryN: string
+ val ML_profiling_entry: {name: string, count: int} -> T
+ val ML_profilingN: string
+ val ML_profiling: string -> T
val browserN: string
val graphviewN: string
val theory_exportsN: string
@@ -657,6 +662,17 @@
val (intensifyN, intensify) = markup_elem "intensify";
+(* ML profiling *)
+
+val countN = "count";
+
+val ML_profiling_entryN = "ML_profiling_entry";
+fun ML_profiling_entry {name, count} =
+ (ML_profiling_entryN, [(nameN, name), (countN, Value.print_int count)]);
+
+val (ML_profilingN, ML_profiling) = markup_string "ML_profiling" kindN;
+
+
(* active areas *)
val browserN = "browser"
--- a/src/Pure/PIDE/markup.scala Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/PIDE/markup.scala Thu Jun 10 11:54:14 2021 +0200
@@ -564,6 +564,30 @@
val INTENSIFY = "intensify"
+ /* ML profiling */
+
+ val COUNT = "count"
+ val ML_PROFILING_ENTRY = "ML_profiling_entry"
+ val ML_PROFILING = "ML_profiling"
+
+ object ML_Profiling
+ {
+ def unapply_entry(tree: XML.Tree): Option[isabelle.ML_Profiling.Entry] =
+ tree match {
+ case XML.Elem(Markup(ML_PROFILING_ENTRY, List((NAME, name), (COUNT, Value.Long(count)))), _) =>
+ Some(isabelle.ML_Profiling.Entry(name, count))
+ case _ => None
+ }
+
+ def unapply_report(tree: XML.Tree): Option[isabelle.ML_Profiling.Report] =
+ tree match {
+ case XML.Elem(Markup(ML_PROFILING, List((KIND, kind))), body) =>
+ Some(isabelle.ML_Profiling.Report(kind, body.flatMap(unapply_entry)))
+ case _ => None
+ }
+ }
+
+
/* active areas */
val BROWSER = "browser"
--- a/src/Pure/PIDE/protocol.scala Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/PIDE/protocol.scala Thu Jun 10 11:54:14 2021 +0200
@@ -210,6 +210,19 @@
}
+ /* ML profiling */
+
+ object ML_Profiling
+ {
+ def unapply(msg: XML.Tree): Option[isabelle.ML_Profiling.Report] =
+ msg match {
+ case XML.Elem(_, List(tree)) if is_tracing(msg) =>
+ Markup.ML_Profiling.unapply_report(tree)
+ case _ => None
+ }
+ }
+
+
/* export */
object Export
--- a/src/Pure/ROOT.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/ROOT.ML Thu Jun 10 11:54:14 2021 +0200
@@ -27,7 +27,6 @@
ML_file "Concurrent/counter.ML";
ML_file "ML/ml_heap.ML";
-ML_file "ML/ml_profiling.ML";
ML_file "ML/ml_print_depth0.ML";
ML_file "ML/ml_pretty.ML";
ML_file "ML/ml_compiler0.ML";
@@ -89,6 +88,7 @@
ML_file "General/sha1.ML";
ML_file "PIDE/yxml.ML";
+ML_file "ML/ml_profiling.ML";
ML_file "PIDE/byte_message.ML";
ML_file "PIDE/protocol_message.ML";
ML_file "PIDE/document_id.ML";
--- a/src/Pure/System/options.scala Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/System/options.scala Thu Jun 10 11:54:14 2021 +0200
@@ -349,7 +349,7 @@
val opt = check_name(name)
opt_value match {
case Some(value) => this + (name, value)
- case None if opt.typ == Options.Bool => this + (name, "true")
+ case None if opt.typ == Options.Bool | opt.typ == Options.String => this + (name, "true")
case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
}
}
--- a/src/Pure/Thy/sessions.scala Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Thy/sessions.scala Thu Jun 10 11:54:14 2021 +0200
@@ -510,7 +510,7 @@
def document_enabled: Boolean =
options.string("document") match {
case "" | "false" => false
- case "pdf" => true
+ case "pdf" | "true" => true
case doc => error("Bad document specification " + quote(doc))
}
--- a/src/Pure/Thy/thy_info.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Jun 10 11:54:14 2021 +0200
@@ -197,6 +197,12 @@
fun result_theory (Result {theory, ...}) = theory;
fun result_commit (Result {commit, ...}) = commit;
+datatype task =
+ Task of string list * (theory list -> result) |
+ Finished of theory;
+
+local
+
fun consolidate_theory (Exn.Exn exn) = [Exn.Exn exn]
| consolidate_theory (Exn.Res (Result {theory, exec_id, ...})) =
let
@@ -212,10 +218,7 @@
| SOME (context as {segments, ...}) =>
[Exn.capture (fn () => (apply_presentation context theory; (theory, segments))) ()]);
-
-datatype task =
- Task of string list * (theory list -> result) |
- Finished of theory;
+in
val schedule_theories = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
let
@@ -251,6 +254,8 @@
val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
in Par_Exn.release_all present_results end);
+end;
+
(* eval theory *)
--- a/src/Pure/Tools/build.ML Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Tools/build.ML Thu Jun 10 11:54:14 2021 +0200
@@ -46,6 +46,7 @@
fun build_theories qualifier (options, thys) =
let
+ val _ = ML_Profiling.check_mode (Options.string options "profiling");
val condition = space_explode "," (Options.string options "condition");
val conds = filter_out (can getenv_strict) condition;
val loaded_theories =
@@ -54,12 +55,6 @@
Isabelle_Process.init_options ();
Future.fork I;
(Thy_Info.use_theories options qualifier
- |>
- (case Options.string options "profiling" of
- "" => I
- | "time" => profile_time
- | "allocations" => profile_allocations
- | bad => error ("Bad profiling option: " ^ quote bad))
|> Unsynchronized.setmp print_mode
(space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
else
--- a/src/Pure/Tools/build.scala Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Tools/build.scala Thu Jun 10 11:54:14 2021 +0200
@@ -296,7 +296,7 @@
val log =
build_options.string("system_log") match {
case "" => No_Logger
- case "-" => Logger.make(progress)
+ case "true" => Logger.make(progress)
case log_file => Logger.make(Some(Path.explode(log_file)))
}
--- a/src/Pure/Tools/build_job.scala Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Tools/build_job.scala Thu Jun 10 11:54:14 2021 +0200
@@ -93,7 +93,6 @@
unicode_symbols: Boolean = false): Unit =
{
val store = Sessions.store(options)
-
val resources = Resources.empty
val session = new Session(options, resources)
@@ -109,9 +108,10 @@
result match {
case None => error("Missing build database for session " + quote(session_name))
case Some((used_theories, errors, rc)) =>
- val bad_theories = theories.filterNot(used_theories.toSet)
- if (bad_theories.nonEmpty) error("Unknown theories " + commas_quote(bad_theories))
-
+ theories.filterNot(used_theories.toSet) match {
+ case Nil =>
+ case bad => error("Unknown theories " + commas_quote(bad))
+ }
val print_theories =
if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
for (thy <- print_theories) {
@@ -170,7 +170,7 @@
-U output Unicode symbols
-m MARGIN margin for pretty printing (default: """ + margin + """)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -v print all messages, including information, tracing etc.
+ -v print all messages, including information etc.
Print messages from the build database of the given session, without any
checks against current sources: results from a failed build can be
--- a/src/Pure/Tools/profiling_report.scala Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/Tools/profiling_report.scala Thu Jun 10 11:54:14 2021 +0200
@@ -1,29 +1,48 @@
/* Title: Pure/Tools/profiling_report.scala
Author: Makarius
-Report Poly/ML profiling information from log files.
+Report Poly/ML profiling information from session build database.
*/
package isabelle
-import java.util.Locale
-
-
object Profiling_Report
{
- def profiling_report(log_file: Build_Log.Log_File): List[(Long, String)] =
+ def profiling_report(
+ options: Options,
+ session_name: String,
+ theories: List[String] = Nil,
+ clean_name: Boolean = false,
+ progress: Progress = new Progress): Unit =
{
- val Line = """^(?:### )?([ 0-9]{10}) (\S+|GARBAGE COLLECTION.*)$""".r
- val Count = """ *(\d+)""".r
- val clean = """-?\(\d+\).*$""".r
+ val store = Sessions.store(options)
+ val resources = Resources.empty
+ val session = new Session(options, resources)
- var results = Map.empty[String, Long]
- for (Line(Count(Value.Long(count)), raw_fun) <- log_file.lines) {
- val fun = clean.replaceAllIn(raw_fun, "")
- results += (fun -> (results.getOrElse(fun, 0L) + count))
- }
- for ((fun, count) <- results.toList.sortBy(_._2)) yield (count, fun)
+ using(store.open_database_context())(db_context =>
+ {
+ val result =
+ db_context.input_database(session_name)((db, name) => Some(store.read_theories(db, name)))
+ result match {
+ case None => error("Missing build database for session " + quote(session_name))
+ case Some(used_theories) =>
+ theories.filterNot(used_theories.toSet) match {
+ case Nil =>
+ case bad => error("Unknown theories " + commas_quote(bad))
+ }
+ val reports =
+ (for {
+ thy <- used_theories.iterator
+ if theories.isEmpty || theories.contains(thy)
+ command <- Build_Job.read_theory(db_context, resources, session_name, thy).iterator
+ snapshot = Document.State.init.snippet(command)
+ (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
+ } yield if (clean_name) report.clean_name else report).toList
+
+ for (report <- ML_Profiling.account(reports)) progress.echo(report.print)
+ }
+ })
}
@@ -33,22 +52,36 @@
Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files",
Scala_Project.here, args =>
{
+ var theories: List[String] = Nil
+ var clean_name = false
+ var options = Options.init()
+
val getopts =
Getopts("""
-Usage: isabelle profiling_report [LOGS ...]
+Usage: isabelle profiling_report [OPTIONS] SESSION
+
+ Options are:
+ -T NAME restrict to given theories (multiple options possible)
+ -c clean function names
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- Report Poly/ML profiling output from log files (potentially compressed).
-""")
- val log_names = getopts(args)
- for (name <- log_names) {
- val log_file = Build_Log.Log_File(Path.explode(name))
- val results =
- for ((count, fun) <- profiling_report(log_file))
- yield
- String.format(Locale.ROOT, "%14d %s",
- count.asInstanceOf[AnyRef], fun.asInstanceOf[AnyRef])
- if (results.nonEmpty)
- Output.writeln(cat_lines((log_file.name + ":") :: results))
- }
+ Report Poly/ML profiling from the build database of the given session
+ (without up-to-date check of sources).
+""",
+ "T:" -> (arg => theories = theories ::: List(arg)),
+ "c" -> (_ => clean_name = true),
+ "o:" -> (arg => options = options + arg))
+
+ val more_args = getopts(args)
+ val session_name =
+ more_args match {
+ case List(session_name) => session_name
+ case _ => getopts.usage()
+ }
+
+ val progress = new Console_Progress()
+
+ profiling_report(options, session_name, theories = theories,
+ clean_name = clean_name, progress = progress)
})
}
--- a/src/Pure/build-jars Thu Jun 10 11:21:57 2021 +0200
+++ b/src/Pure/build-jars Thu Jun 10 11:54:14 2021 +0200
@@ -104,6 +104,7 @@
src/Pure/ML/ml_console.scala
src/Pure/ML/ml_lex.scala
src/Pure/ML/ml_process.scala
+ src/Pure/ML/ml_profiling.scala
src/Pure/ML/ml_statistics.scala
src/Pure/ML/ml_syntax.scala
src/Pure/PIDE/byte_message.scala