伊莎贝尔的二次公式？

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