[isabelle-dev] not-exists problem
Johannes Hölzl
hoelzl at in.tum.de
Tue Sep 13 10:41:58 CEST 2016
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-dev at in.tum.de
> > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
> > > abel
> > > le-dev
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
> > elle-dev
> >
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
More information about the isabelle-dev
mailing list