wenzelm@5363: Isabelle NEWS -- history user-relevant changes wenzelm@5363: ============================================== wenzelm@2553: wenzelm@17754: New in this Isabelle release wenzelm@17754: ---------------------------- wenzelm@17754: wenzelm@17754: *** General *** wenzelm@17754: 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@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@17754: * Command 'find_theorems': support "*" wildcard in "name:" criterion. wenzelm@17754: wenzelm@17754: wenzelm@17865: *** Document preparation *** wenzelm@17865: 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@17865: wenzelm@17779: *** Pure *** wenzelm@17779: 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@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@18540: meta-level equations. Thus many occurrences of the 'unfold' method or wenzelm@18540: 'unfolded' attribute may be replaced by first-class proof text. wenzelm@18540: wenzelm@18233: * Provers/induct: improved internal context management to support wenzelm@18233: local fixes and defines on-the-fly. Thus explicit meta-level wenzelm@18233: connectives !! and ==> are rarely required anymore in inductive goals wenzelm@18233: (using object-logic connectives for this purpose has been long wenzelm@18233: obsolete anyway). The subsequent proof patterns illustrate advanced wenzelm@18233: techniques of natural induction; general datatypes and inductive sets wenzelm@18267: work analogously (see also src/HOL/Lambda for realistic examples). wenzelm@18267: wenzelm@18267: (1) This is how to ``strengthen'' an inductive goal wrt. certain wenzelm@18239: parameters: wenzelm@18233: wenzelm@18233: lemma wenzelm@18233: fixes n :: nat and x :: 'a wenzelm@18233: assumes a: "A n x" wenzelm@18233: shows "P n x" wenzelm@18233: using a -- {* make induct insert fact a *} wenzelm@18233: proof (induct n fixing: x) -- {* generalize goal to "!!x. A n x ==> P n x" *} wenzelm@18248: case 0 wenzelm@18233: show ?case sorry wenzelm@18233: next wenzelm@18248: case (Suc n) wenzelm@18239: note `!!x. A n x ==> P n x` -- {* induction hypothesis, according to induction rule *} wenzelm@18239: note `A (Suc n) x` -- {* induction premise, stemming from fact a *} wenzelm@18233: show ?case sorry wenzelm@18233: qed wenzelm@18233: wenzelm@18267: (2) This is how to perform induction over ``expressions of a certain wenzelm@18233: form'', using a locally defined inductive parameter n == "a x" wenzelm@18239: together with strengthening (the latter is usually required to get wenzelm@18267: sufficiently flexible induction hypotheses): wenzelm@18233: wenzelm@18233: lemma wenzelm@18233: fixes a :: "'a => nat" wenzelm@18233: assumes a: "A (a x)" wenzelm@18233: shows "P (a x)" wenzelm@18233: using a wenzelm@18233: proof (induct n == "a x" fixing: x) wenzelm@18233: ... wenzelm@18233: wenzelm@18267: See also HOL/Isar_examples/Puzzle.thy for an application of the this wenzelm@18267: particular technique. wenzelm@18267: wenzelm@18267: (3) This is how to perform existential reasoning ('obtain') by wenzelm@18267: induction, while avoiding explicit object-logic encodings: wenzelm@18267: wenzelm@18267: fix n :: nat wenzelm@18267: obtain x :: 'a where "P n x" and "Q n x" wenzelm@18267: proof (induct n fixing: thesis) wenzelm@18267: case 0 wenzelm@18267: obtain x where "P 0 x" and "Q 0 x" sorry wenzelm@18399: then show thesis by (rule 0) wenzelm@18267: next wenzelm@18267: case (Suc n) wenzelm@18267: obtain x where "P n x" and "Q n x" by (rule Suc.hyps) wenzelm@18267: obtain x where "P (Suc n) x" and "Q (Suc n) x" sorry wenzelm@18267: then show thesis by (rule Suc.prems) wenzelm@18267: qed wenzelm@18267: wenzelm@18267: Here the 'fixing: thesis' specification essentially modifies the scope wenzelm@18267: of the formal thesis parameter, in order to the get the whole wenzelm@18267: existence statement through the induction as expected. wenzelm@18233: wenzelm@18506: * Provers/induct: mutual induction rules are now specified as a list wenzelm@18506: of rule sharing the same induction cases. HOL packages usually wenzelm@18506: provide foo_bar.inducts for mutually defined items foo and bar wenzelm@18506: (e.g. inductive sets or datatypes). INCOMPATIBILITY, users need to wenzelm@18506: specify mutual induction rules differently, i.e. like this: wenzelm@18506: wenzelm@18506: (induct rule: foo_bar.inducts) wenzelm@18506: (induct set: 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@18506: * Provers/induct: improved handling of simultaneous goals. Instead of wenzelm@18506: introducing object-level conjunction, the statement is now split into wenzelm@18506: several conclusions, while the corresponding symbolic cases are wenzelm@18601: nested accordingly. INCOMPATIBILITY, proofs need to be structured wenzelm@18601: explicitly. For example: wenzelm@18480: wenzelm@18480: lemma wenzelm@18480: fixes n :: nat wenzelm@18480: shows "P n" and "Q n" wenzelm@18480: proof (induct n) wenzelm@18601: case 0 case 1 wenzelm@18480: show "P 0" sorry wenzelm@18480: next wenzelm@18601: case 0 case 2 wenzelm@18480: show "Q 0" sorry wenzelm@18480: next wenzelm@18601: case (Suc n) case 1 wenzelm@18480: note `P n` and `Q n` wenzelm@18480: show "P (Suc n)" sorry wenzelm@18480: next wenzelm@18601: case (Suc n) case 2 wenzelm@18480: note `P n` and `Q n` wenzelm@18480: show "Q (Suc n)" sorry wenzelm@18480: qed wenzelm@18480: wenzelm@18601: The split into subcases may be deferred as follows -- this is wenzelm@18601: particularly relevant for goal statements with local premises. wenzelm@18601: wenzelm@18601: lemma wenzelm@18601: fixes n :: nat wenzelm@18601: shows "A n ==> P n" and "B n ==> Q n" wenzelm@18601: proof (induct n) wenzelm@18601: case 0 wenzelm@18601: { wenzelm@18601: case 1 wenzelm@18601: note `A 0` wenzelm@18601: show "P 0" sorry wenzelm@18601: next wenzelm@18601: case 2 wenzelm@18601: note `B 0` wenzelm@18601: show "Q 0" sorry wenzelm@18601: } wenzelm@18601: next wenzelm@18601: case (Suc n) wenzelm@18601: note `A n ==> P n` and `B n ==> Q n` wenzelm@18601: { wenzelm@18601: case 1 wenzelm@18601: note `A (Suc n)` wenzelm@18601: show "P (Suc n)" sorry wenzelm@18601: next wenzelm@18601: case 2 wenzelm@18601: note `B (Suc n)` wenzelm@18601: show "Q (Suc n)" sorry wenzelm@18601: } wenzelm@18601: qed wenzelm@18601: wenzelm@18506: If simultaneous goals are to be used with mutual rules, the statement wenzelm@18506: needs to be structured carefully as a two-level conjunction, using wenzelm@18506: lists of propositions separated by 'and': wenzelm@18506: wenzelm@18507: lemma wenzelm@18507: shows "a : A ==> P1 a" wenzelm@18507: "a : A ==> P2 a" wenzelm@18507: and "b : B ==> Q1 b" wenzelm@18507: "b : B ==> Q2 b" wenzelm@18507: "b : B ==> Q3 b" wenzelm@18507: proof (induct set: A B) wenzelm@18480: wenzelm@18399: * Provers/induct: support coinduction as well. See wenzelm@18399: src/HOL/Library/Coinductive_List.thy for various examples. wenzelm@18399: nipkow@18674: * Simplifier: by default the simplifier trace only shows top level rewrites nipkow@18674: now. That is, trace_simp_depth_limit is set to 1 by default. Thus there is nipkow@18674: less danger of being flooded by the trace. The trace indicates where parts nipkow@18674: 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@17865: nipkow@17806: *** HOL *** nipkow@17806: wenzelm@18694: * Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the wenzelm@18694: 'rule' method. wenzelm@18694: wenzelm@17996: * Alternative iff syntax "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: nipkow@18674: * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only). nipkow@18674: wenzelm@17865: * In the context of the assumption "~(s = t)" the Simplifier rewrites wenzelm@17865: "t = s" to False (by simproc "neq_simproc"). For backward wenzelm@17865: compatibility this can be disabled by ML "reset use_neq_simproc". wenzelm@17779: webertj@17809: * Tactics 'sat' and 'satx' reimplemented, several improvements: goals webertj@17809: no longer need to be stated as " ==> False", equivalences (i.e. wenzelm@17865: "=" on type bool) are handled, variable names of the form "lit_" wenzelm@17865: are no longer reserved, significant speedup. wenzelm@17865: wenzelm@18480: * inductive and datatype: provide projections of mutual rules, bundled wenzelm@18480: as foo_bar.inducts; wenzelm@18480: wenzelm@18446: * Library: added theory Coinductive_List of potentially infinite lists wenzelm@18446: as greatest fixed-point. wenzelm@18399: webertj@17809: wenzelm@17878: *** ML *** wenzelm@17878: haftmann@18450: * Pure/library: haftmann@18450: haftmann@18450: val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list haftmann@18549: val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd haftmann@18450: wenzelm@18540: The semantics of "burrow" is: "take a function with *simulatanously* wenzelm@18540: transforms a list of value, and apply it *simulatanously* to a list of wenzelm@18540: list of values of the appropriate type". Confer this with "map" which wenzelm@18540: would *not* apply its argument function simulatanously but in haftmann@18549: sequence. "fold_burrow" has an additional context. wenzelm@18540: wenzelm@18540: Both actually avoid the usage of "unflat" since they hide away wenzelm@18540: "unflat" from the user. haftmann@18450: wenzelm@18446: * Pure/library: functions map2 and fold2 with curried syntax for wenzelm@18446: simultanous mapping and folding: wenzelm@18446: haftmann@18422: val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list haftmann@18422: val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c haftmann@18422: wenzelm@18446: * Pure/library: indexed lists - some functions in the Isabelle library wenzelm@18446: treating lists over 'a as finite mappings from [0...n] to 'a have been wenzelm@18446: given more convenient names and signatures reminiscent of similar wenzelm@18446: functions for alists, tables, etc: haftmann@18051: haftmann@18051: val nth: 'a list -> int -> 'a haftmann@18051: val nth_update: int * 'a -> 'a list -> 'a list haftmann@18051: val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list haftmann@18051: val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b haftmann@18051: wenzelm@18446: Note that fold_index starts counting at index 0, not 1 like foldln wenzelm@18446: used to. wenzelm@18446: wenzelm@18446: * Pure/General: name_mangler.ML provides a functor for generic name wenzelm@18446: mangling (bijective mapping from any expression values to strings). wenzelm@18446: wenzelm@18446: * Pure/General: rat.ML implements rational numbers. wenzelm@18446: 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@18642: * Pure: type Context.generic attribute is now the preferred wenzelm@18642: representation for global vs. local attributes while avoiding code wenzelm@18642: duplication; Attrib.theory/context/generic converts between different wenzelm@18642: types of attributes. Various Pure/HOL/ZF packages work with generic wenzelm@18642: attributes now, INCOMPATIBILITY. 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@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@18567: * Pure: structure Goal provides simple interfaces for wenzelm@17981: init/conclude/finish and tactical prove operations (replacing former wenzelm@17981: Tactic.prove). Note that OldGoals.prove_goalw_cterm has long been wenzelm@17981: obsolete, it is ill-behaved in a local proof context (e.g. with local wenzelm@17981: fixes/assumes or in a locale context). wenzelm@17981: wenzelm@18686: * ML/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@18722: * ML/Isar: theory setup now has type (theory -> theory), instead of a wenzelm@18722: list. INCOMPATIBILITY, may use #> to compose setup functions. wenzelm@18722: wenzelm@18590: * Pure/Isar: Toplevel.theory_to_proof admits transactions that modify wenzelm@18590: the theory before entering a proof state. Transactions now always see wenzelm@18590: a quasi-functional intermediate checkpoint, both in interactive and wenzelm@18590: batch mode. wenzelm@18567: 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@17754: 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: 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: 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