author | haftmann |
Fri, 18 Jul 2008 18:25:53 +0200 | |
changeset 27651 | 16a26996c30e |
parent 27599 | ca23ef50c178 |
child 27681 | 8cedebf55539 |
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 |
||
9 |
* Generalized Isar history, with support for linear undo, direct state |
|
10 |
addressing etc. |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
11 |
|
27191 | 12 |
* Recovered hiding of consts, which was accidentally broken in |
13 |
Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really |
|
14 |
makes c inaccessible; consider using ``hide (open) const c'' instead. |
|
15 |
||
27599 | 16 |
* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
17 |
interface instead. |
|
18 |
||
19 |
||
20 |
*** Pure *** |
|
21 |
||
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
22 |
* Command 'instance': attached definitions no longer accepted. |
27141
9bfcdb1905e1
* Attributes cases, induct, coinduct support del option.
wenzelm
parents:
27122
diff
changeset
|
23 |
INCOMPATIBILITY, use proper 'instantiation' target. |
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
24 |
|
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
25 |
* 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
|
26 |
|
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
27 |
|
27381 | 28 |
*** Document preparation *** |
29 |
||
30 |
* Antiquotation @{lemma} now imitates a regular terminal proof, |
|
27392 | 31 |
demanding keyword 'by' and supporting the full method expression |
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
32 |
syntax just like the Isar command 'by'. |
27381 | 33 |
|
34 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
35 |
*** HOL *** |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
36 |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
37 |
* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been moved |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
38 |
to separate class dvd in Ring_and_Field; a couple of lemmas on dvd has been |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
39 |
generalized to class comm_semiring_1. Likewise a bunch of lemmas from Divides |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
40 |
has been generalized from nat to class semiring_div. INCOMPATIBILITY. |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
41 |
This involves the following theorem renames resulting from duplicate elimination: |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
42 |
|
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
43 |
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
|
44 |
zero_dvd_iff ~> dvd_0_left_iff |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
45 |
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
|
46 |
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
|
47 |
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
|
48 |
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
|
49 |
|
27599 | 50 |
* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, |
51 |
zlcm (for int); carried together from various gcd/lcm developements in |
|
52 |
the HOL Distribution. zgcd and zlcm replace former igcd and ilcm; |
|
53 |
corresponding theorems renamed accordingly. INCOMPATIBILY. To |
|
54 |
recover tupled syntax, use syntax declarations like: |
|
27556 | 55 |
|
56 |
hide (open) const gcd |
|
57 |
abbreviation gcd where |
|
58 |
"gcd == (%(a, b). GCD.gcd a b)" |
|
59 |
notation (output) |
|
60 |
GCD.gcd ("gcd '(_, _')") |
|
61 |
||
62 |
(analogously for lcm, zgcd, zlcm). |
|
63 |
||
64 |
* HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. |
|
27551 | 65 |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
66 |
* 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
|
67 |
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
|
68 |
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
|
69 |
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
|
70 |
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
|
71 |
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
|
72 |
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
|
73 |
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
|
74 |
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
|
75 |
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
|
76 |
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
|
77 |
directly in that cases. |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
78 |
|
27424 | 79 |
* Integrated image HOL-Complex with HOL. Entry points Main.thy and |
80 |
Complex_Main.thy remain as they are. |
|
81 |
||
27599 | 82 |
* New image HOL-Plain provides a minimal HOL with the most important |
83 |
tools available (inductive, datatype, primrec, ...). By convention |
|
84 |
the corresponding theory Plain should be ancestor of every further |
|
85 |
(library) theory. Some library theories now have ancestor Plain |
|
86 |
(instead of Main), thus theory Main occasionally has to be imported |
|
87 |
explicitly. |
|
27421 | 88 |
|
27324
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
89 |
* 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
|
90 |
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
|
91 |
corresponding "cases" and "induct" attributes. Mutual induction rules |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
92 |
are now presented as a list of individual projections |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
93 |
(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
|
94 |
explicit HOL conjunction is no longer supported. INCOMPATIBILITY, in |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
95 |
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
|
96 |
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
|
97 |
rule: prod.exhaust) here. |
27122 | 98 |
|
27141
9bfcdb1905e1
* Attributes cases, induct, coinduct support del option.
wenzelm
parents:
27122
diff
changeset
|
99 |
* Attributes "cases", "induct", "coinduct" support "del" option. |
9bfcdb1905e1
* Attributes cases, induct, coinduct support del option.
wenzelm
parents:
27122
diff
changeset
|
100 |
|
27122 | 101 |
* Removed fact "case_split_thm", which duplicates "case_split". |
102 |
||
103 |
* Command 'rep_datatype': instead of theorem names the command now |
|
104 |
takes a list of terms denoting the constructors of the type to be |
|
105 |
represented as datatype. The characteristic theorems have to be |
|
106 |
proven. INCOMPATIBILITY. Also observe that the following theorems |
|
107 |
have disappeared in favour of existing ones: |
|
108 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
109 |
unit_induct ~> unit.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
110 |
prod_induct ~> prod.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
111 |
sum_induct ~> sum.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
112 |
Suc_Suc_eq ~> nat.inject |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
113 |
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
|
114 |
|
27122 | 115 |
* Library/Nat_Infinity: added addition, numeral syntax and more |
116 |
instantiations for algebraic structures. Removed some duplicate |
|
117 |
theorems. Changes in simp rules. INCOMPATIBILITY. |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
118 |
|
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
119 |
|
27485 | 120 |
*** HOL-NSA *** |
121 |
||
122 |
* Created new image HOL-NSA, containing theories of nonstandard |
|
123 |
analysis which were previously part of HOL-Complex. Entry point |
|
124 |
Hyperreal.thy remains valid, but theories formerly using |
|
125 |
Complex_Main.thy should now use new entry point Hypercomplex.thy. |
|
126 |
||
127 |
||
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
128 |
*** ML *** |
27436 | 129 |
|
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
130 |
* 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
|
131 |
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
|
132 |
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
|
133 |
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
|
134 |
thereof. INCOMPATIBILITY. |
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
135 |
|
27287 | 136 |
* Disposed old type and term read functions (Sign.read_def_typ, |
137 |
Sign.read_typ, Sign.read_def_terms, Sign.read_term, |
|
138 |
Thm.read_def_cterms, Thm.read_cterm etc.). INCOMPATIBILITY, should |
|
139 |
use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global, |
|
27269 | 140 |
Syntax.read_term_global etc.; see also OldGoals.read_term as last |
141 |
resort for legacy applications. |
|
142 |
||
27380 | 143 |
* Antiquotations: block-structured compilation context indicated by |
27391 | 144 |
\<lbrace> ... \<rbrace>; additional antiquotation forms: |
145 |
||
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
146 |
@{let ?pat = term} - term abbreviation (HO matching) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
147 |
@{note name = fact} - fact abbreviation |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
148 |
@{thm fact} - singleton fact (with attributes) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
149 |
@{thms fact} - general fact (with attributes) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
150 |
@{lemma prop by method} - singleton goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
151 |
@{lemma prop by meth1 meth2} - singleton goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
152 |
@{lemma prop1 ... propN by method} - general goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
153 |
@{lemma prop1 ... propN by meth1 meth2} - general goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
154 |
@{lemma (open) ...} - open derivation |
27380 | 155 |
|
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
156 |
|
27143 | 157 |
|
27008 | 158 |
New in Isabelle2008 (June 2008) |
159 |
------------------------------- |
|
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
160 |
|
25522 | 161 |
*** General *** |
162 |
||
27061 | 163 |
* The Isabelle/Isar Reference Manual (isar-ref) has been reorganized |
164 |
and updated, with formally checked references as hyperlinks. |
|
165 |
||
25994 | 166 |
* Theory loader: use_thy (and similar operations) no longer set the |
167 |
implicit ML context, which was occasionally hard to predict and in |
|
168 |
conflict with concurrency. INCOMPATIBILITY, use ML within Isar which |
|
169 |
provides a proper context already. |
|
170 |
||
26323
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
171 |
* Theory loader: old-style ML proof scripts being *attached* to a thy |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
172 |
file are no longer supported. INCOMPATIBILITY, regular 'uses' and |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
173 |
'use' within a theory file will do the job. |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
174 |
|
26650 | 175 |
* Name space merge now observes canonical order, i.e. the second space |
176 |
is inserted into the first one, while existing entries in the first |
|
26659 | 177 |
space take precedence. INCOMPATIBILITY in rare situations, may try to |
26650 | 178 |
swap theory imports. |
179 |
||
27067 | 180 |
* Syntax: symbol \<chi> is now considered a letter. Potential |
181 |
INCOMPATIBILITY in identifier syntax etc. |
|
182 |
||
183 |
* Outer syntax: string tokens no longer admit escaped white space, |
|
184 |
which was an accidental (undocumented) feature. INCOMPATIBILITY, use |
|
185 |
white space without escapes. |
|
186 |
||
187 |
* Outer syntax: string tokens may contain arbitrary character codes |
|
188 |
specified via 3 decimal digits (as in SML). E.g. "foo\095bar" for |
|
189 |
"foo_bar". |
|
190 |
||
25522 | 191 |
|
25502 | 192 |
*** Pure *** |
193 |
||
26718 | 194 |
* Context-dependent token translations. Default setup reverts locally |
195 |
fixed variables, and adds hilite markup for undeclared frees. |
|
196 |
||
26681 | 197 |
* Unused theorems can be found using the new command 'unused_thms'. |
198 |
There are three ways of invoking it: |
|
199 |
||
200 |
(1) unused_thms |
|
201 |
Only finds unused theorems in the current theory. |
|
202 |
||
203 |
(2) unused_thms thy_1 ... thy_n - |
|
204 |
Finds unused theorems in the current theory and all of its ancestors, |
|
205 |
excluding the theories thy_1 ... thy_n and all of their ancestors. |
|
206 |
||
207 |
(3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m |
|
208 |
Finds unused theorems in the theories thy'_1 ... thy'_m and all of |
|
209 |
their ancestors, excluding the theories thy_1 ... thy_n and all of |
|
210 |
their ancestors. |
|
211 |
||
26718 | 212 |
In order to increase the readability of the list produced by |
213 |
unused_thms, theorems that have been created by a particular instance |
|
26874 | 214 |
of a theory command such as 'inductive' or 'function' are considered |
215 |
to belong to the same "group", meaning that if at least one theorem in |
|
26718 | 216 |
this group is used, the other theorems in the same group are no longer |
217 |
reported as unused. Moreover, if all theorems in the group are |
|
218 |
unused, only one theorem in the group is displayed. |
|
219 |
||
220 |
Note that proof objects have to be switched on in order for |
|
221 |
unused_thms to work properly (i.e. !proofs must be >= 1, which is |
|
26874 | 222 |
usually the case when using Proof General with the default settings). |
26681 | 223 |
|
26650 | 224 |
* Authentic naming of facts disallows ad-hoc overwriting of previous |
225 |
theorems within the same name space. INCOMPATIBILITY, need to remove |
|
226 |
duplicate fact bindings, or even accidental fact duplications. Note |
|
227 |
that tools may maintain dynamically scoped facts systematically, using |
|
228 |
PureThy.add_thms_dynamic. |
|
229 |
||
26660 | 230 |
* Command 'hide' now allows to hide from "fact" name space as well. |
231 |
||
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
232 |
* Eliminated destructive theorem database, simpset, claset, and |
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
233 |
clasimpset. Potential INCOMPATIBILITY, really need to observe linear |
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
234 |
update of theories within ML code. |
26479 | 235 |
|
26955
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
236 |
* 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
|
237 |
INCOMPATIBILITY, object-logics depending on former Pure require |
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
238 |
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
|
239 |
depending on former CPure need to refer to Pure. |
26650 | 240 |
|
26495 | 241 |
* Commands 'use' and 'ML' are now purely functional, operating on |
26479 | 242 |
theory/local_theory. Removed former 'ML_setup' (on theory), use 'ML' |
243 |
instead. Added 'ML_val' as mere diagnostic replacement for 'ML'. |
|
244 |
INCOMPATIBILITY. |
|
245 |
||
26874 | 246 |
* Command 'setup': discontinued implicit version with ML reference. |
26434 | 247 |
|
25970
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
248 |
* Instantiation target allows for simultaneous specification of class |
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
249 |
instance operations together with an instantiation proof. |
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
250 |
Type-checking phase allows to refer to class operations uniformly. |
27067 | 251 |
See src/HOL/Complex/Complex.thy for an Isar example and |
252 |
src/HOL/Library/Eval.thy for an ML example. |
|
25502 | 253 |
|
26201
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
254 |
* Indexing of literal facts: be more serious about including only |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
255 |
facts from the visible specification/proof context, but not the |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
256 |
background context (locale etc.). Affects `prop` notation and method |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
257 |
"fact". INCOMPATIBILITY: need to name facts explicitly in rare |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
258 |
situations. |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
259 |
|
26925
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
260 |
* Method "cases", "induct", "coinduct": removed obsolete/undocumented |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
261 |
"(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
|
262 |
proof text. |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
263 |
|
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
264 |
* Isar statements: removed obsolete case "rule_context". |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
265 |
INCOMPATIBILITY, better use explicit fixes/assumes. |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
266 |
|
26874 | 267 |
* Locale proofs: default proof step now includes 'unfold_locales'; |
268 |
hence 'proof' without argument may be used to unfold locale |
|
269 |
predicates. |
|
26765 | 270 |
|
271 |
||
26762 | 272 |
*** Document preparation *** |
273 |
||
26914 | 274 |
* Simplified pdfsetup.sty: color/hyperref is used unconditionally for |
275 |
both pdf and dvi (hyperlinks usually work in xdvi as well); removed |
|
276 |
obsolete thumbpdf setup (contemporary PDF viewers do this on the |
|
277 |
spot); renamed link color from "darkblue" to "linkcolor" (default |
|
26920 | 278 |
value unchanged, can be redefined via \definecolor); no longer sets |
279 |
"a4paper" option (unnecessary or even intrusive). |
|
26914 | 280 |
|
27008 | 281 |
* Antiquotation @{lemma A method} proves proposition A by the given |
282 |
method (either a method name or a method name plus (optional) method |
|
283 |
arguments in parentheses) and prints A just like @{prop A}. |
|
26762 | 284 |
|
285 |
||
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
286 |
*** HOL *** |
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
287 |
|
27067 | 288 |
* New primrec package. Specification syntax conforms in style to |
289 |
definition/function/.... No separate induction rule is provided. The |
|
290 |
"primrec" command distinguishes old-style and new-style specifications |
|
291 |
by syntax. The former primrec package is now named OldPrimrecPackage. |
|
292 |
When adjusting theories, beware: constants stemming from new-style |
|
293 |
primrec specifications have authentic syntax. |
|
294 |
||
295 |
* Metis prover is now an order of magnitude faster, and also works |
|
296 |
with multithreading. |
|
297 |
||
298 |
* Metis: the maximum number of clauses that can be produced from a |
|
299 |
theorem is now given by the attribute max_clauses. Theorems that |
|
300 |
exceed this number are ignored, with a warning printed. |
|
301 |
||
302 |
* Sledgehammer no longer produces structured proofs by default. To |
|
303 |
enable, declare [[sledgehammer_full = true]]. Attributes |
|
304 |
reconstruction_modulus, reconstruction_sorts renamed |
|
305 |
sledgehammer_modulus, sledgehammer_sorts. INCOMPATIBILITY. |
|
306 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
307 |
* Method "induct_scheme" derives user-specified induction rules |
27067 | 308 |
from well-founded induction and completeness of patterns. This factors |
309 |
out some operations that are done internally by the function package |
|
310 |
and makes them available separately. See |
|
311 |
src/HOL/ex/Induction_Scheme.thy for examples. |
|
312 |
||
313 |
* More flexible generation of measure functions for termination |
|
314 |
proofs: Measure functions can be declared by proving a rule of the |
|
315 |
form "is_measure f" and giving it the [measure_function] attribute. |
|
316 |
The "is_measure" predicate is logically meaningless (always true), and |
|
317 |
just guides the heuristic. To find suitable measure functions, the |
|
318 |
termination prover sets up the goal "is_measure ?f" of the appropriate |
|
319 |
type and generates all solutions by prolog-style backwards proof using |
|
320 |
the declared rules. |
|
321 |
||
322 |
This setup also deals with rules like |
|
323 |
||
324 |
"is_measure f ==> is_measure (list_size f)" |
|
325 |
||
326 |
which accommodates nested datatypes that recurse through lists. |
|
327 |
Similar rules are predeclared for products and option types. |
|
328 |
||
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
329 |
* 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
|
330 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
331 |
INCOMPATIBILITIES: |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
332 |
|
27008 | 333 |
- Definitions of overloaded constants on sets have to be replaced by |
334 |
definitions on => and bool. |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
335 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
336 |
- Some definitions of overloaded operators on sets can now be proved |
27008 | 337 |
using the definitions of the operators on => and bool. Therefore, |
338 |
the following theorems have been renamed: |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
339 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
340 |
subset_def -> subset_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
341 |
psubset_def -> psubset_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
342 |
set_diff_def -> set_diff_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
343 |
Compl_def -> Compl_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
344 |
Sup_set_def -> Sup_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
345 |
Inf_set_def -> Inf_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
346 |
sup_set_def -> sup_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
347 |
inf_set_def -> inf_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
348 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
349 |
- 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
|
350 |
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
|
351 |
the unknowns in the rule is a set. |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
352 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
353 |
- Higher order unification and forward proofs: |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
354 |
The proof pattern |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
355 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
356 |
have "P (S::'a set)" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
357 |
then have "EX S. P S" .. |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
358 |
|
27008 | 359 |
no longer works (due to the incompleteness of the HO unification |
360 |
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
|
361 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
362 |
have "EX S. P S" |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
363 |
proof |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
364 |
show "P S" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
365 |
qed |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
366 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
367 |
- Calculational reasoning with subst (or similar rules): |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
368 |
The proof pattern |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
369 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
370 |
have "P (S::'a set)" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
371 |
also have "S = T" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
372 |
finally have "P T" . |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
373 |
|
27008 | 374 |
no longer works (for similar reasons as the previous example) and |
375 |
must be replaced by something like |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
376 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
377 |
have "P (S::'a set)" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
378 |
moreover have "S = T" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
379 |
ultimately have "P T" by simp |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
380 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
381 |
- Tactics or packages written in ML code: |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
382 |
Code performing pattern matching on types via |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
383 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
384 |
Type ("set", [T]) => ... |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
385 |
|
27008 | 386 |
must be rewritten. Moreover, functions like strip_type or |
387 |
binder_types no longer return the right value when applied to a |
|
388 |
type of the form |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
389 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
390 |
T1 => ... => Tn => U => bool |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
391 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
392 |
rather than |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
393 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
394 |
T1 => ... => Tn => U set |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
395 |
|
26874 | 396 |
* Merged theories Wellfounded_Recursion, Accessible_Part and |
27067 | 397 |
Wellfounded_Relations to theory Wellfounded. |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26724
diff
changeset
|
398 |
|
26513 | 399 |
* Explicit class "eq" for executable equality. INCOMPATIBILITY. |
400 |
||
26874 | 401 |
* Class finite no longer treats UNIV as class parameter. Use class |
402 |
enum from theory Library/Enum instead to achieve a similar effect. |
|
26445 | 403 |
INCOMPATIBILITY. |
404 |
||
26874 | 405 |
* Theory List: rule list_induct2 now has explicitly named cases "Nil" |
406 |
and "Cons". INCOMPATIBILITY. |
|
407 |
||
26422
d5883907c514
HOL (and FOL): renamed variables in rules imp_elim and swap;
wenzelm
parents:
26401
diff
changeset
|
408 |
* 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
|
409 |
Potential INCOMPATIBILITY. |
d5883907c514
HOL (and FOL): renamed variables in rules imp_elim and swap;
wenzelm
parents:
26401
diff
changeset
|
410 |
|
26874 | 411 |
* Theory Product_Type: duplicated lemmas split_Pair_apply and |
412 |
injective_fst_snd removed, use split_eta and prod_eqI instead. |
|
413 |
Renamed upd_fst to apfst and upd_snd to apsnd. INCOMPATIBILITY. |
|
26355 | 414 |
|
26335
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
415 |
* 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
|
416 |
the same name in theory Orderings: |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
417 |
|
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
418 |
less_trans |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
419 |
less_linear |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
420 |
le_imp_less_or_eq |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
421 |
le_less_trans |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
422 |
less_le_trans |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
423 |
less_not_sym |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
424 |
less_asym |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
425 |
|
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
426 |
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
|
427 |
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
|
428 |
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
|
429 |
|
26231 | 430 |
* Library/Option_ord.thy: Canonical order on option type. |
431 |
||
27008 | 432 |
* Library/RBT.thy: Red-black trees, an efficient implementation of |
433 |
finite maps. |
|
26197 | 434 |
|
26231 | 435 |
* Library/Countable.thy: Type class for countable types. |
436 |
||
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
437 |
* 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
|
438 |
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
|
439 |
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
|
440 |
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
|
441 |
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
|
442 |
accordingly. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
443 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
444 |
* 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
|
445 |
depend on well-founded relations. INCOMPATIBILITY. Definitions |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
446 |
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
|
447 |
[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
|
448 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
449 |
* 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
|
450 |
(whose purpose mainly is for various fold_set functionals) have been |
26874 | 451 |
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
|
452 |
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
|
453 |
lower_semilattice (resp. upper_semilattice) and linorder. |
26139 | 454 |
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
|
455 |
|
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
456 |
* 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
|
457 |
case_names ("base" and "step"). INCOMPATIBILITY. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
458 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
459 |
* 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
|
460 |
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
|
461 |
Inductive.lfp_ordinal_induct_set. |
26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
26006
diff
changeset
|
462 |
|
26874 | 463 |
* Renamed theorems "power.simps" to "power_int.simps". |
27067 | 464 |
INCOMPATIBILITY. |
25961 | 465 |
|
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
466 |
* Class semiring_div provides basic abstract properties of semirings |
25942 | 467 |
with division and modulo operations. Subsumes former class dvd_mod. |
468 |
||
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
469 |
* 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
|
470 |
Int. INCOMPATIBILITY. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
471 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
472 |
* 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
|
473 |
numbers rather than integers. INCOMPATIBILITY. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
474 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
475 |
* 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
|
476 |
"minus" which now only has operation "minus", binary). |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
477 |
INCOMPATIBILITY. |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
478 |
|
25522 | 479 |
* Constants "card", "internal_split", "option_map" now with authentic |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
480 |
syntax. INCOMPATIBILITY. |
25522 | 481 |
|
482 |
* Definitions subset_def, psubset_def, set_diff_def, Compl_def, |
|
483 |
le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def, |
|
484 |
sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def, |
|
485 |
Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def, |
|
486 |
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
|
487 |
equality. INCOMPATIBILITY. |
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
488 |
|
25705 | 489 |
* 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
|
490 |
%x. c. The simplifier setup is now more robust against eta expansion. |
25705 | 491 |
INCOMPATIBILITY: in cases explicitly referring to K_record. |
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
492 |
|
27067 | 493 |
* Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}. |
494 |
||
495 |
* Library/ListVector: new theory of arithmetic vector operations. |
|
496 |
||
497 |
* Library/Order_Relation: new theory of various orderings as sets of |
|
498 |
pairs. Defines preorders, partial orders, linear orders and |
|
499 |
well-orders on sets and on types. |
|
26877 | 500 |
|
25726
9728f319ffc6
* Metis prover an order of magnitude faster, works with multithreading.
wenzelm
parents:
25712
diff
changeset
|
501 |
|
26197 | 502 |
*** ZF *** |
503 |
||
26874 | 504 |
* Renamed some theories to allow to loading both ZF and HOL in the |
505 |
same session: |
|
506 |
||
507 |
Datatype -> Datatype_ZF |
|
508 |
Inductive -> Inductive_ZF |
|
509 |
Int -> Int_ZF |
|
510 |
IntDiv -> IntDiv_ZF |
|
511 |
Nat -> Nat_ZF |
|
512 |
List -> List_ZF |
|
513 |
Main -> Main_ZF |
|
514 |
||
515 |
INCOMPATIBILITY: ZF theories that import individual theories below |
|
516 |
Main might need to be adapted. Regular theory Main is still |
|
517 |
available, as trivial extension of Main_ZF. |
|
26197 | 518 |
|
519 |
||
25737
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
520 |
*** ML *** |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
521 |
|
27067 | 522 |
* ML within Isar: antiquotation @{const name} or @{const |
523 |
name(typargs)} produces statically-checked Const term. |
|
524 |
||
26401
e7a94081dce7
Functor NamedThmsFun: data is available to the user as dynamic fact;
wenzelm
parents:
26387
diff
changeset
|
525 |
* 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
|
526 |
(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
|
527 |
|
27067 | 528 |
* Removed obsolete "use_legacy_bindings" function. |
26188 | 529 |
|
25737
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
530 |
* 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
|
531 |
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
|
532 |
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
|
533 |
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
|
534 |
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
|
535 |
|
26874 | 536 |
* Functions system/system_out provide a robust way to invoke external |
27008 | 537 |
shell commands, with propagation of interrupts (requires Poly/ML 5.2). |
26874 | 538 |
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
|
539 |
|
25737
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
540 |
|
25626
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
541 |
*** System *** |
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
542 |
|
25971 | 543 |
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs --- |
544 |
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
|
545 |
|
25626
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
546 |
* isatool tty runs Isabelle process with plain tty interaction; |
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
547 |
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
|
548 |
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
|
549 |
|
25651 | 550 |
* isatool browser now works with Cygwin as well, using general |
551 |
"javapath" function defined in Isabelle process environment. |
|
552 |
||
27067 | 553 |
* YXML notation provides a simple and efficient alternative to |
554 |
standard XML transfer syntax. See src/Pure/General/yxml.ML and |
|
555 |
isatool yxml as described in the Isabelle system manual. |
|
25651 | 556 |
|
25652 | 557 |
* JVM class isabelle.IsabelleProcess (located in Isabelle/lib/classes) |
25651 | 558 |
provides general wrapper for managing an Isabelle process in a robust |
559 |
fashion, with ``cooked'' output from stdin/stderr. |
|
560 |
||
25855 | 561 |
* Rudimentary Isabelle plugin for jEdit (see Isabelle/lib/jedit), |
562 |
based on Isabelle/JVM process wrapper (see Isabelle/lib/classes). |
|
563 |
||
27067 | 564 |
* Removed obsolete THIS_IS_ISABELLE_BUILD feature. NB: the documented |
565 |
way of changing the user's settings is via |
|
566 |
ISABELLE_HOME_USER/etc/settings, which is a fully featured bash |
|
567 |
script. |
|
568 |
||
569 |
* Multithreading.max_threads := 0 refers to the number of actual CPU |
|
570 |
cores of the underlying machine, which is a good starting point for |
|
571 |
optimal performance tuning. The corresponding usedir option -M allows |
|
572 |
"max" as an alias for "0". WARNING: does not work on certain versions |
|
573 |
of Mac OS (with Poly/ML 5.1). |
|
574 |
||
575 |
* isabelle-process: non-ML sessions are run with "nice", to reduce the |
|
576 |
adverse effect of Isabelle flooding interactive front-ends (notably |
|
577 |
ProofGeneral / XEmacs). |
|
578 |
||
25626
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
579 |
|
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
580 |
|
25429 | 581 |
New in Isabelle2007 (November 2007) |
582 |
----------------------------------- |
|
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
583 |
|
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
584 |
*** General *** |
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
585 |
|
22826 | 586 |
* More uniform information about legacy features, notably a |
587 |
warning/error of "Legacy feature: ...", depending on the state of the |
|
23367 | 588 |
tolerate_legacy_features flag (default true). FUTURE INCOMPATIBILITY: |
589 |
legacy features will disappear eventually. |
|
22826 | 590 |
|
17918
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
591 |
* 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
|
592 |
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
|
593 |
fixheaders to convert existing theory files. INCOMPATIBILITY. |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
594 |
|
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
595 |
* 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
|
596 |
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
|
597 |
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
|
598 |
function use_legacy_bindings. INCOMPATIBILITY. |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
599 |
|
22871 | 600 |
* Theory syntax: some popular names (e.g. 'class', 'declaration', |
601 |
'fun', 'help', 'if') are now keywords. INCOMPATIBILITY, use double |
|
602 |
quotes. |
|
19814
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
603 |
|
23888
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
604 |
* 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
|
605 |
header specifications (including optional directories), but not the |
24172
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
606 |
accidental file locations of previously successful loads. The strict |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
607 |
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
|
608 |
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
|
609 |
theories simultaneously, just as 'imports' within a theory header |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
610 |
specification, but without merging the results. Potential |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
611 |
INCOMPATIBILITY: may need to refine theory headers and commands |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
612 |
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
|
613 |
|
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
614 |
* 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
|
615 |
identification, instead of the traditional scheme of full physical |
23889 | 616 |
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
|
617 |
(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
|
618 |
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
|
619 |
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
|
620 |
|
24187
8bdf5ca5871f
* Theory loader: old-style ML proof scripts are considered a legacy feature;
wenzelm
parents:
24172
diff
changeset
|
621 |
* 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
|
622 |
file (with the same base name as the theory) are considered a legacy |
24800 | 623 |
feature, which will disappear eventually. Even now, the theory loader |
624 |
no longer maintains dependencies on such files. |
|
625 |
||
626 |
* Syntax: the scope for resolving ambiguities via type-inference is |
|
627 |
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
|
628 |
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
|
629 |
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
|
630 |
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
|
631 |
'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
|
632 |
|
25034 | 633 |
* Syntax: constants introduced by new-style packages ('definition', |
634 |
'abbreviation' etc.) are passed through the syntax module in |
|
635 |
``authentic mode''. This means that associated mixfix annotations |
|
636 |
really stick to such constants, independently of potential name space |
|
637 |
ambiguities introduced later on. INCOMPATIBILITY: constants in parse |
|
638 |
trees are represented slightly differently, may need to adapt syntax |
|
639 |
translations accordingly. Use CONST marker in 'translations' and |
|
640 |
@{const_syntax} antiquotation in 'parse_translation' etc. |
|
641 |
||
17981
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
642 |
* 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
|
643 |
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
|
644 |
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
|
645 |
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
|
646 |
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
|
647 |
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
|
648 |
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
|
649 |
|
23379
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
650 |
* Command 'find_theorems': supports "*" wild-card in "name:" |
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
651 |
criterion; "with_dups" option. Certain ProofGeneral versions might |
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
652 |
support a specific search form (see ProofGeneral/CHANGES). |
22965 | 653 |
|
20370 | 654 |
* The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1 |
655 |
by default, which means that "prems" (and also "fixed variables") are |
|
656 |
suppressed from proof state output. Note that the ProofGeneral |
|
657 |
settings mechanism allows to change and save options persistently, but |
|
658 |
older versions of Isabelle will fail to start up if a negative prems |
|
659 |
limit is imposed. |
|
660 |
||
21308
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
661 |
* 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
|
662 |
``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
|
663 |
contain definitions, theorems etc., including any derived mechanism |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
664 |
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
|
665 |
generalizes the existing ``theorem (in ...)'' towards more versatility |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
666 |
and scalability. |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
667 |
|
21960
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
668 |
* 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
|
669 |
discontinued Isabelle/classic mode (ML proof scripts). |
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
670 |
|
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
671 |
|
17865 | 672 |
*** Document preparation *** |
673 |
||
21717 | 674 |
* Added antiquotation @{theory name} which prints the given name, |
675 |
after checking that it refers to a valid ancestor theory in the |
|
676 |
current context. |
|
21339 | 677 |
|
17869 | 678 |
* Added antiquotations @{ML_type text} and @{ML_struct text} which |
679 |
check the given source text as ML type/structure, printing verbatim. |
|
17865 | 680 |
|
21717 | 681 |
* Added antiquotation @{abbrev "c args"} which prints the abbreviation |
682 |
"c args == rhs" given in the current context. (Any number of |
|
21735 | 683 |
arguments may be given on the LHS.) |
21717 | 684 |
|
685 |
||
17779 | 686 |
*** Pure *** |
687 |
||
24800 | 688 |
* The 'class' package offers a combination of axclass and locale to |
25129 | 689 |
achieve Haskell-like type classes in Isabelle. Definitions and |
690 |
theorems within a class context produce both relative results (with |
|
691 |
implicit parameters according to the locale context), and polymorphic |
|
692 |
constants with qualified polymorphism (according to the class |
|
693 |
context). Within the body context of a 'class' target, a separate |
|
694 |
syntax layer ("user space type system") takes care of converting |
|
695 |
between global polymorphic consts and internal locale representation. |
|
25177 | 696 |
See src/HOL/ex/Classpackage.thy for examples (as well as main HOL). |
25184 | 697 |
"isatool doc classes" provides a tutorial. |
20807 | 698 |
|
25199 | 699 |
* Generic code generator framework allows to generate executable |
24800 | 700 |
code for ML and Haskell (including Isabelle classes). A short usage |
701 |
sketch: |
|
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
702 |
|
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
703 |
internal compilation: |
25199 | 704 |
export_code <list of constants (term syntax)> in SML |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
705 |
writing SML code to a file: |
25199 | 706 |
export_code <list of constants (term syntax)> in SML <filename> |
22735 | 707 |
writing OCaml code to a file: |
25199 | 708 |
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
|
709 |
writing Haskell code to a bunch of files: |
25199 | 710 |
export_code <list of constants (term syntax)> in Haskell <filename> |
711 |
||
712 |
evaluating closed propositions to True/False using code generation: |
|
25184 | 713 |
method ``eval'' |
714 |
||
715 |
Reasonable default setup of framework in HOL. |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
716 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
717 |
Theorem attributs for selecting and transforming function equations theorems: |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
718 |
|
22845 | 719 |
[code fun]: select a theorem as function equation for a specific constant |
720 |
[code fun del]: deselect a theorem as function equation for a specific constant |
|
721 |
[code inline]: select an equation theorem for unfolding (inlining) in place |
|
722 |
[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
|
723 |
|
22735 | 724 |
User-defined serializations (target in {SML, OCaml, Haskell}): |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
725 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
726 |
code_const <and-list of constants (term syntax)> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
727 |
{(target) <and-list of const target syntax>}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
728 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
729 |
code_type <and-list of type constructors> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
730 |
{(target) <and-list of type target syntax>}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
731 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
732 |
code_instance <and-list of instances> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
733 |
{(target)}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
734 |
where instance ::= <type constructor> :: <class> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
735 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
736 |
code_class <and_list of classes> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
737 |
{(target) <and-list of class target syntax>}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
738 |
where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}? |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
739 |
|
25199 | 740 |
code_instance and code_class only are effective to target Haskell. |
22735 | 741 |
|
25177 | 742 |
For example usage see src/HOL/ex/Codegenerator.thy and |
743 |
src/HOL/ex/Codegenerator_Pretty.thy. A separate tutorial on code |
|
24800 | 744 |
generation from Isabelle/HOL theories is available via "isatool doc |
745 |
codegen". |
|
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
746 |
|
25129 | 747 |
* Code generator: consts in 'consts_code' Isar commands are now |
748 |
referred to by usual term syntax (including optional type |
|
749 |
annotations). |
|
750 |
||
19254 | 751 |
* Command 'no_translations' removes translation rules from theory |
752 |
syntax. |
|
753 |
||
19625
285771cec083
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
wenzelm
parents:
19587
diff
changeset
|
754 |
* Overloaded definitions are now actually checked for acyclic |
19714 | 755 |
dependencies. The overloading scheme is slightly more general than |
756 |
that of Haskell98, although Isabelle does not demand an exact |
|
757 |
correspondence to type class and instance declarations. |
|
758 |
INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more |
|
759 |
exotic versions of overloading -- at the discretion of the user! |
|
19711 | 760 |
|
761 |
Polymorphic constants are represented via type arguments, i.e. the |
|
762 |
instantiation that matches an instance against the most general |
|
763 |
declaration given in the signature. For example, with the declaration |
|
764 |
c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented |
|
765 |
as c(nat). Overloading is essentially simultaneous structural |
|
766 |
recursion over such type arguments. Incomplete specification patterns |
|
19714 | 767 |
impose global constraints on all occurrences, e.g. c('a * 'a) on the |
19715 | 768 |
LHS means that more general c('a * 'b) will be disallowed on any RHS. |
19714 | 769 |
Command 'print_theory' outputs the normalized system of recursive |
770 |
equations, see section "definitions". |
|
19625
285771cec083
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
wenzelm
parents:
19587
diff
changeset
|
771 |
|
24086 | 772 |
* Configuration options are maintained within the theory or proof |
773 |
context (with name and type bool/int/string), providing a very simple |
|
774 |
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
|
775 |
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
|
776 |
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
|
777 |
associated attribute of the same name. This form of context |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
778 |
declaration works particularly well with commands 'declare' or |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
779 |
'using', for example ``declare [[foo = 42]]''. Thus it has become |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
780 |
very easy to avoid global references, which would not observe Isar |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
781 |
toplevel undo/redo and fail to work with multithreading. |
24086 | 782 |
|
24172
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
783 |
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
|
784 |
configuration options: |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
785 |
|
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
786 |
Unify.search_bound unify_search_bound |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
787 |
Unify.trace_bound unify_trace_bound |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
788 |
Unify.trace_simp unify_trace_simp |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
789 |
Unify.trace_types unify_trace_types |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
790 |
Simplifier.simp_depth_limit simp_depth_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
791 |
Blast.depth_limit blast_depth_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
792 |
DatatypeProp.dtK datatype_distinctness_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
793 |
fast_arith_neq_limit fast_arith_neq_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
794 |
fast_arith_split_limit fast_arith_split_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
795 |
|
24086 | 796 |
* Named collections of theorems may be easily installed as context |
24800 | 797 |
data using the functor NamedThmsFun (see also |
24086 | 798 |
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
|
799 |
attributes; there is also a toplevel print command. This facility is |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
800 |
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
|
801 |
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
|
802 |
order. |
24086 | 803 |
|
24032 | 804 |
* Isar: command 'declaration' augments a local theory by generic |
805 |
declaration functions written in ML. This enables arbitrary content |
|
806 |
being added to the context, depending on a morphism that tells the |
|
807 |
difference of the original declaration context wrt. the application |
|
808 |
context encountered later on. |
|
809 |
||
810 |
* Isar: proper interfaces for simplification procedures. Command |
|
811 |
'simproc_setup' declares named simprocs (with match patterns, and body |
|
812 |
text in ML). Attribute "simproc" adds/deletes simprocs in the current |
|
813 |
context. ML antiquotation @{simproc name} retrieves named simprocs. |
|
814 |
||
815 |
* Isar: an extra pair of brackets around attribute declarations |
|
816 |
abbreviates a theorem reference involving an internal dummy fact, |
|
817 |
which will be ignored later --- only the effect of the attribute on |
|
818 |
the background context will persist. This form of in-place |
|
819 |
declarations is particularly useful with commands like 'declare' and |
|
820 |
'using', for example ``have A using [[simproc a]] by simp''. |
|
821 |
||
23369
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
822 |
* 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
|
823 |
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
|
824 |
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
|
825 |
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
|
826 |
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
|
827 |
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
|
828 |
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
|
829 |
more permissive. |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
830 |
|
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
831 |
* 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
|
832 |
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
|
833 |
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
|
834 |
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
|
835 |
maintainability of proof texts. |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
836 |
|
17865 | 837 |
* Isar: improper proof element 'guess' is like 'obtain', but derives |
838 |
the obtained context from the course of reasoning! For example: |
|
839 |
||
840 |
assume "EX x y. A x & B y" -- "any previous fact" |
|
841 |
then guess x and y by clarify |
|
842 |
||
843 |
This technique is potentially adventurous, depending on the facts and |
|
844 |
proof tools being involved here. |
|
845 |
||
18020 | 846 |
* Isar: known facts from the proof context may be specified as literal |
847 |
propositions, using ASCII back-quote syntax. This works wherever |
|
848 |
named facts used to be allowed so far, in proof commands, proof |
|
849 |
methods, attributes etc. Literal facts are retrieved from the context |
|
850 |
according to unification of type and term parameters. For example, |
|
851 |
provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known |
|
852 |
theorems in the current context, then these are valid literal facts: |
|
853 |
`A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc. |
|
854 |
||
855 |
There is also a proof method "fact" which does the same composition |
|
18044 | 856 |
for explicit goal states, e.g. the following proof texts coincide with |
857 |
certain special cases of literal facts: |
|
18020 | 858 |
|
859 |
have "A" by fact == note `A` |
|
860 |
have "A ==> B" by fact == note `A ==> B` |
|
861 |
have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` |
|
862 |
have "P a ==> Q a" by fact == note `P a ==> Q a` |
|
863 |
||
20118
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
864 |
* 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
|
865 |
outer syntax. Thus symbolic identifiers may be used without |
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
866 |
additional white space in declarations like this: ``assume *: A''. |
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
867 |
|
20013 | 868 |
* Isar: 'print_facts' prints all local facts of the current context, |
869 |
both named and unnamed ones. |
|
870 |
||
18308 | 871 |
* Isar: 'def' now admits simultaneous definitions, e.g.: |
872 |
||
873 |
def x == "t" and y == "u" |
|
874 |
||
18540 | 875 |
* Isar: added command 'unfolding', which is structurally similar to |
876 |
'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
|
877 |
rewrite rules. Thus many occurrences of the 'unfold' method or |
18540 | 878 |
'unfolded' attribute may be replaced by first-class proof text. |
879 |
||
18815
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
880 |
* Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded', |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
881 |
and command 'unfolding' now all support object-level equalities |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
882 |
(potentially conditional). The underlying notion of rewrite rule is |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
883 |
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
|
884 |
Simplifier (which is usually more generous). |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
885 |
|
24238 | 886 |
* Isar: the new attribute [rotated n] (default n = 1) rotates the |
887 |
premises of a theorem by n. Useful in conjunction with drule. |
|
888 |
||
19220 | 889 |
* Isar: the goal restriction operator [N] (default N = 1) evaluates a |
890 |
method expression within a sandbox consisting of the first N |
|
19240 | 891 |
sub-goals, which need to exist. For example, ``simp_all [3]'' |
892 |
simplifies the first three sub-goals, while (rule foo, simp_all)[] |
|
893 |
simplifies all new goals that emerge from applying rule foo to the |
|
894 |
originally first one. |
|
19220 | 895 |
|
19814
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
896 |
* 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
|
897 |
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
|
898 |
expected. |
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
899 |
|
18901 | 900 |
* Isar: the conclusion of a long theorem statement is now either |
901 |
'shows' (a simultaneous conjunction, as before), or 'obtains' |
|
902 |
(essentially a disjunction of cases with local parameters and |
|
903 |
assumptions). The latter allows to express general elimination rules |
|
18910 | 904 |
adequately; in this notation common elimination rules look like this: |
18901 | 905 |
|
906 |
lemma exE: -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis" |
|
907 |
assumes "EX x. P x" |
|
908 |
obtains x where "P x" |
|
909 |
||
910 |
lemma conjE: -- "A & B ==> (A ==> B ==> thesis) ==> thesis" |
|
911 |
assumes "A & B" |
|
912 |
obtains A and B |
|
913 |
||
914 |
lemma disjE: -- "A | B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis" |
|
915 |
assumes "A | B" |
|
916 |
obtains |
|
917 |
A |
|
918 |
| B |
|
919 |
||
18910 | 920 |
The subsequent classical rules even refer to the formal "thesis" |
18901 | 921 |
explicitly: |
922 |
||
923 |
lemma classical: -- "(~ thesis ==> thesis) ==> thesis" |
|
924 |
obtains "~ thesis" |
|
925 |
||
18910 | 926 |
lemma Peirce's_Law: -- "((thesis ==> something) ==> thesis) ==> thesis" |
927 |
obtains "thesis ==> something" |
|
18901 | 928 |
|
929 |
The actual proof of an 'obtains' statement is analogous to that of the |
|
18910 | 930 |
Isar proof element 'obtain', only that there may be several cases. |
931 |
Optional case names may be specified in parentheses; these will be |
|
932 |
available both in the present proof and as annotations in the |
|
933 |
resulting rule, for later use with the 'cases' method (cf. attribute |
|
934 |
case_names). |
|
18901 | 935 |
|
21447
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
936 |
* 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
|
937 |
"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
|
938 |
(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
|
939 |
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
|
940 |
|
19263 | 941 |
* Isar: 'print_statement' prints theorems from the current theory or |
942 |
proof context in long statement form, according to the syntax of a |
|
943 |
top-level lemma. |
|
944 |
||
18901 | 945 |
* Isar: 'obtain' takes an optional case name for the local context |
946 |
introduction rule (default "that"). |
|
947 |
||
19587 | 948 |
* Isar: removed obsolete 'concl is' patterns. INCOMPATIBILITY, use |
949 |
explicit (is "_ ==> ?foo") in the rare cases where this still happens |
|
950 |
to occur. |
|
951 |
||
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
952 |
* Pure: syntax "CONST name" produces a fully internalized constant |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
953 |
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
|
954 |
syntax translations that should refer to internal constant |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
955 |
representations independently of name spaces. |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
956 |
|
21537
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
957 |
* 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
|
958 |
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
|
959 |
in the same context. INCOMPATIBILITY. |
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
960 |
|
21209
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset
|
961 |
* 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
|
962 |
primitive that also works in a locale context (both for constants and |
24950 | 963 |
fixed variables). Type declaration and internal syntactic representation |
964 |
of given constants retrieved from the context. Likewise, the |
|
965 |
'no_notation' command allows to remove given syntax annotations from the |
|
966 |
current context. |
|
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
967 |
|
19665 | 968 |
* Isar/locales: new derived specification elements 'axiomatization', |
969 |
'definition', 'abbreviation', which support type-inference, admit |
|
19083 | 970 |
object-level specifications (equality, equivalence). See also the |
971 |
isar-ref manual. Examples: |
|
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset
|
972 |
|
19665 | 973 |
axiomatization |
21595 | 974 |
eq (infix "===" 50) where |
975 |
eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y" |
|
976 |
||
977 |
definition "f x y = x + y + 1" |
|
978 |
definition g where "g x = f x x" |
|
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset
|
979 |
|
19363 | 980 |
abbreviation |
21595 | 981 |
neq (infix "=!=" 50) where |
19363 | 982 |
"x =!= y == ~ (x === y)" |
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset
|
983 |
|
19083 | 984 |
These specifications may be also used in a locale context. Then the |
985 |
constants being introduced depend on certain fixed parameters, and the |
|
986 |
constant name is qualified by the locale base name. An internal |
|
987 |
abbreviation takes care for convenient input and output, making the |
|
19088 | 988 |
parameters implicit and using the original short name. See also |
25177 | 989 |
src/HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic |
19083 | 990 |
entities from a monomorphic theory. |
991 |
||
992 |
Presently, abbreviations are only available 'in' a target locale, but |
|
19363 | 993 |
not inherited by general import expressions. Also note that |
994 |
'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
|
995 |
'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
|
996 |
prevents folding of abbreviations in term output. |
19084 | 997 |
|
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
998 |
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
|
999 |
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
|
1000 |
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
|
1001 |
'translations' with explicit "CONST" markup to accommodate this. |
19665 | 1002 |
|
24800 | 1003 |
* Pure/Isar: unified syntax for new-style specification mechanisms |
1004 |
(e.g. 'definition', 'abbreviation', or 'inductive' in HOL) admits |
|
1005 |
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
|
1006 |
|
3a55ee2cae70
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm
parents:
24706
diff
changeset
|
1007 |
definition "K x _ = x" |
3a55ee2cae70
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm
parents:
24706
diff
changeset
|
1008 |
|
24738 | 1009 |
inductive conj for A B |
1010 |
where "A ==> B ==> conj A B" |
|
1011 |
||
21735 | 1012 |
* Pure: command 'print_abbrevs' prints all constant abbreviations of |
1013 |
the current context. Print mode "no_abbrevs" prevents inversion of |
|
1014 |
abbreviations on output. |
|
1015 |
||
24800 | 1016 |
* Isar/locales: improved parameter handling: use of locales "var" and |
1017 |
"struct" no longer necessary; - parameter renamings are no longer |
|
1018 |
required to be injective. For example, this allows to define |
|
1019 |
endomorphisms as locale endom = homom mult mult h. |
|
19783 | 1020 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1021 |
* 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
|
1022 |
Instead of accumulating the specification, the imported expression is |
22126 | 1023 |
now an interpretation. INCOMPATIBILITY: different normal form of |
1024 |
locale expressions. In particular, in interpretations of locales with |
|
1025 |
predicates, goals repesenting already interpreted fragments are not |
|
1026 |
removed automatically. Use methods `intro_locales' and |
|
1027 |
`unfold_locales'; see below. |
|
1028 |
||
1029 |
* Isar/locales: new methods `intro_locales' and `unfold_locales' |
|
1030 |
provide backward reasoning on locales predicates. The methods are |
|
1031 |
aware of interpretations and discharge corresponding goals. |
|
1032 |
`intro_locales' is less aggressive then `unfold_locales' and does not |
|
1033 |
unfold predicates to assumptions. |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1034 |
|
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1035 |
* Isar/locales: the order in which locale fragments are accumulated |
22126 | 1036 |
has changed. This enables to override declarations from fragments due |
1037 |
to interpretations -- for example, unwanted simp rules. |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1038 |
|
23920 | 1039 |
* Isar/locales: interpretation in theories and proof contexts has been |
1040 |
extended. One may now specify (and prove) equations, which are |
|
1041 |
unfolded in interpreted theorems. This is useful for replacing |
|
1042 |
defined concepts (constants depending on locale parameters) by |
|
1043 |
concepts already existing in the target context. Example: |
|
1044 |
||
1045 |
interpretation partial_order ["op <= :: [int, int] => bool"] |
|
1046 |
where "partial_order.less (op <=) (x::int) y = (x < y)" |
|
1047 |
||
24800 | 1048 |
Typically, the constant `partial_order.less' is created by a |
1049 |
definition specification element in the context of locale |
|
1050 |
partial_order. |
|
1051 |
||
24859 | 1052 |
* Method "induct": improved internal context management to support |
24800 | 1053 |
local fixes and defines on-the-fly. Thus explicit meta-level |
1054 |
connectives !! and ==> are rarely required anymore in inductive goals |
|
1055 |
(using object-logic connectives for this purpose has been long |
|
1056 |
obsolete anyway). Common proof patterns are explained in |
|
25177 | 1057 |
src/HOL/Induct/Common_Patterns.thy, see also |
1058 |
src/HOL/Isar_examples/Puzzle.thy and src/HOL/Lambda for realistic |
|
1059 |
examples. |
|
24606
7acbb982fc77
moved induct patterns to HOL/Induct/Common_Patterns.thy;
wenzelm
parents:
24507
diff
changeset
|
1060 |
|
24859 | 1061 |
* 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
|
1062 |
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
|
1063 |
several conclusions, while the corresponding symbolic cases are nested |
7acbb982fc77
moved induct patterns to HOL/Induct/Common_Patterns.thy;
wenzelm
parents:
24507
diff
changeset
|
1064 |
accordingly. INCOMPATIBILITY, proofs need to be structured explicitly, |
25177 | 1065 |
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
|
1066 |
|
24859 | 1067 |
* Method "induct": mutual induction rules are now specified as a list |
24800 | 1068 |
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
|
1069 |
foo_bar.inducts for mutually defined items foo and bar (e.g. inductive |
24859 | 1070 |
predicates/sets or datatypes). INCOMPATIBILITY, users need to specify |
1071 |
mutual induction rules differently, i.e. like this: |
|
18506
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
1072 |
|
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
1073 |
(induct rule: foo_bar.inducts) |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
1074 |
(induct set: foo bar) |
24859 | 1075 |
(induct pred: foo bar) |
18506
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
1076 |
(induct type: foo bar) |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
1077 |
|
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
1078 |
The ML function ProjectRule.projections turns old-style rules into the |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
1079 |
new format. |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
1080 |
|
24859 | 1081 |
* Method "coinduct": dual of induction, see |
18399 | 1082 |
src/HOL/Library/Coinductive_List.thy for various examples. |
1083 |
||
24859 | 1084 |
* Method "cases", "induct", "coinduct": the ``(open)'' option is |
1085 |
considered a legacy feature. |
|
1086 |
||
20919
dab803075c62
attribute "symmetric": standardized schematic variables;
wenzelm
parents:
20857
diff
changeset
|
1087 |
* Attribute "symmetric" produces result with standardized schematic |
dab803075c62
attribute "symmetric": standardized schematic variables;
wenzelm
parents:
20857
diff
changeset
|
1088 |
variables (index 0). Potential INCOMPATIBILITY. |
dab803075c62
attribute "symmetric": standardized schematic variables;
wenzelm
parents:
20857
diff
changeset
|
1089 |
|
22126 | 1090 |
* Simplifier: by default the simplifier trace only shows top level |
1091 |
rewrites now. That is, trace_simp_depth_limit is set to 1 by |
|
1092 |
default. Thus there is less danger of being flooded by the trace. The |
|
1093 |
trace indicates where parts have been suppressed. |
|
18674 | 1094 |
|
18536
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1095 |
* Provers/classical: removed obsolete classical version of elim_format |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1096 |
attribute; classical elim/dest rules are now treated uniformly when |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1097 |
manipulating the claset. |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1098 |
|
18694 | 1099 |
* Provers/classical: stricter checks to ensure that supplied intro, |
1100 |
dest and elim rules are well-formed; dest and elim rules must have at |
|
1101 |
least one premise. |
|
1102 |
||
1103 |
* Provers/classical: attributes dest/elim/intro take an optional |
|
18695 | 1104 |
weight argument for the rule (just as the Pure versions). Weights are |
18696 | 1105 |
ignored by automated tools, but determine the search order of single |
18694 | 1106 |
rule steps. |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18549
diff
changeset
|
1107 |
|
18536
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1108 |
* Syntax: input syntax now supports dummy variable binding "%_. b", |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1109 |
where the body does not mention the bound variable. Note that dummy |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1110 |
patterns implicitly depend on their context of bounds, which makes |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1111 |
"{_. _}" match any set comprehension as expected. Potential |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1112 |
INCOMPATIBILITY -- parse translations need to cope with syntactic |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1113 |
constant "_idtdummy" in the binding position. |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1114 |
|
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1115 |
* Syntax: removed obsolete syntactic constant "_K" and its associated |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1116 |
parse translation. INCOMPATIBILITY -- use dummy abstraction instead, |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
1117 |
for example "A -> B" => "Pi A (%_. B)". |
17779 | 1118 |
|
20582
ebd0e03c6a9b
* Pure: 'class_deps' command visualizes the subclass relation;
wenzelm
parents:
20503
diff
changeset
|
1119 |
* Pure: 'class_deps' command visualizes the subclass relation, using |
ebd0e03c6a9b
* Pure: 'class_deps' command visualizes the subclass relation;
wenzelm
parents:
20503
diff
changeset
|
1120 |
the graph browser tool. |
ebd0e03c6a9b
* Pure: 'class_deps' command visualizes the subclass relation;
wenzelm
parents:
20503
diff
changeset
|
1121 |
|
24800 | 1122 |
* Pure: 'print_theory' now suppresses certain internal declarations by |
1123 |
default; use '!' option for full details. |
|
20620
8b26f58c5646
* Pure: 'print_theory' now suppresses entities with internal name;
wenzelm
parents:
20607
diff
changeset
|
1124 |
|
17865 | 1125 |
|
17806 | 1126 |
*** HOL *** |
1127 |
||
25129 | 1128 |
* Method "metis" proves goals by applying the Metis general-purpose |
1129 |
resolution prover (see also http://gilith.com/software/metis/). |
|
1130 |
Examples are in the directory MetisExamples. WARNING: the |
|
1131 |
Isabelle/HOL-Metis integration does not yet work properly with |
|
1132 |
multi-threading. |
|
1133 |
||
1134 |
* Command 'sledgehammer' invokes external automatic theorem provers as |
|
1135 |
background processes. It generates calls to the "metis" method if |
|
1136 |
successful. These can be pasted into the proof. Users do not have to |
|
1137 |
wait for the automatic provers to return. WARNING: does not really |
|
1138 |
work with multi-threading. |
|
1139 |
||
24804 | 1140 |
* New "auto_quickcheck" feature tests outermost goal statements for |
1141 |
potential counter-examples. Controlled by ML references |
|
1142 |
auto_quickcheck (default true) and auto_quickcheck_time_limit (default |
|
25129 | 1143 |
5000 milliseconds). Fails silently if statements is outside of |
1144 |
executable fragment, or any other codgenerator problem occurs. |
|
24804 | 1145 |
|
25184 | 1146 |
* New constant "undefined" with axiom "undefined x = undefined". |
1147 |
||
1148 |
* Added class "HOL.eq", allowing for code generation with polymorphic |
|
1149 |
equality. |
|
1150 |
||
1151 |
* Some renaming of class constants due to canonical name prefixing in |
|
1152 |
the new 'class' package: |
|
1153 |
||
1154 |
HOL.abs ~> HOL.abs_class.abs |
|
1155 |
HOL.divide ~> HOL.divide_class.divide |
|
1156 |
0 ~> HOL.zero_class.zero |
|
1157 |
1 ~> HOL.one_class.one |
|
1158 |
op + ~> HOL.plus_class.plus |
|
1159 |
op - ~> HOL.minus_class.minus |
|
1160 |
uminus ~> HOL.minus_class.uminus |
|
1161 |
op * ~> HOL.times_class.times |
|
1162 |
op < ~> HOL.ord_class.less |
|
1163 |
op <= > HOL.ord_class.less_eq |
|
1164 |
Nat.power ~> Power.power_class.power |
|
1165 |
Nat.size ~> Nat.size_class.size |
|
1166 |
Numeral.number_of ~> Numeral.number_class.number_of |
|
1167 |
FixedPoint.Inf ~> Lattices.complete_lattice_class.Inf |
|
1168 |
FixedPoint.Sup ~> Lattices.complete_lattice_class.Sup |
|
1169 |
Orderings.min ~> Orderings.ord_class.min |
|
1170 |
Orderings.max ~> Orderings.ord_class.max |
|
1171 |
Divides.op div ~> Divides.div_class.div |
|
1172 |
Divides.op mod ~> Divides.div_class.mod |
|
1173 |
Divides.op dvd ~> Divides.div_class.dvd |
|
1174 |
||
1175 |
INCOMPATIBILITY. Adaptions may be required in the following cases: |
|
1176 |
||
1177 |
a) User-defined constants using any of the names "plus", "minus", |
|
1178 |
"times", "less" or "less_eq". The standard syntax translations for |
|
1179 |
"+", "-" and "*" may go wrong. INCOMPATIBILITY: use more specific |
|
1180 |
names. |
|
1181 |
||
1182 |
b) Variables named "plus", "minus", "times", "less", "less_eq" |
|
1183 |
INCOMPATIBILITY: use more specific names. |
|
1184 |
||
1185 |
c) Permutative equations (e.g. "a + b = b + a") |
|
1186 |
Since the change of names also changes the order of terms, permutative |
|
1187 |
rewrite rules may get applied in a different order. Experience shows |
|
1188 |
that this is rarely the case (only two adaptions in the whole Isabelle |
|
1189 |
distribution). INCOMPATIBILITY: rewrite proofs |
|
1190 |
||
1191 |
d) ML code directly refering to constant names |
|
1192 |
This in general only affects hand-written proof tactics, simprocs and |
|
1193 |
so on. INCOMPATIBILITY: grep your sourcecode and replace names. |
|
1194 |
Consider using @{const_name} antiquotation. |
|
1195 |
||
1196 |
* New class "default" with associated constant "default". |
|
1197 |
||
1198 |
* Function "sgn" is now overloaded and available on int, real, complex |
|
1199 |
(and other numeric types), using class "sgn". Two possible defs of |
|
1200 |
sgn are given as equational assumptions in the classes sgn_if and |
|
1201 |
sgn_div_norm; ordered_idom now also inherits from sgn_if. |
|
1202 |
INCOMPATIBILITY. |
|
1203 |
||
1204 |
* Locale "partial_order" now unified with class "order" (cf. theory |
|
1205 |
Orderings), added parameter "less". INCOMPATIBILITY. |
|
1206 |
||
1207 |
* Renamings in classes "order" and "linorder": facts "refl", "trans" and |
|
1208 |
"cases" to "order_refl", "order_trans" and "linorder_cases", to avoid |
|
1209 |
clashes with HOL "refl" and "trans". INCOMPATIBILITY. |
|
1210 |
||
1211 |
* Classes "order" and "linorder": potential INCOMPATIBILITY due to |
|
1212 |
changed order of proof goals in instance proofs. |
|
1213 |
||
1214 |
* The transitivity reasoner for partial and linear orders is set up |
|
1215 |
for classes "order" and "linorder". Instances of the reasoner are available |
|
1216 |
in all contexts importing or interpreting the corresponding locales. |
|
1217 |
Method "order" invokes the reasoner separately; the reasoner |
|
1218 |
is also integrated with the Simplifier as a solver. Diagnostic |
|
1219 |
command 'print_orders' shows the available instances of the reasoner |
|
1220 |
in the current context. |
|
1221 |
||
1222 |
* Localized monotonicity predicate in theory "Orderings"; integrated |
|
1223 |
lemmas max_of_mono and min_of_mono with this predicate. |
|
1224 |
INCOMPATIBILITY. |
|
1225 |
||
1226 |
* Formulation of theorem "dense" changed slightly due to integration |
|
1227 |
with new class dense_linear_order. |
|
1228 |
||
1229 |
* Uniform lattice theory development in HOL. |
|
1230 |
||
1231 |
constants "meet" and "join" now named "inf" and "sup" |
|
1232 |
constant "Meet" now named "Inf" |
|
1233 |
||
1234 |
classes "meet_semilorder" and "join_semilorder" now named |
|
1235 |
"lower_semilattice" and "upper_semilattice" |
|
1236 |
class "lorder" now named "lattice" |
|
1237 |
class "comp_lat" now named "complete_lattice" |
|
1238 |
||
1239 |
Instantiation of lattice classes allows explicit definitions |
|
1240 |
for "inf" and "sup" operations (or "Inf" and "Sup" for complete lattices). |
|
1241 |
||
1242 |
INCOMPATIBILITY. Theorem renames: |
|
1243 |
||
1244 |
meet_left_le ~> inf_le1 |
|
1245 |
meet_right_le ~> inf_le2 |
|
1246 |
join_left_le ~> sup_ge1 |
|
1247 |
join_right_le ~> sup_ge2 |
|
1248 |
meet_join_le ~> inf_sup_ord |
|
1249 |
le_meetI ~> le_infI |
|
1250 |
join_leI ~> le_supI |
|
1251 |
le_meet ~> le_inf_iff |
|
1252 |
le_join ~> ge_sup_conv |
|
1253 |
meet_idempotent ~> inf_idem |
|
1254 |
join_idempotent ~> sup_idem |
|
1255 |
meet_comm ~> inf_commute |
|
1256 |
join_comm ~> sup_commute |
|
1257 |
meet_leI1 ~> le_infI1 |
|
1258 |
meet_leI2 ~> le_infI2 |
|
1259 |
le_joinI1 ~> le_supI1 |
|
1260 |
le_joinI2 ~> le_supI2 |
|
1261 |
meet_assoc ~> inf_assoc |
|
1262 |
join_assoc ~> sup_assoc |
|
1263 |
meet_left_comm ~> inf_left_commute |
|
1264 |
meet_left_idempotent ~> inf_left_idem |
|
1265 |
join_left_comm ~> sup_left_commute |
|
1266 |
join_left_idempotent ~> sup_left_idem |
|
1267 |
meet_aci ~> inf_aci |
|
1268 |
join_aci ~> sup_aci |
|
1269 |
le_def_meet ~> le_iff_inf |
|
1270 |
le_def_join ~> le_iff_sup |
|
1271 |
join_absorp2 ~> sup_absorb2 |
|
1272 |
join_absorp1 ~> sup_absorb1 |
|
1273 |
meet_absorp1 ~> inf_absorb1 |
|
1274 |
meet_absorp2 ~> inf_absorb2 |
|
1275 |
meet_join_absorp ~> inf_sup_absorb |
|
1276 |
join_meet_absorp ~> sup_inf_absorb |
|
1277 |
distrib_join_le ~> distrib_sup_le |
|
1278 |
distrib_meet_le ~> distrib_inf_le |
|
1279 |
||
1280 |
add_meet_distrib_left ~> add_inf_distrib_left |
|
1281 |
add_join_distrib_left ~> add_sup_distrib_left |
|
1282 |
is_join_neg_meet ~> is_join_neg_inf |
|
1283 |
is_meet_neg_join ~> is_meet_neg_sup |
|
1284 |
add_meet_distrib_right ~> add_inf_distrib_right |
|
1285 |
add_join_distrib_right ~> add_sup_distrib_right |
|
1286 |
add_meet_join_distribs ~> add_sup_inf_distribs |
|
1287 |
join_eq_neg_meet ~> sup_eq_neg_inf |
|
1288 |
meet_eq_neg_join ~> inf_eq_neg_sup |
|
1289 |
add_eq_meet_join ~> add_eq_inf_sup |
|
1290 |
meet_0_imp_0 ~> inf_0_imp_0 |
|
1291 |
join_0_imp_0 ~> sup_0_imp_0 |
|
1292 |
meet_0_eq_0 ~> inf_0_eq_0 |
|
1293 |
join_0_eq_0 ~> sup_0_eq_0 |
|
1294 |
neg_meet_eq_join ~> neg_inf_eq_sup |
|
1295 |
neg_join_eq_meet ~> neg_sup_eq_inf |
|
1296 |
join_eq_if ~> sup_eq_if |
|
1297 |
||
1298 |
mono_meet ~> mono_inf |
|
1299 |
mono_join ~> mono_sup |
|
1300 |
meet_bool_eq ~> inf_bool_eq |
|
1301 |
join_bool_eq ~> sup_bool_eq |
|
1302 |
meet_fun_eq ~> inf_fun_eq |
|
1303 |
join_fun_eq ~> sup_fun_eq |
|
1304 |
meet_set_eq ~> inf_set_eq |
|
1305 |
join_set_eq ~> sup_set_eq |
|
1306 |
meet1_iff ~> inf1_iff |
|
1307 |
meet2_iff ~> inf2_iff |
|
1308 |
meet1I ~> inf1I |
|
1309 |
meet2I ~> inf2I |
|
1310 |
meet1D1 ~> inf1D1 |
|
1311 |
meet2D1 ~> inf2D1 |
|
1312 |
meet1D2 ~> inf1D2 |
|
1313 |
meet2D2 ~> inf2D2 |
|
1314 |
meet1E ~> inf1E |
|
1315 |
meet2E ~> inf2E |
|
1316 |
join1_iff ~> sup1_iff |
|
1317 |
join2_iff ~> sup2_iff |
|
1318 |
join1I1 ~> sup1I1 |
|
1319 |
join2I1 ~> sup2I1 |
|
1320 |
join1I1 ~> sup1I1 |
|
1321 |
join2I2 ~> sup1I2 |
|
1322 |
join1CI ~> sup1CI |
|
1323 |
join2CI ~> sup2CI |
|
1324 |
join1E ~> sup1E |
|
1325 |
join2E ~> sup2E |
|
1326 |
||
1327 |
is_meet_Meet ~> is_meet_Inf |
|
1328 |
Meet_bool_def ~> Inf_bool_def |
|
1329 |
Meet_fun_def ~> Inf_fun_def |
|
1330 |
Meet_greatest ~> Inf_greatest |
|
1331 |
Meet_lower ~> Inf_lower |
|
1332 |
Meet_set_def ~> Inf_set_def |
|
1333 |
||
1334 |
Sup_def ~> Sup_Inf |
|
1335 |
Sup_bool_eq ~> Sup_bool_def |
|
1336 |
Sup_fun_eq ~> Sup_fun_def |
|
1337 |
Sup_set_eq ~> Sup_set_def |
|
1338 |
||
1339 |
listsp_meetI ~> listsp_infI |
|
1340 |
listsp_meet_eq ~> listsp_inf_eq |
|
1341 |
||
1342 |
meet_min ~> inf_min |
|
1343 |
join_max ~> sup_max |
|
1344 |
||
1345 |
* Added syntactic class "size"; overloaded constant "size" now has |
|
1346 |
type "'a::size ==> bool" |
|
1347 |
||
24800 | 1348 |
* Internal reorganisation of `size' of datatypes: size theorems |
1349 |
"foo.size" are no longer subsumed by "foo.simps" (but are still |
|
1350 |
simplification rules by default!); theorems "prod.size" now named |
|
25184 | 1351 |
"*.size". |
1352 |
||
1353 |
* Class "div" now inherits from class "times" rather than "type". |
|
1354 |
INCOMPATIBILITY. |
|
24800 | 1355 |
|
1356 |
* HOL/Finite_Set: "name-space" locales Lattice, Distrib_lattice, |
|
1357 |
Linorder etc. have disappeared; operations defined in terms of |
|
1358 |
fold_set now are named Inf_fin, Sup_fin. INCOMPATIBILITY. |
|
1359 |
||
25129 | 1360 |
* HOL/Nat: neq0_conv no longer declared as iff. INCOMPATIBILITY. |
1361 |
||
24800 | 1362 |
* HOL-Word: New extensive library and type for generic, fixed size |
1363 |
machine words, with arithemtic, bit-wise, shifting and rotating |
|
1364 |
operations, reflection into int, nat, and bool lists, automation for |
|
1365 |
linear arithmetic (by automatic reflection into nat or int), including |
|
1366 |
lemmas on overflow and monotonicity. Instantiated to all appropriate |
|
1367 |
arithmetic type classes, supporting automatic simplification of |
|
1368 |
numerals on all operations. |
|
24333 | 1369 |
|
1370 |
* Library/Boolean_Algebra: locales for abstract boolean algebras. |
|
1371 |
||
1372 |
* Library/Numeral_Type: numbers as types, e.g. TYPE(32). |
|
1373 |
||
23850 | 1374 |
* Code generator library theories: |
24993 | 1375 |
- Code_Integer represents HOL integers by big integer literals in target |
23850 | 1376 |
languages. |
24993 | 1377 |
- Code_Char represents HOL characters by character literals in target |
23850 | 1378 |
languages. |
24993 | 1379 |
- Code_Char_chr like Code_Char, but also offers treatment of character |
1380 |
codes; includes Code_Integer. |
|
24800 | 1381 |
- Executable_Set allows to generate code for finite sets using lists. |
1382 |
- Executable_Rat implements rational numbers as triples (sign, enumerator, |
|
23850 | 1383 |
denominator). |
24800 | 1384 |
- Executable_Real implements a subset of real numbers, namly those |
23850 | 1385 |
representable by rational numbers. |
24800 | 1386 |
- Efficient_Nat implements natural numbers by integers, which in general will |
23850 | 1387 |
result in higher efficency; pattern matching with 0/Suc is eliminated; |
24993 | 1388 |
includes Code_Integer. |
1389 |
- Code_Index provides an additional datatype index which is mapped to |
|
1390 |
target-language built-in integers. |
|
26355 | 1391 |
- Code_Message provides an additional datatype message_string which is isomorphic to |
24993 | 1392 |
strings; messages are mapped to target-language strings. |
23850 | 1393 |
|
23783
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
1394 |
* New package for inductive predicates |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
1395 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
1396 |
An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
1397 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
1398 |
inductive |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
1399 |
p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
1400 |
for z_1 :: U_1 and ... and z_n :: U_m |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
1401 |
where |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
1402 |
rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n" |
e4d514f81d95
Added entry for new inductive definition package.
be |