Isabelle/ZF nat inequality

Question

I am new to Isabelle and I tried to prove something like this:

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

I also tried to prove a lemma:

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

but I could not success either. Can anyone give me some advice on how to solve the problem? Thank you very much.

By the way, is it not possible to display value in ZF like

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

I have imported the theory like this:

theory mytheory
imports ZF.Arith

Answer 1

I'm not very familiar with Isabelle/ZF. That said, you can prove your results as follows:

  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)

For more information regarding the frule and frule_tac methods please refer to The Isabelle/Isar Reference Manual, sections 9.2 and 7.3 respectively. However, I encourage you to use Isabelle/Isar instead of proof scripts. For example, your lemma can be proven as follows:

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

Or, more compactly, as follows:

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

Regarding the value command, I think it does not work in Isabelle/ZF.