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