author | haftmann |
Wed, 03 Dec 2008 15:58:44 +0100 | |
changeset 28952 | 15a4b2cf8c34 |
parent 28915 | 0642cbb60c98 |
child 28964 | f0044cdeb945 |
child 28965 | 1de908189869 |
permissions | -rw-r--r-- |
5363 | 1 |
Isabelle NEWS -- history user-relevant changes |
2 |
============================================== |
|
2553 | 3 |
|
27122 | 4 |
New in this Isabelle version |
5 |
---------------------------- |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
6 |
|
27599 | 7 |
*** General *** |
8 |
||
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
9 |
* Simplified main Isabelle executables, with less surprises on |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
10 |
case-insensitive file-systems (such as Mac OS). |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
11 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
12 |
- The main Isabelle tool wrapper is now called "isabelle" instead of |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
13 |
"isatool." |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
14 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
15 |
- The former "isabelle" alias for "isabelle-process" has been |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
16 |
removed (should rarely occur to regular users). |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
17 |
|
28915
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
18 |
- The former "isabelle-interface" and its alias "Isabelle" have been |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
19 |
removed (interfaces are now regular Isabelle tools). |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
20 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
21 |
Within scripts and make files, the Isabelle environment variables |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
22 |
ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE, |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
23 |
respectively. (The latter are still available as legacy feature.) |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
24 |
|
28915
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
25 |
The old isabelle-interface wrapper could react in confusing ways if |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
26 |
the interface was uninstalled or changed otherwise. Individual |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
27 |
interface tool configuration is now more explicit, see also the |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
28 |
Isabelle system manual. In particular, Proof General is now available |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
29 |
via "isabelle emacs". |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
30 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
31 |
INCOMPATIBILITY, need to adapt derivative scripts. Users may need to |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
32 |
purge installed copies of Isabelle executables and re-run "isabelle |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
33 |
install -p ...", or use symlinks. |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
34 |
|
28914
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
35 |
* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
36 |
old ~/isabelle, which was slightly non-standard and apt cause |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
37 |
surprises on case-insensitive file-systems. |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
38 |
|
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
39 |
INCOMPATIBILITY, need to move existing ~/isabelle/etc, |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
40 |
~/isabelle/heaps, ~/isabelle/browser_info to the new place. Special |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
41 |
care is required when using older releases of Isabelle. Note that |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
42 |
ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
43 |
Isabelle distribution. |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
44 |
|
28252 | 45 |
* The Isabelle System Manual (system) has been updated, with formally |
46 |
checked references as hyperlinks. |
|
47 |
||
27599 | 48 |
* Generalized Isar history, with support for linear undo, direct state |
49 |
addressing etc. |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
50 |
|
27191 | 51 |
* Recovered hiding of consts, which was accidentally broken in |
52 |
Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really |
|
53 |
makes c inaccessible; consider using ``hide (open) const c'' instead. |
|
54 |
||
27599 | 55 |
* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
56 |
interface instead. |
|
57 |
||
58 |
||
59 |
*** Pure *** |
|
60 |
||
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
61 |
* Module moves in repository: |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
62 |
src/Pure/Tools/value.ML ~> src/Tools/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
63 |
src/Pure/Tools/quickcheck.ML ~> src/Tools/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
64 |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28855
diff
changeset
|
65 |
* Slightly more coherent Pure syntax, with updated documentation in |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28855
diff
changeset
|
66 |
isar-ref manual. Removed locales meta_term_syntax and |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28855
diff
changeset
|
67 |
meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent, |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28855
diff
changeset
|
68 |
INCOMPATIBILITY in rare situations. |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28855
diff
changeset
|
69 |
|
28629
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
70 |
* Goal-directed proof now enforces strict proof irrelevance wrt. sort |
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
71 |
hypotheses. Sorts required in the course of reasoning need to be |
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
72 |
covered by the constraints in the initial statement, completed by the |
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
73 |
type instance information of the background theory. Non-trivial sort |
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
74 |
hypotheses, which rarely occur in practice, may be specified via |
28633 | 75 |
vacuous propositions of the form SORT_CONSTRAINT('a::c). For example: |
28629
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
76 |
|
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
77 |
lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ... |
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
78 |
|
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
79 |
The result contains an implicit sort hypotheses as before -- |
28631 | 80 |
SORT_CONSTRAINT premises are eliminated as part of the canonical rule |
81 |
normalization. |
|
28629
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
82 |
|
28178
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
83 |
* Changed defaults for unify configuration options: |
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
84 |
|
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
85 |
unify_trace_bound = 50 (formerly 25) |
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
86 |
unify_search_bound = 60 (formerly 30) |
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
87 |
|
28143 | 88 |
* Different bookkeeping for code equations: |
89 |
a) On theory merge, the last set of code equations for a particular constant |
|
90 |
is taken (in accordance with the policy applied by other parts of the |
|
91 |
code generator framework). |
|
92 |
b) Code equations stemming from explicit declarations (e.g. code attribute) |
|
93 |
gain priority over default code equations stemming from definition, primrec, |
|
94 |
fun etc. |
|
95 |
INCOMPATIBILITY. |
|
96 |
||
28058 | 97 |
* Global versions of theorems stemming from classes do not carry |
98 |
a parameter prefix any longer. INCOMPATIBILITY. |
|
99 |
||
28710 | 100 |
* Dropped locale element "includes". This is a major INCOMPATIBILITY. |
101 |
In existing theorem specifications replace the includes element by the |
|
102 |
respective context elements of the included locale, omitting those that |
|
103 |
are already present in the theorem specification. Multiple assume |
|
104 |
elements of a locale should be replaced by a single one involving the |
|
105 |
locale predicate. In the proof body, declarations (most notably |
|
106 |
theorems) may be regained by interpreting the respective locales in the |
|
107 |
proof context as required (command "interpret"). |
|
108 |
If using "includes" in replacement of a target solely because the |
|
109 |
parameter types in the theorem are not as general as in the target, |
|
110 |
consider declaring a new locale with additional type constraints on the |
|
111 |
parameters (context element "constrains"). |
|
112 |
||
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27717
diff
changeset
|
113 |
* Dropped "locale (open)". INCOMPATBILITY. |
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27717
diff
changeset
|
114 |
|
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28067
diff
changeset
|
115 |
* Interpretation commands no longer attempt to simplify goal. |
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27717
diff
changeset
|
116 |
INCOMPATIBILITY: in rare situations the generated goal differs. Use |
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27717
diff
changeset
|
117 |
methods intro_locales and unfold_locales to clarify. |
27681 | 118 |
|
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28067
diff
changeset
|
119 |
* Interpretation commands no longer accept interpretation attributes. |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28067
diff
changeset
|
120 |
INCOMPATBILITY. |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28067
diff
changeset
|
121 |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
122 |
* Command 'instance': attached definitions no longer accepted. |
27141
9bfcdb1905e1
* Attributes cases, induct, coinduct support del option.
wenzelm
parents:
27122
diff
changeset
|
123 |
INCOMPATIBILITY, use proper 'instantiation' target. |
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
124 |
|
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
125 |
* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
126 |
|
28114 | 127 |
* The 'axiomatization' command now only works within a global theory |
128 |
context. INCOMPATIBILITY. |
|
129 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
130 |
|
27381 | 131 |
*** Document preparation *** |
132 |
||
133 |
* Antiquotation @{lemma} now imitates a regular terminal proof, |
|
27392 | 134 |
demanding keyword 'by' and supporting the full method expression |
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
135 |
syntax just like the Isar command 'by'. |
27381 | 136 |
|
137 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
138 |
*** HOL *** |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
139 |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
140 |
* Made repository layout more coherent with logical |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
141 |
distribution structure: |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
142 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
143 |
src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
144 |
src/HOL/Library/Code_Message.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
145 |
src/HOL/Library/GCD.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
146 |
src/HOL/Library/Order_Relation.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
147 |
src/HOL/Library/Parity.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
148 |
src/HOL/Library/Univ_Poly.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
149 |
src/HOL/Real/ContNotDenum.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
150 |
src/HOL/Real/Lubs.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
151 |
src/HOL/Real/PReal.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
152 |
src/HOL/Real/Rational.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
153 |
src/HOL/Real/RComplete.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
154 |
src/HOL/Real/RealDef.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
155 |
src/HOL/Real/RealPow.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
156 |
src/HOL/Real/Real.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
157 |
src/HOL/Complex/Complex_Main.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
158 |
src/HOL/Complex/Complex.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
159 |
src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
160 |
src/HOL/Hyperreal/Deriv.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
161 |
src/HOL/Hyperreal/Fact.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
162 |
src/HOL/Hyperreal/Integration.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
163 |
src/HOL/Hyperreal/Lim.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
164 |
src/HOL/Hyperreal/Ln.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
165 |
src/HOL/Hyperreal/Log.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
166 |
src/HOL/Hyperreal/MacLaurin.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
167 |
src/HOL/Hyperreal/NthRoot.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
168 |
src/HOL/Hyperreal/Series.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
169 |
src/HOL/Hyperreal/Taylor.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
170 |
src/HOL/Hyperreal/Transcendental.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
171 |
src/HOL/Real/Float ~> src/HOL/Library/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
172 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
173 |
src/HOL/arith_data.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
174 |
src/HOL/hologic.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
175 |
src/HOL/simpdata.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
176 |
src/HOL/int_arith1.ML ~> src/HOL/Tools/int_arith.ML |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
177 |
src/HOL/int_factor_simprocs.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
178 |
src/HOL/nat_simprocs.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
179 |
src/HOL/Real/float_arith.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
180 |
src/HOL/Real/float_syntax.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
181 |
src/HOL/Real/rat_arith.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
182 |
src/HOL/Real/real_arith.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
183 |
|
28741 | 184 |
* If methods "eval" and "evaluation" encounter a structured proof state |
185 |
with !!/==>, only the conclusion is evaluated to True (if possible), |
|
186 |
avoiding strange error messages. |
|
187 |
||
188 |
* Simplifier: simproc for let expressions now unfolds if bound variable |
|
189 |
occurs at most one time in let expression body. INCOMPATIBILITY. |
|
190 |
||
28685 | 191 |
* New classes "top" and "bot" with corresponding operations "top" and "bot" |
192 |
in theory Orderings; instantiation of class "complete_lattice" requires |
|
193 |
instantiation of classes "top" and "bot". INCOMPATIBILITY. |
|
194 |
||
195 |
* Changed definition lemma "less_fun_def" in order to provide an instance |
|
196 |
for preorders on functions; use lemma "less_le" instead. INCOMPATIBILITY. |
|
197 |
||
28604
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
198 |
* Unified theorem tables for both code code generators. Thus |
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
199 |
[code func] has disappeared and only [code] remains. INCOMPATIBILITY. |
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
200 |
|
28685 | 201 |
* Constants "undefined" and "default" replace "arbitrary". Usually |
202 |
"undefined" is the right choice to replace "arbitrary", though logically |
|
203 |
there is no difference. INCOMPATIBILITY. |
|
28604
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
204 |
|
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
205 |
* Generic ATP manager for Sledgehammer, based on ML threads instead of |
28605 | 206 |
Posix processes. Avoids potentially expensive forking of the ML |
207 |
process. New thread-based implementation also works on non-Unix |
|
208 |
platforms (Cygwin). Provers are no longer hardwired, but defined |
|
28606 | 209 |
within the theory via plain ML wrapper functions. Basic Sledgehammer |
210 |
commands are covered in the isar-ref manual |
|
28604
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
211 |
|
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
212 |
* Wrapper scripts for remote SystemOnTPTP service allows to use |
28475 | 213 |
sledgehammer without local ATP installation (Vampire etc.). See also |
214 |
ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting |
|
28604
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
215 |
variable. Other provers may be included via suitable ML wrappers, see |
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
216 |
also src/HOL/ATP_Linkup.thy. |
28474
d0b8b0a1fca5
Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
28350
diff
changeset
|
217 |
|
28350 | 218 |
* Normalization by evaluation now allows non-leftlinear equations. |
219 |
Declare with attribute [code nbe]. |
|
220 |
||
221 |
* Command "value" now integrates different evaluation |
|
28248 | 222 |
mechanisms. The result of the first successful evaluation mechanism |
223 |
is printed. In square brackets a particular named evaluation |
|
224 |
mechanisms may be specified (currently, [SML], [code] or [nbe]). See |
|
225 |
further src/HOL/ex/Eval_Examples.thy. |
|
28227 | 226 |
|
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
227 |
* HOL/Orderings: class "wellorder" moved here, with explicit induction |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
228 |
rule "less_induct" as assumption. For instantiation of "wellorder" by |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
229 |
means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY. |
27823 | 230 |
|
27793 | 231 |
* HOL/Orderings: added class "preorder" as superclass of "order". |
232 |
INCOMPATIBILITY: Instantiation proofs for order, linorder |
|
233 |
etc. slightly changed. Some theorems named order_class.* now named |
|
234 |
preorder_class.*. |
|
235 |
||
28855 | 236 |
* HOL/Finite_Set: added a new fold combinator of type |
237 |
('a => 'b => 'b) => 'b => 'a set => 'b |
|
238 |
Occasionally this is more convenient than the old fold combinator which is |
|
239 |
now defined in terms of the new one and renamed to fold_image. |
|
240 |
||
27793 | 241 |
* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been |
242 |
moved to separate class dvd in Ring_and_Field; a couple of lemmas on |
|
243 |
dvd has been generalized to class comm_semiring_1. Likewise a bunch |
|
244 |
of lemmas from Divides has been generalized from nat to class |
|
245 |
semiring_div. INCOMPATIBILITY. This involves the following theorem |
|
246 |
renames resulting from duplicate elimination: |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
247 |
|
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
248 |
dvd_def_mod ~> dvd_eq_mod_eq_0 |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
249 |
zero_dvd_iff ~> dvd_0_left_iff |
28559 | 250 |
dvd_0 ~> dvd_0_right |
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
251 |
DIVISION_BY_ZERO_DIV ~> div_by_0 |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
252 |
DIVISION_BY_ZERO_MOD ~> mod_by_0 |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
253 |
mult_div ~> div_mult_self2_is_id |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
254 |
mult_mod ~> mod_mult_self2_is_0 |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
255 |
|
27599 | 256 |
* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, |
257 |
zlcm (for int); carried together from various gcd/lcm developements in |
|
258 |
the HOL Distribution. zgcd and zlcm replace former igcd and ilcm; |
|
259 |
corresponding theorems renamed accordingly. INCOMPATIBILY. To |
|
260 |
recover tupled syntax, use syntax declarations like: |
|
27556 | 261 |
|
262 |
hide (open) const gcd |
|
263 |
abbreviation gcd where |
|
264 |
"gcd == (%(a, b). GCD.gcd a b)" |
|
265 |
notation (output) |
|
266 |
GCD.gcd ("gcd '(_, _')") |
|
267 |
||
268 |
(analogously for lcm, zgcd, zlcm). |
|
269 |
||
270 |
* HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. |
|
27551 | 271 |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
272 |
* New ML antiquotation @{code}: takes constant as argument, generates |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
273 |
corresponding code in background and inserts name of the corresponding |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
274 |
resulting ML value/function/datatype constructor binding in place. |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
275 |
All occurrences of @{code} with a single ML block are generated |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
276 |
simultaneously. Provides a generic and safe interface for |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
277 |
instrumentalizing code generation. See HOL/ex/Code_Antiq for a toy |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
278 |
example, or HOL/Complex/ex/ReflectedFerrack for a more ambitious |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
279 |
application. In future you ought refrain from ad-hoc compiling |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
280 |
generated SML code on the ML toplevel. Note that (for technical |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
281 |
reasons) @{code} cannot refer to constants for which user-defined |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
282 |
serializations are set. Refer to the corresponding ML counterpart |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
283 |
directly in that cases. |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
284 |
|
27424 | 285 |
* Integrated image HOL-Complex with HOL. Entry points Main.thy and |
286 |
Complex_Main.thy remain as they are. |
|
287 |
||
27599 | 288 |
* New image HOL-Plain provides a minimal HOL with the most important |
289 |
tools available (inductive, datatype, primrec, ...). By convention |
|
290 |
the corresponding theory Plain should be ancestor of every further |
|
291 |
(library) theory. Some library theories now have ancestor Plain |
|
292 |
(instead of Main), thus theory Main occasionally has to be imported |
|
293 |
explicitly. |
|
27421 | 294 |
|
28248 | 295 |
* The metis method now fails in the usual manner, rather than raising |
296 |
an exception, if it determines that it cannot prove the theorem. |
|
28233
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28227
diff
changeset
|
297 |
|
28700
fb92b1d1b285
The metis method no longer fails because the theorem is too trivial
paulson
parents:
28685
diff
changeset
|
298 |
* The metis method no longer fails because the theorem is too trivial |
fb92b1d1b285
The metis method no longer fails because the theorem is too trivial
paulson
parents:
28685
diff
changeset
|
299 |
(contains the empty clause). |
fb92b1d1b285
The metis method no longer fails because the theorem is too trivial
paulson
parents:
28685
diff
changeset
|
300 |
|
27324
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
301 |
* Methods "case_tac" and "induct_tac" now refer to the very same rules |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
302 |
as the structured Isar versions "cases" and "induct", cf. the |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
303 |
corresponding "cases" and "induct" attributes. Mutual induction rules |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
304 |
are now presented as a list of individual projections |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
305 |
(e.g. foo_bar.inducts for types foo and bar); the old format with |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
306 |
explicit HOL conjunction is no longer supported. INCOMPATIBILITY, in |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
307 |
rare situations a different rule is selected --- notably nested tuple |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
308 |
elimination instead of former prod.exhaust: use explicit (case_tac t |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
309 |
rule: prod.exhaust) here. |
27122 | 310 |
|
27141
9bfcdb1905e1
* Attributes cases, induct, coinduct support del option.
wenzelm
parents:
27122
diff
changeset
|
311 |
* Attributes "cases", "induct", "coinduct" support "del" option. |
9bfcdb1905e1
* Attributes cases, induct, coinduct support del option.
wenzelm
parents:
27122
diff
changeset
|
312 |
|
27122 | 313 |
* Removed fact "case_split_thm", which duplicates "case_split". |
314 |
||
315 |
* Command 'rep_datatype': instead of theorem names the command now |
|
316 |
takes a list of terms denoting the constructors of the type to be |
|
317 |
represented as datatype. The characteristic theorems have to be |
|
318 |
proven. INCOMPATIBILITY. Also observe that the following theorems |
|
319 |
have disappeared in favour of existing ones: |
|
320 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
321 |
unit_induct ~> unit.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
322 |
prod_induct ~> prod.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
323 |
sum_induct ~> sum.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
324 |
Suc_Suc_eq ~> nat.inject |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
325 |
Suc_not_Zero Zero_not_Suc ~> nat.distinct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
326 |
|
27122 | 327 |
* Library/Nat_Infinity: added addition, numeral syntax and more |
328 |
instantiations for algebraic structures. Removed some duplicate |
|
329 |
theorems. Changes in simp rules. INCOMPATIBILITY. |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
330 |
|
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
331 |
* ATP selection (E/Vampire/Spass) is now via Proof General's settings |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
332 |
menu. |
28067 | 333 |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
334 |
|
27696 | 335 |
*** HOL-Algebra *** |
336 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
337 |
* New locales for orders and lattices where the equivalence relation |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
338 |
is not restricted to equality. INCOMPATIBILITY: all order and |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
339 |
lattice locales use a record structure with field eq for the |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
340 |
equivalence. |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
341 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
342 |
* New theory of factorial domains. |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
343 |
|
27696 | 344 |
* Units_l_inv and Units_r_inv are now simprules by default. |
345 |
INCOMPATIBILITY. Simplifier proof that require deletion of l_inv |
|
346 |
and/or r_inv will now also require deletion of these lemmas. |
|
347 |
||
348 |
* Renamed the following theorems. INCOMPATIBILITY. |
|
349 |
UpperD ~> Upper_memD |
|
350 |
LowerD ~> Lower_memD |
|
351 |
least_carrier ~> least_closed |
|
352 |
greatest_carrier ~> greatest_closed |
|
353 |
greatest_Lower_above ~> greatest_Lower_below |
|
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
354 |
one_zero ~> carrier_one_zero |
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
355 |
one_not_zero ~> carrier_one_not_zero (collision with assumption) |
27696 | 356 |
|
27793 | 357 |
|
27485 | 358 |
*** HOL-NSA *** |
359 |
||
360 |
* Created new image HOL-NSA, containing theories of nonstandard |
|
361 |
analysis which were previously part of HOL-Complex. Entry point |
|
362 |
Hyperreal.thy remains valid, but theories formerly using |
|
363 |
Complex_Main.thy should now use new entry point Hypercomplex.thy. |
|
364 |
||
365 |
||
27704 | 366 |
*** ZF *** |
367 |
||
368 |
* Proof of Zorn's Lemma for partial orders. |
|
369 |
||
370 |
||
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
371 |
*** ML *** |
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
372 |
|
28294 | 373 |
* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm |
374 |
to 'a -> thm, while results are always tagged with an authentic oracle |
|
375 |
name. The Isar command 'oracle' is now polymorphic, no argument type |
|
376 |
is specified. INCOMPATIBILITY, need to simplify existing oracle code |
|
377 |
accordingly. Note that extra performance may be gained by producing |
|
378 |
the cterm carefully, avoiding slow Thm.cterm_of. |
|
379 |
||
28282
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
380 |
* ML bindings produced via Isar commands are stored within the Isar |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
381 |
context (theory or proof). Consequently, commands like 'use' and 'ML' |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
382 |
become thread-safe and work with undo as expected (concerning |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
383 |
top-level bindings, not side-effects on global references). |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
384 |
INCOMPATIBILITY, need to provide proper Isar context when invoking the |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
385 |
compiler at runtime; really global bindings need to be given outside a |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
386 |
theory. [Poly/ML 5.2 or later] |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
387 |
|
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
388 |
* Command 'ML_prf' is analogous to 'ML' but works within a proof |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
389 |
context. Top-level ML bindings are stored within the proof context in |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
390 |
a purely sequential fashion, disregarding the nested proof structure. |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
391 |
ML bindings introduced by 'ML_prf' are discarded at the end of the |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
392 |
proof. [Poly/ML 5.2 or later] |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
393 |
|
28099
fb16a07d6580
* Generic Toplevel.add_hook interface allows to analyze the result of
wenzelm
parents:
28089
diff
changeset
|
394 |
* Generic Toplevel.add_hook interface allows to analyze the result of |
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28099
diff
changeset
|
395 |
transactions. E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML |
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28099
diff
changeset
|
396 |
for theorem dependency output of transactions resulting in a new |
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28099
diff
changeset
|
397 |
theory state. |
28099
fb16a07d6580
* Generic Toplevel.add_hook interface allows to analyze the result of
wenzelm
parents:
28089
diff
changeset
|
398 |
|
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
399 |
* Name bindings in higher specification mechanisms (notably |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
400 |
LocalTheory.define, LocalTheory.note, and derived packages) are now |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
401 |
formalized as type Name.binding, replacing old bstring. |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
402 |
INCOMPATIBILITY, need to wrap strings via Name.binding function, see |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
403 |
also Name.name_of. Packages should pass name bindings given by the |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
404 |
user to underlying specification mechanisms; this enables precise |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
405 |
tracking of source positions, for example. |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
406 |
|
28089
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
407 |
* Result facts (from PureThy.note_thms, ProofContext.note_thms, |
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
408 |
LocalTheory.note etc.) now refer to the *full* internal name, not the |
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
409 |
bstring as before. INCOMPATIBILITY, not detected by ML type-checking! |
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
410 |
|
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
411 |
* Rules and tactics that read instantiations (read_instantiate, |
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
412 |
res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof |
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
413 |
context, which is required for parsing and type-checking. Moreover, |
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
414 |
the variables are specified as plain indexnames, not string encodings |
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
415 |
thereof. INCOMPATIBILITY. |
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
416 |
|
27287 | 417 |
* Disposed old type and term read functions (Sign.read_def_typ, |
418 |
Sign.read_typ, Sign.read_def_terms, Sign.read_term, |
|
419 |
Thm.read_def_cterms, Thm.read_cterm etc.). INCOMPATIBILITY, should |
|
420 |
use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global, |
|
27269 | 421 |
Syntax.read_term_global etc.; see also OldGoals.read_term as last |
422 |
resort for legacy applications. |
|
423 |
||
27380 | 424 |
* Antiquotations: block-structured compilation context indicated by |
27391 | 425 |
\<lbrace> ... \<rbrace>; additional antiquotation forms: |
426 |
||
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
427 |
@{let ?pat = term} - term abbreviation (HO matching) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
428 |
@{note name = fact} - fact abbreviation |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
429 |
@{thm fact} - singleton fact (with attributes) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
430 |
@{thms fact} - general fact (with attributes) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
431 |
@{lemma prop by method} - singleton goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
432 |
@{lemma prop by meth1 meth2} - singleton goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
433 |
@{lemma prop1 ... propN by method} - general goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
434 |
@{lemma prop1 ... propN by meth1 meth2} - general goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
435 |
@{lemma (open) ...} - open derivation |
27380 | 436 |
|
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
437 |
|
27979 | 438 |
*** System *** |
439 |
||
28676
78688a5fafc2
multithreading support only for polyml-5.2.1 or later;
wenzelm
parents:
28633
diff
changeset
|
440 |
* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for |
78688a5fafc2
multithreading support only for polyml-5.2.1 or later;
wenzelm
parents:
28633
diff
changeset
|
441 |
Poly/ML 5.2.1 or later. |
28254
d67ba23e0277
multithreading for Poly/ML 5.1 is no longer supported;
wenzelm
parents:
28252
diff
changeset
|
442 |
|
28248 | 443 |
* The Isabelle "emacs" tool provides a specific interface to invoke |
444 |
Proof General / Emacs, with more explicit failure if that is not |
|
445 |
installed (the old isabelle-interface script silently falls back on |
|
446 |
isabelle-process). The PROOFGENERAL_HOME setting determines the |
|
447 |
installation location of the Proof General distribution. |
|
448 |
||
27979 | 449 |
* Isabelle/lib/classes/Pure.jar provides basic support to integrate |
450 |
the Isabelle process into a JVM/Scala application. See |
|
451 |
Isabelle/lib/jedit/plugin for a minimal example. (The obsolete Java |
|
452 |
process wrapper has been discontinued.) |
|
453 |
||
454 |
* Status messages (with exact source position information) are |
|
455 |
emitted, if proper markup print mode is enabled. This allows |
|
456 |
user-interface components to provide detailed feedback on internal |
|
457 |
prover operations. |
|
458 |
||
459 |
* Homegrown Isabelle font with unicode layout, see Isabelle/lib/fonts. |
|
460 |
||
461 |
||
27143 | 462 |
|
27008 | 463 |
New in Isabelle2008 (June 2008) |
464 |
------------------------------- |
|
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
465 |
|
25522 | 466 |
*** General *** |
467 |
||
27061 | 468 |
* The Isabelle/Isar Reference Manual (isar-ref) has been reorganized |
469 |
and updated, with formally checked references as hyperlinks. |
|
470 |
||
25994 | 471 |
* Theory loader: use_thy (and similar operations) no longer set the |
472 |
implicit ML context, which was occasionally hard to predict and in |
|
473 |
conflict with concurrency. INCOMPATIBILITY, use ML within Isar which |
|
474 |
provides a proper context already. |
|
475 |
||
26323
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
476 |
* Theory loader: old-style ML proof scripts being *attached* to a thy |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
477 |
file are no longer supported. INCOMPATIBILITY, regular 'uses' and |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
478 |
'use' within a theory file will do the job. |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
479 |
|
26650 | 480 |
* Name space merge now observes canonical order, i.e. the second space |
481 |
is inserted into the first one, while existing entries in the first |
|
26659 | 482 |
space take precedence. INCOMPATIBILITY in rare situations, may try to |
26650 | 483 |
swap theory imports. |
484 |
||
27067 | 485 |
* Syntax: symbol \<chi> is now considered a letter. Potential |
486 |
INCOMPATIBILITY in identifier syntax etc. |
|
487 |
||
488 |
* Outer syntax: string tokens no longer admit escaped white space, |
|
489 |
which was an accidental (undocumented) feature. INCOMPATIBILITY, use |
|
490 |
white space without escapes. |
|
491 |
||
492 |
* Outer syntax: string tokens may contain arbitrary character codes |
|
493 |
specified via 3 decimal digits (as in SML). E.g. "foo\095bar" for |
|
494 |
"foo_bar". |
|
495 |
||
25522 | 496 |
|
25502 | 497 |
*** Pure *** |
498 |
||
26718 | 499 |
* Context-dependent token translations. Default setup reverts locally |
500 |
fixed variables, and adds hilite markup for undeclared frees. |
|
501 |
||
26681 | 502 |
* Unused theorems can be found using the new command 'unused_thms'. |
503 |
There are three ways of invoking it: |
|
504 |
||
505 |
(1) unused_thms |
|
506 |
Only finds unused theorems in the current theory. |
|
507 |
||
508 |
(2) unused_thms thy_1 ... thy_n - |
|
509 |
Finds unused theorems in the current theory and all of its ancestors, |
|
510 |
excluding the theories thy_1 ... thy_n and all of their ancestors. |
|
511 |
||
512 |
(3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m |
|
513 |
Finds unused theorems in the theories thy'_1 ... thy'_m and all of |
|
514 |
their ancestors, excluding the theories thy_1 ... thy_n and all of |
|
515 |
their ancestors. |
|
516 |
||
26718 | 517 |
In order to increase the readability of the list produced by |
518 |
unused_thms, theorems that have been created by a particular instance |
|
26874 | 519 |
of a theory command such as 'inductive' or 'function' are considered |
520 |
to belong to the same "group", meaning that if at least one theorem in |
|
26718 | 521 |
this group is used, the other theorems in the same group are no longer |
522 |
reported as unused. Moreover, if all theorems in the group are |
|
523 |
unused, only one theorem in the group is displayed. |
|
524 |
||
525 |
Note that proof objects have to be switched on in order for |
|
526 |
unused_thms to work properly (i.e. !proofs must be >= 1, which is |
|
26874 | 527 |
usually the case when using Proof General with the default settings). |
26681 | 528 |
|
26650 | 529 |
* Authentic naming of facts disallows ad-hoc overwriting of previous |
530 |
theorems within the same name space. INCOMPATIBILITY, need to remove |
|
531 |
duplicate fact bindings, or even accidental fact duplications. Note |
|
532 |
that tools may maintain dynamically scoped facts systematically, using |
|
533 |
PureThy.add_thms_dynamic. |
|
534 |
||
26660 | 535 |
* Command 'hide' now allows to hide from "fact" name space as well. |
536 |
||
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
537 |
* Eliminated destructive theorem database, simpset, claset, and |
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
538 |
clasimpset. Potential INCOMPATIBILITY, really need to observe linear |
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
539 |
update of theories within ML code. |
26479 | 540 |
|
26955
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
541 |
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory. |
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
542 |
INCOMPATIBILITY, object-logics depending on former Pure require |
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
543 |
additional setup PureThy.old_appl_syntax_setup; object-logics |
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
544 |
depending on former CPure need to refer to Pure. |
26650 | 545 |
|
26495 | 546 |
* Commands 'use' and 'ML' are now purely functional, operating on |
26479 | 547 |
theory/local_theory. Removed former 'ML_setup' (on theory), use 'ML' |
548 |
instead. Added 'ML_val' as mere diagnostic replacement for 'ML'. |
|
549 |
INCOMPATIBILITY. |
|
550 |
||
26874 | 551 |
* Command 'setup': discontinued implicit version with ML reference. |
26434 | 552 |
|
25970
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
553 |
* Instantiation target allows for simultaneous specification of class |
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
554 |
instance operations together with an instantiation proof. |
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
555 |
Type-checking phase allows to refer to class operations uniformly. |
27067 | 556 |
See src/HOL/Complex/Complex.thy for an Isar example and |
557 |
src/HOL/Library/Eval.thy for an ML example. |
|
25502 | 558 |
|
26201
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
559 |
* Indexing of literal facts: be more serious about including only |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
560 |
facts from the visible specification/proof context, but not the |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
561 |
background context (locale etc.). Affects `prop` notation and method |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
562 |
"fact". INCOMPATIBILITY: need to name facts explicitly in rare |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
563 |
situations. |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
564 |
|
26925
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
565 |
* Method "cases", "induct", "coinduct": removed obsolete/undocumented |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
566 |
"(open)" option, which used to expose internal bound variables to the |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
567 |
proof text. |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
568 |
|
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
569 |
* Isar statements: removed obsolete case "rule_context". |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
570 |
INCOMPATIBILITY, better use explicit fixes/assumes. |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
571 |
|
26874 | 572 |
* Locale proofs: default proof step now includes 'unfold_locales'; |
573 |
hence 'proof' without argument may be used to unfold locale |
|
574 |
predicates. |
|
26765 | 575 |
|
576 |
||
26762 | 577 |
*** Document preparation *** |
578 |
||
26914 | 579 |
* Simplified pdfsetup.sty: color/hyperref is used unconditionally for |
580 |
both pdf and dvi (hyperlinks usually work in xdvi as well); removed |
|
581 |
obsolete thumbpdf setup (contemporary PDF viewers do this on the |
|
582 |
spot); renamed link color from "darkblue" to "linkcolor" (default |
|
26920 | 583 |
value unchanged, can be redefined via \definecolor); no longer sets |
584 |
"a4paper" option (unnecessary or even intrusive). |
|
26914 | 585 |
|
27008 | 586 |
* Antiquotation @{lemma A method} proves proposition A by the given |
587 |
method (either a method name or a method name plus (optional) method |
|
588 |
arguments in parentheses) and prints A just like @{prop A}. |
|
26762 | 589 |
|
590 |
||
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
591 |
*** HOL *** |
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
592 |
|
27067 | 593 |
* New primrec package. Specification syntax conforms in style to |
594 |
definition/function/.... No separate induction rule is provided. The |
|
595 |
"primrec" command distinguishes old-style and new-style specifications |
|
596 |
by syntax. The former primrec package is now named OldPrimrecPackage. |
|
597 |
When adjusting theories, beware: constants stemming from new-style |
|
598 |
primrec specifications have authentic syntax. |
|
599 |
||
600 |
* Metis prover is now an order of magnitude faster, and also works |
|
601 |
with multithreading. |
|
602 |
||
603 |
* Metis: the maximum number of clauses that can be produced from a |
|
604 |
theorem is now given by the attribute max_clauses. Theorems that |
|
605 |
exceed this number are ignored, with a warning printed. |
|
606 |
||
607 |
* Sledgehammer no longer produces structured proofs by default. To |
|
608 |
enable, declare [[sledgehammer_full = true]]. Attributes |
|
609 |
reconstruction_modulus, reconstruction_sorts renamed |
|
610 |
sledgehammer_modulus, sledgehammer_sorts. INCOMPATIBILITY. |
|
611 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
612 |
* Method "induct_scheme" derives user-specified induction rules |
27067 | 613 |
from well-founded induction and completeness of patterns. This factors |
614 |
out some operations that are done internally by the function package |
|
615 |
and makes them available separately. See |
|
616 |
src/HOL/ex/Induction_Scheme.thy for examples. |
|
617 |
||
618 |
* More flexible generation of measure functions for termination |
|
619 |
proofs: Measure functions can be declared by proving a rule of the |
|
620 |
form "is_measure f" and giving it the [measure_function] attribute. |
|
621 |
The "is_measure" predicate is logically meaningless (always true), and |
|
622 |
just guides the heuristic. To find suitable measure functions, the |
|
623 |
termination prover sets up the goal "is_measure ?f" of the appropriate |
|
624 |
type and generates all solutions by prolog-style backwards proof using |
|
625 |
the declared rules. |
|
626 |
||
627 |
This setup also deals with rules like |
|
628 |
||
629 |
"is_measure f ==> is_measure (list_size f)" |
|
630 |
||
631 |
which accommodates nested datatypes that recurse through lists. |
|
632 |
Similar rules are predeclared for products and option types. |
|
633 |
||
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
634 |
* Turned the type of sets "'a set" into an abbreviation for "'a => bool" |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
635 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
636 |
INCOMPATIBILITIES: |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
637 |
|
27008 | 638 |
- Definitions of overloaded constants on sets have to be replaced by |
639 |
definitions on => and bool. |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
640 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
641 |
- Some definitions of overloaded operators on sets can now be proved |
27008 | 642 |
using the definitions of the operators on => and bool. Therefore, |
643 |
the following theorems have been renamed: |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
644 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
645 |
subset_def -> subset_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
646 |
psubset_def -> psubset_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
647 |
set_diff_def -> set_diff_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
648 |
Compl_def -> Compl_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
649 |
Sup_set_def -> Sup_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
650 |
Inf_set_def -> Inf_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
651 |
sup_set_def -> sup_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
652 |
inf_set_def -> inf_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
653 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
654 |
- Due to the incompleteness of the HO unification algorithm, some |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
655 |
rules such as subst may require manual instantiation, if some of |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
656 |
the unknowns in the rule is a set. |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
657 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
658 |
- Higher order unification and forward proofs: |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
659 |
The proof pattern |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
660 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
661 |
have "P (S::'a set)" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
662 |
then have "EX S. P S" .. |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
663 |
|
27008 | 664 |
no longer works (due to the incompleteness of the HO unification |
665 |
algorithm) and must be replaced by the pattern |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
666 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
667 |
have "EX S. P S" |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
668 |
proof |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
669 |
show "P S" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
670 |
qed |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
671 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
672 |
- Calculational reasoning with subst (or similar rules): |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
673 |
The proof pattern |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
674 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
675 |
have "P (S::'a set)" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
676 |
also have "S = T" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
677 |
finally have "P T" . |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
678 |
|
27008 | 679 |
no longer works (for similar reasons as the previous example) and |
680 |
must be replaced by something like |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
681 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
682 |
have "P (S::'a set)" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
683 |
moreover have "S = T" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
684 |
ultimately have "P T" by simp |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
685 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
686 |
- Tactics or packages written in ML code: |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
687 |
Code performing pattern matching on types via |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
688 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
689 |
Type ("set", [T]) => ... |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
690 |
|
27008 | 691 |
must be rewritten. Moreover, functions like strip_type or |
692 |
binder_types no longer return the right value when applied to a |
|
693 |
type of the form |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
694 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
695 |
T1 => ... => Tn => U => bool |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
696 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
697 |
rather than |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
698 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
699 |
T1 => ... => Tn => U set |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
700 |
|
26874 | 701 |
* Merged theories Wellfounded_Recursion, Accessible_Part and |
27067 | 702 |
Wellfounded_Relations to theory Wellfounded. |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26724
diff
changeset
|
703 |
|
26513 | 704 |
* Explicit class "eq" for executable equality. INCOMPATIBILITY. |
705 |
||
26874 | 706 |
* Class finite no longer treats UNIV as class parameter. Use class |
707 |
enum from theory Library/Enum instead to achieve a similar effect. |
|
26445 | 708 |
INCOMPATIBILITY. |
709 |
||
26874 | 710 |
* Theory List: rule list_induct2 now has explicitly named cases "Nil" |
711 |
and "Cons". INCOMPATIBILITY. |
|
712 |
||
26422
d5883907c514
HOL (and FOL): renamed variables in rules imp_elim and swap;
wenzelm
parents:
26401
diff
changeset
|
713 |
* HOL (and FOL): renamed variables in rules imp_elim and swap. |
d5883907c514
HOL (and FOL): renamed variables in rules imp_elim and swap;
wenzelm
parents:
26401
diff
changeset
|
714 |
Potential INCOMPATIBILITY. |
d5883907c514
HOL (and FOL): renamed variables in rules imp_elim and swap;
wenzelm
parents:
26401
diff
changeset
|
715 |
|
26874 | 716 |
* Theory Product_Type: duplicated lemmas split_Pair_apply and |
717 |
injective_fst_snd removed, use split_eta and prod_eqI instead. |
|
718 |
Renamed upd_fst to apfst and upd_snd to apsnd. INCOMPATIBILITY. |
|
26355 | 719 |
|
26335
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
720 |
* Theory Nat: removed redundant lemmas that merely duplicate lemmas of |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
721 |
the same name in theory Orderings: |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
722 |
|
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
723 |
less_trans |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
724 |
less_linear |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
725 |
le_imp_less_or_eq |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
726 |
le_less_trans |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
727 |
less_le_trans |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
728 |
less_not_sym |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
729 |
less_asym |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
730 |
|
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
731 |
Renamed less_imp_le to less_imp_le_nat, and less_irrefl to |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
732 |
less_irrefl_nat. Potential INCOMPATIBILITY due to more general types |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
733 |
and different variable names. |
26315
cb3badaa192e
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
wenzelm
parents:
26231
diff
changeset
|
734 |
|
26231 | 735 |
* Library/Option_ord.thy: Canonical order on option type. |
736 |
||
27008 | 737 |
* Library/RBT.thy: Red-black trees, an efficient implementation of |
738 |
finite maps. |
|
26197 | 739 |
|
26231 | 740 |
* Library/Countable.thy: Type class for countable types. |
741 |
||
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
742 |
* Theory Int: The representation of numerals has changed. The infix |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
743 |
operator BIT and the bit datatype with constructors B0 and B1 have |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
744 |
disappeared. INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
745 |
place of "x BIT bit.B0" and "y BIT bit.B1", respectively. Theorems |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
746 |
involving BIT, B0, or B1 have been renamed with "Bit0" or "Bit1" |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
747 |
accordingly. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
748 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
749 |
* Theory Nat: definition of <= and < on natural numbers no longer |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
750 |
depend on well-founded relations. INCOMPATIBILITY. Definitions |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
751 |
le_def and less_def have disappeared. Consider lemmas not_less |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
752 |
[symmetric, where ?'a = nat] and less_eq [symmetric] instead. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
753 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
754 |
* Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
755 |
(whose purpose mainly is for various fold_set functionals) have been |
26874 | 756 |
abandoned in favor of the existing algebraic classes |
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
757 |
ab_semigroup_mult, comm_monoid_mult, ab_semigroup_idem_mult, |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
758 |
lower_semilattice (resp. upper_semilattice) and linorder. |
26139 | 759 |
INCOMPATIBILITY. |
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
26013
diff
changeset
|
760 |
|
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
761 |
* Theory Transitive_Closure: induct and cases rules now declare proper |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
762 |
case_names ("base" and "step"). INCOMPATIBILITY. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
763 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
764 |
* Theorem Inductive.lfp_ordinal_induct generalized to complete |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
765 |
lattices. The form set-specific version is available as |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
766 |
Inductive.lfp_ordinal_induct_set. |
26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
26006
diff
changeset
|
767 |
|
26874 | 768 |
* Renamed theorems "power.simps" to "power_int.simps". |
27067 | 769 |
INCOMPATIBILITY. |
25961 | 770 |
|
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
771 |
* Class semiring_div provides basic abstract properties of semirings |
25942 | 772 |
with division and modulo operations. Subsumes former class dvd_mod. |
773 |
||
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
774 |
* Merged theories IntDef, Numeral and IntArith into unified theory |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
775 |
Int. INCOMPATIBILITY. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
776 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
777 |
* Theory Library/Code_Index: type "index" now represents natural |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
778 |
numbers rather than integers. INCOMPATIBILITY. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
779 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
780 |
* New class "uminus" with operation "uminus" (split of from class |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
781 |
"minus" which now only has operation "minus", binary). |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
782 |
INCOMPATIBILITY. |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
783 |
|
25522 | 784 |
* Constants "card", "internal_split", "option_map" now with authentic |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
785 |
syntax. INCOMPATIBILITY. |
25522 | 786 |
|
787 |
* Definitions subset_def, psubset_def, set_diff_def, Compl_def, |
|
788 |
le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def, |
|
789 |
sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def, |
|
790 |
Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def, |
|
791 |
Sup_set_def, le_def, less_def, option_map_def now with object |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
792 |
equality. INCOMPATIBILITY. |
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
793 |
|
25705 | 794 |
* Records. Removed K_record, and replaced it by pure lambda term |
25726
9728f319ffc6
* Metis prover an order of magnitude faster, works with multithreading.
wenzelm
parents:
25712
diff
changeset
|
795 |
%x. c. The simplifier setup is now more robust against eta expansion. |
25705 | 796 |
INCOMPATIBILITY: in cases explicitly referring to K_record. |
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
797 |
|
27067 | 798 |
* Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}. |
799 |
||
800 |
* Library/ListVector: new theory of arithmetic vector operations. |
|
801 |
||
802 |
* Library/Order_Relation: new theory of various orderings as sets of |
|
803 |
pairs. Defines preorders, partial orders, linear orders and |
|
804 |
well-orders on sets and on types. |
|
26877 | 805 |
|
25726
9728f319ffc6
* Metis prover an order of magnitude faster, works with multithreading.
wenzelm
parents:
25712
diff
changeset
|
806 |
|
26197 | 807 |
*** ZF *** |
808 |
||
26874 | 809 |
* Renamed some theories to allow to loading both ZF and HOL in the |
810 |
same session: |
|
811 |
||
812 |
Datatype -> Datatype_ZF |
|
813 |
Inductive -> Inductive_ZF |
|
814 |
Int -> Int_ZF |
|
815 |
IntDiv -> IntDiv_ZF |
|
816 |
Nat -> Nat_ZF |
|
817 |
List -> List_ZF |
|
818 |
Main -> Main_ZF |
|
819 |
||
820 |
INCOMPATIBILITY: ZF theories that import individual theories below |
|
821 |
Main might need to be adapted. Regular theory Main is still |
|
822 |
available, as trivial extension of Main_ZF. |
|
26197 | 823 |
|
824 |
||
25737
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
825 |
*** ML *** |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
826 |
|
27067 | 827 |
* ML within Isar: antiquotation @{const name} or @{const |
828 |
name(typargs)} produces statically-checked Const term. |
|
829 |
||
26401
e7a94081dce7
Functor NamedThmsFun: data is available to the user as dynamic fact;
wenzelm
parents:
26387
diff
changeset
|
830 |
* Functor NamedThmsFun: data is available to the user as dynamic fact |
26724
ff6ff3a9010e
NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;
wenzelm
parents:
26718
diff
changeset
|
831 |
(of the same name). Removed obsolete print command. |
26401
e7a94081dce7
Functor NamedThmsFun: data is available to the user as dynamic fact;
wenzelm
parents:
26387
diff
changeset
|
832 |
|
27067 | 833 |
* Removed obsolete "use_legacy_bindings" function. |
26188 | 834 |
|
25737
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
835 |
* The ``print mode'' is now a thread-local value derived from a global |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
836 |
template (the former print_mode reference), thus access becomes |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
837 |
non-critical. The global print_mode reference is for session |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
838 |
management only; user-code should use print_mode_value, |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
839 |
print_mode_active, PrintMode.setmp etc. INCOMPATIBILITY. |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
840 |
|
26874 | 841 |
* Functions system/system_out provide a robust way to invoke external |
27008 | 842 |
shell commands, with propagation of interrupts (requires Poly/ML 5.2). |
26874 | 843 |
Do not use OS.Process.system etc. from the basis library! |
26222
edf6473ac9e9
* system/system_out provides a robust way to invoke external shell
wenzelm
parents:
26218
diff
changeset
|
844 |
|
25737
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
845 |
|
25626
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
846 |
*** System *** |
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
847 |
|
25971 | 848 |
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs --- |
849 |
in accordance with Proof General 3.7, which prefers GNU emacs. |
|
25970
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
850 |
|
25626
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
851 |
* isatool tty runs Isabelle process with plain tty interaction; |
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
852 |
optional line editor may be specified via ISABELLE_LINE_EDITOR |
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
853 |
setting, the default settings attempt to locate "ledit" and "rlwrap". |
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
854 |
|
25651 | 855 |
* isatool browser now works with Cygwin as well, using general |
856 |
"javapath" function defined in Isabelle process environment. |
|
857 |
||
27067 | 858 |
* YXML notation provides a simple and efficient alternative to |
859 |
standard XML transfer syntax. See src/Pure/General/yxml.ML and |
|
860 |
isatool yxml as described in the Isabelle system manual. |
|
25651 | 861 |
|
25652 | 862 |
* JVM class isabelle.IsabelleProcess (located in Isabelle/lib/classes) |
25651 | 863 |
provides general wrapper for managing an Isabelle process in a robust |
864 |
fashion, with ``cooked'' output from stdin/stderr. |
|
865 |
||
25855 | 866 |
* Rudimentary Isabelle plugin for jEdit (see Isabelle/lib/jedit), |
867 |
based on Isabelle/JVM process wrapper (see Isabelle/lib/classes). |
|
868 |
||
27067 | 869 |
* Removed obsolete THIS_IS_ISABELLE_BUILD feature. NB: the documented |
870 |
way of changing the user's settings is via |
|
871 |
ISABELLE_HOME_USER/etc/settings, which is a fully featured bash |
|
872 |
script. |
|
873 |
||
874 |
* Multithreading.max_threads := 0 refers to the number of actual CPU |
|
875 |
cores of the underlying machine, which is a good starting point for |
|
876 |
optimal performance tuning. The corresponding usedir option -M allows |
|
877 |
"max" as an alias for "0". WARNING: does not work on certain versions |
|
878 |
of Mac OS (with Poly/ML 5.1). |
|
879 |
||
880 |
* isabelle-process: non-ML sessions are run with "nice", to reduce the |
|
881 |
adverse effect of Isabelle flooding interactive front-ends (notably |
|
882 |
ProofGeneral / XEmacs). |
|
883 |
||
25626
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
884 |
|
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
885 |
|
25429 | 886 |
New in Isabelle2007 (November 2007) |
887 |
----------------------------------- |
|
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
888 |
|
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
889 |
*** General *** |
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
890 |
|
22826 | 891 |
* More uniform information about legacy features, notably a |
892 |
warning/error of "Legacy feature: ...", depending on the state of the |
|
23367 | 893 |
tolerate_legacy_features flag (default true). FUTURE INCOMPATIBILITY: |
894 |
legacy features will disappear eventually. |
|
22826 | 895 |
|
17918
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
896 |
* Theory syntax: the header format ``theory A = B + C:'' has been |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
897 |
discontinued in favour of ``theory A imports B C begin''. Use isatool |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
898 |
fixheaders to convert existing theory files. INCOMPATIBILITY. |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
899 |
|
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
900 |
* Theory syntax: the old non-Isar theory file format has been |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
901 |
discontinued altogether. Note that ML proof scripts may still be used |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
902 |
with Isar theories; migration is usually quite simple with the ML |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
903 |
function use_legacy_bindings. INCOMPATIBILITY. |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
904 |
|
22871 | 905 |
* Theory syntax: some popular names (e.g. 'class', 'declaration', |
906 |
'fun', 'help', 'if') are now keywords. INCOMPATIBILITY, use double |
|
907 |
quotes. |
|
19814
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
908 |
|
23888
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
909 |
* Theory loader: be more serious about observing the static theory |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
910 |
header specifications (including optional directories), but not the |
24172
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
911 |
accidental file locations of previously successful loads. The strict |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
912 |
update policy of former update_thy is now already performed by |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
913 |
use_thy, so the former has been removed; use_thys updates several |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
914 |
theories simultaneously, just as 'imports' within a theory header |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
915 |
specification, but without merging the results. Potential |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
916 |
INCOMPATIBILITY: may need to refine theory headers and commands |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
917 |
ROOT.ML which depend on load order. |
23888
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
918 |
|
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
919 |
* Theory loader: optional support for content-based file |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
920 |
identification, instead of the traditional scheme of full physical |
23889 | 921 |
path plus date stamp; configured by the ISABELLE_FILE_IDENT setting |
23888
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
922 |
(cf. the system manual). The new scheme allows to work with |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
923 |
non-finished theories in persistent session images, such that source |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
924 |
files may be moved later on without requiring reloads. |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
925 |
|
24187
8bdf5ca5871f
* Theory loader: old-style ML proof scripts are considered a legacy feature;
wenzelm
parents:
24172
diff
changeset
|
926 |
* Theory loader: old-style ML proof scripts being *attached* to a thy |
8bdf5ca5871f
* Theory loader: old-style ML proof scripts are considered a legacy feature;
wenzelm
parents:
24172
diff
changeset
|
927 |
file (with the same base name as the theory) are considered a legacy |
24800 | 928 |
feature, which will disappear eventually. Even now, the theory loader |
929 |
no longer maintains dependencies on such files. |
|
930 |
||
931 |
* Syntax: the scope for resolving ambiguities via type-inference is |
|
932 |
now limited to individual terms, instead of whole simultaneous |
|
24234
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
933 |
specifications as before. This greatly reduces the complexity of the |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
934 |
syntax module and improves flexibility by separating parsing and |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
935 |
type-checking. INCOMPATIBILITY: additional type-constraints (explicit |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
936 |
'fixes' etc.) are required in rare situations. |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
937 |
|
25034 | 938 |
* Syntax: constants introduced by new-style packages ('definition', |
939 |
'abbreviation' etc.) are passed through the syntax module in |
|
940 |
``authentic mode''. This means that associated mixfix annotations |
|
941 |
really stick to such constants, independently of potential name space |
|
942 |
ambiguities introduced later on. INCOMPATIBILITY: constants in parse |
|
943 |
trees are represented slightly differently, may need to adapt syntax |
|
944 |
translations accordingly. Use CONST marker in 'translations' and |
|
945 |
@{const_syntax} antiquotation in 'parse_translation' etc. |
|
946 |
||
17981
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
947 |
* Legacy goal package: reduced interface to the bare minimum required |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
948 |
to keep existing proof scripts running. Most other user-level |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
949 |
functions are now part of the OldGoals structure, which is *not* open |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
950 |
by default (consider isatool expandshort before open OldGoals). |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
951 |
Removed top_sg, prin, printyp, pprint_term/typ altogether, because |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
952 |
these tend to cause confusion about the actual goal (!) context being |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
953 |
used here, which is not necessarily the same as the_context(). |
17918
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
954 |
|
23379
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
955 |
* Command 'find_theorems': supports "*" wild-card in "name:" |
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
956 |
criterion; "with_dups" option. Certain ProofGeneral versions might |
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
957 |
support a specific search form (see ProofGeneral/CHANGES). |
22965 | 958 |
|
20370 | 959 |
* The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1 |
960 |
by default, which means that "prems" (and also "fixed variables") are |
|
961 |
suppressed from proof state output. Note that the ProofGeneral |
|
962 |
settings mechanism allows to change and save options persistently, but |
|
963 |
older versions of Isabelle will fail to start up if a negative prems |
|
964 |
limit is imposed. |
|
965 |
||
21308
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
966 |
* Local theory targets may be specified by non-nested blocks of |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
967 |
``context/locale/class ... begin'' followed by ``end''. The body may |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
968 |
contain definitions, theorems etc., including any derived mechanism |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
969 |
that has been implemented on top of these primitives. This concept |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
970 |
generalizes the existing ``theorem (in ...)'' towards more versatility |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
971 |
and scalability. |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
972 |
|
21960
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
973 |
* Proof General interface: proper undo of final 'end' command; |
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
974 |
discontinued Isabelle/classic mode (ML proof scripts). |
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
975 |
|
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
976 |
|
17865 | 977 |
*** Document preparation *** |
978 |
||
21717 | 979 |
* Added antiquotation @{theory name} which prints the given name, |
980 |
after checking that it refers to a valid ancestor theory in the |
|
981 |
current context. |
|
21339 | 982 |
|
17869 | 983 |
* Added antiquotations @{ML_type text} and @{ML_struct text} which |
984 |
check the given source text as ML type/structure, printing verbatim. |
|
17865 | 985 |
|
21717 | 986 |
* Added antiquotation @{abbrev "c args"} which prints the abbreviation |
987 |
"c args == rhs" given in the current context. (Any number of |
|
21735 | 988 |
arguments may be given on the LHS.) |
21717 | 989 |
|
990 |
||
17779 | 991 |
*** Pure *** |
992 |
||
24800 | 993 |
* The 'class' package offers a combination of axclass and locale to |
25129 | 994 |
achieve Haskell-like type classes in Isabelle. Definitions and |
995 |
theorems within a class context produce both relative results (with |
|
996 |
implicit parameters according to the locale context), and polymorphic |
|
997 |
constants with qualified polymorphism (according to the class |
|
998 |
context). Within the body context of a 'class' target, a separate |
|
999 |
syntax layer ("user space type system") takes care of converting |
|
1000 |
between global polymorphic consts and internal locale representation. |
|
25177 | 1001 |
See src/HOL/ex/Classpackage.thy for examples (as well as main HOL). |
25184 | 1002 |
"isatool doc classes" provides a tutorial. |
20807 | 1003 |
|
25199 | 1004 |
* Generic code generator framework allows to generate executable |
24800 | 1005 |
code for ML and Haskell (including Isabelle classes). A short usage |
1006 |
sketch: |
|
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
1007 |
|
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
1008 |
internal compilation: |
25199 | 1009 |
export_code <list of constants (term syntax)> in SML |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1010 |
writing SML code to a file: |
25199 | 1011 |
export_code <list of constants (term syntax)> in SML <filename> |
22735 | 1012 |
writing OCaml code to a file: |
25199 | 1013 |
export_code <list of constants (term syntax)> in OCaml <filename> |
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
1014 |
writing Haskell code to a bunch of files: |
25199 | 1015 |
export_code <list of constants (term syntax)> in Haskell <filename> |
1016 |
||
1017 |
evaluating closed propositions to True/False using code generation: |
|
25184 | 1018 |
method ``eval'' |
1019 |
||
1020 |
Reasonable default setup of framework in HOL. |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1021 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1022 |
Theorem attributs for selecting and transforming function equations theorems: |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1023 |
|
22845 | 1024 |
[code fun]: select a theorem as function equation for a specific constant |
1025 |
[code fun del]: deselect a theorem as function equation for a specific constant |
|
1026 |
[code inline]: select an equation theorem for unfolding (inlining) in place |
|
1027 |
[code inline del]: deselect an equation theorem for unfolding (inlining) in place |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1028 |
|
22735 | 1029 |
User-defined serializations (target in {SML, OCaml, Haskell}): |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1030 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1031 |
code_const <and-list of constants (term syntax)> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1032 |
{(target) <and-list of const target syntax>}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1033 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1034 |
code_type <and-list of type constructors> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1035 |
{(target) <and-list of type target syntax>}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1036 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1037 |
code_instance <and-list of instances> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1038 |
{(target)}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1039 |
where instance ::= <type constructor> :: <class> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1040 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1041 |
code_class <and_list of classes> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1042 |
{(target) <and-list of class target syntax>}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1043 |
where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}? |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1044 |
|
25199 | 1045 |
code_instance and code_class only are effective to target Haskell. |
22735 | 1046 |
|
25177 | 1047 |
For example usage see src/HOL/ex/Codegenerator.thy and |
1048 |
src/HOL/ex/Codegenerator_Pretty.thy. A separate tutorial on code |
|
24800 | 1049 |
generation from Isabelle/HOL theories is available via "isatool doc |
1050 |
codegen". |
|
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
1051 |
|
25129 | 1052 |
* Code generator: consts in 'consts_code' Isar commands are now |
1053 |
referred to by usual term syntax (including optional type |
|
1054 |
annotations). |
|
1055 |
||
19254 | 1056 |
* Command 'no_translations' removes translation rules from theory |
1057 |
syntax. |
|
1058 |
||
19625
285771cec083
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
wenzelm
parents:
19587
diff
changeset
|
1059 |
* Overloaded definitions are now actually checked for acyclic |
19714 | 1060 |
dependencies. The overloading scheme is slightly more general than |
1061 |
that of Haskell98, although Isabelle does not demand an exact |
|
1062 |
correspondence to type class and instance declarations. |
|
1063 |
INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more |
|
1064 |
exotic versions of overloading -- at the discretion of the user! |
|
19711 | 1065 |
|
1066 |
Polymorphic constants are represented via type arguments, i.e. the |
|
1067 |
instantiation that matches an instance against the most general |
|
1068 |
declaration given in the signature. For example, with the declaration |
|
1069 |
c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented |
|
1070 |
as c(nat). Overloading is essentially simultaneous structural |
|
1071 |
recursion over such type arguments. Incomplete specification patterns |
|
19714 | 1072 |
impose global constraints on all occurrences, e.g. c('a * 'a) on the |
19715 | 1073 |
LHS means that more general c('a * 'b) will be disallowed on any RHS. |
19714 | 1074 |
Command 'print_theory' outputs the normalized system of recursive |
1075 |
equations, see section "definitions". |
|
19625
285771cec083
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
wenzelm
parents:
19587
diff
changeset
|
1076 |
|
24086 | 1077 |
* Configuration options are maintained within the theory or proof |
1078 |
context (with name and type bool/int/string), providing a very simple |
|
1079 |
interface to a poor-man's version of general context data. Tools may |
|
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1080 |
declare options in ML (e.g. using Attrib.config_int) and then refer to |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1081 |
these values using Config.get etc. Users may change options via an |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1082 |
associated attribute of the same name. This form of context |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1083 |
declaration works particularly well with commands 'declare' or |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1084 |
'using', for example ``declare [[foo = 42]]''. Thus it has become |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1085 |
very easy to avoid global references, which would not observe Isar |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1086 |
toplevel undo/redo and fail to work with multithreading. |
24086 | 1087 |
|
24172
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1088 |
Various global ML references of Pure and HOL have been turned into |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1089 |
configuration options: |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1090 |
|
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1091 |
Unify.search_bound unify_search_bound |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1092 |
Unify.trace_bound unify_trace_bound |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1093 |
Unify.trace_simp unify_trace_simp |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1094 |
Unify.trace_types unify_trace_types |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1095 |
Simplifier.simp_depth_limit simp_depth_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1096 |
Blast.depth_limit blast_depth_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1097 |
DatatypeProp.dtK datatype_distinctness_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1098 |
fast_arith_neq_limit fast_arith_neq_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1099 |
fast_arith_split_limit fast_arith_split_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1100 |
|
24086 | 1101 |
* Named collections of theorems may be easily installed as context |
24800 | 1102 |
data using the functor NamedThmsFun (see also |
24086 | 1103 |
src/Pure/Tools/named_thms.ML). The user may add or delete facts via |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1104 |
attributes; there is also a toplevel print command. This facility is |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1105 |
just a common case of general context data, which is the preferred way |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1106 |
for anything more complex than just a list of facts in canonical |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1107 |
order. |
24086 | 1108 |
|
24032 | 1109 |
* Isar: command 'declaration' augments a local theory by generic |
1110 |
declaration functions written in ML. This enables arbitrary content |
|
1111 |
being added to the context, depending on a morphism that tells the |
|
1112 |
difference of the original declaration context wrt. the application |
|
1113 |
context encountered later on. |
|
1114 |
||
1115 |
* Isar: proper interfaces for simplification procedures. Command |
|
1116 |
'simproc_setup' declares named simprocs (with match patterns, and body |
|
1117 |
text in ML). Attribute "simproc" adds/deletes simprocs in the current |
|
1118 |
context. ML antiquotation @{simproc name} retrieves named simprocs. |
|
1119 |
||
1120 |
* Isar: an extra pair of brackets around attribute declarations |
|
1121 |
abbreviates a theorem reference involving an internal dummy fact, |
|
1122 |
which will be ignored later --- only the effect of the attribute on |
|
1123 |
the background context will persist. This form of in-place |
|
1124 |
declarations is particularly useful with commands like 'declare' and |
|
1125 |
'using', for example ``have A using [[simproc a]] by simp''. |
|
1126 |
||
23369
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1127 |
* Isar: method "assumption" (and implicit closing of subproofs) now |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1128 |
takes simple non-atomic goal assumptions into account: after applying |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1129 |
an assumption as a rule the resulting subgoals are solved by atomic |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1130 |
assumption steps. This is particularly useful to finish 'obtain' |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1131 |
goals, such as "!!x. (!!x. P x ==> thesis) ==> P x ==> thesis", |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1132 |
without referring to the original premise "!!x. P x ==> thesis" in the |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1133 |
Isar proof context. POTENTIAL INCOMPATIBILITY: method "assumption" is |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1134 |
more permissive. |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1135 |
|
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1136 |
* Isar: implicit use of prems from the Isar proof context is |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1137 |
considered a legacy feature. Common applications like ``have A .'' |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1138 |
may be replaced by ``have A by fact'' or ``note `A`''. In general, |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1139 |
referencing facts explicitly here improves readability and |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1140 |
maintainability of proof texts. |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1141 |
|
17865 | 1142 |
* Isar: improper proof element 'guess' is like 'obtain', but derives |
1143 |
the obtained context from the course of reasoning! For example: |
|
1144 |
||
1145 |
assume "EX x y. A x & B y" -- "any previous fact" |
|
1146 |
then guess x and y by clarify |
|
1147 |
||
1148 |
This technique is potentially adventurous, depending on the facts and |
|
1149 |
proof tools being involved here. |
|
1150 |
||
18020 | 1151 |
* Isar: known facts from the proof context may be specified as literal |
1152 |
propositions, using ASCII back-quote syntax. This works wherever |
|
1153 |
named facts used to be allowed so far, in proof commands, proof |
|
1154 |
methods, attributes etc. Literal facts are retrieved from the context |
|
1155 |
according to unification of type and term parameters. For example, |
|
1156 |
provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known |
|
1157 |
theorems in the current context, then these are valid literal facts: |
|
1158 |
`A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc. |
|
1159 |
||
1160 |
There is also a proof method "fact" which does the same composition |
|
18044 | 1161 |
for explicit goal states, e.g. the following proof texts coincide with |
1162 |
certain special cases of literal facts: |
|
18020 | 1163 |
|
1164 |
have "A" by fact == note `A` |
|
1165 |
have "A ==> B" by fact == note `A ==> B` |
|
1166 |
have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` |
|
1167 |
have "P a ==> Q a" by fact == note `P a ==> Q a` |
|
1168 |
||
20118
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
1169 |
* Isar: ":" (colon) is no longer a symbolic identifier character in |
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
1170 |
outer syntax. Thus symbolic identifiers may be used without |
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
1171 |
additional white space in declarations like this: ``assume *: A''. |
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
1172 |
|
20013 | 1173 |
* Isar: 'print_facts' prints all local facts of the current context, |
1174 |
both named and unnamed ones. |
|
1175 |
||
18308 | 1176 |
* Isar: 'def' now admits simultaneous definitions, e.g.: |
1177 |
||
1178 |
def x == "t" and y == "u" |
|
1179 |
||
18540 | 1180 |
* Isar: added command 'unfolding', which is structurally similar to |
1181 |
'using', but affects both the goal state and facts by unfolding given |
|
18815
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1182 |
rewrite rules. Thus many occurrences of the 'unfold' method or |
18540 | 1183 |
'unfolded' attribute may be replaced by first-class proof text. |
1184 |
||
18815
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1185 |
* Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded', |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1186 |
and command 'unfolding' now all support object-level equalities |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1187 |
(potentially conditional). The underlying notion of rewrite rule is |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1188 |
analogous to the 'rule_format' attribute, but *not* that of the |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1189 |
Simplifier (which is usually more generous). |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1190 |
|
24238 | 1191 |
* Isar: the new attribute [rotated n] (default n = 1) rotates the |
1192 |
premises of a theorem by n. Useful in conjunction with drule. |
|
1193 |
||
19220 | 1194 |
* Isar: the goal restriction operator [N] (default N = 1) evaluates a |
1195 |
method expression within a sandbox consisting of the first N |
|
19240 | 1196 |
sub-goals, which need to exist. For example, ``simp_all [3]'' |
1197 |
simplifies the first three sub-goals, while (rule foo, simp_all)[] |
|
1198 |
simplifies all new goals that emerge from applying rule foo to the |
|
1199 |
originally first one. |
|
19220 | 1200 |
|
19814
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
1201 |
* Isar: schematic goals are no longer restricted to higher-order |
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
1202 |
patterns; e.g. ``lemma "?P(?x)" by (rule TrueI)'' now works as |
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
1203 |
expected. |
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
1204 |
|
18901 | 1205 |
* Isar: the conclusion of a long theorem statement is now either |
1206 |
'shows' (a simultaneous conjunction, as before), or 'obtains' |
|
1207 |
(essentially a disjunction of cases with local parameters and |
|
1208 |
assumptions). The latter allows to express general elimination rules |
|
18910 | 1209 |
adequately; in this notation common elimination rules look like this: |
18901 | 1210 |
|
1211 |
lemma exE: -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis" |
|
1212 |
assumes "EX x. P x" |
|
1213 |
obtains x where "P x" |
|
1214 |
||
1215 |
lemma conjE: -- "A & B ==> (A ==> B ==> thesis) ==> thesis" |
|
1216 |
assumes "A & B" |
|
1217 |
obtains A and B |
|
1218 |
||
1219 |
lemma disjE: -- "A | B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis" |
|
1220 |
assumes "A | B" |
|
1221 |
obtains |
|
1222 |
A |
|
1223 |
| B |
|
1224 |
||
18910 | 1225 |
The subsequent classical rules even refer to the formal "thesis" |
18901 | 1226 |
explicitly: |
1227 |
||
1228 |
lemma classical: -- "(~ thesis ==> thesis) ==> thesis" |
|
1229 |
obtains "~ thesis" |
|
1230 |
||
18910 | 1231 |
lemma Peirce's_Law: -- "((thesis ==> something) ==> thesis) ==> thesis" |
1232 |
obtains "thesis ==> something" |
|
18901 | 1233 |
|
1234 |
The actual proof of an 'obtains' statement is analogous to that of the |
|
18910 | 1235 |
Isar proof element 'obtain', only that there may be several cases. |
1236 |
Optional case names may be specified in parentheses; these will be |
|
1237 |
available both in the present proof and as annotations in the |
|
1238 |
resulting rule, for later use with the 'cases' method (cf. attribute |
|
1239 |
case_names). |
|
18901 | 1240 |
|
21447
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
1241 |
* Isar: the assumptions of a long theorem statement are available as |
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
1242 |
"assms" fact in the proof context. This is more appropriate than the |
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
1243 |
(historical) "prems", which refers to all assumptions of the current |
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
1244 |
context, including those from the target locale, proof body etc. |
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
1245 |
|
19263 | 1246 |
* Isar: 'print_statement' prints theorems from the current theory or |
1247 |
proof context in long statement form, according to the syntax of a |
|
1248 |
top-level lemma. |
|
1249 |
||
18901 | 1250 |
* Isar: 'obtain' takes an optional case name for the local context |
1251 |
introduction rule (default "that"). |
|
1252 |
||
19587 | 1253 |
* Isar: removed obsolete 'concl is' patterns. INCOMPATIBILITY, use |
1254 |
explicit (is "_ ==> ?foo") in the rare cases where this still happens |
|
1255 |
to occur. |
|
1256 |
||
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1257 |
* Pure: syntax "CONST name" produces a fully internalized constant |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1258 |
according to the current context. This is particularly useful for |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1259 |
syntax translations that should refer to internal constant |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1260 |
representations independently of name spaces. |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1261 |
|
21537
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
1262 |
* Pure: syntax constant for foo (binder "FOO ") is called "foo_binder" |
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
1263 |
instead of "FOO ". This allows multiple binder declarations to coexist |
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
1264 |
in the same context. INCOMPATIBILITY. |
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
1265 |
|
21209
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset
|
1266 |
* Isar/locales: 'notation' provides a robust interface to the 'syntax' |
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset
|
1267 |
primitive that also works in a locale context (both for constants and |
24950 | 1268 |
fixed variables). Type declaration and internal syntactic representation |
1269 |
of given constants retrieved from the context. Likewise, the |
|
1270 |
'no_notation' command allows to remove given syntax annotations from the |
|
1271 |
current context. |
|
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1272 |
|
19665 | 1273 |
* Isar/locales: new derived specification elements 'axiomatization', |
1274 |
'definition', 'abbreviation', which support type-inference, admit |
|
19083 | 1275 |
object-level specifications (equality, equivalence). See also the |
1276 |
isar-ref manual. Examples: |
|
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset
|
1277 |
|
19665 | 1278 |
axiomatization |
21595 | 1279 |
eq (infix "===" 50) where |
1280 |
eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y" |
|
1281 |
||
1282 |
definition "f x y = x + y + 1" |
|
1283 |
definition g where "g x = f x x" |
|
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset
|
1284 |
|
19363 | 1285 |
abbreviation |
21595 | 1286 |
neq (infix "=!=" 50) where |
19363 | 1287 |
"x =!= y == ~ (x === y)" |
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset
|
1288 |
|
19083 | 1289 |
These specifications may be also used in a locale context. Then the |
1290 |
constants being introduced depend on certain fixed parameters, and the |
|
1291 |
constant name is qualified by the locale base name. An internal |
|
1292 |
abbreviation takes care for convenient input and output, making the |
|
19088 | 1293 |
parameters implicit and using the original short name. See also |
25177 | 1294 |
src/HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic |
19083 | 1295 |
entities from a monomorphic theory. |
1296 |
||
1297 |
Presently, abbreviations are only available 'in' a target locale, but |
|
19363 | 1298 |
not inherited by general import expressions. Also note that |
1299 |
'abbreviation' may be used as a type-safe replacement for 'syntax' + |
|
24735
3a55ee2cae70
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm
parents:
24706
diff
changeset
|
1300 |
'translations' in common applications. The "no_abbrevs" print mode |
3a55ee2cae70
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm
parents:
24706
diff
changeset
|
1301 |
prevents folding of abbreviations in term output. |
19084 | 1302 |
|
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1303 |
Concrete syntax is attached to specified constants in internal form, |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1304 |
independently of name spaces. The parse tree representation is |
21209
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset
|
1305 |
slightly different -- use 'notation' instead of raw 'syntax', and |
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1306 |
'translations' with explicit "CONST" markup to accommodate this. |
19665 | 1307 |
|
24800 | 1308 |
* Pure/Isar: unified syntax for new-style specification mechanisms |
1309 |
(e.g. 'definition', 'abbreviation', or 'inductive' in HOL) admits |
|
1310 |
full type inference and dummy patterns ("_"). For example: |
|
24735
3a55ee2cae70
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm
parents:
24706
diff
changeset
|
1311 |
|
3a55ee2cae70
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm
parents:
24706
diff
changeset
|
1312 |
definition "K x _ = x" |
3a55ee2cae70
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm
parents:
24706
diff
changeset
|
1313 |
|
24738 | 1314 |
inductive conj for A B |
1315 |
where "A ==> B ==> conj A B" |
|
1316 |
||
21735 | 1317 |
* Pure: command 'print_abbrevs' prints all constant abbreviations of |
1318 |
the current context. Print mode "no_abbrevs" prevents inversion of |
|
1319 |
abbreviations on output. |
|
1320 |
||
24800 | 1321 |
* Isar/locales: improved parameter handling: use of locales "var" and |
1322 |
"struct" no longer necessary; - parameter renamings are no longer |
|
1323 |
required to be injective. For example, this allows to define |
|
1324 |
endomorphisms as locale endom = homom mult mult h. |
|
19783 | 1325 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1326 |
* Isar/locales: changed the way locales with predicates are defined. |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1327 |
Instead of accumulating the specification, the imported expression is |
22126 | 1328 |
now an interpretation. INCOMPATIBILITY: different normal form of |
1329 |
locale expressions. In particular, in interpretations of locales with |
|
1330 |
predicates, goals repesenting already interpreted fragments are not |
|
1331 |
removed automatically. Use methods `intro_locales' and |
|
1332 |
`unfold_locales'; see below. |
|
1333 |
||
1334 |
* Isar/locales: new methods `intro_locales' and `unfold_locales' |
|
1335 |
provide backward reasoning on locales predicates. The methods are |
|
1336 |
aware of interpretations and discharge corresponding goals. |
|
1337 |
`intro_locales' is less aggressive then `unfold_locales' and does not |
|
1338 |
unfold predicates to assumptions. |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1339 |
|
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1340 |
* Isar/locales: the order in which locale fragments are accumulated |
22126 | 1341 |
has changed. This enables to override declarations from fragments due |
1342 |
to interpretations -- for example, unwanted simp rules. |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1343 |
|
23920 | 1344 |
* Isar/locales: interpretation in theories and proof contexts has been |
1345 |
extended. One may now specify (and prove) equations, which are |
|
1346 |
unfolded in interpreted theorems. This is useful for replacing |
|
1347 |
defined concepts (constants depending on locale parameters) by |
|
1348 |
concepts already existing in the target context. Example: |
|
1349 |
||
1350 |
interpretation partial_order ["op <= :: [int, int] => bool"] |
|
1351 |
where "partial_order.less (op <=) (x::int) y = (x < y)" |
|
1352 |
||
24800 | 1353 |
Typically, the constant `partial_order.less' is created by a |
1354 |
definition specification element in the context of locale |
|
1355 |
partial_order. |
|
1356 |
||
24859 | 1357 |
* Method "induct": improved internal context management to support |
24800 | 1358 |
local fixes and defines on-the-fly. Thus explicit meta-level |
1359 |
connectives !! and ==> are rarely required anymore in inductive goals |
|
1360 |
(using object-logic connectives for this purpose has been long |
|
1361 |
obsolete anyway). Common proof patterns are explained in |
|
25177 | 1362 |
src/HOL/Induct/Common_Patterns.thy, see also |
1363 |
src/HOL/Isar_examples/Puzzle.thy and src/HOL/Lambda for realistic |
|
1364 |
examples. |
|
24606
7acbb982fc77
moved induct patterns to HOL/Induct/Common_Patterns.thy;
wenzelm
parents:
24507
diff
changeset
|
1365 |
|
24859 | 1366 |
* Method "induct": improved handling of simultaneous goals. Instead of |
24606
7acbb982fc77
moved induct patterns to HOL/Induct/Common_Patterns.thy;
wenzelm
parents:
24507
diff
changeset
|
1367 |
introducing object-level conjunction, the statement is now split into |
7acbb982fc77
moved induct patterns to HOL/Induct/Common_Patterns.thy;
wenzelm
parents:
24507
diff
changeset
|
1368 |
several conclusions, while the corresponding symbolic cases are nested |
7acbb982fc77
moved induct patterns to HOL/Induct/Common_Patterns.thy;
wenzelm
parents:
24507
diff
changeset
|
1369 |
accordingly. INCOMPATIBILITY, proofs need to be structured explicitly, |
25177 | 1370 |
see src/HOL/Induct/Common_Patterns.thy, for example. |
24606
7acbb982fc77
moved induct patterns to HOL/Induct/Common_Patterns.thy;
wenzelm
parents:
24507
diff
changeset
|
1371 |
|
24859 | 1372 |
* Method "induct": mutual induction rules are now specified as a list |
24800 | 1373 |
of rule sharing the same induction cases. HOL packages usually provide |
24606
7acbb982fc77
moved induct patterns to HOL/Induct/Common_Patterns.thy;
wenzelm
parents:
24507
diff
changeset
|
1374 |
foo_bar.inducts for mutually defined items foo and bar (e.g. inductive |
24859 | 1375 |
predicates/sets or datatypes). INCOMPATIBILITY, users need to specify |
1376 |
mutual induction rules differently, i.e. like this: |
|
18506
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
1377 |
|
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
1378 |
(induct rule: foo_bar.inducts) |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
1379 |
(induct set: foo bar) |
24859 | 1380 |
(induct pred: foo bar) |
18506
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
1381 |
(induct type: foo bar) |