## Stream: Beginner Questions

### Topic: binary numbers

#### tangentstorm (Jun 21 2021 at 22:47):

Hello. :) I'm trying to make a little theory of binary numbers and I could use some help.

``````datatype bin = Z | Q bin | I bin

fun nb :: "bin ⇒ nat" where
"nb   Z = 0"
| "nb (Q x) = 2 * (nb x)"
| "nb (I x) = 2 * (nb x) + 1"

fun bn :: "nat ⇒ bin" where
"bn 0 = Z"
| "bn (Suc 0) = (I Z)"
| "bn x = (if even x then Q (bn (x div 2))
else I (bn ((x-1) div 2)))"
``````
1. I want to use the constructors `O x` to represent the operation "2x" and `I x` to represent "1+2x", but `O` is already defined as an infix operator, so I'm using `Q x`... Can I hide the pre-existing `O` ?

2. The syntax of data constructors forces me to write by binary numbers backwards : to write the value `0b1010`, I have to say `Q I Q I Z` ... Is there a way for me to define a lexer rule that lets me write something like `0b1010` (or at least arrange the bits in the traditional order)?

#### tangentstorm (Jun 21 2021 at 22:55):

Oh wow it's even worse. I have to write it with a set of parens for each bit. :/

``````lemma "10 = nb(Q(I(Q(I Z))))" by simp
``````

#### Mathias Fleury (Jun 22 2021 at 04:35):

Any reason not to use the existing definitions?

``````lemma
‹0b00011 = 3› (*binary*)
‹0x0000F = 15› (*hexa*)
by simp_all
``````

#### tangentstorm (Jun 22 2021 at 05:59):

Well, two reasons. :) 1. I didn't know that was already in the lexer, :) and 2. I want a syntax for constructing the data structure `I(I(Q(Q(Q Z))))` not the number 3.

#### Mathias Fleury (Jun 22 2021 at 06:04):

1. Hiding the notation:
``````no_notation relcomp (infixr "O" 75)
``````

#### Mathias Fleury (Jun 22 2021 at 06:06):

But I don't know if there is a solution for 2…

#### Mathias Fleury (Jun 22 2021 at 06:06):

I would side-step the problem by converting a numeral to a `bin` using your `bn` function whenever needed.

#### Mathias Fleury (Jun 22 2021 at 06:10):

You should be able to create a syntax following the string syntax (`typ string` and control-click `string`). But that seems too much if you don't really use a lot of numbers…

#### tangentstorm (Jun 22 2021 at 06:12):

You may have a point there. I might do it just for the learning experience though. :)

#### tangentstorm (Jun 26 2021 at 09:27):

So it seems Isabelle already comes with a theory of binary numbers: https://isabelle.in.tum.de/repos/isabelle/file/7e2a9a8c2b85/src/HOL/Num.thy

Interestingly, it doesn't have a concept of zero (probably to avoid between 0b1, 0b01, 0b001 etc.)

Last updated: Feb 27 2024 at 08:17 UTC