1 |
1 |
2 Isabelle NEWS -- history user-relevant changes |
2 Isabelle NEWS -- history user-relevant changes |
3 ============================================== |
3 ============================================== |
4 |
4 |
5 New in this Isabelle version |
5 New in Isabelle99-1 (September 2000) |
6 ---------------------------- |
6 ------------------------------------ |
7 |
7 |
8 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
8 *** Overview of INCOMPATIBILITIES *** |
9 |
9 |
10 * HOL: simplification of natural numbers is much changed; to partly |
10 * HOL: simplification of natural numbers is much changed; to partly |
11 recover the old behaviour (e.g. to prevent n+n rewriting to #2*n) |
11 recover the old behaviour (e.g. to prevent n+n rewriting to #2*n) |
12 issue the following ML commands: |
12 issue the following ML commands: |
13 |
13 |
14 Delsimprocs Nat_Numeral_Simprocs.cancel_numerals; |
14 Delsimprocs Nat_Numeral_Simprocs.cancel_numerals; |
15 Delsimprocs [Nat_Numeral_Simprocs.combine_numerals]; |
15 Delsimprocs [Nat_Numeral_Simprocs.combine_numerals]; |
16 |
16 |
17 * HOL: 0 is now overloaded, so the type constraint ::nat may sometimes be |
17 * HOL: simplification no longer dives into case-expressions; |
18 needed; |
18 |
19 |
19 * HOL: nat_less_induct renamed to less_induct; |
20 * HOL: the constant for f``x is now "image" rather than "op ``"; |
20 |
|
21 * HOL: systematic renaming of the SOME (Eps) rules, may use isatool |
|
22 fixsome to patch .thy and .ML sources automatically; |
|
23 |
|
24 select_equality -> some_equality |
|
25 select_eq_Ex -> some_eq_ex |
|
26 selectI2EX -> someI2_ex |
|
27 selectI2 -> someI2 |
|
28 selectI -> someI |
|
29 select1_equality -> some1_equality |
|
30 Eps_sym_eq -> some_sym_eq_trivial |
|
31 Eps_eq -> some_eq_trivial |
|
32 |
|
33 * HOL: exhaust_tac on datatypes superceded by new generic case_tac; |
|
34 |
|
35 * HOL: removed obsolete theorem binding expand_if (refer to split_if |
|
36 instead); |
|
37 |
|
38 * HOL: the recursion equations generated by 'recdef' are now called |
|
39 f.simps instead of f.rules; |
|
40 |
|
41 * HOL: qed_spec_mp now also handles bounded ALL as well; |
|
42 |
|
43 * HOL: 0 is now overloaded, so the type constraint ":: nat" may |
|
44 sometimes be needed; |
|
45 |
|
46 * HOL: the constant for "f``x" is now "image" rather than "op ``"; |
21 |
47 |
22 * HOL: the disjoint sum is now "<+>" instead of "Plus"; the cartesian |
48 * HOL: the disjoint sum is now "<+>" instead of "Plus"; the cartesian |
23 product is now "<*>" instead of "Times"; the lexicographic product is |
49 product is now "<*>" instead of "Times"; the lexicographic product is |
24 now "<*lex*>" instead of "**"; |
50 now "<*lex*>" instead of "**"; |
25 |
51 |
26 * HOL: exhaust_tac on datatypes superceded by new generic case_tac; |
52 * HOL: theory Sexp is now in HOL/Induct examples (it used to be part |
27 |
53 of main HOL, but was unused); better use HOL's datatype package; |
28 * HOL: simplification no longer dives into case-expressions; |
|
29 |
|
30 * HOL: the recursion equations generated by 'recdef' are now called |
|
31 f.simps instead of f.rules; |
|
32 |
|
33 * HOL: theory Sexp now in HOL/Induct examples (it used to be part of |
|
34 main HOL, but was unused); it is better to use HOL's datatype package |
|
35 anyway; |
|
36 |
|
37 * HOL: removed obsolete theorem binding expand_if (refer to split_if |
|
38 instead); |
|
39 |
|
40 * HOL: less_induct is renamed nat_less_induct |
|
41 |
|
42 * HOL: systematic renaming of the @-rules: |
|
43 selectI -> someI |
|
44 selectI2 -> someI2 |
|
45 selectI2EX -> someI2_ex |
|
46 select_equality -> some_equality |
|
47 select1_equality -> some1_equality |
|
48 select_eq_Ex -> some_eq_ex |
|
49 Eps_eq -> some_eq_trivial |
|
50 Eps_sym_eq -> some_sym_eq_trivial |
|
51 |
54 |
52 * HOL/Real: "rabs" replaced by overloaded "abs" function; |
55 * HOL/Real: "rabs" replaced by overloaded "abs" function; |
53 |
56 |
54 * HOL/ML: even fewer consts are declared as global (see theories Ord, |
57 * HOL/ML: even fewer consts are declared as global (see theories Ord, |
55 Lfp, Gfp, WF); this only affects ML packages that refer to const names |
58 Lfp, Gfp, WF); this only affects ML packages that refer to const names |
56 internally; |
59 internally; |
57 |
60 |
58 * HOL, ZF: syntax for quotienting wrt an equivalence relation changed |
61 * HOL and ZF: syntax for quotienting wrt an equivalence relation |
59 from A/r to A//r; |
62 changed from A/r to A//r; |
60 |
63 |
61 * HOL: qed_spec_mp now also removes bounded ALL; |
64 * ZF: new treatment of arithmetic (nat & int) may break some old |
62 |
65 proofs; |
63 * ZF: new treatment of arithmetic (nat & int) may break some old proofs; |
66 |
|
67 * Isar: renamed some attributes (RS -> THEN, simplify -> simplified, |
|
68 rulify -> rule_format, elimify -> elim_format, ...); |
64 |
69 |
65 * Isar/Provers: intro/elim/dest attributes changed; renamed |
70 * Isar/Provers: intro/elim/dest attributes changed; renamed |
66 intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one |
71 intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one |
67 should have to change intro!! to intro? only); replaced "delrule" by |
72 should have to change intro!! to intro? only); replaced "delrule" by |
68 "rule del"; |
73 "rule del"; |
69 |
74 |
70 * Isar: changed syntax of local blocks from {{ }} to { }; |
|
71 |
|
72 * Isar: renamed 'RS' attribute to 'THEN'; |
|
73 |
|
74 * Isar: renamed some attributes (rulify -> rule_format, elimify -> elim_format, ...); |
|
75 |
|
76 * Isar/HOL: renamed "intrs" to "intros" in inductive definitions; |
75 * Isar/HOL: renamed "intrs" to "intros" in inductive definitions; |
77 |
76 |
78 * Provers: strengthened force_tac by using new first_best_tac; |
77 * Provers: strengthened force_tac by using new first_best_tac; |
79 |
78 |
80 * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g. |
79 * LaTeX document preparation: several changes of isabelle.sty (see |
81 [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W |
80 lib/texinputs); |
82 use instead the strong form, |
|
83 [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W |
|
84 In HOL, FOL and ZF the function cla_make_elim will create such rules |
|
85 from destruct-rules; |
|
86 |
|
87 * Provers: safe_asm_full_simp_tac is no longer in the simplifier signature. Use |
|
88 val safe_asm_full_simp_tac = generic_simp_tac true (true,true,true); |
|
89 if required. |
|
90 |
|
91 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global |
|
92 timing flag supersedes proof_timing and Toplevel.trace; |
|
93 |
|
94 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well; |
|
95 |
|
96 * ML: PureThy.add_defs gets additional argument to indicate potential |
|
97 overloading (usually false); |
|
98 |
|
99 * LaTeX: several changes of isabelle.sty; |
|
100 |
81 |
101 |
82 |
102 *** Document preparation *** |
83 *** Document preparation *** |
103 |
84 |
104 * formal comments (text blocks etc.) in new-style theories may now |
85 * formal comments (text blocks etc.) in new-style theories may now |
112 * generated LaTeX sources are now deleted after successful run |
93 * generated LaTeX sources are now deleted after successful run |
113 (isatool document -c); may retain a copy somewhere else via -D option |
94 (isatool document -c); may retain a copy somewhere else via -D option |
114 of isatool usedir; |
95 of isatool usedir; |
115 |
96 |
116 * isatool usedir -D now lets isatool latex -o sty update the Isabelle |
97 * isatool usedir -D now lets isatool latex -o sty update the Isabelle |
117 style files, achieving self-contained LaTeX sources; |
98 style files, achieving self-contained LaTeX sources and simplifying |
|
99 LaTeX debugging; |
118 |
100 |
119 * old-style theories now produce (crude) LaTeX output as well; |
101 * old-style theories now produce (crude) LaTeX output as well; |
120 |
102 |
121 * browser info session directories are now self-contained (may be put |
103 * browser info session directories are now self-contained (may be put |
122 on WWW server seperately); improved graphs of nested sessions; removed |
104 on WWW server seperately); improved graphs of nested sessions; removed |
123 graph for 'all sessions'; |
105 graph for 'all sessions'; |
124 |
106 |
125 * several improvements in isabelle.sty; \isabellestyle{it} produces |
107 * several improvements in isabelle style files; \isabellestyle{it} |
126 near math mode output; \isamarkupheader is now \section by default; |
108 produces fake math mode output; \isamarkupheader is now \section by |
|
109 default; see lib/texinputs/isabelle.sty etc.; |
127 |
110 |
128 |
111 |
129 *** Isar *** |
112 *** Isar *** |
130 |
113 |
131 * Pure: local results and corresponding term bindings are now subject |
114 * Isar/Pure: local results and corresponding term bindings are now |
132 to Hindley-Milner polymorphism (similar to ML); this accommodates |
115 subject to Hindley-Milner polymorphism (similar to ML); this |
133 incremental type-inference nicely; |
116 accommodates incremental type-inference very nicely; |
134 |
117 |
135 * Pure: new derived language element 'obtain' supports generalized |
118 * Isar/Pure: new derived language element 'obtain' supports |
136 existence reasoning; |
119 generalized existence reasoning; |
137 |
120 |
138 * Pure: new calculational elements 'moreover' and 'ultimately' support |
121 * Isar/Pure: new calculational elements 'moreover' and 'ultimately' |
139 accumulation of results, without applying any rules yet; |
122 support accumulation of results, without applying any rules yet; |
140 |
123 useful to collect intermediate results without explicit name |
141 * Pure: scalable support for case-analysis type proofs: new 'case' |
124 references, and for use with transitivity rules with more than 2 |
142 language element refers to local contexts symbolically, as produced by |
125 premises; |
143 certain proof methods; internally, case names are attached to theorems |
126 |
144 as "tags"; |
127 * Isar/Pure: scalable support for case-analysis type proofs: new |
145 |
128 'case' language element refers to local contexts symbolically, as |
146 * Pure: theory command 'hide' removes declarations from |
129 produced by certain proof methods; internally, case names are attached |
|
130 to theorems as "tags"; |
|
131 |
|
132 * Isar/Pure: theory command 'hide' removes declarations from |
147 class/type/const name spaces; |
133 class/type/const name spaces; |
148 |
134 |
149 * Pure: theory command 'defs' supports option "(overloaded)" to |
135 * Isar/Pure: theory command 'defs' supports option "(overloaded)" to |
150 indicate potential overloading; |
136 indicate potential overloading; |
151 |
137 |
152 * Pure: changed syntax of local blocks from {{ }} to { }; |
138 * Isar/Pure: changed syntax of local blocks from {{ }} to { }; |
153 |
139 |
154 * Pure: renamed 'RS' attribute to 'THEN'; |
140 * Isar/Pure: syntax of sorts made 'inner', i.e. have to write |
155 |
141 "{a,b,c}" instead of {a,b,c}; |
156 * Pure: syntax of sorts made 'inner', i.e. have to write "{a, b, c}" |
142 |
157 instead of {a, b, c}; |
143 * Isar/Pure now provides its own version of intro/elim/dest |
158 |
144 attributes; useful for building new logics, but beware of confusion |
159 * Pure now provides its own version of intro/elim/dest attributes; |
145 with the version in Provers/classical; |
160 useful for building new logics, but beware of confusion with the |
146 |
161 version in Provers/classical; |
147 * Isar/Pure: the local context of (non-atomic) goals is provided via |
162 |
148 case name 'antecedent'; |
163 * Pure: the local context of (non-atomic) goals is provided via case |
149 |
164 name 'antecedent'; |
150 * Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms |
165 |
151 to the current context is now done automatically); |
166 * Pure: removed obsolete 'transfer' attribute (transfer of thms to the |
152 |
167 current context is now done automatically); |
153 * Isar/Pure: theory command 'method_setup' provides a simple interface |
168 |
154 for definining proof methods in ML; |
169 * Pure: theory command 'method_setup' provides a simple interface for |
155 |
170 definining proof methods in ML; |
156 * Isar/Provers: intro/elim/dest attributes changed; renamed |
171 |
|
172 * Provers: 'simp' method now supports 'cong' modifiers; |
|
173 |
|
174 * Provers: hypsubst support; also plain subst and symmetric attribute |
|
175 (the latter supercedes [RS sym]); |
|
176 |
|
177 * Provers: splitter support (via 'split' attribute and 'simp' method |
|
178 modifier); 'simp' method: 'only:' modifier removes loopers as well |
|
179 (including splits); |
|
180 |
|
181 * Provers: added 'fastsimp' and 'clarsimp' methods (combination of |
|
182 Simplifier and Classical reasoner); |
|
183 |
|
184 * Provers: added 'arith_split' attribute; |
|
185 |
|
186 * HOL: new proof method 'cases' and improved version of 'induct' now |
|
187 support named cases; major packages (inductive, datatype, primrec, |
|
188 recdef) support case names and properly name parameters; |
|
189 |
|
190 * HOL: removed 'case_split' thm binding, should use 'cases' proof |
|
191 method anyway; |
|
192 |
|
193 * HOL: removed obsolete expand_if = split_if; theorems if_splits = |
|
194 split_if split_if_asm; datatype package provides theorems foo.splits = |
|
195 foo.split foo.split_asm for each datatype; |
|
196 |
|
197 * HOL/Calculation: new rules for substitution in inequalities |
|
198 (monotonicity conditions are extracted to be proven at end); |
|
199 |
|
200 * HOL/inductive: rename "intrs" to "intros" (potential |
|
201 INCOMPATIBILITY); emulation of mk_cases feature for proof scripts: |
|
202 'inductive_cases' command and 'ind_cases' method; NOTE: use (cases |
|
203 (simplified)) method in proper proofs; |
|
204 |
|
205 * Provers: intro/elim/dest attributes changed; renamed |
|
206 intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in |
157 intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in |
207 most cases, one should have to change intro!! to intro? only); |
158 most cases, one should have to change intro!! to intro? only); |
208 replaced "delrule" by "rule del"; |
159 replaced "delrule" by "rule del"; |
209 |
160 |
210 * names of theorems etc. may be natural numbers as well; |
161 * Isar/Provers: new 'hypsubst' method, plain 'subst' method and |
211 |
162 'symmetric' attribute (the latter supercedes [RS sym]); |
212 * 'pr' command: optional arguments for goals_limit and |
163 |
|
164 * Isar/Provers: splitter support (via 'split' attribute and 'simp' |
|
165 method modifier); 'simp' method: 'only:' modifier removes loopers as |
|
166 well (including splits); |
|
167 |
|
168 * Isar/Provers: Simplifier and Classical methods now support all kind |
|
169 of modifiers used in the past, including 'cong', 'iff', etc. |
|
170 |
|
171 * Isar/Provers: added 'fastsimp' and 'clarsimp' methods (combination |
|
172 of Simplifier and Classical reasoner); |
|
173 |
|
174 * Isar/HOL: new proof method 'cases' and improved version of 'induct' |
|
175 now support named cases; major packages (inductive, datatype, primrec, |
|
176 recdef) support case names and properly name parameters; |
|
177 |
|
178 * Isar/HOL: new transitivity rules for substitution in inequalities -- |
|
179 monotonicity conditions are extracted to be proven at end of |
|
180 calculations; |
|
181 |
|
182 * Isar/HOL: removed 'case_split' thm binding, should use 'cases' proof |
|
183 method anyway; |
|
184 |
|
185 * Isar/HOL: removed old expand_if = split_if; theorems if_splits = |
|
186 split_if split_if_asm; datatype package provides theorems foo.splits = |
|
187 foo.split foo.split_asm for each datatype; |
|
188 |
|
189 * Isar/HOL: tuned inductive package, rename "intrs" to "intros" |
|
190 (potential INCOMPATIBILITY), emulation of mk_cases feature for proof |
|
191 scripts: new 'inductive_cases' command and 'ind_cases' method; (Note: |
|
192 use "(cases (simplified))" method in proper proof texts); |
|
193 |
|
194 * Isar/HOL: added global 'arith_split' attribute for 'arith' method; |
|
195 |
|
196 * Isar: names of theorems etc. may be natural numbers as well; |
|
197 |
|
198 * Isar: 'pr' command: optional arguments for goals_limit and |
213 ProofContext.prems_limit; no longer prints theory contexts, but only |
199 ProofContext.prems_limit; no longer prints theory contexts, but only |
214 proof states; |
200 proof states; |
215 |
201 |
216 * diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit |
202 * Isar: diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit |
217 additional print modes to be specified; e.g. "pr(latex)" will print |
203 additional print modes to be specified; e.g. "pr(latex)" will print |
218 proof state according to the Isabelle LaTeX style; |
204 proof state according to the Isabelle LaTeX style; |
219 |
205 |
220 * improved support for emulating tactic scripts, including proof |
206 * Isar: improved support for emulating tactic scripts, including proof |
221 methods 'rule_tac' etc., 'cut_tac', 'thin_tac', 'subgoal_tac', |
207 methods 'rule_tac' etc., 'cut_tac', 'thin_tac', 'subgoal_tac', |
222 'rename_tac', 'rotate_tac', 'tactic', and 'case_tac' / 'induct_tac' |
208 'rename_tac', 'rotate_tac', 'tactic', and 'case_tac' / 'induct_tac' |
223 (for HOL datatypes); |
209 (for HOL datatypes); |
224 |
210 |
225 * simplified (more robust) goal selection of proof methods: 1st goal, |
211 * Isar: simplified (more robust) goal selection of proof methods: 1st |
226 all goals, or explicit goal specifier (tactic emulation); thus 'proof |
212 goal, all goals, or explicit goal specifier (tactic emulation); thus |
227 method scripts' have to be in depth-first order; |
213 'proof method scripts' have to be in depth-first order; |
228 |
214 |
229 * tuned 'let' syntax: replaced 'as' keyword by 'and'; |
215 * Isar: tuned 'let' syntax: replaced 'as' keyword by 'and'; |
230 |
216 |
231 * removed 'help' command, which hasn't been too helpful anyway; should |
217 * Isar: removed 'help' command, which hasn't been too helpful anyway; |
232 instead use individual commands for printing items (print_commands, |
218 should instead use individual commands for printing items |
233 print_methods etc.); |
219 (print_commands, print_methods etc.); |
234 |
220 |
235 * added 'nothing' --- the empty list of theorems; |
221 * Isar: added 'nothing' --- the empty list of theorems; |
236 |
222 |
237 |
223 |
238 *** HOL *** |
224 *** HOL *** |
239 |
|
240 * HOL/Lambda: converted into new-style theory and document; |
|
241 |
225 |
242 * HOL/Algebra: new theory of rings and univariate polynomials, by |
226 * HOL/Algebra: new theory of rings and univariate polynomials, by |
243 Clemens Ballarin; |
227 Clemens Ballarin; |
244 |
228 |
245 * HOL/ex: new theory Factorization proving the Fundamental Theorem of |
229 * HOL/NumberTheory: Fundamental Theorem of Arithmetic, Chinese |
246 Arithmetic, by Thomas M Rasmussen; |
230 Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M |
247 |
231 Rasmussen; |
248 * HOL/ex/Multiquote: multiple nested quotations and anti-quotations -- |
232 |
249 basically a generalized version of de-Bruijn representation; very |
233 * HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David |
250 useful in avoiding lifting of operations; |
234 von Oheimb; |
251 |
235 |
252 * HOL/NumberTheory: Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's |
236 * HOL/Lambda: converted into new-style theory and document; |
253 Theorem, by Thomas M Rasmussen; |
237 |
254 |
238 * HOL/ex/Multiquote: example of multiple nested quotations and |
255 * HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog; |
239 anti-quotations -- basically a generalized version of de-Bruijn |
256 |
240 representation; very useful in avoiding lifting of operations; |
257 * HOL/Real: "rabs" replaced by overloaded "abs" function; |
|
258 |
241 |
259 * HOL/record: added general record equality rule to simpset; fixed |
242 * HOL/record: added general record equality rule to simpset; fixed |
260 select-update simplification procedure to handle extended records as |
243 select-update simplification procedure to handle extended records as |
261 well; admit "r" as field name; |
244 well; admit "r" as field name; |
262 |
245 |
264 other numeric types and also as the identity of groups, rings, etc.; |
247 other numeric types and also as the identity of groups, rings, etc.; |
265 |
248 |
266 * HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity. |
249 * HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity. |
267 Types nat and int belong to this axclass; |
250 Types nat and int belong to this axclass; |
268 |
251 |
269 * greatly improved simplification involving numerals of type nat, int, real: |
252 * HOL: greatly improved simplification involving numerals of type nat, int, real: |
270 (i + #8 + j) = Suc k simplifies to #7 + (i + j) = k |
253 (i + #8 + j) = Suc k simplifies to #7 + (i + j) = k |
271 i*j + k + j*#3*i simplifies to #4*(i*j) + k |
254 i*j + k + j*#3*i simplifies to #4*(i*j) + k |
272 two terms #m*u and #n*u are replaced by #(m+n)*u |
255 two terms #m*u and #n*u are replaced by #(m+n)*u |
273 (where #m, #n and u can implicitly be 1; this is simproc combine_numerals) |
256 (where #m, #n and u can implicitly be 1; this is simproc combine_numerals) |
274 and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y |
257 and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y |
275 or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals); |
258 or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals); |
276 |
259 |
277 * HOL: meson_tac is available (previously in ex/meson.ML). It is a powerful |
260 * HOL: meson_tac is available (previously in ex/meson.ML); it is a |
278 prover for predicate logic but knows nothing of clasets. For examples of |
261 powerful prover for predicate logic but knows nothing of clasets; see |
279 what it can do, see ex/mesontest.ML and ex/mesontest2.ML; |
262 ex/mesontest.ML and ex/mesontest2.ML for example applications; |
280 |
263 |
281 * HOL: new version of "case_tac" subsumes both boolean case split and |
264 * HOL: new version of "case_tac" subsumes both boolean case split and |
282 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer |
265 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer |
283 exists, may define val exhaust_tac = case_tac for ad-hoc portability; |
266 exists, may define val exhaust_tac = case_tac for ad-hoc portability; |
284 |
267 |
285 * HOL: simplification no longer dives into case-expressions: only the |
268 * HOL: simplification no longer dives into case-expressions: only the |
286 selector expression is simplified, but not the remaining arms. To |
269 selector expression is simplified, but not the remaining arms. To |
287 enable full simplification of case-expressions for datatype t, you |
270 enable full simplification of case-expressions for datatype t, you |
288 need to remove t.weak_case_cong from the simpset, either permanently |
271 need to remove t.weak_case_cong from the simpset, either permanently |
289 (Delcongs[thm"t.weak_case_cong"];) or locally (delcongs [...]). |
272 (Delcongs [thm"t.weak_case_cong"];) or locally (delcongs [...]). |
290 |
273 |
291 * HOL/recdef: the recursion equations generated by 'recdef' for |
274 * HOL/recdef: the recursion equations generated by 'recdef' for |
292 function 'f' are now called f.simps instead of f.rules; if all |
275 function 'f' are now called f.simps instead of f.rules; if all |
293 termination conditions are proved automatically, these simplification |
276 termination conditions are proved automatically, these simplification |
294 rules are added to the simpset, as in primrec; rules may be named |
277 rules are added to the simpset, as in primrec; rules may be named |
298 * HOL/While is a new theory that provides a while-combinator. It |
281 * HOL/While is a new theory that provides a while-combinator. It |
299 permits the definition of tail-recursive functions without the |
282 permits the definition of tail-recursive functions without the |
300 provision of a termination measure. The latter is necessary once the |
283 provision of a termination measure. The latter is necessary once the |
301 invariant proof rule for while is applied. |
284 invariant proof rule for while is applied. |
302 |
285 |
303 * HOL: new (overloaded) notation for the set of elements below/above some |
286 * HOL: new (overloaded) notation for the set of elements below/above |
304 element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval. |
287 some element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval. |
305 |
288 |
306 * HOL: theorems impI, allI, ballI bound as "strip"; |
289 * HOL: theorems impI, allI, ballI bound as "strip"; |
307 |
290 |
308 * new tactic induct_thm_tac: thm -> string -> int -> tactic |
291 * HOL: new tactic induct_thm_tac: thm -> string -> int -> tactic |
309 induct_tac th "x1 ... xn" expects th to have a conclusion of the form |
292 induct_tac th "x1 ... xn" expects th to have a conclusion of the form |
310 P v1 ... vn and abbreviates res_inst_tac [("v1","x1"),...,("vn","xn")] th; |
293 P v1 ... vn and abbreviates res_inst_tac [("v1","x1"),...,("vn","xn")] th; |
311 |
294 |
312 * new functions rulify/rulify_no_asm: thm -> thm for turning outer |
295 * HOL/Real: "rabs" replaced by overloaded "abs" function; |
313 -->/All/Ball into ==>/!!; qed_spec_mp now uses rulify_no_asm; |
296 |
314 |
297 * HOL: theory Sexp now in HOL/Induct examples (it used to be part of |
315 * theory Sexp now in HOL/Induct examples (it used to be part of main |
298 main HOL, but was unused); |
316 HOL, but was unused); |
299 |
317 |
300 * HOL: fewer consts declared as global (e.g. have to refer to |
318 * fewer consts declared as global (e.g. have to refer to "Lfp.lfp" |
301 "Lfp.lfp" instead of "lfp" internally; affects ML packages only); |
319 instead of "lfp" internally; affects ML packages only); |
302 |
320 |
303 * HOL: tuned AST representation of nested pairs, avoiding bogus output |
321 * tuned AST representation of nested pairs, avoiding bogus output in |
304 in case of overlap with user translations (e.g. judgements over |
322 case of overlap with user translations (e.g. judgements over tuples); |
305 tuples); (note that the underlying logical represenation is still |
|
306 bogus); |
323 |
307 |
324 |
308 |
325 *** ZF *** |
309 *** ZF *** |
326 |
310 |
327 * simplification automatically cancels common terms in arithmetic expressions |
311 * ZF: simplification automatically cancels common terms in arithmetic |
328 over nat and int; |
312 expressions over nat and int; |
329 |
313 |
330 * new treatment of nat to minimize type-checking: all operators coerce their |
314 * ZF: new treatment of nat to minimize type-checking: all operators |
331 operands to a natural number using the function natify, making the algebraic |
315 coerce their operands to a natural number using the function natify, |
332 laws unconditional; |
316 making the algebraic laws unconditional; |
333 |
317 |
334 * as above, for int: operators coerce their operands to an integer using the |
318 * ZF: as above, for int: operators coerce their operands to an integer |
335 function intify; |
319 using the function intify; |
336 |
320 |
337 * the integer library now contains many of the usual laws for the orderings, |
321 * ZF: the integer library now contains many of the usual laws for the |
338 including $<=, and monotonicity laws for $+ and $*; |
322 orderings, including $<=, and monotonicity laws for $+ and $*; |
339 |
323 |
340 * new example ZF/ex/NatSum to demonstrate integer arithmetic simplification; |
324 * ZF: new example ZF/ex/NatSum to demonstrate integer arithmetic |
341 |
325 simplification; |
342 *** FOL & ZF *** |
326 |
343 |
327 * FOL and ZF: AddIffs now available, giving theorems of the form P<->Q |
344 * AddIffs now available, giving theorems of the form P<->Q to the |
328 to the simplifier and classical reasoner simultaneously; |
345 simplifier and classical reasoner simultaneously; |
|
346 |
329 |
347 |
330 |
348 *** General *** |
331 *** General *** |
|
332 |
|
333 * Provers: blast_tac now handles actual object-logic rules as |
|
334 assumptions; note that auto_tac uses blast_tac internally as well; |
|
335 |
|
336 * Provers: new functions rulify/rulify_no_asm: thm -> thm for turning |
|
337 outer -->/All/Ball into ==>/!!; qed_spec_mp now uses rulify_no_asm; |
349 |
338 |
350 * Provers: delrules now handles destruct rules as well (no longer need |
339 * Provers: delrules now handles destruct rules as well (no longer need |
351 explicit make_elim); |
340 explicit make_elim); |
352 |
341 |
353 * Provers: blast(_tac) now handles actual object-logic rules as |
342 * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g. |
354 assumptions; note that auto(_tac) uses blast(_tac) internally as well; |
343 [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W |
|
344 use instead the strong form, |
|
345 [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W |
|
346 in HOL, FOL and ZF the function cla_make_elim will create such rules |
|
347 from destruct-rules; |
355 |
348 |
356 * Provers: Simplifier.easy_setup provides a fast path to basic |
349 * Provers: Simplifier.easy_setup provides a fast path to basic |
357 Simplifier setup for new object-logics; |
350 Simplifier setup for new object-logics; |
358 |
351 |
359 * Pure: AST translation rules no longer require constant head on LHS; |
352 * Pure: AST translation rules no longer require constant head on LHS; |
360 |
353 |
361 * Pure: improved name spaces: ambiguous output is qualified; support |
354 * Pure: improved name spaces: ambiguous output is qualified; support |
362 for hiding of names; |
355 for hiding of names; |
|
356 |
|
357 * system: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, and |
|
358 XSYMBOL_HOME; no longer need to do manual configuration in most |
|
359 situations; |
363 |
360 |
364 * system: compression of ML heaps images may now be controlled via -c |
361 * system: compression of ML heaps images may now be controlled via -c |
365 option of isabelle and isatool usedir (currently only observed by |
362 option of isabelle and isatool usedir (currently only observed by |
366 Poly/ML); |
363 Poly/ML); |
367 |
364 |
368 * system: isatool installfonts may handle X-Symbol fonts as well (very |
365 * system: isatool installfonts may handle X-Symbol fonts as well (very |
369 useful for remote X11); |
366 useful for remote X11); |
370 |
367 |
371 * system: provide TAGS file for Isabelle sources; |
368 * system: provide TAGS file for Isabelle sources; |
372 |
369 |
373 * settings: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, and |
|
374 XSYMBOL_HOME; no longer need to do manual configuration in most |
|
375 situations; |
|
376 |
|
377 * ML: infix 'OF' is a version of 'MRS' with more appropriate argument |
370 * ML: infix 'OF' is a version of 'MRS' with more appropriate argument |
378 order; |
371 order; |
379 |
372 |
380 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global |
373 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global |
381 timing flag supersedes proof_timing and Toplevel.trace; |
374 timing flag supersedes proof_timing and Toplevel.trace; |
382 |
375 |
|
376 * ML: new combinators |>> and |>>> for incremental transformations |
|
377 with secondary results (e.g. certain theory extensions): |
|
378 |
383 * ML: PureThy.add_defs gets additional argument to indicate potential |
379 * ML: PureThy.add_defs gets additional argument to indicate potential |
384 overloading (usually false); |
380 overloading (usually false); |
385 |
381 |
386 * ML: new combinators |>> and |>>> for incremental transformations |
382 * ML: PureThy.add_thms/add_axioms/add_defs now return theorems as |
387 with secondary results (e.g. certain theory extensions): |
383 results; |
388 |
384 |
389 |
385 |
390 |
386 |
391 New in Isabelle99 (October 1999) |
387 New in Isabelle99 (October 1999) |
392 -------------------------------- |
388 -------------------------------- |