Isabelleで任意の記号の否定版を使用できますか？

Question

Isabelleでは、他のシンボルのバージョンを無効にしたシンボルを使用することができます。例は≠と∉です。 LaTeXの\notマクロのような、任意のシンボルのネガティブバージョンを取得するメカニズムはありますか？

Answer 1

あなたの質問には、2つの部分があります：任意のネゲート記号を使用できるかどうか、そしてそのような記号を便利なマクロで入力できるかどうか。

Isabelle FAQは、JEditが様々な方法で入力された数学記号をユニコードに変換し、ユニコード記号を使用/表示することを説明しています。したがって、Unicodeに希望のシンボルが存在する場合は、それを直接使用する可能性があります（つまり、ctrl-c ctrl-vシンボル）。たとえば、次のように「存在しない」を定義することができます。

abbreviation notexists :: "(('a ⇒ bool) ⇒ bool)" ("∄") where "∄ Φ ≡ (¬ (∃x. Φ(x)))" 

ただし、すべてのユニコード記号を使用できるわけではありません。たとえば、italic nablaはjeditに正しく表示されません。

質問の2番目の部分に：私が知る限り、そのようなマクロは存在しません。しかし、Isabelleには、記号を太字にするための同様のマクロメカニズムがあります。たとえば、\<bold> \<exists>は、太字の「存在」シンボルとして表示されます。これは、マクロの機能が存在することを示しています。また、将来示唆したように、シンボルを無効にするマクロを持つことが可能です。