Re: [isabelle] backward compatibility of development snapshot.
Benedict Kavanagh wrote:
I need the code extraction capabilities of the development snapshot but
the Isabelle2007 syntax for inductive sets has changed (inductive_set
... where ...). I am using OTT to produce Isabelle definition and it
produces Isabelle2005 definitions
Does the development snapshot (Isabelle2007) have any backward
compatibility with these definitions? Is it possible to get the old
definitions to be accepted by Isabelle2007?
The only kind of backward compatibility we are providing is the "inductive_set"
command, which is just a wrapper allowing inductive sets to be defined with
the new inductive definition package. The old package for defining inductive
sets has been discontinued, and the "inductive" command now refers to the new
package for defining inductive predicates. For reasons of uniformity, both
"inductive" and "inductive_set" use the same outer syntax
p_1 :: T_1 and ... and p_n :: T_n
| name_m: "..."
This new format will become the standard way of writing down specifications
in the forthcoming Isabelle 2007 release and is already used by several other
commands such as the fun(ction) command for defining functions by general recursion.
Since the inner syntax for writing down the introduction rules has not been
changed and the behaviour of "inductive_set" is largely the same as the one
of the old "inductive" command, it should not be too difficult to port existing
theories (or code producing theories) to the new format (see the NEWS file
for more information on this).
However, in most situations it is easier to use an inductive predicate instead
of an inductive set, because this does not require the user to introduce clumsy
translations such as in
wt_exp :: "(tyctx × exp × ty) set"
"_wt_exp" :: "[tyctx,exp,ty] ("_ |-exp _ : _" [60,60] 60)
"G |-exp e : t" == "(G,e,t) : wt_exp"
inductive wt_exp intros
With the new inductive definition package, the above four declarations can
be replaced by just one command
wt_exp :: "tyctx => exp => ty => bool" ("_ |-exp _ : _" [60,60] 60)
(See also the message by Holger Gast to the Isabelle mailing list on 28/03/06
for a discussion of this issue)
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
Technische Universitaet Muenchen Fax: +49 89 289 17307
Boltzmannstr. 3 Room: 01.11.059
85748 Garching, GERMANY http://www.in.tum.de/~berghofe
This archive was generated by a fusion of
Pipermail (Mailman edition) and