いわゆる one line proof です． lemma "(f::nat⇒real) 0 < 0 ==> ∃n. 0 ≦ f n ==> ∃n. f n < 0 ∧ 0 ≦ f (Suc n)" by (metis nat_induct [of "%n. f n < 0"] not_le) 参照している定理は thm nat_induct [of "%n. f n f 0 (¬ ?x ≤ ?y) = (?y の２つですが，Z…

以前，HOL Light で書いた定理ですが，Isar では．．． lemma fixes f :: "nat ⇒ real" assumes "f 0 < 0" "∃n. 0 ≦ f n" shows "∃n. f n < 0 ∧ 0 ≦ f (Suc n)" proof (rule ccontr) assume 1: "¬ ?thesis" {fix n have "f n < 0" proof (induct n) show "f …