Re: [isabelle] syntax translation



Am 29/11/2012 06:39, schrieb li yongjian:
> 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)"

If I replace "node", "strand_space", "member" and "casual" (which I don't have)
and just define

syntax
  "_casual1" :: " ['a,'b,'a]\<Rightarrow>bool" ("_\<rightarrow>_/ _")

translations
   "n1\<rightarrow>SP n2" ==  "(n1,n2) : SP"

it works fine for me.

Tobias





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