author | wenzelm |

Thu Apr 02 13:41:02 2009 +0200 (2009-04-02) | |

changeset 30845 | 9a887484de53 |

parent 30828 | 50c8f55cde7f |

child 30846 | fd8ed5a39a8e |

misc cleanup and rearrangements for Isabelle2009 release;

1.1 --- a/NEWS Tue Mar 31 22:25:46 2009 +0200 1.2 +++ b/NEWS Thu Apr 02 13:41:02 2009 +0200 1.3 @@ -1,15 +1,11 @@ 1.4 Isabelle NEWS -- history user-relevant changes 1.5 ============================================== 1.6 1.7 -New in this Isabelle version 1.8 ----------------------------- 1.9 +New in Isabelle2009 (April 2009) 1.10 +-------------------------------- 1.11 1.12 *** General *** 1.13 1.14 -* The main reference manuals (isar-ref, implementation, system) have 1.15 -been updated and extended. Formally checked references as hyperlinks 1.16 -are now available in uniform manner. 1.17 - 1.18 * Simplified main Isabelle executables, with less surprises on 1.19 case-insensitive file-systems (such as Mac OS). 1.20 1.21 @@ -37,110 +33,31 @@ 1.22 install -p ...", or use symlinks. 1.23 1.24 * The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the 1.25 -old ~/isabelle, which was slightly non-standard and apt cause 1.26 -surprises on case-insensitive file-systems. 1.27 +old ~/isabelle, which was slightly non-standard and apt to cause 1.28 +surprises on case-insensitive file-systems (such as Mac OS). 1.29 1.30 INCOMPATIBILITY, need to move existing ~/isabelle/etc, 1.31 ~/isabelle/heaps, ~/isabelle/browser_info to the new place. Special 1.32 care is required when using older releases of Isabelle. Note that 1.33 ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any 1.34 -Isabelle distribution. 1.35 +Isabelle distribution, in order to use the new ~/.isabelle uniformly. 1.36 1.37 * Proofs of fully specified statements are run in parallel on 1.38 -multi-core systems. A speedup factor of 2-3 can be expected on a 1.39 -regular 4-core machine, if the initial heap space is made reasonably 1.40 -large (cf. Poly/ML option -H). [Poly/ML 5.2.1 or later] 1.41 - 1.42 -* Generalized Isar history, with support for linear undo, direct state 1.43 -addressing etc. 1.44 - 1.45 -* Recovered hiding of consts, which was accidentally broken in 1.46 -Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really 1.47 -makes c inaccessible; consider using ``hide (open) const c'' instead. 1.48 - 1.49 -* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML 1.50 -interface instead. 1.51 - 1.52 -* There is a new syntactic category "float_const" for signed decimal 1.53 -fractions (e.g. 123.45 or -123.45). 1.54 - 1.55 -* New prover for coherent logic (see src/Tools/coherent.ML). 1.56 +multi-core systems. A speedup factor of 2.5 to 3.2 can be expected on 1.57 +a regular 4-core machine, if the initial heap space is made reasonably 1.58 +large (cf. Poly/ML option -H). (Requires Poly/ML 5.2.1 or later.) 1.59 + 1.60 +* The main reference manuals ("isar-ref", "implementation", and 1.61 +"system") have been updated and extended. Formally checked references 1.62 +as hyperlinks are now available uniformly. 1.63 + 1.64 1.65 1.66 *** Pure *** 1.67 1.68 -* Class declaration: sc. "base sort" must not be given in import list 1.69 -any longer but is inferred from the specification. Particularly in HOL, 1.70 -write 1.71 - 1.72 - class foo = ... instead of class foo = type + ... 1.73 - 1.74 -* Module moves in repository: 1.75 - src/Pure/Tools/value.ML ~> src/Tools/ 1.76 - src/Pure/Tools/quickcheck.ML ~> src/Tools/ 1.77 - 1.78 -* Slightly more coherent Pure syntax, with updated documentation in 1.79 -isar-ref manual. Removed locales meta_term_syntax and 1.80 -meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent, 1.81 -INCOMPATIBILITY in rare situations. 1.82 - 1.83 -* Goal-directed proof now enforces strict proof irrelevance wrt. sort 1.84 -hypotheses. Sorts required in the course of reasoning need to be 1.85 -covered by the constraints in the initial statement, completed by the 1.86 -type instance information of the background theory. Non-trivial sort 1.87 -hypotheses, which rarely occur in practice, may be specified via 1.88 -vacuous propositions of the form SORT_CONSTRAINT('a::c). For example: 1.89 - 1.90 - lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ... 1.91 - 1.92 -The result contains an implicit sort hypotheses as before -- 1.93 -SORT_CONSTRAINT premises are eliminated as part of the canonical rule 1.94 -normalization. 1.95 - 1.96 -* Changed defaults for unify configuration options: 1.97 - 1.98 - unify_trace_bound = 50 (formerly 25) 1.99 - unify_search_bound = 60 (formerly 30) 1.100 - 1.101 -* Different bookkeeping for code equations (INCOMPATIBILITY): 1.102 - 1.103 - a) On theory merge, the last set of code equations for a particular 1.104 - constant is taken (in accordance with the policy applied by other 1.105 - parts of the code generator framework). 1.106 - 1.107 - b) Code equations stemming from explicit declarations (e.g. code 1.108 - attribute) gain priority over default code equations stemming 1.109 - from definition, primrec, fun etc. 1.110 - 1.111 -* Global versions of theorems stemming from classes do not carry a 1.112 -parameter prefix any longer. INCOMPATIBILITY. 1.113 - 1.114 -* Dropped locale element "includes". This is a major INCOMPATIBILITY. 1.115 -In existing theorem specifications replace the includes element by the 1.116 -respective context elements of the included locale, omitting those 1.117 -that are already present in the theorem specification. Multiple 1.118 -assume elements of a locale should be replaced by a single one 1.119 -involving the locale predicate. In the proof body, declarations (most 1.120 -notably theorems) may be regained by interpreting the respective 1.121 -locales in the proof context as required (command "interpret"). 1.122 - 1.123 -If using "includes" in replacement of a target solely because the 1.124 -parameter types in the theorem are not as general as in the target, 1.125 -consider declaring a new locale with additional type constraints on 1.126 -the parameters (context element "constrains"). 1.127 - 1.128 -* Dropped "locale (open)". INCOMPATIBILITY. 1.129 - 1.130 -* Interpretation commands no longer attempt to simplify goal. 1.131 -INCOMPATIBILITY: in rare situations the generated goal differs. Use 1.132 -methods intro_locales and unfold_locales to clarify. 1.133 - 1.134 -* Interpretation commands no longer accept interpretation attributes. 1.135 -INCOMPATBILITY. 1.136 - 1.137 -* Complete re-implementation of locales. INCOMPATIBILITY. The most 1.138 -important changes are listed below. See the Tutorial on Locales for 1.139 -details. 1.140 +* Complete re-implementation of locales. INCOMPATIBILITY in several 1.141 +respects. The most important changes are listed below. See the 1.142 +Tutorial on Locales ("locales" manual) for details. 1.143 1.144 - In locale expressions, instantiation replaces renaming. Parameters 1.145 must be declared in a for clause. To aid compatibility with previous 1.146 @@ -158,35 +75,116 @@ 1.147 optional (syntax "name?:"). The default depends for plain "name:" 1.148 depends on the situation where a locale expression is used: in 1.149 commands 'locale' and 'sublocale' prefixes are optional, in 1.150 -'interpretation' and 'interpret' prefixes are mandatory. Old-style 1.151 +'interpretation' and 'interpret' prefixes are mandatory. The old 1.152 implicit qualifiers derived from the parameter names of a locale are 1.153 no longer generated. 1.154 1.155 -- "sublocale l < e" replaces "interpretation l < e". The 1.156 +- Command "sublocale l < e" replaces "interpretation l < e". The 1.157 instantiation clause in "interpretation" and "interpret" (square 1.158 brackets) is no longer available. Use locale expressions. 1.159 1.160 -- When converting proof scripts, be sure to mandatory qualifiers in 1.161 +- When converting proof scripts, mandatory qualifiers in 1.162 'interpretation' and 'interpret' should be retained by default, even 1.163 -if this is an INCOMPATIBILITY compared to former behaviour. 1.164 -Qualifiers in locale expressions range over a single locale instance 1.165 -only. 1.166 - 1.167 -* Command 'instance': attached definitions no longer accepted. 1.168 -INCOMPATIBILITY, use proper 'instantiation' target. 1.169 - 1.170 -* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. 1.171 +if this is an INCOMPATIBILITY compared to former behavior. In the 1.172 +worst case, use the "name?:" form for non-mandatory ones. Qualifiers 1.173 +in locale expressions range over a single locale instance only. 1.174 + 1.175 +- Dropped locale element "includes". This is a major INCOMPATIBILITY. 1.176 +In existing theorem specifications replace the includes element by the 1.177 +respective context elements of the included locale, omitting those 1.178 +that are already present in the theorem specification. Multiple 1.179 +assume elements of a locale should be replaced by a single one 1.180 +involving the locale predicate. In the proof body, declarations (most 1.181 +notably theorems) may be regained by interpreting the respective 1.182 +locales in the proof context as required (command "interpret"). 1.183 + 1.184 +If using "includes" in replacement of a target solely because the 1.185 +parameter types in the theorem are not as general as in the target, 1.186 +consider declaring a new locale with additional type constraints on 1.187 +the parameters (context element "constrains"). 1.188 + 1.189 +- Discontinued "locale (open)". INCOMPATIBILITY. 1.190 + 1.191 +- Locale interpretation commands no longer attempt to simplify goal. 1.192 +INCOMPATIBILITY: in rare situations the generated goal differs. Use 1.193 +methods intro_locales and unfold_locales to clarify. 1.194 + 1.195 +- Locale interpretation commands no longer accept interpretation 1.196 +attributes. INCOMPATIBILITY. 1.197 + 1.198 +* Class declaration: so-called "base sort" must not be given in import 1.199 +list any longer, but is inferred from the specification. Particularly 1.200 +in HOL, write 1.201 + 1.202 + class foo = ... 1.203 + 1.204 +instead of 1.205 + 1.206 + class foo = type + ... 1.207 + 1.208 +* Class target: global versions of theorems stemming do not carry a 1.209 +parameter prefix any longer. INCOMPATIBILITY. 1.210 + 1.211 +* Class 'instance' command no longer accepts attached definitions. 1.212 +INCOMPATIBILITY, use proper 'instantiation' target instead. 1.213 + 1.214 +* Recovered hiding of consts, which was accidentally broken in 1.215 +Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really 1.216 +makes c inaccessible; consider using ``hide (open) const c'' instead. 1.217 + 1.218 +* Slightly more coherent Pure syntax, with updated documentation in 1.219 +isar-ref manual. Removed locales meta_term_syntax and 1.220 +meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent, 1.221 +INCOMPATIBILITY in rare situations. Note that &&& should not be used 1.222 +directly in regular applications. 1.223 + 1.224 +* There is a new syntactic category "float_const" for signed decimal 1.225 +fractions (e.g. 123.45 or -123.45). 1.226 + 1.227 +* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML 1.228 +interface with 'setup' command instead. 1.229 + 1.230 +* Command 'local_setup' is similar to 'setup', but operates on a local 1.231 +theory context. 1.232 1.233 * The 'axiomatization' command now only works within a global theory 1.234 context. INCOMPATIBILITY. 1.235 1.236 -* New 'find_theorems' criterion "solves" matching theorems that 1.237 -directly solve the current goal. 1.238 - 1.239 -* Auto solve feature for main theorem statements (cf. option in Proof 1.240 -General Isabelle settings menu, disabled by default). Whenever a new 1.241 -goal is stated, "find_theorems solves" is called; any theorems that 1.242 -could solve the lemma directly are listed as part of the goal state. 1.243 +* Goal-directed proof now enforces strict proof irrelevance wrt. sort 1.244 +hypotheses. Sorts required in the course of reasoning need to be 1.245 +covered by the constraints in the initial statement, completed by the 1.246 +type instance information of the background theory. Non-trivial sort 1.247 +hypotheses, which rarely occur in practice, may be specified via 1.248 +vacuous propositions of the form SORT_CONSTRAINT('a::c). For example: 1.249 + 1.250 + lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ... 1.251 + 1.252 +The result contains an implicit sort hypotheses as before -- 1.253 +SORT_CONSTRAINT premises are eliminated as part of the canonical rule 1.254 +normalization. 1.255 + 1.256 +* Generalized Isar history, with support for linear undo, direct state 1.257 +addressing etc. 1.258 + 1.259 +* Changed defaults for unify configuration options: 1.260 + 1.261 + unify_trace_bound = 50 (formerly 25) 1.262 + unify_search_bound = 60 (formerly 30) 1.263 + 1.264 +* Different bookkeeping for code equations (INCOMPATIBILITY): 1.265 + 1.266 + a) On theory merge, the last set of code equations for a particular 1.267 + constant is taken (in accordance with the policy applied by other 1.268 + parts of the code generator framework). 1.269 + 1.270 + b) Code equations stemming from explicit declarations (e.g. code 1.271 + attribute) gain priority over default code equations stemming 1.272 + from definition, primrec, fun etc. 1.273 + 1.274 +* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. 1.275 + 1.276 +* Unified theorem tables for both code code generators. Thus [code 1.277 +func] has disappeared and only [code] remains. INCOMPATIBILITY. 1.278 1.279 * Command 'find_consts' searches for constants based on type and name 1.280 patterns, e.g. 1.281 @@ -200,8 +198,15 @@ 1.282 1.283 find_consts strict: "_ => bool" name: "Int" -"int => int" 1.284 1.285 -* Command 'local_setup' is similar to 'setup', but operates on a local 1.286 -theory context. 1.287 +* New 'find_theorems' criterion "solves" matches theorems that 1.288 +directly solve the current goal (modulo higher-order unification). 1.289 + 1.290 +* Auto solve feature for main theorem statements: whenever a new goal 1.291 +is stated, "find_theorems solves" is called; any theorems that could 1.292 +solve the lemma directly are listed as part of the goal state. 1.293 +Cf. associated options in Proof General Isabelle settings menu, 1.294 +enabled by default, with reasonable timeout for pathological cases of 1.295 +higher-order unification. 1.296 1.297 1.298 *** Document preparation *** 1.299 @@ -213,34 +218,84 @@ 1.300 1.301 *** HOL *** 1.302 1.303 -* Theory Library/Polynomial.thy defines an abstract type 'a poly of 1.304 -univariate polynomials with coefficients of type 'a. In addition to 1.305 -the standard ring operations, it also supports div and mod. Code 1.306 -generation is also supported, using list-style constructors. 1.307 - 1.308 -* Theory Library/Inner_Product.thy defines a class of real_inner for 1.309 -real inner product spaces, with an overloaded operation inner :: 'a => 1.310 -'a => real. Class real_inner is a subclass of real_normed_vector from 1.311 -RealVector.thy. 1.312 - 1.313 -* Theory Library/Product_Vector.thy provides instances for the product 1.314 -type 'a * 'b of several classes from RealVector.thy and 1.315 -Inner_Product.thy. Definitions of addition, subtraction, scalar 1.316 -multiplication, norms, and inner products are included. 1.317 - 1.318 -* Theory Library/Bit.thy defines the field "bit" of integers modulo 2. 1.319 -In addition to the field operations, numerals and case syntax are also 1.320 -supported. 1.321 - 1.322 -* Theory Library/Diagonalize.thy provides constructive version of 1.323 -Cantor's first diagonalization argument. 1.324 - 1.325 -* New predicate "strict_mono" classifies strict functions on partial orders. 1.326 -With strict functions on linear orders, reasoning about (in)equalities is 1.327 -facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less". 1.328 - 1.329 -* Some set operations are now proper qualified constants with authentic syntax. 1.330 -INCOMPATIBILITY: 1.331 +* Integrated main parts of former image HOL-Complex with HOL. Entry 1.332 +points Main and Complex_Main remain as before. 1.333 + 1.334 +* Logic image HOL-Plain provides a minimal HOL with the most important 1.335 +tools available (inductive, datatype, primrec, ...). This facilitates 1.336 +experimentation and tool development. Note that user applications 1.337 +(and library theories) should never refer to anything below theory 1.338 +Main, as before. 1.339 + 1.340 +* Logic image HOL-Main stops at theory Main, and thus facilitates 1.341 +experimentation due to shorter build times. 1.342 + 1.343 +* Logic image HOL-NSA contains theories of nonstandard analysis which 1.344 +were previously part of former HOL-Complex. Entry point Hyperreal 1.345 +remains valid, but theories formerly using Complex_Main should now use 1.346 +new entry point Hypercomplex. 1.347 + 1.348 +* Generic ATP manager for Sledgehammer, based on ML threads instead of 1.349 +Posix processes. Avoids potentially expensive forking of the ML 1.350 +process. New thread-based implementation also works on non-Unix 1.351 +platforms (Cygwin). Provers are no longer hardwired, but defined 1.352 +within the theory via plain ML wrapper functions. Basic Sledgehammer 1.353 +commands are covered in the isar-ref manual. 1.354 + 1.355 +* Wrapper scripts for remote SystemOnTPTP service allows to use 1.356 +sledgehammer without local ATP installation (Vampire etc.). Other 1.357 +provers may be included via suitable ML wrappers, see also 1.358 +src/HOL/ATP_Linkup.thy. 1.359 + 1.360 +* ATP selection (E/Vampire/Spass) is now via Proof General's settings 1.361 +menu. 1.362 + 1.363 +* The metis method no longer fails because the theorem is too trivial 1.364 +(contains the empty clause). 1.365 + 1.366 +* The metis method now fails in the usual manner, rather than raising 1.367 +an exception, if it determines that it cannot prove the theorem. 1.368 + 1.369 +* Method "coherent" implements a prover for coherent logic (see also 1.370 +src/Tools/coherent.ML). 1.371 + 1.372 +* Constants "undefined" and "default" replace "arbitrary". Usually 1.373 +"undefined" is the right choice to replace "arbitrary", though 1.374 +logically there is no difference. INCOMPATIBILITY. 1.375 + 1.376 +* Command "value" now integrates different evaluation mechanisms. The 1.377 +result of the first successful evaluation mechanism is printed. In 1.378 +square brackets a particular named evaluation mechanisms may be 1.379 +specified (currently, [SML], [code] or [nbe]). See further 1.380 +src/HOL/ex/Eval_Examples.thy. 1.381 + 1.382 +* Normalization by evaluation now allows non-leftlinear equations. 1.383 +Declare with attribute [code nbe]. 1.384 + 1.385 +* Methods "case_tac" and "induct_tac" now refer to the very same rules 1.386 +as the structured Isar versions "cases" and "induct", cf. the 1.387 +corresponding "cases" and "induct" attributes. Mutual induction rules 1.388 +are now presented as a list of individual projections 1.389 +(e.g. foo_bar.inducts for types foo and bar); the old format with 1.390 +explicit HOL conjunction is no longer supported. INCOMPATIBILITY, in 1.391 +rare situations a different rule is selected --- notably nested tuple 1.392 +elimination instead of former prod.exhaust: use explicit (case_tac t 1.393 +rule: prod.exhaust) here. 1.394 + 1.395 +* Attributes "cases", "induct", "coinduct" support "del" option. 1.396 + 1.397 +* Removed fact "case_split_thm", which duplicates "case_split". 1.398 + 1.399 +* The option datatype has been moved to a new theory Option. Renamed 1.400 +option_map to Option.map, and o2s to Option.set, INCOMPATIBILITY. 1.401 + 1.402 +* New predicate "strict_mono" classifies strict functions on partial 1.403 +orders. With strict functions on linear orders, reasoning about 1.404 +(in)equalities is facilitated by theorems "strict_mono_eq", 1.405 +"strict_mono_less_eq" and "strict_mono_less". 1.406 + 1.407 +* Some set operations are now proper qualified constants with 1.408 +authentic syntax. INCOMPATIBILITY: 1.409 1.410 op Int ~> Set.Int 1.411 op Un ~> Set.Un 1.412 @@ -251,26 +306,28 @@ 1.413 {} ~> Set.empty 1.414 UNIV ~> Set.UNIV 1.415 1.416 -* Class complete_lattice with operations Inf, Sup, INFI, SUPR now in theory 1.417 -Set. 1.418 - 1.419 -* Auxiliary class "itself" has disappeared -- classes without any parameter 1.420 -are treated as expected by the 'class' command. 1.421 +* Class complete_lattice with operations Inf, Sup, INFI, SUPR now in 1.422 +theory Set. 1.423 + 1.424 +* Auxiliary class "itself" has disappeared -- classes without any 1.425 +parameter are treated as expected by the 'class' command. 1.426 1.427 * Leibnitz's Series for Pi and the arcus tangens and logarithm series. 1.428 1.429 -* Common decision procedures (Cooper, MIR, Ferrack, Approximation, Dense_Linear_Order) 1.430 -now in directory HOL/Decision_Procs. 1.431 - 1.432 -* Theory HOL/Decision_Procs/Approximation.thy provides the new proof method 1.433 -"approximation". It proves formulas on real values by using interval arithmetic. 1.434 -In the formulas are also the transcendental functions sin, cos, tan, atan, ln, 1.435 -exp and the constant pi are allowed. For examples see 1.436 -HOL/Descision_Procs/ex/Approximation_Ex.thy. 1.437 +* Common decision procedures (Cooper, MIR, Ferrack, Approximation, 1.438 +Dense_Linear_Order) are now in directory HOL/Decision_Procs. 1.439 + 1.440 +* Theory src/HOL/Decision_Procs/Approximation provides the new proof 1.441 +method "approximation". It proves formulas on real values by using 1.442 +interval arithmetic. In the formulas are also the transcendental 1.443 +functions sin, cos, tan, atan, ln, exp and the constant pi are 1.444 +allowed. For examples see 1.445 +src/HOL/Descision_Procs/ex/Approximation_Ex.thy. 1.446 1.447 * Theory "Reflection" now resides in HOL/Library. 1.448 1.449 -* Entry point to Word library now simply named "Word". INCOMPATIBILITY. 1.450 +* Entry point to Word library now simply named "Word". 1.451 +INCOMPATIBILITY. 1.452 1.453 * Made source layout more coherent with logical distribution 1.454 structure: 1.455 @@ -327,82 +384,65 @@ 1.456 src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL 1.457 src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL 1.458 1.459 -* If methods "eval" and "evaluation" encounter a structured proof state 1.460 -with !!/==>, only the conclusion is evaluated to True (if possible), 1.461 -avoiding strange error messages. 1.462 - 1.463 -* Simplifier: simproc for let expressions now unfolds if bound variable 1.464 -occurs at most once in let expression body. INCOMPATIBILITY. 1.465 - 1.466 -* New attribute "arith" for facts that should always be used automaticaly 1.467 -by arithmetic. It is intended to be used locally in proofs, eg 1.468 -assumes [arith]: "x > 0" 1.469 +* If methods "eval" and "evaluation" encounter a structured proof 1.470 +state with !!/==>, only the conclusion is evaluated to True (if 1.471 +possible), avoiding strange error messages. 1.472 + 1.473 +* Method "sizechange" automates termination proofs using (a 1.474 +modification of) the size-change principle. Requires SAT solver. See 1.475 +src/HOL/ex/Termination.thy for examples. 1.476 + 1.477 +* Simplifier: simproc for let expressions now unfolds if bound 1.478 +variable occurs at most once in let expression body. INCOMPATIBILITY. 1.479 + 1.480 +* Method "arith": Linear arithmetic now ignores all inequalities when 1.481 +fast_arith_neq_limit is exceeded, instead of giving up entirely. 1.482 + 1.483 +* New attribute "arith" for facts that should always be used 1.484 +automatically by arithmetic. It is intended to be used locally in 1.485 +proofs, e.g. 1.486 + 1.487 + assumes [arith]: "x > 0" 1.488 + 1.489 Global usage is discouraged because of possible performance impact. 1.490 1.491 -* New classes "top" and "bot" with corresponding operations "top" and "bot" 1.492 -in theory Orderings; instantiation of class "complete_lattice" requires 1.493 -instantiation of classes "top" and "bot". INCOMPATIBILITY. 1.494 - 1.495 -* Changed definition lemma "less_fun_def" in order to provide an instance 1.496 -for preorders on functions; use lemma "less_le" instead. INCOMPATIBILITY. 1.497 - 1.498 -* Unified theorem tables for both code code generators. Thus 1.499 -[code func] has disappeared and only [code] remains. INCOMPATIBILITY. 1.500 - 1.501 -* Constants "undefined" and "default" replace "arbitrary". Usually 1.502 -"undefined" is the right choice to replace "arbitrary", though logically 1.503 -there is no difference. INCOMPATIBILITY. 1.504 - 1.505 -* Generic ATP manager for Sledgehammer, based on ML threads instead of 1.506 -Posix processes. Avoids potentially expensive forking of the ML 1.507 -process. New thread-based implementation also works on non-Unix 1.508 -platforms (Cygwin). Provers are no longer hardwired, but defined 1.509 -within the theory via plain ML wrapper functions. Basic Sledgehammer 1.510 -commands are covered in the isar-ref manual. 1.511 - 1.512 -* Wrapper scripts for remote SystemOnTPTP service allows to use 1.513 -sledgehammer without local ATP installation (Vampire etc.). Other 1.514 -provers may be included via suitable ML wrappers, see also 1.515 -src/HOL/ATP_Linkup.thy. 1.516 - 1.517 -* Normalization by evaluation now allows non-leftlinear equations. 1.518 -Declare with attribute [code nbe]. 1.519 - 1.520 -* Command "value" now integrates different evaluation 1.521 -mechanisms. The result of the first successful evaluation mechanism 1.522 -is printed. In square brackets a particular named evaluation 1.523 -mechanisms may be specified (currently, [SML], [code] or [nbe]). See 1.524 -further src/HOL/ex/Eval_Examples.thy. 1.525 - 1.526 -* New method "sizechange" to automate termination proofs using (a 1.527 -modification of) the size-change principle. Requires SAT solver. See 1.528 -src/HOL/ex/Termination.thy for examples. 1.529 - 1.530 -* HOL/Orderings: class "wellorder" moved here, with explicit induction 1.531 -rule "less_induct" as assumption. For instantiation of "wellorder" by 1.532 -means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY. 1.533 - 1.534 -* HOL/Orderings: added class "preorder" as superclass of "order". 1.535 +* New classes "top" and "bot" with corresponding operations "top" and 1.536 +"bot" in theory Orderings; instantiation of class "complete_lattice" 1.537 +requires instantiation of classes "top" and "bot". INCOMPATIBILITY. 1.538 + 1.539 +* Changed definition lemma "less_fun_def" in order to provide an 1.540 +instance for preorders on functions; use lemma "less_le" instead. 1.541 +INCOMPATIBILITY. 1.542 + 1.543 +* Theory Orderings: class "wellorder" moved here, with explicit 1.544 +induction rule "less_induct" as assumption. For instantiation of 1.545 +"wellorder" by means of predicate "wf", use rule wf_wellorderI. 1.546 +INCOMPATIBILITY. 1.547 + 1.548 +* Theory Orderings: added class "preorder" as superclass of "order". 1.549 INCOMPATIBILITY: Instantiation proofs for order, linorder 1.550 etc. slightly changed. Some theorems named order_class.* now named 1.551 preorder_class.*. 1.552 1.553 -* HOL/Relation: 1.554 -Renamed "refl" to "refl_on", "reflexive" to "refl, "diag" to "Id_on". 1.555 - 1.556 -* HOL/Finite_Set: added a new fold combinator of type 1.557 +* Theory Relation: renamed "refl" to "refl_on", "reflexive" to "refl, 1.558 +"diag" to "Id_on". 1.559 + 1.560 +* Theory Finite_Set: added a new fold combinator of type 1.561 + 1.562 ('a => 'b => 'b) => 'b => 'a set => 'b 1.563 -Occasionally this is more convenient than the old fold combinator which is 1.564 -now defined in terms of the new one and renamed to fold_image. 1.565 - 1.566 -* HOL/Ring_and_Field and HOL/OrderedGroup: The lemmas "group_simps" and 1.567 -"ring_simps" have been replaced by "algebra_simps" (which can be extended with 1.568 -further lemmas!). At the moment both still exist but the former will disappear 1.569 -at some point. 1.570 - 1.571 -* HOL/Power: Lemma power_Suc is now declared as a simp rule in class 1.572 -recpower. Type-specific simp rules for various recpower types have 1.573 -been removed. INCOMPATIBILITY. Rename old lemmas as follows: 1.574 + 1.575 +Occasionally this is more convenient than the old fold combinator 1.576 +which is now defined in terms of the new one and renamed to 1.577 +fold_image. 1.578 + 1.579 +* Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps" 1.580 +and "ring_simps" have been replaced by "algebra_simps" (which can be 1.581 +extended with further lemmas!). At the moment both still exist but 1.582 +the former will disappear at some point. 1.583 + 1.584 +* Theory Power: Lemma power_Suc is now declared as a simp rule in 1.585 +class recpower. Type-specific simp rules for various recpower types 1.586 +have been removed. INCOMPATIBILITY, rename old lemmas as follows: 1.587 1.588 rat_power_0 -> power_0 1.589 rat_power_Suc -> power_Suc 1.590 @@ -413,7 +453,7 @@ 1.591 power_poly_0 -> power_0 1.592 power_poly_Suc -> power_Suc 1.593 1.594 -* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been 1.595 +* Theories Ring_and_Field and Divides: Definition of "op dvd" has been 1.596 moved to separate class dvd in Ring_and_Field; a couple of lemmas on 1.597 dvd has been generalized to class comm_semiring_1. Likewise a bunch 1.598 of lemmas from Divides has been generalized from nat to class 1.599 @@ -428,9 +468,9 @@ 1.600 mult_div ~> div_mult_self2_is_id 1.601 mult_mod ~> mod_mult_self2_is_0 1.602 1.603 -* HOL/IntDiv: removed many lemmas that are instances of class-based 1.604 -generalizations (from Divides and Ring_and_Field). 1.605 -INCOMPATIBILITY. Rename old lemmas as follows: 1.606 +* Theory IntDiv: removed many lemmas that are instances of class-based 1.607 +generalizations (from Divides and Ring_and_Field). INCOMPATIBILITY, 1.608 +rename old lemmas as follows: 1.609 1.610 dvd_diff -> nat_dvd_diff 1.611 dvd_zminus_iff -> dvd_minus_iff 1.612 @@ -478,11 +518,38 @@ 1.613 zdvd_1_left -> one_dvd 1.614 zminus_dvd_iff -> minus_dvd_iff 1.615 1.616 -* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, 1.617 +* Theory Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. 1.618 + 1.619 +* The real numbers offer decimal input syntax: 12.34 is translated 1.620 +into 1234/10^2. This translation is not reversed upon output. 1.621 + 1.622 +* Theory Library/Polynomial defines an abstract type 'a poly of 1.623 +univariate polynomials with coefficients of type 'a. In addition to 1.624 +the standard ring operations, it also supports div and mod. Code 1.625 +generation is also supported, using list-style constructors. 1.626 + 1.627 +* Theory Library/Inner_Product defines a class of real_inner for real 1.628 +inner product spaces, with an overloaded operation inner :: 'a => 'a 1.629 +=> real. Class real_inner is a subclass of real_normed_vector from 1.630 +theory RealVector. 1.631 + 1.632 +* Theory Library/Product_Vector provides instances for the product 1.633 +type 'a * 'b of several classes from RealVector and Inner_Product. 1.634 +Definitions of addition, subtraction, scalar multiplication, norms, 1.635 +and inner products are included. 1.636 + 1.637 +* Theory Library/Bit defines the field "bit" of integers modulo 2. In 1.638 +addition to the field operations, numerals and case syntax are also 1.639 +supported. 1.640 + 1.641 +* Theory Library/Diagonalize provides constructive version of Cantor's 1.642 +first diagonalization argument. 1.643 + 1.644 +* Theory Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, 1.645 zlcm (for int); carried together from various gcd/lcm developements in 1.646 -the HOL Distribution. zgcd and zlcm replace former igcd and ilcm; 1.647 -corresponding theorems renamed accordingly. INCOMPATIBILITY. To 1.648 -recover tupled syntax, use syntax declarations like: 1.649 +the HOL Distribution. Constants zgcd and zlcm replace former igcd and 1.650 +ilcm; corresponding theorems renamed accordingly. INCOMPATIBILITY, 1.651 +may recover tupled syntax as follows: 1.652 1.653 hide (open) const gcd 1.654 abbreviation gcd where 1.655 @@ -490,54 +557,24 @@ 1.656 notation (output) 1.657 GCD.gcd ("gcd '(_, _')") 1.658 1.659 -(analogously for lcm, zgcd, zlcm). 1.660 - 1.661 -* HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. 1.662 - 1.663 -* The real numbers offer decimal input syntax: 12.34 is translated into 1.664 - 1234/10^2. This translation is not reversed upon output. 1.665 - 1.666 -* New ML antiquotation @{code}: takes constant as argument, generates 1.667 +The same works for lcm, zgcd, zlcm. 1.668 + 1.669 +* Theory Library/Nat_Infinity: added addition, numeral syntax and more 1.670 +instantiations for algebraic structures. Removed some duplicate 1.671 +theorems. Changes in simp rules. INCOMPATIBILITY. 1.672 + 1.673 +* ML antiquotation @{code} takes a constant as argument and generates 1.674 corresponding code in background and inserts name of the corresponding 1.675 resulting ML value/function/datatype constructor binding in place. 1.676 All occurrences of @{code} with a single ML block are generated 1.677 simultaneously. Provides a generic and safe interface for 1.678 -instrumentalizing code generation. See HOL/Decision_Procs/Ferrack for 1.679 -a more ambitious application. In future you ought refrain from ad-hoc 1.680 -compiling generated SML code on the ML toplevel. Note that (for technical 1.681 -reasons) @{code} cannot refer to constants for which user-defined 1.682 -serializations are set. Refer to the corresponding ML counterpart 1.683 -directly in that cases. 1.684 - 1.685 -* Integrated image HOL-Complex with HOL. Entry points Main.thy and 1.686 -Complex_Main.thy remain as they are. 1.687 - 1.688 -* New image HOL-Plain provides a minimal HOL with the most important 1.689 -tools available (inductive, datatype, primrec, ...). By convention 1.690 -the corresponding theory Plain should be ancestor of every further 1.691 -(library) theory. Some library theories now have ancestor Plain 1.692 -(instead of Main), thus theory Main occasionally has to be imported 1.693 -explicitly. 1.694 - 1.695 -* The metis method now fails in the usual manner, rather than raising 1.696 -an exception, if it determines that it cannot prove the theorem. 1.697 - 1.698 -* The metis method no longer fails because the theorem is too trivial 1.699 -(contains the empty clause). 1.700 - 1.701 -* Methods "case_tac" and "induct_tac" now refer to the very same rules 1.702 -as the structured Isar versions "cases" and "induct", cf. the 1.703 -corresponding "cases" and "induct" attributes. Mutual induction rules 1.704 -are now presented as a list of individual projections 1.705 -(e.g. foo_bar.inducts for types foo and bar); the old format with 1.706 -explicit HOL conjunction is no longer supported. INCOMPATIBILITY, in 1.707 -rare situations a different rule is selected --- notably nested tuple 1.708 -elimination instead of former prod.exhaust: use explicit (case_tac t 1.709 -rule: prod.exhaust) here. 1.710 - 1.711 -* Attributes "cases", "induct", "coinduct" support "del" option. 1.712 - 1.713 -* Removed fact "case_split_thm", which duplicates "case_split". 1.714 +instrumentalizing code generation. See 1.715 +src/HOL/Decision_Procs/Ferrack.thy for a more ambitious application. 1.716 +In future you ought to refrain from ad-hoc compiling generated SML 1.717 +code on the ML toplevel. Note that (for technical reasons) @{code} 1.718 +cannot refer to constants for which user-defined serializations are 1.719 +set. Refer to the corresponding ML counterpart directly in that 1.720 +cases. 1.721 1.722 * Command 'rep_datatype': instead of theorem names the command now 1.723 takes a list of terms denoting the constructors of the type to be 1.724 @@ -551,19 +588,6 @@ 1.725 Suc_Suc_eq ~> nat.inject 1.726 Suc_not_Zero Zero_not_Suc ~> nat.distinct 1.727 1.728 -* The option datatype has been moved to a new theory HOL/Option.thy. 1.729 -Renamed option_map to Option.map, and o2s to Option.set. 1.730 - 1.731 -* Library/Nat_Infinity: added addition, numeral syntax and more 1.732 -instantiations for algebraic structures. Removed some duplicate 1.733 -theorems. Changes in simp rules. INCOMPATIBILITY. 1.734 - 1.735 -* ATP selection (E/Vampire/Spass) is now via Proof General's settings 1.736 -menu. 1.737 - 1.738 -* Linear arithmetic now ignores all inequalities when 1.739 -fast_arith_neq_limit is exceeded, instead of giving up entirely. 1.740 - 1.741 1.742 *** HOL-Algebra *** 1.743 1.744 @@ -573,11 +597,12 @@ 1.745 1.746 * New theory of factorial domains. 1.747 1.748 -* Units_l_inv and Units_r_inv are now simprules by default. 1.749 +* Units_l_inv and Units_r_inv are now simp rules by default. 1.750 INCOMPATIBILITY. Simplifier proof that require deletion of l_inv 1.751 and/or r_inv will now also require deletion of these lemmas. 1.752 1.753 -* Renamed the following theorems. INCOMPATIBILITY. 1.754 +* Renamed the following theorems, INCOMPATIBILITY: 1.755 + 1.756 UpperD ~> Upper_memD 1.757 LowerD ~> Lower_memD 1.758 least_carrier ~> least_closed 1.759 @@ -587,19 +612,6 @@ 1.760 one_not_zero ~> carrier_one_not_zero (collision with assumption) 1.761 1.762 1.763 -*** HOL-NSA *** 1.764 - 1.765 -* Created new image HOL-NSA, containing theories of nonstandard 1.766 -analysis which were previously part of HOL-Complex. Entry point 1.767 -Hyperreal.thy remains valid, but theories formerly using 1.768 -Complex_Main.thy should now use new entry point Hypercomplex.thy. 1.769 - 1.770 - 1.771 -*** ZF *** 1.772 - 1.773 -* Proof of Zorn's Lemma for partial orders. 1.774 - 1.775 - 1.776 *** HOLCF *** 1.777 1.778 * Reimplemented the simplification procedure for proving continuity 1.779 @@ -612,23 +624,47 @@ 1.780 old one could solve, and "simp add: cont2cont_LAM" may be necessary. 1.781 Potential INCOMPATIBILITY. 1.782 1.783 -* The syntax of the fixrec package has changed. The specification 1.784 -syntax now conforms in style to definition, primrec, function, etc. 1.785 -See HOLCF/ex/Fixrec_ex.thy for examples. INCOMPATIBILITY. 1.786 +* The syntax of the fixrec package now conforms to the general 1.787 +specification format of inductive, primrec, function, etc. See 1.788 +src/HOLCF/ex/Fixrec_ex.thy for examples. INCOMPATIBILITY. 1.789 + 1.790 + 1.791 +*** ZF *** 1.792 + 1.793 +* Proof of Zorn's Lemma for partial orders. 1.794 1.795 1.796 *** ML *** 1.797 1.798 +* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for 1.799 +Poly/ML 5.2.1 or later. Important note: the TimeLimit facility 1.800 +depends on multithreading, so timouts will not work before Poly/ML 1.801 +5.2.1! 1.802 + 1.803 * High-level support for concurrent ML programming, see 1.804 src/Pure/Cuncurrent. The data-oriented model of "future values" is 1.805 particularly convenient to organize independent functional 1.806 computations. The concept of "synchronized variables" provides a 1.807 higher-order interface for components with shared state, avoiding the 1.808 -delicate details of mutexes and condition variables. [Poly/ML 5.2.1 1.809 -or later] 1.810 +delicate details of mutexes and condition variables. (Requires 1.811 +Poly/ML 5.2.1 or later.) 1.812 + 1.813 +* ML bindings produced via Isar commands are stored within the Isar 1.814 +context (theory or proof). Consequently, commands like 'use' and 'ML' 1.815 +become thread-safe and work with undo as expected (concerning 1.816 +top-level bindings, not side-effects on global references). 1.817 +INCOMPATIBILITY, need to provide proper Isar context when invoking the 1.818 +compiler at runtime; really global bindings need to be given outside a 1.819 +theory. (Requires Poly/ML 5.2 or later.) 1.820 + 1.821 +* Command 'ML_prf' is analogous to 'ML' but works within a proof 1.822 +context. Top-level ML bindings are stored within the proof context in 1.823 +a purely sequential fashion, disregarding the nested proof structure. 1.824 +ML bindings introduced by 'ML_prf' are discarded at the end of the 1.825 +proof. (Requires Poly/ML 5.2 or later.) 1.826 1.827 * Simplified ML attribute and method setup, cf. functions Attrib.setup 1.828 -and Method.setup, as well as commands 'attribute_setup' and 1.829 +and Method.setup, as well as Isar commands 'attribute_setup' and 1.830 'method_setup'. INCOMPATIBILITY for 'method_setup', need to simplify 1.831 existing code accordingly, or use plain 'setup' together with old 1.832 Method.add_method. 1.833 @@ -640,52 +676,27 @@ 1.834 accordingly. Note that extra performance may be gained by producing 1.835 the cterm carefully, avoiding slow Thm.cterm_of. 1.836 1.837 -* ML bindings produced via Isar commands are stored within the Isar 1.838 -context (theory or proof). Consequently, commands like 'use' and 'ML' 1.839 -become thread-safe and work with undo as expected (concerning 1.840 -top-level bindings, not side-effects on global references). 1.841 -INCOMPATIBILITY, need to provide proper Isar context when invoking the 1.842 -compiler at runtime; really global bindings need to be given outside a 1.843 -theory. [Poly/ML 5.2 or later] 1.844 - 1.845 -* Command 'ML_prf' is analogous to 'ML' but works within a proof 1.846 -context. Top-level ML bindings are stored within the proof context in 1.847 -a purely sequential fashion, disregarding the nested proof structure. 1.848 -ML bindings introduced by 'ML_prf' are discarded at the end of the 1.849 -proof. [Poly/ML 5.2 or later] 1.850 - 1.851 -* Generic Toplevel.add_hook interface allows to analyze the result of 1.852 -transactions. E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML 1.853 -for theorem dependency output of transactions resulting in a new 1.854 -theory state. 1.855 +* Simplified interface for defining document antiquotations via 1.856 +ThyOutput.antiquotation, ThyOutput.output, and optionally 1.857 +ThyOutput.maybe_pretty_source. INCOMPATIBILITY, need to simplify user 1.858 +antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common 1.859 +examples. 1.860 1.861 * More systematic treatment of long names, abstract name bindings, and 1.862 name space operations. Basic operations on qualified names have been 1.863 move from structure NameSpace to Long_Name, e.g. Long_Name.base_name, 1.864 Long_Name.append. Old type bstring has been mostly replaced by 1.865 abstract type binding (see structure Binding), which supports precise 1.866 -qualification (by packages and local theory targets), as well as 1.867 -proper tracking of source positions. INCOMPATIBILITY, need to wrap 1.868 -old bstring values into Binding.name, or better pass through abstract 1.869 +qualification by packages and local theory targets, as well as proper 1.870 +tracking of source positions. INCOMPATIBILITY, need to wrap old 1.871 +bstring values into Binding.name, or better pass through abstract 1.872 bindings everywhere. See further src/Pure/General/long_name.ML, 1.873 src/Pure/General/binding.ML and src/Pure/General/name_space.ML 1.874 1.875 -* Simplified interface for defining document antiquotations via 1.876 -ThyOutput.antiquotation, ThyOutput.output, and optionally 1.877 -ThyOutput.maybe_pretty_source. INCOMPATIBILITY, need to simplify user 1.878 -antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common 1.879 -examples. 1.880 - 1.881 * Result facts (from PureThy.note_thms, ProofContext.note_thms, 1.882 LocalTheory.note etc.) now refer to the *full* internal name, not the 1.883 bstring as before. INCOMPATIBILITY, not detected by ML type-checking! 1.884 1.885 -* Rules and tactics that read instantiations (read_instantiate, 1.886 -res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof 1.887 -context, which is required for parsing and type-checking. Moreover, 1.888 -the variables are specified as plain indexnames, not string encodings 1.889 -thereof. INCOMPATIBILITY. 1.890 - 1.891 * Disposed old type and term read functions (Sign.read_def_typ, 1.892 Sign.read_typ, Sign.read_def_terms, Sign.read_term, 1.893 Thm.read_def_cterms, Thm.read_cterm etc.). INCOMPATIBILITY, should 1.894 @@ -699,9 +710,21 @@ 1.895 embedded ML text, or local_simpset_of with a proper context passed as 1.896 explicit runtime argument. 1.897 1.898 -* Antiquotations: block-structured compilation context indicated by 1.899 +* Rules and tactics that read instantiations (read_instantiate, 1.900 +res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof 1.901 +context, which is required for parsing and type-checking. Moreover, 1.902 +the variables are specified as plain indexnames, not string encodings 1.903 +thereof. INCOMPATIBILITY. 1.904 + 1.905 +* Generic Toplevel.add_hook interface allows to analyze the result of 1.906 +transactions. E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML 1.907 +for theorem dependency output of transactions resulting in a new 1.908 +theory state. 1.909 + 1.910 +* ML antiquotations: block-structured compilation context indicated by 1.911 \<lbrace> ... \<rbrace>; additional antiquotation forms: 1.912 1.913 + @{binding name} - basic name binding 1.914 @{let ?pat = term} - term abbreviation (HO matching) 1.915 @{note name = fact} - fact abbreviation 1.916 @{thm fact} - singleton fact (with attributes) 1.917 @@ -715,9 +738,6 @@ 1.918 1.919 *** System *** 1.920 1.921 -* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for 1.922 -Poly/ML 5.2.1 or later. 1.923 - 1.924 * The Isabelle "emacs" tool provides a specific interface to invoke 1.925 Proof General / Emacs, with more explicit failure if that is not 1.926 installed (the old isabelle-interface script silently falls back on 1.927 @@ -729,13 +749,13 @@ 1.928 Isabelle/lib/jedit/plugin for a minimal example. (The obsolete Java 1.929 process wrapper has been discontinued.) 1.930 1.931 -* Status messages (with exact source position information) are 1.932 +* Added homegrown Isabelle font with unicode layout, see lib/fonts. 1.933 + 1.934 +* Various status messages (with exact source position information) are 1.935 emitted, if proper markup print mode is enabled. This allows 1.936 user-interface components to provide detailed feedback on internal 1.937 prover operations. 1.938 1.939 -* Homegrown Isabelle font with unicode layout, see Isabelle/lib/fonts. 1.940 - 1.941 1.942 1.943 New in Isabelle2008 (June 2008)