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 `HOL-Library.Quadratic_Discriminant`

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 $\forall t$

`\And t`

is meta-level.

Last updated: Oct 12 2024 at 20:18 UTC