tuned;
authorwenzelm
Thu Jul 30 17:06:54 1998 +0200 (1998-07-30)
changeset 52173ecd7c952396
parent 5216 f0a66af5f2cb
child 5218 1a49756a2e68
tuned;
NEWS
     1.1 --- a/NEWS	Thu Jul 30 15:56:21 1998 +0200
     1.2 +++ b/NEWS	Thu Jul 30 17:06:54 1998 +0200
     1.3 @@ -7,32 +7,12 @@
     1.4  
     1.5  *** Overview of INCOMPATIBILITIES (see below for more details) ***
     1.6  
     1.7 -* several changes of proof tools (see next section);
     1.8 +* several changes of proof tools;
     1.9  
    1.10 -* HOL/datatype:
    1.11 -  - Theories using datatypes must now have Datatype.thy as an
    1.12 -    ancestor.
    1.13 -  - The specific <typename>.induct_tac no longer exists - use the
    1.14 -    generic induct_tac instead.
    1.15 -  - natE has been renamed to nat.exhaustion - use exhaust_tac
    1.16 -    instead of res_inst_tac ... natE. Note that the variable
    1.17 -    names in nat.exhaustion differ from the names in natE, this
    1.18 -    may cause some "fragile" proofs to fail.
    1.19 -  - the theorems split_<typename>_case and split_<typename>_case_asm
    1.20 -    have been renamed to <typename>.split and <typename>.split_asm.
    1.21 -  - Since default sorts are no longer ignored by the package,
    1.22 -    some datatype definitions may have to be annotated with
    1.23 -    explicit sort constraints.
    1.24 -  - Primrec definitions no longer require function name and type
    1.25 -    of recursive argument.
    1.26 -  Use isatool fixdatatype to adapt your theories and proof scripts
    1.27 -  to the new package (as usual, backup your sources first!).
    1.28 +* HOL: major changes to the inductive and datatype packages;
    1.29  
    1.30 -* HOL/inductive requires Inductive.thy as an ancestor; `inj_onto' is
    1.31 -now called `inj_on' (which makes more sense);
    1.32 -
    1.33 -* HOL/Relation: renamed the relational operator r^-1 to 'converse'
    1.34 -from 'inverse' (for compatibility with ZF and some literature);
    1.35 +* HOL: renamed r^-1 to 'converse' from 'inverse'; `inj_onto' is now
    1.36 +called `inj_on';
    1.37  
    1.38  
    1.39  *** Proof tools ***
    1.40 @@ -91,14 +71,14 @@
    1.41  
    1.42  *** General ***
    1.43  
    1.44 -* new toplevel commands `Goal' and `Goalw' that improve upon `goal'
    1.45 +* new top-level commands `Goal' and `Goalw' that improve upon `goal'
    1.46  and `goalw': the theory is no longer needed as an explicit argument -
    1.47  the current theory context is used; assumptions are no longer returned
    1.48  at the ML-level unless one of them starts with ==> or !!; it is
    1.49 -recommended to convert to these new commands using isatool fixgoal (as
    1.50 -usual, backup your sources first!);
    1.51 +recommended to convert to these new commands using isatool fixgoal
    1.52 +(backup your sources first!);
    1.53  
    1.54 -* new toplevel commands 'thm' and 'thms' for retrieving theorems from
    1.55 +* new top-level commands 'thm' and 'thms' for retrieving theorems from
    1.56  the current theory context, and 'theory' to lookup stored theories;
    1.57  
    1.58  * new theory section 'nonterminals' for purely syntactic types;
    1.59 @@ -112,32 +92,74 @@
    1.60  
    1.61  *** HOL ***
    1.62  
    1.63 -* HOL/datatype package reorganized and improved: now supports mutually
    1.64 -  recursive datatypes such as
    1.65 +* HOL/inductive package reorganized and improved: now supports mutual
    1.66 +definitions such as:
    1.67 +
    1.68 +  inductive EVEN ODD
    1.69 +    intrs
    1.70 +      null "0 : EVEN"
    1.71 +      oddI "n : EVEN ==> Suc n : ODD"
    1.72 +      evenI "n : ODD ==> Suc n : EVEN"
    1.73 +
    1.74 +new theorem list "elims" contains an elimination rule for each of the
    1.75 +recursive sets; inductive definitions now handle disjunctive premises
    1.76 +correctly (also ZF);
    1.77  
    1.78 -    datatype
    1.79 -      'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp)
    1.80 -              | SUM ('a aexp) ('a aexp)
    1.81 -              | DIFF ('a aexp) ('a aexp)
    1.82 -              | NUM 'a
    1.83 -    and
    1.84 -      'a bexp = LESS ('a aexp) ('a aexp)
    1.85 -              | AND ('a bexp) ('a bexp)
    1.86 -              | OR ('a bexp) ('a bexp)
    1.87 +INCOMPATIBILITIES: requires Inductive as an ancestor; component
    1.88 +"mutual_induct" no longer exists - the induction rule is always
    1.89 +contained in "induct";
    1.90 +
    1.91 +
    1.92 +* HOL/datatype package re-implemented and greatly improved: now
    1.93 +supports mutually recursive datatypes such as:
    1.94 +
    1.95 +  datatype
    1.96 +    'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp)
    1.97 +            | SUM ('a aexp) ('a aexp)
    1.98 +            | DIFF ('a aexp) ('a aexp)
    1.99 +            | NUM 'a
   1.100 +  and
   1.101 +    'a bexp = LESS ('a aexp) ('a aexp)
   1.102 +            | AND ('a bexp) ('a bexp)
   1.103 +            | OR ('a bexp) ('a bexp)
   1.104 +
   1.105 +as well as indirectly recursive datatypes such as:
   1.106  
   1.107 -  as well as indirectly recursive datatypes such as
   1.108 +  datatype
   1.109 +    ('a, 'b) term = Var 'a
   1.110 +                  | App 'b ((('a, 'b) term) list)
   1.111  
   1.112 -    datatype
   1.113 -      ('a, 'b) term = Var 'a
   1.114 -                    | App 'b ((('a, 'b) term) list)
   1.115 +The new tactic  mutual_induct_tac [<var_1>, ..., <var_n>] i  performs
   1.116 +induction on mutually / indirectly recursive datatypes.
   1.117 +
   1.118 +Primrec equations are now stored in theory and can be accessed via
   1.119 +<function_name>.simps.
   1.120 +
   1.121 +INCOMPATIBILITIES:
   1.122  
   1.123 -  The new tactic
   1.124 -
   1.125 -    mutual_induct_tac [<var_1>, ..., <var_n>] i
   1.126 +  - Theories using datatypes must now have theory Datatype as an
   1.127 +    ancestor.
   1.128 +  - The specific <typename>.induct_tac no longer exists - use the
   1.129 +    generic induct_tac instead.
   1.130 +  - natE has been renamed to nat.exhaustion - use exhaust_tac
   1.131 +    instead of res_inst_tac ... natE. Note that the variable
   1.132 +    names in nat.exhaustion differ from the names in natE, this
   1.133 +    may cause some "fragile" proofs to fail.
   1.134 +  - The theorems split_<typename>_case and split_<typename>_case_asm
   1.135 +    have been renamed to <typename>.split and <typename>.split_asm.
   1.136 +  - Since default sorts of type variables are now handled correctly,
   1.137 +    some datatype definitions may have to be annotated with explicit
   1.138 +    sort constraints.
   1.139 +  - Primrec definitions no longer require function name and type
   1.140 +    of recursive argument.
   1.141  
   1.142 -  performs induction on mutually / indirectly recursive datatypes.
   1.143 -  Primrec equations are now stored in theory and can be accessed
   1.144 -  via <function_name>.simps
   1.145 +Consider using isatool fixdatatype to adapt your theories and proof
   1.146 +scripts to the new package (backup your sources first!).
   1.147 +
   1.148 +
   1.149 +* HOL/record package: now includes concrete syntax for record types,
   1.150 +terms, updates; still lacks important theorems, like surjective
   1.151 +pairing and split;
   1.152  
   1.153  * reorganized the main HOL image: HOL/Integ and String loaded by
   1.154  default; theory Main includes everything;
   1.155 @@ -160,24 +182,12 @@
   1.156  unit_eq_proc on (%u::unit. f u), replacing it by f rather than by
   1.157  %u.f();
   1.158  
   1.159 -* HOL/record package: now includes concrete syntax for record types,
   1.160 -terms, updates; still lacks important theorems, like surjective
   1.161 -pairing and split;
   1.162 -
   1.163 -* HOL/inductive package reorganized and improved: now supports mutual
   1.164 -definitions such as
   1.165 +* HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which
   1.166 +makes more sense);
   1.167  
   1.168 -  inductive EVEN ODD
   1.169 -    intrs
   1.170 -      null "0 : EVEN"
   1.171 -      oddI "n : EVEN ==> Suc n : ODD"
   1.172 -      evenI "n : ODD ==> Suc n : EVEN"
   1.173 -
   1.174 -new component "elims" of the structure created by the package contains
   1.175 -an elimination rule for each of the recursive sets; requires
   1.176 -Inductive.thy as an ancestor; component "mutual_induct" no longer
   1.177 -exists - the induction rule is always contained in "induct"; inductive
   1.178 -definitions now handle disjunctive premises correctly (also ZF);
   1.179 +* HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1
   1.180 +to 'converse' from 'inverse' (for compatibility with ZF and some
   1.181 +literature);
   1.182  
   1.183  * HOL/recdef can now declare non-recursive functions, with {} supplied as
   1.184  the well-founded relation;