There is a simpler solution than copying the setup for let
from HOL, namely, to extend the existing syntax translation for let
by giving another production for letbind
.
abbreviation Let_SOME :: "'a set => ('a => 'b) => 'b"
where "Let_SOME s f == let x = SOME x. x ∈ s in f x"
syntax
"_bindSOME" :: "[pttrn, 'a] => letbind" ("(2_ ∈/ _)" 10)
translations
"let x ∈ a in e" == "CONST Let_SOME a (%x. e)"
This has the advantage over your stand-alone solution that you can mix conventional let
bindings with the new ones, as in
term "let x = 5; y ∈ {1,2}; z = 6 in x + y + z"