Email Gateway (Aug 18 2022 at 11:22): Email Gateway (Aug 18 2022 at 11:22):From: Tom Ridge <tjr22@cam.ac.uk>
Dear All,
I am trying to move old inductive set defns to Isa07 inductive_sets. I
need to include syntax translations, e.g.
syntax
"_reduce" :: "t => t => bool" ("_ ---> _" 50)
translations
"(t1 ---> t2)" \<rightleftharpoons> " ( t1 , t2 ) : reduce"
(** definitions *)
(*defns Jop *)
inductive_set reduce :: "(t*t) set"
where
(* defn reduce *)
ax_appI: "[|is_v_of_t v2|] ==>
(( (\<lambda> x . t12) \<bullet>v2) ---> ( tsubst_t v2 x t12 ) )"
| ctx_app_funI: "[|(t1 ---> t1')|] ==>
((t1\<bullet>t) ---> (t1'\<bullet>t))"
| ctx_app_argI: "[|is_v_of_t v ;
(t1 ---> t1')|] ==>
((v\<bullet>t1) ---> (v\<bullet>t1'))"
But this is not currently accepted by Isabelle07. How can I define
reduce, but introduce syntax _ ---> _ for it at the same time?
Thanks
Tom
Email Gateway (Aug 18 2022 at 11:22):From: Stefan Berghofer <berghofe@in.tum.de>
Tom Ridge wrote:
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
Last updated: May 03 2024 at 12:27 UTC