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