5 New in this Isabelle version |
5 New in this Isabelle version |
6 ---------------------------- |
6 ---------------------------- |
7 |
7 |
8 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
8 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
9 |
9 |
10 * several changes of proof tools (see next section); |
10 * several changes of proof tools; |
11 |
11 |
12 * HOL/datatype: |
12 * HOL: major changes to the inductive and datatype packages; |
13 - Theories using datatypes must now have Datatype.thy as an |
13 |
14 ancestor. |
14 * HOL: renamed r^-1 to 'converse' from 'inverse'; `inj_onto' is now |
15 - The specific <typename>.induct_tac no longer exists - use the |
15 called `inj_on'; |
16 generic induct_tac instead. |
|
17 - natE has been renamed to nat.exhaustion - use exhaust_tac |
|
18 instead of res_inst_tac ... natE. Note that the variable |
|
19 names in nat.exhaustion differ from the names in natE, this |
|
20 may cause some "fragile" proofs to fail. |
|
21 - the theorems split_<typename>_case and split_<typename>_case_asm |
|
22 have been renamed to <typename>.split and <typename>.split_asm. |
|
23 - Since default sorts are no longer ignored by the package, |
|
24 some datatype definitions may have to be annotated with |
|
25 explicit sort constraints. |
|
26 - Primrec definitions no longer require function name and type |
|
27 of recursive argument. |
|
28 Use isatool fixdatatype to adapt your theories and proof scripts |
|
29 to the new package (as usual, backup your sources first!). |
|
30 |
|
31 * HOL/inductive requires Inductive.thy as an ancestor; `inj_onto' is |
|
32 now called `inj_on' (which makes more sense); |
|
33 |
|
34 * HOL/Relation: renamed the relational operator r^-1 to 'converse' |
|
35 from 'inverse' (for compatibility with ZF and some literature); |
|
36 |
16 |
37 |
17 |
38 *** Proof tools *** |
18 *** Proof tools *** |
39 |
19 |
40 * Simplifier: Asm_full_simp_tac is now more aggressive. |
20 * Simplifier: Asm_full_simp_tac is now more aggressive. |
89 aimed to solve the given subgoal completely; |
69 aimed to solve the given subgoal completely; |
90 |
70 |
91 |
71 |
92 *** General *** |
72 *** General *** |
93 |
73 |
94 * new toplevel commands `Goal' and `Goalw' that improve upon `goal' |
74 * new top-level commands `Goal' and `Goalw' that improve upon `goal' |
95 and `goalw': the theory is no longer needed as an explicit argument - |
75 and `goalw': the theory is no longer needed as an explicit argument - |
96 the current theory context is used; assumptions are no longer returned |
76 the current theory context is used; assumptions are no longer returned |
97 at the ML-level unless one of them starts with ==> or !!; it is |
77 at the ML-level unless one of them starts with ==> or !!; it is |
98 recommended to convert to these new commands using isatool fixgoal (as |
78 recommended to convert to these new commands using isatool fixgoal |
99 usual, backup your sources first!); |
79 (backup your sources first!); |
100 |
80 |
101 * new toplevel commands 'thm' and 'thms' for retrieving theorems from |
81 * new top-level commands 'thm' and 'thms' for retrieving theorems from |
102 the current theory context, and 'theory' to lookup stored theories; |
82 the current theory context, and 'theory' to lookup stored theories; |
103 |
83 |
104 * new theory section 'nonterminals' for purely syntactic types; |
84 * new theory section 'nonterminals' for purely syntactic types; |
105 |
85 |
106 * new theory section 'setup' for generic ML setup functions |
86 * new theory section 'setup' for generic ML setup functions |
110 lib/logo/isabelle-{small,tiny}.xpm; |
90 lib/logo/isabelle-{small,tiny}.xpm; |
111 |
91 |
112 |
92 |
113 *** HOL *** |
93 *** HOL *** |
114 |
94 |
115 * HOL/datatype package reorganized and improved: now supports mutually |
95 * HOL/inductive package reorganized and improved: now supports mutual |
116 recursive datatypes such as |
96 definitions such as: |
117 |
97 |
118 datatype |
98 inductive EVEN ODD |
119 'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp) |
99 intrs |
120 | SUM ('a aexp) ('a aexp) |
100 null "0 : EVEN" |
121 | DIFF ('a aexp) ('a aexp) |
101 oddI "n : EVEN ==> Suc n : ODD" |
122 | NUM 'a |
102 evenI "n : ODD ==> Suc n : EVEN" |
123 and |
103 |
124 'a bexp = LESS ('a aexp) ('a aexp) |
104 new theorem list "elims" contains an elimination rule for each of the |
125 | AND ('a bexp) ('a bexp) |
105 recursive sets; inductive definitions now handle disjunctive premises |
126 | OR ('a bexp) ('a bexp) |
106 correctly (also ZF); |
127 |
107 |
128 as well as indirectly recursive datatypes such as |
108 INCOMPATIBILITIES: requires Inductive as an ancestor; component |
129 |
109 "mutual_induct" no longer exists - the induction rule is always |
130 datatype |
110 contained in "induct"; |
131 ('a, 'b) term = Var 'a |
111 |
132 | App 'b ((('a, 'b) term) list) |
112 |
133 |
113 * HOL/datatype package re-implemented and greatly improved: now |
134 The new tactic |
114 supports mutually recursive datatypes such as: |
135 |
115 |
136 mutual_induct_tac [<var_1>, ..., <var_n>] i |
116 datatype |
137 |
117 'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp) |
138 performs induction on mutually / indirectly recursive datatypes. |
118 | SUM ('a aexp) ('a aexp) |
139 Primrec equations are now stored in theory and can be accessed |
119 | DIFF ('a aexp) ('a aexp) |
140 via <function_name>.simps |
120 | NUM 'a |
|
121 and |
|
122 'a bexp = LESS ('a aexp) ('a aexp) |
|
123 | AND ('a bexp) ('a bexp) |
|
124 | OR ('a bexp) ('a bexp) |
|
125 |
|
126 as well as indirectly recursive datatypes such as: |
|
127 |
|
128 datatype |
|
129 ('a, 'b) term = Var 'a |
|
130 | App 'b ((('a, 'b) term) list) |
|
131 |
|
132 The new tactic mutual_induct_tac [<var_1>, ..., <var_n>] i performs |
|
133 induction on mutually / indirectly recursive datatypes. |
|
134 |
|
135 Primrec equations are now stored in theory and can be accessed via |
|
136 <function_name>.simps. |
|
137 |
|
138 INCOMPATIBILITIES: |
|
139 |
|
140 - Theories using datatypes must now have theory Datatype as an |
|
141 ancestor. |
|
142 - The specific <typename>.induct_tac no longer exists - use the |
|
143 generic induct_tac instead. |
|
144 - natE has been renamed to nat.exhaustion - use exhaust_tac |
|
145 instead of res_inst_tac ... natE. Note that the variable |
|
146 names in nat.exhaustion differ from the names in natE, this |
|
147 may cause some "fragile" proofs to fail. |
|
148 - The theorems split_<typename>_case and split_<typename>_case_asm |
|
149 have been renamed to <typename>.split and <typename>.split_asm. |
|
150 - Since default sorts of type variables are now handled correctly, |
|
151 some datatype definitions may have to be annotated with explicit |
|
152 sort constraints. |
|
153 - Primrec definitions no longer require function name and type |
|
154 of recursive argument. |
|
155 |
|
156 Consider using isatool fixdatatype to adapt your theories and proof |
|
157 scripts to the new package (backup your sources first!). |
|
158 |
|
159 |
|
160 * HOL/record package: now includes concrete syntax for record types, |
|
161 terms, updates; still lacks important theorems, like surjective |
|
162 pairing and split; |
141 |
163 |
142 * reorganized the main HOL image: HOL/Integ and String loaded by |
164 * reorganized the main HOL image: HOL/Integ and String loaded by |
143 default; theory Main includes everything; |
165 default; theory Main includes everything; |
144 |
166 |
145 * added option_map_eq_Some to the default simpset claset; |
167 * added option_map_eq_Some to the default simpset claset; |
158 'Delsimprocs [unit_eq_proc];' as last resort); also note that |
180 'Delsimprocs [unit_eq_proc];' as last resort); also note that |
159 unit_abs_eta_conv is added in order to counter the effect of |
181 unit_abs_eta_conv is added in order to counter the effect of |
160 unit_eq_proc on (%u::unit. f u), replacing it by f rather than by |
182 unit_eq_proc on (%u::unit. f u), replacing it by f rather than by |
161 %u.f(); |
183 %u.f(); |
162 |
184 |
163 * HOL/record package: now includes concrete syntax for record types, |
185 * HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which |
164 terms, updates; still lacks important theorems, like surjective |
186 makes more sense); |
165 pairing and split; |
187 |
166 |
188 * HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1 |
167 * HOL/inductive package reorganized and improved: now supports mutual |
189 to 'converse' from 'inverse' (for compatibility with ZF and some |
168 definitions such as |
190 literature); |
169 |
|
170 inductive EVEN ODD |
|
171 intrs |
|
172 null "0 : EVEN" |
|
173 oddI "n : EVEN ==> Suc n : ODD" |
|
174 evenI "n : ODD ==> Suc n : EVEN" |
|
175 |
|
176 new component "elims" of the structure created by the package contains |
|
177 an elimination rule for each of the recursive sets; requires |
|
178 Inductive.thy as an ancestor; component "mutual_induct" no longer |
|
179 exists - the induction rule is always contained in "induct"; inductive |
|
180 definitions now handle disjunctive premises correctly (also ZF); |
|
181 |
191 |
182 * HOL/recdef can now declare non-recursive functions, with {} supplied as |
192 * HOL/recdef can now declare non-recursive functions, with {} supplied as |
183 the well-founded relation; |
193 the well-founded relation; |
184 |
194 |
185 * HOL/Update: new theory of function updates: |
195 * HOL/Update: new theory of function updates: |