Isabelleをいじっているあいだ（＝飽きるまで ^^;）は、ダイアリーにIsabelleの話が入るでしょう。今日は小ネタ。
「ハイコンテキストな定数・記号の解釈」とかで話題にしたmin-plus半環をIsabelleで書いてみました。あの記事では、通常の演算子記号「+」「*」をオーバーロードする話でしたが、今回はエキゾチックな演算子記号「」「
」を使います -- 「零の概念とmax-plus半環の紹介」の説明と同じ記号法になります。
とりあえず書いてみたのは：[追記]コメント内の to proof は to prove ですね。テキストならすぐ修正するけど、画像だから面倒だ、直さない。[/追記]
セオリー記述をお見せするのにスクリーンショット貼り付けるのが、もうナントモ複雑な気分ですが、生のソースコード・テキストじゃ読むの辛いし。（一応、最後にテキストも貼っておきます。）
min-plus半環の台集合は非負実数の集合ですが、realやdoubleがIsabelleに（少なくともMainセオリーには）入ってなかったのでintを台にしました。と
の定義は見りゃわかると思います。生ソースで
は \<oplus>、
は \<odot> で、TeXと同じ記号名です。（[追記 date="2016-06-20"]Realというセオリーをインポートすると実数が使えますね。[/追記]）
「Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか」でも触れたように、Isabelleのソースファイルは7ビットASCIIエンコーディングで*1、演算子記号に対する生のUnicode文字は入っていません。参考までに、「」と「
」のUnicodeコードポイントは：
min-plus半環が実際に半環の公理の満たすことを一部だけ示しています。この程度の定理なら自動証明でいけます。
「min-plus半環は半環である」という主張をIsabelleのなかでキッチリ示すには、半環を型クラスとして定義して、具体的に与えたmin-plus半環が型クラスのインスタンスになることを証明すれば良さそうです。「Coqで半環：アンバンドル方式の例として」でやったような、代数構造の階層的構成もたぶん型クラスで出来るでしょう。
ソースコードのテキスト：
[追記]コメント内の間違い to proof も画像と同じまま。簡単に直せるけど直さない。[/追記]
theory MinPlus imports "Main" begin section \<open>Definition of MinPlus sum and product\<close> fun minplus_sum :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "\<oplus>" 60) where "minplus_sum x y = min x y" fun minplus_prod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "\<odot>" 70) where "minplus_prod x y = x + y" section \<open>Some MinPlus expressions and evaluated values\<close> value "1 \<oplus> 1" (* is 1*) value "1 \<odot> 1" (* is 2 *) value "10 \<oplus> 3\<odot>5" (* is 8*) section \<open>Theorems (insufficient)\<close> theorem sum_assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" apply(auto) (* We do not need to proof by hand. *) done theorem sum_comm: "x \<oplus> y = y \<oplus> x" apply(auto) done theorem dist_l: "x\<odot>(y \<oplus> z) = x\<odot>y \<oplus> x\<odot>z" apply(auto) done
