Isabelle/ZF 自然不平等

Question

我是 Isabelle 的新手，我试图证明这样的事情：

lemma refl_add_help: "[| n:nat; m:nat |] ==> 0 #+ n \<le> m #+ n" 
by(rule add_le_mono1, simp)

theorem mult_le_self: "[| 0 < m; n:nat; m:nat |] ==> n \<le> n #* m"
apply(case_tac m, auto)
apply(simp add: refl_add_help)
oops

我也试图证明一个引理：

lemma "[| n:nat; m:nat |] ==> n \<le> m #+ n"

但是我也没成功。谁能给我一些解决问题的建议？非常感谢。

对了，ZF里面是不是不能显示值啊

value "{m:nat. m < 5}"

我是这样导入理论的：

theory mytheory
imports ZF.Arith

Answer 1

我对Isabelle/ZF不是很熟悉。也就是说，您可以按如下方式证明您的结果：

  theorem mult_le_self: "⟦ 0 < m; n:nat; m:nat ⟧ ⟹ n ≤ n #* m"
    apply (case_tac m, simp)
    apply (frule_tac ?m="n #* x" in refl_add_help)
    apply (auto simp add: add_commute)
    done

  lemma "⟦ n:nat; m:nat ⟧ ⟹ n ≤ m #+ n"
    by (frule refl_add_help, auto)

有关 frule 和 frule_tac 方法的更多信息，请分别参阅 Isabelle/Isar 参考手册 的第 9.2 节和第 7.3 节。但是，我鼓励您使用 Isabelle/Isar 而不是证明脚本。例如，你的引理可以证明如下：

lemma "⟦ n:nat; m:nat ⟧ ⟹ n ≤ m #+ n"
proof -
  assume "n:nat" and "m:nat"
  then show ?thesis using refl_add_help by simp
qed

或者，更简洁地，如下：

lemma
  assumes "n:nat" and "m:nat"
  shows "n ≤ m #+ n"
  using assms and refl_add_help by simp

关于 value 命令，我认为它在 Isabelle/ZF 中不起作用。

Isabelle/ZF 自然不平等

Isabelle/ZF nat inequality

isabelle