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