Bruno Reis (Feb 10 2021 at 14:23): 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 :)
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
Manuel Eberl (Feb 10 2021 at 15:08):Yes, type definitions are axiomatic.
Last updated: Apr 18 2024 at 20:16 UTC