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

author | wenzelm |

Mon, 07 Jun 2010 11:42:54 +0200 | |

changeset 37354 | 865ad5634ed8 |

parent 37350 | 4c8642087c63 (current diff) |

parent 37353 | b6222a65bacf (diff) |

child 37355 | 1255ba99ed1e |

merged

--- a/ANNOUNCE Mon Jun 07 10:37:30 2010 +0200 +++ b/ANNOUNCE Mon Jun 07 11:42:54 2010 +0200 @@ -9,23 +9,24 @@ * Explicit proof terms for type class reasoning. -* Authentic syntax for *all* logical entities (type classes, type -constructors, term constants): provides simple and robust -correspondence between formal entities and concrete syntax. +* Robust treatment of concrete syntax for different logical entities; +mixfix syntax in local proof context. -* HOL: Package for constructing quotient types. +* Type declarations and notation within local theory context. + +* HOL: package for quotient types. -* HOL: Code generation now with simple concept for abstract -datatypes obeying invariants; applications for typical data structures -(e.g. search trees) can be found in the library. +* HOL code generation: simple concept for abstract datatypes obeying +invariants (e.g. red-black trees). -* HOL: New development of the Reals using Cauchy Sequences. +* HOL: new development of the Reals using Cauchy Sequences. -* HOL: Reorganization of abstract algebra type class hierarchy. +* HOL: reorganization of abstract algebra type class hierarchy. -* Commands 'types', 'typedecl' and 'typedef' now work within a local theory -context -- without introducing dependencies on parameters or -assumptions. +* HOL: substantial reorganization of main library and related tools. + +* HOLCF: reorganization of 'domain' package. + You may get Isabelle2009-2 from the following mirror sites:

