summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Mon, 07 Aug 2000 10:25:12 +0200 | |

changeset 9542 | fa19ffdbe1de |

parent 9541 | d17c0b34d5c8 |

child 9543 | ce61d1c1a509 |

ZF arith

--- a/NEWS Sun Aug 06 15:26:53 2000 +0200 +++ b/NEWS Mon Aug 07 10:25:12 2000 +0200 @@ -46,6 +46,8 @@ * HOL, ZF: syntax for quotienting wrt an equivalence relation changed from A/r to A//r; +* ZF: new treatment of arithmetic (nat & int) may break some old proofs; + * Isar/Provers: intro/elim/dest attributes: changed intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one should have to change intro!! to intro? only); @@ -194,14 +196,9 @@ *** HOL *** -* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog; - * HOL/Algebra: new theory of rings and univariate polynomials, by Clemens Ballarin; -* HOL/record: fixed select-update simplification procedure to handle -extended records as well; admit "r" as field name; - * HOL/ex: new theory Factorization proving the Fundamental Theorem of Arithmetic, by Thomas M Rasmussen; @@ -209,8 +206,16 @@ basically a generalized version of de-Bruijn representation; very useful in avoiding lifting of operations; +* HOL/NumberTheory: Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's +Theorem, by Thomas M Rasmussen; + +* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog; + * HOL/Real: "rabs" replaced by overloaded "abs" function; +* HOL/record: fixed select-update simplification procedure to handle +extended records as well; admit "r" as field name; + * HOL: 0 is now overloaded over the new sort "zero", allowing its use with other numeric types and also as the identity of groups, rings, etc.; @@ -262,6 +267,20 @@ case of overlap with user translations (e.g. judgements over tuples); +*** ZF *** + +* simplification automatically cancels common terms in arithmetic expressions over nat; + +* new treatment of nat to minimize type-checking: all operators coerce their +operands to a natural number using the function natify, making the algebraic +laws unconditional; + +* as above, for int; + +* the integer library now contains many of the usual laws for the orderings, +including $<=; + + *** FOL & ZF *** * AddIffs now available, giving theorems of the form P<->Q to the