Suc（Suc（... 0））の代わりにIsabelleが返す数値

Question

valueを使用して自然数を返す関数の値を調べると、返された後続関数0、すなわち、Suc(Suc(... 0))は時々読みにくい場合があります。 Isabelleが返す番号を直接出力する方法はありますか？

Answer 1

これは私がしばらく前に修正したかったものの、明らかに忘れてしまったものです。カルシゲネートの推測は間違っています。これは実際に完全に評価された結果です。問題は、自然な数がこの扱いにくい方法で印刷されていることです。

あなたは次のことを行うことができます。

1. 最も簡単な方法は、すなわち代わりに（foo x y zはあなたがeavluateしたいタイプnatの表現である）value "foo x y z"の、整数に番号を変換することで、あなたはvalue "int (foo x y z)"を書きます。

2. インポートに~~/src/HOL/Library/Code_Target_Numeralを追加できます。これにより、Isabelleのコードジェネレータは、非効率な後続表記ではなく、ターゲット言語の任意精度の整数（valueのMLとそのGMPベースの整数）を使用します。副作用として、これはまた、より自然な方法で自然数を表示します。

は

3. あなたは道valueコマンドで表示自然数を変更し、あなたの理論、次のコードを追加することができます。

コード：valueコマンドは、診断であることを

lemma Suc_numeral_bit0: "Suc (numeral (Num.Bit0 n)) = numeral (Num.Bit1 n)" 
    by (subst Suc_numeral) simp 

lemma Suc_numeral_bit1: "Suc (numeral (Num.Bit1 n)) = numeral (Num.Bit0 (n + Num.One))" 
    by (subst Suc_numeral) simp 

lemmas [code_post] = 
    One_nat_def [symmetric] Suc_numeral_bit0 Suc_numeral_bit1 Num.Suc_1 Num.arith_simps 

注意コマンドのみ。これは主に、迅速な妥当性テストやコード生成設定のデバッグに使用され、動作させるのは難しい場合があります。

デフォルトではvalueはコード生成プログラムを使用しています。すなわち、Isabelleは式の実行可能コードを生成する方法を知っている必要があります。実行できない場合はvalueが失敗します。 （時には、いくつかの他の戦略、単純化による評価や評価による正規化にも戻すことができますが、通常は有用な出力は得られません）

私はちょうどこれを伝えて、 valueコマンドであり、これは人々が常に使用するイザベルの不可欠な部分であるという印象を受けない。