(******************************************************************************)
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\<Colon>nat), Suc (Suc (0\<Colon>nat)))*)

(******************************************************************************)
end
(******************************************************************************)