when I code like:

```
lemma delta2:"b^2 / a^2 = (b / a)^2"
proof-
have "b*b / (a*a) = (b / a)*(b / a)"
using
Fields.field_class.times_divide_times_eq[of b a b a]
by auto
```

why does it fail like:

```
Type unification failed: Variable 'b::{inverse,power} not of sort field
Failed to meet type constraint:
Term: b :: 'b
Type: ??'a
Coercion Inference:
Local coercion insertion on the operand failed:
Variable 'b::{inverse,power} not of sort field
Now trying to infer coercions globally.
Coercion inference failed:
sort mismatch
```

can someone explain the description here?

Types have so-called sorts, which are extra-constraints over types. Isabelle computes the minimum required types and sorts to type a lemma.

Here the type`'b`

has sorts `inverse`

(this is required to have division) and `power`

(because of the `^2`

). However you want to apply the theorem `field_class.times_divide_times_eq`

that only works when `'b`

has also the sort field (i.e., when `'b`

is a field).

The solution is to be more explicit about sorts:

```
lemma delta2:"b^2 / a^2 = ((b::'b :: {field,power}) / a)^2"
```

or

```
lemma delta2:"b^2 / a^2 = (b / a)^2" for b:: "'b :: {field,power}"
```

(untested but if you need the `inverse`

, you know how to add it too)

Last updated: Sep 25 2021 at 09:17 UTC