Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] How do I prove "¬ 2 ≤ 1" and use a simple lemma?

view this post on Zulip Email Gateway (Aug 22 2022 at 18:24):

From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
First, how do I prove a "¬ 2 ≤ 1"? Neither arith nor simp nor (simp add:
eval_nat_numeral) works.

Second, I have simple inductive definition and a lemma:

inductive le :: "nat ⇒ nat ⇒ bool" (infix "⊑" 50) where
le_n: "n ⊑ n" |
le_S: "n ⊑ m ⟹ n ⊑ (Suc m)"

lemma le_leq: "n ⊑ m ⟹ n ≤ m"
apply (induction rule: le.induct)
by (simp_all)

But then when I try to prove:

lemma "¬ 2 ⊑ 1"
proof (intro notI)
assume "2 ⊑ 1"
then have "2 ≤ 1" by (rule le_leq)

I get stuck. I can't figure out how to use the lemma le_leq above.
Isabelle complains:

Failed to apply initial proof method⌂:
using this:
2 ⊑ 1
goal (1 subgoal):

  1. 2 ≤ 1

What does that mean?

Thanks!

Last updated: Apr 19 2024 at 01:05 UTC