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:

  "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,

Am 07.10.2011 04:58, schrieb hkb:

In Isabelle 2008

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

"@INVFUN" :: "['a \<Rightarrow> 'b, 'b set, 'a set] \<Rightarrow> ('b
\<Rightarrow> 'a)"
("(3_\<inverse>\<^bsub>_,_\<^esub>)" [82,82,83]82)
"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 - 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.