[isabelle-dev] NEWS: syntax for unique existence quantifier

Makarius makarius at sketis.net
Mon Sep 19 12:52:20 CEST 2016

*** HOL ***

* The unique existence quantifier no longer provides 'binder' syntax,
but uses syntax translations (as for bounded unique existence). Thus
iterated quantification ∃!x y. P x y with its slightly confusing
sequential meaning ∃!x. ∃!y. P x y is no longer possible. Instead,
pattern abstraction admits simultaneous unique existence ∃!(x, y). P x y
(analogous existing notation ∃!(x, y)∈A. P x y). Potential
INCOMPATIBILITY in rare situations.

This refers to Isabelle/cc15bd7c5396. In e4fdf9580372 there is an
example of using the unique existence of a pair, but such cases are very

Note that the tuple pattern support is a natural consequence of using
translations instead of 'binder'. It has been there for a long time for
the bounded quantifier, e.g.

lemma "∃!(x, y) ∈ {(a, b)}. True" by auto


More information about the isabelle-dev mailing list