--- a/Admin/Release/CHECKLIST Sat Oct 02 20:18:20 2021 +0200
+++ b/Admin/Release/CHECKLIST Sat Oct 02 20:44:33 2021 +0200
@@ -32,8 +32,8 @@
- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
- check versions:
- src/Tools/jEdit/src/Isabelle.props
- src/Tools/jEdit/src-base/Isabelle_Base.props
+ src/Tools/jEdit/jedit_base/plugin.props
+ src/Tools/jEdit/jedit_main/plugin.props
- check Isabelle version:
src/Tools/VSCode/extension/README.md
@@ -71,20 +71,17 @@
Packaging
=========
-- macOS: provide "gnutar" executable via shell PATH
- (e.g. copy of /usr/bin/gnutar from Mountain Lion)
-
- fully-automated packaging (e.g. on lxcisa0):
- hg up -r DISTNAME && Admin/build_release -D /home/isabelle/dist -b HOL -l -R DISTNAME
+ hg up -r DISTNAME && Admin/build_release -J .../java11 -D /home/isabelle/dist -b HOL -l -R DISTNAME
- Docker image:
- isabelle build_docker -o Dockerfile -E -t makarius/isabelle:Isabelle2021 Isabelle2021_linux.tar.gz
+ isabelle build_docker -o Dockerfile -E -t makarius/isabelle:Isabelle2021-1 Isabelle2021-1_linux.tar.gz
docker login
- docker push makarius/isabelle:Isabelle2021
+ docker push makarius/isabelle:Isabelle2021-1
docker tag ... latest
docker push makarius/isabelle:latest
--- a/CONTRIBUTORS Sat Oct 02 20:18:20 2021 +0200
+++ b/CONTRIBUTORS Sat Oct 02 20:44:33 2021 +0200
@@ -3,8 +3,8 @@
listed as an author in one of the source files of this Isabelle distribution.
-Contributions to this Isabelle version
---------------------------------------
+Contributions to Isabelle2021-1
+-------------------------------
* July 2021: Florian Haftmann
Further consolidation of bit operations and word types.
@@ -16,7 +16,7 @@
More context situations susceptible to global_interpretation.
* March 2021: Lukas Stevens
- New order prover
+ New order prover.
* March 2021: Florian Haftmann
Dedicated session for combinatorics.
--- a/NEWS Sat Oct 02 20:18:20 2021 +0200
+++ b/NEWS Sat Oct 02 20:44:33 2021 +0200
@@ -4,16 +4,16 @@
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
-New in this Isabelle version
-----------------------------
+New in Isabelle2021 (December 2021)
+-----------------------------------
*** General ***
* Commands 'syntax' and 'no_syntax' now work in a local theory context,
-but there is no proper way to refer to local entities --- in contrast to
-'notation' and 'no_notation'. Local syntax works well with 'bundle',
-e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory Main of
-Isabelle/HOL.
+but in contrast to 'notation' and 'no_notation' there is no proper way
+to refer to local entities. Note that local syntax works well with
+'bundle', e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory
+Main of Isabelle/HOL.
* Configuration option "show_results" controls output of final results
in commands like 'definition' or 'theorem'. Output is normally enabled
@@ -26,19 +26,6 @@
theorem test by (simp add: test_def)
end
-* Timeouts for Isabelle/ML tools are subject to system option
-"timeout_scale" --- this already used for the overall session build
-process before, and allows to adapt to slow machines. The underlying
-Timeout.apply in Isabelle/ML treats an original timeout specification 0
-as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY
-in boundary cases.
-
-* Remote provers from SystemOnTPTP (notably for Sledgehammer) are now
-managed via Isabelle/Scala instead of perl; the dependency on
-libwww-perl has been eliminated (notably on Linux). Rare
-INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties
-https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html
-
* More symbol definitions for the Z Notation (Isabelle fonts and LaTeX).
See also the group "Z Notation" in the Symbols dockable of
Isabelle/jEdit.
@@ -143,6 +130,63 @@
*** HOL ***
+* 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
+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
+INCOMPATIBILITY; note that for most applications less elementary lemmas
+exists.
+
+* 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.
+
+* Infix syntax for bit operations AND, OR, XOR, NOT is now organized in
+bundle bit_operations_syntax. INCOMPATIBILITY.
+
+* Bit operations set_bit, unset_bit and flip_bit are now class
+operations. INCOMPATIBILITY.
+
+* Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY.
+
+* Simplified class hierarchy for bit operations: bit operations reside
+in classes (semi)ring_bit_operations, class semiring_bit_shifts is
+gone.
+
+* Expressions of the form "NOT (numeral _)" are not simplified by
+default any longer. INCOMPATIBILITY, use not_one_eq and not_numeral_eq
+as simp rule explicitly if needed.
+
+* 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.
+INCOMPATIBILITY.
+
+* Reorganized classes and locales for boolean algebras.
+INCOMPATIBILITY.
+
+* New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3,
+min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor
+INCOMPATIBILITY.
+
+* Sledgehammer:
+ - Removed legacy "lam_lifting" (synonym for "lifting") from option
+ "lam_trans". Minor INCOMPATIBILITY.
+ - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor
+ INCOMPATIBILITY.
+ - Added "opaque_combs" to option "lam_trans": lambda expressions are
+ rewritten using combinators, but the combinators are kept opaque,
+ i.e. without definitions.
+
+* Metis: Renamed option "hide_lams" to "opaque_lifting". Minor
+INCOMPATIBILITY.
+
* Theory HOL-Library.Lattice_Syntax has been superseded by bundle
"lattice_syntax": it can be used in a local context via 'include' or in
a global theory via 'unbundle'. The opposite declarations are bundled as
@@ -181,20 +225,9 @@
before were corrected. Minor INCOMPATIBILITY.
* Session "HOL-Analysis": the complex Arg function has been identified
-with the function "arg" of Complex_Main, renaming arg->Arg also in the
+with the function "arg" of Complex_Main, renaming arg ~> Arg also in the
names of arg_bounded. 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
-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
-INCOMPATIBILITY; note that for most applications less elementary lemmas
-exists.
-
* 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".
@@ -208,52 +241,6 @@
* 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.
-
-* Infix syntax for bit operations AND, OR, XOR, NOT is now organized in
-bundle bit_operations_syntax. INCOMPATIBILITY.
-
-* Bit operations set_bit, unset_bit and flip_bit are now class
-operations. INCOMPATIBILITY.
-
-* Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY.
-
-* Simplified class hierarchy for bit operations: bit operations reside
-in classes (semi)ring_bit_operations, class semiring_bit_shifts is
-gone.
-
-* Expressions of the form "NOT (numeral _)" are not simplified by
-default any longer. INCOMPATIBILITY, use not_one_eq and not_numeral_eq
-as simp rule explicitly if needed.
-
-* 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.
-INCOMPATIBILITY.
-
-* Reorganized classes and locales for boolean algebras.
-INCOMPATIBILITY.
-
-* New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3,
-min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor
-INCOMPATIBILITY.
-
-* Sledgehammer:
- - Removed legacy "lam_lifting" (synonym for "lifting") from option
- "lam_trans". Minor INCOMPATIBILITY.
- - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans".
- Minor INCOMPATIBILITY.
- - Added "opaque_combs" to option "lam_trans": lambda expressions are rewritten
- using combinators, but the combinators are kept opaque, i.e. without
- definitions.
-
-* Metis:
- - Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY.
-
*** ML ***
@@ -380,6 +367,17 @@
- Isabelle_System.rm_tree
- Isabelle_System.download
+* 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 ***
@@ -406,16 +404,18 @@
isabelle.jedit module is now part of Isabelle/Scala (as one big
$ISABELLE_SCALA_JAR).
-* 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.
+* Timeouts for Isabelle/ML tools are subject to system option
+"timeout_scale" --- this already used for the overall session build
+process before, and allows to adapt to slow machines. The underlying
+Timeout.apply in Isabelle/ML treats an original timeout specification 0
+as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY
+in boundary cases.
+
+* Remote provers from SystemOnTPTP (notably for Sledgehammer) are now
+managed via Isabelle/Scala instead of perl; the dependency on
+libwww-perl has been eliminated (notably on Linux). Rare
+INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties
+https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html
* System option "system_log" specifies an optional log file for internal
messages produced by Output.system_message in Isabelle/ML; the value
@@ -429,7 +429,7 @@
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.
+(without full .hg directory). It also provides more options.
* Obsolete settings variable ISABELLE_PLATFORM32 has been discontinued.
Note that only Windows supports old 32 bit executables, via settings
--- a/src/Doc/JEdit/JEdit.thy Sat Oct 02 20:18:20 2021 +0200
+++ b/src/Doc/JEdit/JEdit.thy Sat Oct 02 20:44:33 2021 +0200
@@ -304,7 +304,7 @@
The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
different server name. The default server name is the official distribution
- name (e.g.\ \<^verbatim>\<open>Isabelle2021\<close>). Thus @{tool jedit_client} can connect to the
+ name (e.g.\ \<^verbatim>\<open>Isabelle2021-1\<close>). Thus @{tool jedit_client} can connect to the
Isabelle desktop application without further options.
The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
--- a/src/Doc/System/Environment.thy Sat Oct 02 20:18:20 2021 +0200
+++ b/src/Doc/System/Environment.thy Sat Oct 02 20:44:33 2021 +0200
@@ -58,7 +58,7 @@
\<^enum> The file \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close> (if it
exists) is run in the same way as the site default settings. Note that the
variable @{setting ISABELLE_HOME_USER} has already been set before ---
- usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2021\<close>.
+ usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2021-1\<close>.
Thus individual users may override the site-wide defaults. Typically, a
user settings file contains only a few lines, with some assignments that
@@ -137,7 +137,7 @@
of the @{executable isabelle} executable.
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
- Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2021\<close>''.
+ Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2021-1\<close>''.
\<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
--- a/src/Doc/System/Misc.thy Sat Oct 02 20:18:20 2021 +0200
+++ b/src/Doc/System/Misc.thy Sat Oct 02 20:44:33 2021 +0200
@@ -71,7 +71,7 @@
Isabelle installation: it needs to be a suitable version of Ubuntu Linux.
The default \<^verbatim>\<open>ubuntu\<close> refers to the latest LTS version provided by Canonical
as the official Ubuntu vendor\<^footnote>\<open>\<^url>\<open>https://hub.docker.com/_/ubuntu\<close>\<close>. For
- Isabelle2021 this should be Ubuntu 20.04 LTS.
+ Isabelle2021-1 this should be Ubuntu 20.04 LTS.
Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology
of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution.
@@ -98,22 +98,22 @@
Produce a Dockerfile (without image) from a remote Isabelle distribution:
@{verbatim [display]
\<open> isabelle build_docker -E -n -o Dockerfile
- https://isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021_linux.tar.gz\<close>}
+ https://isabelle.in.tum.de/website-Isabelle2021-1/dist/Isabelle2021-1_linux.tar.gz\<close>}
Build a standard Isabelle Docker image from a local Isabelle distribution,
with \<^verbatim>\<open>bin/isabelle\<close> as executable entry point:
@{verbatim [display]
-\<open> isabelle build_docker -E -t test/isabelle:Isabelle2021 Isabelle2021_linux.tar.gz\<close>}
+\<open> isabelle build_docker -E -t test/isabelle:Isabelle2021-1 Isabelle2021-1_linux.tar.gz\<close>}
Invoke the raw Isabelle/ML process within that image:
@{verbatim [display]
-\<open> docker run test/isabelle:Isabelle2021 process -e "Session.welcome ()"\<close>}
+\<open> docker run test/isabelle:Isabelle2021-1 process -e "Session.welcome ()"\<close>}
Invoke a Linux command-line tool within the contained Isabelle system
environment:
@{verbatim [display]
-\<open> docker run test/isabelle:Isabelle2021 env uname -a\<close>}
+\<open> docker run test/isabelle:Isabelle2021-1 env uname -a\<close>}
The latter should always report a Linux operating system, even when running
on Windows or macOS.
\<close>
@@ -376,7 +376,7 @@
\<^medskip>
The default is to output the full version string of the Isabelle
- distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2021: February 2021\<close>.
+ distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2021-1: December 2021\<close>.
\<^medskip>
Option \<^verbatim>\<open>-i\<close> produces a short identification derived from the Mercurial id
--- a/src/HOL/List.thy Sat Oct 02 20:18:20 2021 +0200
+++ b/src/HOL/List.thy Sat Oct 02 20:44:33 2021 +0200
@@ -371,7 +371,7 @@
begin
abbreviation sorted :: "'a list \<Rightarrow> bool" where
- "sorted \<equiv> sorted_wrt (\<le>)"
+ "sorted \<equiv> sorted_wrt (\<le>)"
lemma sorted_simps: "sorted [] = True" "sorted (x # ys) = ((\<forall>y \<in> set ys. x\<le>y) \<and> sorted ys)"
by auto
@@ -1499,7 +1499,7 @@
| len (Const(\<^const_name>\<open>rev\<close>,_) $ xs) acc = len xs acc
| len (Const(\<^const_name>\<open>map\<close>,_) $ _ $ xs) acc = len xs acc
| len (Const(\<^const_name>\<open>concat\<close>,T) $ (Const(\<^const_name>\<open>rev\<close>,_) $ xss)) acc
- = len (Const(\<^const_name>\<open>concat\<close>,T) $ xss) acc
+ = len (Const(\<^const_name>\<open>concat\<close>,T) $ xss) acc
| len t (ts,n) = (t::ts,n);
val ss = simpset_of \<^context>;
@@ -3128,7 +3128,7 @@
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)
+ (simp_all add: insert_absorb fold_fun_left_comm)
lemma (in comp_fun_idem_on) fold_set_fold:
assumes "set xs \<subseteq> S"
@@ -3510,7 +3510,7 @@
lemma successively_append_iff:
"successively P (xs @ ys) \<longleftrightarrow>
- successively P xs \<and> successively P ys \<and>
+ successively P xs \<and> successively P ys \<and>
(xs = [] \<or> ys = [] \<or> P (last xs) (hd ys))"
by (induction xs) (auto simp: successively_Cons)
@@ -4141,7 +4141,7 @@
by (metis (full_types) dropWhile_eq_self_iff last_snoc remdups_adj_append_dropWhile)
thus ?thesis by (simp add: xs)
qed
- thus ?thesis using assms
+ thus ?thesis using assms
by (cases "xs = []"; cases "ys = []") auto
qed
@@ -4425,7 +4425,7 @@
by (auto dest: length_filter_less simp add: removeAll_filter_not_eq)
lemma distinct_concat_iff: "distinct (concat xs) \<longleftrightarrow>
- distinct (removeAll [] xs) \<and>
+ distinct (removeAll [] xs) \<and>
(\<forall>ys. ys \<in> set xs \<longrightarrow> distinct ys) \<and>
(\<forall>ys zs. ys \<in> set xs \<and> zs \<in> set xs \<and> ys \<noteq> zs \<longrightarrow> set ys \<inter> set zs = {})"
apply (induct xs)
@@ -4993,7 +4993,7 @@
lemma splice_replicate[simp]: "splice (replicate m x) (replicate n x) = replicate (m+n) x"
proof (induction "replicate m x" "replicate n x" arbitrary: m n rule: splice.induct)
case (2 x xs)
- then show ?case
+ then show ?case
by (auto simp add: Cons_replicate_eq dest: gr0_implies_Suc)
qed auto
@@ -5360,7 +5360,7 @@
lemma infinite_UNIV_listI: "\<not> finite(UNIV::'a list set)"
by (metis UNIV_I finite_maxlen length_replicate less_irrefl)
-lemma same_length_different:
+lemma same_length_different:
assumes "xs \<noteq> ys" and "length xs = length ys"
shows "\<exists>pre x xs' y ys'. x\<noteq>y \<and> xs = pre @ [x] @ xs' \<and> ys = pre @ [y] @ ys'"
using assms
@@ -5462,7 +5462,7 @@
proof
assume ?L
thus ?R
- by (simp add: sorted_wrt_iff_nth_less)
+ by (simp add: sorted_wrt_iff_nth_less)
next
assume ?R
have "i < j \<Longrightarrow> j < length xs \<Longrightarrow> P (xs ! i) (xs ! j)" for i j
@@ -5545,7 +5545,7 @@
"sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
by (auto simp: sorted_iff_nth_mono)
-lemma sorted_iff_nth_Suc:
+lemma sorted_iff_nth_Suc:
"sorted xs \<longleftrightarrow> (\<forall>i. Suc i < length xs \<longrightarrow> xs!i \<le> xs!(Suc i))"
by(simp add: sorted_wrt_iff_nth_Suc_transp)
@@ -5573,13 +5573,13 @@
thus ?L by (simp add: sorted_iff_nth_mono)
qed
-lemma sorted_rev_iff_nth_Suc:
+lemma sorted_rev_iff_nth_Suc:
"sorted (rev xs) \<longleftrightarrow> (\<forall>i. Suc i < length xs \<longrightarrow> xs!(Suc i) \<le> xs!i)"
proof-
interpret dual: linorder "(\<lambda>x y. y \<le> x)" "(\<lambda>x y. y < x)"
using dual_linorder .
show ?thesis
- using dual_linorder dual.sorted_iff_nth_Suc dual.sorted_iff_nth_mono
+ using dual_linorder dual.sorted_iff_nth_Suc dual.sorted_iff_nth_mono
unfolding sorted_rev_iff_nth_mono by simp
qed
@@ -6244,7 +6244,7 @@
proof (cases ys)
case Nil
then show ?thesis
- using Cons.prems by auto
+ using Cons.prems by auto
next
case (Cons y ys')
then have "xs = ys'"
@@ -6255,13 +6255,13 @@
using local.Cons by blast
qed
qed auto
-
+
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_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"
+ 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_key_list_of_set by metis
@@ -6326,7 +6326,7 @@
"sorted_list_of_set {m..<n} = [m..<n]"
by (rule sorted_distinct_set_unique) simp_all
-lemma sorted_list_of_set_lessThan_Suc [simp]:
+lemma sorted_list_of_set_lessThan_Suc [simp]:
"sorted_list_of_set {..<Suc k} = sorted_list_of_set {..<k} @ [k]"
using le0 lessThan_atLeast0 sorted_list_of_set_range upt_Suc_append by presburger
@@ -6341,7 +6341,7 @@
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"
+ assumes "Suc i < j"
shows "sorted_list_of_set {i<..<j} = Suc i # sorted_list_of_set {Suc i<..<j}"
proof -
have "{i<..<j} = insert (Suc i) {Suc i<..<j}"
@@ -6351,16 +6351,16 @@
qed
lemma sorted_list_of_set_greaterThanAtMost:
- assumes "Suc i \<le> j"
+ assumes "Suc i \<le> j"
shows "sorted_list_of_set {i<..j} = Suc i # sorted_list_of_set {Suc i<..j}"
using sorted_list_of_set_greaterThanLessThan [of i "Suc j"]
by (metis assms greaterThanAtMost_def greaterThanLessThan_eq le_imp_less_Suc lessThan_Suc_atMost)
-lemma nth_sorted_list_of_set_greaterThanLessThan:
+lemma nth_sorted_list_of_set_greaterThanLessThan:
"n < j - Suc i \<Longrightarrow> sorted_list_of_set {i<..<j} ! n = Suc (i+n)"
by (induction n arbitrary: i) (auto simp: sorted_list_of_set_greaterThanLessThan)
-lemma nth_sorted_list_of_set_greaterThanAtMost:
+lemma nth_sorted_list_of_set_greaterThanAtMost:
"n < j - i \<Longrightarrow> sorted_list_of_set {i<..j} ! n = Suc (i+n)"
using nth_sorted_list_of_set_greaterThanLessThan [of n "Suc j" i]
by (simp add: greaterThanAtMost_def greaterThanLessThan_eq lessThan_Suc_atMost)
@@ -6515,7 +6515,7 @@
"(xs, ys) \<in> lexn r n \<Longrightarrow> length xs = n \<and> length ys = n"
by (induct n arbitrary: xs ys) auto
-lemma wf_lex [intro!]:
+lemma wf_lex [intro!]:
assumes "wf r" shows "wf (lex r)"
unfolding lex_def
proof (rule wf_UN)
@@ -6631,7 +6631,7 @@
if "xs \<noteq> ys" and len: "length xs = length ys" for xs ys
proof -
obtain pre x xs' y ys' where "x\<noteq>y" and xs: "xs = pre @ [x] @ xs'" and ys: "ys = pre @ [y] @ys'"
- by (meson len \<open>xs \<noteq> ys\<close> same_length_different)
+ by (meson len \<open>xs \<noteq> ys\<close> same_length_different)
then consider "(x,y) \<in> r" | "(y,x) \<in> r"
by (meson UNIV_I assms total_on_def)
then show ?thesis
@@ -6662,14 +6662,14 @@
by (simp add: lex_conv) (blast intro: Cons_eq_appendI)
qed
-lemma Nil_lenlex_iff1 [simp]: "([], ns) \<in> lenlex r \<longleftrightarrow> ns \<noteq> []"
+lemma Nil_lenlex_iff1 [simp]: "([], ns) \<in> lenlex r \<longleftrightarrow> ns \<noteq> []"
and Nil_lenlex_iff2 [simp]: "(ns,[]) \<notin> lenlex r"
by (auto simp: lenlex_def)
-lemma Cons_lenlex_iff:
- "((m # ms, n # ns) \<in> lenlex r) \<longleftrightarrow>
- length ms < length ns
- \<or> length ms = length ns \<and> (m,n) \<in> r
+lemma Cons_lenlex_iff:
+ "((m # ms, n # ns) \<in> lenlex r) \<longleftrightarrow>
+ length ms < length ns
+ \<or> length ms = length ns \<and> (m,n) \<in> r
\<or> (m = n \<and> (ms,ns) \<in> lenlex r)"
by (auto simp: lenlex_def)
@@ -6797,19 +6797,19 @@
proof-
from leD[OF assms(2)] assms(1)[unfolded lexord_take_index_conv[of u w r] min_absorb2[OF assms(2)]]
obtain i where "take i u = take i w" and "(u!i,w!i) \<in> r" and "i < length w"
- by blast
+ by blast
hence "((u@v)!i, (w@z)!i) \<in> r"
unfolding nth_append using less_le_trans[OF \<open>i < length w\<close> assms(2)] \<open>(u!i,w!i) \<in> r\<close>
by presburger
moreover have "i < min (length (u@v)) (length (w@z))"
using assms(2) \<open>i < length w\<close> by simp
moreover have "take i (u@v) = take i (w@z)"
- using assms(2) \<open>i < length w\<close> \<open>take i u = take i w\<close> by simp
+ using assms(2) \<open>i < length w\<close> \<open>take i u = take i w\<close> by simp
ultimately show ?thesis
using lexord_take_index_conv by blast
qed
-lemma lexord_sufE:
+lemma lexord_sufE:
assumes "(xs@zs,ys@qs) \<in> lexord r" "xs \<noteq> ys" "length xs = length ys" "length zs = length qs"
shows "(xs,ys) \<in> lexord r"
proof-
@@ -6893,7 +6893,7 @@
qed
corollary lexord_linear: "(\<forall>a b. (a,b) \<in> r \<or> a = b \<or> (b,a) \<in> r) \<Longrightarrow> (x,y) \<in> lexord r \<or> x = y \<or> (y,x) \<in> lexord r"
- using total_lexord by (metis UNIV_I total_on_def)
+ using total_lexord by (metis UNIV_I total_on_def)
lemma lexord_irrefl:
"irrefl R \<Longrightarrow> irrefl (lexord R)"
@@ -6902,7 +6902,7 @@
lemma lexord_asym:
assumes "asym R"
shows "asym (lexord R)"
-proof
+proof
fix xs ys
assume "(xs, ys) \<in> lexord R"
then show "(ys, xs) \<notin> lexord R"
@@ -6932,12 +6932,12 @@
by (simp add: lenlex_def asym_inv_image asym_less_than asym_lex asym_lex_prod)
lemma lenlex_append1:
- assumes len: "(us,xs) \<in> lenlex R" and eq: "length vs = length ys"
+ assumes len: "(us,xs) \<in> lenlex R" and eq: "length vs = length ys"
shows "(us @ vs, xs @ ys) \<in> lenlex R"
using len
proof (induction us)
case Nil
- then show ?case
+ then show ?case
by (simp add: lenlex_def eq)
next
case (Cons u us)
@@ -6950,7 +6950,7 @@
shows "(us @ xs, us @ ys) \<in> lenlex R \<longleftrightarrow> (xs, ys) \<in> lenlex R"
proof (induction us)
case Nil
- then show ?case
+ then show ?case
by (simp add: lenlex_def)
next
case (Cons u us)
--- a/src/Tools/jEdit/jedit_main/plugin.props Sat Oct 02 20:18:20 2021 +0200
+++ b/src/Tools/jEdit/jedit_main/plugin.props Sat Oct 02 20:44:33 2021 +0200
@@ -16,7 +16,7 @@
plugin.isabelle.jedit_main.Plugin.depend.0=jdk 11
plugin.isabelle.jedit_main.Plugin.depend.1=jedit 05.05.00.00
plugin.isabelle.jedit_main.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
-plugin.isabelle.jedit_main.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3
+plugin.isabelle.jedit_main.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.4.0
plugin.isabelle.jedit_main.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8
plugin.isabelle.jedit_main.Plugin.depend.5=plugin isabelle.jedit_base.Plugin 1.0