[isabelle-dev] [isabelle] Tiny minor backward-compatible changes to IFOL

[Makarius]

On 02/05/2020 18:28, Manuel Eberl wrote:
> Do you mean "!" as an abbreviation or as actual syntax?
> 
> In case of the latter: I for one greatly prefer the one from Larry's
> email greatly over "!" since it is much more evocative.

This is from the original proposal
https://github.com/georgydunaev/onlyonequantifier

definition Only1 :: ‹('a ⇒ o) ⇒ o›  (binder ‹!› 10)
  where only1_def: ‹!x. P(x) ≡ (∀x.∀y. P(x) ∧ P(y) ⟶ x = y)›

definition Ex1 :: ‹('a ⇒ o) ⇒ o›  (binder ‹∃!› 10)
  where ex1new_def: ‹∃!x. P(x) ≡ (∃x. P(x)) ∧ (!x. P(x))›


Larry's name "Uniq" for "Only1" is better; I would have chosen the same name.

The syntax idea by Georgy is at least unconventional and creative: it
corresponds to the "!" aspect in the existing "∃!" notation for Ex1.

In contrast, the other idea "∃⇩≤⇩1" from Mathoverflow would come out for Ex1
as "∃⇩=⇩1" or "∃⇩1", and thus introduce an incoherence of notation.

In know that "!" and "?" are popular in the classic HOL community. But we
already have parted from that by ugly "? " (with space) to avoid a conflict
with schematic variables "?x" in Isabelle. So it would again simplify things
to part both from "!" and "? " now.


Depending how bold we are in clearing out old things we could do it like this:

  * A variant of the existing "isabelle update" tool replaces historic binders
"!" / "? " / "?!" by "∀" / "∃" / "∃!". With a little bit of extra work we can
get rid of related syntax variants as well.

  * Input methods for "!" and "?" remain unchanged, and are optional anyway
(single character, leading to popup).

Note that for a few years already, we have had a trend to replace old ASCII
notation by proper Isabelle symbols (while keeping remains of it in input
methods).

  * Fill the free space of "!" by Georgy's proposal with Larry's name for it.


	Makarius