author | wenzelm |

Sat Nov 24 16:53:31 2001 +0100 (2001-11-24) | |

changeset 12280 | fc7e3f01bc40 |

parent 12279 | dc3020e938e2 |

child 12281 | 3bd113b8f7a6 |

tuned;

1.1 --- a/NEWS Sat Nov 24 13:58:19 2001 +0100 1.2 +++ b/NEWS Sat Nov 24 16:53:31 2001 +0100 1.3 @@ -33,39 +33,33 @@ 1.4 *** Isar *** 1.5 1.6 * improved proof by cases and induction: 1.7 + - 'case' command admits impromptu naming of parameters (such as 1.8 + "case (Suc n)"); 1.9 + - 'induct' method divinates rule instantiation from the inductive 1.10 + claim; no longer requires excessive ?P bindings for proper 1.11 + instantiation of cases; 1.12 + - 'induct' method properly enumerates all possibilities of set/type 1.13 + rules; as a consequence facts may be also passed through *type* 1.14 + rules without further ado; 1.15 + - 'induct' method now derives symbolic cases from the *rulified* 1.16 + rule (before it used to rulify cases stemming from the internal 1.17 + atomized version); this means that the context of a non-atomic 1.18 + statement becomes is included in the hypothesis, avoiding the 1.19 + slightly cumbersome show "PROP ?case" form; 1.20 + - 'induct' may now use elim-style induction rules without chaining 1.21 + facts, using ``missing'' premises from the goal state; this allows 1.22 + rules stemming from inductive sets to be applied in unstructured 1.23 + scripts, while still benefitting from proper handling of non-atomic 1.24 + statements; NB: major inductive premises need to be put first, all 1.25 + the rest of the goal is passed through the induction; 1.26 + - 'induct' proper support for mutual induction involving non-atomic 1.27 + rule statements (uses the new concept of simultaneous goals, see 1.28 + below); 1.29 - removed obsolete "(simplified)" and "(stripped)" options of methods; 1.30 - added 'print_induct_rules' (covered by help item in Proof General > 3.3); 1.31 - moved induct/cases attributes to Pure, methods to Provers; 1.32 - generic method setup instantiated for FOL and HOL; 1.33 1.34 - - 'case' command admits impromptu naming of parameters (such as 1.35 -"case (Suc n)"); 1.36 - 1.37 - - 'induct' method divinates rule instantiation from the inductive 1.38 -claim; no longer requires excessive ?P bindings for proper 1.39 -instantiation of cases; 1.40 - 1.41 - - 'induct' method properly enumerates all possibilities of set/type 1.42 -rules; as a consequence facts may be also passed through *type* rules 1.43 -without further ado; 1.44 - 1.45 - - 'induct' method now derives symbolic cases from the *rulified* 1.46 -rule (before it used to rulify cases stemming from the internal 1.47 -atomized version); this means that the context of a non-atomic 1.48 -statement becomes is included in the hypothesis, avoiding the slightly 1.49 -cumbersome show "PROP ?case" form; 1.50 - 1.51 - - 'induct' may now use elim-style induction rules without chaining 1.52 -facts, using ``missing'' premises from the goal state; this allows 1.53 -rules stemming from inductive sets to be applied in unstructured 1.54 -scripts, while still benefitting from proper handling of non-atomic 1.55 -statements; NB: major inductive premises need to be put first, all the 1.56 -rest of the goal is passed through the induction; 1.57 - 1.58 -- 'induct' proper support for mutual induction involving non-atomic 1.59 -rule statements (uses the new concept of simultaneous goals, see 1.60 -below); 1.61 - 1.62 * Pure: support multiple simultaneous goal statements, for example 1.63 "have a: A and b: B" (same for 'theorem' etc.); being a pure 1.64 meta-level mechanism, this acts as if several individual goals had 1.65 @@ -82,7 +76,8 @@ 1.66 * Pure: proper integration with ``locales''; unlike the original 1.67 version by Florian Kammüller, Isar locales package high-level proof 1.68 contexts rather than raw logical ones (e.g. we admit to include 1.69 -attributes everywhere); 1.70 +attributes everywhere); operations on locales include merge and 1.71 +rename; e.g. see HOL/ex/Locales.thy; 1.72 1.73 * Pure: theory goals now support ad-hoc contexts, which are discharged 1.74 in the result, as in ``lemma (assumes A and B) K: A .''; syntax 1.75 @@ -122,6 +117,14 @@ 1.76 * HOL: 'inductive' no longer features separate (collective) attributes 1.77 for 'intros' (was found too confusing); 1.78 1.79 +* HOLCF: domain package adapted to new-style theories, e.g. see 1.80 +HOLCF/ex/Dnat.thy; 1.81 + 1.82 +* ZF: proper integration of logic-specific tools and packages, 1.83 +including theory commands '(co)inductive', '(co)datatype', 1.84 +'rep_datatype', 'inductive_cases', as well as methods 'ind_cases', 1.85 +'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC'); 1.86 + 1.87 1.88 1.89 *** HOL *** 1.90 @@ -152,16 +155,17 @@ 1.91 1.92 - remove all special provisions on numerals in proofs; 1.93 1.94 -* HOL/record: 1.95 - - removed old "make" and "make_scheme" operations -- INCOMPATIBILITY; 1.96 +* HOL/record package improvements: 1.97 + - new derived operations "fields" to build a partial record section, 1.98 + "extend" to promote a fixed record to a record scheme, and 1.99 + "truncate" for the reverse; cf. theorems "xxx.defs", which are *not* 1.100 + declared as simp by default; 1.101 + - removed "make_scheme" operations (use "make" with "extend") -- 1.102 + INCOMPATIBILITY; 1.103 - removed "more" class (simply use "term") -- INCOMPATIBILITY; 1.104 - provides cases/induct rules for use with corresponding Isar 1.105 methods (for concrete records, record schemes, concrete more 1.106 - parts, schematic more parts -- in that order); 1.107 - - new derived operations "make" (for adding fields of current 1.108 - record), "extend" to promote fixed record to record scheme, and 1.109 - "truncate" for the reverse; cf. theorems "derived_defs", which are 1.110 - *not* declared as simp by default; 1.111 + parts, and schematic more parts -- in that order); 1.112 - internal definitions directly based on a light-weight abstract 1.113 theory of product types over typedef rather than datatype; 1.114 1.115 @@ -202,61 +206,62 @@ 1.116 1.117 *** HOLCF *** 1.118 1.119 -* proper rep_datatype lift (see theory Lift); use plain induct_tac 1.120 -instead of former lift.induct_tac; always use UU instead of Undef; 1.121 - 1.122 -* 'domain' package adapted to new-style theories, e.g. see 1.123 -HOLCF/ex/Dnat.thy; 1.124 +* proper rep_datatype lift (see theory Lift) instead of ML hacks -- 1.125 +potential INCOMPATIBILITY; now use plain induct_tac instead of former 1.126 +lift.induct_tac, always use UU instead of Undef; 1.127 1.128 1.129 *** ZF *** 1.130 1.131 -* ZF: new-style theory commands '(co)inductive', '(co)datatype', 1.132 -'rep_datatype', 'inductive_cases'; also methods 'ind_cases', 1.133 -'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC'); 1.134 +* ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a 1.135 +typeless version of the formalism; 1.136 + 1.137 +* ZF/Induct: new directory for examples of inductive definitions, 1.138 +including theory Multiset for multiset orderings; 1.139 1.140 * ZF: the integer library now covers quotients and remainders, with 1.141 many laws relating division to addition, multiplication, etc.; 1.142 1.143 -* ZF/Induct: new directory for examples of inductive definitions, 1.144 -including theory Multiset for multiset orderings; 1.145 - 1.146 -* ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a 1.147 -typeless version of the formalism; 1.148 - 1.149 1.150 *** General *** 1.151 1.152 -* kernel: meta-level proof terms (by Stefan Berghofer), see also ref 1.153 -manual; 1.154 - 1.155 -* Pure/axclass: removed obsolete ML interface goal_subclass/goal_arity; 1.156 - 1.157 -* classical: renamed addaltern to addafter, addSaltern to addSafter; 1.158 - 1.159 -* clasimp: ``iff'' declarations now handle conditional rules as well; 1.160 - 1.161 -* syntax: new token syntax "num" for plain numerals (without "#" of 1.162 -"xnum"); potential INCOMPATIBILITY, since -0, -1 etc. are now separate 1.163 -tokens, so expressions involving minus need to be spaced properly; 1.164 - 1.165 -* syntax: support non-oriented infixes; 1.166 - 1.167 -* syntax: print modes "type_brackets" and "no_type_brackets" control 1.168 -output of nested => (types); the default behavior is "type_brackets"; 1.169 - 1.170 -* syntax: builtin parse translation for "_constify" turns valued 1.171 +* Pure/kernel: meta-level proof terms (by Stefan Berghofer); reference 1.172 +variable proof controls level of detail: 0 = no proofs (only oracle 1.173 +dependencies), 1 = lemma dependencies, 2 = compact proof terms; see 1.174 +also ref manual for further ML interfaces; 1.175 + 1.176 +* Pure/axclass: removed obsolete ML interface 1.177 +goal_subclass/goal_arity; 1.178 + 1.179 +* Pure/syntax: new token syntax "num" for plain numerals (without "#" 1.180 +of "xnum"); potential INCOMPATIBILITY, since -0, -1 etc. are now 1.181 +separate tokens, so expressions involving minus need to be spaced 1.182 +properly; 1.183 + 1.184 +* Pure/syntax: support non-oriented infixes; 1.185 + 1.186 +* Pure/syntax: print modes "type_brackets" and "no_type_brackets" 1.187 +control output of nested => (types); the default behavior is 1.188 +"type_brackets"; 1.189 + 1.190 +* Pure/syntax: builtin parse translation for "_constify" turns valued 1.191 tokens into AST constants; 1.192 1.193 -* syntax: prefer later print_translation functions; potential 1.194 -INCOMPATIBILITY: need to reverse declarations of multiple translation 1.195 -functions for same constant; 1.196 +* Pure/syntax: prefer later declarations of translations and print 1.197 +translation functions; potential INCOMPATIBILITY: need to reverse 1.198 +multiple declarations for same syntax element constant; 1.199 + 1.200 +* Provers/classical: renamed addaltern to addafter, addSaltern to 1.201 +addSafter; 1.202 + 1.203 +* Provers/clasimp: ``iff'' declarations now handle conditional rules 1.204 +as well; 1.205 1.206 * system: refrain from any attempt at filtering input streams; no 1.207 longer support ``8bit'' encoding of old isabelle font, instead proper 1.208 iso-latin characters may now be used; 1.209 1.210 -* system: support Poly/ML 4.1.1 (now able to manage large heaps); 1.211 +* system: support Poly/ML 4.1.1 (able to manage larger heaps); 1.212 1.213 * system: Proof General keywords specification is now part of the 1.214 Isabelle distribution (see etc/isar-keywords.el);