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