[isabelle] short-cut for defining inductive relations



Dear all,

in defining the (static) semantics of programming languages
I myself writing the same four steps again for
every inductively defined relation with infix syntax:
Constant declaration, syntax declaration, translation, and finally,
the inductive definition. (According to HOL/NanoJava and 
others, this seems to be the established best practice.)

For instance, here is the well-typedness for expressions:

--- snip ---
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 wt_exps intros
  ...
monos
  ...
--- snip ---

Is there any fundamental reason why a short-cut like

--- snip ---
inductive_relations
   wt_exp :: tyctx exp ty ("_ |-exp _ : _" [60,60] 60)
intros
 ...
monos
 ...
--- snip ---

cannot replace the above four declarations by suitable
calls to the Isabelle interface functions?
Has anybody implemented it?

Thanks,

Holger



 
  






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