Stream: Beginner Questions

Topic: binary numbers


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

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

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

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

view this post on Zulip Mathias Fleury (Jun 22 2021 at 06:04):

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

view this post on Zulip Mathias Fleury (Jun 22 2021 at 06:06):

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

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

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

view this post on Zulip tangentstorm (Jun 22 2021 at 06:12):

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

view this post on Zulip 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: Sep 25 2022 at 22:23 UTC