13 * Theory syntax: the old non-Isar theory file format has been |
13 * Theory syntax: the old non-Isar theory file format has been |
14 discontinued altogether. Note that ML proof scripts may still be used |
14 discontinued altogether. Note that ML proof scripts may still be used |
15 with Isar theories; migration is usually quite simple with the ML |
15 with Isar theories; migration is usually quite simple with the ML |
16 function use_legacy_bindings. INCOMPATIBILITY. |
16 function use_legacy_bindings. INCOMPATIBILITY. |
17 |
17 |
18 * Theory syntax: some popular names (e.g. "class", "if") are now |
18 * Theory syntax: some popular names (e.g. "class", "if", "fun") are |
19 keywords. INCOMPATIBILITY, use double quotes. |
19 now keywords. INCOMPATIBILITY, use double quotes. |
20 |
20 |
21 * Legacy goal package: reduced interface to the bare minimum required |
21 * Legacy goal package: reduced interface to the bare minimum required |
22 to keep existing proof scripts running. Most other user-level |
22 to keep existing proof scripts running. Most other user-level |
23 functions are now part of the OldGoals structure, which is *not* open |
23 functions are now part of the OldGoals structure, which is *not* open |
24 by default (consider isatool expandshort before open OldGoals). |
24 by default (consider isatool expandshort before open OldGoals). |
42 check the given source text as ML type/structure, printing verbatim. |
42 check the given source text as ML type/structure, printing verbatim. |
43 |
43 |
44 |
44 |
45 *** Pure *** |
45 *** Pure *** |
46 |
46 |
47 * class_package.ML offers a combination of axclasses and locales to achieve |
47 * class_package.ML offers a combination of axclasses and locales to |
48 Haskell-like type classes in Isabelle. See HOL/ex/Classpackage.thy for examples. |
48 achieve Haskell-like type classes in Isabelle. See |
49 |
49 HOL/ex/Classpackage.thy for examples. |
50 * Yet another code generator framework allows to generate executable code |
50 |
51 for ML and Haskell (including "class"es). A short usage sketch: |
51 * Yet another code generator framework allows to generate executable |
|
52 code for ML and Haskell (including "class"es). A short usage sketch: |
52 |
53 |
53 internal compilation: |
54 internal compilation: |
54 code_gen <list of constants (term syntax)> (SML -) |
55 code_gen <list of constants (term syntax)> (SML -) |
55 writing SML code to a file: |
56 writing SML code to a file: |
56 code_gen <list of constants (term syntax)> (SML <filename>) |
57 code_gen <list of constants (term syntax)> (SML <filename>) |
562 still supported as well. |
563 still supported as well. |
563 |
564 |
564 * inductive and datatype: provide projections of mutual rules, bundled |
565 * inductive and datatype: provide projections of mutual rules, bundled |
565 as foo_bar.inducts; |
566 as foo_bar.inducts; |
566 |
567 |
|
568 * Library: theory Infinite_Set has been moved to the library. |
|
569 |
567 * Library: theory Accessible_Part has been move to main HOL. |
570 * Library: theory Accessible_Part has been move to main HOL. |
568 |
571 |
569 * Library: added theory Coinductive_List of potentially infinite lists |
572 * Library: added theory Coinductive_List of potentially infinite lists |
570 as greatest fixed-point. |
573 as greatest fixed-point. |
571 |
574 |
572 * Library: added theory AssocList which implements (finite) maps as |
575 * Library: added theory AssocList which implements (finite) maps as |
573 association lists. |
576 association lists. |
574 |
577 |
575 * New proof method "evaluation" for efficiently solving a goal |
578 * New proof method "evaluation" for efficiently solving a goal (i.e. a |
576 (i.e. a boolean expression) by compiling it to ML. The goal is |
579 boolean expression) by compiling it to ML. The goal is "proved" (via |
577 "proved" (via the oracle "Evaluation") if it evaluates to True. |
580 the oracle "Evaluation") if it evaluates to True. |
578 |
581 |
579 * Linear arithmetic now splits certain operators (e.g. min, max, abs) also |
582 * Linear arithmetic now splits certain operators (e.g. min, max, abs) |
580 when invoked by the simplifier. This results in the simplifier being more |
583 also when invoked by the simplifier. This results in the simplifier |
581 powerful on arithmetic goals. |
584 being more powerful on arithmetic goals. INCOMPATIBILTY. Set |
582 INCOMPATIBILTY: rewrite proofs. Set fast_arith_split_limit to 0 to obtain |
585 fast_arith_split_limit to 0 to obtain the old behavior. |
583 the old behavior. |
|
584 |
586 |
585 * Support for hex (0x20) and binary (0b1001) numerals. |
587 * Support for hex (0x20) and binary (0b1001) numerals. |
586 |
588 |
587 * New method: |
589 * New method: reify eqs (t), where eqs are equations for an |
588 reify eqs (t), where eqs are equations for an interpretation |
590 interpretation I :: 'a list => 'b => 'c and t::'c is an optional |
589 I :: 'a list => 'b => 'c and t::'c is an optional parameter, |
591 parameter, computes a term s::'b and a list xs::'a list and proves the |
590 computes a term s::'b and a list xs::'a list and proves the theorem |
592 theorem I xs s = t. This is also known as reification or quoting. The |
591 I xs s = t. This is also known as reification or quoting. The resulting theorem is applied to the subgoal to substitute t with I xs s. |
593 resulting theorem is applied to the subgoal to substitute t with I xs |
592 If t is omitted, the subgoal itself is reified. |
594 s. If t is omitted, the subgoal itself is reified. |
593 |
595 |
594 * New method: |
596 * New method: reflection corr_thm eqs (t). The parameters eqs and (t) |
595 reflection corr_thm eqs (t). The parameters eqs and (t) are as explained above. corr_thm is a theorem for |
597 are as explained above. corr_thm is a theorem for I vs (f t) = I vs t, |
596 I vs (f t) = I vs t, where f is supposed to be a computable function (in the sense of code generattion). The method uses reify to compute s and xs as above then applies corr_thm and uses normalization by evaluation to "prove" f s = r and finally gets the theorem t = r, which is again applied to the subgoal. An Example is available in HOL/ex/ReflectionEx.thy. |
598 where f is supposed to be a computable function (in the sense of code |
597 |
599 generattion). The method uses reify to compute s and xs as above then |
598 * Reflection: Automatic refification now handels binding, an example is available in HOL/ex/ReflectionEx.thy |
600 applies corr_thm and uses normalization by evaluation to "prove" f s = |
|
601 r and finally gets the theorem t = r, which is again applied to the |
|
602 subgoal. An Example is available in HOL/ex/ReflectionEx.thy. |
|
603 |
|
604 * Reflection: Automatic refification now handels binding, an example |
|
605 is available in HOL/ex/ReflectionEx.thy |
|
606 |
|
607 |
599 *** HOL-Algebra *** |
608 *** HOL-Algebra *** |
600 |
609 |
601 * Method algebra is now set up via an attribute. For examples see CRing.thy. |
610 * Method algebra is now set up via an attribute. For examples see CRing.thy. |
602 INCOMPATIBILITY: the method is now weaker on combinations of algebraic |
611 INCOMPATIBILITY: the method is now weaker on combinations of algebraic |
603 structures. |
612 structures. |
604 |
613 |
605 * Formalisation of ideals and the quotient construction over rings, contributed |
614 * Formalisation of ideals and the quotient construction over rings, contributed |
606 by Stephan Hohe. |
615 by Stephan Hohe. |
607 |
616 |
608 * Renamed `CRing.thy' to `Ring.thy'. INCOMPATIBILITY. |
617 * Renamed `CRing.thy' to `Ring.thy'. INCOMPATIBILITY. |
|
618 |
609 |
619 |
610 *** HOL-Complex *** |
620 *** HOL-Complex *** |
611 |
621 |
612 * Theory Real: new method ferrack implements quantifier elimination |
622 * Theory Real: new method ferrack implements quantifier elimination |
613 for linear arithmetic over the reals. The quantifier elimination |
623 for linear arithmetic over the reals. The quantifier elimination |