# HG changeset patch # User paulson # Date 1528291630 -3600 # Node ID cada19e0c6c7a60af8a71d167ed8147c9f07660c # Parent 194fa3d2d6a4d01f9f3cde59125c466c525216be# Parent 0b71d08528f0599685d89b94b78d66d81363a273 merged diff -r 0b71d08528f0 -r cada19e0c6c7 ANNOUNCE --- a/ANNOUNCE Wed Jun 06 14:25:53 2018 +0100 +++ b/ANNOUNCE Wed Jun 06 14:27:10 2018 +0100 @@ -1,32 +1,15 @@ -Subject: Announcing Isabelle2017 +Subject: Announcing Isabelle2018 To: isabelle-users@cl.cam.ac.uk -Isabelle2017 is now available. +Isabelle2018 is now available. -This version introduces many changes over Isabelle2016-1: see the NEWS +This version introduces many changes over Isabelle2017: see the NEWS file for further details. Some notable points: -* Experimental support for Visual Studio Code as alternative PIDE front-end. - -* Improved Isabelle/jEdit Prover IDE: management of session sources -independently of editor buffers, removal of unused theories, explicit -indication of theory status, more careful auto-indentation. - -* Session-qualified theory imports. - -* Code generator improvements: support for statically embedded computations. - -* Numerous HOL library improvements. - -* More material in HOL-Algebra, HOL-Computational_Algebra and HOL-Analysis -(ported from HOL-Light). - -* Improved Nunchaku model finder, now in main HOL. - -* SQL database support in Isabelle/Scala. +* FIXME. -You may get Isabelle2017 from the following mirror sites: +You may get Isabelle2018 from the following mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle Munich (Germany) http://isabelle.in.tum.de diff -r 0b71d08528f0 -r cada19e0c6c7 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Wed Jun 06 14:25:53 2018 +0100 +++ b/Admin/components/components.sha1 Wed Jun 06 14:27:10 2018 +0100 @@ -215,6 +215,7 @@ b016a785f1f78855c00d351ff598355c3b87450f sqlite-jdbc-3.18.0-1.tar.gz b85b5bc071a59ef2a8326ceb1617d5a9a5be41cf sqlite-jdbc-3.18.0.tar.gz e56117a67ab01fb24c7fc054ede3160cefdac5f8 sqlite-jdbc-3.20.0.tar.gz +27aeac6a91353d69f0438837798ac4ae6f9ff8c5 sqlite-jdbc-3.23.1.tar.gz 8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz 2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz 1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd sumatra_pdf-2.1.1.tar.gz diff -r 0b71d08528f0 -r cada19e0c6c7 Admin/components/main --- a/Admin/components/main Wed Jun 06 14:25:53 2018 +0100 +++ b/Admin/components/main Wed Jun 06 14:27:10 2018 +0100 @@ -17,7 +17,7 @@ smbc-0.4.1 ssh-java-20161009 spass-3.8ds-1 -sqlite-jdbc-3.20.0 +sqlite-jdbc-3.23.1 verit-2016post xz-java-1.8 z3-4.4.0pre-2 diff -r 0b71d08528f0 -r cada19e0c6c7 CONTRIBUTORS --- a/CONTRIBUTORS Wed Jun 06 14:25:53 2018 +0100 +++ b/CONTRIBUTORS Wed Jun 06 14:27:10 2018 +0100 @@ -3,11 +3,11 @@ listed as an author in one of the source files of this Isabelle distribution. -Contributions to this Isabelle version --------------------------------------- +Contributions to Isabelle2018 +----------------------------- * May 2018: Manuel Eberl - Landau symbols and asymptotic equivalence (moved from the AFP) + Landau symbols and asymptotic equivalence (moved from the AFP). * May 2018: Jose Divasón (Universidad de la Rioja), Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam), @@ -22,9 +22,8 @@ Code generation with lazy evaluation semantics. * March 2018: Florian Haftmann - Abstract bit operations push_bit, take_bit, drop_bit, alongside - with an algebraic foundation for bit strings and word types in - HOL-ex. + Abstract bit operations push_bit, take_bit, drop_bit, alongside with an + algebraic foundation for bit strings and word types in HOL-ex. * March 2018: Viorel Preoteasa Generalisation of complete_distrib_lattice @@ -36,7 +35,8 @@ A new conditional parametricity prover. * October 2017: Alexander Maletzky - Derivation of axiom "iff" in HOL.thy from the other axioms. + Derivation of axiom "iff" in theory HOL.HOL from the other axioms. + Contributions to Isabelle2017 ----------------------------- diff -r 0b71d08528f0 -r cada19e0c6c7 COPYRIGHT --- a/COPYRIGHT Wed Jun 06 14:25:53 2018 +0100 +++ b/COPYRIGHT Wed Jun 06 14:27:10 2018 +0100 @@ -1,6 +1,6 @@ ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER. -Copyright (c) 1986-2017, +Copyright (c) 1986-2018, University of Cambridge, Technische Universitaet Muenchen, and contributors. diff -r 0b71d08528f0 -r cada19e0c6c7 NEWS --- a/NEWS Wed Jun 06 14:25:53 2018 +0100 +++ b/NEWS Wed Jun 06 14:27:10 2018 +0100 @@ -4,11 +4,21 @@ (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) -New in this Isabelle version ----------------------------- +New in Isabelle2018 (August 2018) +--------------------------------- *** General *** +* Session-qualified theory names are mandatory: it is no longer possible +to refer to unqualified theories from the parent session. +INCOMPATIBILITY for old developments that have not been updated to +Isabelle2017 yet (using the "isabelle imports" tool). + +* Only the most fundamental theory names are global, usually the entry +points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL, +FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for +formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK". + * Marginal comments need to be written exclusively in the new-style form "\ \text\", old ASCII variants like "-- {* ... *}" are no longer supported. INCOMPATIBILITY, use the command-line tool "isabelle @@ -29,23 +39,9 @@ In case you want to exclude conversion of ML files (because the tool frequently also converts ML's "op" syntax), use option "-m". -* The old 'def' command has been discontinued (legacy since -Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with -object-logic equality or equivalence. - -* Session-qualified theory names are mandatory: it is no longer possible -to refer to unqualified theories from the parent session. -INCOMPATIBILITY for old developments that have not been updated to -Isabelle2017 yet (using the "isabelle imports" tool). - * Theory header 'abbrevs' specifications need to be separated by 'and'. INCOMPATIBILITY. -* Only the most fundamental theory names are global, usually the entry -points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL, -FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for -formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK". - * Command 'external_file' declares the formal dependency on the given file name, such that the Isabelle build process knows about it, but without specific Prover IDE management. @@ -64,13 +60,45 @@ * The command 'display_drafts' has been discontinued. INCOMPATIBILITY, use action "isabelle.draft" (or "print") in Isabelle/jEdit instead. -* Isabelle symbol "\" is rendered as explicit Unicode hyphen U+2010, to -avoid unclear meaning of the old "soft hyphen" U+00AD. Rare -INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML output. +* In HTML output, the Isabelle symbol "\" is rendered as explicit +Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen" +U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML +output. *** Isabelle/jEdit Prover IDE *** +* The command-line tool "isabelle jedit" provides more flexible options +for session management: + + - option -R builds an auxiliary logic image with all required theories + from other sessions, relative to an ancestor session given by option + -A (default: parent) + + - option -S is like -R, with a focus on the selected session and its + descendants (this reduces startup time for big projects like AFP) + + Examples: + isabelle jedit -R HOL-Number_Theory + isabelle jedit -R HOL-Number_Theory -A HOL + isabelle jedit -d '$AFP' -S Formal_SSA -A HOL + isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis + +* PIDE markup for session ROOT files: allows to complete session names, +follow links to theories and document files etc. + +* Completion supports theory header imports, using theory base name. +E.g. "Prob" may be completed to "HOL-Probability.Probability". + +* Named control symbols (without special Unicode rendering) are shown as +bold-italic keyword. This is particularly useful for the short form of +antiquotations with control symbol: \<^name>\argument\. The action +"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1 +arguments into this format. + +* Completion provides templates for named symbols with arguments, +e.g. "\ \ARGUMENT\" or "\<^emph>\ARGUMENT\". + * Slightly more parallel checking, notably for high priority print functions (e.g. State output). @@ -82,37 +110,6 @@ supersede former "spell_checker_elements" to determine regions of text that are subject to spell-checking. Minor INCOMPATIBILITY. -* PIDE markup for session ROOT files: allows to complete session names, -follow links to theories and document files etc. - -* Completion supports theory header imports, using theory base name. -E.g. "Prob" may be completed to "HOL-Probability.Probability". - -* The command-line tool "isabelle jedit" provides more flexible options -for session management: - - option -R builds an auxiliary logic image with all required theories - from other sessions, relative to an ancestor session given by option - -A (default: parent) - - option -S is like -R, with a focus on the selected session and its - descendants (this reduces startup time for big projects like AFP) - - Examples: - isabelle jedit -R HOL-Number_Theory - isabelle jedit -R HOL-Number_Theory -A HOL - isabelle jedit -d '$AFP' -S Formal_SSA -A HOL - isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis - -* Named control symbols (without special Unicode rendering) are shown as -bold-italic keyword. This is particularly useful for the short form of -antiquotations with control symbol: \<^name>\argument\. The action -"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1 -arguments into this format. - -* Completion provides templates for named symbols with arguments, -e.g. "\ \ARGUMENT\" or "\<^emph>\ARGUMENT\". - -* Bibtex database files (.bib) are semantically checked. - * Action "isabelle.preview" is able to present more file formats, notably bibtex database files and ML files. @@ -120,6 +117,8 @@ plain-text document draft. Both are available via the menu "Plugins / Isabelle". +* Bibtex database files (.bib) are semantically checked. + * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle is only used if there is no conflict with existing Unicode sequences in the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle @@ -163,19 +162,23 @@ antiquotations in control symbol notation, e.g. \<^const_name> becomes \isactrlconstUNDERSCOREname. -* Document antiquotation @{cite} now checks the given Bibtex entries -against the Bibtex database files -- only in batch-mode session builds. +* Document preparation with skip_proofs option now preserves the content +more accurately: only terminal proof steps ('by' etc.) are skipped. * Document antiquotation @{session name} checks and prints the given session name verbatim. -* Document preparation with skip_proofs option now preserves the content -more accurately: only terminal proof steps ('by' etc.) are skipped. +* Document antiquotation @{cite} now checks the given Bibtex entries +against the Bibtex database files -- only in batch-mode session builds. * Command-line tool "isabelle document" has been re-implemented in Isabelle/Scala, with simplified arguments and explicit errors from the latex and bibtex process. Minor INCOMPATIBILITY. +* Session ROOT entry: empty 'document_files' means there is no document +for this session. There is no need to specify options [document = false] +anymore. + *** Isar *** @@ -185,13 +188,17 @@ Rare INCOMPATIBILITY, need to refer to explicitly named facts instead (e.g. use 'find_theorems' or 'try' to figure this out). +* The old 'def' command has been discontinued (legacy since +Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with +object-logic equality or equivalence. + * Rewrites clauses (keyword 'rewrites') were moved into the locale -expression syntax, where they are part of locale instances. In -interpretation commands rewrites clauses now need to occur before -'for' and 'defines'. Minor INCOMPATIBILITY. - -* For rewrites clauses, if activating a locale instance fails, fall -back to reading the clause first. This helps avoid qualification of +expression syntax, where they are part of locale instances. In +interpretation commands rewrites clauses now need to occur before 'for' +and 'defines'. Minor INCOMPATIBILITY. + +* For 'rewrites' clauses, if activating a locale instance fails, fall +back to reading the clause first. This helps avoid qualification of locale instances where the qualifier's sole purpose is avoiding duplicate constant declarations. @@ -204,54 +211,55 @@ *** HOL *** -* Landau_Symbols from the AFP was moved to HOL-Library - * Clarified relationship of characters, strings and code generation: - * Type "char" is now a proper datatype of 8-bit values. - - * Conversions "nat_of_char" and "char_of_nat" are gone; use more - general conversions "of_char" and "char_of" with suitable - type constraints instead. - - * The zero character is just written "CHR 0x00", not - "0" any longer. - - * Type "String.literal" (for code generation) is now isomorphic - to lists of 7-bit (ASCII) values; concrete values can be written - as "STR ''...''" for sequences of printable characters and - "STR 0x..." for one single ASCII code point given - as hexadecimal numeral. - - * Type "String.literal" supports concatenation "... + ..." - for all standard target languages. - - * Theory Library/Code_Char is gone; study the explanations concerning - "String.literal" in the tutorial on code generation to get an idea - how target-language string literals can be converted to HOL string - values and vice versa. - - * Imperative-HOL: operation "raise" directly takes a value of type - "String.literal" as argument, not type "string". - -INCOMPATIBILITY. - -* Abstract bit operations as part of Main: push_bit, take_bit, -drop_bit. - -* New, more general, axiomatization of complete_distrib_lattice. -The former axioms: -"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)" -are replaced by -"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \ A . f Y \ Y)})" -The instantiations of sets and functions as complete_distrib_lattice -are moved to Hilbert_Choice.thy because their proofs need the Hilbert -choice operator. The dual of this property is also proved in -Hilbert_Choice.thy. + - Type "char" is now a proper datatype of 8-bit values. + + - Conversions "nat_of_char" and "char_of_nat" are gone; use more + general conversions "of_char" and "char_of" with suitable type + constraints instead. + + - The zero character is just written "CHR 0x00", not "0" any longer. + + - Type "String.literal" (for code generation) is now isomorphic to + lists of 7-bit (ASCII) values; concrete values can be written as + "STR ''...''" for sequences of printable characters and "STR 0x..." + for one single ASCII code point given as hexadecimal numeral. + + - Type "String.literal" supports concatenation "... + ..." for all + standard target languages. + + - Theory HOL-Library.Code_Char is gone; study the explanations + concerning "String.literal" in the tutorial on code generation to + get an idea how target-language string literals can be converted to + HOL string values and vice versa. + + - Session Imperative-HOL: operation "raise" directly takes a value of + type "String.literal" as argument, not type "string". + +INCOMPATIBILITY. + +* Code generation: Code generation takes an explicit option +"case_insensitive" to accomodate case-insensitive file systems. + +* Abstract bit operations as part of Main: push_bit, take_bit, drop_bit. + +* New, more general, axiomatization of complete_distrib_lattice. The +former axioms: + + "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)" + +are replaced by: + + "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \ A . f Y \ Y)})" + +The instantiations of sets and functions as complete_distrib_lattice are +moved to Hilbert_Choice.thy because their proofs need the Hilbert choice +operator. The dual of this property is also proved in theory +HOL.Hilbert_Choice. * New syntax for the minimum/maximum of a function over a finite set: -MIN x\A. B and even MIN x. B (only useful for finite types), also -MAX. +MIN x\A. B and even MIN x. B (only useful for finite types), also MAX. * Clarifed theorem names: @@ -260,83 +268,59 @@ Minor INCOMPATIBILITY. -* A new command parametric_constant for proving parametricity of -non-recursive definitions. For constants that are not fully parametric -the command will infer conditions on relations (e.g., bi_unique, -bi_total, or type class conditions such as "respects 0") sufficient for -parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for -some examples. - -* A new preprocessor for the code generator to generate code for algebraic - types with lazy evaluation semantics even in call-by-value target languages. - See theory HOL-Library.Code_Lazy for the implementation and - HOL-Codegenerator_Test.Code_Lazy_Test for examples. - * SMT module: + - The 'smt_oracle' option is now necessary when using the 'smt' method with a solver other than Z3. INCOMPATIBILITY. + - The encoding to first-order logic is now more complete in the presence of higher-order quantifiers. An 'smt_explicit_application' option has been added to control this. INCOMPATIBILITY. -* Datatypes: - - The legacy command 'old_datatype', provided by - '~~/src/HOL/Library/Old_Datatype.thy', has been removed. INCOMPATIBILITY. - -* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide -instances of rat, real, complex as factorial rings etc. Import -HOL-Computational_Algebra.Field_as_Ring explicitly in case of need. -INCOMPATIBILITY. - * Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on interpretation of abstract locales. INCOMPATIBILITY. +* Predicate coprime is now a real definition, not a mere abbreviation. +INCOMPATIBILITY. + * Predicate pairwise_coprime abolished, use "pairwise coprime" instead. INCOMPATIBILITY. * The relator rel_filter on filters has been strengthened to its -canonical categorical definition with better properties. INCOMPATIBILITY. +canonical categorical definition with better properties. +INCOMPATIBILITY. * Generalized linear algebra involving linear, span, dependent, dim from type class real_vector to locales module and vector_space. Renamed: - - span_inc ~> span_superset - - span_superset ~> span_base - - span_eq ~> span_eq_iff -INCOMPATIBILITY. - -* HOL-Algebra: renamed (^) to [^] - -* Session HOL-Analysis: infinite products, Moebius functions, the Riemann mapping -theorem, the Vitali covering theorem, change-of-variables results for -integration and measures. + + span_inc ~> span_superset + span_superset ~> span_base + span_eq ~> span_eq_iff + +INCOMPATIBILITY. * Class linordered_semiring_1 covers zero_less_one also, ruling out pathologic instances. Minor INCOMPATIBILITY. -* Theory List: functions "sorted_wrt" and "sorted" now compare every - element in a list to all following elements, not just the next one. - -* Theory List: Synatx: - - filter-syntax "[x <- xs. P]" is no longer output syntax - but only input syntax. - - list comprehension syntax now supports tuple patterns in "pat <- xs". +* Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every +element in a list to all following elements, not just the next one. + +* Theory HOL.List syntax: + + - filter-syntax "[x <- xs. P]" is no longer output syntax, but only + input syntax + + - list comprehension syntax now supports tuple patterns in "pat <- xs" * Removed nat-int transfer machinery. Rare INCOMPATIBILITY. -* Predicate coprime is now a real definition, not a mere -abbreviation. INCOMPATIBILITY. - -* Code generation: Code generation takes an explicit option -"case_insensitive" to accomodate case-insensitive file systems. - * Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid clash with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY. * Eliminated some theorem aliasses: - even_times_iff ~> even_mult_iff mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1 even_of_nat ~> even_int_iff @@ -344,18 +328,48 @@ INCOMPATIBILITY. * Eliminated some theorem duplicate variations: - * dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0. - * mod_Suc_eq_Suc_mod can be replaced by mod_Suc. - * mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps. - * mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def. - * The witness of mod_eqD can be given directly as "_ div _". + + - dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0 + - mod_Suc_eq_Suc_mod can be replaced by mod_Suc + - mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps + - mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def + - the witness of mod_eqD can be given directly as "_ div _" INCOMPATIBILITY. * Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no -longer aggresively destroyed to "?q. m = d * q". INCOMPATIBILITY, -adding "elim!: dvd" to classical proof methods in most situations -restores broken proofs. +longer aggresively destroyed to "\q. m = d * q". INCOMPATIBILITY, adding +"elim!: dvd" to classical proof methods in most situations restores +broken proofs. + +* Theory HOL-Library.Conditional_Parametricity provides command +'parametric_constant' for proving parametricity of non-recursive +definitions. For constants that are not fully parametric the command +will infer conditions on relations (e.g., bi_unique, bi_total, or type +class conditions such as "respects 0") sufficient for parametricity. See +theory HOL-ex.Conditional_Parametricity_Examples for some examples. + +* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code +generator to generate code for algebraic types with lazy evaluation +semantics even in call-by-value target languages. See theory +HOL-Codegenerator_Test.Code_Lazy_Test for some examples. + +* Theory HOL-Library.Landau_Symbols has been moved here from AFP. + +* Theory HOL-Library.Old_Datatype no longer provides the legacy command +'old_datatype'. INCOMPATIBILITY. + +* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide +instances of rat, real, complex as factorial rings etc. Import +HOL-Computational_Algebra.Field_as_Ring explicitly in case of need. +INCOMPATIBILITY. + +* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new +infix/prefix notation. + +* Session HOL-Analysis: infinite products, Moebius functions, the +Riemann mapping theorem, the Vitali covering theorem, +change-of-variables results for integration and measures. *** ML *** @@ -371,47 +385,12 @@ *** System *** -* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued: -heap images and session databases are always stored in -$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or -$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or -"isabelle jedit -s" or "isabelle build -s"). - -* The command-line tool "export" and 'export_files' in session ROOT -entries retrieve theory exports from the session build database. - -* The command-line tools "isabelle server" and "isabelle client" provide -access to the Isabelle Server: it supports responsive session management -and concurrent use of theories, based on Isabelle/PIDE infrastructure. -See also the "system" manual. - -* The command-line tool "dump" dumps information from the cumulative -PIDE session database: many sessions may be loaded into a given logic -image, results from all loaded theories are written to the output -directory. - -* The command-line tool "isabelle update_comments" normalizes formal -comments in outer syntax as follows: \ \text\ (whith a single space to -approximate the appearance in document output). This is more specific -than former "isabelle update_cartouches -c": the latter tool option has -been discontinued. - -* Session ROOT entry: empty 'document_files' means there is no document -for this session. There is no need to specify options [document = false] -anymore. - -* The command-line tool "isabelle mkroot" now always produces a document -outline: its options have been adapted accordingly. INCOMPATIBILITY. - -* The command-line tool "isabelle mkroot -I" initializes a Mercurial -repository for the generated session files. - -* Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform -support has been discontinued. - * Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no longer supported. +* Linux and Windows/Cygwin is for x86_64 only, old 32bit platform +support has been discontinued. + * Java runtime is for x86_64 only. Corresponding Isabelle settings have been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS, instead of former 32/64 variants. INCOMPATIBILITY. @@ -439,17 +418,46 @@ corresponding environment values into account, when determining the up-to-date status of a session. +* The command-line tool "dump" dumps information from the cumulative +PIDE session database: many sessions may be loaded into a given logic +image, results from all loaded theories are written to the output +directory. + * Command-line tool "isabelle imports -I" also reports actual session imports. This helps to minimize the session dependency graph. -* Update to current Poly/ML 5.7.1 with slightly improved performance and -PIDE markup for identifier bindings. +* The command-line tool "export" and 'export_files' in session ROOT +entries retrieve theory exports from the session build database. + +* The command-line tools "isabelle server" and "isabelle client" provide +access to the Isabelle Server: it supports responsive session management +and concurrent use of theories, based on Isabelle/PIDE infrastructure. +See also the "system" manual. + +* The command-line tool "isabelle update_comments" normalizes formal +comments in outer syntax as follows: \ \text\ (whith a single space to +approximate the appearance in document output). This is more specific +than former "isabelle update_cartouches -c": the latter tool option has +been discontinued. + +* The command-line tool "isabelle mkroot" now always produces a document +outline: its options have been adapted accordingly. INCOMPATIBILITY. + +* The command-line tool "isabelle mkroot -I" initializes a Mercurial +repository for the generated session files. + +* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued: +heap images and session databases are always stored in +$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or +$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or +"isabelle jedit -s" or "isabelle build -s"). * ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific options for improved error reporting. Potential INCOMPATIBILITY with unusual LaTeX installations, may have to adapt these settings. -* The bundled Poly/ML 5.7.1 now uses The GNU Multiple Precision +* Update to Poly/ML 5.7.1 with slightly improved performance and PIDE +markup for identifier bindings. It now uses The GNU Multiple Precision Arithmetic Library (libgmp) on all platforms, notably Mac OS X with 32/64 bit. diff -r 0b71d08528f0 -r cada19e0c6c7 etc/settings --- a/etc/settings Wed Jun 06 14:25:53 2018 +0100 +++ b/etc/settings Wed Jun 06 14:27:10 2018 +0100 @@ -134,5 +134,8 @@ ISABELLE_GNUPLOT="gnuplot" #ISABELLE_GHC="/usr/bin/ghc" +#ISABELLE_MLTON="/usr/bin/mlton" #ISABELLE_OCAML="/usr/bin/ocaml" +#ISABELLE_OCAMLC="/usr/bin/ocamlc" +#ISABELLE_SMLNJ="/usr/bin/sml" #ISABELLE_SWIPL="/usr/bin/swipl" diff -r 0b71d08528f0 -r cada19e0c6c7 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/Doc/JEdit/JEdit.thy Wed Jun 06 14:27:10 2018 +0100 @@ -305,7 +305,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>\Isabelle2017\). Thus @{tool jedit_client} can connect to the + name (e.g.\ \<^verbatim>\Isabelle2018\). 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 0b71d08528f0 -r cada19e0c6c7 src/Doc/System/Environment.thy --- a/src/Doc/System/Environment.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/Doc/System/Environment.thy Wed Jun 06 14:27:10 2018 +0100 @@ -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/Isabelle2017\. + usually to something like \<^verbatim>\$USER_HOME/.isabelle/Isabelle2018\. Thus individual users may override the site-wide defaults. Typically, a user settings file contains only a few lines, with some assignments that @@ -149,7 +149,7 @@ of the @{executable isabelle} executable. \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\\<^sup>*\] refers to the name of this - Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2017\''. + Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2018\''. \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\\<^sup>*\] diff -r 0b71d08528f0 -r cada19e0c6c7 src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/Doc/System/Misc.thy Wed Jun 06 14:27:10 2018 +0100 @@ -220,7 +220,7 @@ \<^medskip> The default is to output the full version string of the Isabelle - distribution, e.g.\ ``\<^verbatim>\Isabelle2017: October 2017\. + distribution, e.g.\ ``\<^verbatim>\Isabelle2018: August 2018\. The \<^verbatim>\-i\ option produces a short identification derived from the Mercurial id of the @{setting ISABELLE_HOME} directory. diff -r 0b71d08528f0 -r cada19e0c6c7 src/Doc/Tutorial/Inductive/AB.thy --- a/src/Doc/Tutorial/Inductive/AB.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/Doc/Tutorial/Inductive/AB.thy Wed Jun 06 14:27:10 2018 +0100 @@ -64,13 +64,15 @@ \ lemma correctness: - "(w \ S \ size(filter (\x. x=a) w) = size(filter (\x. x=b) w)) \ - (w \ A \ size(filter (\x. x=a) w) = size(filter (\x. x=b) w) + 1) \ - (w \ B \ size(filter (\x. x=b) w) = size(filter (\x. x=a) w) + 1)" + "(w \ S \ size[x\w. x=a] = size[x\w. x=b]) \ + (w \ A \ size[x\w. x=a] = size[x\w. x=b] + 1) \ + (w \ B \ size[x\w. x=b] = size[x\w. x=a] + 1)" txt\\noindent These propositions are expressed with the help of the predefined @{term -filter} function on lists. Remember that on lists @{text size} and @{text length} are synonymous. +filter} function on lists, which has the convenient syntax @{text"[x\xs. P +x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"} +holds. Remember that on lists @{text size} and @{text length} are synonymous. The proof itself is by rule induction and afterwards automatic: \ @@ -110,8 +112,8 @@ \ lemma step1: "\i < size w. - \(int(size(filter P (take (i+1) w)))-int(size(filter (\x. \P x) (take (i+1) w)))) - - (int(size(filter P (take i w)))-int(size(filter (\x. \P x) (take i w))))\ \ 1" + \(int(size[x\take (i+1) w. P x])-int(size[x\take (i+1) w. \P x])) + - (int(size[x\take i w. P x])-int(size[x\take i w. \P x]))\ \ 1" txt\\noindent The lemma is a bit hard to read because of the coercion function @@ -135,8 +137,8 @@ \ lemma part1: - "size(filter P w) = size(filter (\x. \P x) w)+2 \ - \i\size w. size(filter P (take i w)) = size(filter (\x. \P x) (take i w))+1" + "size[x\w. P x] = size[x\w. \P x]+2 \ + \i\size w. size[x\take i w. P x] = size[x\take i w. \P x]+1" txt\\noindent This is proved by @{text force} with the help of the intermediate value theorem, @@ -155,10 +157,10 @@ lemma part2: - "\size(filter P (take i w @ drop i w)) = - size(filter (\x. \P x) (take i w @ drop i w))+2; - size(filter P (take i w)) = size(filter (\x. \P x) (take i w))+1\ - \ size(filter P (drop i w)) = size(filter (\x. \P x) (drop i w))+1" + "\size[x\take i w @ drop i w. P x] = + size[x\take i w @ drop i w. \P x]+2; + size[x\take i w. P x] = size[x\take i w. \P x]+1\ + \ size[x\drop i w. P x] = size[x\drop i w. \P x]+1" by(simp del: append_take_drop_id) text\\noindent @@ -185,9 +187,9 @@ \ theorem completeness: - "(size(filter (\x. x=a) w) = size(filter (\x. x=b) w) \ w \ S) \ - (size(filter (\x. x=a) w) = size(filter (\x. x=b) w) + 1 \ w \ A) \ - (size(filter (\x. x=b) w) = size(filter (\x. x=a) w) + 1 \ w \ B)" + "(size[x\w. x=a] = size[x\w. x=b] \ w \ S) \ + (size[x\w. x=a] = size[x\w. x=b] + 1 \ w \ A) \ + (size[x\w. x=b] = size[x\w. x=a] + 1 \ w \ B)" txt\\noindent The proof is by induction on @{term w}. Structural induction would fail here @@ -232,9 +234,9 @@ apply(clarify) txt\\noindent This yields an index @{prop"i \ length v"} such that -@{prop[display]"length (filter (\x. x=a) (take i v)) = length (filter (\x. x=b) (take i v)) + 1"} +@{prop[display]"length [x\take i v . x = a] = length [x\take i v . x = b] + 1"} With the help of @{thm[source]part2} it follows that -@{prop[display]"length (filter (\x. x=a) (drop i v)) = length (filter (\x. x=b) (drop i v)) + 1"} +@{prop[display]"length [x\drop i v . x = a] = length [x\drop i v . x = b] + 1"} \ apply(drule part2[of "\x. x=a", simplified]) diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/HOLCF/Cfun.thy Wed Jun 06 14:27:10 2018 +0100 @@ -394,7 +394,7 @@ lemma flat_codom: "f\x = c \ f\\ = \ \ (\z. f\z = c)" for c :: "'b::flat" - apply (case_tac "f\x = \") + apply (cases "f\x = \") apply (rule disjI1) apply (rule bottomI) apply (erule_tac t="\" in subst) diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/HOLCF/Completion.thy --- a/src/HOL/HOLCF/Completion.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/HOLCF/Completion.thy Wed Jun 06 14:27:10 2018 +0100 @@ -41,13 +41,13 @@ unfolding ideal_def by fast lemma ideal_principal: "ideal {x. x \ z}" -apply (rule idealI) -apply (rule_tac x=z in exI) -apply (fast intro: r_refl) -apply (rule_tac x=z in bexI, fast) -apply (fast intro: r_refl) -apply (fast intro: r_trans) -done + apply (rule idealI) + apply (rule exI [where x = z]) + apply (fast intro: r_refl) + apply (rule bexI [where x = z], fast) + apply (fast intro: r_refl) + apply (fast intro: r_trans) + done lemma ex_ideal: "\A. A \ {A. ideal A}" by (fast intro: ideal_principal) @@ -59,17 +59,19 @@ assumes ideal_A: "\i. ideal (A i)" assumes chain_A: "\i j. i \ j \ A i \ A j" shows "ideal (\i. A i)" - apply (rule idealI) - apply (cut_tac idealD1 [OF ideal_A], fast) - apply (clarify, rename_tac i j) - apply (drule subsetD [OF chain_A [OF max.cobounded1]]) - apply (drule subsetD [OF chain_A [OF max.cobounded2]]) - apply (drule (1) idealD2 [OF ideal_A]) - apply blast - apply clarify - apply (drule (1) idealD3 [OF ideal_A]) - apply fast -done + apply (rule idealI) + using idealD1 [OF ideal_A] apply fast + apply (clarify) + subgoal for i j + apply (drule subsetD [OF chain_A [OF max.cobounded1]]) + apply (drule subsetD [OF chain_A [OF max.cobounded2]]) + apply (drule (1) idealD2 [OF ideal_A]) + apply blast + done + apply clarify + apply (drule (1) idealD3 [OF ideal_A]) + apply fast + done lemma typedef_ideal_po: fixes Abs :: "'a set \ 'b::below" @@ -208,10 +210,10 @@ have a_mem: "enum a \ rep x" unfolding a_def apply (rule LeastI_ex) - apply (cut_tac ideal_rep [of x]) + apply (insert ideal_rep [of x]) apply (drule idealD1) - apply (clarify, rename_tac a) - apply (rule_tac x="count a" in exI, simp) + apply (clarify) + subgoal for a by (rule exI [where x="count a"]) simp done have b: "\i. P i \ enum i \ rep x \ enum (b i) \ rep x \ \ enum (b i) \ enum i" @@ -220,50 +222,63 @@ \ enum (c i j) \ rep x \ enum i \ enum (c i j) \ enum j \ enum (c i j)" unfolding c_def apply (drule (1) idealD2 [OF ideal_rep], clarify) - apply (rule_tac a="count z" in LeastI2, simp, simp) + subgoal for \ z by (rule LeastI2 [where a="count z"], simp, simp) done - have X_mem: "\n. enum (X n) \ rep x" - apply (induct_tac n) - apply (simp add: X_0 a_mem) - apply (clarsimp simp add: X_Suc, rename_tac n) - apply (simp add: b c) - done + have X_mem: "enum (X n) \ rep x" for n + proof (induct n) + case 0 + then show ?case by (simp add: X_0 a_mem) + next + case (Suc n) + with b c show ?case by (auto simp: X_Suc) + qed have X_chain: "\n. enum (X n) \ enum (X (Suc n))" apply (clarsimp simp add: X_Suc r_refl) apply (simp add: b c X_mem) done have less_b: "\n i. n < b i \ enum n \ rep x \ enum n \ enum i" unfolding b_def by (drule not_less_Least, simp) - have X_covers: "\n. \k\n. enum k \ rep x \ enum k \ enum (X n)" - apply (induct_tac n) - apply (clarsimp simp add: X_0 a_def) - apply (drule_tac k=0 in Least_le, simp add: r_refl) - apply (clarsimp, rename_tac n k) - apply (erule le_SucE) - apply (rule r_trans [OF _ X_chain], simp) - apply (case_tac "P (X n)", simp add: X_Suc) - apply (rule_tac x="b (X n)" and y="Suc n" in linorder_cases) - apply (simp only: less_Suc_eq_le) - apply (drule spec, drule (1) mp, simp add: b X_mem) - apply (simp add: c X_mem) - apply (drule (1) less_b) - apply (erule r_trans) - apply (simp add: b c X_mem) - apply (simp add: X_Suc) - apply (simp add: P_def) - done + have X_covers: "\k\n. enum k \ rep x \ enum k \ enum (X n)" for n + proof (induct n) + case 0 + then show ?case + apply (clarsimp simp add: X_0 a_def) + apply (drule Least_le [where k=0], simp add: r_refl) + done + next + case (Suc n) + then show ?case + apply clarsimp + apply (erule le_SucE) + apply (rule r_trans [OF _ X_chain], simp) + apply (cases "P (X n)", simp add: X_Suc) + apply (rule linorder_cases [where x="b (X n)" and y="Suc n"]) + apply (simp only: less_Suc_eq_le) + apply (drule spec, drule (1) mp, simp add: b X_mem) + apply (simp add: c X_mem) + apply (drule (1) less_b) + apply (erule r_trans) + apply (simp add: b c X_mem) + apply (simp add: X_Suc) + apply (simp add: P_def) + done + qed have 1: "\i. enum (X i) \ enum (X (Suc i))" by (simp add: X_chain) - have 2: "x = (\n. principal (enum (X n)))" + have "x = (\n. principal (enum (X n)))" apply (simp add: eq_iff rep_lub 1 rep_principal) - apply (auto, rename_tac a) - apply (subgoal_tac "\i. a = enum i", erule exE) - apply (rule_tac x=i in exI, simp add: X_covers) - apply (rule_tac x="count a" in exI, simp) - apply (erule idealD3 [OF ideal_rep]) - apply (rule X_mem) + apply auto + subgoal for a + apply (subgoal_tac "\i. a = enum i", erule exE) + apply (rule_tac x=i in exI, simp add: X_covers) + apply (rule_tac x="count a" in exI, simp) + done + subgoal + apply (erule idealD3 [OF ideal_rep]) + apply (rule X_mem) + done done - from 1 2 show ?thesis .. + with 1 show ?thesis .. qed lemma principal_induct: @@ -301,16 +316,20 @@ by (simp add: x rep_lub Y rep_principal) have "f ` rep x <<| (\n. f (Y n))" apply (rule is_lubI) - apply (rule ub_imageI, rename_tac a) - apply (clarsimp simp add: rep_x) - apply (drule f_mono) - apply (erule below_lub [OF chain]) + apply (rule ub_imageI) + subgoal for a + apply (clarsimp simp add: rep_x) + apply (drule f_mono) + apply (erule below_lub [OF chain]) + done apply (rule lub_below [OF chain]) - apply (drule_tac x="Y n" in ub_imageD) - apply (simp add: rep_x, fast intro: r_refl) - apply assumption + subgoal for \ n + apply (drule ub_imageD [where x="Y n"]) + apply (simp add: rep_x, fast intro: r_refl) + apply assumption + done done - thus ?thesis .. + then show ?thesis .. qed lemma extension_beta: @@ -353,16 +372,18 @@ assumes g_mono: "\a b. a \ b \ g a \ g b" assumes below: "\a. f a \ g a" shows "extension f \ extension g" - apply (rule cfun_belowI) - apply (simp only: extension_beta f_mono g_mono) - apply (rule is_lub_thelub_ex) - apply (rule extension_lemma, erule f_mono) - apply (rule ub_imageI, rename_tac a) - apply (rule below_trans [OF below]) - apply (rule is_ub_thelub_ex) - apply (rule extension_lemma, erule g_mono) - apply (erule imageI) -done + apply (rule cfun_belowI) + apply (simp only: extension_beta f_mono g_mono) + apply (rule is_lub_thelub_ex) + apply (rule extension_lemma, erule f_mono) + apply (rule ub_imageI) + subgoal for x a + apply (rule below_trans [OF below]) + apply (rule is_ub_thelub_ex) + apply (rule extension_lemma, erule g_mono) + apply (erule imageI) + done + done lemma cont_extension: assumes f_mono: "\a b x. a \ b \ f x a \ f x b" diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/HOLCF/Domain_Aux.thy --- a/src/HOL/HOLCF/Domain_Aux.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/HOLCF/Domain_Aux.thy Wed Jun 06 14:27:10 2018 +0100 @@ -199,32 +199,40 @@ assumes f: "decisive f" assumes g: "decisive g" shows "decisive (ssum_map\f\g)" -apply (rule decisiveI, rename_tac s) -apply (case_tac s, simp_all) -apply (rule_tac x=x in decisive_cases [OF f], simp_all) -apply (rule_tac x=y in decisive_cases [OF g], simp_all) -done + apply (rule decisiveI) + subgoal for s + apply (cases s, simp_all) + apply (rule_tac x=x in decisive_cases [OF f], simp_all) + apply (rule_tac x=y in decisive_cases [OF g], simp_all) + done + done lemma decisive_sprod_map: assumes f: "decisive f" assumes g: "decisive g" shows "decisive (sprod_map\f\g)" -apply (rule decisiveI, rename_tac s) -apply (case_tac s, simp_all) -apply (rule_tac x=x in decisive_cases [OF f], simp_all) -apply (rule_tac x=y in decisive_cases [OF g], simp_all) -done + apply (rule decisiveI) + subgoal for s + apply (cases s, simp) + subgoal for x y + apply (rule decisive_cases [OF f, where x = x], simp_all) + apply (rule decisive_cases [OF g, where x = y], simp_all) + done + done + done lemma decisive_abs_rep: fixes abs rep assumes iso: "iso abs rep" assumes d: "decisive d" shows "decisive (abs oo d oo rep)" -apply (rule decisiveI) -apply (rule_tac x="rep\x" in decisive_cases [OF d]) -apply (simp add: iso.rep_iso [OF iso]) -apply (simp add: iso.abs_strict [OF iso]) -done + apply (rule decisiveI) + subgoal for s + apply (rule decisive_cases [OF d, where x="rep\s"]) + apply (simp add: iso.rep_iso [OF iso]) + apply (simp add: iso.abs_strict [OF iso]) + done + done lemma lub_ID_finite: assumes chain: "chain d" diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Library/AList.thy --- a/src/HOL/Library/AList.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Library/AList.thy Wed Jun 06 14:27:10 2018 +0100 @@ -45,7 +45,7 @@ using assms by (simp add: update_keys) lemma update_filter: - "a \ k \ update k v (filter (\q. fst q \ a) ps) = filter (\q. fst q \ a) (update k v ps)" + "a \ k \ update k v [q\ps. fst q \ a] = [q\update k v ps. fst q \ a]" by (induct ps) auto lemma update_triv: "map_of al k = Some v \ update k v al = al" @@ -361,12 +361,12 @@ proof - have "y \ x \ x \ y" for y by auto - then show "filter (\p. fst p \ D \ x \ fst p) al = filter (\p. fst p \ D \ fst p \ x) al" + then show "[p \ al. fst p \ D \ x \ fst p] = [p \ al. fst p \ D \ fst p \ x]" by simp assume "x \ D" then have "y \ D \ y \ D \ x \ y" for y by auto - then show "filter (\p. fst p \ D \ x \ fst p) al = filter (\p. fst p \ D) al" + then show "[p \ al . fst p \ D \ x \ fst p] = [p \ al . fst p \ D]" by simp qed @@ -492,7 +492,7 @@ lemma distinct_map_ran: "distinct (map fst al) \ distinct (map fst (map_ran f al))" by (simp add: map_ran_def split_def comp_def) -lemma map_ran_filter: "map_ran f (filter (\p. fst p \ a) ps) = filter (\p. fst p \ a) (map_ran f ps)" +lemma map_ran_filter: "map_ran f [p\ps. fst p \ a] = [p\map_ran f ps. fst p \ a]" by (simp add: map_ran_def filter_map split_def comp_def) lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)" diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Library/Code_Lazy.thy --- a/src/HOL/Library/Code_Lazy.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Library/Code_Lazy.thy Wed Jun 06 14:27:10 2018 +0100 @@ -17,7 +17,7 @@ text \ This theory and the CodeLazy tool described in @{cite "LochbihlerStoop2018"}. - It hooks into Isabelle’s code generator such that the generated code evaluates a user-specified + It hooks into Isabelle's code generator such that the generated code evaluates a user-specified set of type constructors lazily, even in target languages with eager evaluation. The lazy type must be algebraic, i.e., values must be built from constructors and a corresponding case operator decomposes them. Every datatype and codatatype is algebraic diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Library/Finite_Map.thy --- a/src/HOL/Library/Finite_Map.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Library/Finite_Map.thy Wed Jun 06 14:27:10 2018 +0100 @@ -84,10 +84,10 @@ definition map_filter :: "('a \ bool) \ ('a \ 'b) \ ('a \ 'b)" where "map_filter P m = (\x. if P x then m x else None)" -lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of (filter (\(k, _). P k) m)" +lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \ m. P k]" proof fix x - show "map_filter P (map_of m) x = map_of (filter (\(k, _). P k) m) x" + show "map_filter P (map_of m) x = map_of [(k, _) \ m. P k] x" by (induct m) (auto simp: map_filter_def) qed diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Library/Multiset.thy Wed Jun 06 14:27:10 2018 +0100 @@ -1888,7 +1888,7 @@ apply simp done -lemma mset_compl_union [simp]: "mset (filter P xs) + mset (filter (\x. \P x) xs) = mset xs" +lemma mset_compl_union [simp]: "mset [x\xs. P x] + mset [x\xs. \P x] = mset xs" by (induct xs) auto lemma nth_mem_mset: "i < length ls \ (ls ! i) \# mset ls" @@ -2582,14 +2582,14 @@ show "mset ys = mset xs" by simp from \sorted (map f ys)\ show "sorted (map f ys)" . - show "filter (\x. f k = f x) ys = filter (\x. f k = f x) xs" if "k \ set ys" for k + show "[x\ys . f k = f x] = [x\xs . f k = f x]" if "k \ set ys" for k proof - from mset_equal have set_equal: "set xs = set ys" by (rule mset_eq_setD) with that have "insert k (set ys) = set ys" by auto with \inj_on f (set xs)\ have inj: "inj_on f (insert k (set ys))" by (simp add: set_equal) - from inj have "filter (\x. f k = f x) ys = filter (HOL.eq k) ys" + from inj have "[x\ys . f k = f x] = filter (HOL.eq k) ys" by (auto intro!: inj_on_filter_key_eq) also have "\ = replicate (count (mset ys) k) k" by (simp add: replicate_count_mset_eq_filter_eq) @@ -2597,7 +2597,7 @@ using mset_equal by simp also have "\ = filter (HOL.eq k) xs" by (simp add: replicate_count_mset_eq_filter_eq) - also have "\ = filter (\x. f k = f x) xs" + also have "\ = [x\xs . f k = f x]" using inj by (auto intro!: inj_on_filter_key_eq [symmetric] simp add: set_equal) finally show ?thesis . qed @@ -2610,9 +2610,9 @@ by (rule sort_key_inj_key_eq) (simp_all add: assms) lemma sort_key_by_quicksort: - "sort_key f xs = sort_key f (filter (\x. f x < f (xs ! (length xs div 2))) xs) - @ filter (\x. f x = f (xs ! (length xs div 2))) xs - @ sort_key f (filter (\x. f x > f (xs ! (length xs div 2))) xs)" (is "sort_key f ?lhs = ?rhs") + "sort_key f xs = sort_key f [x\xs. f x < f (xs ! (length xs div 2))] + @ [x\xs. f x = f (xs ! (length xs div 2))] + @ sort_key f [x\xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs") proof (rule properties_for_sort_key) show "mset ?rhs = mset ?lhs" by (rule multiset_eqI) (auto simp add: mset_filter) @@ -2623,14 +2623,14 @@ assume "l \ set ?rhs" let ?pivot = "f (xs ! (length xs div 2))" have *: "\x. f l = f x \ f x = f l" by auto - have "filter (\x. f x = f l) (sort_key f xs) = filter (\x. f x = f l) xs" + have "[x \ sort_key f xs . f x = f l] = [x \ xs. f x = f l]" unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) - with * have **: "filter (\x. f l = f x) (sort_key f xs) = filter (\x. f l = f x) xs" by simp + with * have **: "[x \ sort_key f xs . f l = f x] = [x \ xs. f l = f x]" by simp have "\x P. P (f x) ?pivot \ f l = f x \ P (f l) ?pivot \ f l = f x" by auto - then have "\P. filter (\x. P (f x) ?pivot \ f l = f x) (sort_key f xs) = - filter (\x. P (f l) ?pivot \ f l = f x) (sort_key f xs)" by simp + then have "\P. [x \ sort_key f xs . P (f x) ?pivot \ f l = f x] = + [x \ sort_key f xs. P (f l) ?pivot \ f l = f x]" by simp note *** = this [of "(<)"] this [of "(>)"] this [of "(=)"] - show "filter (\x. f l = f x) ?rhs = filter (\x. f l = f x) ?lhs" + show "[x \ ?rhs. f l = f x] = [x \ ?lhs. f l = f x]" proof (cases "f l" ?pivot rule: linorder_cases) case less then have "f l \ ?pivot" and "\ f l > ?pivot" by auto @@ -2648,15 +2648,15 @@ qed lemma sort_by_quicksort: - "sort xs = sort (filter (\x. x < xs ! (length xs div 2)) xs) - @ filter (\x. x = xs ! (length xs div 2)) xs - @ sort (filter (\x. x > xs ! (length xs div 2)) xs)" (is "sort ?lhs = ?rhs") + "sort xs = sort [x\xs. x < xs ! (length xs div 2)] + @ [x\xs. x = xs ! (length xs div 2)] + @ sort [x\xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs") using sort_key_by_quicksort [of "\x. x", symmetric] by simp text \A stable parametrized quicksort\ definition part :: "('b \ 'a) \ 'a \ 'b list \ 'b list \ 'b list \ 'b list" where - "part f pivot xs = (filter (\x. f x < pivot) xs, filter (\x. f x = pivot) xs, filter (\x. f x > pivot) xs)" + "part f pivot xs = ([x \ xs. f x < pivot], [x \ xs. f x = pivot], [x \ xs. pivot < f x])" lemma part_code [code]: "part f pivot [] = ([], [], [])" diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/MicroJava/DFA/Kildall.thy --- a/src/HOL/MicroJava/DFA/Kildall.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/MicroJava/DFA/Kildall.thy Wed Jun 06 14:27:10 2018 +0100 @@ -38,7 +38,7 @@ lemma (in Semilat) nth_merges: "\ss. \p < length ss; ss \ list n A; \(p,t)\set ps. p t\A \ \ - (merges f ps ss)!p = map snd (filter (\(p',t'). p'=p) ps) ++_f ss!p" + (merges f ps ss)!p = map snd [(p',t') \ ps. p'=p] ++_f ss!p" (is "\ss. \_; _; ?steptype ps\ \ ?P ss ps") proof (induct ps) show "\ss. ?P ss []" by simp diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/MicroJava/DFA/LBVComplete.thy --- a/src/HOL/MicroJava/DFA/LBVComplete.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Wed Jun 06 14:27:10 2018 +0100 @@ -80,13 +80,13 @@ assume merge: "?s1 \ T" from x ss1 have "?s1 = (if \(pc', s')\set ss1. pc' \ pc + 1 \ s' <=_r c!pc' - then (map snd (filter (\(p', t'). p'=pc+1) ss1)) ++_f x + then (map snd [(p', t') \ ss1 . p'=pc+1]) ++_f x else \)" by (rule merge_def) with merge obtain app: "\(pc',s')\set ss1. pc' \ pc+1 \ s' <=_r c!pc'" (is "?app ss1") and - sum: "(map snd (filter (\(p',t'). p' = pc+1) ss1) ++_f x) = ?s1" + sum: "(map snd [(p',t') \ ss1 . p' = pc+1] ++_f x) = ?s1" (is "?map ss1 ++_f x = _" is "?sum ss1 = _") by (simp split: if_split_asm) from app less @@ -115,7 +115,7 @@ from x ss2 have "?s2 = (if \(pc', s')\set ss2. pc' \ pc + 1 \ s' <=_r c!pc' - then map snd (filter (\(p', t'). p' = pc + 1) ss2) ++_f x + then map snd [(p', t') \ ss2 . p' = pc + 1] ++_f x else \)" by (rule merge_def) ultimately have ?thesis by simp @@ -194,7 +194,7 @@ ultimately have "merge c pc ?step (c!Suc pc) = (if \(pc',s')\set ?step. pc'\pc+1 \ s' <=_r c!pc' - then map snd (filter (\(p',t').p'=pc+1) ?step) ++_f c!Suc pc + then map snd [(p',t') \ ?step.p'=pc+1] ++_f c!Suc pc else \)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms]) moreover { fix pc' s' assume s': "(pc', s') \ set ?step" and suc_pc: "pc' \ pc+1" @@ -207,7 +207,7 @@ } hence "\(pc',s')\set ?step. pc'\pc+1 \ s' <=_r c!pc'" by auto moreover from pc have "Suc pc = length \ \ Suc pc < length \" by auto - hence "map snd (filter (\(p',t').p'=pc+1) ?step) ++_f c!Suc pc \ \" + hence "map snd [(p',t') \ ?step.p'=pc+1] ++_f c!Suc pc \ \" (is "?map ++_f _ \ _") proof (rule disjE) assume pc': "Suc pc = length \" @@ -215,7 +215,7 @@ moreover from pc' bounded pc have "\(p',t')\set ?step. p'\pc+1" by clarify (drule boundedD, auto) - hence "filter (\(p',t').p'=pc+1) ?step = []" by (blast intro: filter_False) + hence "[(p',t') \ ?step.p'=pc+1] = []" by (blast intro: filter_False) hence "?map = []" by simp ultimately show ?thesis by (simp add: B_neq_T) next @@ -262,7 +262,7 @@ hence "merge c pc ?step (c!Suc pc) \ \" by (simp add: wti) ultimately have "merge c pc ?step (c!Suc pc) = - map snd (filter (\(p',t').p'=pc+1) ?step) ++_f c!Suc pc" by (rule merge_not_top_s) + map snd [(p',t')\ ?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s) hence "?wti = \" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti) also { from suc_pc phi have "\!Suc pc \ A" by simp diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/MicroJava/DFA/LBVCorrect.thy --- a/src/HOL/MicroJava/DFA/LBVCorrect.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/MicroJava/DFA/LBVCorrect.thy Wed Jun 06 14:27:10 2018 +0100 @@ -88,7 +88,7 @@ also from s2 merge have "\ \ \" (is "?merge \ _") by simp with cert_in_A step_in_A - have "?merge = (map snd (filter (\(p',t').p'=pc+1) (?step pc)) ++_f (c!(pc+1)))" + have "?merge = (map snd [(p',t') \ ?step pc. p'=pc+1] ++_f (c!(pc+1)))" by (rule merge_not_top_s) finally have "s' <=_r ?s2" using step_in_A cert_in_A True step diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/MicroJava/DFA/LBVSpec.thy --- a/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Jun 06 14:27:10 2018 +0100 @@ -113,7 +113,7 @@ lemma (in Semilat) pp_ub1': assumes S: "snd`set S \ A" assumes y: "y \ A" and ab: "(a, b) \ set S" - shows "b <=_r map snd (filter (\(p', t'). p' = a) S) ++_f y" + shows "b <=_r map snd [(p', t') \ S . p' = a] ++_f y" proof - from S have "\(x,y) \ set S. y \ A" by auto with semilat y ab show ?thesis by - (rule ub1') @@ -172,7 +172,7 @@ "\x. x \ A \ snd`set ss \ A \ merge c pc ss x = (if \(pc',s') \ set ss. pc'\pc+1 \ s' <=_r c!pc' then - map snd (filter (\(p',t'). p'=pc+1) ss) ++_f x + map snd [(p',t') \ ss. p'=pc+1] ++_f x else \)" (is "\x. _ \ _ \ ?merge ss x = ?if ss x" is "\x. _ \ _ \ ?P ss x") proof (induct ss) @@ -202,15 +202,15 @@ hence "\(pc', s')\set ls. pc'\pc+1 \ s' <=_r c!pc'" by auto moreover from True have - "map snd (filter (\(p',t'). p'=pc+1) ls) ++_f ?if' = - (map snd (filter (\(p',t'). p'=pc+1) (l#ls)) ++_f x)" + "map snd [(p',t')\ls . p'=pc+1] ++_f ?if' = + (map snd [(p',t')\l#ls . p'=pc+1] ++_f x)" by simp ultimately show ?thesis using True by simp next case False moreover - from ls have "set (map snd (filter (\(p', t'). p' = Suc pc) ls)) \ A" by auto + from ls have "set (map snd [(p', t')\ls . p' = Suc pc]) \ A" by auto ultimately show ?thesis by auto qed finally show "?P (l#ls) x" . @@ -219,7 +219,7 @@ lemma (in lbv) merge_not_top_s: assumes x: "x \ A" and ss: "snd`set ss \ A" assumes m: "merge c pc ss x \ \" - shows "merge c pc ss x = (map snd (filter (\(p',t'). p'=pc+1) ss) ++_f x)" + shows "merge c pc ss x = (map snd [(p',t') \ ss. p'=pc+1] ++_f x)" proof - from ss m have "\(pc',s') \ set ss. (pc' \ pc+1 \ s' <=_r c!pc')" by (rule merge_not_top) @@ -307,8 +307,8 @@ assumes s0: "snd`set ss \ A" and x: "x \ A" shows "merge c pc ss x \ A" proof - - from s0 have "set (map snd (filter (\(p', t'). p'=pc+1) ss)) \ A" by auto - with x have "(map snd (filter (\(p', t'). p'=pc+1) ss) ++_f x) \ A" + from s0 have "set (map snd [(p', t')\ss . p'=pc+1]) \ A" by auto + with x have "(map snd [(p', t')\ss . p'=pc+1] ++_f x) \ A" by (auto intro!: plusplus_closed semilat) with s0 x show ?thesis by (simp add: merge_def T_A) qed diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/MicroJava/DFA/SemilatAlg.thy --- a/src/HOL/MicroJava/DFA/SemilatAlg.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy Wed Jun 06 14:27:10 2018 +0100 @@ -155,7 +155,7 @@ lemma ub1': assumes "semilat (A, r, f)" shows "\\(p,s) \ set S. s \ A; y \ A; (a,b) \ set S\ - \ b <=_r map snd (filter (\(p', t'). p' = a) S) ++_f y" + \ b <=_r map snd [(p', t')\S. p' = a] ++_f y" proof - interpret Semilat A r f using assms by (rule Semilat.intro) @@ -175,7 +175,7 @@ lemma plusplus_empty: "\s'. (q, s') \ set S \ s' +_f ss ! q = ss ! q \ - (map snd (filter (\(p', t'). p' = q) S) ++_f ss ! q) = ss ! q" + (map snd [(p', t') \ S. p' = q] ++_f ss ! q) = ss ! q" by (induct S) auto end diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Jun 06 14:27:10 2018 +0100 @@ -317,7 +317,7 @@ | "\v \ B\<^sub>1; v \ B\<^sub>1\ \ a # v @ w \ B\<^sub>1" theorem S\<^sub>1_sound: -"w \ S\<^sub>1 \ length (filter (\x. x = a) w) = length (filter (\x. x = b) w)" +"w \ S\<^sub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" nitpick [expect = genuine] oops @@ -330,7 +330,7 @@ | "\v \ B\<^sub>2; v \ B\<^sub>2\ \ a # v @ w \ B\<^sub>2" theorem S\<^sub>2_sound: -"w \ S\<^sub>2 \ length (filter (\x. x = a) w) = length (filter (\x. x = b) w)" +"w \ S\<^sub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" nitpick [expect = genuine] oops @@ -343,12 +343,12 @@ | "\v \ B\<^sub>3; w \ B\<^sub>3\ \ a # v @ w \ B\<^sub>3" theorem S\<^sub>3_sound: -"w \ S\<^sub>3 \ length (filter (\x. x = a) w) = length (filter (\x. x = b) w)" +"w \ S\<^sub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" nitpick [card = 1-5, expect = none] sorry theorem S\<^sub>3_complete: -"length (filter (\x. x = a) w) = length (filter (\x. x = b) w) \ w \ S\<^sub>3" +"length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^sub>3" nitpick [expect = genuine] oops @@ -362,19 +362,19 @@ | "\v \ B\<^sub>4; w \ B\<^sub>4\ \ a # v @ w \ B\<^sub>4" theorem S\<^sub>4_sound: -"w \ S\<^sub>4 \ length (filter (\x. x = a) w) = length (filter (\x. x = b) w)" +"w \ S\<^sub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" nitpick [card = 1-5, expect = none] sorry theorem S\<^sub>4_complete: -"length (filter (\x. x = a) w) = length (filter (\x. x = b) w) \ w \ S\<^sub>4" +"length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^sub>4" nitpick [card = 1-5, expect = none] sorry theorem S\<^sub>4_A\<^sub>4_B\<^sub>4_sound_and_complete: -"w \ S\<^sub>4 \ length (filter (\x. x = a) w) = length (filter (\x. x = b) w)" -"w \ A\<^sub>4 \ length (filter (\x. x = a) w) = length (filter (\x. x = b) w) + 1" -"w \ B\<^sub>4 \ length (filter (\x. x = b) w) = length (filter (\x. x = a) w) + 1" +"w \ S\<^sub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" +"w \ A\<^sub>4 \ length [x \ w. x = a] = length [x \ w. x = b] + 1" +"w \ B\<^sub>4 \ length [x \ w. x = b] = length [x \ w. x = a] + 1" nitpick [card = 1-5, expect = none] sorry diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Nominal/Examples/W.thy --- a/src/HOL/Nominal/Examples/W.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Nominal/Examples/W.thy Wed Jun 06 14:27:10 2018 +0100 @@ -9,7 +9,7 @@ abbreviation "difference_list" :: "'a list \ 'a list \ 'a list" ("_ - _" [60,60] 60) where - "xs - ys \ filter (\x. x\set ys) xs" + "xs - ys \ [x \ xs. x\set ys]" lemma difference_eqvt_tvar[eqvt]: fixes pi::"tvar prm" diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Parity.thy Wed Jun 06 14:27:10 2018 +0100 @@ -933,7 +933,7 @@ lemma drop_bit_of_nat: "drop_bit n (of_nat m) = of_nat (drop_bit n m)" - by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"]) + by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"]) end diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Wed Jun 06 14:27:10 2018 +0100 @@ -71,7 +71,7 @@ oops theorem S\<^sub>1_sound: -"S\<^sub>1p w \ length (filter (\x. x=a) w) = length (filter (\x. x=b) w)" +"S\<^sub>1p w \ length [x \ w. x = a] = length [x \ w. x = b]" quickcheck[tester=smart_exhaustive, size=15] oops @@ -113,7 +113,7 @@ oops *) theorem S\<^sub>2_sound: -"S\<^sub>2p w \ length (filter (\x. x=a) w) = length (filter (\x. x=b) w)" +"S\<^sub>2p w \ length [x \ w. x = a] = length [x \ w. x = b]" quickcheck[tester=smart_exhaustive, size=5, iterations=10] oops @@ -133,16 +133,16 @@ lemma S\<^sub>3_sound: -"S\<^sub>3p w \ length (filter (\x. x=a) w) = length (filter (\x. x=b) w)" +"S\<^sub>3p w \ length [x \ w. x = a] = length [x \ w. x = b]" quickcheck[tester=smart_exhaustive, size=10, iterations=10] oops -lemma "\ (length w > 2) \ \ (length (filter (\x. x=a) w) = length (filter (\x. x=b) w))" +lemma "\ (length w > 2) \ \ (length [x \ w. x = a] = length [x \ w. x = b])" quickcheck[size=10, tester = smart_exhaustive] oops theorem S\<^sub>3_complete: -"length (filter (\x. x=a) w) = length (filter (\x. x=b) w) \ S\<^sub>3p w" +"length [x \ w. x = a] = length [x \ w. b = x] \ S\<^sub>3p w" (*quickcheck[generator=SML]*) quickcheck[tester=smart_exhaustive, size=10, iterations=100] oops @@ -158,12 +158,12 @@ | "\v \ B\<^sub>4; w \ B\<^sub>4\ \ a # v @ w \ B\<^sub>4" theorem S\<^sub>4_sound: -"S\<^sub>4p w \ length (filter (\x. x=a) w) = length (filter (\x. x=b) w)" +"S\<^sub>4p w \ length [x \ w. x = a] = length [x \ w. x = b]" quickcheck[tester = smart_exhaustive, size=5, iterations=1] oops theorem S\<^sub>4_complete: -"length (filter (\x. x=a) w) = length (filter (\x. x=b) w) \ S\<^sub>4p w" +"length [x \ w. x = a] = length [x \ w. x = b] \ S\<^sub>4p w" quickcheck[tester = smart_exhaustive, size=5, iterations=1] oops @@ -301,7 +301,7 @@ subsection "Compressed matrix" -definition "sparsify xs = filter (\i. snd i \ 0) (zip [0.. zip [0.. 0]" (* lemma sparsify_length: "(i, x) \ set (sparsify xs) \ i < length xs" by (auto simp: sparsify_def set_zip) diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Wed Jun 06 14:27:10 2018 +0100 @@ -2028,7 +2028,7 @@ private lemma pmf_of_list_aux: assumes "\x. x \ set (map snd xs) \ x \ 0" assumes "sum_list (map snd xs) = 1" - shows "(\\<^sup>+ x. ennreal (sum_list (map snd (filter (\z. fst z = x) xs))) \count_space UNIV) = 1" + shows "(\\<^sup>+ x. ennreal (sum_list (map snd [z\xs . fst z = x])) \count_space UNIV) = 1" proof - have "(\\<^sup>+ x. ennreal (sum_list (map snd (filter (\z. fst z = x) xs))) \count_space UNIV) = (\\<^sup>+ x. ennreal (sum_list (map (\(x',p). indicator {x'} x * p) xs)) \count_space UNIV)" @@ -2083,7 +2083,7 @@ show "x \ set (map fst xs)" proof (rule ccontr) assume "x \ set (map fst xs)" - hence "filter (\z. fst z = x) xs = []" by (auto simp: filter_empty_conv) + hence "[z\xs . fst z = x] = []" by (auto simp: filter_empty_conv) with A assms show False by (simp add: pmf_pmf_of_list set_pmf_eq) qed qed @@ -2122,10 +2122,10 @@ have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)" by simp also from assms - have "\ = (\x\set_pmf (pmf_of_list xs) \ A. ennreal (sum_list (map snd (filter (\z. fst z = x) xs))))" + have "\ = (\x\set_pmf (pmf_of_list xs) \ A. ennreal (sum_list (map snd [z\xs . fst z = x])))" by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list Int_def) also from assms - have "\ = ennreal (\x\set_pmf (pmf_of_list xs) \ A. sum_list (map snd (filter (\z. fst z = x) xs)))" + have "\ = ennreal (\x\set_pmf (pmf_of_list xs) \ A. sum_list (map snd [z\xs . fst z = x]))" by (subst sum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg) also have "\ = ennreal (\x\set_pmf (pmf_of_list xs) \ A. indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S") @@ -2184,7 +2184,7 @@ { fix x assume A: "x \ fst ` set xs" and B: "x \ set_pmf (pmf_of_list xs)" then obtain y where y: "(x, y) \ set xs" by auto - from B have "sum_list (map snd (filter (\z. fst z = x) xs)) = 0" + from B have "sum_list (map snd [z\xs. fst z = x]) = 0" by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq) moreover from y have "y \ snd ` {xa \ set xs. fst xa = x}" by force ultimately have "y = 0" using assms(1) @@ -2199,11 +2199,11 @@ defines "xs' \ filter (\z. snd z \ 0) xs" shows "pmf_of_list_wf xs'" "pmf_of_list xs' = pmf_of_list xs" proof - - have "map snd (filter (\z. snd z \ 0) xs) = filter (\x. x \ 0) (map snd xs)" + have "map snd [z\xs . snd z \ 0] = filter (\x. x \ 0) (map snd xs)" by (induction xs) simp_all with assms(1) show wf: "pmf_of_list_wf xs'" by (auto simp: pmf_of_list_wf_def xs'_def sum_list_filter_nonzero) - have "sum_list (map snd (filter (\z. fst z = i) xs')) = sum_list (map snd (filter (\z. fst z = i) xs))" for i + have "sum_list (map snd [z\xs' . fst z = i]) = sum_list (map snd [z\xs . fst z = i])" for i unfolding xs'_def by (induction xs) simp_all with assms(1) wf show "pmf_of_list xs' = pmf_of_list xs" by (intro pmf_eqI) (simp_all add: pmf_pmf_of_list) diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Wed Jun 06 14:27:10 2018 +0100 @@ -186,7 +186,7 @@ oops lemma - "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) (filter (\ys. i < length ys) xs)" + "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]" quickcheck[random, iterations = 10000] quickcheck[exhaustive, expect = counterexample] oops @@ -228,13 +228,13 @@ oops lemma - "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\ys. i < length ys) (remdups xs))" + "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]" quickcheck[random] quickcheck[exhaustive, expect = counterexample] oops lemma - "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\ys. length ys \ {.. xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \ {.. 'a list \ 'a list" where - [simp]: "inter_list xs ys = filter (\x. x \ set xs \ x \ set ys) xs" + [simp]: "inter_list xs ys = [x \ xs. x \ set xs \ x \ set ys]" definition diff_list :: "'a list \ 'a list \ 'a list" where - [simp]: "diff_list xs ys = filter (\x. x \ set ys) xs" + [simp]: "diff_list xs ys = [x \ xs. x \ set ys]" definition rsp_fold :: "('a \ 'b \ 'b) \ bool" diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Random.thy --- a/src/HOL/Random.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Random.thy Wed Jun 06 14:27:10 2018 +0100 @@ -116,7 +116,7 @@ lemma select_weight_drop_zero: "select_weight (filter (\(k, _). k > 0) xs) = select_weight xs" proof - - have "sum_list (map fst (filter (\(k, _). 0 < k) xs)) = sum_list (map fst xs)" + have "sum_list (map fst [(k, _)\xs . 0 < k]) = sum_list (map fst xs)" by (induct xs) (auto simp add: less_natural_def natural_eq_iff) then show ?thesis by (simp only: select_weight_def pick_drop_zero) qed diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Real_Vector_Spaces.thy Wed Jun 06 14:27:10 2018 +0100 @@ -70,7 +70,7 @@ apply (force simp add: linear_def real_scaleR_def[abs_def]) done -hide_const (open)\\locale constants\ +hide_const (open)\ \locale constants\ real_vector.dependent real_vector.independent real_vector.representation @@ -89,7 +89,7 @@ unfolding linear_def real_scaleR_def by (rule refl)+ -hide_const (open)\\locale constants\ +hide_const (open)\ \locale constants\ real_vector.construct lemma linear_compose: "linear f \ linear g \ linear (g o f)" @@ -168,7 +168,7 @@ apply (erule (1) nonzero_inverse_scaleR_distrib) done -lemmas sum_constant_scaleR = real_vector.sum_constant_scale\\legacy name\ +lemmas sum_constant_scaleR = real_vector.sum_constant_scale\ \legacy name\ named_theorems vector_add_divide_simps "to simplify sums of scaled vectors" diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/Vector_Spaces.thy --- a/src/HOL/Vector_Spaces.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/Vector_Spaces.thy Wed Jun 06 14:27:10 2018 +0100 @@ -41,7 +41,7 @@ locale vector_space = fixes scale :: "'a::field \ 'b::ab_group_add \ 'b" (infixr "*s" 75) - assumes vector_space_assms:\\re-stating the assumptions of \module\ instead of extending \module\ + assumes vector_space_assms:\ \re-stating the assumptions of \module\ instead of extending \module\ allows us to rewrite in the sublocale.\ "a *s (x + y) = a *s x + a *s y" "(a + b) *s x = a *s x + b *s x" @@ -68,7 +68,7 @@ sublocale module scale rewrites "module_hom = linear" by (unfold_locales) (fact vector_space_assms module_hom_eq_linear)+ -lemmas\\from \module\\ +lemmas\ \from \module\\ linear_id = module_hom_id and linear_ident = module_hom_ident and linear_scale_self = module_hom_scale_self @@ -607,7 +607,7 @@ context fixes f assumes "linear s1 s2 f" begin interpretation linear s1 s2 f by fact -lemmas\\from locale \module_hom\\ +lemmas\ \from locale \module_hom\\ linear_0 = zero and linear_add = add and linear_scale = scale @@ -634,7 +634,7 @@ rewrites "module_hom = linear" by unfold_locales (fact module_hom_eq_linear) -lemmas\\from locale \module_pair\\ +lemmas\ \from locale \module_pair\\ linear_eq_on_span = module_hom_eq_on_span and linear_compose_scale_right = module_hom_scale and linear_compose_add = module_hom_add @@ -834,7 +834,7 @@ by (auto simp: that construct_in_span in_span_in_range_construct) lemma linear_independent_extend_subspace: - \\legacy: use @{term construct} instead\ + \ \legacy: use @{term construct} instead\ assumes "vs1.independent B" shows "\g. linear s1 s2 g \ (\x\B. g x = f x) \ range g = vs2.span (f`B)" by (rule exI[where x="construct B f"]) diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/ex/Quicksort.thy --- a/src/HOL/ex/Quicksort.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/ex/Quicksort.thy Wed Jun 06 14:27:10 2018 +0100 @@ -13,11 +13,11 @@ fun quicksort :: "'a list \ 'a list" where "quicksort [] = []" -| "quicksort (x#xs) = quicksort (filter (\y. \ x\y) xs) @ [x] @ quicksort (filter (\y. x\y) xs)" +| "quicksort (x#xs) = quicksort [y\xs. \ x\y] @ [x] @ quicksort [y\xs. x\y]" lemma [code]: "quicksort [] = []" - "quicksort (x#xs) = quicksort (filter (\y. \ x\y) xs) @ [x] @ quicksort (filter (\y. x\y) xs)" + "quicksort (x#xs) = quicksort [y\xs. yxs. x\y]" by (simp_all add: not_le) lemma quicksort_permutes [simp]: diff -r 0b71d08528f0 -r cada19e0c6c7 src/HOL/ex/Radix_Sort.thy --- a/src/HOL/ex/Radix_Sort.thy Wed Jun 06 14:25:53 2018 +0100 +++ b/src/HOL/ex/Radix_Sort.thy Wed Jun 06 14:27:10 2018 +0100 @@ -44,7 +44,7 @@ lemma sorted_from_Suc2: "\ cols xss n; i < n; sorted_col i xss; - \x. sorted_from (i+1) (filter (\ys. ys!i = x) xss) \ + \x. sorted_from (i+1) [ys \ xss. ys!i = x] \ \ sorted_from i xss" proof(induction xss rule: induct_list012) case 1 show ?case by simp @@ -68,7 +68,7 @@ proof(rule "3.IH"[OF _ "3.prems"(2)]) show "cols (xs2 # xss) n" using "3.prems"(1) by(simp add: cols_def) show "sorted_col i (xs2 # xss)" using "3.prems"(3) by simp - show "\x. sorted_from (i+1) (filter (\ys. ys ! i = x) (xs2 # xss))" + show "\x. sorted_from (i+1) [ys\xs2 # xss . ys ! i = x]" using "3.prems"(4) sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.order.refl]]]] by fastforce @@ -81,7 +81,7 @@ shows "sorted_from i (sort_col i xss)" proof (rule sorted_from_Suc2[OF cols_sort1[OF assms(1)] assms(2)]) show "sorted_col i (sort_col i xss)" by(simp add: sorted) - fix x show "sorted_from (i+1) (filter (\ys. ys ! i = x) (sort_col i xss))" + fix x show "sorted_from (i+1) [ys \ sort_col i xss . ys ! i = x]" proof - from assms(3) have "sorted_from (i+1) (filter (\ys. ys!i = x) xss)" diff -r 0b71d08528f0 -r cada19e0c6c7 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Wed Jun 06 14:25:53 2018 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Jun 06 14:27:10 2018 +0100 @@ -252,7 +252,6 @@ Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a", detect = Build_Log.Prop.build_start + " < date '2017-03-03'")) - val remote_builds1: List[List[Remote_Build]] = { List( @@ -260,6 +259,12 @@ options = "-m32 -B -M1x2,2", args = "-N -g timing")), List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90, options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), + List(Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90, + options = "-m32 -B -M1x2,2 -t Benchmarks" + + " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + + " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_SMLNJ=sml -e ISABELLE_SWIPL=swipl", + args = "-N -a -d '~~/src/Benchmarks'", + detect = Build_Log.Prop.build_tags + " = " + SQL.string("Benchmarks"))), List( Remote_Build("Mac OS X", "macbroy2", options = "-m32 -M8" + diff -r 0b71d08528f0 -r cada19e0c6c7 src/Pure/General/cache.scala --- a/src/Pure/General/cache.scala Wed Jun 06 14:25:53 2018 +0100 +++ b/src/Pure/General/cache.scala Wed Jun 06 14:27:10 2018 +0100 @@ -1,4 +1,4 @@ -/* Title: Pure/cache.scala +/* Title: Pure/General/cache.scala Author: Makarius cache for partial sharing (weak table). diff -r 0b71d08528f0 -r cada19e0c6c7 src/Tools/jEdit/src-base/Isabelle_Base.props --- a/src/Tools/jEdit/src-base/Isabelle_Base.props Wed Jun 06 14:25:53 2018 +0100 +++ b/src/Tools/jEdit/src-base/Isabelle_Base.props Wed Jun 06 14:27:10 2018 +0100 @@ -14,4 +14,4 @@ #dependencies plugin.isabelle.jedit_base.Plugin.depend.0=jdk 1.8 -plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.04.00.00 +plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.05.00.00 diff -r 0b71d08528f0 -r cada19e0c6c7 src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Wed Jun 06 14:25:53 2018 +0100 +++ b/src/Tools/jEdit/src/Isabelle.props Wed Jun 06 14:27:10 2018 +0100 @@ -5,7 +5,7 @@ #identification plugin.isabelle.jedit.Plugin.name=Isabelle plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel -plugin.isabelle.jedit.Plugin.version=9.0 +plugin.isabelle.jedit.Plugin.version=10.0 plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE #system parameters @@ -14,7 +14,7 @@ #dependencies plugin.isabelle.jedit.Plugin.depend.0=jdk 1.8 -plugin.isabelle.jedit.Plugin.depend.1=jedit 05.04.00.00 +plugin.isabelle.jedit.Plugin.depend.1=jedit 05.05.00.00 plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4 plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3 plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8