summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

author | nipkow |

Mon Aug 04 11:50:35 1997 +0200 (1997-08-04) | |

changeset 3586 | 2ee1ed79c802 |

parent 3580 | 04c6ae944b5e |

child 3658 | f87dd7b68d8c |

permissions | -rw-r--r-- |

Added a take/dropWhile lemma.

2 Isabelle NEWS -- history of user-visible changes

3 ================================================

5 New in Isabelle???? (DATE ????)

6 -------------------------------

8 * HOL/simplifier: terms of the form

9 `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)

10 are rewritten to

11 `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)'

13 * HOL/Lists: the function "set_of_list" has been renamed "set"

15 * removed old README and Makefiles;

17 * removed obsolete init_pps and init_database;

19 * defs may now be conditional; improved rewrite_goals_tac to handle

20 conditional equations;

22 * improved output of warnings / errors;

24 * deleted the obsolete tactical STATE, which was declared by:

25 fun STATE tacfun st = tacfun st st;

27 * added simplification meta rules:

28 (asm_)(full_)simplify: simpset -> thm -> thm;

30 * simplifier.ML no longer part of Pure -- has to be loaded by object

31 logics (again);

33 * added prems argument to simplification procedures;

37 New in Isabelle94-8 (May 1997)

38 ------------------------------

40 *** General Changes ***

42 * new utilities to build / run / maintain Isabelle etc. (in parts

43 still somewhat experimental); old Makefiles etc. still functional;

45 * new 'Isabelle System Manual';

47 * INSTALL text, together with ./configure and ./build scripts;

49 * reimplemented type inference for greater efficiency, better error

50 messages and clean internal interface;

52 * prlim command for dealing with lots of subgoals (an easier way of

53 setting goals_limit);

56 *** Syntax ***

58 * supports alternative (named) syntax tables (parser and pretty

59 printer); internal interface is provided by add_modesyntax(_i);

61 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to

62 be used in conjunction with the Isabelle symbol font; uses the

63 "symbols" syntax table;

65 * added token_translation interface (may translate name tokens in

66 arbitrary ways, dependent on their type (free, bound, tfree, ...) and

67 the current print_mode); IMPORTANT: user print translation functions

68 are responsible for marking newly introduced bounds

69 (Syntax.mark_boundT);

71 * token translations for modes "xterm" and "xterm_color" that display

72 names in bold, underline etc. or colors (which requires a color

73 version of xterm);

75 * infixes may now be declared with names independent of their syntax;

77 * added typed_print_translation (like print_translation, but may

78 access type of constant);

81 *** Classical Reasoner ***

83 Blast_tac: a new tactic! It is often more powerful than fast_tac, but has

84 some limitations. Blast_tac...

85 + ignores addss, addbefore, addafter; this restriction is intrinsic

86 + ignores elimination rules that don't have the correct format

87 (the conclusion MUST be a formula variable)

88 + ignores types, which can make HOL proofs fail

89 + rules must not require higher-order unification, e.g. apply_type in ZF

90 [message "Function Var's argument not a bound variable" relates to this]

91 + its proof strategy is more general but can actually be slower

93 * substitution with equality assumptions no longer permutes other

94 assumptions;

96 * minor changes in semantics of addafter (now called addaltern); renamed

97 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper

98 (and access functions for it);

100 * improved combination of classical reasoner and simplifier:

101 + functions for handling clasimpsets

102 + improvement of addss: now the simplifier is called _after_ the

103 safe steps.

104 + safe variant of addss called addSss: uses safe simplifications

105 _during_ the safe steps. It is more complete as it allows multiple

106 instantiations of unknowns (e.g. with slow_tac).

108 *** Simplifier ***

110 * added interface for simplification procedures (functions that

111 produce *proven* rewrite rules on the fly, depending on current

112 redex);

114 * ordering on terms as parameter (used for ordered rewriting);

116 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss;

118 * the solver is now split into a safe and an unsafe part.

119 This should be invisible for the normal user, except that the

120 functions setsolver and addsolver have been renamed to setSolver and

121 addSolver; added safe_asm_full_simp_tac;

124 *** HOL ***

126 * a generic induction tactic `induct_tac' which works for all datatypes and

127 also for type `nat';

129 * a generic case distinction tactic `exhaust_tac' which works for all

130 datatypes and also for type `nat';

132 * each datatype comes with a function `size';

134 * patterns in case expressions allow tuple patterns as arguments to

135 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';

137 * primrec now also works with type nat;

139 * recdef: a new declaration form, allows general recursive functions to be

140 defined in theory files. See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify.

142 * the constant for negation has been renamed from "not" to "Not" to

143 harmonize with FOL, ZF, LK, etc.;

145 * HOL/ex/LFilter theory of a corecursive "filter" functional for

146 infinite lists;

148 * HOL/Modelcheck demonstrates invocation of model checker oracle;

150 * HOL/ex/Ring.thy declares cring_simp, which solves equational

151 problems in commutative rings, using axiomatic type classes for + and *;

153 * more examples in HOL/MiniML and HOL/Auth;

155 * more default rewrite rules for quantifiers, union/intersection;

157 * a new constant `arbitrary == @x.False';

