Hi! can anyone explain to me why it fails since there is nothing about failure indication.
lemma delta:"∀ t::real. a * t^2 + b * t + c ≥ 0 ⟹ b^2 ≥ 4 * a * c" proof- assume "∀ t::real. a * t^2 + b * t + c ≥ 0 " hence "∀ t::real. a * (t + b / (2*a))^2 ≥ a * ( b^2 / (4 * a^2) - c / a)" by blast
this is not the type of statement that
blast is good at — it's a tableau prover, so it deals with things that are true because of first-order logic
First, let me say that there are some theorems that may help you in
Second, your theorem is false:
lemma delta:"∀ t::real. a * t^2 + b * t + c ≥ 0 ⟹ b^2 ≥ 4 * a * c" sorry thm delta[where a=1 and b=0 and c=1, simplified] (* outputs False *)
You can make this particular inference with
by (simp add: power2_eq_square algebra_simps)
Also, note that it's usually preferred to use the meta-quantifiers where possible:
lemma delta:"(⋀t::real. a * t^2 + b * t + c ≥ 0) ⟹ b^2 ≥ 4 * a * c"
ok, but I am not very clear about the difference between
\and t and
\And t is meta-level.
Last updated: Dec 07 2023 at 08:19 UTC