let-statement with SOME operator

Question

I find myself often wanting to write expressions of this form

let x = SOME x. x ∈ e1 
in e2

that is; let x be an arbitary member of e1 in e2. It's rather verbose, and it seems a bit odd having to bind x twice. Is there a neater way to express this?

Answer 1

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"

Answer 2

I examined the way the let x = e1 in e2 syntax is handled (http://isabelle.in.tum.de/library/HOL/HOL/HOL.html), and found I could mostly duplicate that mechanism to provide a new let x ∈ e1 in e2 syntax. Here is my code (I just renamed let to lett throughout):

nonterminal lettbinds and lettbind
syntax
  "_bind"       :: "[pttrn, 'a] => lettbind"              ("(2_ ∈/ _)" 10)
  ""            :: "lettbind => lettbinds"                ("_")
  "_binds"      :: "[lettbind, lettbinds] => lettbinds"   ("_;/ _")
  "_Lett"       :: "[lettbinds, 'a] => 'a"                ("(let (_)/ in (_))" [0, 10] 10)

definition Lett :: "'a set ⇒ ('a ⇒ 'b) ⇒ 'b"
  where "Lett s f ≡ let x = SOME x. x ∈ s in f x"

translations
  "_Lett (_binds b bs) e" == "_Lett b (_Lett bs e)"
  "let x ∈ a in e"        == "CONST Lett a (λx. e)"

As a quick test:

value "let x ∈ {2::int,3} in x+x"