Email Gateway (Aug 19 2022 at 17:13): Email Gateway (Aug 19 2022 at 17:13):From: "W. Douglas Maurer" <maurer@gwu.edu>
Looking in the Symbols panel under Unsorted, I see a lot of symbols
that wouldn't make sense in Isabelle/Isar (flat, sharp, euros,
pounds, etc.) but one that definitely would make sense, namely
\<emptyset> (the zero with a slash through it). Isabelle does have
notation for the empty set, namely {} (so for example {} union X is
X; {} intersect X is {}; and these can be proved by simp) but these
don't work if {} is replaced by the empty-set symbol, even though
\<em does auto-complete to that symbol. Is there a good reason for
this? If not, perhaps it could be fixed in the next version. (When I
teach discrete mathematics, I always use that symbol instead of {} .)
Email Gateway (Aug 19 2022 at 17:13):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Douglas,
the answer is simple: there is no syntax to interpret \<emptyset>
accordingly.
You can add it using e.g.
notation Set.empty ("\<emptyset> ")
(untested, refer to the Isar reference manual for details).
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 17:14):From: "W. Douglas Maurer" <maurer@gwu.edu>
I posted a message entitled "Why doesn't \<emptyset> work?" (message
5, Sat, 14 Feb 2015). Then Florian Haftmann replied to me privately,
saying: "the answer is simple: there is no syntax to interpret
\<emptyset> accordingly. You can add it using e.g. 'notation
Set.empty ("\<emptyset> ")' (untested, refer to the Isar reference
manual for details)." I tested that, and it does work. Thanks! (I
still think it should be built in, though.)
Last updated: Apr 23 2024 at 04:18 UTC