Isabelleで利用可能なすべての述語

Question

Isabelleで使用できるすべての述語と関数のリストを取得できますか？

もっと頻繁に起こることはないので、私は、それが既に存在することを認識するために証明（例えばcoprimeのような）のために必要な述語を手で定義し始めます。

Answer 1

find_theoremsと同様に、定義された定数をタイプまたは名前のいずれかで検索できるfind_constsがあります。 find_consts "'a list => nat"またはfind_consts name:"lim"。どうやら、これはcoprime（これはgcd a b = 1の略語です）のような略語を見つけることができます。

もちろん、実際にロードした理論の1つ（直接的または間接的に）で定義された定数しか見つけることができません。あなたが必要とするコンセプトは、~~/src/HOL/Libraryまたは配布の他の部分やAFPにすでに公式化されている可能性が常にあります。

これが当てはまると思われる場合は、ディストリビューションまたはAFPに適切なキーワードをgrepするだけです。それについて知っている人に尋ねます。ここにStackOverflowを頼むことは、このサイトを頻繁に訪れるプロフェッショナルなIsabelleユーザーや、そこにあるものとそうでないものについてよく知っている多数のユーザーがいるので、このようなものを見つけることは良い考えかもしれません。