伊莎贝尔的二次公式？

Question

我正在寻找包含二次公式的理论文件：

当然，知道引理的名称也会很有帮助。

我已经找到这篇论文了：

http://www.inf.ed.ac.uk/publications/thesis/online/IM040231.pdf

我可以在其中复制粘贴证明，但之后我将不得不重写它（因为它不能完美复制）。最好有一些立即可用的东西：也许如果有人知道在哪里可以找到与本文匹配的理论文件？

Answer 1

您链接的论文很旧，如果不进行重大更改，其中的证明将无法使用。

这是定理的简短证明：

theory Scratch
  imports Complex_Main
begin

lemma real_sqrt_unique':
  "(x::real) ^ 2 = y ⟹ x = -sqrt y ∨ x = sqrt y"
  using real_sqrt_unique[of x y] real_sqrt_unique[of "-x" y]
  by (cases "x ≥ 0") simp_all

lemma quadratic_roots_formula:
  fixes a b c x :: real
  assumes "a ≠ 0"
  defines "disc ≡ b^2 - 4 * a * c"
  assumes "disc ≥ 0"
  shows   "a * x^2 + b * x + c = 0 ⟷ x ∈ {(-b - sqrt disc) / (2*a), (-b + sqrt disc) / (2*a)}"
proof -
  from assms have "a * x^2 + b * x + c = 0 ⟷ 4 * a * (a * x^2 + b * x + c) = 0"
    by simp
  also have "4 * a * (a * x^2 + b * x + c) = (2 * a * x + b) ^ 2 - b^2 + 4 * a * c"
    by (simp add: algebra_simps power2_eq_square)
  also have "… = 0 ⟷ (2 * a * x + b) ^ 2 = disc" by (simp add: disc_def algebra_simps)
  also from ‹disc ≥ 0› have "… ⟷ (2 * a * x + b) ∈ {-sqrt disc, sqrt disc}"
    by (auto simp: real_sqrt_unique')
  also have "… ⟷ x ∈ {(-b - sqrt disc) / (2*a), (-b + sqrt disc) / (2*a)}"
    using assms by (auto simp: field_simps)
  finally show ?thesis .
qed

伊莎贝尔的二次公式？

Quadratic Formula in Isabelle?

quadratic

isabelle