なぜ '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を見ると、3番目の前提は0 < ?wという形式ですが、3番目の位置にチェーンするのは0 ≤ 2です。それを0 < 2に置き換えると、正常に動作します。あなただけauto intro: frac_leあるいはsimp add: divide_simpsまたはsimp add: field_simpsを書き込むことによって、これらの面倒な手動手順を大幅に節約することができ

注意。 Isabelleの代数的推論は、既存の自動化を十分に活用しない限り、非常に面倒な傾向があります。