Isabelle返回數字而不是Suc（Suc（... 0））

當我使用value找出某個返回自然數的函數的值時，我總是以迭代的Successor函數的形式獲得答案0，即，有時難以閱讀的Suc(Suc(... 0))。有沒有辦法直接輸出Isabelle返回的號碼？Isabelle返回數字而不是Suc（Suc（... 0））

來源

2017-02-18 nicht

這聽起來像值沒有評估;這是一個thunk。我不知道伊莎貝爾，但看起來你需要強制評估。 – Carcigenicate

你在這裏試過答案嗎？ http://stackoverflow.com/questions/22687646/simplify-pretty-printing-of-naturals – ammbauer

這是我以前想解決的問題，但顯然我忘了。 Carcigenate的猜測是不正確的。這確實是全面評估的結果。問題在於自然數以這種笨拙的方式印刷出來。

你可以做以下的事情：

最簡單的方法是將數字轉換成整數，即代替value "foo x y z"（其中foo x y z是類型nat要eavluate的表情）你寫value "int (foo x y z)"。
您可以將~~/src/HOL/Library/Code_Target_Numeral添加到您的導入。這使得Isabelle的代碼生成器使用目標語言的任意精度整數（在value的情況下，即ML和基於GMP的整數），而不是低效的後繼符號。作爲副作用，這也以更好的方式打印自然數。
您可以將下面的代碼添加到您的理論，這改變了方式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命令是診斷命令只。它主要用於代碼生成設置的快速合理性測試和調試，並且使其起作用有時可能會非常棘手。

默認情況下，value依賴於代碼生成器，即Isabelle需要知道如何爲表達式生成可執行代碼，並且如果不能這樣做，value可能會失敗。（它有時也可以回退到其他一些策略，通過評估進行標準化或通過簡化進行評估，但這些策略通常不會提供有用的輸出）

我只是告訴你這一點，以便你知道期望從value命令，並沒有得到這樣的印象，這是人們一直使用伊莎貝爾的一個組成部分。

來源

2017-02-18 17:40:28

哇，請問你是如何學習關於伊莎貝爾的所有這些東西的？你有沒有深入閱讀手冊？這似乎是一個乏味的（但令人印象深刻的）任務，因爲我發現其中有些部分難以閱讀。 – nicht

我已經在這個系統工作了五年多，而且我一直在慕尼黑工業大學的一個椅子上工作，現在共同開發Isabelle幾年。我沒有真正閱讀過很多手冊;他們是有幫助的，但其中大部分並不是真正的東西，你絕對需要知道作爲用戶。大多數情況下，當你使用系統時，或者通過詢問其他人時，你都會接受。 –

Isabelle返回數字而不是Suc（Suc（... 0））

回答

相關問題