Isabelle 是一个基于高阶逻辑(higher-order logic)的通用交互式定理证明器。它是一个 LCF(Logic for Computable Functions)风格的证明辅助工具,使用 Standard ML 语言实现。它拥有一个极小化的逻辑核心;这意味着使用它的证明和形式化验证具有较强的的可信度。
theorem sqrt2_not_rational:
"sqrt (real 2) ∉ ℚ"prooflet ?x = "sqrt (real 2)"assume"?x ∈ ℚ"thenobtain m n :: nat where
sqrt_rat: "¦?x¦ = real m / real n"and lowest_terms: "coprime m n"by (rule Rats_abs_nat_div_natE)
hence"real (m^2) = ?x^2 * real (n^2)"by (auto simp add: power2_eq_square)
hence eq: "m^2 = 2 * n^2"using of_nat_eq_iff power2_eq_square by fastforce
hence"2 dvd m^2"by simp
hence"2 dvd m"by simp
have"2 dvd n"proof -
from‹2 dvd m›obtain k where"m = 2 * k" ..
with eq have"2 * n^2 = 2^2 * k^2"by simp
hence"2 dvd n^2"by simp
thus"2 dvd n"by simp
qedwith‹2 dvd m›have"2 dvd gcd m n"by (rule gcd_greatest)
with lowest_terms have"2 dvd 1"by simp
thus False using odd_one by blast
qed
Lawrence C. Paulson. "The foundation of a generic theorem prover". Journal of Automated Reasoning, Volume 5, Issue 3 (September 1989), pages: 363–397, ISSN0168-7433.
Lawrence C. Paulson: The Isabelle Reference Manual.
M. A. Ozols, K. A. Eastaughffe, and A. Cant. "DOVE: Design Oriented Verification and Evaluation". Proceedings of AMAST 97, M. Johnson, editor, Sydney, Australia. Lecture Notes in Computer Science (LNCS) Vol. 1349, Springer Verlag, 1997.
Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL – A Proof Assistant for Higher-Order Logic.