## Stream: Beginner Questions

### Topic: machine word (morphisms)

#### Bruno Reis (Feb 10 2021 at 14:23):

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!

#### Jakub Kądziołka (Feb 10 2021 at 14:27):

`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

#### Bruno Reis (Feb 10 2021 at 14:32):

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?

#### Jakub Kądziołka (Feb 10 2021 at 14:36):

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

#### Jakub Kądziołka (Feb 10 2021 at 14:37):

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

#### Jakub Kądziołka (Feb 10 2021 at 14:37):

the `morphisms` here doesn't have any logical properties

#### Jakub Kądziołka (Feb 10 2021 at 14:39):

(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)

#### Jakub Kądziołka (Feb 10 2021 at 14:40):

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.

#### Bruno Reis (Feb 10 2021 at 14:48):

@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 :)