Isabelle の一連の数値 (nat) で最大の要素を見つけるにはどうすればよいですか。max 関数は、最大 2 つの要素を取るように定義されているため、機能しません。reduce like 関数を使用して実装する方法については考えていますが、セットからランダムな要素を 1 つ選択する方法がわかりません。
質問する
797 次
2 に答える
7
探している関数は と呼ばれMaxます。基本的な定数を探している場合は、Isabelle の公式ドキュメントの What's in Mainガイドが役立つことがよくあります。find_consts機能を種類別に検索できるコマンドもあります。
于 2013-02-11T20:07:48.633 に答える
4
MaxメインのHOLライブラリのto理論の定義に従うと、次のように定義Big_Operatorsされていることがわかります。
Max = fold1 max
コンビネータfold1は、有限集合で機能する「reducelike関数」です。具体的なリストではなく、任意のセットを折りたたむためにここで必要な数学的背景については、理論Finite_Setとそのロケールも参照してください。folding
于 2013-03-02T17:26:02.783 に答える