[isabelle] Syntax and inductive_set



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.