[isabelle] syntax translation



Dear expert:
   I want to define a syntax abbreaviation as follows:
    In latex source  $n1\rightarrow_{SP}n2 \equiv (n1,n2) \in casual SP$
(please see the figures in attachment),

where casual1 is defined as follows:

definition

  casual1:: "strand_space \<Rightarrow>( node  \<times> node ) set "   where
  "casual1 SP \<equiv>  { (n1,n2) . n1 \<in>  Domain SP \<and> n2 \<in>
 Domain SP \<and>
  node_sign SP  n1= +  \<and>
  node_sign SP  n2= -
  \<and>  node_term SP n1= node_term SP n2
  \<and>  strand n1 \<noteq> strand n2
  } "


I have tried the following code, however, it cannot pass, can you
give me a hand?
syntax
  "_casual1"::" [node,strand_space,node]\<Rightarrow>bool" (
"_\<rightarrow>_/ _" )

translations
  "n1\<rightarrow>SP n2" ==  "CONST  member  (n1,n2)   (casual1 SP)"

regards
lyj

Attachment: syntax.png
Description: PNG image



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