author | urbanc |
Thu, 13 Sep 2007 23:58:38 +0200 | |
changeset 24571 | a6d0428dea8e |
parent 24507 | ac22a2a67100 |
child 24606 | 7acbb982fc77 |
permissions | -rw-r--r-- |
5363 | 1 |
Isabelle NEWS -- history user-relevant changes |
2 |
============================================== |
|
2553 | 3 |
|
20807 | 4 |
New in this Isabelle version |
17754
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 |
|
22826 | 9 |
* More uniform information about legacy features, notably a |
10 |
warning/error of "Legacy feature: ...", depending on the state of the |
|
23367 | 11 |
tolerate_legacy_features flag (default true). FUTURE INCOMPATIBILITY: |
12 |
legacy features will disappear eventually. |
|
22826 | 13 |
|
17918
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
14 |
* 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
|
15 |
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
|
16 |
fixheaders to convert existing theory files. INCOMPATIBILITY. |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
17 |
|
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
18 |
* 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
|
19 |
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
|
20 |
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
|
21 |
function use_legacy_bindings. INCOMPATIBILITY. |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
22 |
|
22871 | 23 |
* Theory syntax: some popular names (e.g. 'class', 'declaration', |
24 |
'fun', 'help', 'if') are now keywords. INCOMPATIBILITY, use double |
|
25 |
quotes. |
|
19814
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
26 |
|
23888
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
27 |
* Theory loader: be more serious about observing the static theory |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
28 |
header specifications (including optional directories), but not the |
24172
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
29 |
accidental file locations of previously successful loads. The strict |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
30 |
update policy of former update_thy is now already performed by |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
31 |
use_thy, so the former has been removed; use_thys updates several |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
32 |
theories simultaneously, just as 'imports' within a theory header |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
33 |
specification, but without merging the results. Potential |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
34 |
INCOMPATIBILITY: may need to refine theory headers and commands |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
35 |
ROOT.ML which depend on load order. |
23888
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
36 |
|
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
37 |
* Theory loader: optional support for content-based file |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
38 |
identification, instead of the traditional scheme of full physical |
23889 | 39 |
path plus date stamp; configured by the ISABELLE_FILE_IDENT setting |
23888
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
40 |
(cf. the system manual). The new scheme allows to work with |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
41 |
non-finished theories in persistent session images, such that source |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
42 |
files may be moved later on without requiring reloads. |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
43 |
|
24187
8bdf5ca5871f
* Theory loader: old-style ML proof scripts are considered a legacy feature;
wenzelm
parents:
24172
diff
changeset
|
44 |
* Theory loader: old-style ML proof scripts being *attached* to a thy |
8bdf5ca5871f
* Theory loader: old-style ML proof scripts are considered a legacy feature;
wenzelm
parents:
24172
diff
changeset
|
45 |
file (with the same base name as the theory) are considered a legacy |
8bdf5ca5871f
* Theory loader: old-style ML proof scripts are considered a legacy feature;
wenzelm
parents:
24172
diff
changeset
|
46 |
feature, which will disappear eventually. Even now, the theory loader no |
8bdf5ca5871f
* Theory loader: old-style ML proof scripts are considered a legacy feature;
wenzelm
parents:
24172
diff
changeset
|
47 |
longer maintains dependencies on such files. |
8bdf5ca5871f
* Theory loader: old-style ML proof scripts are considered a legacy feature;
wenzelm
parents:
24172
diff
changeset
|
48 |
|
24234
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
49 |
* Syntax: the scope for resolving ambiguities via type-inference is now |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
50 |
limited to individual terms, instead of whole simultaneous |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
51 |
specifications as before. This greatly reduces the complexity of the |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
52 |
syntax module and improves flexibility by separating parsing and |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
53 |
type-checking. INCOMPATIBILITY: additional type-constraints (explicit |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
54 |
'fixes' etc.) are required in rare situations. |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
55 |
|
17981
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
56 |
* 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
|
57 |
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
|
58 |
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
|
59 |
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
|
60 |
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
|
61 |
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
|
62 |
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
|
63 |
|
23379
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
64 |
* Command 'find_theorems': supports "*" wild-card in "name:" |
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
65 |
criterion; "with_dups" option. Certain ProofGeneral versions might |
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
66 |
support a specific search form (see ProofGeneral/CHANGES). |
22965 | 67 |
|
20370 | 68 |
* The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1 |
69 |
by default, which means that "prems" (and also "fixed variables") are |
|
70 |
suppressed from proof state output. Note that the ProofGeneral |
|
71 |
settings mechanism allows to change and save options persistently, but |
|
72 |
older versions of Isabelle will fail to start up if a negative prems |
|
73 |
limit is imposed. |
|
74 |
||
21308
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
75 |
* Local theory targets may be specified by non-nested blocks of |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
76 |
``context/locale/class ... begin'' followed by ``end''. The body may |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
77 |
contain definitions, theorems etc., including any derived mechanism |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
78 |
that has been implemented on top of these primitives. This concept |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
79 |
generalizes the existing ``theorem (in ...)'' towards more versatility |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
80 |
and scalability. |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
81 |
|
21960
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
82 |
* Proof General interface: proper undo of final 'end' command; |
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
83 |
discontinued Isabelle/classic mode (ML proof scripts). |
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
84 |
|
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
85 |
|
17865 | 86 |
*** Document preparation *** |
87 |
||
21717 | 88 |
* Added antiquotation @{theory name} which prints the given name, |
89 |
after checking that it refers to a valid ancestor theory in the |
|
90 |
current context. |
|
21339 | 91 |
|
17869 | 92 |
* Added antiquotations @{ML_type text} and @{ML_struct text} which |
93 |
check the given source text as ML type/structure, printing verbatim. |
|
17865 | 94 |
|
21717 | 95 |
* Added antiquotation @{abbrev "c args"} which prints the abbreviation |
96 |
"c args == rhs" given in the current context. (Any number of |
|
21735 | 97 |
arguments may be given on the LHS.) |
21717 | 98 |
|
99 |
||
17865 | 100 |
|
17779 | 101 |
*** Pure *** |
102 |
||
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22871
diff
changeset
|
103 |
* code generator: consts in 'consts_code' Isar commands are now referred |
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22871
diff
changeset
|
104 |
to by usual term syntax (including optional type annotations). |
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22871
diff
changeset
|
105 |
|
22735 | 106 |
* code generator: |
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22871
diff
changeset
|
107 |
- Isar 'definition's, 'constdef's and primitive instance definitions are added |
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22871
diff
changeset
|
108 |
explicitly to the table of defining equations |
22754 | 109 |
- primitive definitions are not used as defining equations by default any longer |
22735 | 110 |
- defining equations are now definitly restricted to meta "==" and object |
111 |
equality "=" |
|
112 |
- HOL theories have been adopted accordingly |
|
113 |
||
20807 | 114 |
* class_package.ML offers a combination of axclasses and locales to |
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22871
diff
changeset
|
115 |
achieve Haskell-like type classes in Isabelle. See |
20807 | 116 |
HOL/ex/Classpackage.thy for examples. |
117 |
||
118 |
* Yet another code generator framework allows to generate executable |
|
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22871
diff
changeset
|
119 |
code for ML and Haskell (including "class"es). A short usage sketch: |
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
120 |
|
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
121 |
internal compilation: |
23850 | 122 |
code_gen <list of constants (term syntax)> in SML |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
123 |
writing SML code to a file: |
23850 | 124 |
code_gen <list of constants (term syntax)> in SML <filename> |
22735 | 125 |
writing OCaml code to a file: |
23850 | 126 |
code_gen <list of constants (term syntax)> in OCaml <filename> |
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
127 |
writing Haskell code to a bunch of files: |
23850 | 128 |
code_gen <list of constants (term syntax)> in Haskell <filename> |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
129 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
130 |
Reasonable default setup of framework in HOL/Main. |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
131 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
132 |
Theorem attributs for selecting and transforming function equations theorems: |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
133 |
|
22845 | 134 |
[code fun]: select a theorem as function equation for a specific constant |
135 |
[code fun del]: deselect a theorem as function equation for a specific constant |
|
136 |
[code inline]: select an equation theorem for unfolding (inlining) in place |
|
137 |
[code inline del]: deselect an equation theorem for unfolding (inlining) in place |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
138 |
|
22735 | 139 |
User-defined serializations (target in {SML, OCaml, Haskell}): |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
140 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
141 |
code_const <and-list of constants (term syntax)> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
142 |
{(target) <and-list of const target syntax>}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
143 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
144 |
code_type <and-list of type constructors> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
145 |
{(target) <and-list of type target syntax>}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
146 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
147 |
code_instance <and-list of instances> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
148 |
{(target)}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
149 |
where instance ::= <type constructor> :: <class> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
150 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
151 |
code_class <and_list of classes> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
152 |
{(target) <and-list of class target syntax>}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
153 |
where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}? |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
154 |
|
22735 | 155 |
code_instance and code_class only apply to target Haskell. |
156 |
||
157 |
See HOL theories and HOL/ex/Codegenerator*.thy for usage examples. |
|
158 |
Doc/Isar/Advanced/Codegen/ provides a tutorial. |
|
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
159 |
|
19254 | 160 |
* Command 'no_translations' removes translation rules from theory |
161 |
syntax. |
|
162 |
||
19625
285771cec083
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
wenzelm
parents:
19587
diff
changeset
|
163 |
* Overloaded definitions are now actually checked for acyclic |
19714 | 164 |
dependencies. The overloading scheme is slightly more general than |
165 |
that of Haskell98, although Isabelle does not demand an exact |
|
166 |
correspondence to type class and instance declarations. |
|
167 |
INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more |
|
168 |
exotic versions of overloading -- at the discretion of the user! |
|
19711 | 169 |
|
170 |
Polymorphic constants are represented via type arguments, i.e. the |
|
171 |
instantiation that matches an instance against the most general |
|
172 |
declaration given in the signature. For example, with the declaration |
|
173 |
c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented |
|
174 |
as c(nat). Overloading is essentially simultaneous structural |
|
175 |
recursion over such type arguments. Incomplete specification patterns |
|
19714 | 176 |
impose global constraints on all occurrences, e.g. c('a * 'a) on the |
19715 | 177 |
LHS means that more general c('a * 'b) will be disallowed on any RHS. |
19714 | 178 |
Command 'print_theory' outputs the normalized system of recursive |
179 |
equations, see section "definitions". |
|
19625
285771cec083
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
wenzelm
parents:
19587
diff
changeset
|
180 |
|
24086 | 181 |
* Configuration options are maintained within the theory or proof |
182 |
context (with name and type bool/int/string), providing a very simple |
|
183 |
interface to a poor-man's version of general context data. Tools may |
|
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
184 |
declare options in ML (e.g. using Attrib.config_int) and then refer to |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
185 |
these values using Config.get etc. Users may change options via an |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
186 |
associated attribute of the same name. This form of context |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
187 |
declaration works particularly well with commands 'declare' or |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
188 |
'using', for example ``declare [[foo = 42]]''. Thus it has become |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
189 |
very easy to avoid global references, which would not observe Isar |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
190 |
toplevel undo/redo and fail to work with multithreading. |
24086 | 191 |
|
24172
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
192 |
Various global ML references of Pure and HOL have been turned into |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
193 |
configuration options: |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
194 |
|
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
195 |
Unify.search_bound unify_search_bound |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
196 |
Unify.trace_bound unify_trace_bound |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
197 |
Unify.trace_simp unify_trace_simp |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
198 |
Unify.trace_types unify_trace_types |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
199 |
Simplifier.simp_depth_limit simp_depth_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
200 |
Blast.depth_limit blast_depth_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
201 |
DatatypeProp.dtK datatype_distinctness_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
202 |
fast_arith_neq_limit fast_arith_neq_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
203 |
fast_arith_split_limit fast_arith_split_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
204 |
|
24086 | 205 |
* Named collections of theorems may be easily installed as context |
206 |
data using the functor NamedThmsFun (see |
|
207 |
src/Pure/Tools/named_thms.ML). The user may add or delete facts via |
|
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
208 |
attributes; there is also a toplevel print command. This facility is |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
209 |
just a common case of general context data, which is the preferred way |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
210 |
for anything more complex than just a list of facts in canonical |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
211 |
order. |
24086 | 212 |
|
24032 | 213 |
* Isar: command 'declaration' augments a local theory by generic |
214 |
declaration functions written in ML. This enables arbitrary content |
|
215 |
being added to the context, depending on a morphism that tells the |
|
216 |
difference of the original declaration context wrt. the application |
|
217 |
context encountered later on. |
|
218 |
||
219 |
* Isar: proper interfaces for simplification procedures. Command |
|
220 |
'simproc_setup' declares named simprocs (with match patterns, and body |
|
221 |
text in ML). Attribute "simproc" adds/deletes simprocs in the current |
|
222 |
context. ML antiquotation @{simproc name} retrieves named simprocs. |
|
223 |
||
224 |
* Isar: an extra pair of brackets around attribute declarations |
|
225 |
abbreviates a theorem reference involving an internal dummy fact, |
|
226 |
which will be ignored later --- only the effect of the attribute on |
|
227 |
the background context will persist. This form of in-place |
|
228 |
declarations is particularly useful with commands like 'declare' and |
|
229 |
'using', for example ``have A using [[simproc a]] by simp''. |
|
230 |
||
23369
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
231 |
* Isar: method "assumption" (and implicit closing of subproofs) now |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
232 |
takes simple non-atomic goal assumptions into account: after applying |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
233 |
an assumption as a rule the resulting subgoals are solved by atomic |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
234 |
assumption steps. This is particularly useful to finish 'obtain' |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
235 |
goals, such as "!!x. (!!x. P x ==> thesis) ==> P x ==> thesis", |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
236 |
without referring to the original premise "!!x. P x ==> thesis" in the |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
237 |
Isar proof context. POTENTIAL INCOMPATIBILITY: method "assumption" is |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
238 |
more permissive. |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
239 |
|
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
240 |
* Isar: implicit use of prems from the Isar proof context is |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
241 |
considered a legacy feature. Common applications like ``have A .'' |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
242 |
may be replaced by ``have A by fact'' or ``note `A`''. In general, |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
243 |
referencing facts explicitly here improves readability and |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
244 |
maintainability of proof texts. |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
245 |
|
17865 | 246 |
* Isar: improper proof element 'guess' is like 'obtain', but derives |
247 |
the obtained context from the course of reasoning! For example: |
|
248 |
||
249 |
assume "EX x y. A x & B y" -- "any previous fact" |
|
250 |
then guess x and y by clarify |
|
251 |
||
252 |
This technique is potentially adventurous, depending on the facts and |
|
253 |
proof tools being involved here. |
|
254 |
||
18020 | 255 |
* Isar: known facts from the proof context may be specified as literal |
256 |
propositions, using ASCII back-quote syntax. This works wherever |
|
257 |
named facts used to be allowed so far, in proof commands, proof |
|
258 |
methods, attributes etc. Literal facts are retrieved from the context |
|
259 |
according to unification of type and term parameters. For example, |
|
260 |
provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known |
|
261 |
theorems in the current context, then these are valid literal facts: |
|
262 |
`A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc. |
|
263 |
||
264 |
There is also a proof method "fact" which does the same composition |
|
18044 | 265 |
for explicit goal states, e.g. the following proof texts coincide with |
266 |
certain special cases of literal facts: |
|
18020 | 267 |
|
268 |
have "A" by fact == note `A` |
|
269 |
have "A ==> B" by fact == note `A ==> B` |
|
270 |
have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` |
|
271 |
have "P a ==> Q a" by fact == note `P a ==> Q a` |
|
272 |
||
20118
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
273 |
* 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
|
274 |
outer syntax. Thus symbolic identifiers may be used without |
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
275 |
additional white space in declarations like this: ``assume *: A''. |
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
276 |
|
20013 | 277 |
* Isar: 'print_facts' prints all local facts of the current context, |
278 |
both named and unnamed ones. |
|
279 |
||
18308 | 280 |
* Isar: 'def' now admits simultaneous definitions, e.g.: |
281 |
||
282 |
def x == "t" and y == "u" |
|
283 |
||
18540 | 284 |
* Isar: added command 'unfolding', which is structurally similar to |
285 |
'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
|
286 |
rewrite rules. Thus many occurrences of the 'unfold' method or |
18540 | 287 |
'unfolded' attribute may be replaced by first-class proof text. |
288 |
||
18815
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
289 |
* Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded', |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
290 |
and command 'unfolding' now all support object-level equalities |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
291 |
(potentially conditional). The underlying notion of rewrite rule is |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
292 |
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
|
293 |
Simplifier (which is usually more generous). |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
294 |
|
24238 | 295 |
* Isar: the new attribute [rotated n] (default n = 1) rotates the |
296 |
premises of a theorem by n. Useful in conjunction with drule. |
|
297 |
||
19220 | 298 |
* Isar: the goal restriction operator [N] (default N = 1) evaluates a |
299 |
method expression within a sandbox consisting of the first N |
|
19240 | 300 |
sub-goals, which need to exist. For example, ``simp_all [3]'' |
301 |
simplifies the first three sub-goals, while (rule foo, simp_all)[] |
|
302 |
simplifies all new goals that emerge from applying rule foo to the |
|
303 |
originally first one. |
|
19220 | 304 |
|
19814
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
305 |
* 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
|
306 |
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
|
307 |
expected. |
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
308 |
|
18901 | 309 |
* Isar: the conclusion of a long theorem statement is now either |
310 |
'shows' (a simultaneous conjunction, as before), or 'obtains' |
|
311 |
(essentially a disjunction of cases with local parameters and |
|
312 |
assumptions). The latter allows to express general elimination rules |
|
18910 | 313 |
adequately; in this notation common elimination rules look like this: |
18901 | 314 |
|
315 |
lemma exE: -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis" |
|
316 |
assumes "EX x. P x" |
|
317 |
obtains x where "P x" |
|
318 |
||
319 |
lemma conjE: -- "A & B ==> (A ==> B ==> thesis) ==> thesis" |
|
320 |
assumes "A & B" |
|
321 |
obtains A and B |
|
322 |
||
323 |
lemma disjE: -- "A | B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis" |
|
324 |
assumes "A | B" |
|
325 |
obtains |
|
326 |
A |
|
327 |
| B |
|
328 |
||
18910 | 329 |
The subsequent classical rules even refer to the formal "thesis" |
18901 | 330 |
explicitly: |
331 |
||
332 |
lemma classical: -- "(~ thesis ==> thesis) ==> thesis" |
|
333 |
obtains "~ thesis" |
|
334 |
||
18910 | 335 |
lemma Peirce's_Law: -- "((thesis ==> something) ==> thesis) ==> thesis" |
336 |
obtains "thesis ==> something" |
|
18901 | 337 |
|
338 |
The actual proof of an 'obtains' statement is analogous to that of the |
|
18910 | 339 |
Isar proof element 'obtain', only that there may be several cases. |
340 |
Optional case names may be specified in parentheses; these will be |
|
341 |
available both in the present proof and as annotations in the |
|
342 |
resulting rule, for later use with the 'cases' method (cf. attribute |
|
343 |
case_names). |
|
18901 | 344 |
|
21447
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
345 |
* Isar: the assumptions of a long theorem statement are available as |
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
346 |
"assms" fact in the proof context. This is more appropriate than the |
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
347 |
(historical) "prems", which refers to all assumptions of the current |
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
348 |
context, including those from the target locale, proof body etc. |
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
349 |
|
19263 | 350 |
* Isar: 'print_statement' prints theorems from the current theory or |
351 |
proof context in long statement form, according to the syntax of a |
|
352 |
top-level lemma. |
|
353 |
||
18901 | 354 |
* Isar: 'obtain' takes an optional case name for the local context |
355 |
introduction rule (default "that"). |
|
356 |
||
19587 | 357 |
* Isar: removed obsolete 'concl is' patterns. INCOMPATIBILITY, use |
358 |
explicit (is "_ ==> ?foo") in the rare cases where this still happens |
|
359 |
to occur. |
|
360 |
||
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
361 |
* Pure: syntax "CONST name" produces a fully internalized constant |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
362 |
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
|
363 |
syntax translations that should refer to internal constant |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
364 |
representations independently of name spaces. |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
365 |
|
21537
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
366 |
* Pure: syntax constant for foo (binder "FOO ") is called "foo_binder" |
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
367 |
instead of "FOO ". This allows multiple binder declarations to coexist |
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
368 |
in the same context. INCOMPATIBILITY. |
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
369 |
|
21209
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset
|
370 |
* Isar/locales: 'notation' provides a robust interface to the 'syntax' |
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset
|
371 |
primitive that also works in a locale context (both for constants and |
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset
|
372 |
fixed variables). Type declaration and internal syntactic |
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset
|
373 |
representation of given constants retrieved from the context. |
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
374 |
|
19665 | 375 |
* Isar/locales: new derived specification elements 'axiomatization', |
376 |
'definition', 'abbreviation', which support type-inference, admit |
|
19083 | 377 |
object-level specifications (equality, equivalence). See also the |
378 |
isar-ref manual. Examples: |
|
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset
|
379 |
|
19665 | 380 |
axiomatization |
21595 | 381 |
eq (infix "===" 50) where |
382 |
eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y" |
|
383 |
||
384 |
definition "f x y = x + y + 1" |
|
385 |
definition g where "g x = f x x" |
|
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset
|
386 |
|
19363 | 387 |
abbreviation |
21595 | 388 |
neq (infix "=!=" 50) where |
19363 | 389 |
"x =!= y == ~ (x === y)" |
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset
|
390 |
|
19083 | 391 |
These specifications may be also used in a locale context. Then the |
392 |
constants being introduced depend on certain fixed parameters, and the |
|
393 |
constant name is qualified by the locale base name. An internal |
|
394 |
abbreviation takes care for convenient input and output, making the |
|
19088 | 395 |
parameters implicit and using the original short name. See also |
19083 | 396 |
HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic |
397 |
entities from a monomorphic theory. |
|
398 |
||
399 |
Presently, abbreviations are only available 'in' a target locale, but |
|
19363 | 400 |
not inherited by general import expressions. Also note that |
401 |
'abbreviation' may be used as a type-safe replacement for 'syntax' + |
|
402 |
'translations' in common applications. |
|
19084 | 403 |
|
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
404 |
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
|
405 |
independently of name spaces. The parse tree representation is |
21209
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset
|
406 |
slightly different -- use 'notation' instead of raw 'syntax', and |
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
407 |
'translations' with explicit "CONST" markup to accommodate this. |
19665 | 408 |
|
21735 | 409 |
* Pure: command 'print_abbrevs' prints all constant abbreviations of |
410 |
the current context. Print mode "no_abbrevs" prevents inversion of |
|
411 |
abbreviations on output. |
|
412 |
||
19783 | 413 |
* Isar/locales: improved parameter handling: |
414 |
- use of locales "var" and "struct" no longer necessary; |
|
415 |
- parameter renamings are no longer required to be injective. |
|
416 |
This enables, for example, to define a locale for endomorphisms thus: |
|
417 |
locale endom = homom mult mult h. |
|
418 |
||
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
419 |
* 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
|
420 |
Instead of accumulating the specification, the imported expression is |
22126 | 421 |
now an interpretation. INCOMPATIBILITY: different normal form of |
422 |
locale expressions. In particular, in interpretations of locales with |
|
423 |
predicates, goals repesenting already interpreted fragments are not |
|
424 |
removed automatically. Use methods `intro_locales' and |
|
425 |
`unfold_locales'; see below. |
|
426 |
||
427 |
* Isar/locales: new methods `intro_locales' and `unfold_locales' |
|
428 |
provide backward reasoning on locales predicates. The methods are |
|
429 |
aware of interpretations and discharge corresponding goals. |
|
430 |
`intro_locales' is less aggressive then `unfold_locales' and does not |
|
431 |
unfold predicates to assumptions. |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
432 |
|
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
433 |
* Isar/locales: the order in which locale fragments are accumulated |
22126 | 434 |
has changed. This enables to override declarations from fragments due |
435 |
to interpretations -- for example, unwanted simp rules. |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
436 |
|
23920 | 437 |
* Isar/locales: interpretation in theories and proof contexts has been |
438 |
extended. One may now specify (and prove) equations, which are |
|
439 |
unfolded in interpreted theorems. This is useful for replacing |
|
440 |
defined concepts (constants depending on locale parameters) by |
|
441 |
concepts already existing in the target context. Example: |
|
442 |
||
443 |
interpretation partial_order ["op <= :: [int, int] => bool"] |
|
444 |
where "partial_order.less (op <=) (x::int) y = (x < y)" |
|
445 |
||
23977 | 446 |
Typically, the constant `partial_order.less' is created by a definition |
447 |
specification element in the context of locale partial_order. |
|
23920 | 448 |
|
18233 | 449 |
* Provers/induct: improved internal context management to support |
450 |
local fixes and defines on-the-fly. Thus explicit meta-level |
|
451 |
connectives !! and ==> are rarely required anymore in inductive goals |
|
452 |
(using object-logic connectives for this purpose has been long |
|
453 |
obsolete anyway). The subsequent proof patterns illustrate advanced |
|
454 |
techniques of natural induction; general datatypes and inductive sets |
|
18267 | 455 |
work analogously (see also src/HOL/Lambda for realistic examples). |
456 |
||
457 |
(1) This is how to ``strengthen'' an inductive goal wrt. certain |
|
18239 | 458 |
parameters: |
18233 | 459 |
|
460 |
lemma |
|
461 |
fixes n :: nat and x :: 'a |
|
462 |
assumes a: "A n x" |
|
463 |
shows "P n x" |
|
464 |
using a -- {* make induct insert fact a *} |
|
20503 | 465 |
proof (induct n arbitrary: x) -- {* generalize goal to "!!x. A n x ==> P n x" *} |
18248 | 466 |
case 0 |
18233 | 467 |
show ?case sorry |
468 |
next |
|
18248 | 469 |
case (Suc n) |
18239 | 470 |
note `!!x. A n x ==> P n x` -- {* induction hypothesis, according to induction rule *} |
471 |
note `A (Suc n) x` -- {* induction premise, stemming from fact a *} |
|
18233 | 472 |
show ?case sorry |
473 |
qed |
|
474 |
||
18267 | 475 |
(2) This is how to perform induction over ``expressions of a certain |
18233 | 476 |
form'', using a locally defined inductive parameter n == "a x" |
18239 | 477 |
together with strengthening (the latter is usually required to get |
18267 | 478 |
sufficiently flexible induction hypotheses): |
18233 | 479 |
|
480 |
lemma |
|
481 |
fixes a :: "'a => nat" |
|
482 |
assumes a: "A (a x)" |
|
483 |
shows "P (a x)" |
|
484 |
using a |
|
20503 | 485 |
proof (induct n == "a x" arbitrary: x) |
18233 | 486 |
... |
487 |
||
18267 | 488 |
See also HOL/Isar_examples/Puzzle.thy for an application of the this |
489 |
particular technique. |
|
490 |
||
18901 | 491 |
(3) This is how to perform existential reasoning ('obtains' or |
492 |
'obtain') by induction, while avoiding explicit object-logic |
|
493 |
encodings: |
|
494 |
||
495 |
lemma |
|
496 |
fixes n :: nat |
|
497 |
obtains x :: 'a where "P n x" and "Q n x" |
|
20503 | 498 |
proof (induct n arbitrary: thesis) |
18267 | 499 |
case 0 |
500 |
obtain x where "P 0 x" and "Q 0 x" sorry |
|
18399 | 501 |
then show thesis by (rule 0) |
18267 | 502 |
next |
503 |
case (Suc n) |
|
504 |
obtain x where "P n x" and "Q n x" by (rule Suc.hyps) |
|
505 |
obtain x where "P (Suc n) x" and "Q (Suc n) x" sorry |
|
506 |
then show thesis by (rule Suc.prems) |
|
507 |
qed |
|
508 |
||
20503 | 509 |
Here the 'arbitrary: thesis' specification essentially modifies the |
510 |
scope of the formal thesis parameter, in order to the get the whole |
|
18267 | 511 |
existence statement through the induction as expected. |
18233 | 512 |
|
18506
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
513 |
* 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
|
514 |
of rule sharing the same induction cases. HOL packages usually |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
515 |
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
|
516 |
(e.g. inductive sets or datatypes). INCOMPATIBILITY, users need to |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
517 |
specify mutual induction rules differently, i.e. like this: |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
518 |
|
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
519 |
(induct rule: foo_bar.inducts) |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
520 |
(induct set: foo bar) |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
521 |
(induct type: foo bar) |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
522 |
|
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
523 |
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
|
524 |
new format. |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
525 |
|
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
526 |
* Provers/induct: improved handling of simultaneous goals. Instead of |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
527 |
introducing object-level conjunction, the statement is now split into |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
528 |
several conclusions, while the corresponding symbolic cases are |
18601
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
529 |
nested accordingly. INCOMPATIBILITY, proofs need to be structured |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
530 |
explicitly. For example: |
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
531 |
|
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
532 |
lemma |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
533 |
fixes n :: nat |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
534 |
shows "P n" and "Q n" |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
535 |
proof (induct n) |
18601
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
536 |
case 0 case 1 |
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
537 |
show "P 0" sorry |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
538 |
next |
18601
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
539 |
case 0 case 2 |
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
540 |
show "Q 0" sorry |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
541 |
next |
18601
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
542 |
case (Suc n) case 1 |
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
543 |
note `P n` and `Q n` |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
544 |
show "P (Suc n)" sorry |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
545 |
next |
18601
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
546 |
case (Suc n) case 2 |
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
547 |
note `P n` and `Q n` |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
548 |
show "Q (Suc n)" sorry |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
549 |
qed |
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
550 |
|
18601
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
551 |
The split into subcases may be deferred as follows -- this is |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
552 |
particularly relevant for goal statements with local premises. |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
553 |
|
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
554 |
lemma |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
555 |
fixes n :: nat |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
556 |
shows "A n ==> P n" and "B n ==> Q n" |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
557 |
proof (induct n) |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
558 |
case 0 |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
559 |
{ |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
560 |
case 1 |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
561 |
note `A 0` |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
562 |
show "P 0" sorry |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
563 |
next |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
564 |
case 2 |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
565 |
note `B 0` |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
566 |
show "Q 0" sorry |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
567 |
} |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
568 |
next |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
569 |
case (Suc n) |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
570 |
note `A n ==> P n` and `B n ==> Q n` |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
571 |
{ |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
572 |
case 1 |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
573 |
note `A (Suc n)` |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
574 |
show "P (Suc n)" sorry |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
575 |
next |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
576 |
case 2 |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
577 |
note `B (Suc n)` |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
578 |
show "Q (Suc n)" sorry |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
579 |
} |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
580 |
qed |
b248754b60bc
* Provers/induct: improved simultaneous goals -- nested cases;
wenzelm
parents:
18590
diff
changeset
|
581 |
|
18506
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
582 |
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
|
583 |
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
|
584 |
lists of propositions separated by 'and': |
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset
|
585 |
|
18507 | 586 |
lemma |
587 |
shows "a : A ==> P1 a" |
|
588 |
"a : A ==> P2 a" |
|
589 |
and "b : B ==> Q1 b" |
|
590 |
"b : B ==> Q2 b" |
|
591 |
"b : B ==> Q3 b" |
|
592 |
proof (induct set: A B) |
|
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset
|
593 |
|
18399 | 594 |
* Provers/induct: support coinduction as well. See |
595 |
src/HOL/Library/Coinductive_List.thy for various examples. |
|
596 |
||
20919
dab803075c62
attribute "symmetric": standardized schematic variables;
wenzelm
parents:
20857
diff
changeset
|
597 |
* Attribute "symmetric" produces result with standardized schematic |
dab803075c62
attribute "symmetric": standardized schematic variables;
wenzelm
parents:
20857
diff
changeset
|
598 |
variables (index 0). Potential INCOMPATIBILITY. |
dab803075c62
attribute "symmetric": standardized schematic variables;
wenzelm
parents:
20857
diff
changeset
|
599 |
|
22126 | 600 |
* Simplifier: by default the simplifier trace only shows top level |
601 |
rewrites now. That is, trace_simp_depth_limit is set to 1 by |
|
602 |
default. Thus there is less danger of being flooded by the trace. The |
|
603 |
trace indicates where parts have been suppressed. |
|
18674 | 604 |
|
18536
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
605 |
* Provers/classical: removed obsolete classical version of elim_format |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
606 |
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
|
607 |
manipulating the claset. |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
608 |
|
18694 | 609 |
* Provers/classical: stricter checks to ensure that supplied intro, |
610 |
dest and elim rules are well-formed; dest and elim rules must have at |
|
611 |
least one premise. |
|
612 |
||
613 |
* Provers/classical: attributes dest/elim/intro take an optional |
|
18695 | 614 |
weight argument for the rule (just as the Pure versions). Weights are |
18696 | 615 |
ignored by automated tools, but determine the search order of single |
18694 | 616 |
rule steps. |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18549
diff
changeset
|
617 |
|
18536
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
618 |
* Syntax: input syntax now supports dummy variable binding "%_. b", |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
619 |
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
|
620 |
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
|
621 |
"{_. _}" match any set comprehension as expected. Potential |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
622 |
INCOMPATIBILITY -- parse translations need to cope with syntactic |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
623 |
constant "_idtdummy" in the binding position. |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
624 |
|
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
625 |
* Syntax: removed obsolete syntactic constant "_K" and its associated |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
626 |
parse translation. INCOMPATIBILITY -- use dummy abstraction instead, |
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset
|
627 |
for example "A -> B" => "Pi A (%_. B)". |
17779 | 628 |
|
20582
ebd0e03c6a9b
* Pure: 'class_deps' command visualizes the subclass relation;
wenzelm
parents:
20503
diff
changeset
|
629 |
* Pure: 'class_deps' command visualizes the subclass relation, using |
ebd0e03c6a9b
* Pure: 'class_deps' command visualizes the subclass relation;
wenzelm
parents:
20503
diff
changeset
|
630 |
the graph browser tool. |
ebd0e03c6a9b
* Pure: 'class_deps' command visualizes the subclass relation;
wenzelm
parents:
20503
diff
changeset
|
631 |
|
20620
8b26f58c5646
* Pure: 'print_theory' now suppresses entities with internal name;
wenzelm
parents:
20607
diff
changeset
|
632 |
* Pure: 'print_theory' now suppresses entities with internal name |
8b26f58c5646
* Pure: 'print_theory' now suppresses entities with internal name;
wenzelm
parents:
20607
diff
changeset
|
633 |
(trailing "_") by default; use '!' option for full details. |
8b26f58c5646
* Pure: 'print_theory' now suppresses entities with internal name;
wenzelm
parents:
20607
diff
changeset
|
634 |
|
17865 | 635 |
|
17806 | 636 |
*** HOL *** |
637 |
||
24422 | 638 |
* Formulation of theorem "dense" changed slightly due to integration with new |
639 |
class dense_linear_order. |
|
640 |
||
24342 | 641 |
* theory Finite_Set: "name-space" locales Lattice, Distrib_lattice, Linorder etc. |
642 |
have disappeared; operations defined in terms of fold_set now are named |
|
643 |
Inf_fin, Sup_fin. INCOMPATIBILITY. |
|
644 |
||
24333 | 645 |
* HOL-Word: |
646 |
New extensive library and type for generic, fixed size machine |
|
647 |
words, with arithemtic, bit-wise, shifting and rotating operations, |
|
648 |
reflection into int, nat, and bool lists, automation for linear |
|
649 |
arithmetic (by automatic reflection into nat or int), including |
|
650 |
lemmas on overflow and monotonicity. Instantiated to all appropriate |
|
651 |
arithmetic type classes, supporting automatic simplification of |
|
652 |
numerals on all operations. Jointly developed by NICTA, Galois, and |
|
653 |
PSU. |
|
654 |
||
655 |
* Library/Boolean_Algebra: locales for abstract boolean algebras. |
|
656 |
||
657 |
* Library/Numeral_Type: numbers as types, e.g. TYPE(32). |
|
658 |
||
23850 | 659 |
* Code generator library theories: |
660 |
* Pretty_Int represents HOL integers by big integer literals in target |
|
661 |
languages. |
|
662 |
* Pretty_Char represents HOL characters by character literals in target |
|
663 |
languages. |
|
664 |
* Pretty_Char_chr like Pretty_Char, but also offers treatment of character |
|
665 |
codes; includes Pretty_Int. |
|
666 |
* Executable_Set allows to generate code for finite sets using lists. |
|
667 |
* Executable_Rat implements rational numbers as triples (sign, enumerator, |
|
668 |
denominator). |
|
669 |
* Executable_Real implements a subset of real numbers, namly those |
|
670 |
representable by rational numbers. |
|
671 |
* Efficient_Nat implements natural numbers by integers, which in general will |
|
672 |
result in higher efficency; pattern matching with 0/Suc is eliminated; |
|
673 |
includes Pretty_Int. |
|
674 |
* ML_String provides an additional datatype ml_string; in the HOL default |
|
675 |
setup, strings in HOL are mapped to lists of HOL characters in SML; values |
|
676 |
of type ml_string are mapped to strings in SML. |
|
677 |
* ML_Int provides an additional datatype ml_int which is mapped to to SML |
|
678 |
built-in integers. |
|
679 |
||
23783
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
680 |
* New package for inductive predicates |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
681 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
682 |
An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
683 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
684 |
inductive |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
685 |
p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
686 |
for z_1 :: U_1 and ... and z_n :: U_m |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
687 |
where |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
688 |
rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
689 |
| ... |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
690 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
691 |
rather than |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
692 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
693 |
consts s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
694 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
695 |
abbreviation p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
696 |
where "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
697 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
698 |
inductive "s z_1 ... z_m" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
699 |
intros |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
700 |
rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
701 |
... |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
702 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
703 |
For backward compatibility, there is a wrapper allowing inductive |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
704 |
sets to be defined with the new package via |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
705 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
706 |
inductive_set |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
707 |
s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
708 |
for z_1 :: U_1 and ... and z_n :: U_m |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
709 |
where |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
710 |
rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
711 |
| ... |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
712 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
713 |
or |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
714 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
715 |
inductive_set |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
716 |
s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
717 |
and p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
718 |
for z_1 :: U_1 and ... and z_n :: U_m |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
719 |
where |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
720 |
"p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
721 |
| rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
722 |
| ... |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
723 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
724 |
if the additional syntax "p ..." is required. |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
725 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
726 |
Many examples can be found in the subdirectories Auth, Bali, Induct, |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
727 |
or MicroJava. |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
728 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
729 |
INCOMPATIBILITIES: |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
730 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
731 |
- Since declaration and definition of inductive sets or predicates |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
732 |
is no longer separated, abbreviations involving the newly introduced |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
733 |
sets or predicates must be specified together with the introduction |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
734 |
rules after the "where" keyword (see example above), rather than before |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
735 |
the actual inductive definition. |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
736 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
737 |
- The variables in induction and elimination rules are now quantified |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
738 |
in the order of their occurrence in the introduction rules, rather than |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
739 |
in alphabetical order. Since this may break some proofs, these proofs |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
740 |
either have to be repaired, e.g. by reordering the variables |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
741 |
a_i_1 ... a_i_{k_i} in Isar "case" statements of the form |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
742 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
743 |
case (rule_i a_i_1 ... a_i_{k_i}) |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
744 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
745 |
or the old order of quantification has to be restored by explicitly adding |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
746 |
meta-level quantifiers in the introduction rules, i.e. |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
747 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
748 |
| rule_i: "!!a_i_1 ... a_i_{k_i}. ... ==> p z_1 ... z_m t_i_1 ... t_i_n" |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
749 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
750 |
- The format of the elimination rules is now |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
751 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
752 |
p z_1 ... z_m x_1 ... x_n ==> |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
753 |
(!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P) |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
754 |
==> ... ==> P |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
755 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
756 |
for predicates and |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
757 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
758 |
(x_1, ..., x_n) : s z_1 ... z_m ==> |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
759 |
(!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P) |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
760 |
==> ... ==> P |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
761 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
762 |
for sets rather than |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
763 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
764 |
x : s z_1 ... z_m ==> |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
765 |
(!!a_1_1 ... a_1_{k_1}. x = (t_1_1, ..., t_1_n) ==> ... ==> P) |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
766 |
==> ... ==> P |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
767 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
768 |
This may require terms in goals to be expanded to n-tuples (e.g. using case_tac |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
769 |
or simplification with the split_paired_all rule) before the above elimination |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
770 |
rule is applicable. |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
771 |
|
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
772 |
- The elimination or case analysis rules for (mutually) inductive sets or |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
773 |
predicates are now called "p_1.cases" ... "p_k.cases". The list of rules |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
774 |
"p_1_..._p_k.elims" is no longer available. |
e4d514f81d95
Added entry for new inductive definition package.
berghofe
parents:
23565
diff
changeset
|
775 |
|
23562 | 776 |
* Method "metis" proves goals by applying the Metis general-purpose |
777 |
resolution prover. Examples are in the directory MetisExamples. See |
|
778 |
also http://gilith.com/software/metis/ |
|
23449 | 779 |
|
23562 | 780 |
* Command 'sledgehammer' invokes external automatic theorem provers as |
781 |
background processes. It generates calls to the "metis" method if |
|
782 |
successful. These can be pasted into the proof. Users do not have to |
|
783 |
wait for the automatic provers to return. |
|
23449 | 784 |
|
23564 | 785 |
* Case-expressions allow arbitrary constructor-patterns (including "_") and |
23565 | 786 |
take their order into account, like in functional programming. |
23564 | 787 |
Internally, this is translated into nested case-expressions; missing cases |
788 |
are added and mapped to the predefined constant "undefined". In complicated |
|
789 |
cases printing may no longer show the original input but the internal |
|
23565 | 790 |
form. Lambda-abstractions allow the same form of pattern matching: |
23564 | 791 |
"% pat1 => e1 | ..." is an abbreviation for |
792 |
"%x. case x of pat1 => e1 | ..." where x is a new variable. |
|
793 |
||
23468 | 794 |
* IntDef: The constant "int :: nat => int" has been removed; now "int" |
795 |
is an abbreviation for "of_nat :: nat => int". The simplification rules |
|
796 |
for "of_nat" have been changed to work like "int" did previously. |
|
797 |
(potential INCOMPATIBILITY) |
|
798 |
- "of_nat (Suc m)" simplifies to "1 + of_nat m" instead of "of_nat m + 1" |
|
799 |
- of_nat_diff and of_nat_mult are no longer default simp rules |
|
23377 | 800 |
|
23295
86e225406859
Method "algebra" solves polynomial equations over (semi)rings
chaieb
parents:
23251
diff
changeset
|
801 |
* Method "algebra" solves polynomial equations over (semi)rings using |
86e225406859
Method "algebra" solves polynomial equations over (semi)rings
chaieb
parents:
23251
diff
changeset
|
802 |
Groebner bases. The (semi)ring structure is defined by locales and |
86e225406859
Method "algebra" solves polynomial equations over (semi)rings
chaieb
parents:
23251
diff
changeset
|
803 |
the tool setup depends on that generic context. Installing the |
86e225406859
Method "algebra" solves polynomial equations over (semi)rings
chaieb
parents:
23251
diff
changeset
|
804 |
method for a specific type involves instantiating the locale and |
86e225406859
Method "algebra" solves polynomial equations over (semi)rings
chaieb
parents:
23251
diff
changeset
|
805 |
possibly adding declarations for computation on the coefficients. |
86e225406859
Method "algebra" solves polynomial equations over (semi)rings
chaieb
parents:
23251
diff
changeset
|
806 |
The method is already instantiated for natural numbers and for the |
86e225406859
Method "algebra" solves polynomial equations over (semi)rings
chaieb
parents:
23251
diff
changeset
|
807 |
axiomatic class of idoms with numerals. See also the paper by |
86e225406859
Method "algebra" solves polynomial equations over (semi)rings
chaieb
parents:
23251
diff
changeset
|
808 |
Chaieb and Wenzel at CALCULEMUS 2007 for the general principles |
86e225406859
Method "algebra" solves polynomial equations over (semi)rings
chaieb
parents:
23251
diff
changeset
|
809 |
underlying this architecture of context-aware proof-tools. |
86e225406859
Method "algebra" solves polynomial equations over (semi)rings
chaieb
parents:
23251
diff
changeset
|
810 |
|
23029 | 811 |
* constant "List.op @" now named "List.append". Use ML antiquotations |
812 |
@{const_name List.append} or @{term " ... @ ... "} to circumvent |
|
813 |
possible incompatibilities when working on ML level. |
|
814 |
||
22997 | 815 |
* Constant renames due to introduction of canonical name prefixing for |
816 |
class package: |
|
817 |
||
818 |
HOL.abs ~> HOL.minus_class.abs |
|
819 |
HOL.divide ~> HOL.divide_class.divide |
|
820 |
Nat.power ~> Nat.power_class.power |
|
821 |
Nat.size ~> Nat.size_class.size |
|
822 |
Numeral.number_of ~> Numeral.number_class.number_of |
|
23129 | 823 |
FixedPoint.Inf ~> FixedPoint.complete_lattice_class.Inf |
24342 | 824 |
FixedPoint.Sup ~> FixedPoint.complete_lattice_class.Sup |
23129 | 825 |
|
23180 | 826 |
* Rudimentary class target mechanism involves constant renames: |
23129 | 827 |
|
828 |
Orderings.min ~> Orderings.ord_class.min |
|
829 |
Orderings.max ~> Orderings.ord_class.max |
|
22997 | 830 |
|
23564 | 831 |
* primrec: missing cases mapped to "undefined" instead of "arbitrary" |
22845 | 832 |
|
833 |
* new constant "undefined" with axiom "undefined x = undefined" |
|
834 |
||
835 |
* new class "default" with associated constant "default" |
|
836 |
||
23104 | 837 |
* new function listsum :: 'a list => 'a for arbitrary monoids. |
838 |
Special syntax: "SUM x <- xs. f x" (and latex variants) |
|
839 |
||
23210 | 840 |
* new (input only) syntax for Haskell-like list comprehension, eg |
841 |
[(x,y). x <- xs, y <- ys, x ~= y] |
|
842 |
For details see List.thy. |
|
23102 | 843 |
|
23300 | 844 |
* The special syntax for function "filter" has changed from [x : xs. P] to |
845 |
[x <- xs. P] to avoid an ambiguity caused by list comprehension syntax, |
|
846 |
and for uniformity. INCOMPATIBILITY |
|
847 |
||
23971
e6d505d5b03d
renamed lemma "set_take_whileD" to "set_takeWhileD"
krauss
parents:
23920
diff
changeset
|
848 |
* Lemma "set_take_whileD" renamed to "set_takeWhileD" |
e6d505d5b03d
renamed lemma "set_take_whileD" to "set_takeWhileD"
krauss
parents:
23920
diff
changeset
|
849 |
|
24507 | 850 |
* function "sgn" is now overloaded and available on int, real, complex |
851 |
(and other numeric types). |
|
852 |
The details: new class "sgn" with function "sgn"; |
|
853 |
two possible defs of sgn in the classes sgn_if and sgn_div_norm |
|
854 |
(as equational assumptions); |
|
855 |
ordered_idom now also inherits from sgn_if - INCOMPATIBILITY. |
|
24492 | 856 |
|
23480 | 857 |
* New lemma collection field_simps (an extension of ring_simps) |
858 |
for manipulating (in)equations involving division. Multiplies |
|
23481 | 859 |
with all denominators that can be proved to be non-zero (in equations) |
23480 | 860 |
or positive/negative (in inequations). |
861 |
||
862 |
* Lemma collections ring_eq_simps, group_eq_simps and ring_distrib |
|
23478 | 863 |
have been improved and renamed to ring_simps, group_simps and ring_distribs. |
23509 | 864 |
Removed lemmas field_xyz in Ring_and_Field |
865 |
because they were subsumed by lemmas xyz. |
|
866 |
INCOMPATIBILITY. |
|
23478 | 867 |
|
22799
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22754
diff
changeset
|
868 |
* Library/Pretty_Int.thy: maps HOL numerals on target language integer literals |
23480 | 869 |
when generating code. |
22799
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22754
diff
changeset
|
870 |
|
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22754
diff
changeset
|
871 |
* Library/Pretty_Char.thy: maps HOL characters on target language character literals |
23480 | 872 |
when generating code. |
22799
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22754
diff
changeset
|
873 |
|
22735 | 874 |
* Library/Commutative_Ring.thy: switched from recdef to function package; |
23480 | 875 |
constants add, mul, pow now curried. Infix syntax for algebraic operations. |
22735 | 876 |
|
22450 | 877 |
* Some steps towards more uniform lattice theory development in HOL. |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
878 |
|
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
879 |
constants "meet" and "join" now named "inf" and "sup" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
880 |
constant "Meet" now named "Inf" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
881 |
|
22450 | 882 |
classes "meet_semilorder" and "join_semilorder" now named |
883 |
"lower_semilattice" and "upper_semilattice" |
|
884 |
class "lorder" now named "lattice" |
|
885 |
class "comp_lat" now named "complete_lattice" |
|
886 |
||
887 |
Instantiation of lattice classes allows explicit definitions |
|
24342 | 888 |
for "inf" and "sup" operations (or "Inf" and "Sup" for complete lattices). |
22450 | 889 |
|
23129 | 890 |
INCOMPATIBILITY. Theorem renames: |
22450 | 891 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
892 |
meet_left_le ~> inf_le1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
893 |
meet_right_le ~> inf_le2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
894 |
join_left_le ~> sup_ge1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
895 |
join_right_le ~> sup_ge2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
896 |
meet_join_le ~> inf_sup_ord |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
897 |
le_meetI ~> le_infI |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
898 |
join_leI ~> le_supI |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
899 |
le_meet ~> le_inf_iff |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
900 |
le_join ~> ge_sup_conv |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
901 |
meet_idempotent ~> inf_idem |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
902 |
join_idempotent ~> sup_idem |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
903 |
meet_comm ~> inf_commute |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
904 |
join_comm ~> sup_commute |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
905 |
meet_leI1 ~> le_infI1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
906 |
meet_leI2 ~> le_infI2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
907 |
le_joinI1 ~> le_supI1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
908 |
le_joinI2 ~> le_supI2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
909 |
meet_assoc ~> inf_assoc |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
910 |
join_assoc ~> sup_assoc |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
911 |
meet_left_comm ~> inf_left_commute |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
912 |
meet_left_idempotent ~> inf_left_idem |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
913 |
join_left_comm ~> sup_left_commute |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
914 |
join_left_idempotent ~> sup_left_idem |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
915 |
meet_aci ~> inf_aci |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
916 |
join_aci ~> sup_aci |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
917 |
le_def_meet ~> le_iff_inf |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
918 |
le_def_join ~> le_iff_sup |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
919 |
join_absorp2 ~> sup_absorb2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
920 |
join_absorp1 ~> sup_absorb1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
921 |
meet_absorp1 ~> inf_absorb1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
922 |
meet_absorp2 ~> inf_absorb2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
923 |
meet_join_absorp ~> inf_sup_absorb |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
924 |
join_meet_absorp ~> sup_inf_absorb |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
925 |
distrib_join_le ~> distrib_sup_le |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
926 |
distrib_meet_le ~> distrib_inf_le |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
927 |
|
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
928 |
add_meet_distrib_left ~> add_inf_distrib_left |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
929 |
add_join_distrib_left ~> add_sup_distrib_left |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
930 |
is_join_neg_meet ~> is_join_neg_inf |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
931 |
is_meet_neg_join ~> is_meet_neg_sup |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
932 |
add_meet_distrib_right ~> add_inf_distrib_right |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
933 |
add_join_distrib_right ~> add_sup_distrib_right |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
934 |
add_meet_join_distribs ~> add_sup_inf_distribs |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
935 |
join_eq_neg_meet ~> sup_eq_neg_inf |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
936 |
meet_eq_neg_join ~> inf_eq_neg_sup |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
937 |
add_eq_meet_join ~> add_eq_inf_sup |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
938 |
meet_0_imp_0 ~> inf_0_imp_0 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
939 |
join_0_imp_0 ~> sup_0_imp_0 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
940 |
meet_0_eq_0 ~> inf_0_eq_0 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
941 |
join_0_eq_0 ~> sup_0_eq_0 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
942 |
neg_meet_eq_join ~> neg_inf_eq_sup |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
943 |
neg_join_eq_meet ~> neg_sup_eq_inf |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
944 |
join_eq_if ~> sup_eq_if |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
945 |
|
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
946 |
mono_meet ~> mono_inf |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
947 |
mono_join ~> mono_sup |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
948 |
meet_bool_eq ~> inf_bool_eq |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
949 |
join_bool_eq ~> sup_bool_eq |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
950 |
meet_fun_eq ~> inf_fun_eq |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
951 |
join_fun_eq ~> sup_fun_eq |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
952 |
meet_set_eq ~> inf_set_eq |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
953 |
join_set_eq ~> sup_set_eq |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
954 |
meet1_iff ~> inf1_iff |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
955 |
meet2_iff ~> inf2_iff |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
956 |
meet1I ~> inf1I |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
957 |
meet2I ~> inf2I |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
958 |
meet1D1 ~> inf1D1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
959 |
meet2D1 ~> inf2D1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
960 |
meet1D2 ~> inf1D2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
961 |
meet2D2 ~> inf2D2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
962 |
meet1E ~> inf1E |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
963 |
meet2E ~> inf2E |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
964 |
join1_iff ~> sup1_iff |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
965 |
join2_iff ~> sup2_iff |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
966 |
join1I1 ~> sup1I1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
967 |
join2I1 ~> sup2I1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
968 |
join1I1 ~> sup1I1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
969 |
join2I2 ~> sup1I2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
970 |
join1CI ~> sup1CI |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
971 |
join2CI ~> sup2CI |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
972 |
join1E ~> sup1E |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
973 |
join2E ~> sup2E |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
974 |
|
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
975 |
is_meet_Meet ~> is_meet_Inf |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
976 |
Meet_bool_def ~> Inf_bool_def |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
977 |
Meet_fun_def ~> Inf_fun_def |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
978 |
Meet_greatest ~> Inf_greatest |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
979 |
Meet_lower ~> Inf_lower |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
980 |
Meet_set_def ~> Inf_set_def |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
981 |
|
24342 | 982 |
Sup_def ~> Sup_Inf |
983 |
Sup_bool_eq ~> Sup_bool_def |
|
984 |
Sup_fun_eq ~> Sup_fun_def |
|
985 |
Sup_set_eq ~> Sup_set_def |
|
986 |
||
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
987 |
listsp_meetI ~> listsp_infI |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
988 |
listsp_meet_eq ~> listsp_inf_eq |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
989 |
|
22450 | 990 |
meet_min ~> inf_min |
991 |
join_max ~> sup_max |
|
992 |
||
22845 | 993 |
* Classes "order" and "linorder": facts "refl", "trans" and |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22376
diff
changeset
|
994 |
"cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to |
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22376
diff
changeset
|
995 |
avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY. |
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22376
diff
changeset
|
996 |
|
22845 | 997 |
* Classes "order" and "linorder": |
22316 | 998 |
potential INCOMPATIBILITY: order of proof goals in order/linorder instance |
999 |
proofs changed. |
|
1000 |
||
22218 | 1001 |
* Dropped lemma duplicate def_imp_eq in favor of meta_eq_to_obj_eq. |
1002 |
INCOMPATIBILITY. |
|
1003 |
||
1004 |
* Dropped lemma duplicate if_def2 in favor of if_bool_eq_conj. |
|
1005 |
INCOMPATIBILITY. |
|
1006 |
||
22126 | 1007 |
* Added syntactic class "size"; overloaded constant "size" now has |
1008 |
type "'a::size ==> bool" |
|
1009 |
||
1010 |
* Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op |
|
22997 | 1011 |
dvd" to "Divides.div_class.div", "Divides.div_class.mod" and "Divides.dvd". INCOMPATIBILITY. |
22126 | 1012 |
|
1013 |
* Added method "lexicographic_order" automatically synthesizes |
|
1014 |
termination relations as lexicographic combinations of size measures |
|
1015 |
-- 'function' package. |
|
1016 |
||
1017 |
* HOL/records: generalised field-update to take a function on the |
|
1018 |
field rather than the new value: r(|A := x|) is translated to A_update |
|
1019 |
(K x) r The K-combinator that is internally used is called K_record. |
|
21226
a607ae87ee81
field-update in records is generalised to take a function on the field
schirmer
parents:
21215
diff
changeset
|
1020 |
INCOMPATIBILITY: Usage of the plain update functions has to be |
a607ae87ee81
field-update in records is generalised to take a function on the field
schirmer
parents:
21215
diff
changeset
|
1021 |
adapted. |
a607ae87ee81
field-update in records is generalised to take a function on the field
schirmer
parents:
21215
diff
changeset
|
1022 |
|
22126 | 1023 |
* axclass "semiring_0" now contains annihilation axioms x * 0 = 0 and |
1024 |
0 * x = 0, which are required for a semiring. Richer structures do |
|
1025 |
not inherit from semiring_0 anymore, because this property is a |
|
1026 |
theorem there, not an axiom. INCOMPATIBILITY: In instances of |
|
1027 |
semiring_0, there is more to prove, but this is mostly trivial. |
|
1028 |
||
1029 |
* axclass "recpower" was generalized to arbitrary monoids, not just |
|
1030 |
commutative semirings. INCOMPATIBILITY: If you use recpower and need |
|
1031 |
commutativity or a semiring property, add the corresponding classes. |
|
1032 |
||
1033 |
* Unified locale partial_order with class definition (cf. theory |
|
1034 |
Orderings), added parameter ``less''. INCOMPATIBILITY. |
|
21215
7c9337a0e30a
made locale partial_order compatible with axclass order
haftmann
parents:
21209
diff
changeset
|
1035 |
|
21099 | 1036 |
* Constant "List.list_all2" in List.thy now uses authentic syntax. |
22126 | 1037 |
INCOMPATIBILITY: translations containing list_all2 may go wrong. On |
1038 |
Isar level, use abbreviations instead. |
|
1039 |
||
1040 |
* Renamed constant "List.op mem" to "List.memberl" INCOMPATIBILITY: |
|
1041 |
rarely occuring name references (e.g. ``List.op mem.simps'') require |
|
1042 |
renaming (e.g. ``List.memberl.simps''). |
|
1043 |
||
22997 | 1044 |
* Renamed constants "0" to "HOL.zero_class.zero" and "1" to "HOL.one_class.one". |
22126 | 1045 |
INCOMPATIBILITY. |
1046 |
||
23251 | 1047 |
* Added class "HOL.eq", allowing for code generation with polymorphic equality. |
22126 | 1048 |
|
1049 |
* Numeral syntax: type 'bin' which was a mere type copy of 'int' has |
|
1050 |
been abandoned in favour of plain 'int'. INCOMPATIBILITY -- |
|
1051 |
significant changes for setting up numeral syntax for types: |
|
20485 | 1052 |
|
1053 |
- new constants Numeral.pred and Numeral.succ instead |
|
1054 |
of former Numeral.bin_pred and Numeral.bin_succ. |
|
1055 |
- Use integer operations instead of bin_add, bin_mult and so on. |
|
1056 |
- Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps. |
|
1057 |
- ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs. |
|
1058 |
||
1059 |
See HOL/Integ/IntArith.thy for an example setup. |
|
1060 |
||
22126 | 1061 |
* New top level command 'normal_form' computes the normal form of a |
1062 |
term that may contain free variables. For example ``normal_form |
|
1063 |
"rev[a,b,c]"'' produces ``[b,c,a]'' (without proof). This command is |
|
1064 |
suitable for heavy-duty computations because the functions are |
|
1065 |
compiled to ML first. |
|
19895 | 1066 |
|
17996 | 1067 |
* Alternative iff syntax "A <-> B" for equality on bool (with priority |
1068 |
25 like -->); output depends on the "iff" print_mode, the default is |
|
1069 |
"A = B" (with priority 50). |
|
1070 |
||
19279 | 1071 |
* Renamed constants in HOL.thy and Orderings.thy: |
22997 | 1072 |
op + ~> HOL.plus_class.plus |
1073 |
op - ~> HOL.minus_class.minus |
|
1074 |
uminus ~> HOL.minus_class.uminus |
|
23881 | 1075 |
abs ~> HOL.abs_class.abs |
22997 | 1076 |
op * ~> HOL.times_class.times |
23881 | 1077 |
op < ~> HOL.ord_class.less |
1078 |
op <= ~> HOL.ord_class.less_eq |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset
|
1079 |
|
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset
|
1080 |
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
|
1081 |
|
19377 | 1082 |
a) User-defined constants using any of the names "plus", "minus", "times", |
1083 |
"less" or "less_eq". The standard syntax translations for "+", "-" and "*" |
|
1084 |
may go wrong. |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset
|
1085 |
INCOMPATIBILITY: use more specific names. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset
|
1086 |
|
19277 | 1087 |
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
|
1088 |
INCOMPATIBILITY: use more specific names. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset
|
1089 |
|
19377 | 1090 |
c) Permutative equations (e.g. "a + b = b + a") |
1091 |
Since the change of names also changes the order of terms, permutative |
|
1092 |
rewrite rules may get applied in a different order. Experience shows that |
|
1093 |
this is rarely the case (only two adaptions in the whole Isabelle |
|
1094 |
distribution). |
|
1095 |
INCOMPATIBILITY: rewrite proofs |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset
|
1096 |
|
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset
|
1097 |
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
|
1098 |
This in general only affects hand-written proof tactics, simprocs and so on. |
22997 | 1099 |
INCOMPATIBILITY: grep your sourcecode and replace names. Consider use |
1100 |
of const_name ML antiquotations. |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset
|
1101 |
|
21265 | 1102 |
* Relations less (<) and less_eq (<=) are also available on type bool. |
1103 |
Modified syntax to disallow nesting without explicit parentheses, |
|
1104 |
e.g. "(x < y) < z" or "x < (y < z)", but NOT "x < y < z". |
|
1105 |
||
18674 | 1106 |
* "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only). |
1107 |
||
20716
a6686a8e1b68
Changed precedence of "op O" (relation composition) from 60 to 75.
krauss
parents:
20712
diff
changeset
|
1108 |
* Relation composition operator "op O" now has precedence 75 and binds |
a6686a8e1b68
Changed precedence of "op O" (relation composition) from 60 to 75.
krauss
parents:
20712
diff
changeset
|
1109 |
stronger than union and intersection. INCOMPATIBILITY. |
a6686a8e1b68
Changed precedence of "op O" (relation composition) from 60 to 75.
krauss
parents:
20712
diff
changeset
|
1110 |
|
22126 | 1111 |
* The old set interval syntax "{m..n(}" (and relatives) has been |
1112 |
removed. Use "{m..<n}" (and relatives) instead. |
|
19377 | 1113 |
|
17865 | 1114 |
* In the context of the assumption "~(s = t)" the Simplifier rewrites |
1115 |
"t = s" to False (by simproc "neq_simproc"). For backward |
|
1116 |
compatibility this can be disabled by ML "reset use_neq_simproc". |
|
17779 | 1117 |
|
22126 | 1118 |
* "m dvd n" where m and n are numbers is evaluated to True/False by |
1119 |
simp. |
|
1120 |
||
1121 |
* Theorem Cons_eq_map_conv no longer declared as ``simp''. |
|
19211 | 1122 |
|
19279 | 1123 |
* Theorem setsum_mult renamed to setsum_right_distrib. |
1124 |
||
19211 | 1125 |
* Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the |
22126 | 1126 |
``rule'' method. |
1127 |
||
1128 |
* Reimplemented methods ``sat'' and ``satx'', with several |
|
1129 |
improvements: goals no longer need to be stated as "<prems> ==> |
|
1130 |
False", equivalences (i.e. "=" on type bool) are handled, variable |
|
1131 |
names of the form "lit_<n>" are no longer reserved, significant |
|
1132 |
speedup. |
|
1133 |
||
1134 |
* Methods ``sat'' and ``satx'' can now replay MiniSat proof traces. |
|
1135 |
zChaff is still supported as well. |
|
1136 |
||
1137 |
* 'inductive' and 'datatype': provide projections of mutual rules, |
|
1138 |
bundled as foo_bar.inducts; |
|
1139 |
||
1140 |
* Library: moved theories Parity, GCD, Binomial, Infinite_Set to |
|
1141 |
Library. |
|
21256 | 1142 |
|
1143 |
* Library: moved theory Accessible_Part to main HOL. |
|
19572
a4b3176f19dd
* Library: theory Accessible_Part has been move to main HOL.
wenzelm
parents:
19508
diff
changeset
|
1144 |
|
18446 | 1145 |
* Library: added theory Coinductive_List of potentially infinite lists |
1146 |
as greatest fixed-point. |
|
18399 | 1147 |
|
19254 | 1148 |
* Library: added theory AssocList which implements (finite) maps as |
19252 | 1149 |
association lists. |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17806
diff
changeset
|
1150 |
|
22126 | 1151 |
* Added proof method ``evaluation'' for efficiently solving a goal |
1152 |
(i.e. a boolean expression) by compiling it to ML. The goal is |
|
1153 |
"proved" (via an oracle) if it evaluates to True. |
|
20807 | 1154 |
|
1155 |
* Linear arithmetic now splits certain operators (e.g. min, max, abs) |
|
1156 |
also when invoked by the simplifier. This results in the simplifier |
|
21056 | 1157 |
being more powerful on arithmetic goals. INCOMPATIBILITY. Set |
20807 | 1158 |
fast_arith_split_limit to 0 to obtain the old behavior. |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20188
diff
changeset
|
1159 |
|
22126 | 1160 |
* Support for hex (0x20) and binary (0b1001) numerals. |
19254 | 1161 |
|
20807 | 1162 |
* New method: reify eqs (t), where eqs are equations for an |
1163 |
interpretation I :: 'a list => 'b => 'c and t::'c is an optional |
|
1164 |
parameter, computes a term s::'b and a list xs::'a list and proves the |
|
1165 |
theorem I xs s = t. This is also known as reification or quoting. The |
|
1166 |
resulting theorem is applied to the subgoal to substitute t with I xs |
|
1167 |
s. If t is omitted, the subgoal itself is reified. |
|
1168 |
||
1169 |
* New method: reflection corr_thm eqs (t). The parameters eqs and (t) |
|
1170 |
are as explained above. corr_thm is a theorem for I vs (f t) = I vs t, |
|
1171 |
where f is supposed to be a computable function (in the sense of code |
|
1172 |
generattion). The method uses reify to compute s and xs as above then |
|
1173 |
applies corr_thm and uses normalization by evaluation to "prove" f s = |
|
1174 |
r and finally gets the theorem t = r, which is again applied to the |
|
1175 |
subgoal. An Example is available in HOL/ex/ReflectionEx.thy. |
|
1176 |
||
23881 | 1177 |
* Reflection: Automatic reification now handels binding, an example |
20807 | 1178 |
is available in HOL/ex/ReflectionEx.thy |
1179 |
||
1180 |
||
20169 | 1181 |
*** HOL-Algebra *** |
1182 |
||
21170 | 1183 |
* Formalisation of ideals and the quotient construction over rings. |
1184 |
||
1185 |
* Order and lattice theory no longer based on records. |
|
1186 |
INCOMPATIBILITY. |
|
1187 |
||
22126 | 1188 |
* Renamed lemmas least_carrier -> least_closed and greatest_carrier -> |
1189 |
greatest_closed. INCOMPATIBILITY. |
|
21896
9a7949815a84
Experimenting with interpretations of "definition".
ballarin
parents:
21879
diff
changeset
|
1190 |
|
21170 | 1191 |
* Method algebra is now set up via an attribute. For examples see |
21896
9a7949815a84
Experimenting with interpretations of "definition".
ballarin
parents:
21879
diff
changeset
|
1192 |
Ring.thy. INCOMPATIBILITY: the method is now weaker on combinations |
21170 | 1193 |
of algebraic structures. |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20217
diff
changeset
|
1194 |
|
22126 | 1195 |
* Renamed theory CRing to Ring. |
20169 | 1196 |
|
20807 | 1197 |
|
19653 | 1198 |
*** HOL-Complex *** |
1199 |
||
1200 |
* Theory Real: new method ferrack implements quantifier elimination |
|
1201 |
for linear arithmetic over the reals. The quantifier elimination |
|
1202 |
feature is used only for decision, for compatibility with arith. This |
|
1203 |
means a goal is either solved or left unchanged, no simplification. |
|
1204 |
||
22971 | 1205 |
* Hyperreal: Functions root and sqrt are now defined on negative real |
1206 |
inputs so that root n (- x) = - root n x and sqrt (- x) = - sqrt x. |
|
1207 |
Nonnegativity side conditions have been removed from many lemmas, so |
|
1208 |
that more subgoals may now be solved by simplification; potential |
|
1209 |
INCOMPATIBILITY. |
|
1210 |
||
21791 | 1211 |
* Real: New axiomatic classes formalize real normed vector spaces and |
1212 |
algebras, using new overloaded constants scaleR :: real => 'a => 'a |
|
1213 |
and norm :: 'a => real. |
|
1214 |
||
22126 | 1215 |
* Real: New constant of_real :: real => 'a::real_algebra_1 injects |
1216 |
from reals into other types. The overloaded constant Reals :: 'a set |
|
1217 |
is now defined as range of_real; potential INCOMPATIBILITY. |
|
1218 |
||
23013 | 1219 |
* Real: ML code generation is supported now and hence also quickcheck. |
1220 |
Reals are implemented as arbitrary precision rationals. |
|
1221 |
||
22126 | 1222 |
* Hyperreal: Several constants that previously worked only for the |
1223 |
reals have been generalized, so they now work over arbitrary vector |
|
1224 |
spaces. Type annotations may need to be added in some cases; potential |
|
1225 |
INCOMPATIBILITY. |
|
21791 | 1226 |
|
22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22971
diff
changeset
|
1227 |
Infinitesimal :: ('a::real_normed_vector) star set |
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22971
diff
changeset
|
1228 |
HFinite :: ('a::real_normed_vector) star set |
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22971
diff
changeset
|
1229 |
HInfinite :: ('a::real_normed_vector) star set |
21791 | 1230 |
approx :: ('a::real_normed_vector) star => 'a star => bool |
1231 |
monad :: ('a::real_normed_vector) star => 'a star set |
|
1232 |
galaxy :: ('a::real_normed_vector) star => 'a star set |
|
22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22971
diff
changeset
|
1233 |
(NS)LIMSEQ :: [nat => 'a::real_normed_vector, 'a] => bool |
21791 | 1234 |
(NS)convergent :: (nat => 'a::real_normed_vector) => bool |
1235 |
(NS)Bseq :: (nat => 'a::real_normed_vector) => bool |
|
1236 |
(NS)Cauchy :: (nat => 'a::real_normed_vector) => bool |
|
1237 |
(NS)LIM :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool |
|
1238 |
is(NS)Cont :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool |
|
1239 |
deriv :: ['a::real_normed_field => 'a, 'a, 'a] => bool |
|
22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22971
diff
changeset
|
1240 |
sgn :: 'a::real_normed_vector => 'a |
23116 | 1241 |
exp :: 'a::{recpower,real_normed_field,banach} => 'a |
21791 | 1242 |
|
1243 |
* Complex: Some complex-specific constants are now abbreviations for |
|
22126 | 1244 |
overloaded ones: complex_of_real = of_real, cmod = norm, hcmod = |
1245 |
hnorm. Other constants have been entirely removed in favor of the |
|
1246 |
polymorphic versions (INCOMPATIBILITY): |
|
21791 | 1247 |
|
1248 |
approx <-- capprox |
|
1249 |
HFinite <-- CFinite |
|
1250 |
HInfinite <-- CInfinite |
|
1251 |
Infinitesimal <-- CInfinitesimal |
|
1252 |
monad <-- cmonad |
|
1253 |
galaxy <-- cgalaxy |
|
1254 |
(NS)LIM <-- (NS)CLIM, (NS)CRLIM |
|
1255 |
is(NS)Cont <-- is(NS)Contc, is(NS)contCR |
|
1256 |
(ns)deriv <-- (ns)cderiv |
|
1257 |
||
19653 | 1258 |
|
17878 | 1259 |
*** ML *** |
1260 |
||
23251 | 1261 |
* Generic arithmetic modules: Tools/integer.ML, Tools/rat.ML, Tools/float.ML |
1262 |
||
22848 | 1263 |
* Context data interfaces (Theory/Proof/GenericDataFun): removed |
22863 | 1264 |
name/print, uninitialized data defaults to ad-hoc copy of empty value, |
1265 |
init only required for impure data. INCOMPATIBILITY: empty really |
|
1266 |
need to be empty (no dependencies on theory content!) |
|
22848 | 1267 |
|
22138 | 1268 |
* ML within Isar: antiquotations allow to embed statically-checked |
1269 |
formal entities in the source, referring to the context available at |
|
1270 |
compile-time. For example: |
|
1271 |
||
1272 |
ML {* @{typ "'a => 'b"} *} |
|
1273 |
ML {* @{term "%x. x"} *} |
|
1274 |
ML {* @{prop "x == y"} *} |
|
1275 |
ML {* @{ctyp "'a => 'b"} *} |
|
1276 |
ML {* @{cterm "%x. x"} *} |
|
1277 |
ML {* @{cprop "x == y"} *} |
|
1278 |
ML {* @{thm asm_rl} *} |
|
1279 |
ML {* @{thms asm_rl} *} |
|
22376 | 1280 |
ML {* @{const_name c} *} |
1281 |
ML {* @{const_syntax c} *} |
|
22138 | 1282 |
ML {* @{context} *} |
1283 |
ML {* @{theory} *} |
|
1284 |
ML {* @{theory Pure} *} |
|
1285 |
ML {* @{simpset} *} |
|
1286 |
ML {* @{claset} *} |
|
1287 |
ML {* @{clasimpset} *} |
|
1288 |
||
22151 | 1289 |
The same works for sources being ``used'' within an Isar context. |
1290 |
||
22152 | 1291 |
* ML in Isar: improved error reporting; extra verbosity with |
1292 |
Toplevel.debug enabled. |
|
1293 |
||
20348 | 1294 |
* Pure/library: |
1295 |
||
18450
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
1296 |
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
|
1297 |
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
|
1298 |
|
18540 | 1299 |
The semantics of "burrow" is: "take a function with *simulatanously* |
1300 |
transforms a list of value, and apply it *simulatanously* to a list of |
|
22126 | 1301 |
list of values of the appropriate type". Compare this with "map" which |
18540 | 1302 |
would *not* apply its argument function simulatanously but in |
22126 | 1303 |
sequence; "fold_burrow" has an additional context. |
18450
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset
|
1304 |
|
18446 | 1305 |
* Pure/library: functions map2 and fold2 with curried syntax for |
1306 |
simultanous mapping and folding: |
|
1307 |
||
18422
875451c9d253
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18399
diff
changeset
|
1308 |
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
|
1309 |
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
|
1310 |
|
18446 | 1311 |
* Pure/library: indexed lists - some functions in the Isabelle library |
1312 |
treating lists over 'a as finite mappings from [0...n] to 'a have been |
|
1313 |
given more convenient names and signatures reminiscent of similar |
|
1314 |
functions for alists, tables, etc: |
|
18051 | 1315 |
|
1316 |
val nth: 'a list -> int -> 'a |
|
1317 |
val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list |
|
1318 |
val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b |
|
1319 |
||
18446 | 1320 |
Note that fold_index starts counting at index 0, not 1 like foldln |
1321 |
used to. |
|
1322 |
||
22126 | 1323 |
* Pure/library: added general ``divide_and_conquer'' combinator on |
1324 |
lists. |
|
19032 | 1325 |
|
1326 |
* 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
|
1327 |
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
|
1328 |
admits slightly more efficient complex applications. |
18446 | 1329 |
|
18642 | 1330 |
* Pure: datatype Context.generic joins theory/Proof.context and |
18644 | 1331 |
provides some facilities for code that works in either kind of |
18642 | 1332 |
context, notably GenericDataFun for uniform theory and proof data. |
1333 |
||
18862
bd83590be0f7
* Pure: 'advanced' translation functions use Context.generic instead of just theory;
wenzelm
parents:
18815
diff
changeset
|
1334 |
* 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
|
1335 |
use Context.generic instead of just theory. |
bd83590be0f7
* Pure: 'advanced' translation functions use Context.generic instead of just theory;
wenzelm
parents:
18815
diff
changeset
|
1336 |
|
18737 | 1337 |
* Pure: simplified internal attribute type, which is now always |
1338 |
Context.generic * thm -> Context.generic * thm. Global (theory) |
|
1339 |
vs. local (Proof.context) attributes have been discontinued, while |
|
18738 | 1340 |
minimizing code duplication. Thm.rule_attribute and |
1341 |
Thm.declaration_attribute build canonical attributes; see also |
|
19006
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset
|
1342 |
structure Context for further operations on Context.generic, notably |
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset
|
1343 |
GenericDataFun. INCOMPATIBILITY, need to adapt attribute type |
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset
|
1344 |
declarations and definitions. |
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset
|
1345 |
|
19508 | 1346 |
* Pure/kernel: consts certification ignores sort constraints given in |
1347 |
signature declarations. (This information is not relevant to the |
|
22126 | 1348 |
logic, but only for type inference.) IMPORTANT INTERNAL CHANGE, |
1349 |
potential INCOMPATIBILITY. |
|
19508 | 1350 |
|
1351 |
* Pure: axiomatic type classes are now purely definitional, with |
|
1352 |
explicit proofs of class axioms and super class relations performed |
|
1353 |
internally. See Pure/axclass.ML for the main internal interfaces -- |
|
1354 |
notably AxClass.define_class supercedes AxClass.add_axclass, and |
|
1355 |
AxClass.axiomatize_class/classrel/arity supercede |
|
1356 |
Sign.add_classes/classrel/arities. |
|
1357 |
||
19006
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset
|
1358 |
* Pure/Isar: Args/Attrib parsers operate on Context.generic -- |
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset
|
1359 |
global/local versions on theory vs. Proof.context have been |
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset
|
1360 |
discontinued; Attrib.syntax and Method.syntax have been adapted |
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset
|
1361 |
accordingly. INCOMPATIBILITY, need to adapt parser expressions for |
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset
|
1362 |
attributes, methods, etc. |
18642 | 1363 |
|
18446 | 1364 |
* Pure: several functions of signature "... -> theory -> theory * ..." |
1365 |
have been reoriented to "... -> theory -> ... * theory" in order to |
|
1366 |
allow natural usage in combination with the ||>, ||>>, |-> and |
|
1367 |
fold_map combinators. |
|
18051 | 1368 |
|
21647
fccafa917a68
* Pure: official theorem names and additional comments are now strictly separate.
wenzelm
parents:
21595
diff
changeset
|
1369 |
* Pure: official theorem names (closed derivations) and additional |
fccafa917a68
* Pure: official theorem names and additional comments are now strictly separate.
wenzelm
parents:
21595
diff
changeset
|
1370 |
comments (tags) are now strictly separate. Name hints -- which are |
fccafa917a68
* Pure: official theorem names and additional comments are now strictly separate.
wenzelm
parents:
21595
diff
changeset
|
1371 |
maintained as tags -- may be attached any time without affecting the |
fccafa917a68
* Pure: official theorem names and additional comments are now strictly separate.
wenzelm
parents:
21595
diff
changeset
|
1372 |
derivation. |
fccafa917a68
* Pure: official theorem names and additional comments are now strictly separate.
wenzelm
parents:
21595
diff
changeset
|
1373 |
|
18020 | 1374 |
* Pure: primitive rule lift_rule now takes goal cterm instead of an |
18145 | 1375 |
actual goal state (thm). Use Thm.lift_rule (Thm.cprem_of st i) to |
18020 | 1376 |
achieve the old behaviour. |
1377 |
||
1378 |
* Pure: the "Goal" constant is now called "prop", supporting a |
|
1379 |
slightly more general idea of ``protecting'' meta-level rule |
|
1380 |
statements. |
|
1381 |
||
20040
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset
|
1382 |
* 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
|
1383 |
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
|
1384 |
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
|
1385 |
|
20090 | 1386 |
* Pure: structure Name provides scalable operations for generating |
1387 |
internal variable names, notably Name.variants etc. This replaces |
|
1388 |
some popular functions from term.ML: |
|
1389 |
||
1390 |
Term.variant -> Name.variant |
|
1391 |
Term.variantlist -> Name.variant_list (*canonical argument order*) |
|
1392 |
Term.invent_names -> Name.invent_list |
|
1393 |
||
1394 |
Note that low-level renaming rarely occurs in new code -- operations |
|
1395 |
from structure Variable are used instead (see below). |
|
1396 |
||
20040
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset
|
1397 |
* 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
|
1398 |
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
|
1399 |
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
|
1400 |
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
|
1401 |
various freeze_thaw operations. |
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset
|
1402 |
|
18567 | 1403 |
* 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
|
1404 |
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
|
1405 |
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
|
1406 |
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
|
1407 |
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
|
1408 |
OldGoals.prove_goalw_cterm has long been obsolete, si |