I know that number literals are overloaded in Isabelle/HOL and that explicit type annotations are necessary in the following cases.

Most of the time I following the rule of thumb of "if there's an error involving number literals, add explicit type annotations".

But I wanted to understand the errors that arise in the following examples a little bit better:

Doing

```
value "5 - 10"
```

will yield the error

```
Wellsortedness error:
Type 'a not of sort term_of
Cannot derive subsort relation {minus,numeral} < term_of
```

and doing

```
value "5 + 10"
```

will yield the error

```
Wellsortedness error:
Type 'a not of sort term_of
Cannot derive subsort relation numeral < term_of
```

I would say that both cases cause an error because a) number literals are overloaded and b) the operations + and - are also overloaded, so Isabelle does not know which functions to apply here.

- Why does the second example not mention
`plus`

in the error message but the first example does mention`minus`

? - And what does
`numeral < term_of`

mean?

If these questions can be answered by looking into the official docs, any pointers to them would be appreciated.

```
class numeral = one + semigroup_add
```

So numerals always have an addition

(I just did a control-click on `numeral`

, because I did not remember it either)

What `value`

does (in its default setting) is to run the code generator on the given term and then execute the generated ML code. The result is an ML value, and that ML value then has to be converted back to a HOL term in order to be displayed. This is done with the `term_of`

type class that contains a function that converts a value of the type to a representation of a HOL term. See the theory `HOL.Code_Evaluation`

for more details.

There are instances of `term_of`

for pretty much anything you should ever encounter, but of course that only works if the term in question is monomorphic. If there are free type variables in there, those do not have the `term_of`

sort (and indeed that approach cannot work even on a conceptual level – how would you execute ML code that contains free variables?).

There are other modes for `value`

that *can* work with free variables, namely ‘nbe’ (normalisation by evaluation) and ‘simp’ (using the simplifier), but they are much slower.

```
value [nbe] "3"
value [simp] "3"
```

With these, you get the result `1 + 1 + 1 :: 'a :: numeral`

, which is not particularly helpful, but at least it works.

A more useful example would be this:

```
value [nbe] "replicate 3 x"
```

Here you get the result `[x, x, x]`

(for some reason, ‘simp’ does not seem to work here).

Oh and `numeral < term_of`

simply means that the sort `numeral`

subsumes `term_of`

. Your term has the sort `numeral`

, but we also need the `term_of`

class here, and that would only be possible if `numeral`

subsumed `term_of`

. Which it doesn't. (And even if it did, you would then get another error due to the polymorphic nature of the term you are trying to evaluate. Something about free dictionaries being present.)

@Manuel Eberl @Mathias Fleury Thanks that clarified a lot!

waynee95 has marked this topic as resolved.

Last updated: Nov 11 2024 at 01:24 UTC