--- a/NEWS Mon Jun 07 10:37:30 2010 +0200 +++ b/NEWS Mon Jun 07 11:42:54 2010 +0200 @@ -6,12 +6,6 @@ *** General *** -* Schematic theorem statements need to be explicitly markup as such, -via commands 'schematic_lemma', 'schematic_theorem', -'schematic_corollary'. Thus the relevance of the proof is made -syntactically clear, which impacts performance in a parallel or -asynchronous interactive environment. Minor INCOMPATIBILITY. - * Authentic syntax for *all* logical entities (type classes, type constructors, term constants): provides simple and robust correspondence between formal entities and concrete syntax. Within @@ -69,8 +63,19 @@ 'def', 'obtain' etc. or via the explicit 'write' command, which is similar to the 'notation' command in theory specifications. +* Discontinued unnamed infix syntax (legacy feature for many years) -- +need to specify constant name and syntax separately. Internal ML +datatype constructors have been renamed from InfixName to Infix etc. +Minor INCOMPATIBILITY. + +* Schematic theorem statements need to be explicitly markup as such, +via commands 'schematic_lemma', 'schematic_theorem', +'schematic_corollary'. Thus the relevance of the proof is made +syntactically clear, which impacts performance in a parallel or +asynchronous interactive environment. Minor INCOMPATIBILITY. + * Use of cumulative prems via "!" in some proof methods has been -discontinued (legacy feature). +discontinued (old legacy feature). * References 'trace_simp' and 'debug_simp' have been replaced by configuration options stored in the context. Enabling tracing (the @@ -92,20 +97,13 @@ *** Pure *** -* Predicates of locales introduced by classes carry a mandatory -"class" prefix. INCOMPATIBILITY. - -* Command 'code_reflect' allows to incorporate generated ML code into -runtime environment; replaces immature code_datatype antiquotation. -INCOMPATIBILITY. - -* Empty class specifications observe default sort. INCOMPATIBILITY. - -* Old 'axclass' command has been discontinued. Use 'class' instead. -INCOMPATIBILITY. - -* Code generator: simple concept for abstract datatypes obeying -invariants. +* Proofterms record type-class reasoning explicitly, using the +"unconstrain" operation internally. This eliminates all sort +constraints from a theorem and proof, introducing explicit +OFCLASS-premises. On the proof term level, this operation is +automatically applied at theorem boundaries, such that closed proofs +are always free of sort constraints. INCOMPATIBILITY for tools that +inspect proof terms. * Local theory specifications may depend on extra type variables that are not present in the result type -- arguments TYPE('a) :: 'a itself @@ -113,18 +111,28 @@ definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)" +* Predicates of locales introduced by classes carry a mandatory +"class" prefix. INCOMPATIBILITY. + +* Vacuous class specifications observe default sort. INCOMPATIBILITY. + +* Old 'axclass' command has been discontinued. INCOMPATIBILITY, use +'class' instead. + +* Command 'code_reflect' allows to incorporate generated ML code into +runtime environment; replaces immature code_datatype antiquotation. +INCOMPATIBILITY. + +* Code generator: simple concept for abstract datatypes obeying +invariants. + * Code generator: details of internal data cache have no impact on the user space functionality any longer. -* Methods unfold_locales and intro_locales ignore non-locale subgoals. -This is more appropriate for interpretations with 'where'. +* Methods "unfold_locales" and "intro_locales" ignore non-locale +subgoals. This is more appropriate for interpretations with 'where'. INCOMPATIBILITY. -* Discontinued unnamed infix syntax (legacy feature for many years) -- -need to specify constant name and syntax separately. Internal ML -datatype constructors have been renamed from InfixName to Infix etc. -Minor INCOMPATIBILITY. - * Command 'example_proof' opens an empty proof body. This allows to experiment with Isar, without producing any persistent result. @@ -139,24 +147,42 @@ * Command 'defaultsort' has been renamed to 'default_sort', it works within a local theory context. Minor INCOMPATIBILITY. -* Raw axioms/defs may no longer carry sort constraints, and raw defs -may no longer carry premises. User-level specifications are -transformed accordingly by Thm.add_axiom/add_def. - -* Proof terms: Type substitutions on proof constants now use canonical -order of type variables. INCOMPATIBILITY for tools working with proof -terms. - -* New operation Thm.unconstrainT eliminates all sort constraints from -a theorem and proof, introducing explicit OFCLASS-premises. On the -proof term level, this operation is automatically applied at PThm -boundaries, such that closed proofs are always free of sort -constraints. The old (axiomatic) unconstrain operation has been -discontinued. INCOMPATIBILITY for tools working with proof terms. - *** HOL *** +* Command 'typedef' now works within a local theory context -- without +introducing dependencies on parameters or assumptions, which is not +possible in Isabelle/Pure/HOL. Note that the logical environment may +contain multiple interpretations of local typedefs (with different +non-emptiness proofs), even in a global theory context. + +* New package for quotient types. Commands 'quotient_type' and +'quotient_definition' may be used for defining types and constants by +quotient constructions. An example is the type of integers created by +quotienting pairs of natural numbers: + + fun + intrel :: "(nat * nat) => (nat * nat) => bool" + where + "intrel (x, y) (u, v) = (x + v = u + y)" + + quotient_type int = "nat × nat" / intrel + by (auto simp add: equivp_def expand_fun_eq) + + quotient_definition + "0::int" is "(0::nat, 0::nat)" + +The method "lifting" can be used to lift of theorems from the +underlying "raw" type to the quotient type. The example +src/HOL/Quotient_Examples/FSet.thy includes such a quotient +construction and provides a reasoning infrastructure for finite sets. + +* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid +clash with new theory Quotient in Main HOL. + +* Moved the SMT binding into the main HOL session, eliminating +separate HOL-SMT session. + * List membership infix mem operation is only an input abbreviation. INCOMPATIBILITY. @@ -177,8 +203,8 @@ instead. INCOMPATIBILITY. * Dropped several real-specific versions of lemmas about floor and -ceiling; use the generic lemmas from Archimedean_Field.thy instead. -INCOMPATIBILITY. +ceiling; use the generic lemmas from theory "Archimedean_Field" +instead. INCOMPATIBILITY. floor_number_of_eq ~> floor_number_of le_floor_eq_number_of ~> number_of_le_floor @@ -218,26 +244,19 @@ provides abstract red-black tree type which is backed by "RBT_Impl" as implementation. INCOMPATIBILTY. -* Command 'typedef' now works within a local theory context -- without -introducing dependencies on parameters or assumptions, which is not -possible in Isabelle/Pure/HOL. Note that the logical environment may -contain multiple interpretations of local typedefs (with different -non-emptiness proofs), even in a global theory context. - * Theory Library/Coinductive_List has been removed -- superseded by AFP/thys/Coinductive. * Theory PReal, including the type "preal" and related operations, has been removed. INCOMPATIBILITY. -* Split off theory Big_Operators containing setsum, setprod, Inf_fin, -Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY. +* Split off theory "Big_Operators" containing setsum, setprod, +Inf_fin, Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY. * Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc. INCOMPATIBILITY. -* Constant Rat.normalize needs to be qualified. Minor -INCOMPATIBILITY. +* Constant Rat.normalize needs to be qualified. INCOMPATIBILITY. * New set of rules "ac_simps" provides combined assoc / commute rewrites for all interpretations of the appropriate generic locales. @@ -295,7 +314,7 @@ ordered_semiring_strict ~> linordered_semiring_strict The following slightly odd type classes have been moved to a - separate theory Library/Lattice_Algebras.thy: + separate theory Library/Lattice_Algebras: lordered_ab_group_add ~> lattice_ab_group_add lordered_ab_group_add_abs ~> lattice_ab_group_add_abs @@ -335,18 +354,16 @@ INTER_fold_inter ~> INFI_fold_inf UNION_fold_union ~> SUPR_fold_sup -* Theory Complete_Lattice: lemmas top_def and bot_def have been +* Theory "Complete_Lattice": lemmas top_def and bot_def have been replaced by the more convenient lemmas Inf_empty and Sup_empty. Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed by Inf_insert and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace former Inf_Univ and Sup_Univ. Lemmas inf_top_right and sup_bot_right subsume inf_top and sup_bot respectively. INCOMPATIBILITY. -* HOLogic.strip_psplit: types are returned in syntactic order, similar -to other strip and tuple operations. INCOMPATIBILITY. - * Reorganized theory Multiset: swapped notation of pointwise and multiset order: + - pointwise ordering is instance of class order with standard syntax <= and <; - multiset ordering has syntax <=# and <#; partial order properties @@ -357,10 +374,13 @@ generation; - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed. + Renamed: - multiset_eq_conv_count_eq -> multiset_ext_iff - multi_count_ext -> multiset_ext - diff_union_inverse2 -> diff_union_cancelR + + multiset_eq_conv_count_eq ~> multiset_ext_iff + multi_count_ext ~> multiset_ext + diff_union_inverse2 ~> diff_union_cancelR + INCOMPATIBILITY. * Theory Permutation: replaced local "remove" by List.remove1. @@ -369,9 +389,6 @@ * Theory List: added transpose. -* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid -clash with new theory Quotient in Main HOL. - * Library/Nat_Bijection.thy is a collection of bijective functions between nat and other types, which supersedes the older libraries Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy. INCOMPATIBILITY. @@ -452,8 +469,6 @@ "sharing_depth", and "show_skolems" options. INCOMPATIBILITY. - Removed "nitpick_intro" attribute. INCOMPATIBILITY. -* Moved the SMT binding into the HOL image. - *** HOLCF *** @@ -469,7 +484,7 @@ * Most definedness lemmas generated by the domain package (previously of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form like "foo$x = UU <-> x = UU", which works better as a simp rule. -Proof scripts that used definedness lemmas as intro rules may break, +Proofs that used definedness lemmas as intro rules may break, potential INCOMPATIBILITY. * Induction and casedist rules generated by the domain package now @@ -513,6 +528,38 @@ *** ML *** +* Antiquotations for basic formal entities: + + @{class NAME} -- type class + @{class_syntax NAME} -- syntax representation of the above + + @{type_name NAME} -- logical type + @{type_abbrev NAME} -- type abbreviation + @{nonterminal NAME} -- type of concrete syntactic category + @{type_syntax NAME} -- syntax representation of any of the above + + @{const_name NAME} -- logical constant (INCOMPATIBILITY) + @{const_abbrev NAME} -- abbreviated constant + @{const_syntax NAME} -- syntax representation of any of the above + +* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw +syntax constant (cf. 'syntax' command). + +* Antiquotation @{make_string} inlines a function to print arbitrary +values similar to the ML toplevel. The result is compiler dependent +and may fall back on "?" in certain situations. + +* Diagnostic commands 'ML_val' and 'ML_command' may refer to +antiquotations @{Isar.state} and @{Isar.goal}. This replaces impure +Isar.state() and Isar.goal(), which belong to the old TTY loop and do +not work with the asynchronous Isar document model. + +* Configuration options now admit dynamic default values, depending on +the context or even global references. + +* SHA1.digest digests strings according to SHA-1 (see RFC 3174). It +uses an efficient external library if available (for Poly/ML). + * Renamed some important ML structures, while keeping the old names for some time as aliases within the structure Legacy: @@ -541,32 +588,6 @@ Pretty.pp argument to merge, which is absent in the standard Theory_Data version. -* Antiquotations for basic formal entities: - - @{class NAME} -- type class - @{class_syntax NAME} -- syntax representation of the above - - @{type_name NAME} -- logical type - @{type_abbrev NAME} -- type abbreviation - @{nonterminal NAME} -- type of concrete syntactic category - @{type_syntax NAME} -- syntax representation of any of the above - - @{const_name NAME} -- logical constant (INCOMPATIBILITY) - @{const_abbrev NAME} -- abbreviated constant - @{const_syntax NAME} -- syntax representation of any of the above - -* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw -syntax constant (cf. 'syntax' command). - -* Antiquotation @{make_string} inlines a function to print arbitrary -values similar to the ML toplevel. The result is compiler dependent -and may fall back on "?" in certain situations. - -* Diagnostic commands 'ML_val' and 'ML_command' may refer to -antiquotations @{Isar.state} and @{Isar.goal}. This replaces impure -Isar.state() and Isar.goal(), which belong to the old TTY loop and do -not work with the asynchronous Isar document model. - * Sorts.certify_sort and derived "cert" operations for types and terms no longer minimize sorts. Thus certification at the boundary of the inference kernel becomes invariant under addition of class relations, @@ -586,15 +607,17 @@ to emphasize that these only work in a global situation (which is quite rare). -* Configuration options now admit dynamic default values, depending on -the context or even global references. - -* SHA1.digest digests strings according to SHA-1 (see RFC 3174). It -uses an efficient external library if available (for Poly/ML). - * Curried take and drop in library.ML; negative length is interpreted as infinity (as in chop). Subtle INCOMPATIBILITY. +* Proof terms: type substitutions on proof constants now use canonical +order of type variables. INCOMPATIBILITY for tools working with proof +terms. + +* Raw axioms/defs may no longer carry sort constraints, and raw defs +may no longer carry premises. User-level specifications are +transformed accordingly by Thm.add_axiom/add_def. + *** System *** @@ -3345,6 +3368,8 @@ * Real: proper support for ML code generation, including 'quickcheck'. Reals are implemented as arbitrary precision rationals. +* Real: new development using Cauchy Sequences. + * Hyperreal: Several constants that previously worked only for the reals have been generalized, so they now work over arbitrary vector spaces. Type annotations may need to be added in some cases; potential