# HG changeset patch # User wenzelm # Date 901811214 -7200 # Node ID 3ecd7c9523968f0290d99a071070ee14b2ecc9dd # Parent f0a66af5f2cb24c0d14f1822d52ee9fb03638ae0 tuned; diff -r f0a66af5f2cb -r 3ecd7c952396 NEWS --- a/NEWS Thu Jul 30 15:56:21 1998 +0200 +++ b/NEWS Thu Jul 30 17:06:54 1998 +0200 @@ -7,32 +7,12 @@ *** Overview of INCOMPATIBILITIES (see below for more details) *** -* several changes of proof tools (see next section); +* several changes of proof tools; -* HOL/datatype: - - Theories using datatypes must now have Datatype.thy as an - ancestor. - - The specific .induct_tac no longer exists - use the - generic induct_tac instead. - - natE has been renamed to nat.exhaustion - use exhaust_tac - instead of res_inst_tac ... natE. Note that the variable - names in nat.exhaustion differ from the names in natE, this - may cause some "fragile" proofs to fail. - - the theorems split__case and split__case_asm - have been renamed to .split and .split_asm. - - Since default sorts are no longer ignored by the package, - some datatype definitions may have to be annotated with - explicit sort constraints. - - Primrec definitions no longer require function name and type - of recursive argument. - Use isatool fixdatatype to adapt your theories and proof scripts - to the new package (as usual, backup your sources first!). +* HOL: major changes to the inductive and datatype packages; -* HOL/inductive requires Inductive.thy as an ancestor; `inj_onto' is -now called `inj_on' (which makes more sense); - -* HOL/Relation: renamed the relational operator r^-1 to 'converse' -from 'inverse' (for compatibility with ZF and some literature); +* HOL: renamed r^-1 to 'converse' from 'inverse'; `inj_onto' is now +called `inj_on'; *** Proof tools *** @@ -91,14 +71,14 @@ *** General *** -* new toplevel commands `Goal' and `Goalw' that improve upon `goal' +* new top-level commands `Goal' and `Goalw' that improve upon `goal' and `goalw': the theory is no longer needed as an explicit argument - the current theory context is used; assumptions are no longer returned at the ML-level unless one of them starts with ==> or !!; it is -recommended to convert to these new commands using isatool fixgoal (as -usual, backup your sources first!); +recommended to convert to these new commands using isatool fixgoal +(backup your sources first!); -* new toplevel commands 'thm' and 'thms' for retrieving theorems from +* new top-level commands 'thm' and 'thms' for retrieving theorems from the current theory context, and 'theory' to lookup stored theories; * new theory section 'nonterminals' for purely syntactic types; @@ -112,32 +92,74 @@ *** HOL *** -* HOL/datatype package reorganized and improved: now supports mutually - recursive datatypes such as +* HOL/inductive package reorganized and improved: now supports mutual +definitions such as: + + inductive EVEN ODD + intrs + null "0 : EVEN" + oddI "n : EVEN ==> Suc n : ODD" + evenI "n : ODD ==> Suc n : EVEN" + +new theorem list "elims" contains an elimination rule for each of the +recursive sets; inductive definitions now handle disjunctive premises +correctly (also ZF); - datatype - 'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp) - | SUM ('a aexp) ('a aexp) - | DIFF ('a aexp) ('a aexp) - | NUM 'a - and - 'a bexp = LESS ('a aexp) ('a aexp) - | AND ('a bexp) ('a bexp) - | OR ('a bexp) ('a bexp) +INCOMPATIBILITIES: requires Inductive as an ancestor; component +"mutual_induct" no longer exists - the induction rule is always +contained in "induct"; + + +* HOL/datatype package re-implemented and greatly improved: now +supports mutually recursive datatypes such as: + + datatype + 'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp) + | SUM ('a aexp) ('a aexp) + | DIFF ('a aexp) ('a aexp) + | NUM 'a + and + 'a bexp = LESS ('a aexp) ('a aexp) + | AND ('a bexp) ('a bexp) + | OR ('a bexp) ('a bexp) + +as well as indirectly recursive datatypes such as: - as well as indirectly recursive datatypes such as + datatype + ('a, 'b) term = Var 'a + | App 'b ((('a, 'b) term) list) - datatype - ('a, 'b) term = Var 'a - | App 'b ((('a, 'b) term) list) +The new tactic mutual_induct_tac [, ..., ] i performs +induction on mutually / indirectly recursive datatypes. + +Primrec equations are now stored in theory and can be accessed via +.simps. + +INCOMPATIBILITIES: - The new tactic - - mutual_induct_tac [, ..., ] i + - Theories using datatypes must now have theory Datatype as an + ancestor. + - The specific .induct_tac no longer exists - use the + generic induct_tac instead. + - natE has been renamed to nat.exhaustion - use exhaust_tac + instead of res_inst_tac ... natE. Note that the variable + names in nat.exhaustion differ from the names in natE, this + may cause some "fragile" proofs to fail. + - The theorems split__case and split__case_asm + have been renamed to .split and .split_asm. + - Since default sorts of type variables are now handled correctly, + some datatype definitions may have to be annotated with explicit + sort constraints. + - Primrec definitions no longer require function name and type + of recursive argument. - performs induction on mutually / indirectly recursive datatypes. - Primrec equations are now stored in theory and can be accessed - via .simps +Consider using isatool fixdatatype to adapt your theories and proof +scripts to the new package (backup your sources first!). + + +* HOL/record package: now includes concrete syntax for record types, +terms, updates; still lacks important theorems, like surjective +pairing and split; * reorganized the main HOL image: HOL/Integ and String loaded by default; theory Main includes everything; @@ -160,24 +182,12 @@ unit_eq_proc on (%u::unit. f u), replacing it by f rather than by %u.f(); -* HOL/record package: now includes concrete syntax for record types, -terms, updates; still lacks important theorems, like surjective -pairing and split; - -* HOL/inductive package reorganized and improved: now supports mutual -definitions such as +* HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which +makes more sense); - inductive EVEN ODD - intrs - null "0 : EVEN" - oddI "n : EVEN ==> Suc n : ODD" - evenI "n : ODD ==> Suc n : EVEN" - -new component "elims" of the structure created by the package contains -an elimination rule for each of the recursive sets; requires -Inductive.thy as an ancestor; component "mutual_induct" no longer -exists - the induction rule is always contained in "induct"; inductive -definitions now handle disjunctive premises correctly (also ZF); +* HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1 +to 'converse' from 'inverse' (for compatibility with ZF and some +literature); * HOL/recdef can now declare non-recursive functions, with {} supplied as the well-founded relation;