author | wenzelm |

Thu Jul 30 17:06:54 1998 +0200 (1998-07-30) | |

changeset 5217 | 3ecd7c952396 |

parent 5216 | f0a66af5f2cb |

child 5218 | 1a49756a2e68 |

tuned;

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;