爲什麼'linordered_field_class.frac_le'規則不起作用？ （Isabelle）

Question

我想在Isar證明中使用規則linordered_field_class.frac_le。這裏是代碼片段（它可能取決於證明的以前的部分，但這不太可能）。 n是nat類型。

... 
    then have 4:"2 ≤ (2^(n+1)::real)" by simp 
    have 1:"(0::real)≤(1::real)" by simp 
    have 2: "1≤(1::real)" by simp 
    have 3:"(0::real)≤(2::real)" by simp 
    from 1 2 3 4 have "1/(2^(n+1))≤1/(2::real)" by (rule linordered_field_class.frac_le) 

我想我已經正確應用規則，但它抱怨'未能完成證明'。我認爲這可能是一個類型錯誤，因此與:: real矯枉過正，但我​​無法修復它。有誰知道可能是什麼問題，以及如何解決它？或者只是另一種證明這種說法的方法。

Answer 1

如果你看規則frac_le，第三個前提的形式是0 < ?w，但是你鏈接到第三個位置的事實是0 ≤ 2。如果你用0 < 2代替它，它工作正常。

請注意，您只需編寫auto intro: frac_le甚至simp add: divide_simps或simp add: field_simps即可節省大量繁瑣的手動步驟。除非您充分利用現有的自動化，否則在伊莎貝爾的代數推理往往非常乏味。