Hi, I'm new to Isabelle and I'm trying to understand a bit about the theory of machine words.

The first definition in the file "HOL/Word/Word.thy" is the following:

```
typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ LENGTH('a::len0)}"
morphisms uint Abs_word by auto
```

Experimenting a bit I was able to conclude that uint is a function that receives a word and return the unsigned int encoded by that word.

Can someone clarify to me what is happening here? What is overloaded and morphisms in this context? What about uint / Abs_word? Where are they defined?

Thanks!

`typedef`

defines a new type `'a word`

out of the specified `{(0::int) ..< 2 ^ LENGTH('a::len0)}`

set. The morphisms are the functions that convert between the type of the elements in the set (true integers) and the newly-defined type

But where are the definitions of those functions that defines that this morphism is actually possible? Also, what (and where) is the definition of a morphism in Isabelle? Is it Just an injective function, or something more deep like an isomorphism?

note that `Abs_word`

will return the corresponding value only if the argument is actually in the set. In other cases, there is no corresponding `word`

and the value of the function is unspecified

Here's some more details on this kind of a partially-undefined function in Isabelle: https://www.joachim-breitner.de/blog/732-Isabelle_functions__Always_total,_sometimes_undefined

the `morphisms`

here doesn't have any logical properties

(you probably don't want to use Abs_word in your everyday formalizations, I suppose there is a function that takes the input integer modulo 2^n first)

But where are the definitions of those functions that defines that this morphism is actually possible?

AFAIK, subset type definitions are an axiom in Isabelle. They certainly are in HOL Light.

@Jakub Kądziołka Thanks a lot. I'll read that blog post and think about what you wrote. After that, if I still have some questions, I'll continue writing in this topic! Thank you :)

See also section 11.7 of https://isabelle.in.tum.de/dist/Isabelle2020/doc/isar-ref.pdf

Yes, type definitions are axiomatic.

Last updated: Oct 12 2024 at 20:18 UTC