wenzelm@5363: Isabelle NEWS -- history user-relevant changes wenzelm@5363: ============================================== wenzelm@2553: wenzelm@25464: New in this Isabelle version wenzelm@25464: ---------------------------- wenzelm@25464: wenzelm@25522: *** General *** wenzelm@25522: wenzelm@25579: * Syntax: symbol \ is now considered a letter. Potential wenzelm@25579: INCOMPATIBILITY in identifier syntax etc. wenzelm@25579: wenzelm@25579: * Outer syntax: string tokens may contain arbitrary character codes wenzelm@25579: specified via 3 decimal digits (as in SML). E.g. "foo\095bar" for wenzelm@25579: "foo_bar". wenzelm@25522: wenzelm@26006: * Outer syntax: string tokens no longer admit escaped white space, wenzelm@26006: which was an accidental (undocumented) feature. INCOMPATIBILITY, use wenzelm@26006: white space directly. wenzelm@26006: wenzelm@25994: * Theory loader: use_thy (and similar operations) no longer set the wenzelm@25994: implicit ML context, which was occasionally hard to predict and in wenzelm@25994: conflict with concurrency. INCOMPATIBILITY, use ML within Isar which wenzelm@25994: provides a proper context already. wenzelm@25994: wenzelm@26323: * Theory loader: old-style ML proof scripts being *attached* to a thy wenzelm@26323: file are no longer supported. INCOMPATIBILITY, regular 'uses' and wenzelm@26323: 'use' within a theory file will do the job. wenzelm@26323: wenzelm@25522: haftmann@25502: *** Pure *** haftmann@25502: wenzelm@25970: * Instantiation target allows for simultaneous specification of class wenzelm@25970: instance operations together with an instantiation proof. wenzelm@25970: Type-checking phase allows to refer to class operations uniformly. wenzelm@25970: See HOL/Complex/Complex.thy for an Isar example and wenzelm@26180: HOL/Library/Eval.thy for an ML example. haftmann@25502: wenzelm@26201: * Indexing of literal facts: be more serious about including only wenzelm@26201: facts from the visible specification/proof context, but not the wenzelm@26201: background context (locale etc.). Affects `prop` notation and method wenzelm@26201: "fact". INCOMPATIBILITY: need to name facts explicitly in rare wenzelm@26201: situations. wenzelm@26201: haftmann@25502: wenzelm@25464: *** HOL *** wenzelm@25464: wenzelm@26335: * Theory Nat: removed redundant lemmas that merely duplicate lemmas of wenzelm@26335: the same name in theory Orderings: wenzelm@26335: wenzelm@26335: less_trans wenzelm@26335: less_linear wenzelm@26335: le_imp_less_or_eq wenzelm@26335: le_less_trans wenzelm@26335: less_le_trans wenzelm@26335: less_not_sym wenzelm@26335: less_asym wenzelm@26335: wenzelm@26335: Renamed less_imp_le to less_imp_le_nat, and less_irrefl to wenzelm@26335: less_irrefl_nat. Potential INCOMPATIBILITY due to more general types wenzelm@26335: and different variable names. wenzelm@26315: haftmann@26231: * Library/Option_ord.thy: Canonical order on option type. haftmann@26231: krauss@26197: * Library/RBT.thy: New theory of red-black trees, an efficient krauss@26197: implementation of finite maps. krauss@26197: haftmann@26231: * Library/Countable.thy: Type class for countable types. haftmann@26231: wenzelm@26180: * Theory Int: The representation of numerals has changed. The infix wenzelm@26180: operator BIT and the bit datatype with constructors B0 and B1 have wenzelm@26180: disappeared. INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in wenzelm@26180: place of "x BIT bit.B0" and "y BIT bit.B1", respectively. Theorems wenzelm@26180: involving BIT, B0, or B1 have been renamed with "Bit0" or "Bit1" wenzelm@26180: accordingly. wenzelm@26180: wenzelm@26180: * Theory Nat: definition of <= and < on natural numbers no longer wenzelm@26180: depend on well-founded relations. INCOMPATIBILITY. Definitions wenzelm@26180: le_def and less_def have disappeared. Consider lemmas not_less wenzelm@26180: [symmetric, where ?'a = nat] and less_eq [symmetric] instead. wenzelm@26180: wenzelm@26180: * Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin wenzelm@26180: (whose purpose mainly is for various fold_set functionals) have been wenzelm@26180: abandoned in favour of the existing algebraic classes wenzelm@26180: ab_semigroup_mult, comm_monoid_mult, ab_semigroup_idem_mult, wenzelm@26180: lower_semilattice (resp. upper_semilattice) and linorder. haftmann@26139: INCOMPATIBILITY. haftmann@26041: wenzelm@26180: * Theory Transitive_Closure: induct and cases rules now declare proper wenzelm@26180: case_names ("base" and "step"). INCOMPATIBILITY. wenzelm@26180: wenzelm@26180: * Theorem Inductive.lfp_ordinal_induct generalized to complete wenzelm@26180: lattices. The form set-specific version is available as wenzelm@26180: Inductive.lfp_ordinal_induct_set. haftmann@26013: haftmann@25961: * Theorems "power.simps" renamed to "power_int.simps". haftmann@25961: wenzelm@26180: * Class semiring_div provides basic abstract properties of semirings haftmann@25942: with division and modulo operations. Subsumes former class dvd_mod. haftmann@25942: wenzelm@26180: * Merged theories IntDef, Numeral and IntArith into unified theory wenzelm@26180: Int. INCOMPATIBILITY. wenzelm@26180: wenzelm@26180: * Theory Library/Code_Index: type "index" now represents natural wenzelm@26180: numbers rather than integers. INCOMPATIBILITY. wenzelm@26180: wenzelm@26180: * New class "uminus" with operation "uminus" (split of from class wenzelm@26180: "minus" which now only has operation "minus", binary). haftmann@25919: INCOMPATIBILITY. haftmann@25919: haftmann@25557: * New primrec package. Specification syntax conforms in style to wenzelm@26180: definition/function/.... No separate induction rule is provided. The wenzelm@26180: "primrec" command distinguishes old-style and new-style specifications haftmann@25599: by syntax. The former primrec package is now named OldPrimrecPackage. haftmann@25609: When adjusting theories, beware: constants stemming for new-style haftmann@25609: primrec specifications have authentic syntax. haftmann@25557: wenzelm@25522: * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}. wenzelm@25522: wenzelm@26180: * Library/ListVector: new theory of arithmetic vector operations. nipkow@25900: wenzelm@25522: * Constants "card", "internal_split", "option_map" now with authentic haftmann@25919: syntax. INCOMPATIBILITY. wenzelm@25522: wenzelm@25522: * Definitions subset_def, psubset_def, set_diff_def, Compl_def, wenzelm@25522: le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def, wenzelm@25522: sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def, wenzelm@25522: Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def, wenzelm@25522: Sup_set_def, le_def, less_def, option_map_def now with object haftmann@25919: equality. INCOMPATIBILITY. wenzelm@25464: wenzelm@26180: * Method "induction_scheme" derives user-specified induction rules krauss@25664: from wellfounded induction and completeness of patterns. This factors krauss@25664: out some operations that are done internally by the function package krauss@25664: and makes them available separately. See "HOL/ex/Induction_Scheme.thy" krauss@25664: for examples, krauss@25664: schirmer@25705: * Records. Removed K_record, and replaced it by pure lambda term wenzelm@25726: %x. c. The simplifier setup is now more robust against eta expansion. schirmer@25705: INCOMPATIBILITY: in cases explicitly referring to K_record. wenzelm@25464: wenzelm@25726: * Metis prover is now an order of magnitude faster, and also works wenzelm@25726: with multithreading. wenzelm@25726: paulson@26333: * Sledgehammer no longer produces structured proofs by default. To enable, paulson@26333: declare [[sledgehammer_full = true]]. Attributes reconstruction_modulus, paulson@26333: reconstruction_sorts renamed sledgehammer_modulus, sledgehammer_sorts. paulson@26333: INCOMPATIBILITY. wenzelm@25726: krauss@26197: *** ZF *** krauss@26197: krauss@26197: * Renamed theories: krauss@26197: krauss@26197: Datatype.thy -> Datatype_ZF.thy krauss@26197: Inductive.thy -> Inductive_ZF.thy krauss@26197: Int.thy -> Int_ZF.thy krauss@26197: IntDiv.thy -> IntDiv_ZF.thy krauss@26197: Nat.thy -> Nat_ZF.thy krauss@26197: List.thy -> List_ZF.thy krauss@26197: Main.thy -> Main_ZF.thy krauss@26197: krauss@26197: This is to allow to load both ZF and HOL in the same session. krauss@26197: krauss@26197: INCOMPATIBILITY: ZF theories that import individual theories below krauss@26197: Main might need to be adapted. For compatibility, a new krauss@26197: "theory Main imports Main_ZF begin end" is provided, so if you just krauss@26197: imported "Main", no changes are needed. krauss@26197: krauss@26197: wenzelm@25737: *** ML *** wenzelm@25737: wenzelm@26188: * ML within Isar: antiquotation @{const name} or @{const wenzelm@26188: name(typargs)} produces statically-checked Const term. wenzelm@26188: wenzelm@25737: * The ``print mode'' is now a thread-local value derived from a global wenzelm@25737: template (the former print_mode reference), thus access becomes wenzelm@25737: non-critical. The global print_mode reference is for session wenzelm@25737: management only; user-code should use print_mode_value, wenzelm@25737: print_mode_active, PrintMode.setmp etc. INCOMPATIBILITY. wenzelm@25737: wenzelm@26222: * system/system_out provides a robust way to invoke external shell wenzelm@26222: commands, with propagation of interrupts (after Poly/ML 5.2). Do not wenzelm@26222: use OS.Process.system etc. directly. wenzelm@26222: wenzelm@25737: wenzelm@25626: *** System *** wenzelm@25626: wenzelm@26218: * System: removed obsolete THIS_IS_ISABELLE_BUILD feature. NB: the wenzelm@26218: documented way of changing the user's settings is via wenzelm@26218: ISABELLE_HOME_USER/etc/settings, which is a fully featured bash wenzelm@26218: script. wenzelm@26218: wenzelm@25971: * Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs --- wenzelm@25971: in accordance with Proof General 3.7, which prefers GNU emacs. wenzelm@25970: wenzelm@25776: * Multithreading.max_threads := 0 refers to the number of actual CPU wenzelm@25776: cores of the underlying machine, which is a good starting point for wenzelm@25776: optimal performance tuning. The corresponding usedir option -M allows wenzelm@25778: "max" as an alias for "0". WARNING: does not work on certain versions wenzelm@25778: of Mac OS (with Poly/ML 5.1). wenzelm@25776: wenzelm@25626: * isatool tty runs Isabelle process with plain tty interaction; wenzelm@25626: optional line editor may be specified via ISABELLE_LINE_EDITOR wenzelm@25626: setting, the default settings attempt to locate "ledit" and "rlwrap". wenzelm@25626: wenzelm@25651: * isatool browser now works with Cygwin as well, using general wenzelm@25651: "javapath" function defined in Isabelle process environment. wenzelm@25651: wenzelm@25651: * isabelle-process: non-ML sessions are run with "nice", to prevent wenzelm@25651: Isabelle from flooding interactive front-ends (notably ProofGeneral / wenzelm@25651: XEmacs). wenzelm@25651: wenzelm@25652: * JVM class isabelle.IsabelleProcess (located in Isabelle/lib/classes) wenzelm@25651: provides general wrapper for managing an Isabelle process in a robust wenzelm@25651: fashion, with ``cooked'' output from stdin/stderr. wenzelm@25651: wenzelm@25855: * Rudimentary Isabelle plugin for jEdit (see Isabelle/lib/jedit), wenzelm@25855: based on Isabelle/JVM process wrapper (see Isabelle/lib/classes). wenzelm@25855: wenzelm@25626: wenzelm@25464: wenzelm@25429: New in Isabelle2007 (November 2007) wenzelm@25429: ----------------------------------- wenzelm@17754: wenzelm@17754: *** General *** wenzelm@17754: wenzelm@22826: * More uniform information about legacy features, notably a wenzelm@22826: warning/error of "Legacy feature: ...", depending on the state of the wenzelm@23367: tolerate_legacy_features flag (default true). FUTURE INCOMPATIBILITY: wenzelm@23367: legacy features will disappear eventually. wenzelm@22826: wenzelm@17918: * Theory syntax: the header format ``theory A = B + C:'' has been wenzelm@17918: discontinued in favour of ``theory A imports B C begin''. Use isatool wenzelm@17918: fixheaders to convert existing theory files. INCOMPATIBILITY. wenzelm@17918: wenzelm@17918: * Theory syntax: the old non-Isar theory file format has been wenzelm@17918: discontinued altogether. Note that ML proof scripts may still be used wenzelm@17918: with Isar theories; migration is usually quite simple with the ML wenzelm@17918: function use_legacy_bindings. INCOMPATIBILITY. wenzelm@17918: wenzelm@22871: * Theory syntax: some popular names (e.g. 'class', 'declaration', wenzelm@22871: 'fun', 'help', 'if') are now keywords. INCOMPATIBILITY, use double wenzelm@22871: quotes. wenzelm@19814: wenzelm@23888: * Theory loader: be more serious about observing the static theory wenzelm@23888: header specifications (including optional directories), but not the wenzelm@24172: accidental file locations of previously successful loads. The strict wenzelm@24172: update policy of former update_thy is now already performed by wenzelm@24172: use_thy, so the former has been removed; use_thys updates several wenzelm@24172: theories simultaneously, just as 'imports' within a theory header wenzelm@24172: specification, but without merging the results. Potential wenzelm@24172: INCOMPATIBILITY: may need to refine theory headers and commands wenzelm@24172: ROOT.ML which depend on load order. wenzelm@23888: wenzelm@23888: * Theory loader: optional support for content-based file wenzelm@23888: identification, instead of the traditional scheme of full physical wenzelm@23889: path plus date stamp; configured by the ISABELLE_FILE_IDENT setting wenzelm@23888: (cf. the system manual). The new scheme allows to work with wenzelm@23888: non-finished theories in persistent session images, such that source wenzelm@23888: files may be moved later on without requiring reloads. wenzelm@23888: wenzelm@24187: * Theory loader: old-style ML proof scripts being *attached* to a thy wenzelm@24187: file (with the same base name as the theory) are considered a legacy wenzelm@24800: feature, which will disappear eventually. Even now, the theory loader wenzelm@24800: no longer maintains dependencies on such files. wenzelm@24800: wenzelm@24800: * Syntax: the scope for resolving ambiguities via type-inference is wenzelm@24800: now limited to individual terms, instead of whole simultaneous wenzelm@24234: specifications as before. This greatly reduces the complexity of the wenzelm@24234: syntax module and improves flexibility by separating parsing and wenzelm@24234: type-checking. INCOMPATIBILITY: additional type-constraints (explicit wenzelm@24234: 'fixes' etc.) are required in rare situations. wenzelm@24234: wenzelm@25034: * Syntax: constants introduced by new-style packages ('definition', wenzelm@25034: 'abbreviation' etc.) are passed through the syntax module in wenzelm@25034: ``authentic mode''. This means that associated mixfix annotations wenzelm@25034: really stick to such constants, independently of potential name space wenzelm@25034: ambiguities introduced later on. INCOMPATIBILITY: constants in parse wenzelm@25034: trees are represented slightly differently, may need to adapt syntax wenzelm@25034: translations accordingly. Use CONST marker in 'translations' and wenzelm@25034: @{const_syntax} antiquotation in 'parse_translation' etc. wenzelm@25034: wenzelm@17981: * Legacy goal package: reduced interface to the bare minimum required wenzelm@17981: to keep existing proof scripts running. Most other user-level wenzelm@17981: functions are now part of the OldGoals structure, which is *not* open wenzelm@17981: by default (consider isatool expandshort before open OldGoals). wenzelm@17981: Removed top_sg, prin, printyp, pprint_term/typ altogether, because wenzelm@17981: these tend to cause confusion about the actual goal (!) context being wenzelm@17981: used here, which is not necessarily the same as the_context(). wenzelm@17918: wenzelm@23379: * Command 'find_theorems': supports "*" wild-card in "name:" wenzelm@23379: criterion; "with_dups" option. Certain ProofGeneral versions might wenzelm@23379: support a specific search form (see ProofGeneral/CHANGES). webertj@22965: wenzelm@20370: * The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1 wenzelm@20370: by default, which means that "prems" (and also "fixed variables") are wenzelm@20370: suppressed from proof state output. Note that the ProofGeneral wenzelm@20370: settings mechanism allows to change and save options persistently, but wenzelm@20370: older versions of Isabelle will fail to start up if a negative prems wenzelm@20370: limit is imposed. wenzelm@20370: wenzelm@21308: * Local theory targets may be specified by non-nested blocks of wenzelm@21308: ``context/locale/class ... begin'' followed by ``end''. The body may wenzelm@21308: contain definitions, theorems etc., including any derived mechanism wenzelm@21308: that has been implemented on top of these primitives. This concept wenzelm@21308: generalizes the existing ``theorem (in ...)'' towards more versatility wenzelm@21308: and scalability. wenzelm@21308: wenzelm@21960: * Proof General interface: proper undo of final 'end' command; wenzelm@21960: discontinued Isabelle/classic mode (ML proof scripts). wenzelm@21960: wenzelm@17754: wenzelm@17865: *** Document preparation *** wenzelm@17865: wenzelm@21717: * Added antiquotation @{theory name} which prints the given name, wenzelm@21717: after checking that it refers to a valid ancestor theory in the wenzelm@21717: current context. haftmann@21339: wenzelm@17869: * Added antiquotations @{ML_type text} and @{ML_struct text} which wenzelm@17869: check the given source text as ML type/structure, printing verbatim. wenzelm@17865: wenzelm@21717: * Added antiquotation @{abbrev "c args"} which prints the abbreviation wenzelm@21717: "c args == rhs" given in the current context. (Any number of wenzelm@21735: arguments may be given on the LHS.) wenzelm@21717: wenzelm@21717: wenzelm@17779: *** Pure *** wenzelm@17779: wenzelm@24800: * The 'class' package offers a combination of axclass and locale to wenzelm@25129: achieve Haskell-like type classes in Isabelle. Definitions and wenzelm@25129: theorems within a class context produce both relative results (with wenzelm@25129: implicit parameters according to the locale context), and polymorphic wenzelm@25129: constants with qualified polymorphism (according to the class wenzelm@25129: context). Within the body context of a 'class' target, a separate wenzelm@25129: syntax layer ("user space type system") takes care of converting wenzelm@25129: between global polymorphic consts and internal locale representation. wenzelm@25177: See src/HOL/ex/Classpackage.thy for examples (as well as main HOL). haftmann@25184: "isatool doc classes" provides a tutorial. wenzelm@20807: haftmann@25199: * Generic code generator framework allows to generate executable wenzelm@24800: code for ML and Haskell (including Isabelle classes). A short usage wenzelm@24800: sketch: haftmann@20188: haftmann@20188: internal compilation: haftmann@25199: export_code in SML haftmann@20453: writing SML code to a file: haftmann@25199: export_code in SML haftmann@22735: writing OCaml code to a file: haftmann@25199: export_code in OCaml haftmann@20188: writing Haskell code to a bunch of files: haftmann@25199: export_code in Haskell haftmann@25199: haftmann@25199: evaluating closed propositions to True/False using code generation: haftmann@25184: method ``eval'' haftmann@25184: haftmann@25184: Reasonable default setup of framework in HOL. haftmann@20453: haftmann@20453: Theorem attributs for selecting and transforming function equations theorems: haftmann@20453: haftmann@22845: [code fun]: select a theorem as function equation for a specific constant haftmann@22845: [code fun del]: deselect a theorem as function equation for a specific constant haftmann@22845: [code inline]: select an equation theorem for unfolding (inlining) in place haftmann@22845: [code inline del]: deselect an equation theorem for unfolding (inlining) in place haftmann@20453: haftmann@22735: User-defined serializations (target in {SML, OCaml, Haskell}): haftmann@20453: haftmann@20453: code_const haftmann@20453: {(target) }+ haftmann@20453: haftmann@20453: code_type haftmann@20453: {(target) }+ haftmann@20453: haftmann@20453: code_instance haftmann@20453: {(target)}+ haftmann@20453: where instance ::= :: haftmann@20453: haftmann@20453: code_class haftmann@20453: {(target) }+ haftmann@20453: where class target syntax ::= {where { == }+}? haftmann@20453: haftmann@25199: code_instance and code_class only are effective to target Haskell. haftmann@22735: wenzelm@25177: For example usage see src/HOL/ex/Codegenerator.thy and wenzelm@25177: src/HOL/ex/Codegenerator_Pretty.thy. A separate tutorial on code wenzelm@24800: generation from Isabelle/HOL theories is available via "isatool doc wenzelm@24800: codegen". haftmann@20188: wenzelm@25129: * Code generator: consts in 'consts_code' Isar commands are now wenzelm@25129: referred to by usual term syntax (including optional type wenzelm@25129: annotations). wenzelm@25129: wenzelm@19254: * Command 'no_translations' removes translation rules from theory wenzelm@19254: syntax. wenzelm@19254: wenzelm@19625: * Overloaded definitions are now actually checked for acyclic wenzelm@19714: dependencies. The overloading scheme is slightly more general than wenzelm@19714: that of Haskell98, although Isabelle does not demand an exact wenzelm@19714: correspondence to type class and instance declarations. wenzelm@19714: INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more wenzelm@19714: exotic versions of overloading -- at the discretion of the user! wenzelm@19711: wenzelm@19711: Polymorphic constants are represented via type arguments, i.e. the wenzelm@19711: instantiation that matches an instance against the most general wenzelm@19711: declaration given in the signature. For example, with the declaration wenzelm@19711: c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented wenzelm@19711: as c(nat). Overloading is essentially simultaneous structural wenzelm@19711: recursion over such type arguments. Incomplete specification patterns wenzelm@19714: impose global constraints on all occurrences, e.g. c('a * 'a) on the wenzelm@19715: LHS means that more general c('a * 'b) will be disallowed on any RHS. wenzelm@19714: Command 'print_theory' outputs the normalized system of recursive wenzelm@19714: equations, see section "definitions". wenzelm@19625: wenzelm@24086: * Configuration options are maintained within the theory or proof wenzelm@24086: context (with name and type bool/int/string), providing a very simple wenzelm@24086: interface to a poor-man's version of general context data. Tools may wenzelm@24110: declare options in ML (e.g. using Attrib.config_int) and then refer to wenzelm@24110: these values using Config.get etc. Users may change options via an wenzelm@24110: associated attribute of the same name. This form of context wenzelm@24110: declaration works particularly well with commands 'declare' or wenzelm@24110: 'using', for example ``declare [[foo = 42]]''. Thus it has become wenzelm@24110: very easy to avoid global references, which would not observe Isar wenzelm@24110: toplevel undo/redo and fail to work with multithreading. wenzelm@24086: wenzelm@24172: Various global ML references of Pure and HOL have been turned into wenzelm@24172: configuration options: wenzelm@24172: wenzelm@24172: Unify.search_bound unify_search_bound wenzelm@24172: Unify.trace_bound unify_trace_bound wenzelm@24172: Unify.trace_simp unify_trace_simp wenzelm@24172: Unify.trace_types unify_trace_types wenzelm@24172: Simplifier.simp_depth_limit simp_depth_limit wenzelm@24172: Blast.depth_limit blast_depth_limit wenzelm@24172: DatatypeProp.dtK datatype_distinctness_limit wenzelm@24172: fast_arith_neq_limit fast_arith_neq_limit wenzelm@24172: fast_arith_split_limit fast_arith_split_limit wenzelm@24172: wenzelm@24086: * Named collections of theorems may be easily installed as context wenzelm@24800: data using the functor NamedThmsFun (see also wenzelm@24086: src/Pure/Tools/named_thms.ML). The user may add or delete facts via wenzelm@24110: attributes; there is also a toplevel print command. This facility is wenzelm@24110: just a common case of general context data, which is the preferred way wenzelm@24110: for anything more complex than just a list of facts in canonical wenzelm@24110: order. wenzelm@24086: wenzelm@24032: * Isar: command 'declaration' augments a local theory by generic wenzelm@24032: declaration functions written in ML. This enables arbitrary content wenzelm@24032: being added to the context, depending on a morphism that tells the wenzelm@24032: difference of the original declaration context wrt. the application wenzelm@24032: context encountered later on. wenzelm@24032: wenzelm@24032: * Isar: proper interfaces for simplification procedures. Command wenzelm@24032: 'simproc_setup' declares named simprocs (with match patterns, and body wenzelm@24032: text in ML). Attribute "simproc" adds/deletes simprocs in the current wenzelm@24032: context. ML antiquotation @{simproc name} retrieves named simprocs. wenzelm@24032: wenzelm@24032: * Isar: an extra pair of brackets around attribute declarations wenzelm@24032: abbreviates a theorem reference involving an internal dummy fact, wenzelm@24032: which will be ignored later --- only the effect of the attribute on wenzelm@24032: the background context will persist. This form of in-place wenzelm@24032: declarations is particularly useful with commands like 'declare' and wenzelm@24032: 'using', for example ``have A using [[simproc a]] by simp''. wenzelm@24032: wenzelm@23369: * Isar: method "assumption" (and implicit closing of subproofs) now wenzelm@23369: takes simple non-atomic goal assumptions into account: after applying wenzelm@23369: an assumption as a rule the resulting subgoals are solved by atomic wenzelm@23369: assumption steps. This is particularly useful to finish 'obtain' wenzelm@23369: goals, such as "!!x. (!!x. P x ==> thesis) ==> P x ==> thesis", wenzelm@23369: without referring to the original premise "!!x. P x ==> thesis" in the wenzelm@23369: Isar proof context. POTENTIAL INCOMPATIBILITY: method "assumption" is wenzelm@23369: more permissive. wenzelm@23369: wenzelm@23369: * Isar: implicit use of prems from the Isar proof context is wenzelm@23369: considered a legacy feature. Common applications like ``have A .'' wenzelm@23369: may be replaced by ``have A by fact'' or ``note `A`''. In general, wenzelm@23369: referencing facts explicitly here improves readability and wenzelm@23369: maintainability of proof texts. wenzelm@23369: wenzelm@17865: * Isar: improper proof element 'guess' is like 'obtain', but derives wenzelm@17865: the obtained context from the course of reasoning! For example: wenzelm@17865: wenzelm@17865: assume "EX x y. A x & B y" -- "any previous fact" wenzelm@17865: then guess x and y by clarify wenzelm@17865: wenzelm@17865: This technique is potentially adventurous, depending on the facts and wenzelm@17865: proof tools being involved here. wenzelm@17865: wenzelm@18020: * Isar: known facts from the proof context may be specified as literal wenzelm@18020: propositions, using ASCII back-quote syntax. This works wherever wenzelm@18020: named facts used to be allowed so far, in proof commands, proof wenzelm@18020: methods, attributes etc. Literal facts are retrieved from the context wenzelm@18020: according to unification of type and term parameters. For example, wenzelm@18020: provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known wenzelm@18020: theorems in the current context, then these are valid literal facts: wenzelm@18020: `A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc. wenzelm@18020: wenzelm@18020: There is also a proof method "fact" which does the same composition wenzelm@18044: for explicit goal states, e.g. the following proof texts coincide with wenzelm@18044: certain special cases of literal facts: wenzelm@18020: wenzelm@18020: have "A" by fact == note `A` wenzelm@18020: have "A ==> B" by fact == note `A ==> B` wenzelm@18020: have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` wenzelm@18020: have "P a ==> Q a" by fact == note `P a ==> Q a` wenzelm@18020: wenzelm@20118: * Isar: ":" (colon) is no longer a symbolic identifier character in wenzelm@20118: outer syntax. Thus symbolic identifiers may be used without wenzelm@20118: additional white space in declarations like this: ``assume *: A''. wenzelm@20118: wenzelm@20013: * Isar: 'print_facts' prints all local facts of the current context, wenzelm@20013: both named and unnamed ones. wenzelm@20013: wenzelm@18308: * Isar: 'def' now admits simultaneous definitions, e.g.: wenzelm@18308: wenzelm@18308: def x == "t" and y == "u" wenzelm@18308: wenzelm@18540: * Isar: added command 'unfolding', which is structurally similar to wenzelm@18540: 'using', but affects both the goal state and facts by unfolding given wenzelm@18815: rewrite rules. Thus many occurrences of the 'unfold' method or wenzelm@18540: 'unfolded' attribute may be replaced by first-class proof text. wenzelm@18540: wenzelm@18815: * Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded', wenzelm@18815: and command 'unfolding' now all support object-level equalities wenzelm@18815: (potentially conditional). The underlying notion of rewrite rule is wenzelm@18815: analogous to the 'rule_format' attribute, but *not* that of the wenzelm@18815: Simplifier (which is usually more generous). wenzelm@18815: kleing@24238: * Isar: the new attribute [rotated n] (default n = 1) rotates the kleing@24238: premises of a theorem by n. Useful in conjunction with drule. kleing@24238: wenzelm@19220: * Isar: the goal restriction operator [N] (default N = 1) evaluates a wenzelm@19220: method expression within a sandbox consisting of the first N wenzelm@19240: sub-goals, which need to exist. For example, ``simp_all [3]'' wenzelm@19240: simplifies the first three sub-goals, while (rule foo, simp_all)[] wenzelm@19240: simplifies all new goals that emerge from applying rule foo to the wenzelm@19240: originally first one. wenzelm@19220: wenzelm@19814: * Isar: schematic goals are no longer restricted to higher-order wenzelm@19814: patterns; e.g. ``lemma "?P(?x)" by (rule TrueI)'' now works as wenzelm@19814: expected. wenzelm@19814: wenzelm@18901: * Isar: the conclusion of a long theorem statement is now either wenzelm@18901: 'shows' (a simultaneous conjunction, as before), or 'obtains' wenzelm@18901: (essentially a disjunction of cases with local parameters and wenzelm@18901: assumptions). The latter allows to express general elimination rules wenzelm@18910: adequately; in this notation common elimination rules look like this: wenzelm@18901: wenzelm@18901: lemma exE: -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis" wenzelm@18901: assumes "EX x. P x" wenzelm@18901: obtains x where "P x" wenzelm@18901: wenzelm@18901: lemma conjE: -- "A & B ==> (A ==> B ==> thesis) ==> thesis" wenzelm@18901: assumes "A & B" wenzelm@18901: obtains A and B wenzelm@18901: wenzelm@18901: lemma disjE: -- "A | B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis" wenzelm@18901: assumes "A | B" wenzelm@18901: obtains wenzelm@18901: A wenzelm@18901: | B wenzelm@18901: wenzelm@18910: The subsequent classical rules even refer to the formal "thesis" wenzelm@18901: explicitly: wenzelm@18901: wenzelm@18901: lemma classical: -- "(~ thesis ==> thesis) ==> thesis" wenzelm@18901: obtains "~ thesis" wenzelm@18901: wenzelm@18910: lemma Peirce's_Law: -- "((thesis ==> something) ==> thesis) ==> thesis" wenzelm@18910: obtains "thesis ==> something" wenzelm@18901: wenzelm@18901: The actual proof of an 'obtains' statement is analogous to that of the wenzelm@18910: Isar proof element 'obtain', only that there may be several cases. wenzelm@18910: Optional case names may be specified in parentheses; these will be wenzelm@18910: available both in the present proof and as annotations in the wenzelm@18910: resulting rule, for later use with the 'cases' method (cf. attribute wenzelm@18910: case_names). wenzelm@18901: wenzelm@21447: * Isar: the assumptions of a long theorem statement are available as wenzelm@21447: "assms" fact in the proof context. This is more appropriate than the wenzelm@21447: (historical) "prems", which refers to all assumptions of the current wenzelm@21447: context, including those from the target locale, proof body etc. wenzelm@21447: wenzelm@19263: * Isar: 'print_statement' prints theorems from the current theory or wenzelm@19263: proof context in long statement form, according to the syntax of a wenzelm@19263: top-level lemma. wenzelm@19263: wenzelm@18901: * Isar: 'obtain' takes an optional case name for the local context wenzelm@18901: introduction rule (default "that"). wenzelm@18901: wenzelm@19587: * Isar: removed obsolete 'concl is' patterns. INCOMPATIBILITY, use wenzelm@19587: explicit (is "_ ==> ?foo") in the rare cases where this still happens wenzelm@19587: to occur. wenzelm@19587: wenzelm@19682: * Pure: syntax "CONST name" produces a fully internalized constant wenzelm@19682: according to the current context. This is particularly useful for wenzelm@19682: syntax translations that should refer to internal constant wenzelm@19682: representations independently of name spaces. wenzelm@19682: wenzelm@21537: * Pure: syntax constant for foo (binder "FOO ") is called "foo_binder" wenzelm@21537: instead of "FOO ". This allows multiple binder declarations to coexist wenzelm@21537: in the same context. INCOMPATIBILITY. wenzelm@21537: wenzelm@21209: * Isar/locales: 'notation' provides a robust interface to the 'syntax' wenzelm@21209: primitive that also works in a locale context (both for constants and wenzelm@24950: fixed variables). Type declaration and internal syntactic representation wenzelm@24950: of given constants retrieved from the context. Likewise, the wenzelm@24950: 'no_notation' command allows to remove given syntax annotations from the wenzelm@24950: current context. wenzelm@19682: wenzelm@19665: * Isar/locales: new derived specification elements 'axiomatization', wenzelm@19665: 'definition', 'abbreviation', which support type-inference, admit wenzelm@19083: object-level specifications (equality, equivalence). See also the wenzelm@19083: isar-ref manual. Examples: wenzelm@19081: wenzelm@19665: axiomatization wenzelm@21595: eq (infix "===" 50) where wenzelm@21595: eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y" wenzelm@21595: wenzelm@21595: definition "f x y = x + y + 1" wenzelm@21595: definition g where "g x = f x x" wenzelm@19081: wenzelm@19363: abbreviation wenzelm@21595: neq (infix "=!=" 50) where wenzelm@19363: "x =!= y == ~ (x === y)" wenzelm@19081: wenzelm@19083: These specifications may be also used in a locale context. Then the wenzelm@19083: constants being introduced depend on certain fixed parameters, and the wenzelm@19083: constant name is qualified by the locale base name. An internal wenzelm@19083: abbreviation takes care for convenient input and output, making the wenzelm@19088: parameters implicit and using the original short name. See also wenzelm@25177: src/HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic wenzelm@19083: entities from a monomorphic theory. wenzelm@19083: wenzelm@19083: Presently, abbreviations are only available 'in' a target locale, but wenzelm@19363: not inherited by general import expressions. Also note that wenzelm@19363: 'abbreviation' may be used as a type-safe replacement for 'syntax' + wenzelm@24735: 'translations' in common applications. The "no_abbrevs" print mode wenzelm@24735: prevents folding of abbreviations in term output. wenzelm@19084: wenzelm@19682: Concrete syntax is attached to specified constants in internal form, wenzelm@19682: independently of name spaces. The parse tree representation is wenzelm@21209: slightly different -- use 'notation' instead of raw 'syntax', and wenzelm@19682: 'translations' with explicit "CONST" markup to accommodate this. wenzelm@19665: wenzelm@24800: * Pure/Isar: unified syntax for new-style specification mechanisms wenzelm@24800: (e.g. 'definition', 'abbreviation', or 'inductive' in HOL) admits wenzelm@24800: full type inference and dummy patterns ("_"). For example: wenzelm@24735: wenzelm@24735: definition "K x _ = x" wenzelm@24735: wenzelm@24738: inductive conj for A B wenzelm@24738: where "A ==> B ==> conj A B" wenzelm@24738: wenzelm@21735: * Pure: command 'print_abbrevs' prints all constant abbreviations of wenzelm@21735: the current context. Print mode "no_abbrevs" prevents inversion of wenzelm@21735: abbreviations on output. wenzelm@21735: wenzelm@24800: * Isar/locales: improved parameter handling: use of locales "var" and wenzelm@24800: "struct" no longer necessary; - parameter renamings are no longer wenzelm@24800: required to be injective. For example, this allows to define wenzelm@24800: endomorphisms as locale endom = homom mult mult h. ballarin@19783: ballarin@19931: * Isar/locales: changed the way locales with predicates are defined. ballarin@19931: Instead of accumulating the specification, the imported expression is wenzelm@22126: now an interpretation. INCOMPATIBILITY: different normal form of wenzelm@22126: locale expressions. In particular, in interpretations of locales with wenzelm@22126: predicates, goals repesenting already interpreted fragments are not wenzelm@22126: removed automatically. Use methods `intro_locales' and wenzelm@22126: `unfold_locales'; see below. wenzelm@22126: wenzelm@22126: * Isar/locales: new methods `intro_locales' and `unfold_locales' wenzelm@22126: provide backward reasoning on locales predicates. The methods are wenzelm@22126: aware of interpretations and discharge corresponding goals. wenzelm@22126: `intro_locales' is less aggressive then `unfold_locales' and does not wenzelm@22126: unfold predicates to assumptions. ballarin@19931: ballarin@19931: * Isar/locales: the order in which locale fragments are accumulated wenzelm@22126: has changed. This enables to override declarations from fragments due wenzelm@22126: to interpretations -- for example, unwanted simp rules. ballarin@19931: ballarin@23920: * Isar/locales: interpretation in theories and proof contexts has been ballarin@23920: extended. One may now specify (and prove) equations, which are ballarin@23920: unfolded in interpreted theorems. This is useful for replacing ballarin@23920: defined concepts (constants depending on locale parameters) by ballarin@23920: concepts already existing in the target context. Example: ballarin@23920: ballarin@23920: interpretation partial_order ["op <= :: [int, int] => bool"] ballarin@23920: where "partial_order.less (op <=) (x::int) y = (x < y)" ballarin@23920: wenzelm@24800: Typically, the constant `partial_order.less' is created by a wenzelm@24800: definition specification element in the context of locale wenzelm@24800: partial_order. wenzelm@24800: wenzelm@24859: * Method "induct": improved internal context management to support wenzelm@24800: local fixes and defines on-the-fly. Thus explicit meta-level wenzelm@24800: connectives !! and ==> are rarely required anymore in inductive goals wenzelm@24800: (using object-logic connectives for this purpose has been long wenzelm@24800: obsolete anyway). Common proof patterns are explained in wenzelm@25177: src/HOL/Induct/Common_Patterns.thy, see also wenzelm@25177: src/HOL/Isar_examples/Puzzle.thy and src/HOL/Lambda for realistic wenzelm@25177: examples. wenzelm@24606: wenzelm@24859: * Method "induct": improved handling of simultaneous goals. Instead of wenzelm@24606: introducing object-level conjunction, the statement is now split into wenzelm@24606: several conclusions, while the corresponding symbolic cases are nested wenzelm@24606: accordingly. INCOMPATIBILITY, proofs need to be structured explicitly, wenzelm@25177: see src/HOL/Induct/Common_Patterns.thy, for example. wenzelm@24606: wenzelm@24859: * Method "induct": mutual induction rules are now specified as a list wenzelm@24800: of rule sharing the same induction cases. HOL packages usually provide wenzelm@24606: foo_bar.inducts for mutually defined items foo and bar (e.g. inductive wenzelm@24859: predicates/sets or datatypes). INCOMPATIBILITY, users need to specify wenzelm@24859: mutual induction rules differently, i.e. like this: wenzelm@18506: wenzelm@18506: (induct rule: foo_bar.inducts) wenzelm@18506: (induct set: foo bar) wenzelm@24859: (induct pred: foo bar) wenzelm@18506: (induct type: foo bar) wenzelm@18506: wenzelm@18506: The ML function ProjectRule.projections turns old-style rules into the wenzelm@18506: new format. wenzelm@18506: wenzelm@24859: * Method "coinduct": dual of induction, see wenzelm@18399: src/HOL/Library/Coinductive_List.thy for various examples. wenzelm@18399: wenzelm@24859: * Method "cases", "induct", "coinduct": the ``(open)'' option is wenzelm@24859: considered a legacy feature. wenzelm@24859: wenzelm@20919: * Attribute "symmetric" produces result with standardized schematic wenzelm@20919: variables (index 0). Potential INCOMPATIBILITY. wenzelm@20919: wenzelm@22126: * Simplifier: by default the simplifier trace only shows top level wenzelm@22126: rewrites now. That is, trace_simp_depth_limit is set to 1 by wenzelm@22126: default. Thus there is less danger of being flooded by the trace. The wenzelm@22126: trace indicates where parts have been suppressed. nipkow@18674: wenzelm@18536: * Provers/classical: removed obsolete classical version of elim_format wenzelm@18536: attribute; classical elim/dest rules are now treated uniformly when wenzelm@18536: manipulating the claset. wenzelm@18536: wenzelm@18694: * Provers/classical: stricter checks to ensure that supplied intro, wenzelm@18694: dest and elim rules are well-formed; dest and elim rules must have at wenzelm@18694: least one premise. wenzelm@18694: wenzelm@18694: * Provers/classical: attributes dest/elim/intro take an optional wenzelm@18695: weight argument for the rule (just as the Pure versions). Weights are wenzelm@18696: ignored by automated tools, but determine the search order of single wenzelm@18694: rule steps. paulson@18557: wenzelm@18536: * Syntax: input syntax now supports dummy variable binding "%_. b", wenzelm@18536: where the body does not mention the bound variable. Note that dummy wenzelm@18536: patterns implicitly depend on their context of bounds, which makes wenzelm@18536: "{_. _}" match any set comprehension as expected. Potential wenzelm@18536: INCOMPATIBILITY -- parse translations need to cope with syntactic wenzelm@18536: constant "_idtdummy" in the binding position. wenzelm@18536: wenzelm@18536: * Syntax: removed obsolete syntactic constant "_K" and its associated wenzelm@18536: parse translation. INCOMPATIBILITY -- use dummy abstraction instead, wenzelm@18536: for example "A -> B" => "Pi A (%_. B)". wenzelm@17779: wenzelm@20582: * Pure: 'class_deps' command visualizes the subclass relation, using wenzelm@20582: the graph browser tool. wenzelm@20582: wenzelm@24800: * Pure: 'print_theory' now suppresses certain internal declarations by wenzelm@24800: default; use '!' option for full details. wenzelm@20620: wenzelm@17865: nipkow@17806: *** HOL *** nipkow@17806: wenzelm@25129: * Method "metis" proves goals by applying the Metis general-purpose wenzelm@25129: resolution prover (see also http://gilith.com/software/metis/). wenzelm@25129: Examples are in the directory MetisExamples. WARNING: the wenzelm@25129: Isabelle/HOL-Metis integration does not yet work properly with wenzelm@25129: multi-threading. wenzelm@25129: wenzelm@25129: * Command 'sledgehammer' invokes external automatic theorem provers as wenzelm@25129: background processes. It generates calls to the "metis" method if wenzelm@25129: successful. These can be pasted into the proof. Users do not have to wenzelm@25129: wait for the automatic provers to return. WARNING: does not really wenzelm@25129: work with multi-threading. wenzelm@25129: wenzelm@24804: * New "auto_quickcheck" feature tests outermost goal statements for wenzelm@24804: potential counter-examples. Controlled by ML references wenzelm@24804: auto_quickcheck (default true) and auto_quickcheck_time_limit (default wenzelm@25129: 5000 milliseconds). Fails silently if statements is outside of wenzelm@25129: executable fragment, or any other codgenerator problem occurs. wenzelm@24804: haftmann@25184: * New constant "undefined" with axiom "undefined x = undefined". haftmann@25184: haftmann@25184: * Added class "HOL.eq", allowing for code generation with polymorphic haftmann@25184: equality. haftmann@25184: haftmann@25184: * Some renaming of class constants due to canonical name prefixing in haftmann@25184: the new 'class' package: haftmann@25184: haftmann@25184: HOL.abs ~> HOL.abs_class.abs haftmann@25184: HOL.divide ~> HOL.divide_class.divide haftmann@25184: 0 ~> HOL.zero_class.zero haftmann@25184: 1 ~> HOL.one_class.one haftmann@25184: op + ~> HOL.plus_class.plus haftmann@25184: op - ~> HOL.minus_class.minus haftmann@25184: uminus ~> HOL.minus_class.uminus haftmann@25184: op * ~> HOL.times_class.times haftmann@25184: op < ~> HOL.ord_class.less haftmann@25184: op <= > HOL.ord_class.less_eq haftmann@25184: Nat.power ~> Power.power_class.power haftmann@25184: Nat.size ~> Nat.size_class.size haftmann@25184: Numeral.number_of ~> Numeral.number_class.number_of haftmann@25184: FixedPoint.Inf ~> Lattices.complete_lattice_class.Inf haftmann@25184: FixedPoint.Sup ~> Lattices.complete_lattice_class.Sup haftmann@25184: Orderings.min ~> Orderings.ord_class.min haftmann@25184: Orderings.max ~> Orderings.ord_class.max haftmann@25184: Divides.op div ~> Divides.div_class.div haftmann@25184: Divides.op mod ~> Divides.div_class.mod haftmann@25184: Divides.op dvd ~> Divides.div_class.dvd haftmann@25184: haftmann@25184: INCOMPATIBILITY. Adaptions may be required in the following cases: haftmann@25184: haftmann@25184: a) User-defined constants using any of the names "plus", "minus", haftmann@25184: "times", "less" or "less_eq". The standard syntax translations for haftmann@25184: "+", "-" and "*" may go wrong. INCOMPATIBILITY: use more specific haftmann@25184: names. haftmann@25184: haftmann@25184: b) Variables named "plus", "minus", "times", "less", "less_eq" haftmann@25184: INCOMPATIBILITY: use more specific names. haftmann@25184: haftmann@25184: c) Permutative equations (e.g. "a + b = b + a") haftmann@25184: Since the change of names also changes the order of terms, permutative haftmann@25184: rewrite rules may get applied in a different order. Experience shows haftmann@25184: that this is rarely the case (only two adaptions in the whole Isabelle haftmann@25184: distribution). INCOMPATIBILITY: rewrite proofs haftmann@25184: haftmann@25184: d) ML code directly refering to constant names haftmann@25184: This in general only affects hand-written proof tactics, simprocs and haftmann@25184: so on. INCOMPATIBILITY: grep your sourcecode and replace names. haftmann@25184: Consider using @{const_name} antiquotation. haftmann@25184: haftmann@25184: * New class "default" with associated constant "default". haftmann@25184: haftmann@25184: * Function "sgn" is now overloaded and available on int, real, complex haftmann@25184: (and other numeric types), using class "sgn". Two possible defs of haftmann@25184: sgn are given as equational assumptions in the classes sgn_if and haftmann@25184: sgn_div_norm; ordered_idom now also inherits from sgn_if. haftmann@25184: INCOMPATIBILITY. haftmann@25184: haftmann@25184: * Locale "partial_order" now unified with class "order" (cf. theory haftmann@25184: Orderings), added parameter "less". INCOMPATIBILITY. haftmann@25184: haftmann@25184: * Renamings in classes "order" and "linorder": facts "refl", "trans" and haftmann@25184: "cases" to "order_refl", "order_trans" and "linorder_cases", to avoid haftmann@25184: clashes with HOL "refl" and "trans". INCOMPATIBILITY. haftmann@25184: haftmann@25184: * Classes "order" and "linorder": potential INCOMPATIBILITY due to haftmann@25184: changed order of proof goals in instance proofs. haftmann@25184: haftmann@25184: * The transitivity reasoner for partial and linear orders is set up haftmann@25184: for classes "order" and "linorder". Instances of the reasoner are available haftmann@25184: in all contexts importing or interpreting the corresponding locales. haftmann@25184: Method "order" invokes the reasoner separately; the reasoner haftmann@25184: is also integrated with the Simplifier as a solver. Diagnostic haftmann@25184: command 'print_orders' shows the available instances of the reasoner haftmann@25184: in the current context. haftmann@25184: haftmann@25184: * Localized monotonicity predicate in theory "Orderings"; integrated haftmann@25184: lemmas max_of_mono and min_of_mono with this predicate. haftmann@25184: INCOMPATIBILITY. haftmann@25184: haftmann@25184: * Formulation of theorem "dense" changed slightly due to integration haftmann@25184: with new class dense_linear_order. haftmann@25184: haftmann@25184: * Uniform lattice theory development in HOL. haftmann@25184: haftmann@25184: constants "meet" and "join" now named "inf" and "sup" haftmann@25184: constant "Meet" now named "Inf" haftmann@25184: haftmann@25184: classes "meet_semilorder" and "join_semilorder" now named haftmann@25184: "lower_semilattice" and "upper_semilattice" haftmann@25184: class "lorder" now named "lattice" haftmann@25184: class "comp_lat" now named "complete_lattice" haftmann@25184: haftmann@25184: Instantiation of lattice classes allows explicit definitions haftmann@25184: for "inf" and "sup" operations (or "Inf" and "Sup" for complete lattices). haftmann@25184: haftmann@25184: INCOMPATIBILITY. Theorem renames: haftmann@25184: haftmann@25184: meet_left_le ~> inf_le1 haftmann@25184: meet_right_le ~> inf_le2 haftmann@25184: join_left_le ~> sup_ge1 haftmann@25184: join_right_le ~> sup_ge2 haftmann@25184: meet_join_le ~> inf_sup_ord haftmann@25184: le_meetI ~> le_infI haftmann@25184: join_leI ~> le_supI haftmann@25184: le_meet ~> le_inf_iff haftmann@25184: le_join ~> ge_sup_conv haftmann@25184: meet_idempotent ~> inf_idem haftmann@25184: join_idempotent ~> sup_idem haftmann@25184: meet_comm ~> inf_commute haftmann@25184: join_comm ~> sup_commute haftmann@25184: meet_leI1 ~> le_infI1 haftmann@25184: meet_leI2 ~> le_infI2 haftmann@25184: le_joinI1 ~> le_supI1 haftmann@25184: le_joinI2 ~> le_supI2 haftmann@25184: meet_assoc ~> inf_assoc haftmann@25184: join_assoc ~> sup_assoc haftmann@25184: meet_left_comm ~> inf_left_commute haftmann@25184: meet_left_idempotent ~> inf_left_idem haftmann@25184: join_left_comm ~> sup_left_commute haftmann@25184: join_left_idempotent ~> sup_left_idem haftmann@25184: meet_aci ~> inf_aci haftmann@25184: join_aci ~> sup_aci haftmann@25184: le_def_meet ~> le_iff_inf haftmann@25184: le_def_join ~> le_iff_sup haftmann@25184: join_absorp2 ~> sup_absorb2 haftmann@25184: join_absorp1 ~> sup_absorb1 haftmann@25184: meet_absorp1 ~> inf_absorb1 haftmann@25184: meet_absorp2 ~> inf_absorb2 haftmann@25184: meet_join_absorp ~> inf_sup_absorb haftmann@25184: join_meet_absorp ~> sup_inf_absorb haftmann@25184: distrib_join_le ~> distrib_sup_le haftmann@25184: distrib_meet_le ~> distrib_inf_le haftmann@25184: haftmann@25184: add_meet_distrib_left ~> add_inf_distrib_left haftmann@25184: add_join_distrib_left ~> add_sup_distrib_left haftmann@25184: is_join_neg_meet ~> is_join_neg_inf haftmann@25184: is_meet_neg_join ~> is_meet_neg_sup haftmann@25184: add_meet_distrib_right ~> add_inf_distrib_right haftmann@25184: add_join_distrib_right ~> add_sup_distrib_right haftmann@25184: add_meet_join_distribs ~> add_sup_inf_distribs haftmann@25184: join_eq_neg_meet ~> sup_eq_neg_inf haftmann@25184: meet_eq_neg_join ~> inf_eq_neg_sup haftmann@25184: add_eq_meet_join ~> add_eq_inf_sup haftmann@25184: meet_0_imp_0 ~> inf_0_imp_0 haftmann@25184: join_0_imp_0 ~> sup_0_imp_0 haftmann@25184: meet_0_eq_0 ~> inf_0_eq_0 haftmann@25184: join_0_eq_0 ~> sup_0_eq_0 haftmann@25184: neg_meet_eq_join ~> neg_inf_eq_sup haftmann@25184: neg_join_eq_meet ~> neg_sup_eq_inf haftmann@25184: join_eq_if ~> sup_eq_if haftmann@25184: haftmann@25184: mono_meet ~> mono_inf haftmann@25184: mono_join ~> mono_sup haftmann@25184: meet_bool_eq ~> inf_bool_eq haftmann@25184: join_bool_eq ~> sup_bool_eq haftmann@25184: meet_fun_eq ~> inf_fun_eq haftmann@25184: join_fun_eq ~> sup_fun_eq haftmann@25184: meet_set_eq ~> inf_set_eq haftmann@25184: join_set_eq ~> sup_set_eq haftmann@25184: meet1_iff ~> inf1_iff haftmann@25184: meet2_iff ~> inf2_iff haftmann@25184: meet1I ~> inf1I haftmann@25184: meet2I ~> inf2I haftmann@25184: meet1D1 ~> inf1D1 haftmann@25184: meet2D1 ~> inf2D1 haftmann@25184: meet1D2 ~> inf1D2 haftmann@25184: meet2D2 ~> inf2D2 haftmann@25184: meet1E ~> inf1E haftmann@25184: meet2E ~> inf2E haftmann@25184: join1_iff ~> sup1_iff haftmann@25184: join2_iff ~> sup2_iff haftmann@25184: join1I1 ~> sup1I1 haftmann@25184: join2I1 ~> sup2I1 haftmann@25184: join1I1 ~> sup1I1 haftmann@25184: join2I2 ~> sup1I2 haftmann@25184: join1CI ~> sup1CI haftmann@25184: join2CI ~> sup2CI haftmann@25184: join1E ~> sup1E haftmann@25184: join2E ~> sup2E haftmann@25184: haftmann@25184: is_meet_Meet ~> is_meet_Inf haftmann@25184: Meet_bool_def ~> Inf_bool_def haftmann@25184: Meet_fun_def ~> Inf_fun_def haftmann@25184: Meet_greatest ~> Inf_greatest haftmann@25184: Meet_lower ~> Inf_lower haftmann@25184: Meet_set_def ~> Inf_set_def haftmann@25184: haftmann@25184: Sup_def ~> Sup_Inf haftmann@25184: Sup_bool_eq ~> Sup_bool_def haftmann@25184: Sup_fun_eq ~> Sup_fun_def haftmann@25184: Sup_set_eq ~> Sup_set_def haftmann@25184: haftmann@25184: listsp_meetI ~> listsp_infI haftmann@25184: listsp_meet_eq ~> listsp_inf_eq haftmann@25184: haftmann@25184: meet_min ~> inf_min haftmann@25184: join_max ~> sup_max haftmann@25184: haftmann@25184: * Added syntactic class "size"; overloaded constant "size" now has haftmann@25184: type "'a::size ==> bool" haftmann@25184: wenzelm@24800: * Internal reorganisation of `size' of datatypes: size theorems wenzelm@24800: "foo.size" are no longer subsumed by "foo.simps" (but are still wenzelm@24800: simplification rules by default!); theorems "prod.size" now named haftmann@25184: "*.size". haftmann@25184: haftmann@25184: * Class "div" now inherits from class "times" rather than "type". haftmann@25184: INCOMPATIBILITY. wenzelm@24800: wenzelm@24800: * HOL/Finite_Set: "name-space" locales Lattice, Distrib_lattice, wenzelm@24800: Linorder etc. have disappeared; operations defined in terms of wenzelm@24800: fold_set now are named Inf_fin, Sup_fin. INCOMPATIBILITY. wenzelm@24800: wenzelm@25129: * HOL/Nat: neq0_conv no longer declared as iff. INCOMPATIBILITY. wenzelm@25129: wenzelm@24800: * HOL-Word: New extensive library and type for generic, fixed size wenzelm@24800: machine words, with arithemtic, bit-wise, shifting and rotating wenzelm@24800: operations, reflection into int, nat, and bool lists, automation for wenzelm@24800: linear arithmetic (by automatic reflection into nat or int), including wenzelm@24800: lemmas on overflow and monotonicity. Instantiated to all appropriate wenzelm@24800: arithmetic type classes, supporting automatic simplification of wenzelm@24800: numerals on all operations. kleing@24333: kleing@24333: * Library/Boolean_Algebra: locales for abstract boolean algebras. kleing@24333: kleing@24333: * Library/Numeral_Type: numbers as types, e.g. TYPE(32). kleing@24333: haftmann@23850: * Code generator library theories: haftmann@24993: - Code_Integer represents HOL integers by big integer literals in target haftmann@23850: languages. haftmann@24993: - Code_Char represents HOL characters by character literals in target haftmann@23850: languages. haftmann@24993: - Code_Char_chr like Code_Char, but also offers treatment of character haftmann@24993: codes; includes Code_Integer. wenzelm@24800: - Executable_Set allows to generate code for finite sets using lists. wenzelm@24800: - Executable_Rat implements rational numbers as triples (sign, enumerator, haftmann@23850: denominator). wenzelm@24800: - Executable_Real implements a subset of real numbers, namly those haftmann@23850: representable by rational numbers. wenzelm@24800: - Efficient_Nat implements natural numbers by integers, which in general will haftmann@23850: result in higher efficency; pattern matching with 0/Suc is eliminated; haftmann@24993: includes Code_Integer. haftmann@24993: - Code_Index provides an additional datatype index which is mapped to haftmann@24993: target-language built-in integers. haftmann@24993: - Code_Message provides an additional datatype message_string} which is isomorphic to haftmann@24993: strings; messages are mapped to target-language strings. haftmann@23850: berghofe@23783: * New package for inductive predicates berghofe@23783: berghofe@23783: An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via berghofe@23783: berghofe@23783: inductive berghofe@23783: p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool" berghofe@23783: for z_1 :: U_1 and ... and z_n :: U_m berghofe@23783: where berghofe@23783: rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n" berghofe@23783: | ... berghofe@23783: wenzelm@24800: with full support for type-inference, rather than berghofe@23783: berghofe@23783: consts s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set" berghofe@23783: berghofe@23783: abbreviation p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool" berghofe@23783: where "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m" berghofe@23783: berghofe@23783: inductive "s z_1 ... z_m" berghofe@23783: intros berghofe@23783: rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m" berghofe@23783: ... berghofe@23783: berghofe@23783: For backward compatibility, there is a wrapper allowing inductive berghofe@23783: sets to be defined with the new package via berghofe@23783: berghofe@23783: inductive_set berghofe@23783: s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set" berghofe@23783: for z_1 :: U_1 and ... and z_n :: U_m berghofe@23783: where berghofe@23783: rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m" berghofe@23783: | ... berghofe@23783: berghofe@23783: or berghofe@23783: berghofe@23783: inductive_set berghofe@23783: s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set" berghofe@23783: and p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool" berghofe@23783: for z_1 :: U_1 and ... and z_n :: U_m berghofe@23783: where berghofe@23783: "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m" berghofe@23783: | rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n" berghofe@23783: | ... berghofe@23783: berghofe@23783: if the additional syntax "p ..." is required. berghofe@23783: wenzelm@25177: Numerous examples can be found in the subdirectories src/HOL/Auth, wenzelm@25177: src/HOL/Bali, src/HOL/Induct, and src/HOL/MicroJava. berghofe@23783: berghofe@23783: INCOMPATIBILITIES: berghofe@23783: berghofe@23783: - Since declaration and definition of inductive sets or predicates wenzelm@24800: is no longer separated, abbreviations involving the newly wenzelm@24800: introduced sets or predicates must be specified together with the wenzelm@24800: introduction rules after the 'where' keyword (see above), rather wenzelm@24800: than before the actual inductive definition. wenzelm@24800: wenzelm@24800: - The variables in induction and elimination rules are now wenzelm@24800: quantified in the order of their occurrence in the introduction wenzelm@24800: rules, rather than in alphabetical order. Since this may break wenzelm@24800: some proofs, these proofs either have to be repaired, e.g. by wenzelm@24800: reordering the variables a_i_1 ... a_i_{k_i} in Isar 'case' wenzelm@24800: statements of the form berghofe@23783: berghofe@23783: case (rule_i a_i_1 ... a_i_{k_i}) berghofe@23783: berghofe@23783: or the old order of quantification has to be restored by explicitly adding berghofe@23783: meta-level quantifiers in the introduction rules, i.e. berghofe@23783: berghofe@23783: | rule_i: "!!a_i_1 ... a_i_{k_i}. ... ==> p z_1 ... z_m t_i_1 ... t_i_n" berghofe@23783: berghofe@23783: - The format of the elimination rules is now berghofe@23783: berghofe@23783: p z_1 ... z_m x_1 ... x_n ==> berghofe@23783: (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P) berghofe@23783: ==> ... ==> P berghofe@23783: berghofe@23783: for predicates and berghofe@23783: berghofe@23783: (x_1, ..., x_n) : s z_1 ... z_m ==> berghofe@23783: (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P) berghofe@23783: ==> ... ==> P berghofe@23783: berghofe@23783: for sets rather than berghofe@23783: berghofe@23783: x : s z_1 ... z_m ==> berghofe@23783: (!!a_1_1 ... a_1_{k_1}. x = (t_1_1, ..., t_1_n) ==> ... ==> P) berghofe@23783: ==> ... ==> P berghofe@23783: wenzelm@24800: This may require terms in goals to be expanded to n-tuples wenzelm@24800: (e.g. using case_tac or simplification with the split_paired_all wenzelm@24800: rule) before the above elimination rule is applicable. wenzelm@24800: wenzelm@24800: - The elimination or case analysis rules for (mutually) inductive wenzelm@24800: sets or predicates are now called "p_1.cases" ... "p_k.cases". The wenzelm@24800: list of rules "p_1_..._p_k.elims" is no longer available. berghofe@23783: krauss@25198: * New package "function"/"fun" for general recursive functions, krauss@25198: supporting mutual and nested recursion, definitions in local contexts, krauss@25198: more general pattern matching and partiality. See HOL/ex/Fundefs.thy krauss@25198: for small examples, and the separate tutorial on the function krauss@25198: package. The old recdef "package" is still available as before, but krauss@25198: users are encouraged to use the new package. krauss@25198: krauss@25198: * Method "lexicographic_order" automatically synthesizes termination krauss@25198: relations as lexicographic combinations of size measures. krauss@25198: wenzelm@24800: * Case-expressions allow arbitrary constructor-patterns (including wenzelm@24800: "_") and take their order into account, like in functional wenzelm@24800: programming. Internally, this is translated into nested wenzelm@24800: case-expressions; missing cases are added and mapped to the predefined wenzelm@24800: constant "undefined". In complicated cases printing may no longer show wenzelm@24800: the original input but the internal form. Lambda-abstractions allow wenzelm@24800: the same form of pattern matching: "% pat1 => e1 | ..." is an wenzelm@24800: abbreviation for "%x. case x of pat1 => e1 | ..." where x is a new wenzelm@24800: variable. nipkow@23564: huffman@23468: * IntDef: The constant "int :: nat => int" has been removed; now "int" wenzelm@24800: is an abbreviation for "of_nat :: nat => int". The simplification wenzelm@24800: rules for "of_nat" have been changed to work like "int" did wenzelm@24800: previously. Potential INCOMPATIBILITY: huffman@23468: - "of_nat (Suc m)" simplifies to "1 + of_nat m" instead of "of_nat m + 1" huffman@23468: - of_nat_diff and of_nat_mult are no longer default simp rules huffman@23377: chaieb@23295: * Method "algebra" solves polynomial equations over (semi)rings using wenzelm@24800: Groebner bases. The (semi)ring structure is defined by locales and the wenzelm@24800: tool setup depends on that generic context. Installing the method for wenzelm@24800: a specific type involves instantiating the locale and possibly adding wenzelm@24800: declarations for computation on the coefficients. The method is wenzelm@24800: already instantiated for natural numbers and for the axiomatic class wenzelm@24800: of idoms with numerals. See also the paper by Chaieb and Wenzel at wenzelm@24800: CALCULEMUS 2007 for the general principles underlying this wenzelm@24800: architecture of context-aware proof-tools. wenzelm@24800: wenzelm@25033: * Method "ferrack" implements quantifier elimination over wenzelm@25033: special-purpose dense linear orders using locales (analogous to wenzelm@25033: "algebra"). The method is already installed for class wenzelm@25033: {ordered_field,recpower,number_ring} which subsumes real, hyperreal, wenzelm@25033: rat, etc. wenzelm@25033: wenzelm@24800: * Former constant "List.op @" now named "List.append". Use ML wenzelm@24800: antiquotations @{const_name List.append} or @{term " ... @ ... "} to wenzelm@24800: circumvent possible incompatibilities when working on ML level. wenzelm@24800: haftmann@24996: * primrec: missing cases mapped to "undefined" instead of "arbitrary". haftmann@22845: wenzelm@24800: * New function listsum :: 'a list => 'a for arbitrary monoids. wenzelm@24800: Special syntax: "SUM x <- xs. f x" (and latex variants) wenzelm@24800: wenzelm@24800: * New syntax for Haskell-like list comprehension (input only), eg. wenzelm@25177: [(x,y). x <- xs, y <- ys, x ~= y], see also src/HOL/List.thy. wenzelm@24800: wenzelm@24800: * The special syntax for function "filter" has changed from [x : wenzelm@24800: xs. P] to [x <- xs. P] to avoid an ambiguity caused by list wenzelm@24800: comprehension syntax, and for uniformity. INCOMPATIBILITY. wenzelm@24800: wenzelm@24800: * [a..b] is now defined for arbitrary linear orders. It used to be wenzelm@24800: defined on nat only, as an abbreviation for [a.. B" for equality on bool (with priority wenzelm@17996: 25 like -->); output depends on the "iff" print_mode, the default is wenzelm@17996: "A = B" (with priority 50). wenzelm@17996: wenzelm@21265: * Relations less (<) and less_eq (<=) are also available on type bool. wenzelm@21265: Modified syntax to disallow nesting without explicit parentheses, wenzelm@24800: e.g. "(x < y) < z" or "x < (y < z)", but NOT "x < y < z". Potential wenzelm@24800: INCOMPATIBILITY. wenzelm@21265: nipkow@18674: * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only). nipkow@18674: krauss@20716: * Relation composition operator "op O" now has precedence 75 and binds krauss@20716: stronger than union and intersection. INCOMPATIBILITY. krauss@20716: wenzelm@22126: * The old set interval syntax "{m..n(}" (and relatives) has been wenzelm@22126: removed. Use "{m.. ==> False", equivalences wenzelm@24800: (i.e. "=" on type bool) are handled, variable names of the form wenzelm@24800: "lit_" are no longer reserved, significant speedup. wenzelm@24800: wenzelm@24800: * Methods "sat" and "satx" can now replay MiniSat proof traces. wenzelm@22126: zChaff is still supported as well. wenzelm@22126: wenzelm@22126: * 'inductive' and 'datatype': provide projections of mutual rules, wenzelm@22126: bundled as foo_bar.inducts; wenzelm@22126: wenzelm@22126: * Library: moved theories Parity, GCD, Binomial, Infinite_Set to wenzelm@22126: Library. wenzelm@21256: wenzelm@21256: * Library: moved theory Accessible_Part to main HOL. wenzelm@19572: wenzelm@18446: * Library: added theory Coinductive_List of potentially infinite lists wenzelm@18446: as greatest fixed-point. wenzelm@18399: wenzelm@19254: * Library: added theory AssocList which implements (finite) maps as schirmer@19252: association lists. webertj@17809: wenzelm@24800: * Method "evaluation" solves goals (i.e. a boolean expression) wenzelm@24800: efficiently by compiling it to ML. The goal is "proved" (via an wenzelm@24800: oracle) if it evaluates to True. wenzelm@20807: wenzelm@20807: * Linear arithmetic now splits certain operators (e.g. min, max, abs) wenzelm@24800: also when invoked by the simplifier. This results in the Simplifier wenzelm@24800: being more powerful on arithmetic goals. INCOMPATIBILITY. wenzelm@24800: Configuration option fast_arith_split_limit=0 recovers the old wenzelm@24800: behavior. webertj@20217: wenzelm@22126: * Support for hex (0x20) and binary (0b1001) numerals. wenzelm@19254: wenzelm@20807: * New method: reify eqs (t), where eqs are equations for an wenzelm@20807: interpretation I :: 'a list => 'b => 'c and t::'c is an optional wenzelm@20807: parameter, computes a term s::'b and a list xs::'a list and proves the wenzelm@20807: theorem I xs s = t. This is also known as reification or quoting. The wenzelm@20807: resulting theorem is applied to the subgoal to substitute t with I xs wenzelm@20807: s. If t is omitted, the subgoal itself is reified. wenzelm@20807: wenzelm@20807: * New method: reflection corr_thm eqs (t). The parameters eqs and (t) wenzelm@20807: are as explained above. corr_thm is a theorem for I vs (f t) = I vs t, wenzelm@20807: where f is supposed to be a computable function (in the sense of code wenzelm@20807: generattion). The method uses reify to compute s and xs as above then wenzelm@20807: applies corr_thm and uses normalization by evaluation to "prove" f s = wenzelm@20807: r and finally gets the theorem t = r, which is again applied to the wenzelm@25177: subgoal. An Example is available in src/HOL/ex/ReflectionEx.thy. wenzelm@25177: wenzelm@25177: * Reflection: Automatic reification now handels binding, an example is wenzelm@25177: available in src/HOL/ex/ReflectionEx.thy wenzelm@20807: wenzelm@25397: * HOL-Statespace: ``State Spaces: The Locale Way'' introduces a schirmer@25409: command 'statespace' that is similar to 'record', but introduces an wenzelm@25397: abstract specification based on the locale infrastructure instead of wenzelm@25397: HOL types. This leads to extra flexibility in composing state spaces, wenzelm@25397: in particular multiple inheritance and renaming of components. wenzelm@25397: wenzelm@25397: wenzelm@19653: *** HOL-Complex *** wenzelm@19653: huffman@22971: * Hyperreal: Functions root and sqrt are now defined on negative real huffman@22971: inputs so that root n (- x) = - root n x and sqrt (- x) = - sqrt x. huffman@22971: Nonnegativity side conditions have been removed from many lemmas, so huffman@22971: that more subgoals may now be solved by simplification; potential huffman@22971: INCOMPATIBILITY. huffman@22971: wenzelm@24800: * Real: new type classes formalize real normed vector spaces and huffman@21791: algebras, using new overloaded constants scaleR :: real => 'a => 'a huffman@21791: and norm :: 'a => real. huffman@21791: wenzelm@24800: * Real: constant of_real :: real => 'a::real_algebra_1 injects from wenzelm@24800: reals into other types. The overloaded constant Reals :: 'a set is now wenzelm@24800: defined as range of_real; potential INCOMPATIBILITY. wenzelm@24800: wenzelm@24800: * Real: proper support for ML code generation, including 'quickcheck'. nipkow@23013: Reals are implemented as arbitrary precision rationals. nipkow@23013: wenzelm@22126: * Hyperreal: Several constants that previously worked only for the wenzelm@22126: reals have been generalized, so they now work over arbitrary vector wenzelm@22126: spaces. Type annotations may need to be added in some cases; potential wenzelm@22126: INCOMPATIBILITY. huffman@21791: huffman@22972: Infinitesimal :: ('a::real_normed_vector) star set huffman@22972: HFinite :: ('a::real_normed_vector) star set huffman@22972: HInfinite :: ('a::real_normed_vector) star set huffman@21791: approx :: ('a::real_normed_vector) star => 'a star => bool huffman@21791: monad :: ('a::real_normed_vector) star => 'a star set huffman@21791: galaxy :: ('a::real_normed_vector) star => 'a star set huffman@22972: (NS)LIMSEQ :: [nat => 'a::real_normed_vector, 'a] => bool huffman@21791: (NS)convergent :: (nat => 'a::real_normed_vector) => bool huffman@21791: (NS)Bseq :: (nat => 'a::real_normed_vector) => bool huffman@21791: (NS)Cauchy :: (nat => 'a::real_normed_vector) => bool huffman@21791: (NS)LIM :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool huffman@21791: is(NS)Cont :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool huffman@21791: deriv :: ['a::real_normed_field => 'a, 'a, 'a] => bool huffman@22972: sgn :: 'a::real_normed_vector => 'a huffman@23116: exp :: 'a::{recpower,real_normed_field,banach} => 'a huffman@21791: huffman@21791: * Complex: Some complex-specific constants are now abbreviations for wenzelm@22126: overloaded ones: complex_of_real = of_real, cmod = norm, hcmod = wenzelm@22126: hnorm. Other constants have been entirely removed in favor of the wenzelm@22126: polymorphic versions (INCOMPATIBILITY): huffman@21791: huffman@21791: approx <-- capprox huffman@21791: HFinite <-- CFinite huffman@21791: HInfinite <-- CInfinite huffman@21791: Infinitesimal <-- CInfinitesimal huffman@21791: monad <-- cmonad huffman@21791: galaxy <-- cgalaxy huffman@21791: (NS)LIM <-- (NS)CLIM, (NS)CRLIM huffman@21791: is(NS)Cont <-- is(NS)Contc, is(NS)contCR huffman@21791: (ns)deriv <-- (ns)cderiv huffman@21791: wenzelm@19653: wenzelm@24801: *** HOL-Algebra *** wenzelm@24801: wenzelm@24801: * Formalisation of ideals and the quotient construction over rings. wenzelm@24801: wenzelm@24801: * Order and lattice theory no longer based on records. wenzelm@24801: INCOMPATIBILITY. wenzelm@24801: wenzelm@24801: * Renamed lemmas least_carrier -> least_closed and greatest_carrier -> wenzelm@24801: greatest_closed. INCOMPATIBILITY. wenzelm@24801: wenzelm@24801: * Method algebra is now set up via an attribute. For examples see wenzelm@24801: Ring.thy. INCOMPATIBILITY: the method is now weaker on combinations wenzelm@24801: of algebraic structures. wenzelm@24801: wenzelm@24801: * Renamed theory CRing to Ring. wenzelm@24801: wenzelm@24801: wenzelm@24801: *** HOL-Nominal *** wenzelm@24801: wenzelm@25148: * Substantial, yet incomplete support for nominal datatypes (binding wenzelm@25177: structures) based on HOL-Nominal logic. See src/HOL/Nominal and wenzelm@25177: src/HOL/Nominal/Examples. Prospective users should consult wenzelm@25148: http://isabelle.in.tum.de/nominal/ wenzelm@25148: wenzelm@24801: wenzelm@17878: *** ML *** wenzelm@17878: wenzelm@24643: * ML basics: just one true type int, which coincides with IntInf.int wenzelm@24643: (even on SML/NJ). wenzelm@24643: wenzelm@22138: * ML within Isar: antiquotations allow to embed statically-checked wenzelm@22138: formal entities in the source, referring to the context available at wenzelm@22138: compile-time. For example: wenzelm@22138: wenzelm@25142: ML {* @{sort "{zero,one}"} *} wenzelm@22138: ML {* @{typ "'a => 'b"} *} wenzelm@22138: ML {* @{term "%x. x"} *} wenzelm@22138: ML {* @{prop "x == y"} *} wenzelm@22138: ML {* @{ctyp "'a => 'b"} *} wenzelm@22138: ML {* @{cterm "%x. x"} *} wenzelm@22138: ML {* @{cprop "x == y"} *} wenzelm@22138: ML {* @{thm asm_rl} *} wenzelm@22138: ML {* @{thms asm_rl} *} wenzelm@24692: ML {* @{type_name c} *} wenzelm@25142: ML {* @{type_syntax c} *} wenzelm@22376: ML {* @{const_name c} *} wenzelm@22376: ML {* @{const_syntax c} *} wenzelm@22138: ML {* @{context} *} wenzelm@22138: ML {* @{theory} *} wenzelm@22138: ML {* @{theory Pure} *} wenzelm@24692: ML {* @{theory_ref} *} wenzelm@24692: ML {* @{theory_ref Pure} *} wenzelm@22138: ML {* @{simpset} *} wenzelm@22138: ML {* @{claset} *} wenzelm@22138: ML {* @{clasimpset} *} wenzelm@22138: wenzelm@22151: The same works for sources being ``used'' within an Isar context. wenzelm@22151: wenzelm@22152: * ML in Isar: improved error reporting; extra verbosity with wenzelm@24706: ML_Context.trace enabled. wenzelm@22152: wenzelm@19032: * Pure/General/table.ML: the join operations now works via exceptions wenzelm@24706: DUP/SAME instead of type option. This is simpler in simple cases, and wenzelm@19081: admits slightly more efficient complex applications. wenzelm@18446: wenzelm@24800: * Pure: 'advanced' translation functions (parse_translation etc.) now wenzelm@24800: use Context.generic instead of just theory. wenzelm@24800: wenzelm@18642: * Pure: datatype Context.generic joins theory/Proof.context and wenzelm@18644: provides some facilities for code that works in either kind of wenzelm@18642: context, notably GenericDataFun for uniform theory and proof data. wenzelm@18642: wenzelm@18737: * Pure: simplified internal attribute type, which is now always wenzelm@24706: Context.generic * thm -> Context.generic * thm. Global (theory) vs. wenzelm@24706: local (Proof.context) attributes have been discontinued, while wenzelm@24706: minimizing code duplication. Thm.rule_attribute and wenzelm@24706: Thm.declaration_attribute build canonical attributes; see also structure wenzelm@24706: Context for further operations on Context.generic, notably wenzelm@24706: GenericDataFun. INCOMPATIBILITY, need to adapt attribute type wenzelm@19006: declarations and definitions. wenzelm@19006: wenzelm@24800: * Context data interfaces (Theory/Proof/GenericDataFun): removed wenzelm@24800: name/print, uninitialized data defaults to ad-hoc copy of empty value, wenzelm@24800: init only required for impure data. INCOMPATIBILITY: empty really need wenzelm@24800: to be empty (no dependencies on theory content!) wenzelm@24800: wenzelm@19508: * Pure/kernel: consts certification ignores sort constraints given in wenzelm@24800: signature declarations. (This information is not relevant to the wenzelm@24800: logic, but only for type inference.) SIGNIFICANT INTERNAL CHANGE, wenzelm@24800: potential INCOMPATIBILITY. wenzelm@19508: wenzelm@19508: * Pure: axiomatic type classes are now purely definitional, with wenzelm@19508: explicit proofs of class axioms and super class relations performed wenzelm@24706: internally. See Pure/axclass.ML for the main internal interfaces -- wenzelm@19508: notably AxClass.define_class supercedes AxClass.add_axclass, and wenzelm@24706: AxClass.axiomatize_class/classrel/arity supersede wenzelm@19508: Sign.add_classes/classrel/arities. wenzelm@19508: wenzelm@19006: * Pure/Isar: Args/Attrib parsers operate on Context.generic -- wenzelm@19006: global/local versions on theory vs. Proof.context have been wenzelm@19006: discontinued; Attrib.syntax and Method.syntax have been adapted wenzelm@19006: accordingly. INCOMPATIBILITY, need to adapt parser expressions for wenzelm@19006: attributes, methods, etc. wenzelm@18642: wenzelm@18446: * Pure: several functions of signature "... -> theory -> theory * ..." wenzelm@18446: have been reoriented to "... -> theory -> ... * theory" in order to wenzelm@18446: allow natural usage in combination with the ||>, ||>>, |-> and wenzelm@18446: fold_map combinators. haftmann@18051: wenzelm@21647: * Pure: official theorem names (closed derivations) and additional wenzelm@21647: comments (tags) are now strictly separate. Name hints -- which are wenzelm@21647: maintained as tags -- may be attached any time without affecting the wenzelm@21647: derivation. wenzelm@21647: wenzelm@18020: * Pure: primitive rule lift_rule now takes goal cterm instead of an wenzelm@18145: actual goal state (thm). Use Thm.lift_rule (Thm.cprem_of st i) to wenzelm@18020: achieve the old behaviour. wenzelm@18020: wenzelm@18020: * Pure: the "Goal" constant is now called "prop", supporting a wenzelm@18020: slightly more general idea of ``protecting'' meta-level rule wenzelm@18020: statements. wenzelm@18020: wenzelm@20040: * Pure: Logic.(un)varify only works in a global context, which is now wenzelm@20040: enforced instead of silently assumed. INCOMPATIBILITY, may use wenzelm@20040: Logic.legacy_(un)varify as temporary workaround. wenzelm@20040: wenzelm@20090: * Pure: structure Name provides scalable operations for generating wenzelm@20090: internal variable names, notably Name.variants etc. This replaces wenzelm@20090: some popular functions from term.ML: wenzelm@20090: wenzelm@20090: Term.variant -> Name.variant wenzelm@24800: Term.variantlist -> Name.variant_list wenzelm@20090: Term.invent_names -> Name.invent_list wenzelm@20090: wenzelm@20090: Note that low-level renaming rarely occurs in new code -- operations wenzelm@20090: from structure Variable are used instead (see below). wenzelm@20090: wenzelm@20040: * Pure: structure Variable provides fundamental operations for proper wenzelm@20040: treatment of fixed/schematic variables in a context. For example, wenzelm@20040: Variable.import introduces fixes for schematics of given facts and wenzelm@20040: Variable.export reverses the effect (up to renaming) -- this replaces wenzelm@20040: various freeze_thaw operations. wenzelm@20040: wenzelm@18567: * Pure: structure Goal provides simple interfaces for wenzelm@17981: init/conclude/finish and tactical prove operations (replacing former wenzelm@20040: Tactic.prove). Goal.prove is the canonical way to prove results wenzelm@20040: within a given context; Goal.prove_global is a degraded version for wenzelm@20040: theory level goals, including a global Drule.standard. Note that wenzelm@20040: OldGoals.prove_goalw_cterm has long been obsolete, since it is wenzelm@20040: ill-behaved in a local proof context (e.g. with local fixes/assumes or wenzelm@20040: in a locale context). wenzelm@17981: wenzelm@24706: * Pure/Syntax: generic interfaces for parsing (Syntax.parse_term etc.) wenzelm@24706: and type checking (Syntax.check_term etc.), with common combinations wenzelm@24706: (Syntax.read_term etc.). These supersede former Sign.read_term etc. wenzelm@24706: which are considered legacy and await removal. wenzelm@24706: wenzelm@24920: * Pure/Syntax: generic interfaces for type unchecking wenzelm@24920: (Syntax.uncheck_terms etc.) and unparsing (Syntax.unparse_term etc.), wenzelm@24920: with common combinations (Syntax.pretty_term, Syntax.string_of_term wenzelm@24920: etc.). Former Sign.pretty_term, Sign.string_of_term etc. are still wenzelm@24924: available for convenience, but refer to the very same operations using wenzelm@24924: a mere theory instead of a full context. wenzelm@24920: wenzelm@18815: * Isar: simplified treatment of user-level errors, using exception wenzelm@18687: ERROR of string uniformly. Function error now merely raises ERROR, wenzelm@18686: without any side effect on output channels. The Isar toplevel takes wenzelm@18686: care of proper display of ERROR exceptions. ML code may use plain wenzelm@18686: handle/can/try; cat_error may be used to concatenate errors like this: wenzelm@18686: wenzelm@18686: ... handle ERROR msg => cat_error msg "..." wenzelm@18686: wenzelm@18686: Toplevel ML code (run directly or through the Isar toplevel) may be wenzelm@18687: embedded into the Isar toplevel with exception display/debug like wenzelm@18687: this: wenzelm@18686: wenzelm@18686: Isar.toplevel (fn () => ...) wenzelm@18686: wenzelm@18686: INCOMPATIBILITY, removed special transform_error facilities, removed wenzelm@18686: obsolete variants of user-level exceptions (ERROR_MESSAGE, wenzelm@18686: Context.PROOF, ProofContext.CONTEXT, Proof.STATE, ProofHistory.FAIL) wenzelm@18686: -- use plain ERROR instead. wenzelm@18686: wenzelm@18815: * Isar: theory setup now has type (theory -> theory), instead of a wenzelm@18722: list. INCOMPATIBILITY, may use #> to compose setup functions. wenzelm@18722: wenzelm@24706: * Isar: ML toplevel pretty printer for type Proof.context, subject to wenzelm@24706: ProofContext.debug/verbose flags. wenzelm@18815: wenzelm@18815: * Isar: Toplevel.theory_to_proof admits transactions that modify the wenzelm@18815: theory before entering a proof state. Transactions now always see a wenzelm@18815: quasi-functional intermediate checkpoint, both in interactive and wenzelm@18590: batch mode. wenzelm@18567: wenzelm@24867: * Isar: simplified interfaces for outer syntax. Renamed wenzelm@24867: OuterSyntax.add_keywords to OuterSyntax.keywords. Removed wenzelm@24867: OuterSyntax.add_parsers -- this functionality is now included in wenzelm@24867: OuterSyntax.command etc. INCOMPATIBILITY. wenzelm@24867: wenzelm@17878: * Simplifier: the simpset of a running simplification process now wenzelm@17878: contains a proof context (cf. Simplifier.the_context), which is the wenzelm@17878: very context that the initial simpset has been retrieved from (by wenzelm@17890: simpset_of/local_simpset_of). Consequently, all plug-in components wenzelm@17878: (solver, looper etc.) may depend on arbitrary proof data. wenzelm@17878: wenzelm@17878: * Simplifier.inherit_context inherits the proof context (plus the wenzelm@17878: local bounds) of the current simplification process; any simproc wenzelm@17878: etc. that calls the Simplifier recursively should do this! Removed wenzelm@17878: former Simplifier.inherit_bounds, which is already included here -- wenzelm@17890: INCOMPATIBILITY. Tools based on low-level rewriting may even have to wenzelm@17890: specify an explicit context using Simplifier.context/theory_context. wenzelm@17878: wenzelm@17878: * Simplifier/Classical Reasoner: more abstract interfaces wenzelm@17878: change_simpset/claset for modifying the simpset/claset reference of a wenzelm@17878: theory; raw versions simpset/claset_ref etc. have been discontinued -- wenzelm@17878: INCOMPATIBILITY. wenzelm@17878: wenzelm@18540: * Provers: more generic wrt. syntax of object-logics, avoid hardwired wenzelm@18540: "Trueprop" etc. wenzelm@18540: wenzelm@17878: wenzelm@20988: *** System *** wenzelm@20988: wenzelm@25433: * settings: the default heap location within ISABELLE_HOME_USER now wenzelm@25433: includes ISABELLE_IDENTIFIER. This simplifies use of multiple wenzelm@25433: Isabelle installations. wenzelm@21471: wenzelm@20988: * isabelle-process: option -S (secure mode) disables some critical wenzelm@20988: operations, notably runtime compilation and evaluation of ML source wenzelm@20988: code. wenzelm@20988: wenzelm@24891: * Basic Isabelle mode for jEdit, see Isabelle/lib/jedit/. wenzelm@24891: wenzelm@24801: * Support for parallel execution, using native multicore support of wenzelm@24800: Poly/ML 5.1. The theory loader exploits parallelism when processing wenzelm@24800: independent theories, according to the given theory header wenzelm@24800: specifications. The maximum number of worker threads is specified via wenzelm@24800: usedir option -M or the "max-threads" setting in Proof General. A wenzelm@24800: speedup factor of 1.5--3.5 can be expected on a 4-core machine, and up wenzelm@24800: to 6 on a 8-core machine. User-code needs to observe certain wenzelm@24800: guidelines for thread-safe programming, see appendix A in the Isar wenzelm@24800: Implementation manual. wenzelm@24210: wenzelm@17754: wenzelm@25448: wenzelm@17720: New in Isabelle2005 (October 2005) wenzelm@17720: ---------------------------------- wenzelm@14655: wenzelm@14655: *** General *** wenzelm@14655: nipkow@15130: * Theory headers: the new header syntax for Isar theories is nipkow@15130: nipkow@15130: theory wenzelm@16234: imports ... wenzelm@16234: uses ... nipkow@15130: begin nipkow@15130: wenzelm@16234: where the 'uses' part is optional. The previous syntax wenzelm@16234: wenzelm@16234: theory = + ... + : wenzelm@16234: wenzelm@16717: will disappear in the next release. Use isatool fixheaders to convert wenzelm@16717: existing theory files. Note that there is no change in ancient wenzelm@17371: non-Isar theories now, but these will disappear soon. nipkow@15130: berghofe@15475: * Theory loader: parent theories can now also be referred to via wenzelm@16234: relative and absolute paths. wenzelm@16234: wenzelm@17408: * Command 'find_theorems' searches for a list of criteria instead of a wenzelm@17408: list of constants. Known criteria are: intro, elim, dest, name:string, wenzelm@17408: simp:term, and any term. Criteria can be preceded by '-' to select wenzelm@17408: theorems that do not match. Intro, elim, dest select theorems that wenzelm@17408: match the current goal, name:s selects theorems whose fully qualified wenzelm@17408: name contain s, and simp:term selects all simplification rules whose wenzelm@17408: lhs match term. Any other term is interpreted as pattern and selects wenzelm@17408: all theorems matching the pattern. Available in ProofGeneral under wenzelm@17408: 'ProofGeneral -> Find Theorems' or C-c C-f. Example: wenzelm@16234: wenzelm@17275: C-c C-f (100) "(_::nat) + _ + _" intro -name: "HOL." wenzelm@16234: wenzelm@16234: prints the last 100 theorems matching the pattern "(_::nat) + _ + _", wenzelm@16234: matching the current goal as introduction rule and not having "HOL." wenzelm@16234: in their name (i.e. not being defined in theory HOL). wenzelm@16013: wenzelm@17408: * Command 'thms_containing' has been discontinued in favour of wenzelm@17408: 'find_theorems'; INCOMPATIBILITY. wenzelm@17408: wenzelm@17385: * Communication with Proof General is now 8bit clean, which means that wenzelm@17385: Unicode text in UTF-8 encoding may be used within theory texts (both wenzelm@17408: formal and informal parts). Cf. option -U of the Isabelle Proof wenzelm@17538: General interface. Here are some simple examples (cf. src/HOL/ex): wenzelm@17538: wenzelm@17538: http://isabelle.in.tum.de/library/HOL/ex/Hebrew.html wenzelm@17538: http://isabelle.in.tum.de/library/HOL/ex/Chinese.html wenzelm@17385: wenzelm@17425: * Improved efficiency of the Simplifier and, to a lesser degree, the wenzelm@17425: Classical Reasoner. Typical big applications run around 2 times wenzelm@17425: faster. wenzelm@17425: wenzelm@15703: wenzelm@15703: *** Document preparation *** wenzelm@15703: wenzelm@16234: * Commands 'display_drafts' and 'print_drafts' perform simple output wenzelm@16234: of raw sources. Only those symbols that do not require additional wenzelm@16234: LaTeX packages (depending on comments in isabellesym.sty) are wenzelm@16234: displayed properly, everything else is left verbatim. isatool display wenzelm@16234: and isatool print are used as front ends (these are subject to the wenzelm@16234: DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively). wenzelm@16234: wenzelm@17047: * Command tags control specific markup of certain regions of text, wenzelm@17047: notably folding and hiding. Predefined tags include "theory" (for wenzelm@17047: theory begin and end), "proof" for proof commands, and "ML" for wenzelm@17047: commands involving ML code; the additional tags "visible" and wenzelm@17047: "invisible" are unused by default. Users may give explicit tag wenzelm@17047: specifications in the text, e.g. ''by %invisible (auto)''. The wenzelm@17047: interpretation of tags is determined by the LaTeX job during document wenzelm@17047: preparation: see option -V of isatool usedir, or options -n and -t of wenzelm@17047: isatool document, or even the LaTeX macros \isakeeptag, \isafoldtag, wenzelm@17047: \isadroptag. wenzelm@17047: wenzelm@17047: Several document versions may be produced at the same time via isatool wenzelm@17047: usedir (the generated index.html will link all of them). Typical wenzelm@17047: specifications include ''-V document=theory,proof,ML'' to present wenzelm@17047: theory/proof/ML parts faithfully, ''-V outline=/proof,/ML'' to fold wenzelm@17047: proof and ML commands, and ''-V mutilated=-theory,-proof,-ML'' to omit wenzelm@17047: these parts without any formal replacement text. The Isabelle site wenzelm@17047: default settings produce ''document'' and ''outline'' versions as wenzelm@17047: specified above. wenzelm@16234: haftmann@17402: * Several new antiquotations: wenzelm@15979: wenzelm@15979: @{term_type term} prints a term with its type annotated; wenzelm@15979: wenzelm@15979: @{typeof term} prints the type of a term; wenzelm@15979: wenzelm@16234: @{const const} is the same as @{term const}, but checks that the wenzelm@16234: argument is a known logical constant; wenzelm@15979: wenzelm@15979: @{term_style style term} and @{thm_style style thm} print a term or wenzelm@16234: theorem applying a "style" to it wenzelm@16234: wenzelm@17117: @{ML text} wenzelm@17117: wenzelm@16234: Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of wenzelm@16234: definitions, equations, inequations etc., 'concl' printing only the schirmer@17393: conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem19' wenzelm@16234: to print the specified premise. TermStyle.add_style provides an ML wenzelm@16234: interface for introducing further styles. See also the "LaTeX Sugar" wenzelm@17117: document practical applications. The ML antiquotation prints wenzelm@17117: type-checked ML expressions verbatim. wenzelm@16234: wenzelm@17259: * Markup commands 'chapter', 'section', 'subsection', 'subsubsection', wenzelm@17259: and 'text' support optional locale specification '(in loc)', which wenzelm@17269: specifies the default context for interpreting antiquotations. For wenzelm@17269: example: 'text (in lattice) {* @{thm inf_assoc}*}'. wenzelm@17259: wenzelm@17259: * Option 'locale=NAME' of antiquotations specifies an alternative wenzelm@17259: context interpreting the subsequent argument. For example: @{thm wenzelm@17269: [locale=lattice] inf_assoc}. wenzelm@17259: wenzelm@17097: * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within wenzelm@17097: a proof context. wenzelm@17097: wenzelm@17097: * Proper output of antiquotations for theory commands involving a wenzelm@17097: proof context (such as 'locale' or 'theorem (in loc) ...'). wenzelm@17097: wenzelm@17193: * Delimiters of outer tokens (string etc.) now produce separate LaTeX wenzelm@17193: macros (\isachardoublequoteopen, isachardoublequoteclose etc.). wenzelm@17193: wenzelm@17193: * isatool usedir: new option -C (default true) controls whether option wenzelm@17193: -D should include a copy of the original document directory; -C false wenzelm@17193: prevents unwanted effects such as copying of administrative CVS data. wenzelm@17193: wenzelm@16234: wenzelm@16234: *** Pure *** wenzelm@16234: wenzelm@16234: * Considerably improved version of 'constdefs' command. Now performs wenzelm@16234: automatic type-inference of declared constants; additional support for wenzelm@16234: local structure declarations (cf. locales and HOL records), see also wenzelm@16234: isar-ref manual. Potential INCOMPATIBILITY: need to observe strictly wenzelm@16234: sequential dependencies of definitions within a single 'constdefs' wenzelm@16234: section; moreover, the declared name needs to be an identifier. If wenzelm@16234: all fails, consider to fall back on 'consts' and 'defs' separately. wenzelm@16234: wenzelm@16234: * Improved indexed syntax and implicit structures. First of all, wenzelm@16234: indexed syntax provides a notational device for subscripted wenzelm@16234: application, using the new syntax \<^bsub>term\<^esub> for arbitrary wenzelm@16234: expressions. Secondly, in a local context with structure wenzelm@16234: declarations, number indexes \<^sub>n or the empty index (default wenzelm@16234: number 1) refer to a certain fixed variable implicitly; option wenzelm@16234: show_structs controls printing of implicit structures. Typical wenzelm@16234: applications of these concepts involve record types and locales. wenzelm@16234: wenzelm@16234: * New command 'no_syntax' removes grammar declarations (and wenzelm@16234: translations) resulting from the given syntax specification, which is wenzelm@16234: interpreted in the same manner as for the 'syntax' command. wenzelm@16234: wenzelm@16234: * 'Advanced' translation functions (parse_translation etc.) may depend wenzelm@16234: on the signature of the theory context being presently used for wenzelm@16234: parsing/printing, see also isar-ref manual. wenzelm@16234: wenzelm@16856: * Improved 'oracle' command provides a type-safe interface to turn an wenzelm@16856: ML expression of type theory -> T -> term into a primitive rule of wenzelm@16856: type theory -> T -> thm (i.e. the functionality of Thm.invoke_oracle wenzelm@16856: is already included here); see also FOL/ex/IffExample.thy; wenzelm@16856: INCOMPATIBILITY. wenzelm@16856: wenzelm@17275: * axclass: name space prefix for class "c" is now "c_class" (was "c" wenzelm@17275: before); "cI" is no longer bound, use "c.intro" instead. wenzelm@17275: INCOMPATIBILITY. This change avoids clashes of fact bindings for wenzelm@17275: axclasses vs. locales. wenzelm@17275: wenzelm@16234: * Improved internal renaming of symbolic identifiers -- attach primes wenzelm@16234: instead of base 26 numbers. wenzelm@16234: wenzelm@16234: * New flag show_question_marks controls printing of leading question wenzelm@16234: marks in schematic variable names. wenzelm@16234: wenzelm@16234: * In schematic variable names, *any* symbol following \<^isub> or wenzelm@16234: \<^isup> is now treated as part of the base name. For example, the wenzelm@16234: following works without printing of awkward ".0" indexes: wenzelm@16234: wenzelm@16234: lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1" wenzelm@16234: by simp wenzelm@16234: wenzelm@16234: * Inner syntax includes (*(*nested*) comments*). wenzelm@16234: wenzelm@17548: * Pretty printer now supports unbreakable blocks, specified in mixfix wenzelm@16234: annotations as "(00...)". wenzelm@16234: wenzelm@16234: * Clear separation of logical types and nonterminals, where the latter wenzelm@16234: may only occur in 'syntax' specifications or type abbreviations. wenzelm@16234: Before that distinction was only partially implemented via type class wenzelm@16234: "logic" vs. "{}". Potential INCOMPATIBILITY in rare cases of improper wenzelm@16234: use of 'types'/'consts' instead of 'nonterminals'/'syntax'. Some very wenzelm@16234: exotic syntax specifications may require further adaption wenzelm@17691: (e.g. Cube/Cube.thy). wenzelm@16234: wenzelm@16234: * Removed obsolete type class "logic", use the top sort {} instead. wenzelm@16234: Note that non-logical types should be declared as 'nonterminals' wenzelm@16234: rather than 'types'. INCOMPATIBILITY for new object-logic wenzelm@16234: specifications. wenzelm@16234: ballarin@17095: * Attributes 'induct' and 'cases': type or set names may now be ballarin@17095: locally fixed variables as well. ballarin@17095: wenzelm@16234: * Simplifier: can now control the depth to which conditional rewriting wenzelm@16234: is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth wenzelm@16234: Limit. wenzelm@16234: wenzelm@16234: * Simplifier: simplification procedures may now take the current wenzelm@16234: simpset into account (cf. Simplifier.simproc(_i) / mk_simproc wenzelm@16234: interface), which is very useful for calling the Simplifier wenzelm@16234: recursively. Minor INCOMPATIBILITY: the 'prems' argument of simprocs wenzelm@16234: is gone -- use prems_of_ss on the simpset instead. Moreover, the wenzelm@16234: low-level mk_simproc no longer applies Logic.varify internally, to wenzelm@16234: allow for use in a context of fixed variables. wenzelm@16234: wenzelm@16234: * thin_tac now works even if the assumption being deleted contains !! wenzelm@16234: or ==>. More generally, erule now works even if the major premise of wenzelm@16234: the elimination rule contains !! or ==>. wenzelm@16234: wenzelm@17597: * Method 'rules' has been renamed to 'iprover'. INCOMPATIBILITY. nipkow@17590: wenzelm@16234: * Reorganized bootstrapping of the Pure theories; CPure is now derived wenzelm@16234: from Pure, which contains all common declarations already. Both wenzelm@16234: theories are defined via plain Isabelle/Isar .thy files. wenzelm@16234: INCOMPATIBILITY: elements of CPure (such as the CPure.intro / wenzelm@16234: CPure.elim / CPure.dest attributes) now appear in the Pure name space; wenzelm@16234: use isatool fixcpure to adapt your theory and ML sources. wenzelm@16234: wenzelm@16234: * New syntax 'name(i-j, i-, i, ...)' for referring to specific wenzelm@16234: selections of theorems in named facts via index ranges. wenzelm@16234: wenzelm@17097: * 'print_theorems': in theory mode, really print the difference wenzelm@17097: wrt. the last state (works for interactive theory development only), wenzelm@17097: in proof mode print all local facts (cf. 'print_facts'); wenzelm@17097: wenzelm@17397: * 'hide': option '(open)' hides only base names. wenzelm@17397: wenzelm@17275: * More efficient treatment of intermediate checkpoints in interactive wenzelm@17275: theory development. wenzelm@17275: berghofe@17663: * Code generator is now invoked via code_module (incremental code wenzelm@17664: generation) and code_library (modular code generation, ML structures wenzelm@17664: for each theory). INCOMPATIBILITY: new keywords 'file' and 'contains' wenzelm@17664: must be quoted when used as identifiers. wenzelm@17664: wenzelm@17664: * New 'value' command for reading, evaluating and printing terms using wenzelm@17664: the code generator. INCOMPATIBILITY: command keyword 'value' must be wenzelm@17664: quoted when used as identifier. berghofe@17663: wenzelm@16234: wenzelm@16234: *** Locales *** ballarin@17095: wenzelm@17385: * New commands for the interpretation of locale expressions in wenzelm@17385: theories (1), locales (2) and proof contexts (3). These generate wenzelm@17385: proof obligations from the expression specification. After the wenzelm@17385: obligations have been discharged, theorems of the expression are added wenzelm@17385: to the theory, target locale or proof context. The synopsis of the wenzelm@17385: commands is a follows: wenzelm@17385: ballarin@17095: (1) interpretation expr inst ballarin@17095: (2) interpretation target < expr ballarin@17095: (3) interpret expr inst wenzelm@17385: ballarin@17095: Interpretation in theories and proof contexts require a parameter ballarin@17095: instantiation of terms from the current context. This is applied to wenzelm@17385: specifications and theorems of the interpreted expression. wenzelm@17385: Interpretation in locales only permits parameter renaming through the wenzelm@17385: locale expression. Interpretation is smart in that interpretations wenzelm@17385: that are active already do not occur in proof obligations, neither are wenzelm@17385: instantiated theorems stored in duplicate. Use 'print_interps' to wenzelm@17385: inspect active interpretations of a particular locale. For details, ballarin@17436: see the Isar Reference manual. Examples can be found in ballarin@17436: HOL/Finite_Set.thy and HOL/Algebra/UnivPoly.thy. wenzelm@16234: wenzelm@16234: INCOMPATIBILITY: former 'instantiate' has been withdrawn, use wenzelm@16234: 'interpret' instead. wenzelm@16234: wenzelm@17385: * New context element 'constrains' for adding type constraints to wenzelm@17385: parameters. wenzelm@17385: wenzelm@17385: * Context expressions: renaming of parameters with syntax wenzelm@17385: redeclaration. ballarin@17095: ballarin@17095: * Locale declaration: 'includes' disallowed. ballarin@17095: wenzelm@16234: * Proper static binding of attribute syntax -- i.e. types / terms / wenzelm@16234: facts mentioned as arguments are always those of the locale definition wenzelm@16234: context, independently of the context of later invocations. Moreover, wenzelm@16234: locale operations (renaming and type / term instantiation) are applied wenzelm@16234: to attribute arguments as expected. wenzelm@16234: wenzelm@16234: INCOMPATIBILITY of the ML interface: always pass Attrib.src instead of wenzelm@16234: actual attributes; rare situations may require Attrib.attribute to wenzelm@16234: embed those attributes into Attrib.src that lack concrete syntax. wenzelm@16234: Attribute implementations need to cooperate properly with the static wenzelm@16234: binding mechanism. Basic parsers Args.XXX_typ/term/prop and wenzelm@16234: Attrib.XXX_thm etc. already do the right thing without further wenzelm@16234: intervention. Only unusual applications -- such as "where" or "of" wenzelm@16234: (cf. src/Pure/Isar/attrib.ML), which process arguments depending both wenzelm@16234: on the context and the facts involved -- may have to assign parsed wenzelm@16234: values to argument tokens explicitly. wenzelm@16234: wenzelm@16234: * Changed parameter management in theorem generation for long goal wenzelm@16234: statements with 'includes'. INCOMPATIBILITY: produces a different wenzelm@16234: theorem statement in rare situations. wenzelm@16234: ballarin@17228: * Locale inspection command 'print_locale' omits notes elements. Use ballarin@17228: 'print_locale!' to have them included in the output. ballarin@17228: wenzelm@16234: wenzelm@16234: *** Provers *** wenzelm@16234: wenzelm@16234: * Provers/hypsubst.ML: improved version of the subst method, for wenzelm@16234: single-step rewriting: it now works in bound variable contexts. New is wenzelm@16234: 'subst (asm)', for rewriting an assumption. INCOMPATIBILITY: may wenzelm@16234: rewrite a different subterm than the original subst method, which is wenzelm@16234: still available as 'simplesubst'. wenzelm@16234: wenzelm@16234: * Provers/quasi.ML: new transitivity reasoners for transitivity only wenzelm@16234: and quasi orders. wenzelm@16234: wenzelm@16234: * Provers/trancl.ML: new transitivity reasoner for transitive and wenzelm@16234: reflexive-transitive closure of relations. wenzelm@16234: wenzelm@16234: * Provers/blast.ML: new reference depth_limit to make blast's depth wenzelm@16234: limit (previously hard-coded with a value of 20) user-definable. wenzelm@16234: wenzelm@16234: * Provers/simplifier.ML has been moved to Pure, where Simplifier.setup wenzelm@16234: is peformed already. Object-logics merely need to finish their wenzelm@16234: initial simpset configuration as before. INCOMPATIBILITY. wenzelm@15703: berghofe@15475: schirmer@14700: *** HOL *** schirmer@14700: wenzelm@16234: * Symbolic syntax of Hilbert Choice Operator is now as follows: wenzelm@14878: wenzelm@14878: syntax (epsilon) wenzelm@14878: "_Eps" :: "[pttrn, bool] => 'a" ("(3\_./ _)" [0, 10] 10) wenzelm@14878: wenzelm@16234: The symbol \ is displayed as the alternative epsilon of LaTeX wenzelm@16234: and x-symbol; use option '-m epsilon' to get it actually printed. wenzelm@16234: Moreover, the mathematically important symbolic identifier \ wenzelm@16234: becomes available as variable, constant etc. INCOMPATIBILITY, wenzelm@16234: wenzelm@16234: * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x". wenzelm@16234: Similarly for all quantifiers: "ALL x > y" etc. The x-symbol for >= wenzelm@17371: is \. New transitivity rules have been added to HOL/Orderings.thy to avigad@17016: support corresponding Isar calculations. wenzelm@16234: wenzelm@16234: * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\" wenzelm@16234: instead of ":". wenzelm@16234: wenzelm@16234: * theory SetInterval: changed the syntax for open intervals: wenzelm@16234: wenzelm@16234: Old New wenzelm@16234: {..n(} {.. {\1<\.\.} nipkow@15046: \.\.\([^(}]*\)(} -> \.\.<\1} nipkow@15046: wenzelm@17533: * Theory Commutative_Ring (in Library): method comm_ring for proving wenzelm@17533: equalities in commutative rings; method 'algebra' provides a generic wenzelm@17533: interface. wenzelm@17389: wenzelm@17389: * Theory Finite_Set: changed the syntax for 'setsum', summation over wenzelm@16234: finite sets: "setsum (%x. e) A", which used to be "\x:A. e", is wenzelm@17371: now either "SUM x:A. e" or "\x \ A. e". The bound variable can paulson@17189: be a tuple pattern. wenzelm@16234: wenzelm@16234: Some new syntax forms are available: wenzelm@16234: wenzelm@16234: "\x | P. e" for "setsum (%x. e) {x. P}" wenzelm@16234: "\x = a..b. e" for "setsum (%x. e) {a..b}" wenzelm@16234: "\x = a..x < k. e" for "setsum (%x. e) {..x < k. e" used to be based on a separate wenzelm@16234: function "Summation", which has been discontinued. wenzelm@16234: wenzelm@16234: * theory Finite_Set: in structured induction proofs, the insert case wenzelm@16234: is now 'case (insert x F)' instead of the old counterintuitive 'case wenzelm@16234: (insert F x)'. wenzelm@16234: wenzelm@16234: * The 'refute' command has been extended to support a much larger wenzelm@16234: fragment of HOL, including axiomatic type classes, constdefs and wenzelm@16234: typedefs, inductive datatypes and recursion. wenzelm@16234: webertj@17700: * New tactics 'sat' and 'satx' to prove propositional tautologies. webertj@17700: Requires zChaff with proof generation to be installed. See webertj@17700: HOL/ex/SAT_Examples.thy for examples. webertj@17619: wenzelm@16234: * Datatype induction via method 'induct' now preserves the name of the wenzelm@16234: induction variable. For example, when proving P(xs::'a list) by wenzelm@16234: induction on xs, the induction step is now P(xs) ==> P(a#xs) rather wenzelm@16234: than P(list) ==> P(a#list) as previously. Potential INCOMPATIBILITY wenzelm@16234: in unstructured proof scripts. wenzelm@16234: wenzelm@16234: * Reworked implementation of records. Improved scalability for wenzelm@16234: records with many fields, avoiding performance problems for type wenzelm@16234: inference. Records are no longer composed of nested field types, but wenzelm@16234: of nested extension types. Therefore the record type only grows linear wenzelm@16234: in the number of extensions and not in the number of fields. The wenzelm@16234: top-level (users) view on records is preserved. Potential wenzelm@16234: INCOMPATIBILITY only in strange cases, where the theory depends on the wenzelm@16234: old record representation. The type generated for a record is called wenzelm@16234: _ext_type. wenzelm@16234: wenzelm@16234: Flag record_quick_and_dirty_sensitive can be enabled to skip the wenzelm@16234: proofs triggered by a record definition or a simproc (if wenzelm@16234: quick_and_dirty is enabled). Definitions of large records can take wenzelm@16234: quite long. wenzelm@16234: wenzelm@16234: New simproc record_upd_simproc for simplification of multiple record wenzelm@16234: updates enabled by default. Moreover, trivial updates are also wenzelm@16234: removed: r(|x := x r|) = r. INCOMPATIBILITY: old proofs break wenzelm@16234: occasionally, since simplification is more powerful by default. wenzelm@16234: wenzelm@17275: * typedef: proper support for polymorphic sets, which contain extra wenzelm@17275: type-variables in the term. wenzelm@17275: wenzelm@16234: * Simplifier: automatically reasons about transitivity chains wenzelm@16234: involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics wenzelm@16234: provided by Provers/trancl.ML as additional solvers. INCOMPATIBILITY: wenzelm@16234: old proofs break occasionally as simplification may now solve more wenzelm@16234: goals than previously. wenzelm@16234: wenzelm@16234: * Simplifier: converts x <= y into x = y if assumption y <= x is wenzelm@16234: present. Works for all partial orders (class "order"), in particular wenzelm@16234: numbers and sets. For linear orders (e.g. numbers) it treats ~ x < y wenzelm@16234: just like y <= x. wenzelm@16234: wenzelm@16234: * Simplifier: new simproc for "let x = a in f x". If a is a free or wenzelm@16234: bound variable or a constant then the let is unfolded. Otherwise wenzelm@16234: first a is simplified to b, and then f b is simplified to g. If wenzelm@16234: possible we abstract b from g arriving at "let x = b in h x", wenzelm@16234: otherwise we unfold the let and arrive at g. The simproc can be wenzelm@16234: enabled/disabled by the reference use_let_simproc. Potential wenzelm@16234: INCOMPATIBILITY since simplification is more powerful by default. webertj@15776: paulson@16563: * Classical reasoning: the meson method now accepts theorems as arguments. paulson@16563: paulson@17595: * Prover support: pre-release of the Isabelle-ATP linkup, which runs background paulson@17595: jobs to provide advice on the provability of subgoals. paulson@17595: wenzelm@16891: * Theory OrderedGroup and Ring_and_Field: various additions and wenzelm@16891: improvements to faciliate calculations involving equalities and wenzelm@16891: inequalities. wenzelm@16891: wenzelm@16891: The following theorems have been eliminated or modified wenzelm@16891: (INCOMPATIBILITY): avigad@16888: avigad@16888: abs_eq now named abs_of_nonneg wenzelm@17371: abs_of_ge_0 now named abs_of_nonneg wenzelm@17371: abs_minus_eq now named abs_of_nonpos avigad@16888: imp_abs_id now named abs_of_nonneg avigad@16888: imp_abs_neg_id now named abs_of_nonpos avigad@16888: mult_pos now named mult_pos_pos avigad@16888: mult_pos_le now named mult_nonneg_nonneg avigad@16888: mult_pos_neg_le now named mult_nonneg_nonpos avigad@16888: mult_pos_neg2_le now named mult_nonneg_nonpos2 avigad@16888: mult_neg now named mult_neg_neg avigad@16888: mult_neg_le now named mult_nonpos_nonpos avigad@16888: obua@23495: * The following lemmas in Ring_and_Field have been added to the simplifier: obua@23495: obua@23495: zero_le_square obua@23495: not_square_less_zero obua@23495: obua@23495: The following lemmas have been deleted from Real/RealPow: obua@23495: obua@23495: realpow_zero_zero obua@23495: realpow_two obua@23495: realpow_less obua@23495: zero_le_power obua@23495: realpow_two_le obua@23495: abs_realpow_two obua@23495: realpow_two_abs obua@23495: wenzelm@16891: * Theory Parity: added rules for simplifying exponents. wenzelm@16891: nipkow@17092: * Theory List: nipkow@17092: nipkow@17092: The following theorems have been eliminated or modified nipkow@17092: (INCOMPATIBILITY): nipkow@17092: nipkow@17092: list_all_Nil now named list_all.simps(1) nipkow@17092: list_all_Cons now named list_all.simps(2) nipkow@17092: list_all_conv now named list_all_iff nipkow@17092: set_mem_eq now named mem_iff nipkow@17092: wenzelm@16929: * Theories SetsAndFunctions and BigO (see HOL/Library) support wenzelm@16929: asymptotic "big O" calculations. See the notes in BigO.thy. wenzelm@16929: avigad@16888: avigad@16888: *** HOL-Complex *** avigad@16888: wenzelm@16891: * Theory RealDef: better support for embedding natural numbers and wenzelm@16891: integers in the reals. wenzelm@16891: wenzelm@16891: The following theorems have been eliminated or modified wenzelm@16891: (INCOMPATIBILITY): wenzelm@16891: avigad@17016: exp_ge_add_one_self now requires no hypotheses avigad@17016: real_of_int_add reversed direction of equality (use [symmetric]) avigad@17016: real_of_int_minus reversed direction of equality (use [symmetric]) avigad@17016: real_of_int_diff reversed direction of equality (use [symmetric]) avigad@17016: real_of_int_mult reversed direction of equality (use [symmetric]) wenzelm@16891: wenzelm@16891: * Theory RComplete: expanded support for floor and ceiling functions. avigad@16888: avigad@16962: * Theory Ln is new, with properties of the natural logarithm avigad@16962: wenzelm@17423: * Hyperreal: There is a new type constructor "star" for making wenzelm@17423: nonstandard types. The old type names are now type synonyms: wenzelm@17423: wenzelm@17423: hypreal = real star wenzelm@17423: hypnat = nat star wenzelm@17423: hcomplex = complex star wenzelm@17423: wenzelm@17423: * Hyperreal: Many groups of similarly-defined constants have been huffman@17442: replaced by polymorphic versions (INCOMPATIBILITY): wenzelm@17423: wenzelm@17423: star_of <-- hypreal_of_real, hypnat_of_nat, hcomplex_of_complex wenzelm@17423: wenzelm@17423: starset <-- starsetNat, starsetC wenzelm@17423: *s* <-- *sNat*, *sc* wenzelm@17423: starset_n <-- starsetNat_n, starsetC_n wenzelm@17423: *sn* <-- *sNatn*, *scn* wenzelm@17423: InternalSets <-- InternalNatSets, InternalCSets wenzelm@17423: huffman@17442: starfun <-- starfun{Nat,Nat2,C,RC,CR} wenzelm@17423: *f* <-- *fNat*, *fNat2*, *fc*, *fRc*, *fcR* huffman@17442: starfun_n <-- starfun{Nat,Nat2,C,RC,CR}_n wenzelm@17423: *fn* <-- *fNatn*, *fNat2n*, *fcn*, *fRcn*, *fcRn* huffman@17442: InternalFuns <-- InternalNatFuns, InternalNatFuns2, Internal{C,RC,CR}Funs wenzelm@17423: wenzelm@17423: * Hyperreal: Many type-specific theorems have been removed in favor of huffman@17442: theorems specific to various axiomatic type classes (INCOMPATIBILITY): huffman@17442: huffman@17442: add_commute <-- {hypreal,hypnat,hcomplex}_add_commute huffman@17442: add_assoc <-- {hypreal,hypnat,hcomplex}_add_assocs huffman@17442: OrderedGroup.add_0 <-- {hypreal,hypnat,hcomplex}_add_zero_left huffman@17442: OrderedGroup.add_0_right <-- {hypreal,hcomplex}_add_zero_right wenzelm@17423: right_minus <-- hypreal_add_minus huffman@17442: left_minus <-- {hypreal,hcomplex}_add_minus_left huffman@17442: mult_commute <-- {hypreal,hypnat,hcomplex}_mult_commute huffman@17442: mult_assoc <-- {hypreal,hypnat,hcomplex}_mult_assoc huffman@17442: mult_1_left <-- {hypreal,hypnat}_mult_1, hcomplex_mult_one_left wenzelm@17423: mult_1_right <-- hcomplex_mult_one_right wenzelm@17423: mult_zero_left <-- hcomplex_mult_zero_left huffman@17442: left_distrib <-- {hypreal,hypnat,hcomplex}_add_mult_distrib wenzelm@17423: right_distrib <-- hypnat_add_mult_distrib2 huffman@17442: zero_neq_one <-- {hypreal,hypnat,hcomplex}_zero_not_eq_one wenzelm@17423: right_inverse <-- hypreal_mult_inverse wenzelm@17423: left_inverse <-- hypreal_mult_inverse_left, hcomplex_mult_inv_left huffman@17442: order_refl <-- {hypreal,hypnat}_le_refl huffman@17442: order_trans <-- {hypreal,hypnat}_le_trans huffman@17442: order_antisym <-- {hypreal,hypnat}_le_anti_sym huffman@17442: order_less_le <-- {hypreal,hypnat}_less_le huffman@17442: linorder_linear <-- {hypreal,hypnat}_le_linear huffman@17442: add_left_mono <-- {hypreal,hypnat}_add_left_mono huffman@17442: mult_strict_left_mono <-- {hypreal,hypnat}_mult_less_mono2 wenzelm@17423: add_nonneg_nonneg <-- hypreal_le_add_order wenzelm@17423: wenzelm@17423: * Hyperreal: Separate theorems having to do with type-specific wenzelm@17423: versions of constants have been merged into theorems that apply to the huffman@17442: new polymorphic constants (INCOMPATIBILITY): huffman@17442: huffman@17442: STAR_UNIV_set <-- {STAR_real,NatStar_real,STARC_complex}_set huffman@17442: STAR_empty_set <-- {STAR,NatStar,STARC}_empty_set huffman@17442: STAR_Un <-- {STAR,NatStar,STARC}_Un huffman@17442: STAR_Int <-- {STAR,NatStar,STARC}_Int huffman@17442: STAR_Compl <-- {STAR,NatStar,STARC}_Compl huffman@17442: STAR_subset <-- {STAR,NatStar,STARC}_subset huffman@17442: STAR_mem <-- {STAR,NatStar,STARC}_mem huffman@17442: STAR_mem_Compl <-- {STAR,STARC}_mem_Compl huffman@17442: STAR_diff <-- {STAR,STARC}_diff huffman@17442: STAR_star_of_image_subset <-- {STAR_hypreal_of_real, NatStar_hypreal_of_real, huffman@17442: STARC_hcomplex_of_complex}_image_subset huffman@17442: starset_n_Un <-- starset{Nat,C}_n_Un huffman@17442: starset_n_Int <-- starset{Nat,C}_n_Int huffman@17442: starset_n_Compl <-- starset{Nat,C}_n_Compl huffman@17442: starset_n_diff <-- starset{Nat,C}_n_diff huffman@17442: InternalSets_Un <-- Internal{Nat,C}Sets_Un huffman@17442: InternalSets_Int <-- Internal{Nat,C}Sets_Int huffman@17442: InternalSets_Compl <-- Internal{Nat,C}Sets_Compl huffman@17442: InternalSets_diff <-- Internal{Nat,C}Sets_diff huffman@17442: InternalSets_UNIV_diff <-- Internal{Nat,C}Sets_UNIV_diff huffman@17442: InternalSets_starset_n <-- Internal{Nat,C}Sets_starset{Nat,C}_n huffman@17442: starset_starset_n_eq <-- starset{Nat,C}_starset{Nat,C}_n_eq huffman@17442: starset_n_starset <-- starset{Nat,C}_n_starset{Nat,C} huffman@17442: starfun_n_starfun <-- starfun{Nat,Nat2,C,RC,CR}_n_starfun{Nat,Nat2,C,RC,CR} huffman@17442: starfun <-- starfun{Nat,Nat2,C,RC,CR} huffman@17442: starfun_mult <-- starfun{Nat,Nat2,C,RC,CR}_mult huffman@17442: starfun_add <-- starfun{Nat,Nat2,C,RC,CR}_add huffman@17442: starfun_minus <-- starfun{Nat,Nat2,C,RC,CR}_minus huffman@17442: starfun_diff <-- starfun{C,RC,CR}_diff huffman@17442: starfun_o <-- starfun{NatNat2,Nat2,_stafunNat,C,C_starfunRC,_starfunCR}_o huffman@17442: starfun_o2 <-- starfun{NatNat2,_stafunNat,C,C_starfunRC,_starfunCR}_o2 huffman@17442: starfun_const_fun <-- starfun{Nat,Nat2,C,RC,CR}_const_fun huffman@17442: starfun_inverse <-- starfun{Nat,C,RC,CR}_inverse huffman@17442: starfun_eq <-- starfun{Nat,Nat2,C,RC,CR}_eq huffman@17442: starfun_eq_iff <-- starfun{C,RC,CR}_eq_iff wenzelm@17423: starfun_Id <-- starfunC_Id huffman@17442: starfun_approx <-- starfun{Nat,CR}_approx huffman@17442: starfun_capprox <-- starfun{C,RC}_capprox wenzelm@17423: starfun_abs <-- starfunNat_rabs huffman@17442: starfun_lambda_cancel <-- starfun{C,CR,RC}_lambda_cancel huffman@17442: starfun_lambda_cancel2 <-- starfun{C,CR,RC}_lambda_cancel2 wenzelm@17423: starfun_mult_HFinite_approx <-- starfunCR_mult_HFinite_capprox huffman@17442: starfun_mult_CFinite_capprox <-- starfun{C,RC}_mult_CFinite_capprox huffman@17442: starfun_add_capprox <-- starfun{C,RC}_add_capprox wenzelm@17423: starfun_add_approx <-- starfunCR_add_approx wenzelm@17423: starfun_inverse_inverse <-- starfunC_inverse_inverse huffman@17442: starfun_divide <-- starfun{C,CR,RC}_divide huffman@17442: starfun_n <-- starfun{Nat,C}_n huffman@17442: starfun_n_mult <-- starfun{Nat,C}_n_mult huffman@17442: starfun_n_add <-- starfun{Nat,C}_n_add wenzelm@17423: starfun_n_add_minus <-- starfunNat_n_add_minus huffman@17442: starfun_n_const_fun <-- starfun{Nat,C}_n_const_fun huffman@17442: starfun_n_minus <-- starfun{Nat,C}_n_minus huffman@17442: starfun_n_eq <-- starfun{Nat,C}_n_eq huffman@17442: huffman@17442: star_n_add <-- {hypreal,hypnat,hcomplex}_add huffman@17442: star_n_minus <-- {hypreal,hcomplex}_minus huffman@17442: star_n_diff <-- {hypreal,hcomplex}_diff huffman@17442: star_n_mult <-- {hypreal,hcomplex}_mult huffman@17442: star_n_inverse <-- {hypreal,hcomplex}_inverse huffman@17442: star_n_le <-- {hypreal,hypnat}_le huffman@17442: star_n_less <-- {hypreal,hypnat}_less huffman@17442: star_n_zero_num <-- {hypreal,hypnat,hcomplex}_zero_num huffman@17442: star_n_one_num <-- {hypreal,hypnat,hcomplex}_one_num wenzelm@17423: star_n_abs <-- hypreal_hrabs wenzelm@17423: star_n_divide <-- hcomplex_divide wenzelm@17423: huffman@17442: star_of_add <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_add huffman@17442: star_of_minus <-- {hypreal_of_real,hcomplex_of_complex}_minus wenzelm@17423: star_of_diff <-- hypreal_of_real_diff huffman@17442: star_of_mult <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_mult huffman@17442: star_of_one <-- {hypreal_of_real,hcomplex_of_complex}_one huffman@17442: star_of_zero <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_zero huffman@17442: star_of_le <-- {hypreal_of_real,hypnat_of_nat}_le_iff huffman@17442: star_of_less <-- {hypreal_of_real,hypnat_of_nat}_less_iff huffman@17442: star_of_eq <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_eq_iff huffman@17442: star_of_inverse <-- {hypreal_of_real,hcomplex_of_complex}_inverse huffman@17442: star_of_divide <-- {hypreal_of_real,hcomplex_of_complex}_divide huffman@17442: star_of_of_nat <-- {hypreal_of_real,hcomplex_of_complex}_of_nat huffman@17442: star_of_of_int <-- {hypreal_of_real,hcomplex_of_complex}_of_int huffman@17442: star_of_number_of <-- {hypreal,hcomplex}_number_of wenzelm@17423: star_of_number_less <-- number_of_less_hypreal_of_real_iff wenzelm@17423: star_of_number_le <-- number_of_le_hypreal_of_real_iff wenzelm@17423: star_of_eq_number <-- hypreal_of_real_eq_number_of_iff wenzelm@17423: star_of_less_number <-- hypreal_of_real_less_number_of_iff wenzelm@17423: star_of_le_number <-- hypreal_of_real_le_number_of_iff wenzelm@17423: star_of_power <-- hypreal_of_real_power wenzelm@17423: star_of_eq_0 <-- hcomplex_of_complex_zero_iff wenzelm@17423: huffman@17442: * Hyperreal: new method "transfer" that implements the transfer huffman@17442: principle of nonstandard analysis. With a subgoal that mentions huffman@17442: nonstandard types like "'a star", the command "apply transfer" huffman@17442: replaces it with an equivalent one that mentions only standard types. huffman@17442: To be successful, all free variables must have standard types; non- huffman@17442: standard variables must have explicit universal quantifiers. huffman@17442: wenzelm@17641: * Hyperreal: A theory of Taylor series. wenzelm@17641: wenzelm@14655: wenzelm@14682: *** HOLCF *** wenzelm@14682: wenzelm@17533: * Discontinued special version of 'constdefs' (which used to support wenzelm@17533: continuous functions) in favor of the general Pure one with full wenzelm@17533: type-inference. wenzelm@17533: wenzelm@17533: * New simplification procedure for solving continuity conditions; it wenzelm@17533: is much faster on terms with many nested lambda abstractions (cubic huffman@17442: instead of exponential time). huffman@17442: wenzelm@17533: * New syntax for domain package: selector names are now optional. huffman@17442: Parentheses should be omitted unless argument is lazy, for example: huffman@17442: huffman@17442: domain 'a stream = cons "'a" (lazy "'a stream") huffman@17442: wenzelm@17533: * New command 'fixrec' for defining recursive functions with pattern wenzelm@17533: matching; defining multiple functions with mutual recursion is also wenzelm@17533: supported. Patterns may include the constants cpair, spair, up, sinl, wenzelm@17533: sinr, or any data constructor defined by the domain package. The given wenzelm@17533: equations are proven as rewrite rules. See HOLCF/ex/Fixrec_ex.thy for wenzelm@17533: syntax and examples. wenzelm@17533: wenzelm@17533: * New commands 'cpodef' and 'pcpodef' for defining predicate subtypes wenzelm@17533: of cpo and pcpo types. Syntax is exactly like the 'typedef' command, wenzelm@17533: but the proof obligation additionally includes an admissibility wenzelm@17533: requirement. The packages generate instances of class cpo or pcpo, wenzelm@17533: with continuity and strictness theorems for Rep and Abs. huffman@17442: huffman@17584: * HOLCF: Many theorems have been renamed according to a more standard naming huffman@17584: scheme (INCOMPATIBILITY): huffman@17584: huffman@17584: foo_inject: "foo$x = foo$y ==> x = y" huffman@17584: foo_eq: "(foo$x = foo$y) = (x = y)" huffman@17584: foo_less: "(foo$x << foo$y) = (x << y)" huffman@17584: foo_strict: "foo$UU = UU" huffman@17584: foo_defined: "... ==> foo$x ~= UU" huffman@17584: foo_defined_iff: "(foo$x = UU) = (x = UU)" huffman@17584: wenzelm@14682: paulson@14885: *** ZF *** paulson@14885: wenzelm@16234: * ZF/ex: theories Group and Ring provide examples in abstract algebra, wenzelm@16234: including the First Isomorphism Theorem (on quotienting by the kernel wenzelm@16234: of a homomorphism). wenzelm@15089: wenzelm@15089: * ZF/Simplifier: install second copy of type solver that actually wenzelm@16234: makes use of TC rules declared to Isar proof contexts (or locales); wenzelm@16234: the old version is still required for ML proof scripts. wenzelm@15703: wenzelm@15703: wenzelm@17445: *** Cube *** wenzelm@17445: wenzelm@17445: * Converted to Isar theory format; use locales instead of axiomatic wenzelm@17445: theories. wenzelm@17445: wenzelm@17445: wenzelm@15703: *** ML *** wenzelm@15703: haftmann@21339: * Pure/library.ML: added ##>, ##>>, #>> -- higher-order counterparts haftmann@21339: for ||>, ||>>, |>>, haftmann@21339: wenzelm@15973: * Pure/library.ML no longer defines its own option datatype, but uses wenzelm@16234: that of the SML basis, which has constructors NONE and SOME instead of wenzelm@16234: None and Some, as well as exception Option.Option instead of OPTION. wenzelm@16234: The functions the, if_none, is_some, is_none have been adapted wenzelm@16234: accordingly, while Option.map replaces apsome. wenzelm@15973: wenzelm@16860: * Pure/library.ML: the exception LIST has been given up in favour of wenzelm@16860: the standard exceptions Empty and Subscript, as well as wenzelm@16860: Library.UnequalLengths. Function like Library.hd and Library.tl are wenzelm@16860: superceded by the standard hd and tl functions etc. wenzelm@16860: wenzelm@16860: A number of basic list functions are no longer exported to the ML wenzelm@16860: toplevel, as they are variants of predefined functions. The following wenzelm@16234: suggests how one can translate existing code: wenzelm@15973: wenzelm@15973: rev_append xs ys = List.revAppend (xs, ys) wenzelm@15973: nth_elem (i, xs) = List.nth (xs, i) wenzelm@15973: last_elem xs = List.last xs wenzelm@15973: flat xss = List.concat xss wenzelm@16234: seq fs = List.app fs wenzelm@15973: partition P xs = List.partition P xs wenzelm@15973: mapfilter f xs = List.mapPartial f xs wenzelm@15973: wenzelm@16860: * Pure/library.ML: several combinators for linear functional wenzelm@16860: transformations, notably reverse application and composition: wenzelm@16860: wenzelm@17371: x |> f f #> g wenzelm@17371: (x, y) |-> f f #-> g wenzelm@16860: haftmann@17495: * Pure/library.ML: introduced/changed precedence of infix operators: haftmann@17495: haftmann@17495: infix 1 |> |-> ||> ||>> |>> |>>> #> #->; haftmann@17495: infix 2 ?; haftmann@17495: infix 3 o oo ooo oooo; haftmann@17495: infix 4 ~~ upto downto; haftmann@17495: haftmann@17495: Maybe INCOMPATIBILITY when any of those is used in conjunction with other haftmann@17495: infix operators. haftmann@17495: wenzelm@17408: * Pure/library.ML: natural list combinators fold, fold_rev, and haftmann@16869: fold_map support linear functional transformations and nesting. For wenzelm@16860: example: wenzelm@16860: wenzelm@16860: fold f [x1, ..., xN] y = wenzelm@16860: y |> f x1 |> ... |> f xN wenzelm@16860: wenzelm@16860: (fold o fold) f [xs1, ..., xsN] y = wenzelm@16860: y |> fold f xs1 |> ... |> fold f xsN wenzelm@16860: wenzelm@16860: fold f [x1, ..., xN] = wenzelm@16860: f x1 #> ... #> f xN wenzelm@16860: wenzelm@16860: (fold o fold) f [xs1, ..., xsN] = wenzelm@16860: fold f xs1 #> ... #> fold f xsN wenzelm@16860: wenzelm@17408: * Pure/library.ML: the following selectors on type 'a option are wenzelm@17408: available: wenzelm@17408: wenzelm@17408: the: 'a option -> 'a (*partial*) wenzelm@17408: these: 'a option -> 'a where 'a = 'b list haftmann@17402: the_default: 'a -> 'a option -> 'a haftmann@17402: the_list: 'a option -> 'a list haftmann@17402: wenzelm@17408: * Pure/General: structure AList (cf. Pure/General/alist.ML) provides wenzelm@17408: basic operations for association lists, following natural argument haftmann@17564: order; moreover the explicit equality predicate passed here avoids haftmann@17495: potentially expensive polymorphic runtime equality checks. haftmann@17495: The old functions may be expressed as follows: wenzelm@17408: wenzelm@17408: assoc = uncurry (AList.lookup (op =)) wenzelm@17408: assocs = these oo AList.lookup (op =) wenzelm@17408: overwrite = uncurry (AList.update (op =)) o swap wenzelm@17408: haftmann@17564: * Pure/General: structure AList (cf. Pure/General/alist.ML) provides haftmann@17564: haftmann@17564: val make: ('a -> 'b) -> 'a list -> ('a * 'b) list haftmann@17564: val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list haftmann@17564: haftmann@17564: replacing make_keylist and keyfilter (occassionally used) haftmann@17564: Naive rewrites: haftmann@17564: haftmann@17564: make_keylist = AList.make haftmann@17564: keyfilter = AList.find (op =) haftmann@17564: haftmann@17564: * eq_fst and eq_snd now take explicit equality parameter, thus haftmann@17564: avoiding eqtypes. Naive rewrites: haftmann@17564: haftmann@17564: eq_fst = eq_fst (op =) haftmann@17564: eq_snd = eq_snd (op =) haftmann@17564: haftmann@17564: * Removed deprecated apl and apr (rarely used). haftmann@17564: Naive rewrites: haftmann@17564: haftmann@17564: apl (n, op) =>>= curry op n haftmann@17564: apr (op, m) =>>= fn n => op (n, m) haftmann@17564: wenzelm@17408: * Pure/General: structure OrdList (cf. Pure/General/ord_list.ML) wenzelm@17408: provides a reasonably efficient light-weight implementation of sets as wenzelm@17408: lists. wenzelm@17408: wenzelm@17408: * Pure/General: generic tables (cf. Pure/General/table.ML) provide a wenzelm@17408: few new operations; existing lookup and update are now curried to wenzelm@17408: follow natural argument order (for use with fold etc.); wenzelm@17408: INCOMPATIBILITY, use (uncurry Symtab.lookup) etc. as last resort. wenzelm@17408: wenzelm@17408: * Pure/General: output via the Isabelle channels of wenzelm@17408: writeln/warning/error etc. is now passed through Output.output, with a wenzelm@17408: hook for arbitrary transformations depending on the print_mode wenzelm@17408: (cf. Output.add_mode -- the first active mode that provides a output wenzelm@17408: function wins). Already formatted output may be embedded into further wenzelm@17408: text via Output.raw; the result of Pretty.string_of/str_of and derived wenzelm@17408: functions (string_of_term/cterm/thm etc.) is already marked raw to wenzelm@17408: accommodate easy composition of diagnostic messages etc. Programmers wenzelm@17408: rarely need to care about Output.output or Output.raw at all, with wenzelm@17408: some notable exceptions: Output.output is required when bypassing the wenzelm@17408: standard channels (writeln etc.), or in token translations to produce wenzelm@17408: properly formatted results; Output.raw is required when capturing wenzelm@17408: already output material that will eventually be presented to the user wenzelm@17408: a second time. For the default print mode, both Output.output and wenzelm@17408: Output.raw have no effect. wenzelm@17408: wenzelm@17408: * Pure/General: Output.time_accumulator NAME creates an operator ('a wenzelm@17408: -> 'b) -> 'a -> 'b to measure runtime and count invocations; the wenzelm@17408: cumulative results are displayed at the end of a batch session. wenzelm@17408: wenzelm@17408: * Pure/General: File.sysify_path and File.quote_sysify path have been wenzelm@17408: replaced by File.platform_path and File.shell_path (with appropriate wenzelm@17408: hooks). This provides a clean interface for unusual systems where the wenzelm@17408: internal and external process view of file names are different. wenzelm@17408: wenzelm@16689: * Pure: more efficient orders for basic syntactic entities: added wenzelm@16689: fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord wenzelm@16689: and typ_ord to use fast_string_ord and fast_indexname_ord (term_ord is wenzelm@16689: NOT affected); structures Symtab, Vartab, Typtab, Termtab use the fast wenzelm@16689: orders now -- potential INCOMPATIBILITY for code that depends on a wenzelm@16689: particular order for Symtab.keys, Symtab.dest, etc. (consider using wenzelm@16689: Library.sort_strings on result). wenzelm@16689: wenzelm@17408: * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, wenzelm@17408: fold_types traverse types/terms from left to right, observing natural wenzelm@17408: argument order. Supercedes previous foldl_XXX versions, add_frees, wenzelm@17408: add_vars etc. have been adapted as well: INCOMPATIBILITY. wenzelm@17408: wenzelm@16151: * Pure: name spaces have been refined, with significant changes of the wenzelm@16234: internal interfaces -- INCOMPATIBILITY. Renamed cond_extern(_table) wenzelm@16234: to extern(_table). The plain name entry path is superceded by a wenzelm@16234: general 'naming' context, which also includes the 'policy' to produce wenzelm@16234: a fully qualified name and external accesses of a fully qualified wenzelm@16234: name; NameSpace.extend is superceded by context dependent wenzelm@16234: Sign.declare_name. Several theory and proof context operations modify wenzelm@16234: the naming context. Especially note Theory.restore_naming and wenzelm@16234: ProofContext.restore_naming to get back to a sane state; note that wenzelm@16234: Theory.add_path is no longer sufficient to recover from wenzelm@16234: Theory.absolute_path in particular. wenzelm@16234: wenzelm@16234: * Pure: new flags short_names (default false) and unique_names wenzelm@16234: (default true) for controlling output of qualified names. If wenzelm@16234: short_names is set, names are printed unqualified. If unique_names is wenzelm@16234: reset, the name prefix is reduced to the minimum required to achieve wenzelm@16234: the original result when interning again, even if there is an overlap wenzelm@16234: with earlier declarations. wenzelm@16151: wenzelm@16456: * Pure/TheoryDataFun: change of the argument structure; 'prep_ext' is wenzelm@16456: now 'extend', and 'merge' gets an additional Pretty.pp argument wenzelm@16456: (useful for printing error messages). INCOMPATIBILITY. wenzelm@16456: wenzelm@16456: * Pure: major reorganization of the theory context. Type Sign.sg and wenzelm@16456: Theory.theory are now identified, referring to the universal wenzelm@16456: Context.theory (see Pure/context.ML). Actual signature and theory wenzelm@16456: content is managed as theory data. The old code and interfaces were wenzelm@16456: spread over many files and structures; the new arrangement introduces wenzelm@16456: considerable INCOMPATIBILITY to gain more clarity: wenzelm@16456: wenzelm@16456: Context -- theory management operations (name, identity, inclusion, wenzelm@16456: parents, ancestors, merge, etc.), plus generic theory data; wenzelm@16456: wenzelm@16456: Sign -- logical signature and syntax operations (declaring consts, wenzelm@16456: types, etc.), plus certify/read for common entities; wenzelm@16456: wenzelm@16456: Theory -- logical theory operations (stating axioms, definitions, wenzelm@16456: oracles), plus a copy of logical signature operations (consts, wenzelm@16456: types, etc.); also a few basic management operations (Theory.copy, wenzelm@16456: Theory.merge, etc.) wenzelm@16456: wenzelm@16456: The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm wenzelm@16456: etc.) as well as the sign field in Thm.rep_thm etc. have been retained wenzelm@16456: for convenience -- they merely return the theory. wenzelm@16456: wenzelm@17193: * Pure: type Type.tsig is superceded by theory in most interfaces. wenzelm@17193: wenzelm@16547: * Pure: the Isar proof context type is already defined early in Pure wenzelm@16547: as Context.proof (note that ProofContext.context and Proof.context are wenzelm@16547: aliases, where the latter is the preferred name). This enables other wenzelm@16547: Isabelle components to refer to that type even before Isar is present. wenzelm@16547: wenzelm@16373: * Pure/sign/theory: discontinued named name spaces (i.e. classK, wenzelm@16373: typeK, constK, axiomK, oracleK), but provide explicit operations for wenzelm@16373: any of these kinds. For example, Sign.intern typeK is now wenzelm@16373: Sign.intern_type, Theory.hide_space Sign.typeK is now wenzelm@16373: Theory.hide_types. Also note that former wenzelm@16373: Theory.hide_classes/types/consts are now wenzelm@16373: Theory.hide_classes_i/types_i/consts_i, while the non '_i' versions wenzelm@16373: internalize their arguments! INCOMPATIBILITY. wenzelm@16373: wenzelm@16506: * Pure: get_thm interface (of PureThy and ProofContext) expects wenzelm@16506: datatype thmref (with constructors Name and NameSelection) instead of wenzelm@16506: plain string -- INCOMPATIBILITY; wenzelm@16506: wenzelm@16151: * Pure: cases produced by proof methods specify options, where NONE wenzelm@16234: means to remove case bindings -- INCOMPATIBILITY in wenzelm@16234: (RAW_)METHOD_CASES. wenzelm@16151: wenzelm@16373: * Pure: the following operations retrieve axioms or theorems from a wenzelm@16373: theory node or theory hierarchy, respectively: wenzelm@16373: wenzelm@16373: Theory.axioms_of: theory -> (string * term) list wenzelm@16373: Theory.all_axioms_of: theory -> (string * term) list wenzelm@16373: PureThy.thms_of: theory -> (string * thm) list wenzelm@16373: PureThy.all_thms_of: theory -> (string * thm) list wenzelm@16373: wenzelm@16718: * Pure: print_tac now outputs the goal through the trace channel. wenzelm@16718: wenzelm@17408: * Isar toplevel: improved diagnostics, mostly for Poly/ML only. wenzelm@17408: Reference Toplevel.debug (default false) controls detailed printing wenzelm@17408: and tracing of low-level exceptions; Toplevel.profiling (default 0) wenzelm@17408: controls execution profiling -- set to 1 for time and 2 for space wenzelm@17408: (both increase the runtime). wenzelm@17408: wenzelm@17408: * Isar session: The initial use of ROOT.ML is now always timed, wenzelm@17408: i.e. the log will show the actual process times, in contrast to the wenzelm@17408: elapsed wall-clock time that the outer shell wrapper produces. wenzelm@17408: wenzelm@17408: * Simplifier: improved handling of bound variables (nameless wenzelm@16997: representation, avoid allocating new strings). Simprocs that invoke wenzelm@16997: the Simplifier recursively should use Simplifier.inherit_bounds to wenzelm@17720: avoid local name clashes. Failure to do so produces warnings wenzelm@17720: "Simplifier: renamed bound variable ..."; set Simplifier.debug_bounds wenzelm@17720: for further details. wenzelm@16234: wenzelm@17166: * ML functions legacy_bindings and use_legacy_bindings produce ML fact wenzelm@17166: bindings for all theorems stored within a given theory; this may help wenzelm@17166: in porting non-Isar theories to Isar ones, while keeping ML proof wenzelm@17166: scripts for the time being. wenzelm@17166: wenzelm@17457: * ML operator HTML.with_charset specifies the charset begin used for wenzelm@17457: generated HTML files. For example: wenzelm@17457: wenzelm@17457: HTML.with_charset "utf-8" use_thy "Hebrew"; wenzelm@17538: HTML.with_charset "utf-8" use_thy "Chinese"; wenzelm@17457: wenzelm@16234: wenzelm@16234: *** System *** wenzelm@16234: wenzelm@16234: * Allow symlinks to all proper Isabelle executables (Isabelle, wenzelm@16234: isabelle, isatool etc.). wenzelm@16234: wenzelm@16234: * ISABELLE_DOC_FORMAT setting specifies preferred document format (for wenzelm@16234: isatool doc, isatool mkdir, display_drafts etc.). wenzelm@16234: wenzelm@16234: * isatool usedir: option -f allows specification of the ML file to be wenzelm@16234: used by Isabelle; default is ROOT.ML. wenzelm@16234: wenzelm@16251: * New isatool version outputs the version identifier of the Isabelle wenzelm@16251: distribution being used. wenzelm@16251: wenzelm@16251: * HOL: new isatool dimacs2hol converts files in DIMACS CNF format wenzelm@16234: (containing Boolean satisfiability problems) into Isabelle/HOL wenzelm@16234: theories. wenzelm@15703: wenzelm@15703: wenzelm@14655: wenzelm@14606: New in Isabelle2004 (April 2004) wenzelm@14606: -------------------------------- wenzelm@13280: skalberg@14171: *** General *** skalberg@14171: ballarin@14398: * Provers/order.ML: new efficient reasoner for partial and linear orders. ballarin@14398: Replaces linorder.ML. ballarin@14398: wenzelm@14606: * Pure: Greek letters (except small lambda, \), as well as Gothic wenzelm@14606: (\...\\...\), calligraphic (\...\), and Euler skalberg@14173: (\...\), are now considered normal letters, and can therefore skalberg@14173: be used anywhere where an ASCII letter (a...zA...Z) has until skalberg@14173: now. COMPATIBILITY: This obviously changes the parsing of some skalberg@14173: terms, especially where a symbol has been used as a binder, say skalberg@14173: '\x. ...', which is now a type error since \x will be parsed skalberg@14173: as an identifier. Fix it by inserting a space around former skalberg@14173: symbols. Call 'isatool fixgreek' to try to fix parsing errors in skalberg@14173: existing theory and ML files. skalberg@14171: paulson@14237: * Pure: Macintosh and Windows line-breaks are now allowed in theory files. paulson@14237: wenzelm@14731: * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now wenzelm@14731: allowed in identifiers. Similar to Greek letters \<^isub> is now considered wenzelm@14731: a normal (but invisible) letter. For multiple letter subscripts repeat wenzelm@14731: \<^isub> like this: x\<^isub>1\<^isub>2. kleing@14233: kleing@14333: * Pure: There are now sub-/superscripts that can span more than one kleing@14333: character. Text between \<^bsub> and \<^esub> is set in subscript in wenzelm@14606: ProofGeneral and LaTeX, text between \<^bsup> and \<^esup> in wenzelm@14606: superscript. The new control characters are not identifier parts. kleing@14333: schirmer@14561: * Pure: Control-symbols of the form \<^raw:...> will literally print the wenzelm@14606: content of "..." to the latex file instead of \isacntrl... . The "..." wenzelm@14606: may consist of any printable characters excluding the end bracket >. schirmer@14361: paulson@14237: * Pure: Using new Isar command "finalconsts" (or the ML functions paulson@14237: Theory.add_finals or Theory.add_finals_i) it is now possible to paulson@14237: declare constants "final", which prevents their being given a definition paulson@14237: later. It is useful for constants whose behaviour is fixed axiomatically skalberg@14224: rather than definitionally, such as the meta-logic connectives. skalberg@14224: wenzelm@14606: * Pure: 'instance' now handles general arities with general sorts wenzelm@14606: (i.e. intersections of classes), skalberg@14503: kleing@14547: * Presentation: generated HTML now uses a CSS style sheet to make layout wenzelm@14731: (somewhat) independent of content. It is copied from lib/html/isabelle.css. kleing@14547: It can be changed to alter the colors/layout of generated pages. kleing@14547: wenzelm@14556: ballarin@14175: *** Isar *** ballarin@14175: ballarin@14508: * Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac, ballarin@14508: cut_tac, subgoal_tac and thin_tac: ballarin@14175: - Now understand static (Isar) contexts. As a consequence, users of Isar ballarin@14175: locales are no longer forced to write Isar proof scripts. ballarin@14175: For details see Isar Reference Manual, paragraph 4.3.2: Further tactic ballarin@14175: emulations. ballarin@14175: - INCOMPATIBILITY: names of variables to be instantiated may no ballarin@14211: longer be enclosed in quotes. Instead, precede variable name with `?'. ballarin@14211: This is consistent with the instantiation attribute "where". ballarin@14211: ballarin@14257: * Attributes "where" and "of": ballarin@14285: - Now take type variables of instantiated theorem into account when reading ballarin@14285: the instantiation string. This fixes a bug that caused instantiated ballarin@14285: theorems to have too special types in some circumstances. ballarin@14285: - "where" permits explicit instantiations of type variables. ballarin@14257: wenzelm@14556: * Calculation commands "moreover" and "also" no longer interfere with wenzelm@14556: current facts ("this"), admitting arbitrary combinations with "then" wenzelm@14556: and derived forms. kleing@14283: ballarin@14211: * Locales: ballarin@14211: - Goal statements involving the context element "includes" no longer ballarin@14211: generate theorems with internal delta predicates (those ending on ballarin@14211: "_axioms") in the premise. ballarin@14211: Resolve particular premise with .intro to obtain old form. ballarin@14211: - Fixed bug in type inference ("unify_frozen") that prevented mix of target ballarin@14211: specification and "includes" elements in goal statement. ballarin@14254: - Rule sets .intro and .axioms no longer declared as ballarin@14254: [intro?] and [elim?] (respectively) by default. ballarin@14508: - Experimental command for instantiation of locales in proof contexts: ballarin@14551: instantiate