Re: [isabelle] Syntax and inductive_set



Tom Ridge wrote:
Dear All,

I am trying to move old inductive set defns to Isa07 inductive_sets. I need to include syntax translations, e.g.

[...]

But this is not currently accepted by Isabelle07. How can I define reduce, but introduce syntax _ ---> _ for it at the same time?

Dear Tom,

by using inductive instead of inductive_set, you can directly define
reduce without any syntax translations:

  inductive reduce :: "t => t => bool" ("_ ---> _" 50)
  where
    ...

If for whatever reason your theory depends on reduce being a set, note that
inductive_set as well as inductive allow translations and introduction
rules to be specified simultaneosly, i.e. you can write something like

  inductive_set
    reduce :: "(t * t) set"
    and reduce' :: "t => t =>  bool" ("_ ---> _" 50)
  where
    "(t1 ---> t2) \<equiv> (t1, t2) : reduce"
  | ...

There is also a quite lengthy section in the NEWS file entitled "New package
for inductive predicates" that describes how to port your inductive definitions
to the new format.

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.