Email Gateway (Aug 18 2022 at 10:55): Email Gateway (Aug 18 2022 at 10:55):From: Benedict Kavanagh <b.i.kavanagh@sms.ed.ac.uk>
Dear All,
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
consts ..
inductive ..
intros..
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?
Cheers,
Ben
Email Gateway (Aug 18 2022 at 10:56):From: Stefan Berghofer <berghofe@in.tum.de>
Benedict Kavanagh wrote:
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
where
name_1: "..."
| ...
| 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
consts
wt_exp :: "(tyctx × exp × ty) set"
syntax
"_wt_exp" :: "[tyctx,exp,ty] ("_ |-exp _ : _" [60,60] 60)
translations
"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
inductive
wt_exp :: "tyctx => exp => ty => bool" ("_ |-exp _ : _" [60,60] 60)
where
...
(See also the message by Holger Gast to the Isabelle mailing list on 28/03/06
for a discussion of this issue)
Greetings,
Stefan
Last updated: May 03 2024 at 04:19 UTC