0

我正在尝试linordered_field_class.frac_le在 Isar 证明中使用该规则。这是代码片段（它可能取决于证明的前面部分，但这不太可能）。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，但我无法修复它。有谁知道可能是什么问题，以及如何解决？或者只是证明这种陈述的另一种方法。

4

1 回答 1

1

如果你看规则frac_le，第三个前提是形式0 < ?w，但你在第三个位置上链的事实是0 ≤ 2。如果将其替换为0 < 2，则可以正常工作。

请注意，您只需编写或auto intro: frac_le什至可以节省大量这些繁琐的手动步骤。除非您充分利用现有的自动化，否则 Isabelle 中的代数推理往往非常乏味。simp add: divide_simpssimp add: field_simps

于 2016-12-27T17:01:02.083 回答