Email Gateway (Aug 19 2022 at 14:04): Email Gateway (Aug 19 2022 at 14:04):From: Gottfried Barrow <igbi@gmx.com>
There are:
(1) the "num" datatype,
(2) the "numeral" type class,
(3) the "numeral :: num => 'a" function in the numeral type class,
(4) and the "num_of_nat :: nat => num" function.
So, I make this goal:
GOAL: Never use the numeral type class directly. Only access numerals,
which are polymorphic, through nat.
To explain that, I list some "huge facts":
(1) The use of numbers in a number system needs to be consistent,
practical, and unified, in particular, the use of number system constants.
(2) The need for pattern matching with numbers is huge!
(3) The need for recursive functions with numbers is huge!
(4) Facilitating the magic of "fun" for pattern matching and recursion,
especially with "nat", is huge, huge, huge!
Types and the need for type coercion complicate things. As I show in the
source, the usual subset hierarchy from nat, int, rat, to real is not
seamless. Even if it was seamless, there are more needs that just to
have that hierarchy be seamless.
What are rational numbers? Abstract rationals are functions which take
natural number arguments. I can think of 6 types of rational numbers, 5
of which I list using 5 functions that I've defined:
(1) natN, the natural numbers.
(2) natZ, the integers.
(3) natQ, fractions.
(4) natQm, mixed numbers.
(5) natQd, terminating decimal numbers.
(6) Non-terminating decimal numbers, which would be a notationally messy
form of natQd involving an infinite sum [Wiki].
If I have functions which give me the rational numbers, which are
functions that take natural numbers, then the irrational numbers are
special constants, or functions which take those constants and/or
rational numbers (which are functions which take natural numbers).
Beyond that, it's just a matter of setting up all the notation for those
functions. Unless it's not like that at all.
I include and attach the source.
Regards,
GB
[Wiki] http://en.wikipedia.org/wiki/Decimal#Other_rational_numbers
(******************)
theory z140323a__numeral_nat_of_num_front_for_numerals
imports Complex_Main
begin
(******************)
(* AUTO COERCIONS: NAT & INT DON'T COERCE TO RAT, RAT DOESN'T TO REAL *)
(******************)
(yes) term "(3::nat)::int"
(no)(term "(3::nat)::rat")
(no)(term "(3::int)::rat")
(yes) term "(3::nat)::real"
(no)(term "(3::rat)::real")
(yes) term "(3::int)::real"
(******************)
(* NUMBER OF DIGITS IN A NAT *)
(******************)
fun dec_digits :: "nat => nat" where
"dec_digits n = (if (n div 10 = 0) then 1 else 1 + dec_digits(n div 10))"
fun bin_digits :: "nat => nat" where
"bin_digits n = (if (n div 0b10 = 0) then 1 else 1 + bin_digits(n div
0b10))"
fun hex_digits :: "nat => nat" where
"hex_digits n = (if (n div 0x10 = 0) then 1 else 1 + hex_digits(n div
0x10))"
value "dec_digits 5555 = 4" (True)
value "bin_digits 0b1111111111 = 10" (True)
value "hex_digits 0xfff = 3" (True)
value "hex_digits 2048 = 3" (True)
(******************)
(* natN, natZ: ABSTRACT NAT AND INTEGER *)
(******************)
(*NOTES:
(1) Rather than curry natZ, I use (nat * nat). This will allow me to be
able to
work with sets of (nat * nat). Similarly, I use ((nat*nat) * (nat*nat))
as a rational.
(2) "One = num_of_nat 0" and "One = num_of_nat 1", which means I need class
zero.
(a) It's not as simple as "numeral(num_of_nat n) - numeral(num_of_nat m)".
(b) class numeral = one + semigroup_add, so numeral doesn't have zero.
(c) class neg_numeral = numeral + group_add, so neg_numeral has zero.
*)
fun natN :: "nat => 'a::{zero,numeral}" where
"natN 0 = 0"
|"natN n = numeral(num_of_nat n)"
value "(natN 0::nat) = 0"
value "(numeral(num_of_nat 0)::nat) = 1"
fun natZ :: "(nat * nat) => 'a::neg_numeral" where
"natZ (0,0) = 0"
|"natZ (n,0) = numeral(num_of_nat n)"
|"natZ (0,n) = -numeral(num_of_nat n)"
|"natZ (n,m) = numeral(num_of_nat n) - numeral(num_of_nat m)"
term "natZ"
value "(natZ (0,0)::int) = 0"
value "(natZ (3,0)::int) = 3"
value "(natZ (0,3)::int) = -3"
value "(natZ (5,3)::int) = 2"
value "(natZ (3,5)::int) = -2"
value "(natZ (0,0)::'a::neg_numeral) = 0"
value "(natZ (3,0)::'a::neg_numeral) = 3"
value "(natZ (0,3)::'a::neg_numeral) = -3"
value "(natZ (5,3)::'a::neg_numeral) = 2"
value "(natZ (3,5)::'a::neg_numeral) = -2"
(******************)
(* natQ FRACTION *)
(******************)
fun natQ :: "((nat * nat) * (nat * nat)) => 'a::{neg_numeral,inverse}"
where
"natQ (n,d) = natZ n / natZ d"
value "natQ ((5,2),(2,4))::rat" (* -3/2 *)
value "natQ ((5,2),(2,4))::'a::{neg_numeral,inverse}"
(******************)
(* natQm MIXED NUMBER *)
(******************)
abbreviation (input) natQm
:: "(nat * nat) => ((nat * nat) * (nat * nat)) =>
'a::{neg_numeral,inverse}"
where "natQm i q == natZ i + natQ q"
term "natQm (3,0) ((5,2),(2,4))" (* 3 3/-2 *)
value "natQm (3,0) ((5,2),(2,4))::rat" (* 3/2 *)
value "natQm (3,0) ((3,0),(0,2))::'a::{neg_numeral,inverse}"
value "natQm (3,0) ((5,2),(2,4))::'a::{neg_numeral,inverse}"
(******************)
(* natQd TERMINATING DECIMAL NUMBER *)
(******************)
(*NOTE: The digits argument allows for functions that more efficiently
calculate the number of digits in frac.*)
abbreviation (input) natQd
:: "(nat => nat) => (nat * nat) => nat => 'a::{neg_numeral,inverse}"
where "natQd digits i frac == natQm i ((frac,0),(10 ^ (digits frac),0))"
term "(natQd dec_digits (3,0) 123)" (* 3.123 *)
value "(natQd dec_digits (3,0) 123)::rat" (* 3123/1000*)
value "(natQd dec_digits (3,0) 123)::'a::{neg_numeral,inverse}"
(******************)
(******************)
(* natZA: ABS_INTEG VERSION *)
(******************)
(******************)
(*
(1) Here I use Abs_Integ to try to be more efficient, but value doesn't
simplify Abs_Integ.
(2) Above, the 4th case, natZ n m, is inefficient for quotient_type
integers.
(a) For ints, subtraction is "%(x, y) (u, v). (x + v, y + u)", so
2 - 3 = natZ 2 3 is "%(2,0) (3,0). (2 + 0, 0 + 3)", which will get
expanded to (1 + 1 + (0 + 0 + 0), 0 + 0 + (1 + 1 + 1)).
(b) This might not be important. I don't think I would use that case much.
*)
fun natZA :: "(nat * nat) => int" where
"natZA (0,0) = 0"
|"natZA (n,0) = numeral(num_of_nat n)"
|"natZA (0,n) = -numeral(num_of_nat n)"
|"natZA (n,m) = Abs_Integ(numeral(num_of_nat n), numeral(num_of_nat m))"
value "natZA (0,0)::int"
value "natZA (3,0)::int"
value "natZA (0,3)::int"
value "natZA (3,5)::int"
value "natZA (5,3)::int"
value "natZA (1,2)::int" (Abs_Integ (Suc (0∷nat), Suc (Suc (0∷nat))))
(******************)
end
(******************)
z140323a__numeral_nat_of_num_front_for_numerals.thy
Last updated: Nov 21 2024 at 12:39 UTC