Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Special syntax for a binder

Email Gateway (May 30 2024 at 13:34):

From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
Hi there,

I would like to have this syntax for lambda abstraction:

exp | x ≡ λx. exp

How could I define this in Isabelle? I got the advice to use abbreviation,
but it takes values and here x is not a value but a variable.

It's also not clear how I could use a mixfix syntax for this for the same
reason.

• Gergely

Email Gateway (May 30 2024 at 22:18):

From: Mike Stannett <cl-isabelle-users@lists.cam.ac.uk>
Hi Gergely - using the following approach seems to work. [I've not used
syntax/translations before so if this is wrong, someone please correct me!]

syntax
"_Bindme" :: "term ⇒ idt ⇒ term" ("( _ ¦ _ )")

translations
"(exp ¦ x)" ⇌ "(λx. exp)"

lemma bindme_binds: "∀ exp x v . ( exp ¦ x ) v = (λ x . exp) v"
by simp

(* Example *)
value "((xx) ¦ x) (2::nat)" ( = 4 *)
value "((xx) ¦ y) (2::nat)" ( = x*x *)

Mike

Email Gateway (May 31 2024 at 08:07):

From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
Dear Mike,

thanks. Now I discovered a paragraph at section 8.5.2 of the Isar Reference
Manual that states

Raw syntax and translations provides a slightly more low-level access to
the grammar and the form of resulting parse trees. It is often possible
to avoid this untyped macro mechanism, and use type-safe abbreviation
or notation instead. Some important situations where syntax and
translations are really need are as follows:

• Iterated replacement via recursive translations. For example, con-
sider list enumeration [a, b, c, d] as defined in theory HOL.List.

• Change of binding status of variables: anything beyond the built-in
binder mixfix annotation requires explicit syntax translations. For
example, consider the set comprehension syntax {x. P} as defined in
theory HOL.Set.

so indeed syntax and translations should be used here, abbreviation and
notation are not suitable.

• Gergely

Email Gateway (May 31 2024 at 10:02):

From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
My syntax/translations code works when in the main context of Isabelle, but
when I try to use it in a locale it complains about a bad context:

theory SyntaxTranslations

imports Main

begin

locale A begin

typedecl 'a M

consts mmap :: "('a ⇒ 'b) ⇒ ('a M ⇒ 'b M)" (* Bad context for command
"consts" *)

syntax
"_mmap_comprehension" :: "term ⇒ idt ⇒ term ⇒ term" ("[ _ | _ <- _ ]")

translations (* Bad context for
command "translations" *)
"[ exp | x <- e ]" ⇌ "CONST mmap (λx. exp) e"

It complains not only at translations but at consts as well. Are these too
low-level to be used in a locale?

• Gergely

Last updated: Jan 04 2025 at 20:18 UTC