--- a/CONTRIBUTORS Sat Dec 04 12:38:32 2021 +0100
+++ b/CONTRIBUTORS Sat Dec 04 12:38:51 2021 +0100
@@ -3,6 +3,10 @@
listed as an author in one of the source files of this Isabelle distribution.
+Contributions to this Isabelle version
+--------------------------------------
+
+
Contributions to Isabelle2021-1
-------------------------------
--- a/NEWS Sat Dec 04 12:38:32 2021 +0100
+++ b/NEWS Sat Dec 04 12:38:51 2021 +0100
@@ -4,6 +4,31 @@
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
+New in this Isabelle version
+----------------------------
+
+*** HOL ***
+
+* Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to
+ type class preorder.
+
+* Theory "HOL-Library.Multiset":
+ - Consolidated operation and fact names.
+ multp ~> multp_code
+ multeqp ~> multeqp_code
+ multp_cancel_add_mset ~> multp_cancel_add_mset0
+ multp_cancel_add_mset0[simplified] ~> multp_cancel_add_mset
+ multp_code_iff ~> multp_code_iff_mult
+ multeqp_code_iff ~> multeqp_code_iff_reflcl_mult
+ Minor INCOMPATIBILITY.
+ - Moved mult1_lessE out of preorder type class and add explicit
+ assumption. Minor INCOMPATIBILITY.
+ - Added predicate multp equivalent to set mult. Reuse name previously
+ used for what is now called multp_code. Minor INCOMPATIBILITY.
+ - Lifted multiple lemmas from mult to multp.
+ - Redefined less_multiset to be based on multp. INCOMPATIBILITY.
+
+
New in Isabelle2021-1 (December 2021)
-------------------------------------
--- a/src/HOL/Library/Multiset.thy Sat Dec 04 12:38:32 2021 +0100
+++ b/src/HOL/Library/Multiset.thy Sat Dec 04 12:38:51 2021 +0100
@@ -4,12 +4,13 @@
Author: Jasmin Blanchette, Inria, LORIA, MPII
Author: Dmitriy Traytel, TU Muenchen
Author: Mathias Fleury, MPII
+ Author: Martin Desharnais, MPI-INF Saarbruecken
*)
section \<open>(Finite) Multisets\<close>
theory Multiset
-imports Cancellation
+ imports Cancellation
begin
subsection \<open>The type of multisets\<close>
@@ -2788,8 +2789,6 @@
subsection \<open>The multiset order\<close>
-subsubsection \<open>Well-foundedness\<close>
-
definition mult1 :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
"mult1 r = {(N, M). \<exists>a M0 K. M = add_mset a M0 \<and> N = M0 + K \<and>
(\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r)}"
@@ -2797,6 +2796,9 @@
definition mult :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
"mult r = (mult1 r)\<^sup>+"
+definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ "multp r M N \<longleftrightarrow> (M, N) \<in> mult {(x, y). r x y}"
+
lemma mult1I:
assumes "M = add_mset a M0" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
shows "(N, M) \<in> mult1 r"
@@ -2809,14 +2811,29 @@
lemma mono_mult1:
assumes "r \<subseteq> r'" shows "mult1 r \<subseteq> mult1 r'"
-unfolding mult1_def using assms by blast
+ unfolding mult1_def using assms by blast
lemma mono_mult:
assumes "r \<subseteq> r'" shows "mult r \<subseteq> mult r'"
-unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+ unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+
+lemma mono_multp[mono]: "r \<le> r' \<Longrightarrow> multp r \<le> multp r'"
+ unfolding le_fun_def le_bool_def
+proof (intro allI impI)
+ fix M N :: "'a multiset"
+ assume "\<forall>x xa. r x xa \<longrightarrow> r' x xa"
+ hence "{(x, y). r x y} \<subseteq> {(x, y). r' x y}"
+ by blast
+ thus "multp r M N \<Longrightarrow> multp r' M N"
+ unfolding multp_def
+ by (fact mono_mult[THEN subsetD, rotated])
+qed
lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
-by (simp add: mult1_def)
+ by (simp add: mult1_def)
+
+
+subsubsection \<open>Well-foundedness\<close>
lemma less_add:
assumes mult1: "(N, add_mset a M0) \<in> mult1 r"
@@ -2918,11 +2935,15 @@
qed
qed
-theorem wf_mult1: "wf r \<Longrightarrow> wf (mult1 r)"
-by (rule acc_wfI) (rule all_accessible)
-
-theorem wf_mult: "wf r \<Longrightarrow> wf (mult r)"
-unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
+lemma wf_mult1: "wf r \<Longrightarrow> wf (mult1 r)"
+ by (rule acc_wfI) (rule all_accessible)
+
+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
+ by (simp add: wf_mult)
subsubsection \<open>Closure-free presentation\<close>
@@ -2965,6 +2986,9 @@
qed
qed
+lemmas multp_implies_one_step =
+ mult_implies_one_step[of "{(x, y). r x y}" for r, folded multp_def transp_trans, simplified]
+
lemma one_step_implies_mult:
assumes
"J \<noteq> {#}" and
@@ -2997,6 +3021,9 @@
qed
qed
+lemmas one_step_implies_multp =
+ one_step_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def, simplified]
+
lemma subset_implies_mult:
assumes sub: "A \<subset># B"
shows "(A, B) \<in> mult r"
@@ -3009,8 +3036,10 @@
by (rule one_step_implies_mult[of "B - A" "{#}" _ A, unfolded ApBmA, simplified])
qed
-
-subsection \<open>The multiset extension is cancellative for multiset union\<close>
+lemmas subset_implies_multp = subset_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def]
+
+
+subsubsection \<open>The multiset extension is cancellative for multiset union\<close>
lemma mult_cancel:
assumes "trans s" and "irrefl s"
@@ -3045,10 +3074,18 @@
thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
qed
+lemmas multp_cancel =
+ mult_cancel[of "{(x, y). r x y}" for r,
+ folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
lemmas mult_cancel_add_mset =
mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral]
-lemma mult_cancel_max:
+lemmas multp_cancel_add_mset =
+ mult_cancel_add_mset[of "{(x, y). r x y}" for r,
+ folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
+lemma mult_cancel_max0:
assumes "trans s" and "irrefl s"
shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
proof -
@@ -3056,6 +3093,112 @@
thus ?thesis using mult_cancel[OF assms, of "X - X \<inter># Y" "X \<inter># Y" "Y - X \<inter># Y"] by auto
qed
+lemmas mult_cancel_max = mult_cancel_max0[simplified]
+
+lemmas multp_cancel_max =
+ mult_cancel_max[of "{(x, y). r x y}" for r,
+ folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
+
+subsubsection \<open>Partial-order properties\<close>
+
+lemma mult1_lessE:
+ assumes "(N, M) \<in> mult1 {(a, b). r a b}" and "asymp r"
+ obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
+ "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a"
+proof -
+ from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
+ *: "b \<in># K \<Longrightarrow> r b a" for b by (blast elim: mult1E)
+ moreover from * [of a] have "a \<notin># K"
+ using \<open>asymp r\<close> by (meson asymp.cases)
+ ultimately show thesis by (auto intro: that)
+qed
+
+lemma trans_mult: "trans r \<Longrightarrow> trans (mult r)"
+ by (simp add: mult_def)
+
+lemma transp_multp: "transp r \<Longrightarrow> transp (multp r)"
+ unfolding multp_def transp_trans_eq
+ by (fact trans_mult[of "{(x, y). r x y}" for r, folded transp_trans])
+
+lemma irrefl_mult:
+ assumes "trans r" "irrefl r"
+ shows "irrefl (mult r)"
+proof (intro irreflI notI)
+ fix M
+ assume "(M, M) \<in> mult r"
+ then obtain I J K where "M = I + J" and "M = I + K"
+ and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> r)"
+ using mult_implies_one_step[OF \<open>trans r\<close>] by blast
+ then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. (k, j) \<in> r" by auto
+ have "finite (set_mset K)" by simp
+ hence "set_mset K = {}"
+ using **
+ proof (induction rule: finite_induct)
+ case empty
+ thus ?case by simp
+ next
+ case (insert x F)
+ have False
+ using \<open>irrefl r\<close>[unfolded irrefl_def, rule_format]
+ using \<open>trans r\<close>[THEN transD]
+ by (metis equals0D insert.IH insert.prems insertE insertI1 insertI2)
+ thus ?case ..
+ qed
+ with * show False by simp
+qed
+
+lemmas irreflp_multp =
+ irrefl_mult[of "{(x, y). r x y}" for r,
+ folded transp_trans_eq irreflp_irrefl_eq, simplified, folded multp_def]
+
+instantiation multiset :: (preorder) order begin
+
+definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+ where "M < N \<longleftrightarrow> multp (<) M N"
+
+definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+ where "less_eq_multiset M N \<longleftrightarrow> M < N \<or> M = N"
+
+instance
+proof intro_classes
+ fix M N :: "'a multiset"
+ show "(M < N) = (M \<le> N \<and> \<not> N \<le> M)"
+ unfolding less_eq_multiset_def less_multiset_def
+ by (metis irreflp_def irreflp_less irreflp_multp transpE transp_less transp_multp)
+next
+ fix M :: "'a multiset"
+ show "M \<le> M"
+ unfolding less_eq_multiset_def
+ by simp
+next
+ fix M1 M2 M3 :: "'a multiset"
+ show "M1 \<le> M2 \<Longrightarrow> M2 \<le> M3 \<Longrightarrow> M1 \<le> M3"
+ unfolding less_eq_multiset_def less_multiset_def
+ using transp_multp[OF transp_less, THEN transpD]
+ by blast
+next
+ fix M N :: "'a multiset"
+ show "M \<le> N \<Longrightarrow> N \<le> M \<Longrightarrow> M = N"
+ unfolding less_eq_multiset_def less_multiset_def
+ using transp_multp[OF transp_less, THEN transpD]
+ using irreflp_multp[OF transp_less irreflp_less, unfolded irreflp_def, rule_format]
+ by blast
+qed
+
+end
+
+lemma mset_le_irrefl [elim!]:
+ fixes M :: "'a::preorder multiset"
+ 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)"
+ using wfP_multp[OF wfP_less] less_multiset_def
+ by (metis wfPUNIVI wfP_induct)
+
subsection \<open>Quasi-executable version of the multiset extension\<close>
@@ -3063,22 +3206,22 @@
Predicate variants of \<open>mult\<close> and the reflexive closure of \<open>mult\<close>, which are
executable whenever the given predicate \<open>P\<close> is. Together with the standard
code equations for \<open>(\<inter>#\<close>) and \<open>(-\<close>) this should yield quadratic
- (with respect to calls to \<open>P\<close>) implementations of \<open>multp\<close> and \<open>multeqp\<close>.
+ (with respect to calls to \<open>P\<close>) implementations of \<open>multp_code\<close> and \<open>multeqp_code\<close>.
\<close>
-definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
- "multp P N M =
+definition multp_code :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ "multp_code P N M =
(let Z = M \<inter># N; X = M - Z in
X \<noteq> {#} \<and> (let Y = N - Z in (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x)))"
-definition multeqp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
- "multeqp P N M =
+definition multeqp_code :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ "multeqp_code P N M =
(let Z = M \<inter># N; X = M - Z; Y = N - Z in
(\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x))"
-lemma multp_iff:
+lemma multp_code_iff_mult:
assumes "irrefl R" and "trans R" and [simp]: "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
- shows "multp P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
+ shows "multp_code P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
proof -
have *: "M \<inter># N + (N - M \<inter># N) = N" "M \<inter># N + (M - M \<inter># N) = M"
"(M - M \<inter># N) \<inter># (N - M \<inter># N) = {#}" by (auto simp flip: count_inject)
@@ -3086,87 +3229,40 @@
proof
assume ?L thus ?R
using one_step_implies_mult[of "M - M \<inter># N" "N - M \<inter># N" R "M \<inter># N"] *
- by (auto simp: multp_def Let_def)
+ by (auto simp: multp_code_def Let_def)
next
{ fix I J K :: "'a multiset" assume "(I + J) \<inter># (I + K) = {#}"
then have "I = {#}" by (metis inter_union_distrib_right union_eq_empty)
} note [dest!] = this
assume ?R thus ?L
using mult_implies_one_step[OF assms(2), of "N - M \<inter># N" "M - M \<inter># N"]
- mult_cancel_max[OF assms(2,1), of "N" "M"] * by (auto simp: multp_def)
+ mult_cancel_max[OF assms(2,1), of "N" "M"] * by (auto simp: multp_code_def)
qed
qed
-lemma multeqp_iff:
+lemma multp_code_eq_multp: "irreflp r \<Longrightarrow> transp r \<Longrightarrow> multp_code r = multp r"
+ using multp_code_iff_mult[of "{(x, y). r x y}" r for r,
+ folded irreflp_irrefl_eq transp_trans multp_def, simplified]
+ by blast
+
+lemma multeqp_code_iff_reflcl_mult:
assumes "irrefl R" and "trans R" and "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
- shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
+ shows "multeqp_code P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
proof -
{ assume "N \<noteq> M" "M - M \<inter># N = {#}"
then obtain y where "count N y \<noteq> count M y" by (auto simp flip: count_inject)
then have "\<exists>y. count M y < count N y" using \<open>M - M \<inter># N = {#}\<close>
by (auto simp flip: count_inject dest!: le_neq_implies_less fun_cong[of _ _ y])
}
- then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M"
- by (auto simp: multeqp_def multp_def Let_def in_diff_count)
- thus ?thesis using multp_iff[OF assms] by simp
-qed
-
-
-subsubsection \<open>Partial-order properties\<close>
-
-lemma (in preorder) mult1_lessE:
- assumes "(N, M) \<in> mult1 {(a, b). a < b}"
- obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
- "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
-proof -
- from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
- *: "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
- moreover from * [of a] have "a \<notin># K" by auto
- ultimately show thesis by (auto intro: that)
+ then have "multeqp_code P N M \<longleftrightarrow> multp_code P N M \<or> N = M"
+ by (auto simp: multeqp_code_def multp_code_def Let_def in_diff_count)
+ thus ?thesis using multp_code_iff_mult[OF assms] by simp
qed
-instantiation multiset :: (preorder) order
-begin
-
-definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
- where "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
- where "less_eq_multiset M' M \<longleftrightarrow> M' < M \<or> M' = M"
-
-instance
-proof -
- have irrefl: "\<not> M < M" for M :: "'a multiset"
- proof
- assume "M < M"
- then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def)
- have "trans {(x'::'a, x). x' < x}"
- by (metis (mono_tags, lifting) case_prodD case_prodI less_trans mem_Collect_eq transI)
- moreover note MM
- ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
- \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
- by (rule mult_implies_one_step)
- then obtain I J K where "M = I + J" and "M = I + K"
- and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
- then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
- have "finite (set_mset K)" by simp
- moreover note **
- ultimately have "set_mset K = {}"
- by (induct rule: finite_induct) (auto intro: order_less_trans)
- with * show False by simp
- qed
- have trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < N" for K M N :: "'a multiset"
- unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
- show "OFCLASS('a multiset, order_class)"
- by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
-qed
-
-end
-
-lemma mset_le_irrefl [elim!]:
- fixes M :: "'a::preorder multiset"
- shows "M < M \<Longrightarrow> R"
- by simp
+lemma multeqp_code_eq_reflclp_multp: "irreflp r \<Longrightarrow> transp r \<Longrightarrow> multeqp_code r = (multp r)\<^sup>=\<^sup>="
+ using multeqp_code_iff_reflcl_mult[of "{(x, y). r x y}" r for r,
+ folded irreflp_irrefl_eq transp_trans, simplified, folded multp_def]
+ by blast
subsubsection \<open>Monotonicity of multiset union\<close>
@@ -3175,7 +3271,7 @@
by (force simp: mult1_def)
lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::preorder multiset)"
-apply (unfold less_multiset_def mult_def)
+apply (unfold less_multiset_def multp_def mult_def)
apply (erule trancl_induct)
apply (blast intro: mult1_union)
apply (blast intro: mult1_union trancl_trans)
--- a/src/HOL/Library/Multiset_Order.thy Sat Dec 04 12:38:32 2021 +0100
+++ b/src/HOL/Library/Multiset_Order.thy Sat Dec 04 12:38:51 2021 +0100
@@ -11,6 +11,135 @@
subsection \<open>Alternative Characterizations\<close>
+subsubsection \<open>The Dershowitz--Manna Ordering\<close>
+
+definition multp\<^sub>D\<^sub>M where
+ "multp\<^sub>D\<^sub>M r M N \<longleftrightarrow>
+ (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)))"
+
+lemma multp\<^sub>D\<^sub>M_imp_multp:
+ "multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N"
+proof -
+ assume "multp\<^sub>D\<^sub>M r M N"
+ then obtain X Y where
+ "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)"
+ unfolding multp\<^sub>D\<^sub>M_def by blast
+ then have "multp r (N - X + Y) (N - X + X)"
+ by (intro one_step_implies_multp) (auto simp: Bex_def trans_def)
+ with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "multp r M N"
+ by (metis subset_mset.diff_add)
+qed
+
+subsubsection \<open>The Huet--Oppen Ordering\<close>
+
+definition multp\<^sub>H\<^sub>O where
+ "multp\<^sub>H\<^sub>O r M N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. r y x \<and> count M x < count N x))"
+
+lemma multp_imp_multp\<^sub>H\<^sub>O:
+ assumes "asymp r" and "transp r"
+ shows "multp r M N \<Longrightarrow> multp\<^sub>H\<^sub>O r M N"
+ unfolding multp_def mult_def
+proof (induction rule: trancl_induct)
+ case (base P)
+ then show ?case
+ using \<open>asymp r\<close>
+ by (auto elim!: mult1_lessE simp: count_eq_zero_iff multp\<^sub>H\<^sub>O_def split: if_splits
+ dest!: Suc_lessD)
+next
+ case (step N P)
+ from step(3) have "M \<noteq> N" and
+ **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x. r y x \<and> count M x < count N x)"
+ by (simp_all add: multp\<^sub>H\<^sub>O_def)
+ from step(2) obtain M0 a K where
+ *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a"
+ using \<open>asymp r\<close> by (auto elim: mult1_lessE)
+ from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P"
+ using *(4) \<open>asymp r\<close>
+ by (metis asymp.cases add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI
+ count_union diff_diff_add_mset diff_single_trivial in_diff_count multi_member_last)
+ moreover
+ { assume "count P a \<le> count M a"
+ with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
+ by (auto simp add: not_in_iff)
+ with ** obtain z where z: "r a z" "count M z < count N z"
+ by blast
+ with * have "count N z \<le> count P z"
+ using \<open>asymp r\<close>
+ by (metis add_diff_cancel_left' add_mset_add_single asymp.cases diff_diff_add_mset
+ diff_single_trivial in_diff_count not_le_imp_less)
+ with z have "\<exists>z. r a z \<and> count M z < count P z" by auto
+ } note count_a = this
+ { fix y
+ assume count_y: "count P y < count M y"
+ have "\<exists>x. r y x \<and> count M x < count P x"
+ proof (cases "y = a")
+ case True
+ with count_y count_a show ?thesis by auto
+ next
+ case False
+ show ?thesis
+ proof (cases "y \<in># K")
+ case True
+ with *(4) have "r y a" by simp
+ then show ?thesis
+ by (cases "count P a \<le> count M a") (auto dest: count_a intro: \<open>transp r\<close>[THEN transpD])
+ next
+ case False
+ with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
+ by (simp add: not_in_iff)
+ with count_y ** obtain z where z: "r y z" "count M z < count N z" by auto
+ show ?thesis
+ proof (cases "z \<in># K")
+ case True
+ with *(4) have "r z a" by simp
+ with z(1) show ?thesis
+ by (cases "count P a \<le> count M a") (auto dest!: count_a intro: \<open>transp r\<close>[THEN transpD])
+ next
+ case False
+ with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
+ by (auto simp add: not_in_iff)
+ with z show ?thesis by auto
+ qed
+ qed
+ qed
+ }
+ ultimately show ?case unfolding multp\<^sub>H\<^sub>O_def by blast
+qed
+
+lemma multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M: "multp\<^sub>H\<^sub>O r M N \<Longrightarrow> multp\<^sub>D\<^sub>M r M N"
+unfolding multp\<^sub>D\<^sub>M_def
+proof (intro iffI exI conjI)
+ assume "multp\<^sub>H\<^sub>O r M N"
+ then obtain z where z: "count M z < count N z"
+ unfolding multp\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
+ define X where "X = N - M"
+ define Y where "Y = M - N"
+ from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
+ from z show "X \<subseteq># N" unfolding X_def by auto
+ show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
+ show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)"
+ proof (intro allI impI)
+ fix k
+ assume "k \<in># Y"
+ then have "count N k < count M k" unfolding Y_def
+ by (auto simp add: in_diff_count)
+ with \<open>multp\<^sub>H\<^sub>O r M N\<close> obtain a where "r k a" and "count M a < count N a"
+ unfolding multp\<^sub>H\<^sub>O_def by blast
+ then show "\<exists>a. a \<in># X \<and> r k a" unfolding X_def
+ by (auto simp add: in_diff_count)
+ qed
+qed
+
+lemma multp_eq_multp\<^sub>D\<^sub>M: "asymp r \<Longrightarrow> transp r \<Longrightarrow> multp r = multp\<^sub>D\<^sub>M r"
+ using multp\<^sub>D\<^sub>M_imp_multp multp_imp_multp\<^sub>H\<^sub>O[THEN multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M]
+ by blast
+
+lemma multp_eq_multp\<^sub>H\<^sub>O: "asymp r \<Longrightarrow> transp r \<Longrightarrow> multp r = multp\<^sub>H\<^sub>O r"
+ using multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M[THEN multp\<^sub>D\<^sub>M_imp_multp] multp_imp_multp\<^sub>H\<^sub>O
+ by blast
+
+subsubsection \<open>Properties of Preorders\<close>
+
context preorder
begin
@@ -59,107 +188,29 @@
lemma mult_imp_less_multiset\<^sub>H\<^sub>O:
"(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
-proof (unfold mult_def, induct rule: trancl_induct)
- case (base P)
- then show ?case
- by (auto elim!: mult1_lessE simp add: count_eq_zero_iff less_multiset\<^sub>H\<^sub>O_def split: if_splits dest!: Suc_lessD)
-next
- case (step N P)
- from step(3) have "M \<noteq> N" and
- **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)"
- by (simp_all add: less_multiset\<^sub>H\<^sub>O_def)
- from step(2) obtain M0 a K where
- *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
- by (blast elim: mult1_lessE)
- from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits )
- moreover
- { assume "count P a \<le> count M a"
- with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
- by (auto simp add: not_in_iff)
- with ** obtain z where z: "z > a" "count M z < count N z"
- by blast
- with * have "count N z \<le> count P z"
- by (auto elim: less_asym intro: count_inI)
- with z have "\<exists>z > a. count M z < count P z" by auto
- } note count_a = this
- { fix y
- assume count_y: "count P y < count M y"
- have "\<exists>x>y. count M x < count P x"
- proof (cases "y = a")
- case True
- with count_y count_a show ?thesis by auto
- next
- case False
- show ?thesis
- proof (cases "y \<in># K")
- case True
- with *(4) have "y < a" by simp
- then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans)
- next
- case False
- with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
- by (simp add: not_in_iff)
- with count_y ** obtain z where z: "z > y" "count M z < count N z" by auto
- show ?thesis
- proof (cases "z \<in># K")
- case True
- with *(4) have "z < a" by simp
- with z(1) show ?thesis
- by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans)
- next
- case False
- with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
- by (auto simp add: not_in_iff)
- with z show ?thesis by auto
- qed
- qed
- qed
- }
- ultimately show ?case unfolding less_multiset\<^sub>H\<^sub>O_def by blast
-qed
+ unfolding multp_def[of "(<)", symmetric]
+ using multp_imp_multp\<^sub>H\<^sub>O[of "(<)"]
+ by (simp add: less_multiset\<^sub>H\<^sub>O_def multp\<^sub>H\<^sub>O_def)
lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
"less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}"
-proof -
- assume "less_multiset\<^sub>D\<^sub>M M N"
- then obtain X Y where
- "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
- unfolding less_multiset\<^sub>D\<^sub>M_def by blast
- then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
- by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
- with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
- by (metis subset_mset.diff_add)
-qed
+ unfolding multp_def[of "(<)", symmetric]
+ by (rule multp\<^sub>D\<^sub>M_imp_multp[of "(<)" M N]) (simp add: less_multiset\<^sub>D\<^sub>M_def multp\<^sub>D\<^sub>M_def)
lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \<Longrightarrow> less_multiset\<^sub>D\<^sub>M M N"
-unfolding less_multiset\<^sub>D\<^sub>M_def
-proof (intro iffI exI conjI)
- assume "less_multiset\<^sub>H\<^sub>O M N"
- then obtain z where z: "count M z < count N z"
- unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
- define X where "X = N - M"
- define Y where "Y = M - N"
- from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
- from z show "X \<subseteq># N" unfolding X_def by auto
- show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
- show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
- proof (intro allI impI)
- fix k
- assume "k \<in># Y"
- then have "count N k < count M k" unfolding Y_def
- by (auto simp add: in_diff_count)
- with \<open>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a"
- unfolding less_multiset\<^sub>H\<^sub>O_def by blast
- then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def
- by (auto simp add: in_diff_count)
- qed
-qed
+ unfolding less_multiset\<^sub>D\<^sub>M_def less_multiset\<^sub>H\<^sub>O_def
+ unfolding multp\<^sub>D\<^sub>M_def[symmetric] multp\<^sub>H\<^sub>O_def[symmetric]
+ by (rule multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M)
lemma mult_less_multiset\<^sub>D\<^sub>M: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>D\<^sub>M M N"
- by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O)
+ unfolding multp_def[of "(<)", symmetric]
+ using multp_eq_multp\<^sub>D\<^sub>M[of "(<)", simplified]
+ by (simp add: multp\<^sub>D\<^sub>M_def less_multiset\<^sub>D\<^sub>M_def)
lemma mult_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
- by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O)
+ unfolding multp_def[of "(<)", symmetric]
+ using multp_eq_multp\<^sub>H\<^sub>O[of "(<)", simplified]
+ by (simp add: multp\<^sub>H\<^sub>O_def less_multiset\<^sub>H\<^sub>O_def)
lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def]
lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def]
@@ -167,10 +218,15 @@
end
lemma less_multiset_less_multiset\<^sub>H\<^sub>O: "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
- unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
+ unfolding less_multiset_def multp_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
-lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
-lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
+lemma less_multiset\<^sub>D\<^sub>M:
+ "M < N \<longleftrightarrow> (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = N - X + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
+ by (rule mult\<^sub>D\<^sub>M[folded multp_def less_multiset_def])
+
+lemma less_multiset\<^sub>H\<^sub>O:
+ "M < N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x>y. count M x < count N x))"
+ by (rule mult\<^sub>H\<^sub>O[folded multp_def less_multiset_def])
lemma subset_eq_imp_le_multiset:
shows "M \<subseteq># N \<Longrightarrow> M \<le> N"
@@ -198,7 +254,7 @@
(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
- using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
+ using subset_mset.le_zero_eq less_multiset_def multp_def less_multiset\<^sub>D\<^sub>M by blast
(* FIXME: "le" should be "less" in this and other names *)
lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
@@ -381,9 +437,9 @@
begin
lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
- unfolding less_multiset_def by (auto intro: wf_mult wf)
+ unfolding less_multiset_def multp_def by (auto intro: wf_mult wf)
-instance by standard (metis less_multiset_def wf wf_def wf_mult)
+instance by standard (metis less_multiset_def multp_def wf wf_def wf_mult)
end
--- a/src/HOL/List.thy Sat Dec 04 12:38:32 2021 +0100
+++ b/src/HOL/List.thy Sat Dec 04 12:38:51 2021 +0100
@@ -4238,6 +4238,8 @@
case (Cons x xs) thus ?case by (fastforce split: if_splits)
qed
+lemmas find_None_iff2 = find_None_iff[THEN eq_iff_swap]
+
lemma find_Some_iff:
"List.find P xs = Some x \<longleftrightarrow>
(\<exists>i<length xs. P (xs!i) \<and> x = xs!i \<and> (\<forall>j<i. \<not> P (xs!j)))"
@@ -4249,6 +4251,8 @@
using diff_Suc_1[unfolded One_nat_def] less_Suc_eq_0_disj by fastforce
qed
+lemmas find_Some_iff2 = find_Some_iff[THEN eq_iff_swap]
+
lemma find_cong[fundef_cong]:
assumes "xs = ys" and "\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x"
shows "List.find P xs = List.find Q ys"
--- a/src/HOL/Map.thy Sat Dec 04 12:38:32 2021 +0100
+++ b/src/HOL/Map.thy Sat Dec 04 12:38:51 2021 +0100
@@ -667,6 +667,10 @@
lemma fun_upd_None_if_notin_dom[simp]: "k \<notin> dom m \<Longrightarrow> m(k := None) = m"
by auto
+lemma ran_map_upd_Some:
+ "\<lbrakk> m x = Some y; inj_on m (dom m); z \<notin> ran m \<rbrakk> \<Longrightarrow> ran(m(x := Some z)) = ran m - {y} \<union> {z}"
+by(force simp add: ran_def domI inj_onD)
+
lemma ran_map_add:
assumes "dom m1 \<inter> dom m2 = {}"
shows "ran (m1 ++ m2) = ran m1 \<union> ran m2"
--- a/src/HOL/Relation.thy Sat Dec 04 12:38:32 2021 +0100
+++ b/src/HOL/Relation.thy Sat Dec 04 12:38:51 2021 +0100
@@ -241,6 +241,11 @@
lemma irrefl_distinct [code]: "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)"
by (auto simp add: irrefl_def)
+lemma (in preorder) irreflp_less[simp]: "irreflp (<)"
+ by (simp add: irreflpI)
+
+lemma (in preorder) irreflp_greater[simp]: "irreflp (>)"
+ by (simp add: irreflpI)
subsubsection \<open>Asymmetry\<close>
@@ -259,6 +264,17 @@
lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)"
by (blast intro: asymI dest: asymD)
+context preorder begin
+
+lemma asymp_less[simp]: "asymp (<)"
+ by (auto intro: asympI dual_order.asym)
+
+lemma asymp_greater[simp]: "asymp (>)"
+ by (auto intro: asympI dual_order.asym)
+
+end
+
+
subsubsection \<open>Symmetry\<close>
definition sym :: "'a rel \<Rightarrow> bool"
--- a/src/HOL/Wellfounded.thy Sat Dec 04 12:38:32 2021 +0100
+++ b/src/HOL/Wellfounded.thy Sat Dec 04 12:38:51 2021 +0100
@@ -79,6 +79,9 @@
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)
+
subsection \<open>Basic Results\<close>
--- a/src/Pure/Admin/build_release.scala Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Pure/Admin/build_release.scala Sat Dec 04 12:38:51 2021 +0100
@@ -837,6 +837,9 @@
val other_isabelle = context.other_isabelle(tmp_dir)
+ Isabelle_System.make_directory(other_isabelle.etc)
+ File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\n")
+
other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
" -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
" -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
--- a/src/Pure/Admin/build_status.scala Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Pure/Admin/build_status.scala Sat Dec 04 12:38:51 2021 +0100
@@ -204,7 +204,7 @@
profiles: List[Profile] = default_profiles,
only_sessions: Set[String] = Set.empty,
ml_statistics: Boolean = false,
- ml_statistics_domain: String => Boolean = (key: String) => true,
+ ml_statistics_domain: String => Boolean = _ => true,
verbose: Boolean = false): Data =
{
val date = Date.now()
@@ -377,7 +377,7 @@
List(HTML.description(
List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
HTML.par(
- List(HTML.itemize(data.entries.map({ case data_entry =>
+ List(HTML.itemize(data.entries.map(data_entry =>
List(
HTML.link(clean_name(data_entry.name) + "/index.html",
HTML.text(data_entry.name))) :::
@@ -388,7 +388,7 @@
List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) :::
List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
})
- }))))))
+ ))))))
for (data_entry <- data.entries) {
val data_name = data_entry.name
@@ -423,10 +423,10 @@
entry.ml_timing.elapsed.minutes.toString,
entry.ml_timing.resources.minutes.toString,
entry.maximum_code.toString,
- entry.maximum_code.toString,
+ entry.average_code.toString,
+ entry.maximum_stack.toString,
entry.average_stack.toString,
- entry.maximum_stack.toString,
- entry.average_heap.toString,
+ entry.maximum_heap.toString,
entry.average_heap.toString,
entry.stored_heap.toString).mkString(" "))))
@@ -608,7 +608,7 @@
"l:" -> (arg => options = options + ("build_log_history=" + arg)),
"o:" -> (arg => options = options + arg),
"s:" -> (arg =>
- space_explode('x', arg).map(Value.Int.parse(_)) match {
+ space_explode('x', arg).map(Value.Int.parse) match {
case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
case _ => error("Error bad PNG image size: " + quote(arg))
}),
--- a/src/Pure/Admin/isabelle_cronjob.scala Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sat Dec 04 12:38:51 2021 +0100
@@ -314,7 +314,7 @@
{
List(
List(Remote_Build("Linux A", "augsburg1",
- options = "-m32 -B -M1x2,2,4" +
+ options = "-m32 -B -M4" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_MLTON=mlton" +
--- a/src/Pure/ML/ml_statistics.scala Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala Sat Dec 04 12:38:51 2021 +0100
@@ -194,7 +194,7 @@
val empty: ML_Statistics = apply(Nil)
def apply(ml_statistics0: List[Properties.T], heading: String = "",
- domain: String => Boolean = (key: String) => true): ML_Statistics =
+ domain: String => Boolean = _ => true): ML_Statistics =
{
require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field")
@@ -260,6 +260,11 @@
val time_start: Double,
val duration: Double)
{
+ override def toString: String =
+ if (content.isEmpty) "ML_Statistics.empty"
+ else "ML_Statistics(length = " + content.length + ", fields = " + fields.size + ")"
+
+
/* content */
def maximum(field: String): Double =
@@ -286,7 +291,7 @@
def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit =
{
- data.removeAllSeries
+ data.removeAllSeries()
for (field <- selected_fields) {
val series = new XYSeries(field)
content.foreach(entry => series.add(entry.time, entry.get(field)))
--- a/src/Tools/VSCode/extension/README.md Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Tools/VSCode/extension/README.md Sat Dec 04 12:38:51 2021 +0100
@@ -1,14 +1,15 @@
# Isabelle Prover IDE support
This extension connects VSCode to the Isabelle Prover IDE infrastructure: it
-requires Isabelle2021-1.
+requires a suitable repository version of Isabelle.
The implementation is centered around the VSCode Language Server protocol, but
with many add-ons that are specific to VSCode and Isabelle/PIDE.
See also:
- * <https://isabelle.in.tum.de/website-Isabelle2021-1>
+ * <https://isabelle.sketis.net/repos/isabelle/file/tip/src/Tools/VSCode>
+ * <https://github.com/Microsoft/language-server-protocol>
## Screenshot
@@ -57,8 +58,8 @@
### Isabelle/VSCode Installation
- * Download Isabelle2021-1 from <https://isabelle.in.tum.de/website-Isabelle2021-1>
- or any of its mirror sites.
+ * Download a recent Isabelle development snapshot from
+ <https://isabelle.sketis.net/devel/release_snapshot>
* Unpack and run the main Isabelle/jEdit application as usual, to ensure that
the logic image is built properly and Isabelle works as expected.
@@ -88,17 +89,17 @@
+ Linux:
```
- "isabelle.home": "/home/makarius/Isabelle2021-1"
+ "isabelle.home": "/home/makarius/Isabelle"
```
+ Mac OS X:
```
- "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2021-1"
+ "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle"
```
+ Windows:
```
- "isabelle.home": "C:\\Users\\makarius\\Isabelle2021-1"
+ "isabelle.home": "C:\\Users\\makarius\\Isabelle"
```
* Restart the VSCode application to ensure that all extensions are properly
--- a/src/Tools/VSCode/extension/package.json Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Tools/VSCode/extension/package.json Sat Dec 04 12:38:51 2021 +0100
@@ -1,6 +1,6 @@
{
- "name": "Isabelle2021-1",
- "displayName": "Isabelle2021-1",
+ "name": "Isabelle",
+ "displayName": "Isabelle",
"description": "Isabelle Prover IDE",
"keywords": [
"theorem prover",