# HG changeset patch # User wenzelm # Date 1633200273 -7200 # Node ID dd1f5a00115fab73b45253d5840b98fdb49139e4 # Parent 7fd8fb6149a6f4fcfc0e4c9805e3fef74a514eab# Parent 011ecb267e417ced63ec02cd0a71a24cce5ccacf merged diff -r 7fd8fb6149a6 -r dd1f5a00115f Admin/Release/CHECKLIST --- 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 diff -r 7fd8fb6149a6 -r dd1f5a00115f CONTRIBUTORS --- 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. diff -r 7fd8fb6149a6 -r dd1f5a00115f NEWS --- 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 diff -r 7fd8fb6149a6 -r dd1f5a00115f src/Doc/JEdit/JEdit.thy --- 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>\-n\ option reports the server name, and the \<^verbatim>\-s\ option provides a different server name. The default server name is the official distribution - name (e.g.\ \<^verbatim>\Isabelle2021\). Thus @{tool jedit_client} can connect to the + name (e.g.\ \<^verbatim>\Isabelle2021-1\). Thus @{tool jedit_client} can connect to the Isabelle desktop application without further options. The \<^verbatim>\-p\ option allows to override the implicit default of the system diff -r 7fd8fb6149a6 -r dd1f5a00115f src/Doc/System/Environment.thy --- 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>\$ISABELLE_HOME_USER/etc/settings\ (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>\$USER_HOME/.isabelle/Isabelle2021\. + usually to something like \<^verbatim>\$USER_HOME/.isabelle/Isabelle2021-1\. 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}\\<^sup>*\] refers to the name of this - Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2021\''. + Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2021-1\''. \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\\<^sup>*\] diff -r 7fd8fb6149a6 -r dd1f5a00115f src/Doc/System/Misc.thy --- 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>\ubuntu\ refers to the latest LTS version provided by Canonical as the official Ubuntu vendor\<^footnote>\\<^url>\https://hub.docker.com/_/ubuntu\\. For - Isabelle2021 this should be Ubuntu 20.04 LTS. + Isabelle2021-1 this should be Ubuntu 20.04 LTS. Option \<^verbatim>\-p\ includes additional Ubuntu packages, using the terminology of \<^verbatim>\apt-get install\ within the underlying Linux distribution. @@ -98,22 +98,22 @@ Produce a Dockerfile (without image) from a remote Isabelle distribution: @{verbatim [display] \ isabelle build_docker -E -n -o Dockerfile - https://isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021_linux.tar.gz\} + https://isabelle.in.tum.de/website-Isabelle2021-1/dist/Isabelle2021-1_linux.tar.gz\} Build a standard Isabelle Docker image from a local Isabelle distribution, with \<^verbatim>\bin/isabelle\ as executable entry point: @{verbatim [display] -\ isabelle build_docker -E -t test/isabelle:Isabelle2021 Isabelle2021_linux.tar.gz\} +\ isabelle build_docker -E -t test/isabelle:Isabelle2021-1 Isabelle2021-1_linux.tar.gz\} Invoke the raw Isabelle/ML process within that image: @{verbatim [display] -\ docker run test/isabelle:Isabelle2021 process -e "Session.welcome ()"\} +\ docker run test/isabelle:Isabelle2021-1 process -e "Session.welcome ()"\} Invoke a Linux command-line tool within the contained Isabelle system environment: @{verbatim [display] -\ docker run test/isabelle:Isabelle2021 env uname -a\} +\ docker run test/isabelle:Isabelle2021-1 env uname -a\} The latter should always report a Linux operating system, even when running on Windows or macOS. \ @@ -376,7 +376,7 @@ \<^medskip> The default is to output the full version string of the Isabelle - distribution, e.g.\ ``\<^verbatim>\Isabelle2021: February 2021\. + distribution, e.g.\ ``\<^verbatim>\Isabelle2021-1: December 2021\. \<^medskip> Option \<^verbatim>\-i\ produces a short identification derived from the Mercurial id diff -r 7fd8fb6149a6 -r dd1f5a00115f src/HOL/List.thy --- 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 \ bool" where - "sorted \ sorted_wrt (\)" + "sorted \ sorted_wrt (\)" lemma sorted_simps: "sorted [] = True" "sorted (x # ys) = ((\y \ set ys. x\y) \ sorted ys)" by auto @@ -1499,7 +1499,7 @@ | len (Const(\<^const_name>\rev\,_) $ xs) acc = len xs acc | len (Const(\<^const_name>\map\,_) $ _ $ xs) acc = len xs acc | len (Const(\<^const_name>\concat\,T) $ (Const(\<^const_name>\rev\,_) $ xss)) acc - = len (Const(\<^const_name>\concat\,T) $ xss) acc + = len (Const(\<^const_name>\concat\,T) $ xss) acc | len t (ts,n) = (t::ts,n); val ss = simpset_of \<^context>; @@ -3128,7 +3128,7 @@ assumes "set xs \ S" shows "Finite_Set.fold f y (set xs) = fold f (remdups xs) y" by (rule sym, use assms in \induct xs arbitrary: y\) - (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 \ S" @@ -3510,7 +3510,7 @@ lemma successively_append_iff: "successively P (xs @ ys) \ - successively P xs \ successively P ys \ + successively P xs \ successively P ys \ (xs = [] \ ys = [] \ 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) \ - distinct (removeAll [] xs) \ + distinct (removeAll [] xs) \ (\ys. ys \ set xs \ distinct ys) \ (\ys zs. ys \ set xs \ zs \ set xs \ ys \ zs \ set ys \ 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: "\ 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 \ ys" and "length xs = length ys" shows "\pre x xs' y ys'. x\y \ xs = pre @ [x] @ xs' \ 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 \ j < length xs \ P (xs ! i) (xs ! j)" for i j @@ -5545,7 +5545,7 @@ "sorted xs \ i \ j \ j < length xs \ xs!i \ xs!j" by (auto simp: sorted_iff_nth_mono) -lemma sorted_iff_nth_Suc: +lemma sorted_iff_nth_Suc: "sorted xs \ (\i. Suc i < length xs \ xs!i \ 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) \ (\i. Suc i < length xs \ xs!(Suc i) \ xs!i)" proof- interpret dual: linorder "(\x y. y \ x)" "(\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: "\\<^sub>\\<^sub>1xs. sorted_wrt (<) xs \ set xs = A" by (simp add: Uniq_def strict_sorted_equal) lemma sorted_key_list_of_set_inject: assumes "A \ S" "B \ 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.. j" + assumes "Suc i \ 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 \ sorted_list_of_set {i<.. 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) \ lexn r n \ length xs = n \ 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 \ ys" and len: "length xs = length ys" for xs ys proof - obtain pre x xs' y ys' where "x\y" and xs: "xs = pre @ [x] @ xs'" and ys: "ys = pre @ [y] @ys'" - by (meson len \xs \ ys\ same_length_different) + by (meson len \xs \ ys\ same_length_different) then consider "(x,y) \ r" | "(y,x) \ 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) \ lenlex r \ ns \ []" +lemma Nil_lenlex_iff1 [simp]: "([], ns) \ lenlex r \ ns \ []" and Nil_lenlex_iff2 [simp]: "(ns,[]) \ lenlex r" by (auto simp: lenlex_def) -lemma Cons_lenlex_iff: - "((m # ms, n # ns) \ lenlex r) \ - length ms < length ns - \ length ms = length ns \ (m,n) \ r +lemma Cons_lenlex_iff: + "((m # ms, n # ns) \ lenlex r) \ + length ms < length ns + \ length ms = length ns \ (m,n) \ r \ (m = n \ (ms,ns) \ 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) \ r" and "i < length w" - by blast + by blast hence "((u@v)!i, (w@z)!i) \ r" unfolding nth_append using less_le_trans[OF \i < length w\ assms(2)] \(u!i,w!i) \ r\ by presburger moreover have "i < min (length (u@v)) (length (w@z))" using assms(2) \i < length w\ by simp moreover have "take i (u@v) = take i (w@z)" - using assms(2) \i < length w\ \take i u = take i w\ by simp + using assms(2) \i < length w\ \take i u = take i w\ by simp ultimately show ?thesis using lexord_take_index_conv by blast qed -lemma lexord_sufE: +lemma lexord_sufE: assumes "(xs@zs,ys@qs) \ lexord r" "xs \ ys" "length xs = length ys" "length zs = length qs" shows "(xs,ys) \ lexord r" proof- @@ -6893,7 +6893,7 @@ qed corollary lexord_linear: "(\a b. (a,b) \ r \ a = b \ (b,a) \ r) \ (x,y) \ lexord r \ x = y \ (y,x) \ 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 \ 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) \ lexord R" then show "(ys, xs) \ 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) \ lenlex R" and eq: "length vs = length ys" + assumes len: "(us,xs) \ lenlex R" and eq: "length vs = length ys" shows "(us @ vs, xs @ ys) \ 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) \ lenlex R \ (xs, ys) \ lenlex R" proof (induction us) case Nil - then show ?case + then show ?case by (simp add: lenlex_def) next case (Cons u us) diff -r 7fd8fb6149a6 -r dd1f5a00115f src/Tools/jEdit/jedit_main/plugin.props --- 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