> 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
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
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
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
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
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
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:
>
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
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
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
10 matches
Mail list logo