时间戳

首页 > 解决方案 > Isabelle/ZF nat 不等式

isabelle - Isabelle/ZF nat 不等式

问题描述

我是伊莎贝尔的新手，我试图证明这样的事情：

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

标签： isabelle

解决方案

我对伊莎贝尔/采埃孚不是很熟悉。也就是说，您可以按如下方式证明您的结果：

  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 中不起作用。

推荐阅读