Re: [isabelle] syntax, translations



On Fri, 7 Oct 2011, hkb wrote:

 In Isabelle 2008

invfun :: "['a set, 'b set, 'a \<Rightarrow> 'b] \<Rightarrow> ('b \<Rightarrow> 'a)" "invfun A B (f :: 'a \<Rightarrow> 'b) == \<lambda>y\<in>B.(SOME x. (x \<in> A \<and> f x = y))"

syntax
"@INVFUN" :: "['a \<Rightarrow> 'b, 'b set, 'a set] \<Rightarrow> ('b \<Rightarrow> 'a)"
             ("(3_\<inverse>\<^bsub>_,_\<^esub>)" [82,82,83]82)
 translations
   "f\<inverse>\<^bsub>B,A\<^esub>" == "invfun A B f"

works, but in the latest version, it does not.

Using 'syntax' + 'translations' to simulate abbreviations is a bit old-fashioned. You can use 'abbreviation' directly like this (also in Isabelle2008):

abbreviation invfun_syntax ::
  "['a \<Rightarrow> 'b, 'b set, 'a set] \<Rightarrow> ('b \<Rightarrow> 'a)"
    ("(3_\<inverse>\<^bsub>_,_\<^esub>)" [82,82,83]82)
  where "f\<inverse>\<^bsub>B,A\<^esub> == invfun A B f"


	Makarius





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