Stream: Beginner Questions

Topic: machine word (morphisms)


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (Feb 10 2021 at 14:37):

the morphisms here doesn't have any logical properties

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip Jakub Kądziołka (Feb 10 2021 at 14:50):

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

view this post on Zulip Manuel Eberl (Feb 10 2021 at 15:08):

Yes, type definitions are axiomatic.


Last updated: Feb 27 2024 at 08:17 UTC