author | wenzelm |
Thu, 22 Dec 2005 00:29:12 +0100 | |
changeset 18480 | 8ac97f71369d |
parent 18450 | e57731ba01dd |
child 18488 | a353a61c4544 |
permissions | -rw-r--r-- |
5363 | 1 |
Isabelle NEWS -- history user-relevant changes |
2 |
============================================== |
|
2553 | 3 |
|
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
4 |
New in this Isabelle release |
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
5 |
---------------------------- |
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
6 |
|
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
7 |
*** General *** |
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
8 |
|
17918
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
9 |
* 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
|
10 |
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
|
11 |
fixheaders to convert existing theory files. INCOMPATIBILITY. |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
12 |
|
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
13 |
* 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
|
14 |
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
|
15 |
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
|
16 |
function use_legacy_bindings. INCOMPATIBILITY. |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
17 |
|
17981
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
18 |
* 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
|
19 |
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
|
20 |
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
|
21 |
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
|
22 |
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
|
23 |
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
|
24 |
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
|
25 |
|
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
26 |
* Command 'find_theorems': support "*" wildcard in "name:" criterion. |
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
27 |
|
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
28 |
|
17865 | 29 |
*** Document preparation *** |
30 |
||
17869 | 31 |
* Added antiquotations @{ML_type text} and @{ML_struct text} which |
32 |
check the given source text as ML type/structure, printing verbatim. |
|
17865 | 33 |
|
34 |
||
17779 | 35 |
*** Pure *** |
36 |
||
17865 | 37 |
* Isar: improper proof element 'guess' is like 'obtain', but derives |
38 |
the obtained context from the course of reasoning! For example: |
|
39 |
||
40 |
assume "EX x y. A x & B y" -- "any previous fact" |
|
41 |
then guess x and y by clarify |
|
42 |
||
43 |
This technique is potentially adventurous, depending on the facts and |
|
44 |
proof tools being involved here. |
|
45 |
||
18020 | 46 |
* Isar: known facts from the proof context may be specified as literal |
47 |
propositions, using ASCII back-quote syntax. This works wherever |
|
48 |
named facts used to be allowed so far, in proof commands, proof |
|
49 |
methods, attributes etc. Literal facts are retrieved from the context |
|
50 |
according to unification of type and term parameters. For example, |
|
51 |
provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known |
|
52 |
theorems in the current context, then these are valid literal facts: |
|
53 |
`A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc. |
|
54 |
||
55 |
There is also a proof method "fact" which does the same composition |
|
18044 | 56 |
for explicit goal states, e.g. the following proof texts coincide with |
57 |
certain special cases of literal facts: |
|
18020 | 58 |
|
59 |
have "A" by fact == note `A` |
|
60 |
have "A ==> B" by fact == note `A ==> B` |
|
61 |
have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` |
|
62 |
have "P a ==> Q a" by fact == note `P a ==> Q a` |
|
63 |
||
18308 | 64 |
* Isar: 'def' now admits simultaneous definitions, e.g.: |
65 |
||
66 |
def x == "t" and y == "u" |
|
67 |
||
18233 | 68 |
* Provers/induct: improved internal context management to support |
69 |
local fixes and defines on-the-fly. Thus explicit meta-level |
|
70 |
connectives !! and ==> are rarely required anymore in inductive goals |
|
71 |
(using object-logic connectives for this purpose has been long |
|
72 |
obsolete anyway). The subsequent proof patterns illustrate advanced |
|
73 |
techniques of natural induction; general datatypes and inductive sets |
|
18267 | 74 |
work analogously (see also src/HOL/Lambda for realistic examples). |
75 |
||
76 |
(1) This is how to ``strengthen'' an inductive goal wrt. certain |
|
18239 | 77 |
parameters: |
18233 | 78 |
|
79 |
lemma |
|
80 |
fixes n :: nat and x :: 'a |
|
81 |
assumes a: "A n x" |
|
82 |
shows "P n x" |
|
83 |
using a -- {* make induct insert fact a *} |
|
84 |
proof (induct n fixing: x) -- {* generalize goal to "!!x. A n x ==> P n x" *} |
|
18248 | 85 |
case 0 |
18233 | 86 |
show ?case sorry |
87 |
next |
|
18248 | 88 |
case (Suc n) |
18239 | 89 |
note `!!x. A n x ==> P n x` -- {* induction hypothesis, according to induction rule *} |
90 |
note `A (Suc n) x` -- {* induction premise, stemming from fact a *} |
|
18233 | 91 |
show ?case sorry |
92 |
qed |
|
93 |
||
18267 | 94 |
(2) This is how to perform induction over ``expressions of a certain |
18233 | 95 |
form'', using a locally defined inductive parameter n == "a x" |
18239 | 96 |
together with strengthening (the latter is usually required to get |
18267 | 97 |
sufficiently flexible induction hypotheses): |
18233 | 98 |
|
99 |
lemma |
|
100 |
fixes a :: "'a => nat" |
|
101 |
assumes a: "A (a x)" |
|
102 |
shows "P (a x)" |
|
103 |
using a |
|
104 |
proof (induct n == "a x" fixing: x) |
|
105 |
... |
|
106 |
||
18267 | 107 |
See also HOL/Isar_examples/Puzzle.thy for an application of the this |
108 |
particular technique. |
|
109 |
||
110 |
(3) This is how to perform existential reasoning ('obtain') by |
|
111 |
induction, while avoiding explicit object-logic encodings: |
|
112 |
||
113 |
fix n :: nat |
|
114 |
obtain x :: 'a where "P n x" and "Q n x" |
|
115 |
proof (induct n fixing: thesis) |
|
116 |
case 0 |
|
117 |
obtain x where "P 0 x" and "Q 0 x" sorry |
|
18399 | 118 |
then show thesis by (rule 0) |
18267 | 119 |
next |
120 |
case (Suc n) |
|
121 |
obtain x where "P n x" and "Q n x" by (rule Suc.hyps) |
|
122 |
obtain x where "P (Suc n) x" and "Q (Suc n) x" sorry |
|
123 |
then show thesis by (rule Suc.prems) |
|
124 |
qed |
|
125 |
||
126 |
Here the 'fixing: thesis' specification essentially modifies the scope |
|
127 |
of the formal thesis parameter, in order to the get the whole |
|
128 |
existence statement through the induction as expected. |
|
18233 | 129 |
|
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
130 |
* Provers/induct: mutual goals no longer result in object-level |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
131 |
conjunction, but in properly split meta-level statements, |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
132 |
INCOMPATIBILITY. The corresponding cases are duplicated accordingly, |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
133 |
with the case names being indexed according to the number of |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
134 |
conjuncts. For example: |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
135 |
|
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
136 |
lemma |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
137 |
fixes n :: nat |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
138 |
shows "P n" and "Q n" |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
139 |
proof (induct n) |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
140 |
case 01 |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
141 |
show "P 0" sorry |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
142 |
next |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
143 |
case 02 |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
144 |
show "Q 0" sorry |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
145 |
next |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
146 |
case (Suc1 n) |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
147 |
note `P n` and `Q n` |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
148 |
show "P (Suc n)" sorry |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
149 |
next |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
150 |
case (Suc2 n) |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
151 |
note `P n` and `Q n` |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
152 |
show "Q (Suc n)" sorry |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
153 |
qed |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
154 |
|
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
155 |
* Provers/induct: mutual induction rules are now specified as a list |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
156 |
of rule sharing the same induction cases. HOL packages usually |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
157 |
provide foo_bar.inducts for mutually defined items foo and bar |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
158 |
(e.g. inductive sets or datatypes). INCOMPATIBILITY, users need to |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
159 |
specify mutual induction rules differently, e.g. like this: |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
160 |
|
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
161 |
(induct rule: foo_bar.inducts) |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
162 |
(induct set: foo bar) |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
163 |
(induct type: foo bar) |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
164 |
|
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
165 |
Moreover, the ML function ProjectRule.projections turns old-style |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
166 |
rules into the new format. |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
167 |
|
18399 | 168 |
* Provers/induct: support coinduction as well. See |
169 |
src/HOL/Library/Coinductive_List.thy for various examples. |
|
170 |
||
17779 | 171 |
* Input syntax now supports dummy variable binding "%_. b", where the |
172 |
body does not mention the bound variable. Note that dummy patterns |
|
173 |
implicitly depend on their context of bounds, which makes "{_. _}" |
|
17780 | 174 |
match any set comprehension as expected. Potential INCOMPATIBILITY -- |
175 |
parse translations need to cope with syntactic constant "_idtdummy" in |
|
176 |
the binding position. |
|
177 |
||
178 |
* Removed obsolete syntactic constant "_K" and its associated parse |
|
179 |
translation. INCOMPATIBILITY -- use dummy abstraction instead, for |
|
17779 | 180 |
example "A -> B" => "Pi A (%_. B)". |
181 |
||
17865 | 182 |
|
17806 | 183 |
*** HOL *** |
184 |
||
17996 | 185 |
* Alternative iff syntax "A <-> B" for equality on bool (with priority |
186 |
25 like -->); output depends on the "iff" print_mode, the default is |
|
187 |
"A = B" (with priority 50). |
|
188 |
||
17865 | 189 |
* In the context of the assumption "~(s = t)" the Simplifier rewrites |
190 |
"t = s" to False (by simproc "neq_simproc"). For backward |
|
191 |
compatibility this can be disabled by ML "reset use_neq_simproc". |
|
17779 | 192 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17806
diff
changeset
|
193 |
* Tactics 'sat' and 'satx' reimplemented, several improvements: goals |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17806
diff
changeset
|
194 |
no longer need to be stated as "<prems> ==> False", equivalences (i.e. |
17865 | 195 |
"=" on type bool) are handled, variable names of the form "lit_<n>" |
196 |
are no longer reserved, significant speedup. |
|
197 |
||
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
198 |
* inductive and datatype: provide projections of mutual rules, bundled |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
199 |
as foo_bar.inducts; |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
200 |
|
18446 | 201 |
* Library: added theory Coinductive_List of potentially infinite lists |
202 |
as greatest fixed-point. |
|
18399 | 203 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17806
diff
changeset
|
204 |
|
17878 | 205 |
*** ML *** |
206 |
||
18450
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
207 |
* Pure/library: |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
208 |
|
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
209 |
val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
210 |
val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
211 |
|
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
212 |
The semantics of "burrow" is: "take a function with *simulatanously* transforms |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
213 |
a list of value, and apply it *simulatanously* to a list of list of values of the |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
214 |
appropriate type". Confer this with "map" which would *not* apply its argument |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
215 |
function simulatanously but in sequence. "burrow_split" allows the transformator |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
216 |
function to yield an additional side result. |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
217 |
|
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
218 |
Both actually avoid the usage of "unflat" since they hide away "unflat" |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
219 |
from the user. |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
220 |
|
18446 | 221 |
* Pure/library: functions map2 and fold2 with curried syntax for |
222 |
simultanous mapping and folding: |
|
223 |
||
18422
875451c9d253
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18399
diff
changeset
|
224 |
val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list |
875451c9d253
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18399
diff
changeset
|
225 |
val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c |
875451c9d253
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18399
diff
changeset
|
226 |
|
18446 | 227 |
* Pure/library: indexed lists - some functions in the Isabelle library |
228 |
treating lists over 'a as finite mappings from [0...n] to 'a have been |
|
229 |
given more convenient names and signatures reminiscent of similar |
|
230 |
functions for alists, tables, etc: |
|
18051 | 231 |
|
232 |
val nth: 'a list -> int -> 'a |
|
233 |
val nth_update: int * 'a -> 'a list -> 'a list |
|
234 |
val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list |
|
235 |
val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b |
|
236 |
||
18446 | 237 |
Note that fold_index starts counting at index 0, not 1 like foldln |
238 |
used to. |
|
239 |
||
240 |
* Pure/General: name_mangler.ML provides a functor for generic name |
|
241 |
mangling (bijective mapping from any expression values to strings). |
|
242 |
||
243 |
* Pure/General: rat.ML implements rational numbers. |
|
244 |
||
245 |
* Pure: several functions of signature "... -> theory -> theory * ..." |
|
246 |
have been reoriented to "... -> theory -> ... * theory" in order to |
|
247 |
allow natural usage in combination with the ||>, ||>>, |-> and |
|
248 |
fold_map combinators. |
|
18051 | 249 |
|
18020 | 250 |
* Pure: primitive rule lift_rule now takes goal cterm instead of an |
18145 | 251 |
actual goal state (thm). Use Thm.lift_rule (Thm.cprem_of st i) to |
18020 | 252 |
achieve the old behaviour. |
253 |
||
254 |
* Pure: the "Goal" constant is now called "prop", supporting a |
|
255 |
slightly more general idea of ``protecting'' meta-level rule |
|
256 |
statements. |
|
257 |
||
17981
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
258 |
* Internal goals: structure Goal provides simple interfaces for |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
259 |
init/conclude/finish and tactical prove operations (replacing former |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
260 |
Tactic.prove). Note that OldGoals.prove_goalw_cterm has long been |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
261 |
obsolete, it is ill-behaved in a local proof context (e.g. with local |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
262 |
fixes/assumes or in a locale context). |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
263 |
|
17878 | 264 |
* Simplifier: the simpset of a running simplification process now |
265 |
contains a proof context (cf. Simplifier.the_context), which is the |
|
266 |
very context that the initial simpset has been retrieved from (by |
|
17890 | 267 |
simpset_of/local_simpset_of). Consequently, all plug-in components |
17878 | 268 |
(solver, looper etc.) may depend on arbitrary proof data. |
269 |
||
270 |
* Simplifier.inherit_context inherits the proof context (plus the |
|
271 |
local bounds) of the current simplification process; any simproc |
|
272 |
etc. that calls the Simplifier recursively should do this! Removed |
|
273 |
former Simplifier.inherit_bounds, which is already included here -- |
|
17890 | 274 |
INCOMPATIBILITY. Tools based on low-level rewriting may even have to |
275 |
specify an explicit context using Simplifier.context/theory_context. |
|
17878 | 276 |
|
277 |
* Simplifier/Classical Reasoner: more abstract interfaces |
|
278 |
change_simpset/claset for modifying the simpset/claset reference of a |
|
279 |
theory; raw versions simpset/claset_ref etc. have been discontinued -- |
|
280 |
INCOMPATIBILITY. |
|
281 |
||
282 |
||
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
283 |
|
17720 | 284 |
New in Isabelle2005 (October 2005) |
285 |
---------------------------------- |
|
14655
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset
|
286 |
|
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset
|
287 |
*** General *** |
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset
|
288 |
|
15130 | 289 |
* Theory headers: the new header syntax for Isar theories is |
290 |
||
291 |
theory <name> |
|
16234 | 292 |
imports <theory1> ... <theoryN> |
293 |
uses <file1> ... <fileM> |
|
15130 | 294 |
begin |
295 |
||
16234 | 296 |
where the 'uses' part is optional. The previous syntax |
297 |
||
298 |
theory <name> = <theory1> + ... + <theoryN>: |
|
299 |
||
16717 | 300 |
will disappear in the next release. Use isatool fixheaders to convert |
301 |
existing theory files. Note that there is no change in ancient |
|
17371 | 302 |
non-Isar theories now, but these will disappear soon. |
15130 | 303 |
|
15475
fdf9434b04ea
- Proofs are now hidden by default when generating documents
berghofe
parents:
15454
diff
changeset
|
304 |
* Theory loader: parent theories can now also be referred to via |
16234 | 305 |
relative and absolute paths. |
306 |
||
17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
307 |
* Command 'find_theorems' searches for a list of criteria instead of a |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
308 |
list of constants. Known criteria are: intro, elim, dest, name:string, |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
309 |
simp:term, and any term. Criteria can be preceded by '-' to select |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
310 |
theorems that do not match. Intro, elim, dest select theorems that |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
311 |
match the current goal, name:s selects theorems whose fully qualified |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
312 |
name contain s, and simp:term selects all simplification rules whose |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
313 |
lhs match term. Any other term is interpreted as pattern and selects |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
314 |
all theorems matching the pattern. Available in ProofGeneral under |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
315 |
'ProofGeneral -> Find Theorems' or C-c C-f. Example: |
16234 | 316 |
|
17275
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset
|
317 |
C-c C-f (100) "(_::nat) + _ + _" intro -name: "HOL." |
16234 | 318 |
|
319 |
prints the last 100 theorems matching the pattern "(_::nat) + _ + _", |
|
320 |
matching the current goal as introduction rule and not having "HOL." |
|
321 |
in their name (i.e. not being defined in theory HOL). |
|
16013
3010430d894d
removed find_rewrites (superceded by improved thms_containing);
wenzelm
parents:
16000
diff
changeset
|
322 |
|
17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
323 |
* Command 'thms_containing' has been discontinued in favour of |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
324 |
'find_theorems'; INCOMPATIBILITY. |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
325 |
|
17385 | 326 |
* Communication with Proof General is now 8bit clean, which means that |
327 |
Unicode text in UTF-8 encoding may be used within theory texts (both |
|
17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
328 |
formal and informal parts). Cf. option -U of the Isabelle Proof |
17538 | 329 |
General interface. Here are some simple examples (cf. src/HOL/ex): |
330 |
||
331 |
http://isabelle.in.tum.de/library/HOL/ex/Hebrew.html |
|
332 |
http://isabelle.in.tum.de/library/HOL/ex/Chinese.html |
|
17385 | 333 |
|
17425 | 334 |
* Improved efficiency of the Simplifier and, to a lesser degree, the |
335 |
Classical Reasoner. Typical big applications run around 2 times |
|
336 |
faster. |
|
337 |
||
15703 | 338 |
|
339 |
*** Document preparation *** |
|
340 |
||
16234 | 341 |
* Commands 'display_drafts' and 'print_drafts' perform simple output |
342 |
of raw sources. Only those symbols that do not require additional |
|
343 |
LaTeX packages (depending on comments in isabellesym.sty) are |
|
344 |
displayed properly, everything else is left verbatim. isatool display |
|
345 |
and isatool print are used as front ends (these are subject to the |
|
346 |
DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively). |
|
347 |
||
17047
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
348 |
* Command tags control specific markup of certain regions of text, |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
349 |
notably folding and hiding. Predefined tags include "theory" (for |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
350 |
theory begin and end), "proof" for proof commands, and "ML" for |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
351 |
commands involving ML code; the additional tags "visible" and |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
352 |
"invisible" are unused by default. Users may give explicit tag |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
353 |
specifications in the text, e.g. ''by %invisible (auto)''. The |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
354 |
interpretation of tags is determined by the LaTeX job during document |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
355 |
preparation: see option -V of isatool usedir, or options -n and -t of |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
356 |
isatool document, or even the LaTeX macros \isakeeptag, \isafoldtag, |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
357 |
\isadroptag. |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
358 |
|
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
359 |
Several document versions may be produced at the same time via isatool |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
360 |
usedir (the generated index.html will link all of them). Typical |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
361 |
specifications include ''-V document=theory,proof,ML'' to present |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
362 |
theory/proof/ML parts faithfully, ''-V outline=/proof,/ML'' to fold |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
363 |
proof and ML commands, and ''-V mutilated=-theory,-proof,-ML'' to omit |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
364 |
these parts without any formal replacement text. The Isabelle site |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
365 |
default settings produce ''document'' and ''outline'' versions as |
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir -H);
wenzelm
parents:
17016
diff
changeset
|
366 |
specified above. |
16234 | 367 |
|
17402 | 368 |
* Several new antiquotations: |
15979 | 369 |
|
370 |
@{term_type term} prints a term with its type annotated; |
|
371 |
||
372 |
@{typeof term} prints the type of a term; |
|
373 |
||
16234 | 374 |
@{const const} is the same as @{term const}, but checks that the |
375 |
argument is a known logical constant; |
|
15979 | 376 |
|
377 |
@{term_style style term} and @{thm_style style thm} print a term or |
|
16234 | 378 |
theorem applying a "style" to it |
379 |
||
17117
e2bed9e82454
* The ML antiquotation prints type-checked ML expressions verbatim.
wenzelm
parents:
17097
diff
changeset
|
380 |
@{ML text} |
e2bed9e82454
* The ML antiquotation prints type-checked ML expressions verbatim.
wenzelm
parents:
17097
diff
changeset
|
381 |
|
16234 | 382 |
Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of |
383 |
definitions, equations, inequations etc., 'concl' printing only the |
|
17393 | 384 |
conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem19' |
16234 | 385 |
to print the specified premise. TermStyle.add_style provides an ML |
386 |
interface for introducing further styles. See also the "LaTeX Sugar" |
|
17117
e2bed9e82454
* The ML antiquotation prints type-checked ML expressions verbatim.
wenzelm
parents:
17097
diff
changeset
|
387 |
document practical applications. The ML antiquotation prints |
e2bed9e82454
* The ML antiquotation prints type-checked ML expressions verbatim.
wenzelm
parents:
17097
diff
changeset
|
388 |
type-checked ML expressions verbatim. |
16234 | 389 |
|
17259
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset
|
390 |
* Markup commands 'chapter', 'section', 'subsection', 'subsubsection', |
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset
|
391 |
and 'text' support optional locale specification '(in loc)', which |
17269 | 392 |
specifies the default context for interpreting antiquotations. For |
393 |
example: 'text (in lattice) {* @{thm inf_assoc}*}'. |
|
17259
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset
|
394 |
|
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset
|
395 |
* Option 'locale=NAME' of antiquotations specifies an alternative |
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset
|
396 |
context interpreting the subsequent argument. For example: @{thm |
17269 | 397 |
[locale=lattice] inf_assoc}. |
17259
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset
|
398 |
|
17097
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset
|
399 |
* Proper output of proof terms (@{prf ...} and @{full_prf ...}) within |
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset
|
400 |
a proof context. |
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset
|
401 |
|
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset
|
402 |
* Proper output of antiquotations for theory commands involving a |
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset
|
403 |
proof context (such as 'locale' or 'theorem (in loc) ...'). |
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset
|
404 |
|
17193
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset
|
405 |
* Delimiters of outer tokens (string etc.) now produce separate LaTeX |
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset
|
406 |
macros (\isachardoublequoteopen, isachardoublequoteclose etc.). |
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset
|
407 |
|
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset
|
408 |
* isatool usedir: new option -C (default true) controls whether option |
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset
|
409 |
-D should include a copy of the original document directory; -C false |
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset
|
410 |
prevents unwanted effects such as copying of administrative CVS data. |
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset
|
411 |
|
16234 | 412 |
|
413 |
*** Pure *** |
|
414 |
||
415 |
* Considerably improved version of 'constdefs' command. Now performs |
|
416 |
automatic type-inference of declared constants; additional support for |
|
417 |
local structure declarations (cf. locales and HOL records), see also |
|
418 |
isar-ref manual. Potential INCOMPATIBILITY: need to observe strictly |
|
419 |
sequential dependencies of definitions within a single 'constdefs' |
|
420 |
section; moreover, the declared name needs to be an identifier. If |
|
421 |
all fails, consider to fall back on 'consts' and 'defs' separately. |
|
422 |
||
423 |
* Improved indexed syntax and implicit structures. First of all, |
|
424 |
indexed syntax provides a notational device for subscripted |
|
425 |
application, using the new syntax \<^bsub>term\<^esub> for arbitrary |
|
426 |
expressions. Secondly, in a local context with structure |
|
427 |
declarations, number indexes \<^sub>n or the empty index (default |
|
428 |
number 1) refer to a certain fixed variable implicitly; option |
|
429 |
show_structs controls printing of implicit structures. Typical |
|
430 |
applications of these concepts involve record types and locales. |
|
431 |
||
432 |
* New command 'no_syntax' removes grammar declarations (and |
|
433 |
translations) resulting from the given syntax specification, which is |
|
434 |
interpreted in the same manner as for the 'syntax' command. |
|
435 |
||
436 |
* 'Advanced' translation functions (parse_translation etc.) may depend |
|
437 |
on the signature of the theory context being presently used for |
|
438 |
parsing/printing, see also isar-ref manual. |
|
439 |
||
16856 | 440 |
* Improved 'oracle' command provides a type-safe interface to turn an |
441 |
ML expression of type theory -> T -> term into a primitive rule of |
|
442 |
type theory -> T -> thm (i.e. the functionality of Thm.invoke_oracle |
|
443 |
is already included here); see also FOL/ex/IffExample.thy; |
|
444 |
INCOMPATIBILITY. |
|
445 |
||
17275
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset
|
446 |
* axclass: name space prefix for class "c" is now "c_class" (was "c" |
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset
|
447 |
before); "cI" is no longer bound, use "c.intro" instead. |
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset
|
448 |
INCOMPATIBILITY. This change avoids clashes of fact bindings for |
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset
|
449 |
axclasses vs. locales. |
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset
|
450 |
|
16234 | 451 |
* Improved internal renaming of symbolic identifiers -- attach primes |
452 |
instead of base 26 numbers. |
|
453 |
||
454 |
* New flag show_question_marks controls printing of leading question |
|
455 |
marks in schematic variable names. |
|
456 |
||
457 |
* In schematic variable names, *any* symbol following \<^isub> or |
|
458 |
\<^isup> is now treated as part of the base name. For example, the |
|
459 |
following works without printing of awkward ".0" indexes: |
|
460 |
||
461 |
lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1" |
|
462 |
by simp |
|
463 |
||
464 |
* Inner syntax includes (*(*nested*) comments*). |
|
465 |
||
17548 | 466 |
* Pretty printer now supports unbreakable blocks, specified in mixfix |
16234 | 467 |
annotations as "(00...)". |
468 |
||
469 |
* Clear separation of logical types and nonterminals, where the latter |
|
470 |
may only occur in 'syntax' specifications or type abbreviations. |
|
471 |
Before that distinction was only partially implemented via type class |
|
472 |
"logic" vs. "{}". Potential INCOMPATIBILITY in rare cases of improper |
|
473 |
use of 'types'/'consts' instead of 'nonterminals'/'syntax'. Some very |
|
474 |
exotic syntax specifications may require further adaption |
|
17691 | 475 |
(e.g. Cube/Cube.thy). |
16234 | 476 |
|
477 |
* Removed obsolete type class "logic", use the top sort {} instead. |
|
478 |
Note that non-logical types should be declared as 'nonterminals' |
|
479 |
rather than 'types'. INCOMPATIBILITY for new object-logic |
|
480 |
specifications. |
|
481 |
||
17095 | 482 |
* Attributes 'induct' and 'cases': type or set names may now be |
483 |
locally fixed variables as well. |
|
484 |
||
16234 | 485 |
* Simplifier: can now control the depth to which conditional rewriting |
486 |
is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth |
|
487 |
Limit. |
|
488 |
||
489 |
* Simplifier: simplification procedures may now take the current |
|
490 |
simpset into account (cf. Simplifier.simproc(_i) / mk_simproc |
|
491 |
interface), which is very useful for calling the Simplifier |
|
492 |
recursively. Minor INCOMPATIBILITY: the 'prems' argument of simprocs |
|
493 |
is gone -- use prems_of_ss on the simpset instead. Moreover, the |
|
494 |
low-level mk_simproc no longer applies Logic.varify internally, to |
|
495 |
allow for use in a context of fixed variables. |
|
496 |
||
497 |
* thin_tac now works even if the assumption being deleted contains !! |
|
498 |
or ==>. More generally, erule now works even if the major premise of |
|
499 |
the elimination rule contains !! or ==>. |
|
500 |
||
17597 | 501 |
* Method 'rules' has been renamed to 'iprover'. INCOMPATIBILITY. |
17590 | 502 |
|
16234 | 503 |
* Reorganized bootstrapping of the Pure theories; CPure is now derived |
504 |
from Pure, which contains all common declarations already. Both |
|
505 |
theories are defined via plain Isabelle/Isar .thy files. |
|
506 |
INCOMPATIBILITY: elements of CPure (such as the CPure.intro / |
|
507 |
CPure.elim / CPure.dest attributes) now appear in the Pure name space; |
|
508 |
use isatool fixcpure to adapt your theory and ML sources. |
|
509 |
||
510 |
* New syntax 'name(i-j, i-, i, ...)' for referring to specific |
|
511 |
selections of theorems in named facts via index ranges. |
|
512 |
||
17097
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset
|
513 |
* 'print_theorems': in theory mode, really print the difference |
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset
|
514 |
wrt. the last state (works for interactive theory development only), |
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset
|
515 |
in proof mode print all local facts (cf. 'print_facts'); |
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset
|
516 |
|
17397 | 517 |
* 'hide': option '(open)' hides only base names. |
518 |
||
17275
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset
|
519 |
* More efficient treatment of intermediate checkpoints in interactive |
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset
|
520 |
theory development. |
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset
|
521 |
|
17663
28be54ff74f8
Added entries for code_module, code_library, and value.
berghofe
parents:
17641
diff
changeset
|
522 |
* Code generator is now invoked via code_module (incremental code |
17664 | 523 |
generation) and code_library (modular code generation, ML structures |
524 |
for each theory). INCOMPATIBILITY: new keywords 'file' and 'contains' |
|
525 |
must be quoted when used as identifiers. |
|
526 |
||
527 |
* New 'value' command for reading, evaluating and printing terms using |
|
528 |
the code generator. INCOMPATIBILITY: command keyword 'value' must be |
|
529 |
quoted when used as identifier. |
|
17663
28be54ff74f8
Added entries for code_module, code_library, and value.
berghofe
parents:
17641
diff
changeset
|
530 |
|
16234 | 531 |
|
532 |
*** Locales *** |
|
17095 | 533 |
|
17385 | 534 |
* New commands for the interpretation of locale expressions in |
535 |
theories (1), locales (2) and proof contexts (3). These generate |
|
536 |
proof obligations from the expression specification. After the |
|
537 |
obligations have been discharged, theorems of the expression are added |
|
538 |
to the theory, target locale or proof context. The synopsis of the |
|
539 |
commands is a follows: |
|
540 |
||
17095 | 541 |
(1) interpretation expr inst |
542 |
(2) interpretation target < expr |
|
543 |
(3) interpret expr inst |
|
17385 | 544 |
|
17095 | 545 |
Interpretation in theories and proof contexts require a parameter |
546 |
instantiation of terms from the current context. This is applied to |
|
17385 | 547 |
specifications and theorems of the interpreted expression. |
548 |
Interpretation in locales only permits parameter renaming through the |
|
549 |
locale expression. Interpretation is smart in that interpretations |
|
550 |
that are active already do not occur in proof obligations, neither are |
|
551 |
instantiated theorems stored in duplicate. Use 'print_interps' to |
|
552 |
inspect active interpretations of a particular locale. For details, |
|
17436 | 553 |
see the Isar Reference manual. Examples can be found in |
554 |
HOL/Finite_Set.thy and HOL/Algebra/UnivPoly.thy. |
|
16234 | 555 |
|
556 |
INCOMPATIBILITY: former 'instantiate' has been withdrawn, use |
|
557 |
'interpret' instead. |
|
558 |
||
17385 | 559 |
* New context element 'constrains' for adding type constraints to |
560 |
parameters. |
|
561 |
||
562 |
* Context expressions: renaming of parameters with syntax |
|
563 |
redeclaration. |
|
17095 | 564 |
|
565 |
* Locale declaration: 'includes' disallowed. |
|
566 |
||
16234 | 567 |
* Proper static binding of attribute syntax -- i.e. types / terms / |
568 |
facts mentioned as arguments are always those of the locale definition |
|
569 |
context, independently of the context of later invocations. Moreover, |
|
570 |
locale operations (renaming and type / term instantiation) are applied |
|
571 |
to attribute arguments as expected. |
|
572 |
||
573 |
INCOMPATIBILITY of the ML interface: always pass Attrib.src instead of |
|
574 |
actual attributes; rare situations may require Attrib.attribute to |
|
575 |
embed those attributes into Attrib.src that lack concrete syntax. |
|
576 |
Attribute implementations need to cooperate properly with the static |
|
577 |
binding mechanism. Basic parsers Args.XXX_typ/term/prop and |
|
578 |
Attrib.XXX_thm etc. already do the right thing without further |
|
579 |
intervention. Only unusual applications -- such as "where" or "of" |
|
580 |
(cf. src/Pure/Isar/attrib.ML), which process arguments depending both |
|
581 |
on the context and the facts involved -- may have to assign parsed |
|
582 |
values to argument tokens explicitly. |
|
583 |
||
584 |
* Changed parameter management in theorem generation for long goal |
|
585 |
statements with 'includes'. INCOMPATIBILITY: produces a different |
|
586 |
theorem statement in rare situations. |
|
587 |
||
17228 | 588 |
* Locale inspection command 'print_locale' omits notes elements. Use |
589 |
'print_locale!' to have them included in the output. |
|
590 |
||
16234 | 591 |
|
592 |
*** Provers *** |
|
593 |
||
594 |
* Provers/hypsubst.ML: improved version of the subst method, for |
|
595 |
single-step rewriting: it now works in bound variable contexts. New is |
|
596 |
'subst (asm)', for rewriting an assumption. INCOMPATIBILITY: may |
|
597 |
rewrite a different subterm than the original subst method, which is |
|
598 |
still available as 'simplesubst'. |
|
599 |
||
600 |
* Provers/quasi.ML: new transitivity reasoners for transitivity only |
|
601 |
and quasi orders. |
|
602 |
||
603 |
* Provers/trancl.ML: new transitivity reasoner for transitive and |
|
604 |
reflexive-transitive closure of relations. |
|
605 |
||
606 |
* Provers/blast.ML: new reference depth_limit to make blast's depth |
|
607 |
limit (previously hard-coded with a value of 20) user-definable. |
|
608 |
||
609 |
* Provers/simplifier.ML has been moved to Pure, where Simplifier.setup |
|
610 |
is peformed already. Object-logics merely need to finish their |
|
611 |
initial simpset configuration as before. INCOMPATIBILITY. |
|
15703 | 612 |
|
15475
fdf9434b04ea
- Proofs are now hidden by default when generating documents
berghofe
parents:
15454
diff
changeset
|
613 |
|
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14699
diff
changeset
|
614 |
*** HOL *** |
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14699
diff
changeset
|
615 |
|
16234 | 616 |
* Symbolic syntax of Hilbert Choice Operator is now as follows: |
14878 | 617 |
|
618 |
syntax (epsilon) |
|
619 |
"_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) |
|
620 |
||
16234 | 621 |
The symbol \<some> is displayed as the alternative epsilon of LaTeX |
622 |
and x-symbol; use option '-m epsilon' to get it actually printed. |
|
623 |
Moreover, the mathematically important symbolic identifier \<epsilon> |
|
624 |
becomes available as variable, constant etc. INCOMPATIBILITY, |
|
625 |
||
626 |
* "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x". |
|
627 |
Similarly for all quantifiers: "ALL x > y" etc. The x-symbol for >= |
|
17371 | 628 |
is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to |
17016
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset
|
629 |
support corresponding Isar calculations. |
16234 | 630 |
|
631 |
* "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>" |
|
632 |
instead of ":". |
|
633 |
||
634 |
* theory SetInterval: changed the syntax for open intervals: |
|
635 |
||
636 |
Old New |
|
637 |
{..n(} {..<n} |
|
638 |
{)n..} {n<..} |
|
639 |
{m..n(} {m..<n} |
|
640 |
{)m..n} {m<..n} |
|
641 |
{)m..n(} {m<..<n} |
|
642 |
||
643 |
The old syntax is still supported but will disappear in the next |
|
644 |
release. For conversion use the following Emacs search and replace |
|
645 |
patterns (these are not perfect but work quite well): |
|
15046 | 646 |
|
647 |
{)\([^\.]*\)\.\. -> {\1<\.\.} |
|
648 |
\.\.\([^(}]*\)(} -> \.\.<\1} |
|
649 |
||
17533 | 650 |
* Theory Commutative_Ring (in Library): method comm_ring for proving |
651 |
equalities in commutative rings; method 'algebra' provides a generic |
|
652 |
interface. |
|
17389
b4743198b939
Method comm_ring for proving equalities in commutative rings.
wenzelm
parents:
17385
diff
changeset
|
653 |
|
b4743198b939
Method comm_ring for proving equalities in commutative rings.
wenzelm
parents:
17385
diff
changeset
|
654 |
* Theory Finite_Set: changed the syntax for 'setsum', summation over |
16234 | 655 |
finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is |
17371 | 656 |
now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can |
17189 | 657 |
be a tuple pattern. |
16234 | 658 |
|
659 |
Some new syntax forms are available: |
|
660 |
||
661 |
"\<Sum>x | P. e" for "setsum (%x. e) {x. P}" |
|
662 |
"\<Sum>x = a..b. e" for "setsum (%x. e) {a..b}" |
|
663 |
"\<Sum>x = a..<b. e" for "setsum (%x. e) {a..<b}" |
|
664 |
"\<Sum>x < k. e" for "setsum (%x. e) {..<k}" |
|
665 |
||
666 |
The latter form "\<Sum>x < k. e" used to be based on a separate |
|
667 |
function "Summation", which has been discontinued. |
|
668 |
||
669 |
* theory Finite_Set: in structured induction proofs, the insert case |
|
670 |
is now 'case (insert x F)' instead of the old counterintuitive 'case |
|
671 |
(insert F x)'. |
|
672 |
||
673 |
* The 'refute' command has been extended to support a much larger |
|
674 |
fragment of HOL, including axiomatic type classes, constdefs and |
|
675 |
typedefs, inductive datatypes and recursion. |
|
676 |
||
17700 | 677 |
* New tactics 'sat' and 'satx' to prove propositional tautologies. |
678 |
Requires zChaff with proof generation to be installed. See |
|
679 |
HOL/ex/SAT_Examples.thy for examples. |
|
17619 | 680 |
|
16234 | 681 |
* Datatype induction via method 'induct' now preserves the name of the |
682 |
induction variable. For example, when proving P(xs::'a list) by |
|
683 |
induction on xs, the induction step is now P(xs) ==> P(a#xs) rather |
|
684 |
than P(list) ==> P(a#list) as previously. Potential INCOMPATIBILITY |
|
685 |
in unstructured proof scripts. |
|
686 |
||
687 |
* Reworked implementation of records. Improved scalability for |
|
688 |
records with many fields, avoiding performance problems for type |
|
689 |
inference. Records are no longer composed of nested field types, but |
|
690 |
of nested extension types. Therefore the record type only grows linear |
|
691 |
in the number of extensions and not in the number of fields. The |
|
692 |
top-level (users) view on records is preserved. Potential |
|
693 |
INCOMPATIBILITY only in strange cases, where the theory depends on the |
|
694 |
old record representation. The type generated for a record is called |
|
695 |
<record_name>_ext_type. |
|
696 |
||
697 |
Flag record_quick_and_dirty_sensitive can be enabled to skip the |
|
698 |
proofs triggered by a record definition or a simproc (if |
|
699 |
quick_and_dirty is enabled). Definitions of large records can take |
|
700 |
quite long. |
|
701 |
||
702 |
New simproc record_upd_simproc for simplification of multiple record |
|
703 |
updates enabled by default. Moreover, trivial updates are also |
|
704 |
removed: r(|x := x r|) = r. INCOMPATIBILITY: old proofs break |
|
705 |
occasionally, since simplification is more powerful by default. |
|
706 |
||
17275
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset
|
707 |
* typedef: proper support for polymorphic sets, which contain extra |
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset
|
708 |
type-variables in the term. |
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset
|
709 |
|
16234 | 710 |
* Simplifier: automatically reasons about transitivity chains |
711 |
involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics |
|
712 |
provided by Provers/trancl.ML as additional solvers. INCOMPATIBILITY: |
|
713 |
old proofs break occasionally as simplification may now solve more |
|
714 |
goals than previously. |
|
715 |
||
716 |
* Simplifier: converts x <= y into x = y if assumption y <= x is |
|
717 |
present. Works for all partial orders (class "order"), in particular |
|
718 |
numbers and sets. For linear orders (e.g. numbers) it treats ~ x < y |
|
719 |
just like y <= x. |
|
720 |
||
721 |
* Simplifier: new simproc for "let x = a in f x". If a is a free or |
|
722 |
bound variable or a constant then the let is unfolded. Otherwise |
|
723 |
first a is simplified to b, and then f b is simplified to g. If |
|
724 |
possible we abstract b from g arriving at "let x = b in h x", |
|
725 |
otherwise we unfold the let and arrive at g. The simproc can be |
|
726 |
enabled/disabled by the reference use_let_simproc. Potential |
|
727 |
INCOMPATIBILITY since simplification is more powerful by default. |
|
15776 | 728 |
|
16563 | 729 |
* Classical reasoning: the meson method now accepts theorems as arguments. |
730 |
||
17595 | 731 |
* Prover support: pre-release of the Isabelle-ATP linkup, which runs background |
732 |
jobs to provide advice on the provability of subgoals. |
|
733 |
||
16891 | 734 |
* Theory OrderedGroup and Ring_and_Field: various additions and |
735 |
improvements to faciliate calculations involving equalities and |
|
736 |
inequalities. |
|
737 |
||
738 |
The following theorems have been eliminated or modified |
|
739 |
(INCOMPATIBILITY): |
|
16888 | 740 |
|
741 |
abs_eq now named abs_of_nonneg |
|
17371 | 742 |
abs_of_ge_0 now named abs_of_nonneg |
743 |
abs_minus_eq now named abs_of_nonpos |
|
16888 | 744 |
imp_abs_id now named abs_of_nonneg |
745 |
imp_abs_neg_id now named abs_of_nonpos |
|
746 |
mult_pos now named mult_pos_pos |
|
747 |
mult_pos_le now named mult_nonneg_nonneg |
|
748 |
mult_pos_neg_le now named mult_nonneg_nonpos |
|
749 |
mult_pos_neg2_le now named mult_nonneg_nonpos2 |
|
750 |
mult_neg now named mult_neg_neg |
|
751 |
mult_neg_le now named mult_nonpos_nonpos |
|
752 |
||
16891 | 753 |
* Theory Parity: added rules for simplifying exponents. |
754 |
||
17092 | 755 |
* Theory List: |
756 |
||
757 |
The following theorems have been eliminated or modified |
|
758 |
(INCOMPATIBILITY): |
|
759 |
||
760 |
list_all_Nil now named list_all.simps(1) |
|
761 |
list_all_Cons now named list_all.simps(2) |
|
762 |
list_all_conv now named list_all_iff |
|
763 |
set_mem_eq now named mem_iff |
|
764 |
||
16929 | 765 |
* Theories SetsAndFunctions and BigO (see HOL/Library) support |
766 |
asymptotic "big O" calculations. See the notes in BigO.thy. |
|
767 |
||
16888 | 768 |
|
769 |
*** HOL-Complex *** |
|
770 |
||
16891 | 771 |
* Theory RealDef: better support for embedding natural numbers and |
772 |
integers in the reals. |
|
773 |
||
774 |
The following theorems have been eliminated or modified |
|
775 |
(INCOMPATIBILITY): |
|
776 |
||
17016
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset
|
777 |
exp_ge_add_one_self now requires no hypotheses |
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset
|
778 |
real_of_int_add reversed direction of equality (use [symmetric]) |
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset
|
779 |
real_of_int_minus reversed direction of equality (use [symmetric]) |
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset
|
780 |
real_of_int_diff reversed direction of equality (use [symmetric]) |
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset
|
781 |
real_of_int_mult reversed direction of equality (use [symmetric]) |
16891 | 782 |
|
783 |
* Theory RComplete: expanded support for floor and ceiling functions. |
|
16888 | 784 |
|
16962 | 785 |
* Theory Ln is new, with properties of the natural logarithm |
786 |
||
17423 | 787 |
* Hyperreal: There is a new type constructor "star" for making |
788 |
nonstandard types. The old type names are now type synonyms: |
|
789 |
||
790 |
hypreal = real star |
|
791 |
hypnat = nat star |
|
792 |
hcomplex = complex star |
|
793 |
||
794 |
* Hyperreal: Many groups of similarly-defined constants have been |
|
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
795 |
replaced by polymorphic versions (INCOMPATIBILITY): |
17423 | 796 |
|
797 |
star_of <-- hypreal_of_real, hypnat_of_nat, hcomplex_of_complex |
|
798 |
||
799 |
starset <-- starsetNat, starsetC |
|
800 |
*s* <-- *sNat*, *sc* |
|
801 |
starset_n <-- starsetNat_n, starsetC_n |
|
802 |
*sn* <-- *sNatn*, *scn* |
|
803 |
InternalSets <-- InternalNatSets, InternalCSets |
|
804 |
||
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
805 |
starfun <-- starfun{Nat,Nat2,C,RC,CR} |
17423 | 806 |
*f* <-- *fNat*, *fNat2*, *fc*, *fRc*, *fcR* |
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
807 |
starfun_n <-- starfun{Nat,Nat2,C,RC,CR}_n |
17423 | 808 |
*fn* <-- *fNatn*, *fNat2n*, *fcn*, *fRcn*, *fcRn* |
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
809 |
InternalFuns <-- InternalNatFuns, InternalNatFuns2, Internal{C,RC,CR}Funs |
17423 | 810 |
|
811 |
* Hyperreal: Many type-specific theorems have been removed in favor of |
|
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
812 |
theorems specific to various axiomatic type classes (INCOMPATIBILITY): |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
813 |
|
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
814 |
add_commute <-- {hypreal,hypnat,hcomplex}_add_commute |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
815 |
add_assoc <-- {hypreal,hypnat,hcomplex}_add_assocs |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
816 |
OrderedGroup.add_0 <-- {hypreal,hypnat,hcomplex}_add_zero_left |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
817 |
OrderedGroup.add_0_right <-- {hypreal,hcomplex}_add_zero_right |
17423 | 818 |
right_minus <-- hypreal_add_minus |
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
819 |
left_minus <-- {hypreal,hcomplex}_add_minus_left |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
820 |
mult_commute <-- {hypreal,hypnat,hcomplex}_mult_commute |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
821 |
mult_assoc <-- {hypreal,hypnat,hcomplex}_mult_assoc |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
822 |
mult_1_left <-- {hypreal,hypnat}_mult_1, hcomplex_mult_one_left |
17423 | 823 |
mult_1_right <-- hcomplex_mult_one_right |
824 |
mult_zero_left <-- hcomplex_mult_zero_left |
|
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
825 |
left_distrib <-- {hypreal,hypnat,hcomplex}_add_mult_distrib |
17423 | 826 |
right_distrib <-- hypnat_add_mult_distrib2 |
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
827 |
zero_neq_one <-- {hypreal,hypnat,hcomplex}_zero_not_eq_one |
17423 | 828 |
right_inverse <-- hypreal_mult_inverse |
829 |
left_inverse <-- hypreal_mult_inverse_left, hcomplex_mult_inv_left |
|
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
830 |
order_refl <-- {hypreal,hypnat}_le_refl |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
831 |
order_trans <-- {hypreal,hypnat}_le_trans |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
832 |
order_antisym <-- {hypreal,hypnat}_le_anti_sym |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
833 |
order_less_le <-- {hypreal,hypnat}_less_le |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
834 |
linorder_linear <-- {hypreal,hypnat}_le_linear |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
835 |
add_left_mono <-- {hypreal,hypnat}_add_left_mono |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
836 |
mult_strict_left_mono <-- {hypreal,hypnat}_mult_less_mono2 |
17423 | 837 |
add_nonneg_nonneg <-- hypreal_le_add_order |
838 |
||
839 |
* Hyperreal: Separate theorems having to do with type-specific |
|
840 |
versions of constants have been merged into theorems that apply to the |
|
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
841 |
new polymorphic constants (INCOMPATIBILITY): |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
842 |
|
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
843 |
STAR_UNIV_set <-- {STAR_real,NatStar_real,STARC_complex}_set |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
844 |
STAR_empty_set <-- {STAR,NatStar,STARC}_empty_set |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
845 |
STAR_Un <-- {STAR,NatStar,STARC}_Un |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
846 |
STAR_Int <-- {STAR,NatStar,STARC}_Int |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
847 |
STAR_Compl <-- {STAR,NatStar,STARC}_Compl |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
848 |
STAR_subset <-- {STAR,NatStar,STARC}_subset |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
849 |
STAR_mem <-- {STAR,NatStar,STARC}_mem |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
850 |
STAR_mem_Compl <-- {STAR,STARC}_mem_Compl |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
851 |
STAR_diff <-- {STAR,STARC}_diff |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
852 |
STAR_star_of_image_subset <-- {STAR_hypreal_of_real, NatStar_hypreal_of_real, |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
853 |
STARC_hcomplex_of_complex}_image_subset |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
854 |
starset_n_Un <-- starset{Nat,C}_n_Un |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
855 |
starset_n_Int <-- starset{Nat,C}_n_Int |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
856 |
starset_n_Compl <-- starset{Nat,C}_n_Compl |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
857 |
starset_n_diff <-- starset{Nat,C}_n_diff |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
858 |
InternalSets_Un <-- Internal{Nat,C}Sets_Un |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
859 |
InternalSets_Int <-- Internal{Nat,C}Sets_Int |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
860 |
InternalSets_Compl <-- Internal{Nat,C}Sets_Compl |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
861 |
InternalSets_diff <-- Internal{Nat,C}Sets_diff |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
862 |
InternalSets_UNIV_diff <-- Internal{Nat,C}Sets_UNIV_diff |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
863 |
InternalSets_starset_n <-- Internal{Nat,C}Sets_starset{Nat,C}_n |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
864 |
starset_starset_n_eq <-- starset{Nat,C}_starset{Nat,C}_n_eq |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
865 |
starset_n_starset <-- starset{Nat,C}_n_starset{Nat,C} |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
866 |
starfun_n_starfun <-- starfun{Nat,Nat2,C,RC,CR}_n_starfun{Nat,Nat2,C,RC,CR} |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
867 |
starfun <-- starfun{Nat,Nat2,C,RC,CR} |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
868 |
starfun_mult <-- starfun{Nat,Nat2,C,RC,CR}_mult |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
869 |
starfun_add <-- starfun{Nat,Nat2,C,RC,CR}_add |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
870 |
starfun_minus <-- starfun{Nat,Nat2,C,RC,CR}_minus |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
871 |
starfun_diff <-- starfun{C,RC,CR}_diff |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
872 |
starfun_o <-- starfun{NatNat2,Nat2,_stafunNat,C,C_starfunRC,_starfunCR}_o |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
873 |
starfun_o2 <-- starfun{NatNat2,_stafunNat,C,C_starfunRC,_starfunCR}_o2 |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
874 |
starfun_const_fun <-- starfun{Nat,Nat2,C,RC,CR}_const_fun |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
875 |
starfun_inverse <-- starfun{Nat,C,RC,CR}_inverse |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
876 |
starfun_eq <-- starfun{Nat,Nat2,C,RC,CR}_eq |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
877 |
starfun_eq_iff <-- starfun{C,RC,CR}_eq_iff |
17423 | 878 |
starfun_Id <-- starfunC_Id |
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
879 |
starfun_approx <-- starfun{Nat,CR}_approx |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
880 |
starfun_capprox <-- starfun{C,RC}_capprox |
17423 | 881 |
starfun_abs <-- starfunNat_rabs |
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
882 |
starfun_lambda_cancel <-- starfun{C,CR,RC}_lambda_cancel |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
883 |
starfun_lambda_cancel2 <-- starfun{C,CR,RC}_lambda_cancel2 |
17423 | 884 |
starfun_mult_HFinite_approx <-- starfunCR_mult_HFinite_capprox |
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
885 |
starfun_mult_CFinite_capprox <-- starfun{C,RC}_mult_CFinite_capprox |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
886 |
starfun_add_capprox <-- starfun{C,RC}_add_capprox |
17423 | 887 |
starfun_add_approx <-- starfunCR_add_approx |
888 |
starfun_inverse_inverse <-- starfunC_inverse_inverse |
|
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
889 |
starfun_divide <-- starfun{C,CR,RC}_divide |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
890 |
starfun_n <-- starfun{Nat,C}_n |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
891 |
starfun_n_mult <-- starfun{Nat,C}_n_mult |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
892 |
starfun_n_add <-- starfun{Nat,C}_n_add |
17423 | 893 |
starfun_n_add_minus <-- starfunNat_n_add_minus |
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
894 |
starfun_n_const_fun <-- starfun{Nat,C}_n_const_fun |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
895 |
starfun_n_minus <-- starfun{Nat,C}_n_minus |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
896 |
starfun_n_eq <-- starfun{Nat,C}_n_eq |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
897 |
|
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
898 |
star_n_add <-- {hypreal,hypnat,hcomplex}_add |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
899 |
star_n_minus <-- {hypreal,hcomplex}_minus |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
900 |
star_n_diff <-- {hypreal,hcomplex}_diff |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
901 |
star_n_mult <-- {hypreal,hcomplex}_mult |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
902 |
star_n_inverse <-- {hypreal,hcomplex}_inverse |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
903 |
star_n_le <-- {hypreal,hypnat}_le |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
904 |
star_n_less <-- {hypreal,hypnat}_less |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
905 |
star_n_zero_num <-- {hypreal,hypnat,hcomplex}_zero_num |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
906 |
star_n_one_num <-- {hypreal,hypnat,hcomplex}_one_num |
17423 | 907 |
star_n_abs <-- hypreal_hrabs |
908 |
star_n_divide <-- hcomplex_divide |
|
909 |
||
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
910 |
star_of_add <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_add |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
911 |
star_of_minus <-- {hypreal_of_real,hcomplex_of_complex}_minus |
17423 | 912 |
star_of_diff <-- hypreal_of_real_diff |
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
913 |
star_of_mult <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_mult |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
914 |
star_of_one <-- {hypreal_of_real,hcomplex_of_complex}_one |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
915 |
star_of_zero <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_zero |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
916 |
star_of_le <-- {hypreal_of_real,hypnat_of_nat}_le_iff |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
917 |
star_of_less <-- {hypreal_of_real,hypnat_of_nat}_less_iff |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
918 |
star_of_eq <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_eq_iff |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
919 |
star_of_inverse <-- {hypreal_of_real,hcomplex_of_complex}_inverse |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
920 |
star_of_divide <-- {hypreal_of_real,hcomplex_of_complex}_divide |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
921 |
star_of_of_nat <-- {hypreal_of_real,hcomplex_of_complex}_of_nat |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
922 |
star_of_of_int <-- {hypreal_of_real,hcomplex_of_complex}_of_int |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
923 |
star_of_number_of <-- {hypreal,hcomplex}_number_of |
17423 | 924 |
star_of_number_less <-- number_of_less_hypreal_of_real_iff |
925 |
star_of_number_le <-- number_of_le_hypreal_of_real_iff |
|
926 |
star_of_eq_number <-- hypreal_of_real_eq_number_of_iff |
|
927 |
star_of_less_number <-- hypreal_of_real_less_number_of_iff |
|
928 |
star_of_le_number <-- hypreal_of_real_le_number_of_iff |
|
929 |
star_of_power <-- hypreal_of_real_power |
|
930 |
star_of_eq_0 <-- hcomplex_of_complex_zero_iff |
|
931 |
||
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
932 |
* Hyperreal: new method "transfer" that implements the transfer |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
933 |
principle of nonstandard analysis. With a subgoal that mentions |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
934 |
nonstandard types like "'a star", the command "apply transfer" |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
935 |
replaces it with an equivalent one that mentions only standard types. |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
936 |
To be successful, all free variables must have standard types; non- |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
937 |
standard variables must have explicit universal quantifiers. |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
938 |
|
17641 | 939 |
* Hyperreal: A theory of Taylor series. |
940 |
||
14655
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset
|
941 |
|
14682
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14655
diff
changeset
|
942 |
*** HOLCF *** |
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14655
diff
changeset
|
943 |
|
17533 | 944 |
* Discontinued special version of 'constdefs' (which used to support |
945 |
continuous functions) in favor of the general Pure one with full |
|
946 |
type-inference. |
|
947 |
||
948 |
* New simplification procedure for solving continuity conditions; it |
|
949 |
is much faster on terms with many nested lambda abstractions (cubic |
|
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
950 |
instead of exponential time). |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
951 |
|
17533 | 952 |
* New syntax for domain package: selector names are now optional. |
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
953 |
Parentheses should be omitted unless argument is lazy, for example: |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
954 |
|
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
955 |
domain 'a stream = cons "'a" (lazy "'a stream") |
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
956 |
|
17533 | 957 |
* New command 'fixrec' for defining recursive functions with pattern |
958 |
matching; defining multiple functions with mutual recursion is also |
|
959 |
supported. Patterns may include the constants cpair, spair, up, sinl, |
|
960 |
sinr, or any data constructor defined by the domain package. The given |
|
961 |
equations are proven as rewrite rules. See HOLCF/ex/Fixrec_ex.thy for |
|
962 |
syntax and examples. |
|
963 |
||
964 |
* New commands 'cpodef' and 'pcpodef' for defining predicate subtypes |
|
965 |
of cpo and pcpo types. Syntax is exactly like the 'typedef' command, |
|
966 |
but the proof obligation additionally includes an admissibility |
|
967 |
requirement. The packages generate instances of class cpo or pcpo, |
|
968 |
with continuity and strictness theorems for Rep and Abs. |
|
17442
c0f0b92c198c
add HOLCF entries for pcpodef, cont_proc, fixrec;
huffman
parents:
17436
diff
changeset
|
969 |
|
17584 | 970 |
* HOLCF: Many theorems have been renamed according to a more standard naming |
971 |
scheme (INCOMPATIBILITY): |
|
972 |
||
973 |
foo_inject: "foo$x = foo$y ==> x = y" |
|
974 |
foo_eq: "(foo$x = foo$y) = (x = y)" |
|
975 |
foo_less: "(foo$x << foo$y) = (x << y)" |
|
976 |
foo_strict: "foo$UU = UU" |
|
977 |
foo_defined: "... ==> foo$x ~= UU" |
|
978 |
foo_defined_iff: "(foo$x = UU) = (x = UU)" |
|
979 |
||
14682
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14655
diff
changeset
|
980 |
|
14885 | 981 |
*** ZF *** |
982 |
||
16234 | 983 |
* ZF/ex: theories Group and Ring provide examples in abstract algebra, |
984 |
including the First Isomorphism Theorem (on quotienting by the kernel |
|
985 |
of a homomorphism). |
|
15089
430264838064
ZF/Simplifier: second copy of context type solver;
wenzelm
parents:
15076
diff
changeset
|
986 |
|
430264838064
ZF/Simplifier: second copy of context type solver;
wenzelm
parents:
15076
diff
changeset
|
987 |
* ZF/Simplifier: install second copy of type solver that actually |
16234 | 988 |
makes use of TC rules declared to Isar proof contexts (or locales); |
989 |
the old version is still required for ML proof scripts. |
|
15703 | 990 |
|
991 |
||
17445 | 992 |
*** Cube *** |
993 |
||
994 |
* Converted to Isar theory format; use locales instead of axiomatic |
|
995 |
theories. |
|
996 |
||
997 |
||
15703 | 998 |
*** ML *** |
999 |
||
15973 | 1000 |
* Pure/library.ML no longer defines its own option datatype, but uses |
16234 | 1001 |
that of the SML basis, which has constructors NONE and SOME instead of |
1002 |
None and Some, as well as exception Option.Option instead of OPTION. |
|
1003 |
The functions the, if_none, is_some, is_none have been adapted |
|
1004 |
accordingly, while Option.map replaces apsome. |
|
15973 | 1005 |
|
16860
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1006 |
* Pure/library.ML: the exception LIST has been given up in favour of |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1007 |
the standard exceptions Empty and Subscript, as well as |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1008 |
Library.UnequalLengths. Function like Library.hd and Library.tl are |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1009 |
superceded by the standard hd and tl functions etc. |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1010 |
|
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1011 |
A number of basic list functions are no longer exported to the ML |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1012 |
toplevel, as they are variants of predefined functions. The following |
16234 | 1013 |
suggests how one can translate existing code: |
15973 | 1014 |
|
1015 |
rev_append xs ys = List.revAppend (xs, ys) |
|
1016 |
nth_elem (i, xs) = List.nth (xs, i) |
|
1017 |
last_elem xs = List.last xs |
|
1018 |
flat xss = List.concat xss |
|
16234 | 1019 |
seq fs = List.app fs |
15973 | 1020 |
partition P xs = List.partition P xs |
1021 |
mapfilter f xs = List.mapPartial f xs |
|
1022 |
||
16860
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1023 |
* Pure/library.ML: several combinators for linear functional |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1024 |
transformations, notably reverse application and composition: |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1025 |
|
17371 | 1026 |
x |> f f #> g |
1027 |
(x, y) |-> f f #-> g |
|
16860
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1028 |
|
17495 | 1029 |
* Pure/library.ML: introduced/changed precedence of infix operators: |
1030 |
||
1031 |
infix 1 |> |-> ||> ||>> |>> |>>> #> #->; |
|
1032 |
infix 2 ?; |
|
1033 |
infix 3 o oo ooo oooo; |
|
1034 |
infix 4 ~~ upto downto; |
|
1035 |
||
1036 |
Maybe INCOMPATIBILITY when any of those is used in conjunction with other |
|
1037 |
infix operators. |
|
1038 |
||
17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1039 |
* Pure/library.ML: natural list combinators fold, fold_rev, and |
16869 | 1040 |
fold_map support linear functional transformations and nesting. For |
16860
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1041 |
example: |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1042 |
|
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1043 |
fold f [x1, ..., xN] y = |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1044 |
y |> f x1 |> ... |> f xN |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1045 |
|
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1046 |
(fold o fold) f [xs1, ..., xsN] y = |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1047 |
y |> fold f xs1 |> ... |> fold f xsN |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1048 |
|
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1049 |
fold f [x1, ..., xN] = |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1050 |
f x1 #> ... #> f xN |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1051 |
|
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1052 |
(fold o fold) f [xs1, ..., xsN] = |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1053 |
fold f xs1 #> ... #> fold f xsN |
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset
|
1054 |
|
17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1055 |
* Pure/library.ML: the following selectors on type 'a option are |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1056 |
available: |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1057 |
|
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1058 |
the: 'a option -> 'a (*partial*) |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1059 |
these: 'a option -> 'a where 'a = 'b list |
17402 | 1060 |
the_default: 'a -> 'a option -> 'a |
1061 |
the_list: 'a option -> 'a list |
|
1062 |
||
17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1063 |
* Pure/General: structure AList (cf. Pure/General/alist.ML) provides |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1064 |
basic operations for association lists, following natural argument |
17564 | 1065 |
order; moreover the explicit equality predicate passed here avoids |
17495 | 1066 |
potentially expensive polymorphic runtime equality checks. |
1067 |
The old functions may be expressed as follows: |
|
17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1068 |
|
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1069 |
assoc = uncurry (AList.lookup (op =)) |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1070 |
assocs = these oo AList.lookup (op =) |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1071 |
overwrite = uncurry (AList.update (op =)) o swap |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1072 |
|
17564 | 1073 |
* Pure/General: structure AList (cf. Pure/General/alist.ML) provides |
1074 |
||
1075 |
val make: ('a -> 'b) -> 'a list -> ('a * 'b) list |
|
1076 |
val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list |
|
1077 |
||
1078 |
replacing make_keylist and keyfilter (occassionally used) |
|
1079 |
Naive rewrites: |
|
1080 |
||
1081 |
make_keylist = AList.make |
|
1082 |
keyfilter = AList.find (op =) |
|
1083 |
||
1084 |
* eq_fst and eq_snd now take explicit equality parameter, thus |
|
1085 |
avoiding eqtypes. Naive rewrites: |
|
1086 |
||
1087 |
eq_fst = eq_fst (op =) |
|
1088 |
eq_snd = eq_snd (op =) |
|
1089 |
||
1090 |
* Removed deprecated apl and apr (rarely used). |
|
1091 |
Naive rewrites: |
|
1092 |
||
1093 |
apl (n, op) =>>= curry op n |
|
1094 |
apr (op, m) =>>= fn n => op (n, m) |
|
1095 |
||
17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1096 |
* Pure/General: structure OrdList (cf. Pure/General/ord_list.ML) |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1097 |
provides a reasonably efficient light-weight implementation of sets as |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1098 |
lists. |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1099 |
|
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1100 |
* Pure/General: generic tables (cf. Pure/General/table.ML) provide a |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1101 |
few new operations; existing lookup and update are now curried to |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1102 |
follow natural argument order (for use with fold etc.); |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1103 |
INCOMPATIBILITY, use (uncurry Symtab.lookup) etc. as last resort. |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1104 |
|
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1105 |
* Pure/General: output via the Isabelle channels of |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1106 |
writeln/warning/error etc. is now passed through Output.output, with a |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1107 |
hook for arbitrary transformations depending on the print_mode |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1108 |
(cf. Output.add_mode -- the first active mode that provides a output |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1109 |
function wins). Already formatted output may be embedded into further |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1110 |
text via Output.raw; the result of Pretty.string_of/str_of and derived |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1111 |
functions (string_of_term/cterm/thm etc.) is already marked raw to |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1112 |
accommodate easy composition of diagnostic messages etc. Programmers |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1113 |
rarely need to care about Output.output or Output.raw at all, with |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1114 |
some notable exceptions: Output.output is required when bypassing the |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1115 |
standard channels (writeln etc.), or in token translations to produce |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1116 |
properly formatted results; Output.raw is required when capturing |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1117 |
already output material that will eventually be presented to the user |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1118 |
a second time. For the default print mode, both Output.output and |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1119 |
Output.raw have no effect. |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1120 |
|
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1121 |
* Pure/General: Output.time_accumulator NAME creates an operator ('a |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1122 |
-> 'b) -> 'a -> 'b to measure runtime and count invocations; the |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1123 |
cumulative results are displayed at the end of a batch session. |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1124 |
|
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1125 |
* Pure/General: File.sysify_path and File.quote_sysify path have been |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1126 |
replaced by File.platform_path and File.shell_path (with appropriate |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1127 |
hooks). This provides a clean interface for unusual systems where the |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1128 |
internal and external process view of file names are different. |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1129 |
|
16689
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset
|
1130 |
* Pure: more efficient orders for basic syntactic entities: added |
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset
|
1131 |
fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord |
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset
|
1132 |
and typ_ord to use fast_string_ord and fast_indexname_ord (term_ord is |
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset
|
1133 |
NOT affected); structures Symtab, Vartab, Typtab, Termtab use the fast |
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset
|
1134 |
orders now -- potential INCOMPATIBILITY for code that depends on a |
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset
|
1135 |
particular order for Symtab.keys, Symtab.dest, etc. (consider using |
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset
|
1136 |
Library.sort_strings on result). |
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset
|
1137 |
|
17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1138 |
* Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1139 |
fold_types traverse types/terms from left to right, observing natural |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1140 |
argument order. Supercedes previous foldl_XXX versions, add_frees, |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1141 |
add_vars etc. have been adapted as well: INCOMPATIBILITY. |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1142 |
|
16151 | 1143 |
* Pure: name spaces have been refined, with significant changes of the |
16234 | 1144 |
internal interfaces -- INCOMPATIBILITY. Renamed cond_extern(_table) |
1145 |
to extern(_table). The plain name entry path is superceded by a |
|
1146 |
general 'naming' context, which also includes the 'policy' to produce |
|
1147 |
a fully qualified name and external accesses of a fully qualified |
|
1148 |
name; NameSpace.extend is superceded by context dependent |
|
1149 |
Sign.declare_name. Several theory and proof context operations modify |
|
1150 |
the naming context. Especially note Theory.restore_naming and |
|
1151 |
ProofContext.restore_naming to get back to a sane state; note that |
|
1152 |
Theory.add_path is no longer sufficient to recover from |
|
1153 |
Theory.absolute_path in particular. |
|
1154 |
||
1155 |
* Pure: new flags short_names (default false) and unique_names |
|
1156 |
(default true) for controlling output of qualified names. If |
|
1157 |
short_names is set, names are printed unqualified. If unique_names is |
|
1158 |
reset, the name prefix is reduced to the minimum required to achieve |
|
1159 |
the original result when interning again, even if there is an overlap |
|
1160 |
with earlier declarations. |
|
16151 | 1161 |
|
16456
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1162 |
* Pure/TheoryDataFun: change of the argument structure; 'prep_ext' is |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1163 |
now 'extend', and 'merge' gets an additional Pretty.pp argument |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1164 |
(useful for printing error messages). INCOMPATIBILITY. |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1165 |
|
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1166 |
* Pure: major reorganization of the theory context. Type Sign.sg and |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1167 |
Theory.theory are now identified, referring to the universal |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1168 |
Context.theory (see Pure/context.ML). Actual signature and theory |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1169 |
content is managed as theory data. The old code and interfaces were |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1170 |
spread over many files and structures; the new arrangement introduces |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1171 |
considerable INCOMPATIBILITY to gain more clarity: |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1172 |
|
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1173 |
Context -- theory management operations (name, identity, inclusion, |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1174 |
parents, ancestors, merge, etc.), plus generic theory data; |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1175 |
|
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1176 |
Sign -- logical signature and syntax operations (declaring consts, |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1177 |
types, etc.), plus certify/read for common entities; |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1178 |
|
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1179 |
Theory -- logical theory operations (stating axioms, definitions, |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1180 |
oracles), plus a copy of logical signature operations (consts, |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1181 |
types, etc.); also a few basic management operations (Theory.copy, |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1182 |
Theory.merge, etc.) |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1183 |
|
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1184 |
The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1185 |
etc.) as well as the sign field in Thm.rep_thm etc. have been retained |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1186 |
for convenience -- they merely return the theory. |
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset
|
1187 |
|
17193
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset
|
1188 |
* Pure: type Type.tsig is superceded by theory in most interfaces. |
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset
|
1189 |
|
16547
09f7a953d2d6
* Pure: the Isar proof context type is already defined early in Pure
wenzelm
parents:
16506
diff
changeset
|
1190 |
* Pure: the Isar proof context type is already defined early in Pure |
09f7a953d2d6
* Pure: the Isar proof context type is already defined early in Pure
wenzelm
parents:
16506
diff
changeset
|
1191 |
as Context.proof (note that ProofContext.context and Proof.context are |
09f7a953d2d6
* Pure: the Isar proof context type is already defined early in Pure
wenzelm
parents:
16506
diff
changeset
|
1192 |
aliases, where the latter is the preferred name). This enables other |
09f7a953d2d6
* Pure: the Isar proof context type is already defined early in Pure
wenzelm
parents:
16506
diff
changeset
|
1193 |
Isabelle components to refer to that type even before Isar is present. |
09f7a953d2d6
* Pure: the Isar proof context type is already defined early in Pure
wenzelm
parents:
16506
diff
changeset
|
1194 |
|
16373
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1195 |
* Pure/sign/theory: discontinued named name spaces (i.e. classK, |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1196 |
typeK, constK, axiomK, oracleK), but provide explicit operations for |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1197 |
any of these kinds. For example, Sign.intern typeK is now |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1198 |
Sign.intern_type, Theory.hide_space Sign.typeK is now |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1199 |
Theory.hide_types. Also note that former |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1200 |
Theory.hide_classes/types/consts are now |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1201 |
Theory.hide_classes_i/types_i/consts_i, while the non '_i' versions |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1202 |
internalize their arguments! INCOMPATIBILITY. |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1203 |
|
16506
b2687ce38433
* Pure: get_thm interface expects datatype thmref;
wenzelm
parents:
16456
diff
changeset
|
1204 |
* Pure: get_thm interface (of PureThy and ProofContext) expects |
b2687ce38433
* Pure: get_thm interface expects datatype thmref;
wenzelm
parents:
16456
diff
changeset
|
1205 |
datatype thmref (with constructors Name and NameSelection) instead of |
b2687ce38433
* Pure: get_thm interface expects datatype thmref;
wenzelm
parents:
16456
diff
changeset
|
1206 |
plain string -- INCOMPATIBILITY; |
b2687ce38433
* Pure: get_thm interface expects datatype thmref;
wenzelm
parents:
16456
diff
changeset
|
1207 |
|
16151 | 1208 |
* Pure: cases produced by proof methods specify options, where NONE |
16234 | 1209 |
means to remove case bindings -- INCOMPATIBILITY in |
1210 |
(RAW_)METHOD_CASES. |
|
16151 | 1211 |
|
16373
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1212 |
* Pure: the following operations retrieve axioms or theorems from a |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1213 |
theory node or theory hierarchy, respectively: |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1214 |
|
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1215 |
Theory.axioms_of: theory -> (string * term) list |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1216 |
Theory.all_axioms_of: theory -> (string * term) list |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1217 |
PureThy.thms_of: theory -> (string * thm) list |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1218 |
PureThy.all_thms_of: theory -> (string * thm) list |
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset
|
1219 |
|
16718 | 1220 |
* Pure: print_tac now outputs the goal through the trace channel. |
1221 |
||
17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1222 |
* Isar toplevel: improved diagnostics, mostly for Poly/ML only. |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1223 |
Reference Toplevel.debug (default false) controls detailed printing |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1224 |
and tracing of low-level exceptions; Toplevel.profiling (default 0) |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1225 |
controls execution profiling -- set to 1 for time and 2 for space |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1226 |
(both increase the runtime). |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1227 |
|
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1228 |
* Isar session: The initial use of ROOT.ML is now always timed, |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1229 |
i.e. the log will show the actual process times, in contrast to the |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1230 |
elapsed wall-clock time that the outer shell wrapper produces. |
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1231 |
|
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset
|
1232 |
* Simplifier: improved handling of bound variables (nameless |
16997
7dfc99f62dd9
* Pure/Simplifier: improved handling of bound variables;
wenzelm
parents:
16962
diff
changeset
|
1233 |
representation, avoid allocating new strings). Simprocs that invoke |
7dfc99f62dd9
* Pure/Simplifier: improved handling of bound variables;
wenzelm
parents:
16962
diff
changeset
|
1234 |
the Simplifier recursively should use Simplifier.inherit_bounds to |
17720 | 1235 |
avoid local name clashes. Failure to do so produces warnings |
1236 |
"Simplifier: renamed bound variable ..."; set Simplifier.debug_bounds |
|
1237 |
for further details. |
|
16234 | 1238 |
|
17166 | 1239 |
* ML functions legacy_bindings and use_legacy_bindings produce ML fact |
1240 |
bindings for all theorems stored within a given theory; this may help |
|
1241 |
in porting non-Isar theories to Isar ones, while keeping ML proof |
|
1242 |
scripts for the time being. |
|
1243 |
||
17457 | 1244 |
* ML operator HTML.with_charset specifies the charset begin used for |
1245 |
generated HTML files. For example: |
|
1246 |
||
1247 |
HTML.with_charset "utf-8" use_thy "Hebrew"; |
|
17538 | 1248 |
HTML.with_charset "utf-8" use_thy "Chinese"; |
17457 | 1249 |
|
16234 | 1250 |
|
1251 |
*** System *** |
|
1252 |
||
1253 |
* Allow symlinks to all proper Isabelle executables (Isabelle, |
|
1254 |
isabelle, isatool etc.). |
|
1255 |
||
1256 |
* ISABELLE_DOC_FORMAT setting specifies preferred document format (for |
|
1257 |
isatool doc, isatool mkdir, display_drafts etc.). |
|
1258 |
||
1259 |
* isatool usedir: option -f allows specification of the ML file to be |
|
1260 |
used by Isabelle; default is ROOT.ML. |
|
1261 |
||
16251
121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset
|
1262 |
* New isatool version outputs the version identifier of the Isabelle |
121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset
|
1263 |
distribution being used. |
121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset
|
1264 |
|
121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset
|
1265 |
* HOL: new isatool dimacs2hol converts files in DIMACS CNF format |
16234 | 1266 |
(containing Boolean satisfiability problems) into Isabelle/HOL |
1267 |
theories. |
|
15703 | 1268 |
|
1269 |
||
14655
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset
|
1270 |
|
14606 | 1271 |
New in Isabelle2004 (April 2004) |
1272 |
-------------------------------- |
|
13280
306ef3aef61b
* improved thms_containing: proper indexing of facts instead of raw
wenzelm
parents:
13190
diff
changeset
|
1273 |
|
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
14136
diff
changeset
|
1274 |
*** General *** |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
14136
diff
changeset
|
1275 |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1276 |
* Provers/order.ML: new efficient reasoner for partial and linear orders. |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1277 |
Replaces linorder.ML. |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1278 |
|
14606 | 1279 |
* Pure: Greek letters (except small lambda, \<lambda>), as well as Gothic |
1280 |
(\<aa>...\<zz>\<AA>...\<ZZ>), calligraphic (\<A>...\<Z>), and Euler |
|
14173 | 1281 |
(\<a>...\<z>), are now considered normal letters, and can therefore |
1282 |
be used anywhere where an ASCII letter (a...zA...Z) has until |
|
1283 |
now. COMPATIBILITY: This obviously changes the parsing of some |
|
1284 |
terms, especially where a symbol has been used as a binder, say |
|
1285 |
'\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed |
|
1286 |
as an identifier. Fix it by inserting a space around former |
|
1287 |
symbols. Call 'isatool fixgreek' to try to fix parsing errors in |
|
1288 |
existing theory and ML files. |
|
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
14136
diff
changeset
|
1289 |
|
14237 | 1290 |
* Pure: Macintosh and Windows line-breaks are now allowed in theory files. |
1291 |
||
14731 | 1292 |
* Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now |
1293 |
allowed in identifiers. Similar to Greek letters \<^isub> is now considered |
|
1294 |
a normal (but invisible) letter. For multiple letter subscripts repeat |
|
1295 |
\<^isub> like this: x\<^isub>1\<^isub>2. |
|
14233 | 1296 |
|
14333 | 1297 |
* Pure: There are now sub-/superscripts that can span more than one |
1298 |
character. Text between \<^bsub> and \<^esub> is set in subscript in |
|
14606 | 1299 |
ProofGeneral and LaTeX, text between \<^bsup> and \<^esup> in |
1300 |
superscript. The new control characters are not identifier parts. |
|
14333 | 1301 |
|
14561
c53396af770e
* raw control symbols are of the form \<^raw:...> now.
schirmer
parents:
14556
diff
changeset
|
1302 |
* Pure: Control-symbols of the form \<^raw:...> will literally print the |
14606 | 1303 |
content of "..." to the latex file instead of \isacntrl... . The "..." |
1304 |
may consist of any printable characters excluding the end bracket >. |
|
14361
ad2f5da643b4
* Support for raw latex output in control symbols: \<^raw...>
schirmer
parents:
14333
diff
changeset
|
1305 |
|
14237 | 1306 |
* Pure: Using new Isar command "finalconsts" (or the ML functions |
1307 |
Theory.add_finals or Theory.add_finals_i) it is now possible to |
|
1308 |
declare constants "final", which prevents their being given a definition |
|
1309 |
later. It is useful for constants whose behaviour is fixed axiomatically |
|
14224 | 1310 |
rather than definitionally, such as the meta-logic connectives. |
1311 |
||
14606 | 1312 |
* Pure: 'instance' now handles general arities with general sorts |
1313 |
(i.e. intersections of classes), |
|
14503
255ad604e08e
Added check that Theory.ML does not occur in the files section of the theory
skalberg
parents:
14480
diff
changeset
|
1314 |
|
14547 | 1315 |
* Presentation: generated HTML now uses a CSS style sheet to make layout |
14731 | 1316 |
(somewhat) independent of content. It is copied from lib/html/isabelle.css. |
14547 | 1317 |
It can be changed to alter the colors/layout of generated pages. |
1318 |
||
14556
c5078f6c99a9
* Calculation commands "moreover" and "also" no longer interfere with
wenzelm
parents:
14551
diff
changeset
|
1319 |
|
14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset
|
1320 |
*** Isar *** |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset
|
1321 |
|
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14503
diff
changeset
|
1322 |
* Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac, |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14503
diff
changeset
|
1323 |
cut_tac, subgoal_tac and thin_tac: |
14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset
|
1324 |
- Now understand static (Isar) contexts. As a consequence, users of Isar |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset
|
1325 |
locales are no longer forced to write Isar proof scripts. |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset
|
1326 |
For details see Isar Reference Manual, paragraph 4.3.2: Further tactic |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset
|
1327 |
emulations. |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset
|
1328 |
- INCOMPATIBILITY: names of variables to be instantiated may no |
14211
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset
|
1329 |
longer be enclosed in quotes. Instead, precede variable name with `?'. |
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset
|
1330 |
This is consistent with the instantiation attribute "where". |
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset
|
1331 |
|
14257
a7ef3f7588c5
Type inference bug in Isar attributes "where" and "of" fixed.
ballarin
parents:
14255
diff
changeset
|
1332 |
* Attributes "where" and "of": |
14285
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14283
diff
changeset
|
1333 |
- Now take type variables of instantiated theorem into account when reading |
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14283
diff
changeset
|
1334 |
the instantiation string. This fixes a bug that caused instantiated |
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14283
diff
changeset
|
1335 |
theorems to have too special types in some circumstances. |
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14283
diff
changeset
|
1336 |
- "where" permits explicit instantiations of type variables. |
14257
a7ef3f7588c5
Type inference bug in Isar attributes "where" and "of" fixed.
ballarin
parents:
14255
diff
changeset
|
1337 |
|
14556
c5078f6c99a9
* Calculation commands "moreover" and "also" no longer interfere with
wenzelm
parents:
14551
diff
changeset
|
1338 |
* Calculation commands "moreover" and "also" no longer interfere with |
c5078f6c99a9
* Calculation commands "moreover" and "also" no longer interfere with
wenzelm
parents:
14551
diff
changeset
|
1339 |
current facts ("this"), admitting arbitrary combinations with "then" |
c5078f6c99a9
* Calculation commands "moreover" and "also" no longer interfere with
wenzelm
parents:
14551
diff
changeset
|
1340 |
and derived forms. |
14283 | 1341 |
|
14211
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset
|
1342 |
* Locales: |
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset
|
1343 |
- Goal statements involving the context element "includes" no longer |
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset
|
1344 |
generate theorems with internal delta predicates (those ending on |
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset
|
1345 |
"_axioms") in the premise. |
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset
|
1346 |
Resolve particular premise with <locale>.intro to obtain old form. |
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset
|
1347 |
- Fixed bug in type inference ("unify_frozen") that prevented mix of target |
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset
|
1348 |
specification and "includes" elements in goal statement. |
14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
14243
diff
changeset
|
1349 |
- Rule sets <locale>.intro and <locale>.axioms no longer declared as |
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
14243
diff
changeset
|
1350 |
[intro?] and [elim?] (respectively) by default. |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14503
diff
changeset
|
1351 |
- Experimental command for instantiation of locales in proof contexts: |
14551 | 1352 |
instantiate <label>[<attrs>]: <loc> |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14503
diff
changeset
|
1353 |
Instantiates locale <loc> and adds all its theorems to the current context |
14551 | 1354 |
taking into account their attributes. Label and attrs are optional |
1355 |
modifiers, like in theorem declarations. If present, names of |
|
1356 |
instantiated theorems are qualified with <label>, and the attributes |
|
1357 |
<attrs> are applied after any attributes these theorems might have already. |
|
1358 |
If the locale has assumptions, a chained fact of the form |
|
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14503
diff
changeset
|
1359 |
"<loc> t1 ... tn" is expected from which instantiations of the parameters |
14551 | 1360 |
are derived. The command does not support old-style locales declared |
1361 |
with "locale (open)". |
|
1362 |
A few (very simple) examples can be found in FOL/ex/LocaleInst.thy. |
|
14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset
|
1363 |
|
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset
|
1364 |
* HOL: Tactic emulation methods induct_tac and case_tac understand static |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset
|
1365 |
(Isar) contexts. |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset
|
1366 |
|
14556
c5078f6c99a9
* Calculation commands "moreover" and "also" no longer interfere with
wenzelm
parents:
14551
diff
changeset
|
1367 |
|
14136 | 1368 |
*** HOL *** |
1369 |
||
14624 | 1370 |
* Proof import: new image HOL4 contains the imported library from |
1371 |
the HOL4 system with about 2500 theorems. It is imported by |
|
1372 |
replaying proof terms produced by HOL4 in Isabelle. The HOL4 image |
|
1373 |
can be used like any other Isabelle image. See |
|
1374 |
HOL/Import/HOL/README for more information. |
|
1375 |
||
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1376 |
* Simplifier: |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1377 |
- Much improved handling of linear and partial orders. |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1378 |
Reasoners for linear and partial orders are set up for type classes |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1379 |
"linorder" and "order" respectively, and are added to the default simpset |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1380 |
as solvers. This means that the simplifier can build transitivity chains |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1381 |
to solve goals from the assumptions. |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1382 |
- INCOMPATIBILITY: old proofs break occasionally. Typically, applications |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1383 |
of blast or auto after simplification become unnecessary because the goal |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1384 |
is solved by simplification already. |
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset
|
1385 |
|
14731 | 1386 |
* Numerics: new theory Ring_and_Field contains over 250 basic numerical laws, |
14389 | 1387 |
all proved in axiomatic type classes for semirings, rings and fields. |
1388 |
||
1389 |
* Numerics: |
|
1390 |
- Numeric types (nat, int, and in HOL-Complex rat, real, complex, etc.) are |
|
14731 | 1391 |
now formalized using the Ring_and_Field theory mentioned above. |
14389 | 1392 |
- INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently |
1393 |
than before, because now they are set up once in a generic manner. |
|
14731 | 1394 |
- INCOMPATIBILITY: many type-specific arithmetic laws have gone. |
14480 | 1395 |
Look for the general versions in Ring_and_Field (and Power if they concern |
1396 |
exponentiation). |
|
14389 | 1397 |
|
14401 | 1398 |
* Type "rat" of the rational numbers is now available in HOL-Complex. |
14389 | 1399 |
|
14255 | 1400 |
* Records: |
1401 |
- Record types are now by default printed with their type abbreviation |
|
1402 |
instead of the list of all field types. This can be configured via |
|
1403 |
the reference "print_record_type_abbr". |
|
14731 | 1404 |
- Simproc "record_upd_simproc" for simplification of multiple updates added |
14255 | 1405 |
(not enabled by default). |
14427 | 1406 |
- Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp. |
1407 |
EX x. x = sel r to True (not enabled by default). |
|
14255 | 1408 |
- Tactic "record_split_simp_tac" to split and simplify records added. |
14731 | 1409 |
|
14136 | 1410 |
* 'specification' command added, allowing for definition by |