Isabelleのクラスインスタンスの印刷/照会

Question

私はちょうどIsabelleを使い始めています。

theory Z 
    imports Main Int 
begin 

value "(2::int) + (2::int)" 

lemma "(n::int) + (m::int) = m + n" 
apply(auto) done 

print_locale comm_ring_1 
print_interps comm_ring_1 

end 

これのほとんどは、私が期待通りに動作します：イザベルは、2 + 2 = 4と言われます、そして、それはそれを証明する方法を知っているN + M = m + nは、それが印刷さ私はこのようなファイルを持っています可換単位リングの公理。

しかし、私は、 "print_interps comm_ring_1"という行が、整数がクラスcomm_ring_1のインスタンスであることを知っていることをIsabelleに教えてくれることを期待していました（この事実は確かにファイルInt.thy私たちがインポートした標準ライブラリ）。しかし、イザベルは実際にそれを私に伝えていません。

Isabelleに知っているcomm_ring_1のすべてのインスタンスをリストするように他の方法がありますか？または、intがcomm_ring_1のインスタンスであるかどうかを特に照会するには？私はこのようなコマンドのリファレンスマニュアルを見てきましたが、見つけられませんでした。

Answer 1

Isabelleのすべての型クラスは、同じ名前のロケールを定義しますが、同じではありません。 print_localeとprint_interpsのコマンドは、型クラスのロケール・アスペクトのみを考慮しています。 instanceまたはinstantiationの型クラス登録は、そのロケールの解釈として型を登録しません。そのため、print_interpsには、タイプクラスの実績のあるインスタンスがリストされていません。これはコマンドprint_classesによって行われます。