I ask my question first.
Question: I need binary and hex syntax for the num datatype. Is there some source somewhere I can easily adapt? Can someone provide it for me? Or, does it already exist?
The numeral type class allows the use of binary and hexadecimal notation, such as 0b0101 and 0xAA. However, num is not instantiated as numeral, and I only see the constructors used directly, such as with this source:
primrec sqr :: "num => num" where
"sqr One = One" |
"sqr (Bit0 n) = Bit0 (Bit0 (sqr n))" |
"sqr (Bit1 n) = Bit1 (Bit0 (sqr n + n))"
Below, I include a complete theory in which I've defined notation to allow me to use binary and hex notation with num, but it's not standard notation. The notation I have is acceptable, but it looks like it could eventually cause some conflicts.
I was initially building tables to learn how One, Bit0, and Bit1 are used to create a binary number. It was tricky at first, because the order of bits is reversed from normal, along with a few other quirks, but I finally got it. For anyone interested, there are some things that are good to know about num, along with a numeral wiki page:
- The most significant digit is on the right, not on the left.
- The
num type has no zero, so the rightmost digit will always be 1, though the rightmost digit increases in value by powers of 2 when you add enough digits on the left.
- Adding zeros on the left makes a number bigger.
The included theory is too involved to convert it to ASCII. Some might be interested in loading it in the PIDE to look at it. I show a use for the notation at the bottom, where I define the function num_left_shift.
I'm just looking for syntax that has a 2 character prefix, like 0u1010101, along with hex syntax like 0m555. The translation of the syntax would build up a number from the num constructors.
I couldn't get translations to work for me. I also see the use of parse_translation in Num.thy, but I don't know how to use it.
Update: 140326
I update this to answer Brian Huffman's question. I do it here since it will take more characters than a comment allows. Brian's question is this:
Is there a reason why you need to use type num directly? Why not define a separate type of naturals > 0, and make it an instance of class numeral?
The short answer is that I don't need num because it has no zero, I need it because that's the only way I know of to use fun with binary and hex at the bit level. In particular, I'm talking about pattern matching with fun, on binary and hex patterns.
From here, I talk about how num is part of my grand scheme, and why I think I need it to do a binary bit shift.
Numeral for abstraction, nat for Suc, and num for One, Bit0, and Bit1
This is related to my plans to eventually try and do a lot of work in algebra type classes.
Take the type class linordered_idom. How do I fully exploit the power of HOL for that type class? I don't, because I don't have a constructor to work with.
I spent a number of days trying to use datatype and typedef to put a constructor on UNIV::'a::linordered_idom set, though it also involved zero having its own constructor.
It sort of worked, but it was a bunch of clutter, and not a completely good solution.
That led to my idea to use nat as a means to front all numbers, using numeral(num_of_nat).
As part of that I defined a function to calculate the number of digits in a decimal number:
fun dec_digits :: "nat => nat" where
"dec_digits n = (if (n div 10 = 0) then 1 else 1 + dec_digits(n div 10))"
I assume that a bit shift operation on a binary number is faster than div, so I started pursuing a binary bit shift function to use with binary and hex numbers, and that led to num.
This ties back into the section title above. With nat, I get a constructor for building numbers by adding one. But how do I do binary bit shifts using nat?
There's a lot I don't know about numeral and num, but my conclusion is that as a complete solution for working with numbers, I need to work with all three of numeral, num, and nat.
The left bit shift for binary and hex division
The function num_left_shift is part of the culmination of my preliminary effort to get some basic ideas settled for the future, in relation to number systems, and their relation to algebraic type classes.
The type nat is foundational to HOL, and fun works a lot of magic with it. The numeral type class gives me an abstract set of number constants, where you work a lot of low-level magic for it with the algebraic binary operations.
But how do I manipulate numbers based on their structure? I know there's a lot of math in HOL, like div and mod, but how do I do binary bit shifts without using num?
All I know right now is how to use num to do that for binary and hex. If there's a high level way to do that, I'll be happy to learn about it.
One question I still have is this, "How do I manipulate numbers in HOL based on decimal digits, without using div?
(******************************************************************************)
theory i140326a_num_bin_hex_notation
imports Complex_Main
begin
(******************************************************************************)
(*NOTE
(1) The binary and hex notation for num can't prevent fun from directly
using the num constructors. One main use for fun is to do pattern matching
on binary and hex number patterns.
*)
notation
numeral ("N\<^sub>a:_" [1000] 1000)
abbreviation nat_numeral :: "num \<Rightarrow> nat" where
"nat_numeral n == (numeral n)::nat"
notation
nat_numeral ("N\<^sub>n:_" [1000] 1000)
notation
nat_of_num ("\<nn>:_" [1000] 1000)
notation
num_of_nat ("\<uu>:_" [1000] 1000)
notation Num.One ("1\<^sub>1:")
notation Num.Bit0 ("0:_" [1000] 1000)
notation Num.Bit1 ("1:_" [1000] 1000)
value "\<uu>:0b0000" (*.................One..*) (*.......0:0:0:0..................*)
value "\<uu>:0b0001" (* One *) value "\<nn>: 1\<^sub>1:" term " 1\<^sub>1:"
value "\<uu>:0b0010" (* Bit0 One *) value "\<nn>: 0:1\<^sub>1:" term " 0:1\<^sub>1:"
value "\<uu>:0b0011" (* Bit1 One *) value "\<nn>: 1:1\<^sub>1:" term " 1:1\<^sub>1:"
value "\<uu>:0b0100" (* Bit0 (Bit0 One) *) value "\<nn>: 0:0:1\<^sub>1:" term " 0:0:1\<^sub>1:"
value "\<uu>:0b0101" (* Bit1 (Bit0 One) *) value "\<nn>: 1:0:1\<^sub>1:" term " 1:0:1\<^sub>1:"
value "\<uu>:0b0110" (* Bit0 (Bit1 One) *) value "\<nn>: 0:1:1\<^sub>1:" term " 0:1:1\<^sub>1:"
value "\<uu>:0b0111" (* Bit1 (Bit1 One) *) value "\<nn>: 1:1:1\<^sub>1:" term " 1:1:1\<^sub>1:"
value "\<uu>:0b1000" (*Bit0 (Bit0 (Bit0 One))*) value "\<nn>:0:0:0:1\<^sub>1:" term "0:0:0:1\<^sub>1:"
value "\<uu>:0b1001" (*Bit1 (Bit0 (Bit0 One))*) value "\<nn>:1:0:0:1\<^sub>1:" term "1:0:0:1\<^sub>1:"
value "\<uu>:0b1010" (*Bit0 (Bit1 (Bit0 One))*) value "\<nn>:0:1:0:1\<^sub>1:" term "0:1:0:1\<^sub>1:"
value "\<uu>:0b1011" (*Bit1 (Bit1 (Bit0 One))*) value "\<nn>:1:1:0:1\<^sub>1:" term "1:1:0:1\<^sub>1:"
value "\<uu>:0b1100" (*Bit0 (Bit0 (Bit1 One))*) value "\<nn>:0:0:1:1\<^sub>1:" term "0:0:1:1\<^sub>1:"
value "\<uu>:0b1101" (*Bit1 (Bit0 (Bit1 One))*) value "\<nn>:1:0:1:1\<^sub>1:" term "1:0:1:1\<^sub>1:"
value "\<uu>:0b1110" (*Bit0 (Bit1 (Bit1 One))*) value "\<nn>:0:1:1:1\<^sub>1:" term "0:1:1:1\<^sub>1:"
value "\<uu>:0b1111" (*Bit1 (Bit1 (Bit1 One))*) value "\<nn>:1:1:1:1\<^sub>1:" term "1:1:1:1\<^sub>1:"
lemma "\<nn>:0:0:0:1\<^sub>1: = 0b1000" by simp
(*|HEX FIRST RIGHT DIGITS.|*)
(*|Digits 1-7 are used with nothing to the left, and 0 is never a first digit|*)
abbreviation (input) "h0x1 == 1\<^sub>1:" notation h0x1 ("1\<^sub>1\<cdot>")
abbreviation (input) "h0x2 == 0:1\<^sub>1:" notation h0x2 ("2\<^sub>1\<cdot>")
abbreviation (input) "h0x3 == 1:1\<^sub>1:" notation h0x3 ("3\<^sub>1\<cdot>")
abbreviation (input) "h0x4 == 0:0:1\<^sub>1:" notation h0x4 ("4\<^sub>1\<cdot>")
abbreviation (input) "h0x5 == 1:0:1\<^sub>1:" notation h0x5 ("5\<^sub>1\<cdot>")
abbreviation (input) "h0x6 == 0:1:1\<^sub>1:" notation h0x6 ("6\<^sub>1\<cdot>")
abbreviation (input) "h0x7 == 1:1:1\<^sub>1:" notation h0x7 ("7\<^sub>1\<cdot>")
(*|Digits 8-F can be used alone, or with digits to the left.|*)
abbreviation (input) "h0x8 == 0:0:0:1\<^sub>1:" notation h0x8 ("8\<^sub>1\<cdot>")
abbreviation (input) "h0x9 == 1:0:0:1\<^sub>1:" notation h0x9 ("9\<^sub>1\<cdot>")
abbreviation (input) "h0xA == 0:1:0:1\<^sub>1:" notation h0xA ("A\<^sub>1\<cdot>")
abbreviation (input) "h0xB == 1:1:0:1\<^sub>1:" notation h0xB ("B\<^sub>1\<cdot>")
abbreviation (input) "h0xC == 0:0:1:1\<^sub>1:" notation h0xC ("C\<^sub>1\<cdot>")
abbreviation (input) "h0xD == 1:0:1:1\<^sub>1:" notation h0xD ("D\<^sub>1\<cdot>")
abbreviation (input) "h0xE == 0:1:1:1\<^sub>1:" notation h0xE ("E\<^sub>1\<cdot>")
abbreviation (input) "h0xF == 1:1:1:1\<^sub>1:" notation h0xF ("F\<^sub>1\<cdot>")
(*|HEX MIDDLE DIGITS AND LEFT DIGITS|*)
abbreviation (input) lh0x0 :: "num \<Rightarrow> num" ("0\<cdot>_" [1000] 1000)
where "lh0x0 n == 0:0:0:0:n"
abbreviation (input) lh0x1 :: "num \<Rightarrow> num" ("1\<cdot>_" [1000] 1000)
where "lh0x1 n == 1:0:0:0:n"
abbreviation (input) lh0x2 :: "num \<Rightarrow> num" ("2\<cdot>_" [1000] 1000)
where "lh0x2 n == 0:1:0:0:n"
abbreviation (input) lh0x3 :: "num \<Rightarrow> num" ("3\<cdot>_" [1000] 1000)
where "lh0x3 n == 1:1:0:0:n"
abbreviation (input) lh0x4 :: "num \<Rightarrow> num" ("4\<cdot>_" [1000] 1000)
where "lh0x4 n == 0:0:1:0:n"
abbreviation (input) lh0x5 :: "num \<Rightarrow> num" ("5\<cdot>_" [1000] 1000)
where "lh0x5 n == 1:0:1:0:n"
abbreviation (input) lh0x6 :: "num \<Rightarrow> num" ("6\<cdot>_" [1000] 1000)
where "lh0x6 n == 0:1:1:0:n"
abbreviation (input) lh0x7 :: "num \<Rightarrow> num" ("7\<cdot>_" [1000] 1000)
where "lh0x7 n == 1:1:1:0:n"
abbreviation (input) lh0x8 :: "num \<Rightarrow> num" ("8\<cdot>_" [1000] 1000)
where "lh0x8 n == 0:0:0:1:n"
abbreviation (input) lh0x9 :: "num \<Rightarrow> num" ("9\<cdot>_" [1000] 1000)
where "lh0x9 n == 1:0:0:1:n"
abbreviation (input) lh0xA :: "num \<Rightarrow> num" ("A\<cdot>_" [1000] 1000)
where "lh0xA n == 0:1:0:1:n"
abbreviation (input) lh0xB :: "num \<Rightarrow> num" ("B\<cdot>_" [1000] 1000)
where "lh0xB n == 1:1:0:1:n"
abbreviation (input) lh0xC :: "num \<Rightarrow> num" ("C\<cdot>_" [1000] 1000)
where "lh0xC n == 0:0:1:1:n"
abbreviation (input) lh0xD :: "num \<Rightarrow> num" ("D\<cdot>_" [1000] 1000)
where "lh0xD n == 1:0:1:1:n"
abbreviation (input) lh0xE :: "num \<Rightarrow> num" ("E\<cdot>_" [1000] 1000)
where "lh0xE n == 0:1:1:1:n"
abbreviation (input) lh0xF :: "num \<Rightarrow> num" ("F\<cdot>_" [1000] 1000)
where "lh0xF n == 1:1:1:1:n"
lemma "N\<^sub>a:0\<cdot>1\<cdot>2\<cdot>3\<cdot>4\<cdot>5\<cdot>6\<cdot>7\<cdot>8\<cdot>9\<cdot>A\<cdot>B\<cdot>C\<cdot>D\<cdot>E\<cdot>F\<^sub>1\<cdot> = 0xFEDCBA9876543210"
by(rule refl)
lemma "N\<^sub>n:0\<cdot>1\<cdot>2\<cdot>3\<cdot>4\<cdot>5\<cdot>6\<cdot>7\<cdot>8\<cdot>9\<cdot>A\<cdot>B\<cdot>C\<cdot>D\<cdot>E\<cdot>F\<^sub>1\<cdot> = 0xFEDCBA9876543210"
by(rule refl)
value "\<nn>:1\<cdot>8\<^sub>1\<cdot>" term "1\<cdot>8\<^sub>1\<cdot>" value "numeral 1\<cdot>8\<^sub>1\<cdot>"
value "\<nn>:2\<cdot>8\<^sub>1\<cdot>" term "2\<cdot>8\<^sub>1\<cdot>" value "numeral 2\<cdot>8\<^sub>1\<cdot>"
value "\<nn>:3\<cdot>8\<^sub>1\<cdot>" term "3\<cdot>8\<^sub>1\<cdot>" value "numeral 3\<cdot>8\<^sub>1\<cdot>"
(******************************************************************************)
(* SHIFT OPERATIONS *)
(******************************************************************************)
fun num_left_shift :: "num \<Rightarrow> num" where
"num_left_shift 1\<^sub>1: = 1\<^sub>1:"
|"num_left_shift (0:1\<^sub>1:) = 1\<^sub>1:"
|"num_left_shift (1:1\<^sub>1:) = 1\<^sub>1:"
|"num_left_shift (0:0:n) = 0:(num_left_shift 0:n)"
|"num_left_shift (0:1:n) = 1:(num_left_shift 1:n)"
|"num_left_shift (1:0:n) = 0:(num_left_shift 0:n)"
|"num_left_shift (1:1:n) = 1:(num_left_shift 1:n)"
value "num_left_shift A\<cdot>A\<^sub>1\<cdot>"
value "num_left_shift 5\<cdot>D\<^sub>1\<cdot>"
(******************************************************************************)
end
(******************************************************************************)
https://stackoverflow.com/questions/22653029
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
Russian