tangentstorm (Jun 21 2021 at 22:47): 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)))"
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)?
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
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.
Mathias Fleury (Jun 22 2021 at 06:04):no_notation relcomp (infixr "O" 75)
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: Apr 18 2024 at 20:16 UTC