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: > 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 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 have funny semantics when used with multiple > > variables: > > > > lemma "(∄x y. P x y) ⟷ ¬(∃x. ¬(∃y. P x y))" > > by (rule refl) > > > > lemma "(∃!x y. P x y) ⟷ (∃!x. (∃!y. P x y))" > > by (rule refl) > > > > this leads to funny lemmas like: > > > > lemma not_what_you_might_think: "∄x y. x+y = (3::int)" > > by presburger > > > > lemma also_strange: "∃!x y. x = abs (y::int)" > > by (metis (no_types, hide_lams) abs_0_eq abs_minus_cancel > > equal_neg_zero) > > > > > > 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)) > > > > > > > > We should either forbid multiple variables on those quantifiers, or > > try > > to figure out whether there is a widely-accepted consensus on their > > meaning. > > > > -- > > Peter > > > > > > > > > > > > > Note that ∄x y. P x y would be fine. > > > > > > Larry > > > > > > ~/isabelle/Repos/src/HOL: hg id > > > dca6fabd8060 tip > > > > > > _______________________________________________ > > > isabelle-dev mailing list > > > isabelle-...@in.tum.de > > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is > > > abel > > > le-dev > > _______________________________________________ > > isabelle-dev mailing list > > isabelle-...@in.tum.de > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab > > elle-dev > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel > le-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev