summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 04 Jun 2005 18:20:00 +0200 | |

changeset 16234 | 421c3522f160 |

parent 16233 | e634d33deb86 |

child 16235 | f4c43d241eb7 |

major reorganization and cleanup;

--- a/NEWS Sat Jun 04 10:26:08 2005 +0200 +++ b/NEWS Sat Jun 04 18:20:00 2005 +0200 @@ -9,456 +9,465 @@ * Theory headers: the new header syntax for Isar theories is theory <name> - imports <theory1> ... <theoryn> + imports <theory1> ... <theoryN> + uses <file1> ... <fileM> begin - optionally also with a "files" section. The syntax - - theory <name> = <theory1> + ... + <theoryn>: - - will still be supported for some time but will eventually disappear. - The syntax of old-style theories has not changed. +where the 'uses' part is optional. The previous syntax + + theory <name> = <theory1> + ... + <theoryN>: + +will disappear in the next release. Note that there is no change in +ancient non-Isar theories. * Theory loader: parent theories can now also be referred to via - relative and absolute paths. - -* Provers/quasi.ML: new transitivity reasoners for transitivity only - and quasi orders. - -* Provers/trancl.ML: new transitivity reasoner for transitive and - reflexive-transitive closure of relations. - -* Provers/blast.ML: new reference depth_limit to make blast's depth - limit (previously hard-coded with a value of 20) user-definable. - -* Provers: new version of the subst method, for single-step rewriting: it now - works in bound variable contexts. New is subst (asm), for rewriting an - assumption. Thanks to Lucas Dixon! INCOMPATIBILITY: may rewrite a different - subterm than the original subst method, which is still available under the - name simplesubst. - -* Pure: thin_tac now works even if the assumption being deleted contains !! or ==>. - More generally, erule now works even if the major premise of the elimination rule - contains !! or ==>. - -* Pure: considerably improved version of 'constdefs' command. Now - performs automatic type-inference of declared constants; additional - support for local structure declarations (cf. locales and HOL - records), see also isar-ref manual. Potential INCOMPATIBILITY: need - to observe strictly sequential dependencies of definitions within a - single 'constdefs' section; moreover, the declared name needs to be - an identifier. If all fails, consider to fall back on 'consts' and - 'defs' separately. - -* Pure: improved indexed syntax and implicit structures. First of - all, indexed syntax provides a notational device for subscripted - application, using the new syntax \<^bsub>term\<^esub> for arbitrary - expressions. Secondly, in a local context with structure - declarations, number indexes \<^sub>n or the empty index (default - number 1) refer to a certain fixed variable implicitly; option - show_structs controls printing of implicit structures. Typical - applications of these concepts involve record types and locales. - -* Pure: clear separation of logical types and nonterminals, where the - latter may only occur in 'syntax' specifications or type - abbreviations. Before that distinction was only partially - implemented via type class "logic" vs. "{}". Potential - INCOMPATIBILITY in rare cases of improper use of 'types'/'consts' - instead of 'nonterminals'/'syntax'. Some very exotic syntax - specifications may require further adaption (e.g. Cube/Base.thy). - -* Pure: removed obsolete type class "logic", use the top sort {} - instead. Note that non-logical types should be declared as - 'nonterminals' rather than 'types'. INCOMPATIBILITY for new - object-logic specifications. - -* Pure: command 'no_syntax' removes grammar declarations (and - translations) resulting from the given syntax specification, which - is interpreted in the same manner as for the 'syntax' command. - -* Pure: print_tac now outputs the goal through the trace channel. - -* Pure: reference NameSpace.unique_names included. If true the - (shortest) namespace-prefix is printed to disambiguate conflicts (as - yet). If false the first entry wins (as during parsing). Default - value is true. - -* Pure: tuned internal renaming of symbolic identifiers -- attach - primes instead of base 26 numbers. - -* Pure: new flag show_question_marks controls printing of leading - question marks in schematic variable names. - -* Pure: new version of thms_containing that searches for a list of - criteria instead of a list of constants. Known criteria are: intro, - elim, dest, name:string, simp:term, and any term. Criteria can be - preceded by '-' to select theorems that do not match. Intro, elim, - dest select theorems that match the current goal, name:s selects - theorems whose fully qualified name contain s, and simp:term selects - all simplification rules whose lhs match term. Any other term is - interpreted as pattern and selects all theorems matching the - pattern. Available in ProofGeneral under 'ProofGeneral -> Find - Theorems' or C-c C-f. - - Example: C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL." - - prints the last 100 theorems matching the pattern "(_::nat) + _ + _", - matching the current goal as introduction rule and not having "HOL." - in their name (i.e. not being defined in theory HOL). - -* Pure/Syntax: In schematic variable names, *any* symbol following - \<^isub> or \<^isup> is now treated as part of the base name. For - example, the following works without printing of ugly ".0" indexes: - - lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1" - by simp - -* Pure/Syntax: inner syntax includes (*(*nested*) comments*). - -* Pure/Syntax: pretty pinter now supports unbreakable blocks, - specified in mixfix annotations as "(00...)". - -* Pure/Syntax: 'advanced' translation functions (parse_translation - etc.) may depend on the signature of the theory context being - presently used for parsing/printing, see also isar-ref manual. - -* Pure/Simplifier: you can control the depth to which conditional rewriting - is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth Limit. - -* Pure/Simplifier: simplification procedures may now take the current - simpset into account (cf. Simplifier.simproc(_i) / mk_simproc - interface), which is very useful for calling the Simplifier - recursively. Minor INCOMPATIBILITY: the 'prems' argument of - simprocs is gone -- use prems_of_ss on the simpset instead. - Moreover, the low-level mk_simproc no longer applies Logic.varify - internally, to allow for use in a context of fixed variables. - -* Isar debugging: new reference Toplevel.debug; default false. Set to - make printing of exceptions THM, TERM, TYPE and THEORY more verbose. - -* Locales: modifications regarding "includes" - - "includes" disallowed in declaration of named locales (command "locale"). - - Fixed parameter management in theorem generation for goals with "includes". - INCOMPATIBILITY: rarely, the generated theorem statement is different. - -* Locales: new context element "constrains" for adding type constraints - to parameters. - -* Locales: context expressions permit optional syntax redeclaration when - renaming parameters. - -* Locales: new commands for the interpretation of locale expressions - in theories (interpretation) and proof contexts (interpret). These take an - instantiation of the locale parameters and compute proof obligations from - the instantiated specification. After the obligations have been discharged, - the instantiated theorems of the locale are added to the theory or proof - context. Interpretation is smart in that already active interpretations - do not occur in proof obligations, neither are instantiated theorems stored - in duplicate. - Use print_interps to inspect active interpretations of a particular locale. - For details, see the Isar Reference manual. - -* Locales: INCOMPATIBILITY: experimental command "instantiate" has - been withdrawn. Use "interpret" instead. - -* Locales: proper static binding of attribute syntax -- i.e. types / - terms / facts mentioned as arguments are always those of the locale - definition context, independently of the context of later - invocations. Moreover, locale operations (renaming and type / term - instantiation) are applied to attribute arguments as expected. - - INCOMPATIBILITY of the ML interface: always pass Attrib.src instead - of actual attributes; rare situations may require Attrib.attribute - to embed those attributes into Attrib.src that lack concrete syntax. - - Attribute implementations need to cooperate properly with the static - binding mechanism. Basic parsers Args.XXX_typ/term/prop and - Attrib.XXX_thm etc. already do the right thing without further - intervention. Only unusual applications -- such as "where" or "of" - (cf. src/Pure/Isar/attrib.ML), which process arguments depending - both on the context and the facts involved -- may have to assign - parsed values to argument tokens explicitly. - -* Attributes 'induct' and 'cases': type or set names may now be - locally fixed variables as well. - -* Isar: new syntax 'name(i-j, i-, i, ...)' for referring to specific - selections of theorems in named facts via indices. - -* Pure: reorganized bootstrapping of the Pure theories; CPure is now - derived from Pure, which contains all common declarations already. - Both theories are defined via plain Isabelle/Isar .thy files. - INCOMPATIBILITY: elements of CPure (such as the CPure.intro / - CPure.elim / CPure.dest attributes) now appear in the Pure name - space; use isatool fixcpure to adapt your theory and ML sources. - -* Provers/simplifier.ML has been moved to Pure, where Simplifier.setup - is peformed already. Object-logics merely need to finish their - initial simpset configuration as before. +relative and absolute paths. + +* Improved version of thms_containing searches for a list of criteria +instead of a list of constants. Known criteria are: intro, elim, dest, +name:string, simp:term, and any term. Criteria can be preceded by '-' +to select theorems that do not match. Intro, elim, dest select +theorems that match the current goal, name:s selects theorems whose +fully qualified name contain s, and simp:term selects all +simplification rules whose lhs match term. Any other term is +interpreted as pattern and selects all theorems matching the +pattern. Available in ProofGeneral under 'ProofGeneral -> Find +Theorems' or C-c C-f. Example: + + C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL." + +prints the last 100 theorems matching the pattern "(_::nat) + _ + _", +matching the current goal as introduction rule and not having "HOL." +in their name (i.e. not being defined in theory HOL). *** Document preparation *** +* Commands 'display_drafts' and 'print_drafts' perform simple output +of raw sources. Only those symbols that do not require additional +LaTeX packages (depending on comments in isabellesym.sty) are +displayed properly, everything else is left verbatim. isatool display +and isatool print are used as front ends (these are subject to the +DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively). + +* There is now a flag to control hiding of proofs and some other +commands (such as 'ML' or 'parse/print_translation') in document +output. Hiding is enabled by default, and can be disabled by the +option '-H false' of isatool usedir or by resetting the reference +variable IsarOutput.hide_commands in ML. Additional commands to be +hidden may be declared using IsarOutput.add_hidden_commands. + * Several new antiquotation: @{term_type term} prints a term with its type annotated; @{typeof term} prints the type of a term; - @{const const} is the same as @{term const}, but checks - that the argument is a known logical constant; + @{const const} is the same as @{term const}, but checks that the + argument is a known logical constant; @{term_style style term} and @{thm_style style thm} print a term or - theorem applying a "style" to it - - Predefined styles are "lhs" and "rhs" printing the lhs/rhs of - definitions, equations, inequations etc. and "conclusion" printing - only the conclusion of a meta-logical statement theorem. Styles may - be defined via TermStyle.add_style in ML. See the "LaTeX Sugar" - document for more information. + theorem applying a "style" to it + +Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of +definitions, equations, inequations etc., 'concl' printing only the +conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem9' +to print the specified premise. TermStyle.add_style provides an ML +interface for introducing further styles. See also the "LaTeX Sugar" +document practical applications. + + +*** Pure *** + +* Considerably improved version of 'constdefs' command. Now performs +automatic type-inference of declared constants; additional support for +local structure declarations (cf. locales and HOL records), see also +isar-ref manual. Potential INCOMPATIBILITY: need to observe strictly +sequential dependencies of definitions within a single 'constdefs' +section; moreover, the declared name needs to be an identifier. If +all fails, consider to fall back on 'consts' and 'defs' separately. + +* Improved indexed syntax and implicit structures. First of all, +indexed syntax provides a notational device for subscripted +application, using the new syntax \<^bsub>term\<^esub> for arbitrary +expressions. Secondly, in a local context with structure +declarations, number indexes \<^sub>n or the empty index (default +number 1) refer to a certain fixed variable implicitly; option +show_structs controls printing of implicit structures. Typical +applications of these concepts involve record types and locales. + +* New command 'no_syntax' removes grammar declarations (and +translations) resulting from the given syntax specification, which is +interpreted in the same manner as for the 'syntax' command. + +* 'Advanced' translation functions (parse_translation etc.) may depend +on the signature of the theory context being presently used for +parsing/printing, see also isar-ref manual. + +* Improved internal renaming of symbolic identifiers -- attach primes +instead of base 26 numbers. + +* New flag show_question_marks controls printing of leading question +marks in schematic variable names. + +* In schematic variable names, *any* symbol following \<^isub> or +\<^isup> is now treated as part of the base name. For example, the +following works without printing of awkward ".0" indexes: + + lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1" + by simp + +* Inner syntax includes (*(*nested*) comments*). + +* Pretty pinter now supports unbreakable blocks, specified in mixfix +annotations as "(00...)". + +* Clear separation of logical types and nonterminals, where the latter +may only occur in 'syntax' specifications or type abbreviations. +Before that distinction was only partially implemented via type class +"logic" vs. "{}". Potential INCOMPATIBILITY in rare cases of improper +use of 'types'/'consts' instead of 'nonterminals'/'syntax'. Some very +exotic syntax specifications may require further adaption +(e.g. Cube/Base.thy). + +* Removed obsolete type class "logic", use the top sort {} instead. +Note that non-logical types should be declared as 'nonterminals' +rather than 'types'. INCOMPATIBILITY for new object-logic +specifications. + +* Simplifier: can now control the depth to which conditional rewriting +is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth +Limit. + +* Simplifier: simplification procedures may now take the current +simpset into account (cf. Simplifier.simproc(_i) / mk_simproc +interface), which is very useful for calling the Simplifier +recursively. Minor INCOMPATIBILITY: the 'prems' argument of simprocs +is gone -- use prems_of_ss on the simpset instead. Moreover, the +low-level mk_simproc no longer applies Logic.varify internally, to +allow for use in a context of fixed variables. + +* thin_tac now works even if the assumption being deleted contains !! +or ==>. More generally, erule now works even if the major premise of +the elimination rule contains !! or ==>. + +* Reorganized bootstrapping of the Pure theories; CPure is now derived +from Pure, which contains all common declarations already. Both +theories are defined via plain Isabelle/Isar .thy files. +INCOMPATIBILITY: elements of CPure (such as the CPure.intro / +CPure.elim / CPure.dest attributes) now appear in the Pure name space; +use isatool fixcpure to adapt your theory and ML sources. + +* New syntax 'name(i-j, i-, i, ...)' for referring to specific +selections of theorems in named facts via index ranges. + + +*** Locales *** + +* New commands for the interpretation of locale expressions in +theories ('interpretation') and proof contexts ('interpret'). These +take an instantiation of the locale parameters and compute proof +obligations from the instantiated specification. After the +obligations have been discharged, the instantiated theorems of the +locale are added to the theory or proof context. Interpretation is +smart in that already active interpretations do not occur in proof +obligations, neither are instantiated theorems stored in duplicate. +Use print_interps to inspect active interpretations of a particular +locale. For details, see the Isar Reference manual. + +INCOMPATIBILITY: former 'instantiate' has been withdrawn, use +'interpret' instead. + +* Proper static binding of attribute syntax -- i.e. types / terms / +facts mentioned as arguments are always those of the locale definition +context, independently of the context of later invocations. Moreover, +locale operations (renaming and type / term instantiation) are applied +to attribute arguments as expected. + +INCOMPATIBILITY of the ML interface: always pass Attrib.src instead of +actual attributes; rare situations may require Attrib.attribute to +embed those attributes into Attrib.src that lack concrete syntax. +Attribute implementations need to cooperate properly with the static +binding mechanism. Basic parsers Args.XXX_typ/term/prop and +Attrib.XXX_thm etc. already do the right thing without further +intervention. Only unusual applications -- such as "where" or "of" +(cf. src/Pure/Isar/attrib.ML), which process arguments depending both +on the context and the facts involved -- may have to assign parsed +values to argument tokens explicitly. + +* New context element "constrains" adds type constraints to parameters -- +there is no logical significance. + +* Context expressions: renaming parameters permits syntax +redeclaration as well. + +* Locale definition: 'includes' now disallowed. + +* Changed parameter management in theorem generation for long goal +statements with 'includes'. INCOMPATIBILITY: produces a different +theorem statement in rare situations. + +* Attributes 'induct' and 'cases': type or set names may now be +locally fixed variables as well. * Antiquotations now provide the option 'locale=NAME' to specify an - alternative context used for evaluating and printing the subsequent - argument, as in @{thm [locale=LC] fold_commute}, for example. - -* Commands 'display_drafts' and 'print_drafts' perform simple output - of raw sources. Only those symbols that do not require additional - LaTeX packages (depending on comments in isabellesym.sty) are - displayed properly, everything else is left verbatim. We use - isatool display and isatool print as front ends; these are subject - to the DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively. - -* Proof scripts as well as some other commands such as ML or - parse/print_translation can now be hidden in the document. Hiding - is enabled by default, and can be disabled either via the option '-H - false' of isatool usedir or by resetting the reference variable - IsarOutput.hide_commands. Additional commands to be hidden may be - declared using IsarOutput.add_hidden_commands. +alternative context used for evaluating and printing the subsequent +argument, as in @{thm [locale=LC] fold_commute}, for example. + + +*** Provers *** + +* Provers/hypsubst.ML: improved version of the subst method, for +single-step rewriting: it now works in bound variable contexts. New is +'subst (asm)', for rewriting an assumption. INCOMPATIBILITY: may +rewrite a different subterm than the original subst method, which is +still available as 'simplesubst'. + +* Provers/quasi.ML: new transitivity reasoners for transitivity only +and quasi orders. + +* Provers/trancl.ML: new transitivity reasoner for transitive and +reflexive-transitive closure of relations. + +* Provers/blast.ML: new reference depth_limit to make blast's depth +limit (previously hard-coded with a value of 20) user-definable. + +* Provers/simplifier.ML has been moved to Pure, where Simplifier.setup +is peformed already. Object-logics merely need to finish their +initial simpset configuration as before. INCOMPATIBILITY. *** HOL *** -* Datatype induction via method `induct' now preserves the name of the - induction variable. For example, when proving P(xs::'a list) by induction - on xs, the induction step is now P(xs) ==> P(a#xs) rather than - P(list) ==> P(a#list) as previously. - -* HOL/record: reimplementation of records. Improved scalability for - records with many fields, avoiding performance problems for type - inference. Records are no longer composed of nested field types, but - of nested extension types. Therefore the record type only grows - linear in the number of extensions and not in the number of fields. - The top-level (users) view on records is preserved. Potential - INCOMPATIBILITY only in strange cases, where the theory depends on - the old record representation. The type generated for a record is - called <record_name>_ext_type. - -* HOL/record: Reference record_quick_and_dirty_sensitive can be - enabled to skip the proofs triggered by a record definition or a - simproc (if quick_and_dirty is enabled). Definitions of large - records can take quite long. - -* HOL/record: "record_upd_simproc" for simplification of multiple - record updates enabled by default. Moreover, trivial updates are - also removed: r(|x := x r|) = r. INCOMPATIBILITY: old proofs break - occasionally, since simplification is more powerful by default. - -* HOL: symbolic syntax of Hilbert Choice Operator is now as follows: +* Symbolic syntax of Hilbert Choice Operator is now as follows: syntax (epsilon) "_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) - The symbol \<some> is displayed as the alternative epsilon of LaTeX - and x-symbol; use option '-m epsilon' to get it actually printed. - Moreover, the mathematically important symbolic identifier - \<epsilon> becomes available as variable, constant etc. - -* HOL: "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x". - Similarly for all quantifiers: "ALL x > y" etc. The x-symbol for >= - is \<ge>. - -* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}" (and similarly for - "\<in>" instead of ":"). - -* HOL/SetInterval: The syntax for open intervals has changed: - - Old New - {..n(} -> {..<n} - {)n..} -> {n<..} - {m..n(} -> {m..<n} - {)m..n} -> {m<..n} - {)m..n(} -> {m<..<n} - - The old syntax is still supported but will disappear in the future. - For conversion use the following emacs search and replace patterns: +The symbol \<some> is displayed as the alternative epsilon of LaTeX +and x-symbol; use option '-m epsilon' to get it actually printed. +Moreover, the mathematically important symbolic identifier \<epsilon> +becomes available as variable, constant etc. INCOMPATIBILITY, + +* "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x". +Similarly for all quantifiers: "ALL x > y" etc. The x-symbol for >= +is \<ge>. + +* "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>" +instead of ":". + +* theory SetInterval: changed the syntax for open intervals: + + Old New + {..n(} {..<n} + {)n..} {n<..} + {m..n(} {m..<n} + {)m..n} {m<..n} + {)m..n(} {m<..<n} + +The old syntax is still supported but will disappear in the next +release. For conversion use the following Emacs search and replace +patterns (these are not perfect but work quite well): {)\([^\.]*\)\.\. -> {\1<\.\.} \.\.\([^(}]*\)(} -> \.\.<\1} - They are not perfect but work quite well. - -* HOL: The syntax for 'setsum', summation over finite sets, has changed: - - The syntax for 'setsum (%x. e) A' used to be '\<Sum>x:A. e' - and is now either 'SUM x:A. e' or '\<Sum>x\<in>A. e'. - - There is new syntax for summation over finite sets: - - '\<Sum>x | P. e' is the same as 'setsum (%x. e) {x. P}' - '\<Sum>x=a..b. e' is the same as 'setsum (%x. e) {a..b}' - '\<Sum>x=a..<b. e' is the same as 'setsum (%x. e) {a..<b}' - '\<Sum>x<k. e' is the same as 'setsum (%x. e) {..<k}' - - Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e' - now translates into 'setsum' as above. - -* HOL: Finite set induction: In Isar proofs, the insert case is now - "case (insert x F)" instead of the old counterintuitive "case (insert F x)". - -* HOL/Simplifier: - - - Is now set up to reason about transitivity chains involving "trancl" - (r^+) and "rtrancl" (r^*) by setting up tactics provided by - Provers/trancl.ML as additional solvers. INCOMPATIBILITY: old proofs break - occasionally as simplification may now solve more goals than previously. - - - Converts x <= y into x = y if assumption y <= x is present. Works for - all partial orders (class "order"), in particular numbers and sets. For - linear orders (e.g. numbers) it treats ~ x < y just like y <= x. - - - Simproc for "let x = a in f x" - If a is a free or bound variable or a constant then the let is unfolded. - Otherwise first a is simplified to a', and then f a' is simplified to - g. If possible we abstract a' from g arriving at "let x = a' in g' x", - otherwise we unfold the let and arrive at g. The simproc can be - enabled/disabled by the reference use_let_simproc. Potential - INCOMPATIBILITY since simplification is more powerful by default. - -* HOL: The 'refute' command has been extended to support a much larger - fragment of HOL, including axiomatic type classes, constdefs and typedefs, - inductive datatypes and recursion. +* theory Finite_Set: changed the syntax for 'setsum', summation over +finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is +now either "SUM x:A. e" or "\<Sum>x \<in> A. e". + +Some new syntax forms are available: + + "\<Sum>x | P. e" for "setsum (%x. e) {x. P}" + "\<Sum>x = a..b. e" for "setsum (%x. e) {a..b}" + "\<Sum>x = a..<b. e" for "setsum (%x. e) {a..<b}" + "\<Sum>x < k. e" for "setsum (%x. e) {..<k}" + +The latter form "\<Sum>x < k. e" used to be based on a separate +function "Summation", which has been discontinued. + +* theory Finite_Set: in structured induction proofs, the insert case +is now 'case (insert x F)' instead of the old counterintuitive 'case +(insert F x)'. + +* The 'refute' command has been extended to support a much larger +fragment of HOL, including axiomatic type classes, constdefs and +typedefs, inductive datatypes and recursion. + +* Datatype induction via method 'induct' now preserves the name of the +induction variable. For example, when proving P(xs::'a list) by +induction on xs, the induction step is now P(xs) ==> P(a#xs) rather +than P(list) ==> P(a#list) as previously. Potential INCOMPATIBILITY +in unstructured proof scripts. + +* Reworked implementation of records. Improved scalability for +records with many fields, avoiding performance problems for type +inference. Records are no longer composed of nested field types, but +of nested extension types. Therefore the record type only grows linear +in the number of extensions and not in the number of fields. The +top-level (users) view on records is preserved. Potential +INCOMPATIBILITY only in strange cases, where the theory depends on the +old record representation. The type generated for a record is called +<record_name>_ext_type. + +Flag record_quick_and_dirty_sensitive can be enabled to skip the +proofs triggered by a record definition or a simproc (if +quick_and_dirty is enabled). Definitions of large records can take +quite long. + +New simproc record_upd_simproc for simplification of multiple record +updates enabled by default. Moreover, trivial updates are also +removed: r(|x := x r|) = r. INCOMPATIBILITY: old proofs break +occasionally, since simplification is more powerful by default. + +* Simplifier: automatically reasons about transitivity chains +involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics +provided by Provers/trancl.ML as additional solvers. INCOMPATIBILITY: +old proofs break occasionally as simplification may now solve more +goals than previously. + +* Simplifier: converts x <= y into x = y if assumption y <= x is +present. Works for all partial orders (class "order"), in particular +numbers and sets. For linear orders (e.g. numbers) it treats ~ x < y +just like y <= x. + +* Simplifier: new simproc for "let x = a in f x". If a is a free or +bound variable or a constant then the let is unfolded. Otherwise +first a is simplified to b, and then f b is simplified to g. If +possible we abstract b from g arriving at "let x = b in h x", +otherwise we unfold the let and arrive at g. The simproc can be +enabled/disabled by the reference use_let_simproc. Potential +INCOMPATIBILITY since simplification is more powerful by default. *** HOLCF *** * HOLCF: discontinued special version of 'constdefs' (which used to - support continuous functions) in favor of the general Pure one with - full type-inference. +support continuous functions) in favor of the general Pure one with +full type-inference. *** ZF *** -* ZF/ex/{Group,Ring}: examples in abstract algebra, including the - First Isomorphism Theorem (on quotienting by the kernel of a - homomorphism). +* ZF/ex: theories Group and Ring provide examples in abstract algebra, +including the First Isomorphism Theorem (on quotienting by the kernel +of a homomorphism). * ZF/Simplifier: install second copy of type solver that actually - makes use of TC rules declared to Isar proof contexts (or locales); - the old version is still required for ML proof scripts. - - -*** System *** - -* Allow symlinks to all proper Isabelle executables (Isabelle, - isabelle, isatool etc.). - -* isabelle-process: Poly/ML no longer needs Perl to run an interactive - session. - -* ISABELLE_DOC_FORMAT setting specifies preferred document format (for - isatool doc, isatool mkdir, display_drafts etc.). - -* isatool usedir: option -f allows specification of the ML file to be - used by Isabelle; default is ROOT.ML. - -* HOL: isatool dimacs2hol converts files in DIMACS CNF format - (containing Boolean satisfiability problems) into Isabelle/HOL - theories. +makes use of TC rules declared to Isar proof contexts (or locales); +the old version is still required for ML proof scripts. *** ML *** * Pure/library.ML no longer defines its own option datatype, but uses - that of the SML basis, which has constructors NONE and SOME instead - of None and Some, as well as exception Option.Option instead of - OPTION. The functions the, if_none, is_some, is_none have been - adapted accordingly, while Option.map replaces apsome. +that of the SML basis, which has constructors NONE and SOME instead of +None and Some, as well as exception Option.Option instead of OPTION. +The functions the, if_none, is_some, is_none have been adapted +accordingly, while Option.map replaces apsome. * The exception LIST has been given up in favour of the standard - exceptions Empty and Subscript, as well as Library.UnequalLengths. - Function like Library.hd and Library.tl are superceded by the - standard hd and tl functions etc. - - A number of basic functions are now no longer exported to the ML - toplevel, as they are variants of standard functions. The following - suggests how one can translate existing code: +exceptions Empty and Subscript, as well as Library.UnequalLengths. +Function like Library.hd and Library.tl are superceded by the standard +hd and tl functions etc. + +A number of basic functions are now no longer exported to the ML +toplevel, as they are variants of standard functions. The following +suggests how one can translate existing code: rev_append xs ys = List.revAppend (xs, ys) nth_elem (i, xs) = List.nth (xs, i) last_elem xs = List.last xs flat xss = List.concat xss - seq fs = app fs + seq fs = List.app fs partition P xs = List.partition P xs filter P xs = List.filter P xs mapfilter f xs = List.mapPartial f xs * Pure: output via the Isabelle channels of writeln/warning/error - etc. is now passed through Output.output, with a hook for arbitrary - transformations depending on the print_mode (cf. Output.add_mode -- - the first active mode that provides a output function wins). - Already formatted output may be embedded into further text via - Output.raw; the result of Pretty.string_of/str_of and derived - functions (string_of_term/cterm/thm etc.) is already marked raw to - accommodate easy composition of diagnostic messages etc. - Programmers rarely need to care about Output.output or Output.raw at - all, with some notable exceptions: Output.output is required when - bypassing the standard channels (writeln etc.), or in token - translations to produce properly formatted results; Output.raw is - required when capturing already output material that will eventually - be presented to the user a second time. For the default print mode, - both Output.output and Output.raw have no effect. +etc. is now passed through Output.output, with a hook for arbitrary +transformations depending on the print_mode (cf. Output.add_mode -- +the first active mode that provides a output function wins). Already +formatted output may be embedded into further text via Output.raw; the +result of Pretty.string_of/str_of and derived functions +(string_of_term/cterm/thm etc.) is already marked raw to accommodate +easy composition of diagnostic messages etc. Programmers rarely need +to care about Output.output or Output.raw at all, with some notable +exceptions: Output.output is required when bypassing the standard +channels (writeln etc.), or in token translations to produce properly +formatted results; Output.raw is required when capturing already +output material that will eventually be presented to the user a second +time. For the default print mode, both Output.output and Output.raw +have no effect. + +* Pure: print_tac now outputs the goal through the trace channel. + +* Isar debugging: new reference Toplevel.debug; default false. Set to +make printing of exceptions THM, TERM, TYPE and THEORY more verbose. * Pure: name spaces have been refined, with significant changes of the - internal interfaces -- INCOMPATIBILITY. Renamed cond_extern(_table) - to extern(_table). The plain name entry path is superceded by a - general 'naming' context, which also includes the 'policy' to - produce a fully qualified name and external accesses of a fully - qualified name; NameSpace.extend is superceded by context dependent - Sign.declare_name. Several theory and proof context operations - modify the naming context. Especially note Theory.restore_naming - and ProofContext.restore_naming to get back to a sane state; note - that Theory.add_path is no longer sufficient to recover from - Theory.absolute_path in particular. +internal interfaces -- INCOMPATIBILITY. Renamed cond_extern(_table) +to extern(_table). The plain name entry path is superceded by a +general 'naming' context, which also includes the 'policy' to produce +a fully qualified name and external accesses of a fully qualified +name; NameSpace.extend is superceded by context dependent +Sign.declare_name. Several theory and proof context operations modify +the naming context. Especially note Theory.restore_naming and +ProofContext.restore_naming to get back to a sane state; note that +Theory.add_path is no longer sufficient to recover from +Theory.absolute_path in particular. + +* Pure: new flags short_names (default false) and unique_names +(default true) for controlling output of qualified names. If +short_names is set, names are printed unqualified. If unique_names is +reset, the name prefix is reduced to the minimum required to achieve +the original result when interning again, even if there is an overlap +with earlier declarations. * Pure: cases produced by proof methods specify options, where NONE - means to remove case bindings -- INCOMPATIBILITY in - (RAW_)METHOD_CASES. +means to remove case bindings -- INCOMPATIBILITY in +(RAW_)METHOD_CASES. * Provers: Simplifier and Classical Reasoner now support proof context - dependent plug-ins (simprocs, solvers, wrappers etc.). These extra - components are stored in the theory and patched into the - simpset/claset when used in an Isar proof context. Context - dependent components are maintained by the following theory - operations: - - Simplifier.add_context_simprocs - Simplifier.del_context_simprocs - Simplifier.set_context_subgoaler - Simplifier.reset_context_subgoaler - Simplifier.add_context_looper - Simplifier.del_context_looper - Simplifier.add_context_unsafe_solver - Simplifier.add_context_safe_solver - - Classical.add_context_safe_wrapper - Classical.del_context_safe_wrapper - Classical.add_context_unsafe_wrapper - Classical.del_context_unsafe_wrapper - - IMPORTANT NOTE: proof tools (methods etc.) need to use - local_simpset_of and local_claset_of to instead of the primitive - Simplifier.get_local_simpset and Classical.get_local_claset, - respectively, in order to see the context dependent fields! +dependent plug-ins (simprocs, solvers, wrappers etc.). These extra +components are stored in the theory and patched into the +simpset/claset when used in an Isar proof context. Context dependent +components are maintained by the following theory operations: + + Simplifier.add_context_simprocs + Simplifier.del_context_simprocs + Simplifier.set_context_subgoaler + Simplifier.reset_context_subgoaler + Simplifier.add_context_looper + Simplifier.del_context_looper + Simplifier.add_context_unsafe_solver + Simplifier.add_context_safe_solver + + Classical.add_context_safe_wrapper + Classical.del_context_safe_wrapper + Classical.add_context_unsafe_wrapper + Classical.del_context_unsafe_wrapper + +IMPORTANT NOTE: proof tools (methods etc.) need to use +local_simpset_of and local_claset_of to instead of the primitive +Simplifier.get_local_simpset and Classical.get_local_claset, +respectively, in order to see the context dependent fields! + + +*** System *** + +* Allow symlinks to all proper Isabelle executables (Isabelle, +isabelle, isatool etc.). + +* ISABELLE_DOC_FORMAT setting specifies preferred document format (for +isatool doc, isatool mkdir, display_drafts etc.). + +* isatool usedir: option -f allows specification of the ML file to be +used by Isabelle; default is ROOT.ML. + +* HOL: isatool dimacs2hol converts files in DIMACS CNF format +(containing Boolean satisfiability problems) into Isabelle/HOL +theories.