Re: [isabelle] Syntax and inductive_set
Tom Ridge wrote:
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?
by using inductive instead of inductive_set, you can directly define
reduce without any syntax translations:
inductive reduce :: "t => t => bool" ("_ ---> _" 50)
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
reduce :: "(t * t) set"
and reduce' :: "t => t => bool" ("_ ---> _" 50)
"(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.
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