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)))"
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
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)?
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
Any reason not to use the existing definitions?
lemma ‹0b00011 = 3› (*binary*) ‹0x0000F = 15› (*hexa*) by simp_all
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.
no_notation relcomp (infixr "O" 75)
But I don't know if there is a solution for 2…
I would side-step the problem by converting a numeral to a
bin using your
bn function whenever needed.
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…
You may have a point there. I might do it just for the learning experience though. :)
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: Dec 07 2023 at 20:16 UTC