405 Concrete syntax is attached to specified constants in internal form, |
407 Concrete syntax is attached to specified constants in internal form, |
406 independently of name spaces. The parse tree representation is |
408 independently of name spaces. The parse tree representation is |
407 slightly different -- use 'notation' instead of raw 'syntax', and |
409 slightly different -- use 'notation' instead of raw 'syntax', and |
408 'translations' with explicit "CONST" markup to accommodate this. |
410 'translations' with explicit "CONST" markup to accommodate this. |
409 |
411 |
410 * Pure/Isar: unified syntax for new-style specification mechanisms (e.g. |
412 * Pure/Isar: unified syntax for new-style specification mechanisms |
411 'definition', 'abbreviation', or 'inductive' in HOL) admits full type |
413 (e.g. 'definition', 'abbreviation', or 'inductive' in HOL) admits |
412 inference and dummy patterns ("_"). For example: |
414 full type inference and dummy patterns ("_"). For example: |
413 |
415 |
414 definition "K x _ = x" |
416 definition "K x _ = x" |
415 |
417 |
416 inductive conj for A B |
418 inductive conj for A B |
417 where "A ==> B ==> conj A B" |
419 where "A ==> B ==> conj A B" |
418 |
420 |
419 * Pure: command 'print_abbrevs' prints all constant abbreviations of |
421 * Pure: command 'print_abbrevs' prints all constant abbreviations of |
420 the current context. Print mode "no_abbrevs" prevents inversion of |
422 the current context. Print mode "no_abbrevs" prevents inversion of |
421 abbreviations on output. |
423 abbreviations on output. |
422 |
424 |
423 * Isar/locales: improved parameter handling: |
425 * Isar/locales: improved parameter handling: use of locales "var" and |
424 - use of locales "var" and "struct" no longer necessary; |
426 "struct" no longer necessary; - parameter renamings are no longer |
425 - parameter renamings are no longer required to be injective. |
427 required to be injective. For example, this allows to define |
426 This enables, for example, to define a locale for endomorphisms thus: |
428 endomorphisms as locale endom = homom mult mult h. |
427 locale endom = homom mult mult h. |
|
428 |
429 |
429 * Isar/locales: changed the way locales with predicates are defined. |
430 * Isar/locales: changed the way locales with predicates are defined. |
430 Instead of accumulating the specification, the imported expression is |
431 Instead of accumulating the specification, the imported expression is |
431 now an interpretation. INCOMPATIBILITY: different normal form of |
432 now an interpretation. INCOMPATIBILITY: different normal form of |
432 locale expressions. In particular, in interpretations of locales with |
433 locale expressions. In particular, in interpretations of locales with |
451 concepts already existing in the target context. Example: |
452 concepts already existing in the target context. Example: |
452 |
453 |
453 interpretation partial_order ["op <= :: [int, int] => bool"] |
454 interpretation partial_order ["op <= :: [int, int] => bool"] |
454 where "partial_order.less (op <=) (x::int) y = (x < y)" |
455 where "partial_order.less (op <=) (x::int) y = (x < y)" |
455 |
456 |
456 Typically, the constant `partial_order.less' is created by a definition |
457 Typically, the constant `partial_order.less' is created by a |
457 specification element in the context of locale partial_order. |
458 definition specification element in the context of locale |
458 |
459 partial_order. |
459 * Provers/induct: improved internal context management to support local |
460 |
460 fixes and defines on-the-fly. Thus explicit meta-level connectives !! |
461 * Provers/induct: improved internal context management to support |
461 and ==> are rarely required anymore in inductive goals (using |
462 local fixes and defines on-the-fly. Thus explicit meta-level |
462 object-logic connectives for this purpose has been long obsolete |
463 connectives !! and ==> are rarely required anymore in inductive goals |
463 anyway). Common proof patterns are explained in |
464 (using object-logic connectives for this purpose has been long |
|
465 obsolete anyway). Common proof patterns are explained in |
464 HOL/Induct/Common_Patterns.thy, see also HOL/Isar_examples/Puzzle.thy |
466 HOL/Induct/Common_Patterns.thy, see also HOL/Isar_examples/Puzzle.thy |
465 and src/HOL/Lambda for realistic examples. |
467 and src/HOL/Lambda for realistic examples. |
466 |
468 |
467 * Provers/induct: improved handling of simultaneous goals. Instead of |
469 * Provers/induct: improved handling of simultaneous goals. Instead of |
468 introducing object-level conjunction, the statement is now split into |
470 introducing object-level conjunction, the statement is now split into |
469 several conclusions, while the corresponding symbolic cases are nested |
471 several conclusions, while the corresponding symbolic cases are nested |
470 accordingly. INCOMPATIBILITY, proofs need to be structured explicitly, |
472 accordingly. INCOMPATIBILITY, proofs need to be structured explicitly, |
471 see HOL/Induct/Common_Patterns.thy, for example. |
473 see HOL/Induct/Common_Patterns.thy, for example. |
472 |
474 |
473 * Provers/induct: mutual induction rules are now specified as a list of |
475 * Provers/induct: mutual induction rules are now specified as a list |
474 rule sharing the same induction cases. HOL packages usually provide |
476 of rule sharing the same induction cases. HOL packages usually provide |
475 foo_bar.inducts for mutually defined items foo and bar (e.g. inductive |
477 foo_bar.inducts for mutually defined items foo and bar (e.g. inductive |
476 sets or datatypes). INCOMPATIBILITY, users need to specify mutual |
478 sets or datatypes). INCOMPATIBILITY, users need to specify mutual |
477 induction rules differently, i.e. like this: |
479 induction rules differently, i.e. like this: |
478 |
480 |
479 (induct rule: foo_bar.inducts) |
481 (induct rule: foo_bar.inducts) |
519 for example "A -> B" => "Pi A (%_. B)". |
521 for example "A -> B" => "Pi A (%_. B)". |
520 |
522 |
521 * Pure: 'class_deps' command visualizes the subclass relation, using |
523 * Pure: 'class_deps' command visualizes the subclass relation, using |
522 the graph browser tool. |
524 the graph browser tool. |
523 |
525 |
524 * Pure: 'print_theory' now suppresses entities with internal name |
526 * Pure: 'print_theory' now suppresses certain internal declarations by |
525 (trailing "_") by default; use '!' option for full details. |
527 default; use '!' option for full details. |
526 |
528 |
527 |
529 |
528 *** HOL *** |
530 *** HOL *** |
529 |
531 |
530 * Internal reorganisation of `size' of datatypes: |
532 * Internal reorganisation of `size' of datatypes: size theorems |
531 - size theorems "foo.size" are no longer subsumed by "foo.simps" (but are still |
533 "foo.size" are no longer subsumed by "foo.simps" (but are still |
532 simplification rules by default!) |
534 simplification rules by default!); theorems "prod.size" now named |
533 - theorems "prod.size" now named "*.size" |
535 "*.size" |
534 |
536 |
535 * The transitivity reasoner for partial and linear orders is set up for |
537 * The transitivity reasoner for partial and linear orders is set up |
536 locales `order' and `linorder' generated by the new class package. Previously |
538 for locales "order" and "linorder" generated by the new class package |
537 the reasoner was only set up for axiomatic type classes. Instances of the |
539 (instead of axiomatic type classes used before). Instances of the |
538 reasoner are available in all contexts importing or interpreting these locales. |
540 reasoner are available in all contexts importing or interpreting these |
539 The following functionality is provided: |
541 locales. Method "order" invokes the reasoner separately; the reasoner |
540 - method `order' to invoke the reasoner manually. |
542 is also integrated with the Simplifier as a solver. Diagnostic |
541 - diagnostic command `print_orders' shows which instances of the reasoner are |
543 command 'print_orders' shows the available instances of the reasoner |
542 available in the current context. |
544 in the current context. |
543 As previously, the reasoner is integrated with the simplifier as a solver. |
545 |
544 |
546 * Formulation of theorem "dense" changed slightly due to integration |
545 * Formulation of theorem "dense" changed slightly due to integration with new |
547 with new class dense_linear_order. |
546 class dense_linear_order. |
548 |
547 |
549 * HOL/Finite_Set: "name-space" locales Lattice, Distrib_lattice, |
548 * theory Finite_Set: "name-space" locales Lattice, Distrib_lattice, Linorder etc. |
550 Linorder etc. have disappeared; operations defined in terms of |
549 have disappeared; operations defined in terms of fold_set now are named |
551 fold_set now are named Inf_fin, Sup_fin. INCOMPATIBILITY. |
550 Inf_fin, Sup_fin. INCOMPATIBILITY. |
552 |
551 |
553 * HOL-Word: New extensive library and type for generic, fixed size |
552 * HOL-Word: |
554 machine words, with arithemtic, bit-wise, shifting and rotating |
553 New extensive library and type for generic, fixed size machine |
555 operations, reflection into int, nat, and bool lists, automation for |
554 words, with arithemtic, bit-wise, shifting and rotating operations, |
556 linear arithmetic (by automatic reflection into nat or int), including |
555 reflection into int, nat, and bool lists, automation for linear |
557 lemmas on overflow and monotonicity. Instantiated to all appropriate |
556 arithmetic (by automatic reflection into nat or int), including |
558 arithmetic type classes, supporting automatic simplification of |
557 lemmas on overflow and monotonicity. Instantiated to all appropriate |
559 numerals on all operations. |
558 arithmetic type classes, supporting automatic simplification of |
|
559 numerals on all operations. Jointly developed by NICTA, Galois, and |
|
560 PSU. |
|
561 |
560 |
562 * Library/Boolean_Algebra: locales for abstract boolean algebras. |
561 * Library/Boolean_Algebra: locales for abstract boolean algebras. |
563 |
562 |
564 * Library/Numeral_Type: numbers as types, e.g. TYPE(32). |
563 * Library/Numeral_Type: numbers as types, e.g. TYPE(32). |
565 |
564 |
566 * Code generator library theories: |
565 * Code generator library theories: |
567 * Pretty_Int represents HOL integers by big integer literals in target |
566 - Pretty_Int represents HOL integers by big integer literals in target |
568 languages. |
567 languages. |
569 * Pretty_Char represents HOL characters by character literals in target |
568 - Pretty_Char represents HOL characters by character literals in target |
570 languages. |
569 languages. |
571 * Pretty_Char_chr like Pretty_Char, but also offers treatment of character |
570 - Pretty_Char_chr like Pretty_Char, but also offers treatment of character |
572 codes; includes Pretty_Int. |
571 codes; includes Pretty_Int. |
573 * Executable_Set allows to generate code for finite sets using lists. |
572 - Executable_Set allows to generate code for finite sets using lists. |
574 * Executable_Rat implements rational numbers as triples (sign, enumerator, |
573 - Executable_Rat implements rational numbers as triples (sign, enumerator, |
575 denominator). |
574 denominator). |
576 * Executable_Real implements a subset of real numbers, namly those |
575 - Executable_Real implements a subset of real numbers, namly those |
577 representable by rational numbers. |
576 representable by rational numbers. |
578 * Efficient_Nat implements natural numbers by integers, which in general will |
577 - Efficient_Nat implements natural numbers by integers, which in general will |
579 result in higher efficency; pattern matching with 0/Suc is eliminated; |
578 result in higher efficency; pattern matching with 0/Suc is eliminated; |
580 includes Pretty_Int. |
579 includes Pretty_Int. |
581 * ML_String provides an additional datatype ml_string; in the HOL default |
580 - ML_String provides an additional datatype ml_string; in the HOL default |
582 setup, strings in HOL are mapped to lists of HOL characters in SML; values |
581 setup, strings in HOL are mapped to lists of HOL characters in SML; values |
583 of type ml_string are mapped to strings in SML. |
582 of type ml_string are mapped to strings in SML. |
584 * ML_Int provides an additional datatype ml_int which is mapped to to SML |
583 - ML_Int provides an additional datatype ml_int which is mapped to to SML |
585 built-in integers. |
584 built-in integers. |
586 |
585 |
587 * New package for inductive predicates |
586 * New package for inductive predicates |
588 |
587 |
589 An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via |
588 An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via |
628 | rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n" |
627 | rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n" |
629 | ... |
628 | ... |
630 |
629 |
631 if the additional syntax "p ..." is required. |
630 if the additional syntax "p ..." is required. |
632 |
631 |
633 Many examples can be found in the subdirectories Auth, Bali, Induct, |
632 Numerous examples can be found in the subdirectories HOL/Auth, HOL/Bali, |
634 or MicroJava. |
633 HOL/Induct, and HOL/MicroJava. |
635 |
634 |
636 INCOMPATIBILITIES: |
635 INCOMPATIBILITIES: |
637 |
636 |
638 - Since declaration and definition of inductive sets or predicates |
637 - Since declaration and definition of inductive sets or predicates |
639 is no longer separated, abbreviations involving the newly introduced |
638 is no longer separated, abbreviations involving the newly |
640 sets or predicates must be specified together with the introduction |
639 introduced sets or predicates must be specified together with the |
641 rules after the "where" keyword (see example above), rather than before |
640 introduction rules after the 'where' keyword (see above), rather |
642 the actual inductive definition. |
641 than before the actual inductive definition. |
643 |
642 |
644 - The variables in induction and elimination rules are now quantified |
643 - The variables in induction and elimination rules are now |
645 in the order of their occurrence in the introduction rules, rather than |
644 quantified in the order of their occurrence in the introduction |
646 in alphabetical order. Since this may break some proofs, these proofs |
645 rules, rather than in alphabetical order. Since this may break |
647 either have to be repaired, e.g. by reordering the variables |
646 some proofs, these proofs either have to be repaired, e.g. by |
648 a_i_1 ... a_i_{k_i} in Isar "case" statements of the form |
647 reordering the variables a_i_1 ... a_i_{k_i} in Isar 'case' |
|
648 statements of the form |
649 |
649 |
650 case (rule_i a_i_1 ... a_i_{k_i}) |
650 case (rule_i a_i_1 ... a_i_{k_i}) |
651 |
651 |
652 or the old order of quantification has to be restored by explicitly adding |
652 or the old order of quantification has to be restored by explicitly adding |
653 meta-level quantifiers in the introduction rules, i.e. |
653 meta-level quantifiers in the introduction rules, i.e. |
670 |
670 |
671 x : s z_1 ... z_m ==> |
671 x : s z_1 ... z_m ==> |
672 (!!a_1_1 ... a_1_{k_1}. x = (t_1_1, ..., t_1_n) ==> ... ==> P) |
672 (!!a_1_1 ... a_1_{k_1}. x = (t_1_1, ..., t_1_n) ==> ... ==> P) |
673 ==> ... ==> P |
673 ==> ... ==> P |
674 |
674 |
675 This may require terms in goals to be expanded to n-tuples (e.g. using case_tac |
675 This may require terms in goals to be expanded to n-tuples |
676 or simplification with the split_paired_all rule) before the above elimination |
676 (e.g. using case_tac or simplification with the split_paired_all |
677 rule is applicable. |
677 rule) before the above elimination rule is applicable. |
678 |
678 |
679 - The elimination or case analysis rules for (mutually) inductive sets or |
679 - The elimination or case analysis rules for (mutually) inductive |
680 predicates are now called "p_1.cases" ... "p_k.cases". The list of rules |
680 sets or predicates are now called "p_1.cases" ... "p_k.cases". The |
681 "p_1_..._p_k.elims" is no longer available. |
681 list of rules "p_1_..._p_k.elims" is no longer available. |
682 |
682 |
683 * Method "metis" proves goals by applying the Metis general-purpose |
683 * Method "metis" proves goals by applying the Metis general-purpose |
684 resolution prover. Examples are in the directory MetisExamples. See |
684 resolution prover. Examples are in the directory MetisExamples. See |
685 also http://gilith.com/software/metis/ |
685 also http://gilith.com/software/metis/ |
|
686 |
|
687 WARNING: the Isabelle/HOL-Metis integration does not yet work properly |
|
688 with multi-threading. |
686 |
689 |
687 * Command 'sledgehammer' invokes external automatic theorem provers as |
690 * Command 'sledgehammer' invokes external automatic theorem provers as |
688 background processes. It generates calls to the "metis" method if |
691 background processes. It generates calls to the "metis" method if |
689 successful. These can be pasted into the proof. Users do not have to |
692 successful. These can be pasted into the proof. Users do not have to |
690 wait for the automatic provers to return. |
693 wait for the automatic provers to return. |
691 |
694 |
692 * Case-expressions allow arbitrary constructor-patterns (including "_") and |
695 * Case-expressions allow arbitrary constructor-patterns (including |
693 take their order into account, like in functional programming. |
696 "_") and take their order into account, like in functional |
694 Internally, this is translated into nested case-expressions; missing cases |
697 programming. Internally, this is translated into nested |
695 are added and mapped to the predefined constant "undefined". In complicated |
698 case-expressions; missing cases are added and mapped to the predefined |
696 cases printing may no longer show the original input but the internal |
699 constant "undefined". In complicated cases printing may no longer show |
697 form. Lambda-abstractions allow the same form of pattern matching: |
700 the original input but the internal form. Lambda-abstractions allow |
698 "% pat1 => e1 | ..." is an abbreviation for |
701 the same form of pattern matching: "% pat1 => e1 | ..." is an |
699 "%x. case x of pat1 => e1 | ..." where x is a new variable. |
702 abbreviation for "%x. case x of pat1 => e1 | ..." where x is a new |
|
703 variable. |
700 |
704 |
701 * IntDef: The constant "int :: nat => int" has been removed; now "int" |
705 * IntDef: The constant "int :: nat => int" has been removed; now "int" |
702 is an abbreviation for "of_nat :: nat => int". The simplification rules |
706 is an abbreviation for "of_nat :: nat => int". The simplification |
703 for "of_nat" have been changed to work like "int" did previously. |
707 rules for "of_nat" have been changed to work like "int" did |
704 (potential INCOMPATIBILITY) |
708 previously. Potential INCOMPATIBILITY: |
705 - "of_nat (Suc m)" simplifies to "1 + of_nat m" instead of "of_nat m + 1" |
709 - "of_nat (Suc m)" simplifies to "1 + of_nat m" instead of "of_nat m + 1" |
706 - of_nat_diff and of_nat_mult are no longer default simp rules |
710 - of_nat_diff and of_nat_mult are no longer default simp rules |
707 |
711 |
708 * Method "algebra" solves polynomial equations over (semi)rings using |
712 * Method "algebra" solves polynomial equations over (semi)rings using |
709 Groebner bases. The (semi)ring structure is defined by locales and |
713 Groebner bases. The (semi)ring structure is defined by locales and the |
710 the tool setup depends on that generic context. Installing the |
714 tool setup depends on that generic context. Installing the method for |
711 method for a specific type involves instantiating the locale and |
715 a specific type involves instantiating the locale and possibly adding |
712 possibly adding declarations for computation on the coefficients. |
716 declarations for computation on the coefficients. The method is |
713 The method is already instantiated for natural numbers and for the |
717 already instantiated for natural numbers and for the axiomatic class |
714 axiomatic class of idoms with numerals. See also the paper by |
718 of idoms with numerals. See also the paper by Chaieb and Wenzel at |
715 Chaieb and Wenzel at CALCULEMUS 2007 for the general principles |
719 CALCULEMUS 2007 for the general principles underlying this |
716 underlying this architecture of context-aware proof-tools. |
720 architecture of context-aware proof-tools. |
717 |
721 |
718 * constant "List.op @" now named "List.append". Use ML antiquotations |
722 * Former constant "List.op @" now named "List.append". Use ML |
719 @{const_name List.append} or @{term " ... @ ... "} to circumvent |
723 antiquotations @{const_name List.append} or @{term " ... @ ... "} to |
720 possible incompatibilities when working on ML level. |
724 circumvent possible incompatibilities when working on ML level. |
721 |
725 |
722 * Constant renames due to introduction of canonical name prefixing for |
726 * Some renaming of class constants due to canonical name prefixing in |
723 class package: |
727 the new 'class' package: |
724 |
728 |
725 HOL.abs ~> HOL.minus_class.abs |
729 HOL.abs ~> HOL.minus_class.abs |
726 HOL.divide ~> HOL.divide_class.divide |
730 HOL.divide ~> HOL.divide_class.divide |
727 Nat.power ~> Nat.power_class.power |
731 Nat.power ~> Nat.power_class.power |
728 Nat.size ~> Nat.size_class.size |
732 Nat.size ~> Nat.size_class.size |
729 Numeral.number_of ~> Numeral.number_class.number_of |
733 Numeral.number_of ~> Numeral.number_class.number_of |
730 FixedPoint.Inf ~> FixedPoint.complete_lattice_class.Inf |
734 FixedPoint.Inf ~> FixedPoint.complete_lattice_class.Inf |
731 FixedPoint.Sup ~> FixedPoint.complete_lattice_class.Sup |
735 FixedPoint.Sup ~> FixedPoint.complete_lattice_class.Sup |
732 |
|
733 * Rudimentary class target mechanism involves constant renames: |
|
734 |
|
735 Orderings.min ~> Orderings.ord_class.min |
736 Orderings.min ~> Orderings.ord_class.min |
736 Orderings.max ~> Orderings.ord_class.max |
737 Orderings.max ~> Orderings.ord_class.max |
737 |
738 |
|
739 * New class "default" with associated constant "default". |
|
740 |
|
741 * New constant "undefined" with axiom "undefined x = undefined". |
|
742 |
738 * primrec: missing cases mapped to "undefined" instead of "arbitrary" |
743 * primrec: missing cases mapped to "undefined" instead of "arbitrary" |
739 |
744 |
740 * new constant "undefined" with axiom "undefined x = undefined" |
745 * New function listsum :: 'a list => 'a for arbitrary monoids. |
741 |
746 Special syntax: "SUM x <- xs. f x" (and latex variants) |
742 * new class "default" with associated constant "default" |
747 |
743 |
748 * New syntax for Haskell-like list comprehension (input only), eg. |
744 * new function listsum :: 'a list => 'a for arbitrary monoids. |
749 [(x,y). x <- xs, y <- ys, x ~= y], see also HOL/List.thy. |
745 Special syntax: "SUM x <- xs. f x" (and latex variants) |
750 |
746 |
751 * The special syntax for function "filter" has changed from [x : |
747 * new (input only) syntax for Haskell-like list comprehension, eg |
752 xs. P] to [x <- xs. P] to avoid an ambiguity caused by list |
748 [(x,y). x <- xs, y <- ys, x ~= y] |
753 comprehension syntax, and for uniformity. INCOMPATIBILITY. |
749 For details see List.thy. |
754 |
750 |
755 * [a..b] is now defined for arbitrary linear orders. It used to be |
751 * The special syntax for function "filter" has changed from [x : xs. P] to |
756 defined on nat only, as an abbreviation for [a..<Suc b] |
752 [x <- xs. P] to avoid an ambiguity caused by list comprehension syntax, |
757 INCOMPATIBILITY. |
753 and for uniformity. INCOMPATIBILITY |
758 |
754 |
759 * Renamed lemma "set_take_whileD" to "set_takeWhileD". |
755 * [a..b] is now defined for arbitrary linear orders. |
760 |
756 It used to be defined on nat only, as an abbreviation for [a..<Suc b] |
761 * New functions "sorted" and "sort" in HOL/List.thy. |
757 INCOMPATIBILITY |
762 |
758 |
763 * Function "sgn" is now overloaded and available on int, real, complex |
759 * Lemma "set_take_whileD" renamed to "set_takeWhileD" |
764 (and other numeric types), using class "sgn". Two possible defs of |
760 |
765 sgn are given as equational assumptions in the classes sgn_if and |
761 * new functions sorted and sort in List. |
766 sgn_div_norm; ordered_idom now also inherits from sgn_if. |
762 |
767 INCOMPATIBILITY. |
763 * function "sgn" is now overloaded and available on int, real, complex |
768 |
764 (and other numeric types). |
769 * New lemma collection field_simps (an extension of ring_simps) for |
765 The details: new class "sgn" with function "sgn"; |
770 manipulating (in)equations involving division. Multiplies with all |
766 two possible defs of sgn in the classes sgn_if and sgn_div_norm |
771 denominators that can be proved to be non-zero (in equations) or |
767 (as equational assumptions); |
772 positive/negative (in inequations). |
768 ordered_idom now also inherits from sgn_if - INCOMPATIBILITY. |
|
769 |
|
770 * New lemma collection field_simps (an extension of ring_simps) |
|
771 for manipulating (in)equations involving division. Multiplies |
|
772 with all denominators that can be proved to be non-zero (in equations) |
|
773 or positive/negative (in inequations). |
|
774 |
773 |
775 * Lemma collections ring_eq_simps, group_eq_simps and ring_distrib |
774 * Lemma collections ring_eq_simps, group_eq_simps and ring_distrib |
776 have been improved and renamed to ring_simps, group_simps and ring_distribs. |
775 have been improved and renamed to ring_simps, group_simps and |
777 Removed lemmas field_xyz in Ring_and_Field |
776 ring_distribs. Removed lemmas field_xyz in theory Ring_and_Field |
778 because they were subsumed by lemmas xyz. |
777 because they were subsumed by lemmas xyz. INCOMPATIBILITY. |
779 INCOMPATIBILITY. |
778 |
780 |
779 * Library/Pretty_Int.thy: maps HOL numerals on target language integer |
781 * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals |
780 literals when generating code. |
782 when generating code. |
781 |
783 |
782 * Library/Pretty_Char.thy: maps HOL characters on target language |
784 * Library/Pretty_Char.thy: maps HOL characters on target language character literals |
783 character literals when generating code. |
785 when generating code. |
784 |
786 |
785 * Library/Commutative_Ring.thy: switched from recdef to function |
787 * Library/Commutative_Ring.thy: switched from recdef to function package; |
786 package; constants add, mul, pow now curried. Infix syntax for |
788 constants add, mul, pow now curried. Infix syntax for algebraic operations. |
787 algebraic operations. |
789 |
788 |
790 * Some steps towards more uniform lattice theory development in HOL. |
789 * Some steps towards more uniform lattice theory development in HOL. |
791 |
790 |
792 constants "meet" and "join" now named "inf" and "sup" |
791 constants "meet" and "join" now named "inf" and "sup" |
793 constant "Meet" now named "Inf" |
792 constant "Meet" now named "Inf" |
901 listsp_meet_eq ~> listsp_inf_eq |
900 listsp_meet_eq ~> listsp_inf_eq |
902 |
901 |
903 meet_min ~> inf_min |
902 meet_min ~> inf_min |
904 join_max ~> sup_max |
903 join_max ~> sup_max |
905 |
904 |
906 * Classes "order" and "linorder": facts "refl", "trans" and |
905 * Renamed classes "order" and "linorder": facts "refl", "trans" and |
907 "cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to |
906 "cases" to "order_refl", "order_trans" and "linorder_cases", to avoid |
908 avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY. |
907 clashes with HOL "refl" and "trans". INCOMPATIBILITY. |
909 |
908 |
910 * Classes "order" and "linorder": |
909 * Classes "order" and "linorder": potential INCOMPATIBILITY due to |
911 potential INCOMPATIBILITY: order of proof goals in order/linorder instance |
910 changed order of proof goals instance proofs. |
912 proofs changed. |
911 |
913 |
912 * Dropped redundant lemma def_imp_eq in favor of meta_eq_to_obj_eq. |
914 * Dropped lemma duplicate def_imp_eq in favor of meta_eq_to_obj_eq. |
|
915 INCOMPATIBILITY. |
913 INCOMPATIBILITY. |
916 |
914 |
917 * Dropped lemma duplicate if_def2 in favor of if_bool_eq_conj. |
915 * Dropped redundant lemma if_def2 in favor of if_bool_eq_conj. |
918 INCOMPATIBILITY. |
916 INCOMPATIBILITY. |
919 |
917 |
920 * Added syntactic class "size"; overloaded constant "size" now has |
918 * Added syntactic class "size"; overloaded constant "size" now has |
921 type "'a::size ==> bool" |
919 type "'a::size ==> bool" |
922 |
920 |
923 * Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op |
921 * Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op |
924 dvd" to "Divides.div_class.div", "Divides.div_class.mod" and "Divides.dvd". INCOMPATIBILITY. |
922 dvd" to "Divides.div_class.div", "Divides.div_class.mod" and |
925 |
923 "Divides.dvd". INCOMPATIBILITY. |
926 * Added method "lexicographic_order" automatically synthesizes |
924 |
927 termination relations as lexicographic combinations of size measures |
925 * Method "lexicographic_order" automatically synthesizes termination |
928 -- 'function' package. |
926 relations as lexicographic combinations of size measures -- 'function' |
|
927 package. |
929 |
928 |
930 * HOL/records: generalised field-update to take a function on the |
929 * HOL/records: generalised field-update to take a function on the |
931 field rather than the new value: r(|A := x|) is translated to A_update |
930 field rather than the new value: r(|A := x|) is translated to A_update |
932 (K x) r The K-combinator that is internally used is called K_record. |
931 (K x) r The K-combinator that is internally used is called K_record. |
933 INCOMPATIBILITY: Usage of the plain update functions has to be |
932 INCOMPATIBILITY: Usage of the plain update functions has to be |
934 adapted. |
933 adapted. |
935 |
934 |
936 * axclass "semiring_0" now contains annihilation axioms x * 0 = 0 and |
935 * Class "semiring_0" now contains annihilation axioms x * 0 = 0 and 0 |
937 0 * x = 0, which are required for a semiring. Richer structures do |
936 * x = 0, which are required for a semiring. Richer structures do not |
938 not inherit from semiring_0 anymore, because this property is a |
937 inherit from semiring_0 anymore, because this property is a theorem |
939 theorem there, not an axiom. INCOMPATIBILITY: In instances of |
938 there, not an axiom. INCOMPATIBILITY: In instances of semiring_0, |
940 semiring_0, there is more to prove, but this is mostly trivial. |
939 there is more to prove, but this is mostly trivial. |
941 |
940 |
942 * axclass "recpower" was generalized to arbitrary monoids, not just |
941 * Class "recpower" is generalized to arbitrary monoids, not just |
943 commutative semirings. INCOMPATIBILITY: If you use recpower and need |
942 commutative semirings. INCOMPATIBILITY: may need to incorporate |
944 commutativity or a semiring property, add the corresponding classes. |
943 commutativity or a semiring properties additionally. |
945 |
944 |
946 * Unified locale partial_order with class definition (cf. theory |
945 * Unified locale "partial_order" with class definition (cf. theory |
947 Orderings), added parameter ``less''. INCOMPATIBILITY. |
946 Orderings), added parameter "less". INCOMPATIBILITY. |
948 |
947 |
949 * Constant "List.list_all2" in List.thy now uses authentic syntax. |
948 * Constant "List.list_all2" in List.thy now uses authentic syntax. |
950 INCOMPATIBILITY: translations containing list_all2 may go wrong. On |
949 INCOMPATIBILITY: translations containing list_all2 may go wrong, |
951 Isar level, use abbreviations instead. |
950 better use 'abbreviation'. |
952 |
951 |
953 * Renamed constant "List.op mem" to "List.memberl" INCOMPATIBILITY: |
952 * Renamed constant "List.op mem" to "List.member". INCOMPATIBILITY. |
954 rarely occuring name references (e.g. ``List.op mem.simps'') require |
953 |
955 renaming (e.g. ``List.memberl.simps''). |
954 * Renamed constants "0" to "HOL.zero_class.zero" and "1" to |
956 |
955 "HOL.one_class.one". INCOMPATIBILITY. |
957 * Renamed constants "0" to "HOL.zero_class.zero" and "1" to "HOL.one_class.one". |
956 |
958 INCOMPATIBILITY. |
957 * Added class "HOL.eq", allowing for code generation with polymorphic |
959 |
958 equality. |
960 * Added class "HOL.eq", allowing for code generation with polymorphic equality. |
|
961 |
959 |
962 * Numeral syntax: type 'bin' which was a mere type copy of 'int' has |
960 * Numeral syntax: type 'bin' which was a mere type copy of 'int' has |
963 been abandoned in favour of plain 'int'. INCOMPATIBILITY -- |
961 been abandoned in favour of plain 'int'. INCOMPATIBILITY -- |
964 significant changes for setting up numeral syntax for types: |
962 significant changes for setting up numeral syntax for types: |
965 |
963 - New constants Numeral.pred and Numeral.succ instead |
966 - new constants Numeral.pred and Numeral.succ instead |
|
967 of former Numeral.bin_pred and Numeral.bin_succ. |
964 of former Numeral.bin_pred and Numeral.bin_succ. |
968 - Use integer operations instead of bin_add, bin_mult and so on. |
965 - Use integer operations instead of bin_add, bin_mult and so on. |
969 - Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps. |
966 - Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps. |
970 - ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs. |
967 - ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs. |
971 |
968 |
972 See HOL/Integ/IntArith.thy for an example setup. |
969 See HOL/Integ/IntArith.thy for an example setup. |
973 |
970 |
974 * New top level command 'normal_form' computes the normal form of a |
971 * New top level command 'normal_form' computes the normal form of a |
975 term that may contain free variables. For example ``normal_form |
972 term that may contain free variables. For example ``normal_form |
976 "rev[a,b,c]"'' produces ``[b,c,a]'' (without proof). This command is |
973 "rev[a,b,c]"'' produces ``[b,c,a]'' (without proof). This command is |
977 suitable for heavy-duty computations because the functions are |
974 suitable for heavy-duty computations because the functions are |
978 compiled to ML first. |
975 compiled to ML first. |
979 |
976 |
980 * Alternative iff syntax "A <-> B" for equality on bool (with priority |
977 * Alternative iff syntax "A <-> B" for equality on bool (with priority |
990 op < ~> HOL.ord_class.less |
987 op < ~> HOL.ord_class.less |
991 op <= ~> HOL.ord_class.less_eq |
988 op <= ~> HOL.ord_class.less_eq |
992 |
989 |
993 Adaptions may be required in the following cases: |
990 Adaptions may be required in the following cases: |
994 |
991 |
995 a) User-defined constants using any of the names "plus", "minus", "times", |
992 a) User-defined constants using any of the names "plus", "minus", |
996 "less" or "less_eq". The standard syntax translations for "+", "-" and "*" |
993 "times", "less" or "less_eq". The standard syntax translations for |
997 may go wrong. |
994 "+", "-" and "*" may go wrong. INCOMPATIBILITY: use more specific |
998 INCOMPATIBILITY: use more specific names. |
995 names. |
999 |
996 |
1000 b) Variables named "plus", "minus", "times", "less", "less_eq" |
997 b) Variables named "plus", "minus", "times", "less", "less_eq" |
1001 INCOMPATIBILITY: use more specific names. |
998 INCOMPATIBILITY: use more specific names. |
1002 |
999 |
1003 c) Permutative equations (e.g. "a + b = b + a") |
1000 c) Permutative equations (e.g. "a + b = b + a") |
1004 Since the change of names also changes the order of terms, permutative |
1001 Since the change of names also changes the order of terms, permutative |
1005 rewrite rules may get applied in a different order. Experience shows that |
1002 rewrite rules may get applied in a different order. Experience shows |
1006 this is rarely the case (only two adaptions in the whole Isabelle |
1003 that this is rarely the case (only two adaptions in the whole Isabelle |
1007 distribution). |
1004 distribution). INCOMPATIBILITY: rewrite proofs |
1008 INCOMPATIBILITY: rewrite proofs |
|
1009 |
1005 |
1010 d) ML code directly refering to constant names |
1006 d) ML code directly refering to constant names |
1011 This in general only affects hand-written proof tactics, simprocs and so on. |
1007 This in general only affects hand-written proof tactics, simprocs and |
1012 INCOMPATIBILITY: grep your sourcecode and replace names. Consider use |
1008 so on. INCOMPATIBILITY: grep your sourcecode and replace names. |
1013 of const_name ML antiquotations. |
1009 Consider using @{const_name} antiquotation. |
1014 |
1010 |
1015 * Relations less (<) and less_eq (<=) are also available on type bool. |
1011 * Relations less (<) and less_eq (<=) are also available on type bool. |
1016 Modified syntax to disallow nesting without explicit parentheses, |
1012 Modified syntax to disallow nesting without explicit parentheses, |
1017 e.g. "(x < y) < z" or "x < (y < z)", but NOT "x < y < z". |
1013 e.g. "(x < y) < z" or "x < (y < z)", but NOT "x < y < z". Potential |
|
1014 INCOMPATIBILITY. |
1018 |
1015 |
1019 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only). |
1016 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only). |
1020 |
1017 |
1021 * Relation composition operator "op O" now has precedence 75 and binds |
1018 * Relation composition operator "op O" now has precedence 75 and binds |
1022 stronger than union and intersection. INCOMPATIBILITY. |
1019 stronger than union and intersection. INCOMPATIBILITY. |
1023 |
1020 |
1024 * The old set interval syntax "{m..n(}" (and relatives) has been |
1021 * The old set interval syntax "{m..n(}" (and relatives) has been |
1025 removed. Use "{m..<n}" (and relatives) instead. |
1022 removed. Use "{m..<n}" (and relatives) instead. |
1026 |
1023 |
1027 * In the context of the assumption "~(s = t)" the Simplifier rewrites |
1024 * In the context of the assumption "~(s = t)" the Simplifier rewrites |
1028 "t = s" to False (by simproc "neq_simproc"). For backward |
1025 "t = s" to False (by simproc "neq"). INCOMPATIBILITY, consider using |
1029 compatibility this can be disabled by ML "reset use_neq_simproc". |
1026 ``declare [[simproc del: neq]]''. |
1030 |
1027 |
1031 * "m dvd n" where m and n are numbers is evaluated to True/False by |
1028 * Simplifier: "m dvd n" where m and n are numbers is evaluated to |
1032 simp. |
1029 True/False. |
1033 |
1030 |
1034 * Theorem Cons_eq_map_conv no longer declared as ``simp''. |
1031 * Theorem Cons_eq_map_conv no longer declared as "simp". |
1035 |
1032 |
1036 * Theorem setsum_mult renamed to setsum_right_distrib. |
1033 * Theorem setsum_mult renamed to setsum_right_distrib. |
1037 |
1034 |
1038 * Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the |
1035 * Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the |
1039 ``rule'' method. |
1036 ``rule'' method. |
1040 |
1037 |
1041 * Reimplemented methods ``sat'' and ``satx'', with several |
1038 * Reimplemented methods "sat" and "satx", with several improvements: |
1042 improvements: goals no longer need to be stated as "<prems> ==> |
1039 goals no longer need to be stated as "<prems> ==> False", equivalences |
1043 False", equivalences (i.e. "=" on type bool) are handled, variable |
1040 (i.e. "=" on type bool) are handled, variable names of the form |
1044 names of the form "lit_<n>" are no longer reserved, significant |
1041 "lit_<n>" are no longer reserved, significant speedup. |
1045 speedup. |
1042 |
1046 |
1043 * Methods "sat" and "satx" can now replay MiniSat proof traces. |
1047 * Methods ``sat'' and ``satx'' can now replay MiniSat proof traces. |
|
1048 zChaff is still supported as well. |
1044 zChaff is still supported as well. |
1049 |
1045 |
1050 * 'inductive' and 'datatype': provide projections of mutual rules, |
1046 * 'inductive' and 'datatype': provide projections of mutual rules, |
1051 bundled as foo_bar.inducts; |
1047 bundled as foo_bar.inducts; |
1052 |
1048 |
1108 * Renamed theory CRing to Ring. |
1105 * Renamed theory CRing to Ring. |
1109 |
1106 |
1110 |
1107 |
1111 *** HOL-Complex *** |
1108 *** HOL-Complex *** |
1112 |
1109 |
1113 * Theory Real: new method ferrack implements quantifier elimination |
|
1114 for linear arithmetic over the reals. The quantifier elimination |
|
1115 feature is used only for decision, for compatibility with arith. This |
|
1116 means a goal is either solved or left unchanged, no simplification. |
|
1117 |
|
1118 * Hyperreal: Functions root and sqrt are now defined on negative real |
1110 * Hyperreal: Functions root and sqrt are now defined on negative real |
1119 inputs so that root n (- x) = - root n x and sqrt (- x) = - sqrt x. |
1111 inputs so that root n (- x) = - root n x and sqrt (- x) = - sqrt x. |
1120 Nonnegativity side conditions have been removed from many lemmas, so |
1112 Nonnegativity side conditions have been removed from many lemmas, so |
1121 that more subgoals may now be solved by simplification; potential |
1113 that more subgoals may now be solved by simplification; potential |
1122 INCOMPATIBILITY. |
1114 INCOMPATIBILITY. |
1123 |
1115 |
1124 * Real: New axiomatic classes formalize real normed vector spaces and |
1116 * Real: new type classes formalize real normed vector spaces and |
1125 algebras, using new overloaded constants scaleR :: real => 'a => 'a |
1117 algebras, using new overloaded constants scaleR :: real => 'a => 'a |
1126 and norm :: 'a => real. |
1118 and norm :: 'a => real. |
1127 |
1119 |
1128 * Real: New constant of_real :: real => 'a::real_algebra_1 injects |
1120 * Real: constant of_real :: real => 'a::real_algebra_1 injects from |
1129 from reals into other types. The overloaded constant Reals :: 'a set |
1121 reals into other types. The overloaded constant Reals :: 'a set is now |
1130 is now defined as range of_real; potential INCOMPATIBILITY. |
1122 defined as range of_real; potential INCOMPATIBILITY. |
1131 |
1123 |
1132 * Real: ML code generation is supported now and hence also quickcheck. |
1124 * Real: proper support for ML code generation, including 'quickcheck'. |
1133 Reals are implemented as arbitrary precision rationals. |
1125 Reals are implemented as arbitrary precision rationals. |
1134 |
1126 |
1135 * Hyperreal: Several constants that previously worked only for the |
1127 * Hyperreal: Several constants that previously worked only for the |
1136 reals have been generalized, so they now work over arbitrary vector |
1128 reals have been generalized, so they now work over arbitrary vector |
1137 spaces. Type annotations may need to be added in some cases; potential |
1129 spaces. Type annotations may need to be added in some cases; potential |
1206 The same works for sources being ``used'' within an Isar context. |
1193 The same works for sources being ``used'' within an Isar context. |
1207 |
1194 |
1208 * ML in Isar: improved error reporting; extra verbosity with |
1195 * ML in Isar: improved error reporting; extra verbosity with |
1209 ML_Context.trace enabled. |
1196 ML_Context.trace enabled. |
1210 |
1197 |
1211 * Pure/library: |
|
1212 |
|
1213 val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list |
|
1214 val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd |
|
1215 |
|
1216 The semantics of "burrow" is: "take a function with *simulatanously* |
|
1217 transforms a list of value, and apply it *simulatanously* to a list of |
|
1218 list of values of the appropriate type". Compare this with "map" which |
|
1219 would *not* apply its argument function simulatanously but in |
|
1220 sequence; "fold_burrow" has an additional context. |
|
1221 |
|
1222 * Pure/library: indexed lists - some functions in the Isabelle library |
|
1223 treating lists over 'a as finite mappings from [0...n] to 'a have been |
|
1224 given more convenient names and signatures reminiscent of similar |
|
1225 functions for alists, tables, etc: |
|
1226 |
|
1227 val nth: 'a list -> int -> 'a |
|
1228 val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list |
|
1229 val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b |
|
1230 |
|
1231 Note that fold_index starts counting at index 0, not 1 like foldln |
|
1232 used to. |
|
1233 |
|
1234 * Pure/General/table.ML: the join operations now works via exceptions |
1198 * Pure/General/table.ML: the join operations now works via exceptions |
1235 DUP/SAME instead of type option. This is simpler in simple cases, and |
1199 DUP/SAME instead of type option. This is simpler in simple cases, and |
1236 admits slightly more efficient complex applications. |
1200 admits slightly more efficient complex applications. |
1237 |
1201 |
|
1202 * Pure: 'advanced' translation functions (parse_translation etc.) now |
|
1203 use Context.generic instead of just theory. |
|
1204 |
1238 * Pure: datatype Context.generic joins theory/Proof.context and |
1205 * Pure: datatype Context.generic joins theory/Proof.context and |
1239 provides some facilities for code that works in either kind of |
1206 provides some facilities for code that works in either kind of |
1240 context, notably GenericDataFun for uniform theory and proof data. |
1207 context, notably GenericDataFun for uniform theory and proof data. |
1241 |
|
1242 * Pure: 'advanced' translation functions (parse_translation etc.) now |
|
1243 use Context.generic instead of just theory. |
|
1244 |
1208 |
1245 * Pure: simplified internal attribute type, which is now always |
1209 * Pure: simplified internal attribute type, which is now always |
1246 Context.generic * thm -> Context.generic * thm. Global (theory) vs. |
1210 Context.generic * thm -> Context.generic * thm. Global (theory) vs. |
1247 local (Proof.context) attributes have been discontinued, while |
1211 local (Proof.context) attributes have been discontinued, while |
1248 minimizing code duplication. Thm.rule_attribute and |
1212 minimizing code duplication. Thm.rule_attribute and |
1249 Thm.declaration_attribute build canonical attributes; see also structure |
1213 Thm.declaration_attribute build canonical attributes; see also structure |
1250 Context for further operations on Context.generic, notably |
1214 Context for further operations on Context.generic, notably |
1251 GenericDataFun. INCOMPATIBILITY, need to adapt attribute type |
1215 GenericDataFun. INCOMPATIBILITY, need to adapt attribute type |
1252 declarations and definitions. |
1216 declarations and definitions. |
1253 |
1217 |
|
1218 * Context data interfaces (Theory/Proof/GenericDataFun): removed |
|
1219 name/print, uninitialized data defaults to ad-hoc copy of empty value, |
|
1220 init only required for impure data. INCOMPATIBILITY: empty really need |
|
1221 to be empty (no dependencies on theory content!) |
|
1222 |
1254 * Pure/kernel: consts certification ignores sort constraints given in |
1223 * Pure/kernel: consts certification ignores sort constraints given in |
1255 signature declarations. (This information is not relevant to the logic, |
1224 signature declarations. (This information is not relevant to the |
1256 but only for type inference.) IMPORTANT INTERNAL CHANGE, potential |
1225 logic, but only for type inference.) SIGNIFICANT INTERNAL CHANGE, |
1257 INCOMPATIBILITY. |
1226 potential INCOMPATIBILITY. |
1258 |
1227 |
1259 * Pure: axiomatic type classes are now purely definitional, with |
1228 * Pure: axiomatic type classes are now purely definitional, with |
1260 explicit proofs of class axioms and super class relations performed |
1229 explicit proofs of class axioms and super class relations performed |
1261 internally. See Pure/axclass.ML for the main internal interfaces -- |
1230 internally. See Pure/axclass.ML for the main internal interfaces -- |
1262 notably AxClass.define_class supercedes AxClass.add_axclass, and |
1231 notably AxClass.define_class supercedes AxClass.add_axclass, and |