159 * HOLCF/IOA replaces old HOL/IOA;

161 * HOLCF changes: derived all rules and arities

162 + axiomatic type classes instead of classes

163 + typedef instead of faking type definitions

164 + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.

165 + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po

166 + eliminated the types void, one, tr

167 + use unit lift and bool lift (with translations) instead of one and tr

168 + eliminated blift from Lift3.thy (use Def instead of blift)

169 all eliminated rules are derived as theorems --> no visible changes ;

172 *** ZF ***

174 * ZF now has Fast_tac, Simp_tac and Auto_tac. Union_iff is a now a default

175 rewrite rule; this may affect some proofs. eq_cs is gone but can be put back

176 as ZF_cs addSIs [equalityI];

180 New in Isabelle94-7 (November 96)

181 ---------------------------------

183 * allowing negative levels (as offsets) in prlev and choplev;

185 * super-linear speedup for large simplifications;

187 * FOL, ZF and HOL now use miniscoping: rewriting pushes

188 quantifications in as far as possible (COULD MAKE EXISTING PROOFS

189 FAIL); can suppress it using the command Delsimps (ex_simps @

190 all_simps); De Morgan laws are also now included, by default;

192 * improved printing of ==> : ~:

194 * new object-logic "Sequents" adds linear logic, while replacing LK

195 and Modal (thanks to Sara Kalvala);

197 * HOL/Auth: correctness proofs for authentication protocols;

199 * HOL: new auto_tac combines rewriting and classical reasoning (many

200 examples on HOL/Auth);

202 * HOL: new command AddIffs for declaring theorems of the form P=Q to

203 the rewriter and classical reasoner simultaneously;

205 * function uresult no longer returns theorems in "standard" format;

206 regain previous version by: val uresult = standard o uresult;

210 New in Isabelle94-6

211 -------------------

213 * oracles -- these establish an interface between Isabelle and trusted

214 external reasoners, which may deliver results as theorems;

216 * proof objects (in particular record all uses of oracles);

218 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;

220 * "constdefs" section in theory files;

222 * "primrec" section (HOL) no longer requires names;

224 * internal type "tactic" now simply "thm -> thm Sequence.seq";

228 New in Isabelle94-5

229 -------------------

231 * reduced space requirements;

233 * automatic HTML generation from theories;

235 * theory files no longer require "..." (quotes) around most types;

237 * new examples, including two proofs of the Church-Rosser theorem;

239 * non-curried (1994) version of HOL is no longer distributed;

243 New in Isabelle94-4

244 -------------------

246 * greatly reduced space requirements;

248 * theory files (.thy) no longer require \...\ escapes at line breaks;

250 * searchable theorem database (see the section "Retrieving theorems" on

251 page 8 of the Reference Manual);

253 * new examples, including Grabczewski's monumental case study of the

254 Axiom of Choice;

256 * The previous version of HOL renamed to Old_HOL;

258 * The new version of HOL (previously called CHOL) uses a curried syntax

259 for functions. Application looks like f a b instead of f(a,b);

261 * Mutually recursive inductive definitions finally work in HOL;

263 * In ZF, pattern-matching on tuples is now available in all abstractions and

264 translates to the operator "split";

268 New in Isabelle94-3

269 -------------------

271 * new infix operator, addss, allowing the classical reasoner to

272 perform simplification at each step of its search. Example:

273 fast_tac (cs addss ss)

275 * a new logic, CHOL, the same as HOL, but with a curried syntax

276 for functions. Application looks like f a b instead of f(a,b). Also pairs

277 look like (a,b) instead of <a,b>;

279 * PLEASE NOTE: CHOL will eventually replace HOL!

281 * In CHOL, pattern-matching on tuples is now available in all abstractions.

282 It translates to the operator "split". A new theory of integers is available;

284 * In ZF, integer numerals now denote two's-complement binary integers.

285 Arithmetic operations can be performed by rewriting. See ZF/ex/Bin.ML;

287 * Many new examples: I/O automata, Church-Rosser theorem, equivalents

288 of the Axiom of Choice;

292 New in Isabelle94-2

293 -------------------

295 * Significantly faster resolution;

297 * the different sections in a .thy file can now be mixed and repeated

298 freely;

300 * Database of theorems for FOL, HOL and ZF. New

301 commands including qed, qed_goal and bind_thm store theorems in the database.

303 * Simple database queries: return a named theorem (get_thm) or all theorems of

304 a given theory (thms_of), or find out what theory a theorem was proved in

305 (theory_of_thm);

307 * Bugs fixed in the inductive definition and datatype packages;

309 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs

310 and HOL_dup_cs obsolete;

312 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1

313 have been removed;

315 * Simpler definition of function space in ZF;

317 * new results about cardinal and ordinal arithmetic in ZF;

319 * 'subtype' facility in HOL for introducing new types as subsets of existing

320 types;

323 $Id$