Re: [isabelle] backward compatibility of development snapshot.



Benedict Kavanagh wrote:
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?

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

--
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 MHonArc.