1.1 --- a/NEWS Sun Jun 06 18:47:29 2010 +0200
1.2 +++ b/NEWS Mon Jun 07 11:27:08 2010 +0200
1.3 @@ -6,12 +6,6 @@
1.4
1.5 *** General ***
1.6
1.7 -* Schematic theorem statements need to be explicitly markup as such,
1.8 -via commands 'schematic_lemma', 'schematic_theorem',
1.9 -'schematic_corollary'. Thus the relevance of the proof is made
1.10 -syntactically clear, which impacts performance in a parallel or
1.11 -asynchronous interactive environment. Minor INCOMPATIBILITY.
1.12 -
1.13 * Authentic syntax for *all* logical entities (type classes, type
1.14 constructors, term constants): provides simple and robust
1.15 correspondence between formal entities and concrete syntax. Within
1.16 @@ -69,62 +63,76 @@
1.17 'def', 'obtain' etc. or via the explicit 'write' command, which is
1.18 similar to the 'notation' command in theory specifications.
1.19
1.20 -* Use of cumulative prems via "!" in some proof methods has been
1.21 -discontinued (legacy feature).
1.22 -
1.23 -* References 'trace_simp' and 'debug_simp' have been replaced by
1.24 -configuration options stored in the context. Enabling tracing (the
1.25 -case of debugging is similar) in proofs works via
1.26 -
1.27 - using [[trace_simp = true]]
1.28 -
1.29 -Tracing is then active for all invocations of the simplifier in
1.30 -subsequent goal refinement steps. Tracing may also still be enabled or
1.31 -disabled via the ProofGeneral settings menu.
1.32 -
1.33 -* Separate commands 'hide_class', 'hide_type', 'hide_const',
1.34 -'hide_fact' replace the former 'hide' KIND command. Minor
1.35 -INCOMPATIBILITY.
1.36 -
1.37 -* Improved parallelism of proof term normalization: usedir -p2 -q0 is
1.38 -more efficient than combinations with -q1 or -q2.
1.39 -
1.40 -
1.41 -*** Pure ***
1.42 -
1.43 -* Predicates of locales introduced by classes carry a mandatory
1.44 -"class" prefix. INCOMPATIBILITY.
1.45 -
1.46 -* Command 'code_reflect' allows to incorporate generated ML code into
1.47 -runtime environment; replaces immature code_datatype antiquotation.
1.48 -INCOMPATIBILITY.
1.49 -
1.50 -* Empty class specifications observe default sort. INCOMPATIBILITY.
1.51 -
1.52 -* Old 'axclass' command has been discontinued. Use 'class' instead.
1.53 -INCOMPATIBILITY.
1.54 -
1.55 -* Code generator: simple concept for abstract datatypes obeying
1.56 -invariants.
1.57 -
1.58 -* Local theory specifications may depend on extra type variables that
1.59 -are not present in the result type -- arguments TYPE('a) :: 'a itself
1.60 -are added internally. For example:
1.61 -
1.62 - definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
1.63 -
1.64 -* Code generator: details of internal data cache have no impact on the
1.65 -user space functionality any longer.
1.66 -
1.67 -* Methods unfold_locales and intro_locales ignore non-locale subgoals.
1.68 -This is more appropriate for interpretations with 'where'.
1.69 -INCOMPATIBILITY.
1.70 -
1.71 * Discontinued unnamed infix syntax (legacy feature for many years) --
1.72 need to specify constant name and syntax separately. Internal ML
1.73 datatype constructors have been renamed from InfixName to Infix etc.
1.74 Minor INCOMPATIBILITY.
1.75
1.76 +* Schematic theorem statements need to be explicitly markup as such,
1.77 +via commands 'schematic_lemma', 'schematic_theorem',
1.78 +'schematic_corollary'. Thus the relevance of the proof is made
1.79 +syntactically clear, which impacts performance in a parallel or
1.80 +asynchronous interactive environment. Minor INCOMPATIBILITY.
1.81 +
1.82 +* Use of cumulative prems via "!" in some proof methods has been
1.83 +discontinued (old legacy feature).
1.84 +
1.85 +* References 'trace_simp' and 'debug_simp' have been replaced by
1.86 +configuration options stored in the context. Enabling tracing (the
1.87 +case of debugging is similar) in proofs works via
1.88 +
1.89 + using [[trace_simp = true]]
1.90 +
1.91 +Tracing is then active for all invocations of the simplifier in
1.92 +subsequent goal refinement steps. Tracing may also still be enabled or
1.93 +disabled via the ProofGeneral settings menu.
1.94 +
1.95 +* Separate commands 'hide_class', 'hide_type', 'hide_const',
1.96 +'hide_fact' replace the former 'hide' KIND command. Minor
1.97 +INCOMPATIBILITY.
1.98 +
1.99 +* Improved parallelism of proof term normalization: usedir -p2 -q0 is
1.100 +more efficient than combinations with -q1 or -q2.
1.101 +
1.102 +
1.103 +*** Pure ***
1.104 +
1.105 +* Proofterms record type-class reasoning explicitly, using the
1.106 +"unconstrain" operation internally. This eliminates all sort
1.107 +constraints from a theorem and proof, introducing explicit
1.108 +OFCLASS-premises. On the proof term level, this operation is
1.109 +automatically applied at theorem boundaries, such that closed proofs
1.110 +are always free of sort constraints. INCOMPATIBILITY for tools that
1.111 +inspect proof terms.
1.112 +
1.113 +* Local theory specifications may depend on extra type variables that
1.114 +are not present in the result type -- arguments TYPE('a) :: 'a itself
1.115 +are added internally. For example:
1.116 +
1.117 + definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
1.118 +
1.119 +* Predicates of locales introduced by classes carry a mandatory
1.120 +"class" prefix. INCOMPATIBILITY.
1.121 +
1.122 +* Vacuous class specifications observe default sort. INCOMPATIBILITY.
1.123 +
1.124 +* Old 'axclass' command has been discontinued. INCOMPATIBILITY, use
1.125 +'class' instead.
1.126 +
1.127 +* Command 'code_reflect' allows to incorporate generated ML code into
1.128 +runtime environment; replaces immature code_datatype antiquotation.
1.129 +INCOMPATIBILITY.
1.130 +
1.131 +* Code generator: simple concept for abstract datatypes obeying
1.132 +invariants.
1.133 +
1.134 +* Code generator: details of internal data cache have no impact on the
1.135 +user space functionality any longer.
1.136 +
1.137 +* Methods "unfold_locales" and "intro_locales" ignore non-locale
1.138 +subgoals. This is more appropriate for interpretations with 'where'.
1.139 +INCOMPATIBILITY.
1.140 +
1.141 * Command 'example_proof' opens an empty proof body. This allows to
1.142 experiment with Isar, without producing any persistent result.
1.143
1.144 @@ -139,24 +147,42 @@
1.145 * Command 'defaultsort' has been renamed to 'default_sort', it works
1.146 within a local theory context. Minor INCOMPATIBILITY.
1.147
1.148 -* Raw axioms/defs may no longer carry sort constraints, and raw defs
1.149 -may no longer carry premises. User-level specifications are
1.150 -transformed accordingly by Thm.add_axiom/add_def.
1.151 -
1.152 -* Proof terms: Type substitutions on proof constants now use canonical
1.153 -order of type variables. INCOMPATIBILITY for tools working with proof
1.154 -terms.
1.155 -
1.156 -* New operation Thm.unconstrainT eliminates all sort constraints from
1.157 -a theorem and proof, introducing explicit OFCLASS-premises. On the
1.158 -proof term level, this operation is automatically applied at PThm
1.159 -boundaries, such that closed proofs are always free of sort
1.160 -constraints. The old (axiomatic) unconstrain operation has been
1.161 -discontinued. INCOMPATIBILITY for tools working with proof terms.
1.162 -
1.163
1.164 *** HOL ***
1.165
1.166 +* Command 'typedef' now works within a local theory context -- without
1.167 +introducing dependencies on parameters or assumptions, which is not
1.168 +possible in Isabelle/Pure/HOL. Note that the logical environment may
1.169 +contain multiple interpretations of local typedefs (with different
1.170 +non-emptiness proofs), even in a global theory context.
1.171 +
1.172 +* New package for quotient types. Commands 'quotient_type' and
1.173 +'quotient_definition' may be used for defining types and constants by
1.174 +quotient constructions. An example is the type of integers created by
1.175 +quotienting pairs of natural numbers:
1.176 +
1.177 + fun
1.178 + intrel :: "(nat * nat) => (nat * nat) => bool"
1.179 + where
1.180 + "intrel (x, y) (u, v) = (x + v = u + y)"
1.181 +
1.182 + quotient_type int = "nat × nat" / intrel
1.183 + by (auto simp add: equivp_def expand_fun_eq)
1.184 +
1.185 + quotient_definition
1.186 + "0::int" is "(0::nat, 0::nat)"
1.187 +
1.188 +The method "lifting" can be used to lift of theorems from the
1.189 +underlying "raw" type to the quotient type. The example
1.190 +src/HOL/Quotient_Examples/FSet.thy includes such a quotient
1.191 +construction and provides a reasoning infrastructure for finite sets.
1.192 +
1.193 +* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid
1.194 +clash with new theory Quotient in Main HOL.
1.195 +
1.196 +* Moved the SMT binding into the main HOL session, eliminating
1.197 +separate HOL-SMT session.
1.198 +
1.199 * List membership infix mem operation is only an input abbreviation.
1.200 INCOMPATIBILITY.
1.201
1.202 @@ -177,8 +203,8 @@
1.203 instead. INCOMPATIBILITY.
1.204
1.205 * Dropped several real-specific versions of lemmas about floor and
1.206 -ceiling; use the generic lemmas from Archimedean_Field.thy instead.
1.207 -INCOMPATIBILITY.
1.208 +ceiling; use the generic lemmas from theory "Archimedean_Field"
1.209 +instead. INCOMPATIBILITY.
1.210
1.211 floor_number_of_eq ~> floor_number_of
1.212 le_floor_eq_number_of ~> number_of_le_floor
1.213 @@ -218,26 +244,19 @@
1.214 provides abstract red-black tree type which is backed by "RBT_Impl" as
1.215 implementation. INCOMPATIBILTY.
1.216
1.217 -* Command 'typedef' now works within a local theory context -- without
1.218 -introducing dependencies on parameters or assumptions, which is not
1.219 -possible in Isabelle/Pure/HOL. Note that the logical environment may
1.220 -contain multiple interpretations of local typedefs (with different
1.221 -non-emptiness proofs), even in a global theory context.
1.222 -
1.223 * Theory Library/Coinductive_List has been removed -- superseded by
1.224 AFP/thys/Coinductive.
1.225
1.226 * Theory PReal, including the type "preal" and related operations, has
1.227 been removed. INCOMPATIBILITY.
1.228
1.229 -* Split off theory Big_Operators containing setsum, setprod, Inf_fin,
1.230 -Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY.
1.231 +* Split off theory "Big_Operators" containing setsum, setprod,
1.232 +Inf_fin, Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY.
1.233
1.234 * Theory "Rational" renamed to "Rat", for consistency with "Nat",
1.235 "Int" etc. INCOMPATIBILITY.
1.236
1.237 -* Constant Rat.normalize needs to be qualified. Minor
1.238 -INCOMPATIBILITY.
1.239 +* Constant Rat.normalize needs to be qualified. INCOMPATIBILITY.
1.240
1.241 * New set of rules "ac_simps" provides combined assoc / commute
1.242 rewrites for all interpretations of the appropriate generic locales.
1.243 @@ -295,7 +314,7 @@
1.244 ordered_semiring_strict ~> linordered_semiring_strict
1.245
1.246 The following slightly odd type classes have been moved to a
1.247 - separate theory Library/Lattice_Algebras.thy:
1.248 + separate theory Library/Lattice_Algebras:
1.249
1.250 lordered_ab_group_add ~> lattice_ab_group_add
1.251 lordered_ab_group_add_abs ~> lattice_ab_group_add_abs
1.252 @@ -335,18 +354,16 @@
1.253 INTER_fold_inter ~> INFI_fold_inf
1.254 UNION_fold_union ~> SUPR_fold_sup
1.255
1.256 -* Theory Complete_Lattice: lemmas top_def and bot_def have been
1.257 +* Theory "Complete_Lattice": lemmas top_def and bot_def have been
1.258 replaced by the more convenient lemmas Inf_empty and Sup_empty.
1.259 Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
1.260 by Inf_insert and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace
1.261 former Inf_Univ and Sup_Univ. Lemmas inf_top_right and sup_bot_right
1.262 subsume inf_top and sup_bot respectively. INCOMPATIBILITY.
1.263
1.264 -* HOLogic.strip_psplit: types are returned in syntactic order, similar
1.265 -to other strip and tuple operations. INCOMPATIBILITY.
1.266 -
1.267 * Reorganized theory Multiset: swapped notation of pointwise and
1.268 multiset order:
1.269 +
1.270 - pointwise ordering is instance of class order with standard syntax
1.271 <= and <;
1.272 - multiset ordering has syntax <=# and <#; partial order properties
1.273 @@ -357,10 +374,13 @@
1.274 generation;
1.275 - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
1.276 if needed.
1.277 +
1.278 Renamed:
1.279 - multiset_eq_conv_count_eq -> multiset_ext_iff
1.280 - multi_count_ext -> multiset_ext
1.281 - diff_union_inverse2 -> diff_union_cancelR
1.282 +
1.283 + multiset_eq_conv_count_eq ~> multiset_ext_iff
1.284 + multi_count_ext ~> multiset_ext
1.285 + diff_union_inverse2 ~> diff_union_cancelR
1.286 +
1.287 INCOMPATIBILITY.
1.288
1.289 * Theory Permutation: replaced local "remove" by List.remove1.
1.290 @@ -369,9 +389,6 @@
1.291
1.292 * Theory List: added transpose.
1.293
1.294 -* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid
1.295 -clash with new theory Quotient in Main HOL.
1.296 -
1.297 * Library/Nat_Bijection.thy is a collection of bijective functions
1.298 between nat and other types, which supersedes the older libraries
1.299 Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy. INCOMPATIBILITY.
1.300 @@ -452,8 +469,6 @@
1.301 "sharing_depth", and "show_skolems" options. INCOMPATIBILITY.
1.302 - Removed "nitpick_intro" attribute. INCOMPATIBILITY.
1.303
1.304 -* Moved the SMT binding into the HOL image.
1.305 -
1.306
1.307 *** HOLCF ***
1.308
1.309 @@ -469,7 +484,7 @@
1.310 * Most definedness lemmas generated by the domain package (previously
1.311 of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form
1.312 like "foo$x = UU <-> x = UU", which works better as a simp rule.
1.313 -Proof scripts that used definedness lemmas as intro rules may break,
1.314 +Proofs that used definedness lemmas as intro rules may break,
1.315 potential INCOMPATIBILITY.
1.316
1.317 * Induction and casedist rules generated by the domain package now
1.318 @@ -513,6 +528,38 @@
1.319
1.320 *** ML ***
1.321
1.322 +* Antiquotations for basic formal entities:
1.323 +
1.324 + @{class NAME} -- type class
1.325 + @{class_syntax NAME} -- syntax representation of the above
1.326 +
1.327 + @{type_name NAME} -- logical type
1.328 + @{type_abbrev NAME} -- type abbreviation
1.329 + @{nonterminal NAME} -- type of concrete syntactic category
1.330 + @{type_syntax NAME} -- syntax representation of any of the above
1.331 +
1.332 + @{const_name NAME} -- logical constant (INCOMPATIBILITY)
1.333 + @{const_abbrev NAME} -- abbreviated constant
1.334 + @{const_syntax NAME} -- syntax representation of any of the above
1.335 +
1.336 +* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
1.337 +syntax constant (cf. 'syntax' command).
1.338 +
1.339 +* Antiquotation @{make_string} inlines a function to print arbitrary
1.340 +values similar to the ML toplevel. The result is compiler dependent
1.341 +and may fall back on "?" in certain situations.
1.342 +
1.343 +* Diagnostic commands 'ML_val' and 'ML_command' may refer to
1.344 +antiquotations @{Isar.state} and @{Isar.goal}. This replaces impure
1.345 +Isar.state() and Isar.goal(), which belong to the old TTY loop and do
1.346 +not work with the asynchronous Isar document model.
1.347 +
1.348 +* Configuration options now admit dynamic default values, depending on
1.349 +the context or even global references.
1.350 +
1.351 +* SHA1.digest digests strings according to SHA-1 (see RFC 3174). It
1.352 +uses an efficient external library if available (for Poly/ML).
1.353 +
1.354 * Renamed some important ML structures, while keeping the old names
1.355 for some time as aliases within the structure Legacy:
1.356
1.357 @@ -541,32 +588,6 @@
1.358 Pretty.pp argument to merge, which is absent in the standard
1.359 Theory_Data version.
1.360
1.361 -* Antiquotations for basic formal entities:
1.362 -
1.363 - @{class NAME} -- type class
1.364 - @{class_syntax NAME} -- syntax representation of the above
1.365 -
1.366 - @{type_name NAME} -- logical type
1.367 - @{type_abbrev NAME} -- type abbreviation
1.368 - @{nonterminal NAME} -- type of concrete syntactic category
1.369 - @{type_syntax NAME} -- syntax representation of any of the above
1.370 -
1.371 - @{const_name NAME} -- logical constant (INCOMPATIBILITY)
1.372 - @{const_abbrev NAME} -- abbreviated constant
1.373 - @{const_syntax NAME} -- syntax representation of any of the above
1.374 -
1.375 -* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
1.376 -syntax constant (cf. 'syntax' command).
1.377 -
1.378 -* Antiquotation @{make_string} inlines a function to print arbitrary
1.379 -values similar to the ML toplevel. The result is compiler dependent
1.380 -and may fall back on "?" in certain situations.
1.381 -
1.382 -* Diagnostic commands 'ML_val' and 'ML_command' may refer to
1.383 -antiquotations @{Isar.state} and @{Isar.goal}. This replaces impure
1.384 -Isar.state() and Isar.goal(), which belong to the old TTY loop and do
1.385 -not work with the asynchronous Isar document model.
1.386 -
1.387 * Sorts.certify_sort and derived "cert" operations for types and terms
1.388 no longer minimize sorts. Thus certification at the boundary of the
1.389 inference kernel becomes invariant under addition of class relations,
1.390 @@ -586,15 +607,17 @@
1.391 to emphasize that these only work in a global situation (which is
1.392 quite rare).
1.393
1.394 -* Configuration options now admit dynamic default values, depending on
1.395 -the context or even global references.
1.396 -
1.397 -* SHA1.digest digests strings according to SHA-1 (see RFC 3174). It
1.398 -uses an efficient external library if available (for Poly/ML).
1.399 -
1.400 * Curried take and drop in library.ML; negative length is interpreted
1.401 as infinity (as in chop). Subtle INCOMPATIBILITY.
1.402
1.403 +* Proof terms: type substitutions on proof constants now use canonical
1.404 +order of type variables. INCOMPATIBILITY for tools working with proof
1.405 +terms.
1.406 +
1.407 +* Raw axioms/defs may no longer carry sort constraints, and raw defs
1.408 +may no longer carry premises. User-level specifications are
1.409 +transformed accordingly by Thm.add_axiom/add_def.
1.410 +
1.411
1.412 *** System ***
1.413