Re: [isabelle-dev] not-exists problem

2016-09-13 Thread Jasmin Blanchette
> 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

2016-09-13 Thread Lawrence Paulson
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

2016-09-13 Thread Makarius
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

2016-09-13 Thread Lawrence Paulson
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

2016-09-13 Thread Manuel Eberl
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

[isabelle-dev] Code Folding and errors

2016-09-13 Thread Peter Lammich
Feature Request: (Isabelle: caae34eabcef) If an error appears in folded code, make it somehow visible in the main text window.  Currently, there is no indication of such an error that allows precise localization. Trying to jump to the error via clicking on the red bars on the left requires very

Re: [isabelle-dev] not-exists problem

2016-09-13 Thread Johannes Hölzl
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

2016-09-13 Thread Tjark Weber
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

2016-09-13 Thread Tobias Nipkow
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

2016-09-13 Thread Peter Lammich
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