Re: [isabelle-dev] not-exists problem

On 13/09/16 01:46, Lawrence Paulson wrote: > We have a problem with the ∄ operator, when existential quantifiers are > nested: > > lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))" > by (rule refl) > > Note that ∄x y. P x y would be fine. Back to this thread. There is now the following change:

Re: [isabelle-dev] not-exists problem

The symmetry between the variables in ~(∃x y. P x y) is completely lost in ∄x. ∃y. P x y. It’s a terrible notation. Larry > On 13 Sep 2016, at 22:56, Jasmin Blanchette > wrote: > >> I’m not sure that this suggestion addresses my original problem: that the >> use

Re: [isabelle-dev] not-exists problem

This discussion clearly shows that ∃! with multiple bound variables is a recipe for confusion and should be avoided. Tobias On 14/09/2016 09:49, Peter Lammich wrote: On Di, 2016-09-13 at 23:35 +, michael.norr...@data61.csiro.au wrote: Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy.

Re: [isabelle-dev] not-exists problem

On Di, 2016-09-13 at 23:35 +, michael.norr...@data61.csiro.au wrote: > Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy. P (fst xy) (snd > xy). > > If you were going to support ∃!x y at all (and I can certainly see > the argument for forbidding it outright), I'd expect it to map to the >

Re: [isabelle-dev] not-exists problem

Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy. P (fst xy) (snd xy). If you were going to support ∃!x y at all (and I can certainly see the argument for forbidding it outright), I'd expect it to map to the first formula above, and not the second. Michael On 13/09/2016, 18:41,

Re: [isabelle-dev] not-exists problem

> On 13.09.2016, at 23:33, Lawrence Paulson wrote: > > I’m not sure that this suggestion addresses my original problem: that the use > of the negated quantifier (by an output translation, i.e., not by request) > produced a confusing output. This output already contains only a

Re: [isabelle-dev] not-exists problem

I’m not sure that this suggestion addresses my original problem: that the use of the negated quantifier (by an output translation, i.e., not by request) produced a confusing output. This output already contains only a single variable bound by ∄. Larry > On 13 Sep 2016, at 19:56, Makarius

Re: [isabelle-dev] not-exists problem

On 13/09/16 01:46, Lawrence Paulson wrote: > We have a problem with the ∄ operator, when existential quantifiers are > nested: > > lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))" > by (rule refl) > > Note that ∄x y. P x y would be fine. Looking briefly over this thread, my impression is that the

Re: [isabelle-dev] not-exists problem

When mathematicians use such notations, they are communicating informally and they can count on the reader to understand what they mean. But that’s not how it works for us. Any notation that could be misinterpreted should be input only (assuming we support it at all). That way, the user

Re: [isabelle-dev] not-exists problem

The desired multi-variable semantics of ∄ seem obvious enough to me and I think that this should be allowed. For ∃!, the implicit complexity introduced by the pairing seems too much to me, so I think this should be forbidden. On 13/09/16 10:41, Johannes Hölzl wrote: There is even a third

Re: [isabelle-dev] not-exists problem

There is even a third one: ∄! I would vote to forbid the multiple variable case. At least for the next release. Is it possible to restrict this by a mixfix syntax or does it require to write a ML parse translations.  - Johannes Am Dienstag, den 13.09.2016, 10:30 +0200 schrieb Tobias Nipkow: >

Re: [isabelle-dev] not-exists problem

On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote: > I would have expected: > (∄x y. P x y) ⟷ ¬(∃x y. P x y) > and > (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x)) +1 Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] not-exists problem

There is a method to this madness: if B is a binder, "B x y. t" is short for "B x. B y. t". However, I agree that for ∄ and ∃! this is confusing and one of the solutions proposed should be adopted. Tobias On 13/09/2016 09:45, Peter Lammich wrote: On Di, 2016-09-13 at 00:46 +0100, Lawrence

Re: [isabelle-dev] not-exists problem

On Di, 2016-09-13 at 00:46 +0100, Lawrence Paulson wrote: > We have a problem with the ∄ operator, when existential quantifiers > are nested: > > lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))" >   by (rule refl) I do not see a particular problem with this, however, not-exists and also exists-one

[isabelle-dev] not-exists problem

We have a problem with the ∄ operator, when existential quantifiers are nested: lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))" by (rule refl) Note that ∄x y. P x y would be fine. Larry ~/isabelle/Repos/src/HOL: hg id dca6fabd8060 tip ___ isabelle-dev