--- a/NEWS Mon Jun 10 20:23:42 2024 +0200
+++ b/NEWS Mon Jun 10 23:24:33 2024 +0200
@@ -9,8 +9,31 @@
* Theory "HOL.Wellfounded":
- Renamed lemmas. Minor INCOMPATIBILITY.
+ accp_wfPD ~> accp_wfpD
+ accp_wfPI ~> accp_wfpI
+ wfPUNIVI ~> wfpUNIVI
+ wfP_SUP ~> wfp_SUP
+ wfP_accp_iff ~> wfp_accp_iff
+ wfP_acyclicP ~> wfp_acyclicP
+ wfP_def ~> wfp_def
+ wfP_empty ~> wfp_empty
+ wfP_eq_minimal ~> wfp_eq_minimal
wfP_if_convertible_to_nat ~> wfp_if_convertible_to_nat
wfP_if_convertible_to_wfP ~> wfp_if_convertible_to_wfp
+ wfP_imp_asymp ~> wfp_imp_asymp
+ wfP_imp_irreflp ~> wfp_imp_irreflp
+ wfP_induct ~> wfp_induct
+ wfP_induct_rule ~> wfp_induct_rule
+ wfP_subset ~> wfp_subset
+ wfP_trancl ~> wfp_tranclp
+ wfP_wf_eq ~> wfp_wf_eq
+ wf_acc_iff ~> wf_iff_acc
+
+* Theory "HOL-Library.Multiset":
+ - Renamed lemmas. Minor INCOMPATIBILITY.
+ wfP_less_multiset ~> wfp_less_multiset
+ wfP_multp ~> wfp_multp
+ wfP_subset_mset ~> wfp_subset_mset
New in Isabelle2024 (May 2024)
--- a/src/HOL/Fun_Def.thy Mon Jun 10 20:23:42 2024 +0200
+++ b/src/HOL/Fun_Def.thy Mon Jun 10 23:24:33 2024 +0200
@@ -68,8 +68,8 @@
definition in_rel_def[simp]: "in_rel R x y \<equiv> (x, y) \<in> R"
-lemma wf_in_rel: "wf R \<Longrightarrow> wfP (in_rel R)"
- by (simp add: wfP_def)
+lemma wf_in_rel: "wf R \<Longrightarrow> wfp (in_rel R)"
+ by (simp add: wfp_def)
ML_file \<open>Tools/Function/function_core.ML\<close>
ML_file \<open>Tools/Function/mutual.ML\<close>
--- a/src/HOL/Library/Multiset.thy Mon Jun 10 20:23:42 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Jun 10 23:24:33 2024 +0200
@@ -1548,9 +1548,9 @@
text \<open>Well-foundedness of strict subset relation\<close>
lemma wf_subset_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
- using mset_subset_size wfP_def wfp_if_convertible_to_nat by blast
-
-lemma wfP_subset_mset[simp]: "wfP (\<subset>#)"
+ using mset_subset_size wfp_def wfp_if_convertible_to_nat by blast
+
+lemma wfp_subset_mset[simp]: "wfp (\<subset>#)"
by (rule wf_subset_mset_rel[to_pred])
lemma full_multiset_induct [case_names less]:
@@ -3245,8 +3245,8 @@
lemma wf_mult: "wf r \<Longrightarrow> wf (mult r)"
unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
-lemma wfP_multp: "wfP r \<Longrightarrow> wfP (multp r)"
- unfolding multp_def wfP_def
+lemma wfp_multp: "wfp r \<Longrightarrow> wfp (multp r)"
+ unfolding multp_def wfp_def
by (simp add: wf_mult)
@@ -3694,11 +3694,11 @@
shows "M < M \<Longrightarrow> R"
by simp
-lemma wfP_less_multiset[simp]:
- assumes wfP_less: "wfP ((<) :: ('a :: preorder) \<Rightarrow> 'a \<Rightarrow> bool)"
- shows "wfP ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
+lemma wfp_less_multiset[simp]:
+ assumes wfp_less: "wfp ((<) :: ('a :: preorder) \<Rightarrow> 'a \<Rightarrow> bool)"
+ shows "wfp ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
unfolding less_multiset_def
- using wfP_multp[OF wfP_less] .
+ using wfp_multp[OF wfp_less] .
subsubsection \<open>Strict total-order properties\<close>
--- a/src/HOL/Library/Multiset_Order.thy Mon Jun 10 20:23:42 2024 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Mon Jun 10 23:24:33 2024 +0200
@@ -819,7 +819,7 @@
have "wfp ((<) :: 'a \<Rightarrow> 'a \<Rightarrow> bool)"
using wfp_on_less .
hence "wfp ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
- unfolding less_multiset_def by (rule wfP_multp)
+ unfolding less_multiset_def by (rule wfp_multp)
thus "(\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a"
unfolding wfp_on_def[of UNIV, simplified] by metis
qed
--- a/src/HOL/List.thy Mon Jun 10 20:23:42 2024 +0200
+++ b/src/HOL/List.thy Mon Jun 10 23:24:33 2024 +0200
@@ -7383,7 +7383,7 @@
qed
lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
-by (auto simp: wf_acc_iff
+by (auto simp: wf_iff_acc
intro: lists_accD lists_accI[THEN Cons_in_lists_iff[THEN iffD1, THEN conjunct1]])
subsubsection \<open>Lifting Relations to Lists: all elements\<close>
--- a/src/HOL/MicroJava/DFA/Kildall.thy Mon Jun 10 20:23:42 2024 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Mon Jun 10 23:24:33 2024 +0200
@@ -399,7 +399,7 @@
\<comment> \<open>Well-foundedness of the termination relation:\<close>
apply (rule wf_lex_prod)
apply (insert orderI [THEN acc_le_listI])
- apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric])
+ apply (simp add: acc_def lesssub_def wfp_wf_eq [symmetric])
apply (rule wf_finite_psubset)
\<comment> \<open>Loop decreases along termination relation:\<close>
--- a/src/HOL/Tools/Function/function_core.ML Mon Jun 10 20:23:42 2024 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Mon Jun 10 23:24:33 2024 +0200
@@ -715,7 +715,7 @@
(** Termination rule **)
-val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
+val wf_induct_rule = @{thm Wellfounded.wfp_induct_rule}
val wf_in_rel = @{thm Fun_Def.wf_in_rel}
val in_rel_def = @{thm Fun_Def.in_rel_def}
--- a/src/HOL/Wellfounded.thy Mon Jun 10 20:23:42 2024 +0200
+++ b/src/HOL/Wellfounded.thy Mon Jun 10 23:24:33 2024 +0200
@@ -41,10 +41,10 @@
lemma wf_def: "wf r \<longleftrightarrow> (\<forall>P. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x. P x))"
unfolding wf_on_def by simp
-lemma wfP_def: "wfP r \<longleftrightarrow> wf {(x, y). r x y}"
+lemma wfp_def: "wfp r \<longleftrightarrow> wf {(x, y). r x y}"
unfolding wf_def wfp_on_def by simp
-lemma wfP_wf_eq: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
+lemma wfp_wf_eq: "wfp (\<lambda>x y. (x, y) \<in> r) = wf r"
using wfp_on_wf_on_eq .
@@ -66,11 +66,11 @@
shows "P a"
using assms by (auto intro: wf_on_induct[of UNIV])
-lemmas wfP_induct = wf_induct [to_pred]
+lemmas wfp_induct = wf_induct [to_pred]
lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
-lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]
+lemmas wfp_induct_rule = wf_induct_rule [to_pred, induct set: wfp]
lemma wf_on_iff_wf: "wf_on A r \<longleftrightarrow> wf {(x, y) \<in> r. x \<in> A \<and> y \<in> A}"
proof (rule iffI)
@@ -129,7 +129,7 @@
lemma wfUNIVI: "(\<And>P x. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<Longrightarrow> P x) \<Longrightarrow> wf r"
unfolding wf_def by blast
-lemmas wfPUNIVI = wfUNIVI [to_pred]
+lemmas wfpUNIVI = wfUNIVI [to_pred]
text \<open>Restriction to domain \<open>A\<close> and range \<open>B\<close>.
If \<open>r\<close> is well-founded over their intersection, then \<open>wf r\<close>.\<close>
@@ -153,7 +153,7 @@
lemma wf_imp_asym: "wf r \<Longrightarrow> asym r"
by (auto intro: asymI elim: wf_asym)
-lemma wfP_imp_asymp: "wfP r \<Longrightarrow> asymp r"
+lemma wfp_imp_asymp: "wfp r \<Longrightarrow> asymp r"
by (rule wf_imp_asym[to_pred])
lemma wf_not_refl [simp]: "wf r \<Longrightarrow> (a, a) \<notin> r"
@@ -168,7 +168,7 @@
assumes "wf r" shows "irrefl r"
using wf_irrefl [OF assms] by (auto simp add: irrefl_def)
-lemma wfP_imp_irreflp: "wfP r \<Longrightarrow> irreflp r"
+lemma wfp_imp_irreflp: "wfp r \<Longrightarrow> irreflp r"
by (rule wf_imp_irrefl[to_pred])
lemma wf_wellorderI:
@@ -182,8 +182,8 @@
lemma (in wellorder) wf: "wf {(x, y). x < y}"
unfolding wf_def by (blast intro: less_induct)
-lemma (in wellorder) wfP_less[simp]: "wfP (<)"
- by (simp add: wf wfP_def)
+lemma (in wellorder) wfP_less[simp]: "wfp (<)"
+ by (simp add: wf wfp_def)
lemma (in wellorder) wfp_on_less[simp]: "wfp_on A (<)"
unfolding wfp_on_def
@@ -307,7 +307,7 @@
lemma wf_eq_minimal: "wf r \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q))"
unfolding wf_iff_ex_minimal by blast
-lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
+lemmas wfp_eq_minimal = wf_eq_minimal [to_pred]
subsubsection \<open>Antimonotonicity\<close>
@@ -376,7 +376,7 @@
then show ?thesis unfolding wf_def by blast
qed
-lemmas wfP_trancl = wf_trancl [to_pred]
+lemmas wfp_tranclp = wf_trancl [to_pred]
lemma wf_converse_trancl: "wf (r\<inverse>) \<Longrightarrow> wf ((r\<^sup>+)\<inverse>)"
apply (subst trancl_converse [symmetric])
@@ -388,16 +388,16 @@
lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p"
by (simp add: wf_eq_minimal) fast
-lemmas wfP_subset = wf_subset [to_pred]
+lemmas wfp_subset = wf_subset [to_pred]
text \<open>Well-foundedness of the empty relation\<close>
lemma wf_empty [iff]: "wf {}"
by (simp add: wf_def)
-lemma wfP_empty [iff]: "wfP (\<lambda>x y. False)"
+lemma wfp_empty [iff]: "wfp (\<lambda>x y. False)"
proof -
- have "wfP bot"
+ have "wfp bot"
by (fact wf_empty[to_pred bot_empty_eq2])
then show ?thesis
by (simp add: bot_fun_def)
@@ -602,9 +602,9 @@
qed
qed
-lemma wfP_SUP:
- "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow>
- wfP (\<Squnion>(range r))"
+lemma wfp_SUP:
+ "\<forall>i. wfp (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow>
+ wfp (\<Squnion>(range r))"
by (rule wf_UN[to_pred]) simp_all
lemma wf_Union:
@@ -757,7 +757,7 @@
lemma wf_acyclic: "wf r \<Longrightarrow> acyclic r"
by (simp add: acyclic_def) (blast elim: wf_trancl [THEN wf_irrefl])
-lemmas wfP_acyclicP = wf_acyclic [to_pred]
+lemmas wfp_acyclicP = wf_acyclic [to_pred]
subsubsection \<open>Wellfoundedness of finite acyclic relations\<close>
@@ -921,22 +921,22 @@
theorem accp_downwards: "accp r a \<Longrightarrow> r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r b"
by (blast dest: accp_downwards_aux)
-theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r"
-proof (rule wfPUNIVI)
+theorem accp_wfpI: "\<forall>x. accp r x \<Longrightarrow> wfp r"
+proof (rule wfpUNIVI)
fix P x
assume "\<forall>x. accp r x" "\<forall>x. (\<forall>y. r y x \<longrightarrow> P y) \<longrightarrow> P x"
then show "P x"
using accp_induct[where P = P] by blast
qed
-theorem accp_wfPD: "wfP r \<Longrightarrow> accp r x"
- apply (erule wfP_induct_rule)
+theorem accp_wfpD: "wfp r \<Longrightarrow> accp r x"
+ apply (erule wfp_induct_rule)
apply (rule accp.accI)
apply blast
done
-theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)"
- by (blast intro: accp_wfPI dest: accp_wfPD)
+theorem wfp_iff_accp: "wfp r = (\<forall>x. accp r x)"
+ by (blast intro: accp_wfpI dest: accp_wfpD)
text \<open>Smaller relations have bigger accessible parts:\<close>
@@ -986,9 +986,9 @@
lemmas not_acc_down = not_accp_down [to_set]
lemmas acc_downwards_aux = accp_downwards_aux [to_set]
lemmas acc_downwards = accp_downwards [to_set]
-lemmas acc_wfI = accp_wfPI [to_set]
-lemmas acc_wfD = accp_wfPD [to_set]
-lemmas wf_acc_iff = wfP_accp_iff [to_set]
+lemmas acc_wfI = accp_wfpI [to_set]
+lemmas acc_wfD = accp_wfpD [to_set]
+lemmas wf_iff_acc = wfp_iff_accp [to_set]
lemmas acc_subset = accp_subset [to_set]
lemmas acc_subset_induct = accp_subset_induct [to_set]
@@ -1065,7 +1065,7 @@
using convertible .
qed
-lemma wfp_if_convertible_to_wfp: "wfP S \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> S (f x) (f y)) \<Longrightarrow> wfP R"
+lemma wfp_if_convertible_to_wfp: "wfp S \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> S (f x) (f y)) \<Longrightarrow> wfp R"
using wf_if_convertible_to_wf[to_pred, of S R f] by simp
text \<open>Converting to @{typ nat} is a very common special case that might be found more easily by
@@ -1073,7 +1073,7 @@
lemma wfp_if_convertible_to_nat:
fixes f :: "_ \<Rightarrow> nat"
- shows "(\<And>x y. R x y \<Longrightarrow> f x < f y) \<Longrightarrow> wfP R"
+ shows "(\<And>x y. R x y \<Longrightarrow> f x < f y) \<Longrightarrow> wfp R"
by (rule wfp_if_convertible_to_wfp[of "(<) :: nat \<Rightarrow> nat \<Rightarrow> bool", simplified])
--- a/src/Pure/Build/build_manager.scala Mon Jun 10 20:23:42 2024 +0200
+++ b/src/Pure/Build/build_manager.scala Mon Jun 10 23:24:33 2024 +0200
@@ -32,19 +32,21 @@
def name: String
def components: List[Component]
def fresh_build: Boolean
+ def build_cluster: Boolean
def command(build_hosts: List[Build_Cluster.Host]): String
}
object CI_Build {
def apply(job: isabelle.CI_Build.Job): CI_Build =
- CI_Build(job.name, job.components.map(Component(_, "default")))
+ CI_Build(job.name, job.hosts.build_cluster, job.components.map(Component(_, "default")))
}
- case class CI_Build(name: String, components: List[Component]) extends Build_Config {
+ case class CI_Build(name: String, build_cluster: Boolean, components: List[Component])
+ extends Build_Config {
def fresh_build: Boolean = true
def command(build_hosts: List[Build_Cluster.Host]): String =
" ci_build" +
- build_hosts.map(host => " -H " + Bash.string(host.print)).mkString +
+ if_proper(build_cluster, build_hosts.map(host => " -H " + Bash.string(host.print)).mkString) +
" " + name
}
@@ -71,6 +73,7 @@
) extends Build_Config {
def name: String = User_Build.name
def components: List[Component] = afp_rev.map(Component.AFP).toList
+ def build_cluster: Boolean = true
def command(build_hosts: List[Build_Cluster.Host]): String = {
" build" +
if_proper(afp_rev, " -A:") +
@@ -95,7 +98,6 @@
sealed case class Task(
build_config: Build_Config,
- build_cluster: Boolean,
hosts_spec: String,
id: UUID.T = UUID.random(),
submit_date: Date = Date.now(),
@@ -106,6 +108,7 @@
def kind: String = build_config.name
def components: List[Component] = build_config.components
+ def build_cluster = build_config.build_cluster
def build_hosts: List[Build_Cluster.Host] =
Build_Cluster.Host.parse(Registry.global, hosts_spec)
}
@@ -319,7 +322,7 @@
val components = space_explode(',', res.string(Pending.components)).map(Component.parse)
val build_config =
- if (kind != User_Build.name) CI_Build(kind, components)
+ if (kind != User_Build.name) CI_Build(kind, build_cluster, components)
else {
val prefs = Options.Spec.parse(res.string(Pending.prefs))
val requirements = res.bool(Pending.requirements)
@@ -343,8 +346,8 @@
clean_build, export_files, fresh_build, presentation, verbose)
}
- val task = Task(build_config, build_cluster, hosts_spec, UUID.make(id), submit_date,
- priority, isabelle_rev)
+ val task =
+ Task(build_config, hosts_spec, UUID.make(id), submit_date, priority, isabelle_rev)
task.name -> task
})
@@ -805,8 +808,8 @@
if isabelle_updated || ci_job.components.exists(updated_components.contains)
if !_state.pending.values.exists(_.kind == ci_job.name)
} {
- val task = Task(CI_Build(ci_job), ci_job.hosts.build_cluster, ci_job.hosts.hosts_spec,
- priority = Priority.low, isabelle_rev = "default")
+ val task = Task(CI_Build(ci_job), ci_job.hosts.hosts_spec, priority = Priority.low,
+ isabelle_rev = "default")
_state = _state.add_pending(task)
}
}
@@ -841,8 +844,7 @@
for (ci_job <-ci_jobs)
ci_job.trigger match {
case isabelle.CI_Build.Timed(in_interval) if in_interval(previous, next) =>
- val task = Task(CI_Build(ci_job), ci_job.hosts.build_cluster, ci_job.hosts.hosts_spec,
- isabelle_rev = "default")
+ val task = Task(CI_Build(ci_job), ci_job.hosts.hosts_spec, isabelle_rev = "default")
_state = _state.add_pending(task)
case _ =>
}
@@ -1095,8 +1097,11 @@
Get(Page.OVERVIEW, "overview", get_overview),
Get(Page.BUILD, "build", get_build),
Post(API.BUILD_CANCEL, "cancel build", cancel_build))
+ val logo = Bytes.read(Path.explode("$ISABELLE_HOME/lib/logo/isabelle_transparent-48.gif"))
val head =
List(
+ HTML.title("Isabelle Build Manager"),
+ Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64),
HTML.style_file("https://hawkz.github.io/gdcss/gd.css"),
HTML.style("html { background-color: white; }"))
}
@@ -1309,7 +1314,7 @@
val build_config = User_Build(afp_rev, prefs, requirements, all_sessions,
base_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions, build_heap,
clean_build, export_files, fresh_build, presentation, verbose)
- val task = Task(build_config, true, hosts_spec, id, Date.now(), Priority.high)
+ val task = Task(build_config, hosts_spec, id, Date.now(), Priority.high)
val dir = store.task_dir(task)
--- a/src/Pure/System/web_app.scala Mon Jun 10 20:23:42 2024 +0200
+++ b/src/Pure/System/web_app.scala Mon Jun 10 23:24:33 2024 +0200
@@ -28,6 +28,9 @@
val fieldset = new Operator("fieldset")
val button = new Operator("button")
+ def icon(href: String): XML.Elem =
+ XML.Elem(Markup("link", List("rel" -> "icon", "type" -> "image/x-icon", "href" -> href)), Nil)
+
def legend(txt: String): XML.Elem = XML.Elem(Markup("legend", Nil), text(txt))
def input(typ: String): XML.Elem = XML.Elem(Markup("input", List("type" -> typ)), Nil)
def hidden(k: Params.Key, v: String): XML.Elem =