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

author | wenzelm |

Thu, 02 Apr 2009 13:41:02 +0200 | |

changeset 30845 | 9a887484de53 |

parent 30828 | 50c8f55cde7f |

child 30846 | fd8ed5a39a8e |

misc cleanup and rearrangements for Isabelle2009 release;

--- a/NEWS Tue Mar 31 22:25:46 2009 +0200 +++ b/NEWS Thu Apr 02 13:41:02 2009 +0200 @@ -1,15 +1,11 @@ Isabelle NEWS -- history user-relevant changes ============================================== -New in this Isabelle version ----------------------------- +New in Isabelle2009 (April 2009) +-------------------------------- *** General *** -* The main reference manuals (isar-ref, implementation, system) have -been updated and extended. Formally checked references as hyperlinks -are now available in uniform manner. - * Simplified main Isabelle executables, with less surprises on case-insensitive file-systems (such as Mac OS). @@ -37,110 +33,31 @@ install -p ...", or use symlinks. * The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the -old ~/isabelle, which was slightly non-standard and apt cause -surprises on case-insensitive file-systems. +old ~/isabelle, which was slightly non-standard and apt to cause +surprises on case-insensitive file-systems (such as Mac OS). INCOMPATIBILITY, need to move existing ~/isabelle/etc, ~/isabelle/heaps, ~/isabelle/browser_info to the new place. Special care is required when using older releases of Isabelle. Note that ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any -Isabelle distribution. +Isabelle distribution, in order to use the new ~/.isabelle uniformly. * Proofs of fully specified statements are run in parallel on -multi-core systems. A speedup factor of 2-3 can be expected on a -regular 4-core machine, if the initial heap space is made reasonably -large (cf. Poly/ML option -H). [Poly/ML 5.2.1 or later] - -* Generalized Isar history, with support for linear undo, direct state -addressing etc. - -* Recovered hiding of consts, which was accidentally broken in -Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really -makes c inaccessible; consider using ``hide (open) const c'' instead. - -* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML -interface instead. - -* There is a new syntactic category "float_const" for signed decimal -fractions (e.g. 123.45 or -123.45). - -* New prover for coherent logic (see src/Tools/coherent.ML). +multi-core systems. A speedup factor of 2.5 to 3.2 can be expected on +a regular 4-core machine, if the initial heap space is made reasonably +large (cf. Poly/ML option -H). (Requires Poly/ML 5.2.1 or later.) + +* The main reference manuals ("isar-ref", "implementation", and +"system") have been updated and extended. Formally checked references +as hyperlinks are now available uniformly. + *** Pure *** -* Class declaration: sc. "base sort" must not be given in import list -any longer but is inferred from the specification. Particularly in HOL, -write - - class foo = ... instead of class foo = type + ... - -* Module moves in repository: - src/Pure/Tools/value.ML ~> src/Tools/ - src/Pure/Tools/quickcheck.ML ~> src/Tools/ - -* Slightly more coherent Pure syntax, with updated documentation in -isar-ref manual. Removed locales meta_term_syntax and -meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent, -INCOMPATIBILITY in rare situations. - -* Goal-directed proof now enforces strict proof irrelevance wrt. sort -hypotheses. Sorts required in the course of reasoning need to be -covered by the constraints in the initial statement, completed by the -type instance information of the background theory. Non-trivial sort -hypotheses, which rarely occur in practice, may be specified via -vacuous propositions of the form SORT_CONSTRAINT('a::c). For example: - - lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ... - -The result contains an implicit sort hypotheses as before -- -SORT_CONSTRAINT premises are eliminated as part of the canonical rule -normalization. - -* Changed defaults for unify configuration options: - - unify_trace_bound = 50 (formerly 25) - unify_search_bound = 60 (formerly 30) - -* Different bookkeeping for code equations (INCOMPATIBILITY): - - a) On theory merge, the last set of code equations for a particular - constant is taken (in accordance with the policy applied by other - parts of the code generator framework). - - b) Code equations stemming from explicit declarations (e.g. code - attribute) gain priority over default code equations stemming - from definition, primrec, fun etc. - -* Global versions of theorems stemming from classes do not carry a -parameter prefix any longer. INCOMPATIBILITY. - -* Dropped locale element "includes". This is a major INCOMPATIBILITY. -In existing theorem specifications replace the includes element by the -respective context elements of the included locale, omitting those -that are already present in the theorem specification. Multiple -assume elements of a locale should be replaced by a single one -involving the locale predicate. In the proof body, declarations (most -notably theorems) may be regained by interpreting the respective -locales in the proof context as required (command "interpret"). - -If using "includes" in replacement of a target solely because the -parameter types in the theorem are not as general as in the target, -consider declaring a new locale with additional type constraints on -the parameters (context element "constrains"). - -* Dropped "locale (open)". INCOMPATIBILITY. - -* Interpretation commands no longer attempt to simplify goal. -INCOMPATIBILITY: in rare situations the generated goal differs. Use -methods intro_locales and unfold_locales to clarify. - -* Interpretation commands no longer accept interpretation attributes. -INCOMPATBILITY. - -* Complete re-implementation of locales. INCOMPATIBILITY. The most -important changes are listed below. See the Tutorial on Locales for -details. +* Complete re-implementation of locales. INCOMPATIBILITY in several +respects. The most important changes are listed below. See the +Tutorial on Locales ("locales" manual) for details. - In locale expressions, instantiation replaces renaming. Parameters must be declared in a for clause. To aid compatibility with previous @@ -158,35 +75,116 @@ optional (syntax "name?:"). The default depends for plain "name:" depends on the situation where a locale expression is used: in commands 'locale' and 'sublocale' prefixes are optional, in -'interpretation' and 'interpret' prefixes are mandatory. Old-style +'interpretation' and 'interpret' prefixes are mandatory. The old implicit qualifiers derived from the parameter names of a locale are no longer generated. -- "sublocale l < e" replaces "interpretation l < e". The +- Command "sublocale l < e" replaces "interpretation l < e". The instantiation clause in "interpretation" and "interpret" (square brackets) is no longer available. Use locale expressions. -- When converting proof scripts, be sure to mandatory qualifiers in +- When converting proof scripts, mandatory qualifiers in 'interpretation' and 'interpret' should be retained by default, even -if this is an INCOMPATIBILITY compared to former behaviour. -Qualifiers in locale expressions range over a single locale instance -only. - -* Command 'instance': attached definitions no longer accepted. -INCOMPATIBILITY, use proper 'instantiation' target. - -* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. +if this is an INCOMPATIBILITY compared to former behavior. In the +worst case, use the "name?:" form for non-mandatory ones. Qualifiers +in locale expressions range over a single locale instance only. + +- Dropped locale element "includes". This is a major INCOMPATIBILITY. +In existing theorem specifications replace the includes element by the +respective context elements of the included locale, omitting those +that are already present in the theorem specification. Multiple +assume elements of a locale should be replaced by a single one +involving the locale predicate. In the proof body, declarations (most +notably theorems) may be regained by interpreting the respective +locales in the proof context as required (command "interpret"). + +If using "includes" in replacement of a target solely because the +parameter types in the theorem are not as general as in the target, +consider declaring a new locale with additional type constraints on +the parameters (context element "constrains"). + +- Discontinued "locale (open)". INCOMPATIBILITY. + +- Locale interpretation commands no longer attempt to simplify goal. +INCOMPATIBILITY: in rare situations the generated goal differs. Use +methods intro_locales and unfold_locales to clarify. + +- Locale interpretation commands no longer accept interpretation +attributes. INCOMPATIBILITY. + +* Class declaration: so-called "base sort" must not be given in import +list any longer, but is inferred from the specification. Particularly +in HOL, write + + class foo = ... + +instead of + + class foo = type + ... + +* Class target: global versions of theorems stemming do not carry a +parameter prefix any longer. INCOMPATIBILITY. + +* Class 'instance' command no longer accepts attached definitions. +INCOMPATIBILITY, use proper 'instantiation' target instead. + +* Recovered hiding of consts, which was accidentally broken in +Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really +makes c inaccessible; consider using ``hide (open) const c'' instead. + +* Slightly more coherent Pure syntax, with updated documentation in +isar-ref manual. Removed locales meta_term_syntax and +meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent, +INCOMPATIBILITY in rare situations. Note that &&& should not be used +directly in regular applications. + +* There is a new syntactic category "float_const" for signed decimal +fractions (e.g. 123.45 or -123.45). + +* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML +interface with 'setup' command instead. + +* Command 'local_setup' is similar to 'setup', but operates on a local +theory context. * The 'axiomatization' command now only works within a global theory context. INCOMPATIBILITY. -* New 'find_theorems' criterion "solves" matching theorems that -directly solve the current goal. - -* Auto solve feature for main theorem statements (cf. option in Proof -General Isabelle settings menu, disabled by default). Whenever a new -goal is stated, "find_theorems solves" is called; any theorems that -could solve the lemma directly are listed as part of the goal state. +* Goal-directed proof now enforces strict proof irrelevance wrt. sort +hypotheses. Sorts required in the course of reasoning need to be +covered by the constraints in the initial statement, completed by the +type instance information of the background theory. Non-trivial sort +hypotheses, which rarely occur in practice, may be specified via +vacuous propositions of the form SORT_CONSTRAINT('a::c). For example: + + lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ... + +The result contains an implicit sort hypotheses as before -- +SORT_CONSTRAINT premises are eliminated as part of the canonical rule +normalization. + +* Generalized Isar history, with support for linear undo, direct state +addressing etc. + +* Changed defaults for unify configuration options: + + unify_trace_bound = 50 (formerly 25) + unify_search_bound = 60 (formerly 30) + +* Different bookkeeping for code equations (INCOMPATIBILITY): + + a) On theory merge, the last set of code equations for a particular + constant is taken (in accordance with the policy applied by other + parts of the code generator framework). + + b) Code equations stemming from explicit declarations (e.g. code + attribute) gain priority over default code equations stemming + from definition, primrec, fun etc. + +* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. + +* Unified theorem tables for both code code generators. Thus [code +func] has disappeared and only [code] remains. INCOMPATIBILITY. * Command 'find_consts' searches for constants based on type and name patterns, e.g. @@ -200,8 +198,15 @@ find_consts strict: "_ => bool" name: "Int" -"int => int" -* Command 'local_setup' is similar to 'setup', but operates on a local -theory context. +* New 'find_theorems' criterion "solves" matches theorems that +directly solve the current goal (modulo higher-order unification). + +* Auto solve feature for main theorem statements: whenever a new goal +is stated, "find_theorems solves" is called; any theorems that could +solve the lemma directly are listed as part of the goal state. +Cf. associated options in Proof General Isabelle settings menu, +enabled by default, with reasonable timeout for pathological cases of +higher-order unification. *** Document preparation *** @@ -213,34 +218,84 @@ *** HOL *** -* Theory Library/Polynomial.thy defines an abstract type 'a poly of -univariate polynomials with coefficients of type 'a. In addition to -the standard ring operations, it also supports div and mod. Code -generation is also supported, using list-style constructors. - -* Theory Library/Inner_Product.thy defines a class of real_inner for -real inner product spaces, with an overloaded operation inner :: 'a => -'a => real. Class real_inner is a subclass of real_normed_vector from -RealVector.thy. - -* Theory Library/Product_Vector.thy provides instances for the product -type 'a * 'b of several classes from RealVector.thy and -Inner_Product.thy. Definitions of addition, subtraction, scalar -multiplication, norms, and inner products are included. - -* Theory Library/Bit.thy defines the field "bit" of integers modulo 2. -In addition to the field operations, numerals and case syntax are also -supported. - -* Theory Library/Diagonalize.thy provides constructive version of -Cantor's first diagonalization argument. - -* New predicate "strict_mono" classifies strict functions on partial orders. -With strict functions on linear orders, reasoning about (in)equalities is -facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less". - -* Some set operations are now proper qualified constants with authentic syntax. -INCOMPATIBILITY: +* Integrated main parts of former image HOL-Complex with HOL. Entry +points Main and Complex_Main remain as before. + +* Logic image HOL-Plain provides a minimal HOL with the most important +tools available (inductive, datatype, primrec, ...). This facilitates +experimentation and tool development. Note that user applications +(and library theories) should never refer to anything below theory +Main, as before. + +* Logic image HOL-Main stops at theory Main, and thus facilitates +experimentation due to shorter build times. + +* Logic image HOL-NSA contains theories of nonstandard analysis which +were previously part of former HOL-Complex. Entry point Hyperreal +remains valid, but theories formerly using Complex_Main should now use +new entry point Hypercomplex. + +* Generic ATP manager for Sledgehammer, based on ML threads instead of +Posix processes. Avoids potentially expensive forking of the ML +process. New thread-based implementation also works on non-Unix +platforms (Cygwin). Provers are no longer hardwired, but defined +within the theory via plain ML wrapper functions. Basic Sledgehammer +commands are covered in the isar-ref manual. + +* Wrapper scripts for remote SystemOnTPTP service allows to use +sledgehammer without local ATP installation (Vampire etc.). Other +provers may be included via suitable ML wrappers, see also +src/HOL/ATP_Linkup.thy. + +* ATP selection (E/Vampire/Spass) is now via Proof General's settings +menu. + +* The metis method no longer fails because the theorem is too trivial +(contains the empty clause). + +* The metis method now fails in the usual manner, rather than raising +an exception, if it determines that it cannot prove the theorem. + +* Method "coherent" implements a prover for coherent logic (see also +src/Tools/coherent.ML). + +* Constants "undefined" and "default" replace "arbitrary". Usually +"undefined" is the right choice to replace "arbitrary", though +logically there is no difference. INCOMPATIBILITY. + +* Command "value" now integrates different evaluation mechanisms. The +result of the first successful evaluation mechanism is printed. In +square brackets a particular named evaluation mechanisms may be +specified (currently, [SML], [code] or [nbe]). See further +src/HOL/ex/Eval_Examples.thy. + +* Normalization by evaluation now allows non-leftlinear equations. +Declare with attribute [code nbe]. + +* Methods "case_tac" and "induct_tac" now refer to the very same rules +as the structured Isar versions "cases" and "induct", cf. the +corresponding "cases" and "induct" attributes. Mutual induction rules +are now presented as a list of individual projections +(e.g. foo_bar.inducts for types foo and bar); the old format with +explicit HOL conjunction is no longer supported. INCOMPATIBILITY, in +rare situations a different rule is selected --- notably nested tuple +elimination instead of former prod.exhaust: use explicit (case_tac t +rule: prod.exhaust) here. + +* Attributes "cases", "induct", "coinduct" support "del" option. + +* Removed fact "case_split_thm", which duplicates "case_split". + +* The option datatype has been moved to a new theory Option. Renamed +option_map to Option.map, and o2s to Option.set, INCOMPATIBILITY. + +* New predicate "strict_mono" classifies strict functions on partial +orders. With strict functions on linear orders, reasoning about +(in)equalities is facilitated by theorems "strict_mono_eq", +"strict_mono_less_eq" and "strict_mono_less". + +* Some set operations are now proper qualified constants with +authentic syntax. INCOMPATIBILITY: op Int ~> Set.Int op Un ~> Set.Un @@ -251,26 +306,28 @@ {} ~> Set.empty UNIV ~> Set.UNIV -* Class complete_lattice with operations Inf, Sup, INFI, SUPR now in theory -Set. - -* Auxiliary class "itself" has disappeared -- classes without any parameter -are treated as expected by the 'class' command. +* Class complete_lattice with operations Inf, Sup, INFI, SUPR now in +theory Set. + +* Auxiliary class "itself" has disappeared -- classes without any +parameter are treated as expected by the 'class' command. * Leibnitz's Series for Pi and the arcus tangens and logarithm series. -* Common decision procedures (Cooper, MIR, Ferrack, Approximation, Dense_Linear_Order) -now in directory HOL/Decision_Procs. - -* Theory HOL/Decision_Procs/Approximation.thy provides the new proof method -"approximation". It proves formulas on real values by using interval arithmetic. -In the formulas are also the transcendental functions sin, cos, tan, atan, ln, -exp and the constant pi are allowed. For examples see -HOL/Descision_Procs/ex/Approximation_Ex.thy. +* Common decision procedures (Cooper, MIR, Ferrack, Approximation, +Dense_Linear_Order) are now in directory HOL/Decision_Procs. + +* Theory src/HOL/Decision_Procs/Approximation provides the new proof +method "approximation". It proves formulas on real values by using +interval arithmetic. In the formulas are also the transcendental +functions sin, cos, tan, atan, ln, exp and the constant pi are +allowed. For examples see +src/HOL/Descision_Procs/ex/Approximation_Ex.thy. * Theory "Reflection" now resides in HOL/Library. -* Entry point to Word library now simply named "Word". INCOMPATIBILITY. +* Entry point to Word library now simply named "Word". +INCOMPATIBILITY. * Made source layout more coherent with logical distribution structure: @@ -327,82 +384,65 @@ src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL -* If methods "eval" and "evaluation" encounter a structured proof state -with !!/==>, only the conclusion is evaluated to True (if possible), -avoiding strange error messages. - -* Simplifier: simproc for let expressions now unfolds if bound variable -occurs at most once in let expression body. INCOMPATIBILITY. - -* New attribute "arith" for facts that should always be used automaticaly -by arithmetic. It is intended to be used locally in proofs, eg -assumes [arith]: "x > 0" +* If methods "eval" and "evaluation" encounter a structured proof +state with !!/==>, only the conclusion is evaluated to True (if +possible), avoiding strange error messages. + +* Method "sizechange" automates termination proofs using (a +modification of) the size-change principle. Requires SAT solver. See +src/HOL/ex/Termination.thy for examples. + +* Simplifier: simproc for let expressions now unfolds if bound +variable occurs at most once in let expression body. INCOMPATIBILITY. + +* Method "arith": Linear arithmetic now ignores all inequalities when +fast_arith_neq_limit is exceeded, instead of giving up entirely. + +* New attribute "arith" for facts that should always be used +automatically by arithmetic. It is intended to be used locally in +proofs, e.g. + + assumes [arith]: "x > 0" + Global usage is discouraged because of possible performance impact. -* New classes "top" and "bot" with corresponding operations "top" and "bot" -in theory Orderings; instantiation of class "complete_lattice" requires -instantiation of classes "top" and "bot". INCOMPATIBILITY. - -* Changed definition lemma "less_fun_def" in order to provide an instance -for preorders on functions; use lemma "less_le" instead. INCOMPATIBILITY. - -* Unified theorem tables for both code code generators. Thus -[code func] has disappeared and only [code] remains. INCOMPATIBILITY. - -* Constants "undefined" and "default" replace "arbitrary". Usually -"undefined" is the right choice to replace "arbitrary", though logically -there is no difference. INCOMPATIBILITY. - -* Generic ATP manager for Sledgehammer, based on ML threads instead of -Posix processes. Avoids potentially expensive forking of the ML -process. New thread-based implementation also works on non-Unix -platforms (Cygwin). Provers are no longer hardwired, but defined -within the theory via plain ML wrapper functions. Basic Sledgehammer -commands are covered in the isar-ref manual. - -* Wrapper scripts for remote SystemOnTPTP service allows to use -sledgehammer without local ATP installation (Vampire etc.). Other -provers may be included via suitable ML wrappers, see also -src/HOL/ATP_Linkup.thy. - -* Normalization by evaluation now allows non-leftlinear equations. -Declare with attribute [code nbe]. - -* Command "value" now integrates different evaluation -mechanisms. The result of the first successful evaluation mechanism -is printed. In square brackets a particular named evaluation -mechanisms may be specified (currently, [SML], [code] or [nbe]). See -further src/HOL/ex/Eval_Examples.thy. - -* New method "sizechange" to automate termination proofs using (a -modification of) the size-change principle. Requires SAT solver. See -src/HOL/ex/Termination.thy for examples. - -* HOL/Orderings: class "wellorder" moved here, with explicit induction -rule "less_induct" as assumption. For instantiation of "wellorder" by -means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY. - -* HOL/Orderings: added class "preorder" as superclass of "order". +* New classes "top" and "bot" with corresponding operations "top" and +"bot" in theory Orderings; instantiation of class "complete_lattice" +requires instantiation of classes "top" and "bot". INCOMPATIBILITY. + +* Changed definition lemma "less_fun_def" in order to provide an +instance for preorders on functions; use lemma "less_le" instead. +INCOMPATIBILITY. + +* Theory Orderings: class "wellorder" moved here, with explicit +induction rule "less_induct" as assumption. For instantiation of +"wellorder" by means of predicate "wf", use rule wf_wellorderI. +INCOMPATIBILITY. + +* Theory Orderings: added class "preorder" as superclass of "order". INCOMPATIBILITY: Instantiation proofs for order, linorder etc. slightly changed. Some theorems named order_class.* now named preorder_class.*. -* HOL/Relation: -Renamed "refl" to "refl_on", "reflexive" to "refl, "diag" to "Id_on". - -* HOL/Finite_Set: added a new fold combinator of type +* Theory Relation: renamed "refl" to "refl_on", "reflexive" to "refl, +"diag" to "Id_on". + +* Theory Finite_Set: added a new fold combinator of type + ('a => 'b => 'b) => 'b => 'a set => 'b -Occasionally this is more convenient than the old fold combinator which is -now defined in terms of the new one and renamed to fold_image. - -* HOL/Ring_and_Field and HOL/OrderedGroup: The lemmas "group_simps" and -"ring_simps" have been replaced by "algebra_simps" (which can be extended with -further lemmas!). At the moment both still exist but the former will disappear -at some point. - -* HOL/Power: Lemma power_Suc is now declared as a simp rule in class -recpower. Type-specific simp rules for various recpower types have -been removed. INCOMPATIBILITY. Rename old lemmas as follows: + +Occasionally this is more convenient than the old fold combinator +which is now defined in terms of the new one and renamed to +fold_image. + +* Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps" +and "ring_simps" have been replaced by "algebra_simps" (which can be +extended with further lemmas!). At the moment both still exist but +the former will disappear at some point. + +* Theory Power: Lemma power_Suc is now declared as a simp rule in +class recpower. Type-specific simp rules for various recpower types +have been removed. INCOMPATIBILITY, rename old lemmas as follows: rat_power_0 -> power_0 rat_power_Suc -> power_Suc @@ -413,7 +453,7 @@ power_poly_0 -> power_0 power_poly_Suc -> power_Suc -* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been +* Theories Ring_and_Field and Divides: Definition of "op dvd" has been moved to separate class dvd in Ring_and_Field; a couple of lemmas on dvd has been generalized to class comm_semiring_1. Likewise a bunch of lemmas from Divides has been generalized from nat to class @@ -428,9 +468,9 @@ mult_div ~> div_mult_self2_is_id mult_mod ~> mod_mult_self2_is_0 -* HOL/IntDiv: removed many lemmas that are instances of class-based -generalizations (from Divides and Ring_and_Field). -INCOMPATIBILITY. Rename old lemmas as follows: +* Theory IntDiv: removed many lemmas that are instances of class-based +generalizations (from Divides and Ring_and_Field). INCOMPATIBILITY, +rename old lemmas as follows: dvd_diff -> nat_dvd_diff dvd_zminus_iff -> dvd_minus_iff @@ -478,11 +518,38 @@ zdvd_1_left -> one_dvd zminus_dvd_iff -> minus_dvd_iff -* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, +* Theory Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. + +* The real numbers offer decimal input syntax: 12.34 is translated +into 1234/10^2. This translation is not reversed upon output. + +* Theory Library/Polynomial defines an abstract type 'a poly of +univariate polynomials with coefficients of type 'a. In addition to +the standard ring operations, it also supports div and mod. Code +generation is also supported, using list-style constructors. + +* Theory Library/Inner_Product defines a class of real_inner for real +inner product spaces, with an overloaded operation inner :: 'a => 'a +=> real. Class real_inner is a subclass of real_normed_vector from +theory RealVector. + +* Theory Library/Product_Vector provides instances for the product +type 'a * 'b of several classes from RealVector and Inner_Product. +Definitions of addition, subtraction, scalar multiplication, norms, +and inner products are included. + +* Theory Library/Bit defines the field "bit" of integers modulo 2. In +addition to the field operations, numerals and case syntax are also +supported. + +* Theory Library/Diagonalize provides constructive version of Cantor's +first diagonalization argument. + +* Theory Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, zlcm (for int); carried together from various gcd/lcm developements in -the HOL Distribution. zgcd and zlcm replace former igcd and ilcm; -corresponding theorems renamed accordingly. INCOMPATIBILITY. To -recover tupled syntax, use syntax declarations like: +the HOL Distribution. Constants zgcd and zlcm replace former igcd and +ilcm; corresponding theorems renamed accordingly. INCOMPATIBILITY, +may recover tupled syntax as follows: hide (open) const gcd abbreviation gcd where @@ -490,54 +557,24 @@ notation (output) GCD.gcd ("gcd '(_, _')") -(analogously for lcm, zgcd, zlcm). - -* HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. - -* The real numbers offer decimal input syntax: 12.34 is translated into - 1234/10^2. This translation is not reversed upon output. - -* New ML antiquotation @{code}: takes constant as argument, generates +The same works for lcm, zgcd, zlcm. + +* Theory Library/Nat_Infinity: added addition, numeral syntax and more +instantiations for algebraic structures. Removed some duplicate +theorems. Changes in simp rules. INCOMPATIBILITY. + +* ML antiquotation @{code} takes a constant as argument and generates corresponding code in background and inserts name of the corresponding resulting ML value/function/datatype constructor binding in place. All occurrences of @{code} with a single ML block are generated simultaneously. Provides a generic and safe interface for -instrumentalizing code generation. See HOL/Decision_Procs/Ferrack for -a more ambitious application. In future you ought refrain from ad-hoc -compiling generated SML code on the ML toplevel. Note that (for technical -reasons) @{code} cannot refer to constants for which user-defined -serializations are set. Refer to the corresponding ML counterpart -directly in that cases. - -* Integrated image HOL-Complex with HOL. Entry points Main.thy and -Complex_Main.thy remain as they are. - -* New image HOL-Plain provides a minimal HOL with the most important -tools available (inductive, datatype, primrec, ...). By convention -the corresponding theory Plain should be ancestor of every further -(library) theory. Some library theories now have ancestor Plain -(instead of Main), thus theory Main occasionally has to be imported -explicitly. - -* The metis method now fails in the usual manner, rather than raising -an exception, if it determines that it cannot prove the theorem. - -* The metis method no longer fails because the theorem is too trivial -(contains the empty clause). - -* Methods "case_tac" and "induct_tac" now refer to the very same rules -as the structured Isar versions "cases" and "induct", cf. the -corresponding "cases" and "induct" attributes. Mutual induction rules -are now presented as a list of individual projections -(e.g. foo_bar.inducts for types foo and bar); the old format with -explicit HOL conjunction is no longer supported. INCOMPATIBILITY, in -rare situations a different rule is selected --- notably nested tuple -elimination instead of former prod.exhaust: use explicit (case_tac t -rule: prod.exhaust) here. - -* Attributes "cases", "induct", "coinduct" support "del" option. - -* Removed fact "case_split_thm", which duplicates "case_split". +instrumentalizing code generation. See +src/HOL/Decision_Procs/Ferrack.thy for a more ambitious application. +In future you ought to refrain from ad-hoc compiling generated SML +code on the ML toplevel. Note that (for technical reasons) @{code} +cannot refer to constants for which user-defined serializations are +set. Refer to the corresponding ML counterpart directly in that +cases. * Command 'rep_datatype': instead of theorem names the command now takes a list of terms denoting the constructors of the type to be @@ -551,19 +588,6 @@ Suc_Suc_eq ~> nat.inject Suc_not_Zero Zero_not_Suc ~> nat.distinct -* The option datatype has been moved to a new theory HOL/Option.thy. -Renamed option_map to Option.map, and o2s to Option.set. - -* Library/Nat_Infinity: added addition, numeral syntax and more -instantiations for algebraic structures. Removed some duplicate -theorems. Changes in simp rules. INCOMPATIBILITY. - -* ATP selection (E/Vampire/Spass) is now via Proof General's settings -menu. - -* Linear arithmetic now ignores all inequalities when -fast_arith_neq_limit is exceeded, instead of giving up entirely. - *** HOL-Algebra *** @@ -573,11 +597,12 @@ * New theory of factorial domains. -* Units_l_inv and Units_r_inv are now simprules by default. +* Units_l_inv and Units_r_inv are now simp rules by default. INCOMPATIBILITY. Simplifier proof that require deletion of l_inv and/or r_inv will now also require deletion of these lemmas. -* Renamed the following theorems. INCOMPATIBILITY. +* Renamed the following theorems, INCOMPATIBILITY: + UpperD ~> Upper_memD LowerD ~> Lower_memD least_carrier ~> least_closed @@ -587,19 +612,6 @@ one_not_zero ~> carrier_one_not_zero (collision with assumption) -*** HOL-NSA *** - -* Created new image HOL-NSA, containing theories of nonstandard -analysis which were previously part of HOL-Complex. Entry point -Hyperreal.thy remains valid, but theories formerly using -Complex_Main.thy should now use new entry point Hypercomplex.thy. - - -*** ZF *** - -* Proof of Zorn's Lemma for partial orders. - - *** HOLCF *** * Reimplemented the simplification procedure for proving continuity @@ -612,23 +624,47 @@ old one could solve, and "simp add: cont2cont_LAM" may be necessary. Potential INCOMPATIBILITY. -* The syntax of the fixrec package has changed. The specification -syntax now conforms in style to definition, primrec, function, etc. -See HOLCF/ex/Fixrec_ex.thy for examples. INCOMPATIBILITY. +* The syntax of the fixrec package now conforms to the general +specification format of inductive, primrec, function, etc. See +src/HOLCF/ex/Fixrec_ex.thy for examples. INCOMPATIBILITY. + + +*** ZF *** + +* Proof of Zorn's Lemma for partial orders. *** ML *** +* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for +Poly/ML 5.2.1 or later. Important note: the TimeLimit facility +depends on multithreading, so timouts will not work before Poly/ML +5.2.1! + * High-level support for concurrent ML programming, see src/Pure/Cuncurrent. The data-oriented model of "future values" is particularly convenient to organize independent functional computations. The concept of "synchronized variables" provides a higher-order interface for components with shared state, avoiding the -delicate details of mutexes and condition variables. [Poly/ML 5.2.1 -or later] +delicate details of mutexes and condition variables. (Requires +Poly/ML 5.2.1 or later.) + +* ML bindings produced via Isar commands are stored within the Isar +context (theory or proof). Consequently, commands like 'use' and 'ML' +become thread-safe and work with undo as expected (concerning +top-level bindings, not side-effects on global references). +INCOMPATIBILITY, need to provide proper Isar context when invoking the +compiler at runtime; really global bindings need to be given outside a +theory. (Requires Poly/ML 5.2 or later.) + +* Command 'ML_prf' is analogous to 'ML' but works within a proof +context. Top-level ML bindings are stored within the proof context in +a purely sequential fashion, disregarding the nested proof structure. +ML bindings introduced by 'ML_prf' are discarded at the end of the +proof. (Requires Poly/ML 5.2 or later.) * Simplified ML attribute and method setup, cf. functions Attrib.setup -and Method.setup, as well as commands 'attribute_setup' and +and Method.setup, as well as Isar commands 'attribute_setup' and 'method_setup'. INCOMPATIBILITY for 'method_setup', need to simplify existing code accordingly, or use plain 'setup' together with old Method.add_method. @@ -640,52 +676,27 @@ accordingly. Note that extra performance may be gained by producing the cterm carefully, avoiding slow Thm.cterm_of. -* ML bindings produced via Isar commands are stored within the Isar -context (theory or proof). Consequently, commands like 'use' and 'ML' -become thread-safe and work with undo as expected (concerning -top-level bindings, not side-effects on global references). -INCOMPATIBILITY, need to provide proper Isar context when invoking the -compiler at runtime; really global bindings need to be given outside a -theory. [Poly/ML 5.2 or later] - -* Command 'ML_prf' is analogous to 'ML' but works within a proof -context. Top-level ML bindings are stored within the proof context in -a purely sequential fashion, disregarding the nested proof structure. -ML bindings introduced by 'ML_prf' are discarded at the end of the -proof. [Poly/ML 5.2 or later] - -* Generic Toplevel.add_hook interface allows to analyze the result of -transactions. E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML -for theorem dependency output of transactions resulting in a new -theory state. +* Simplified interface for defining document antiquotations via +ThyOutput.antiquotation, ThyOutput.output, and optionally +ThyOutput.maybe_pretty_source. INCOMPATIBILITY, need to simplify user +antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common +examples. * More systematic treatment of long names, abstract name bindings, and name space operations. Basic operations on qualified names have been move from structure NameSpace to Long_Name, e.g. Long_Name.base_name, Long_Name.append. Old type bstring has been mostly replaced by abstract type binding (see structure Binding), which supports precise -qualification (by packages and local theory targets), as well as -proper tracking of source positions. INCOMPATIBILITY, need to wrap -old bstring values into Binding.name, or better pass through abstract +qualification by packages and local theory targets, as well as proper +tracking of source positions. INCOMPATIBILITY, need to wrap old +bstring values into Binding.name, or better pass through abstract bindings everywhere. See further src/Pure/General/long_name.ML, src/Pure/General/binding.ML and src/Pure/General/name_space.ML -* Simplified interface for defining document antiquotations via -ThyOutput.antiquotation, ThyOutput.output, and optionally -ThyOutput.maybe_pretty_source. INCOMPATIBILITY, need to simplify user -antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common -examples. - * Result facts (from PureThy.note_thms, ProofContext.note_thms, LocalTheory.note etc.) now refer to the *full* internal name, not the bstring as before. INCOMPATIBILITY, not detected by ML type-checking! -* Rules and tactics that read instantiations (read_instantiate, -res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof -context, which is required for parsing and type-checking. Moreover, -the variables are specified as plain indexnames, not string encodings -thereof. INCOMPATIBILITY. - * Disposed old type and term read functions (Sign.read_def_typ, Sign.read_typ, Sign.read_def_terms, Sign.read_term, Thm.read_def_cterms, Thm.read_cterm etc.). INCOMPATIBILITY, should @@ -699,9 +710,21 @@ embedded ML text, or local_simpset_of with a proper context passed as explicit runtime argument. -* Antiquotations: block-structured compilation context indicated by +* Rules and tactics that read instantiations (read_instantiate, +res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof +context, which is required for parsing and type-checking. Moreover, +the variables are specified as plain indexnames, not string encodings +thereof. INCOMPATIBILITY. + +* Generic Toplevel.add_hook interface allows to analyze the result of +transactions. E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML +for theorem dependency output of transactions resulting in a new +theory state. + +* ML antiquotations: block-structured compilation context indicated by \<lbrace> ... \<rbrace>; additional antiquotation forms: + @{binding name} - basic name binding @{let ?pat = term} - term abbreviation (HO matching) @{note name = fact} - fact abbreviation @{thm fact} - singleton fact (with attributes) @@ -715,9 +738,6 @@ *** System *** -* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for -Poly/ML 5.2.1 or later. - * The Isabelle "emacs" tool provides a specific interface to invoke Proof General / Emacs, with more explicit failure if that is not installed (the old isabelle-interface script silently falls back on @@ -729,13 +749,13 @@ Isabelle/lib/jedit/plugin for a minimal example. (The obsolete Java process wrapper has been discontinued.) -* Status messages (with exact source position information) are +* Added homegrown Isabelle font with unicode layout, see lib/fonts. + +* Various status messages (with exact source position information) are emitted, if proper markup print mode is enabled. This allows user-interface components to provide detailed feedback on internal prover operations. -* Homegrown Isabelle font with unicode layout, see Isabelle/lib/fonts. - New in Isabelle2008 (June 2008)