Re: [isabelle] syntax, translations



Dear Hidetsune,

in Isabelle 2009-2, authentic syntax has been introduced for all constants.
Hence, you must explicitly mark constant names in low-level syntax translations with CONST. In your case:

translations
  "f\<inverse>\<^bsub>B,A\<^esub>" == "CONST invfun A B f"

Note that there is now a more convenient (and type-safe) way to introduce such simple syntax translations known as abbreviations.

abbreviation INVFUN
  :: "['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"

Hope this helps,
Andreas

Am 07.10.2011 04:58, schrieb hkb:
Hi,

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. How to fix it?

Hidetsune Kobayashi


--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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