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 simplest
solution is to disallow multiple variables for
∄ and ∃! as well.

We already have special quantifiers like ∃x:A that cannot be repeated
(for very basic technical reasons). This means users are used to
non-iterated quantifiers: it should cause less surprise than extra
syntax that is unclear.


        Makarius

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to