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 O
?
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