Email Gateway (Aug 18 2022 at 18:30): Email Gateway (Aug 18 2022 at 18:30):From: hkb <hkb@icl.or.jp>
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
Email Gateway (Aug 18 2022 at 18:30):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 18:30):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Email Gateway (Aug 18 2022 at 18:30):From: Hidetsune Kobayashi <hkb@icl.or.jp>
Dear Andreas,
Thank you.
Hidetsune
(2011/10/07 16:55), Andreas Lochbihler wrote:
Last updated: Nov 21 2024 at 12:39 UTC