(*Generated by Lem from num.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_boolTheory lem_basic_classesTheory integerTheory intReduce wordsTheory wordsLib ratTheory realTheory intrealTheory transcTheory;

val _ = numLib.prefer_num();



val _ = new_theory "lem_num"



(*open import Bool Basic_classes*)
(*open import {isabelle} `~~/src/HOL/Word/Word` `Real` `~~/src/HOL/NthRoot`*)
(*open import {hol} `integerTheory` `intReduce` `wordsTheory` `wordsLib` `ratTheory` `realTheory` `intrealTheory` `transcTheory`*)
(*open import {coq} `Coq.Numbers.BinNums` `Coq.ZArith.BinInt` `Coq.ZArith.Zpower` `Coq.ZArith.Zdiv` `Coq.ZArith.Zmax` `Coq.Numbers.Natural.Peano.NPeano` `Coq.QArith.Qabs` `Coq.QArith.Qminmax` `Coq.QArith.Qround` `Coq.Reals.ROrderedType` `Coq.Reals.Rbase` `Coq.Reals.Rfunctions`*) 

(*class inline ( Numeral 'a ) 
  val fromNumeral : numeral -> 'a 
end*)

(* ========================================================================== *)
(* Syntactic type-classes for common operations                               *)
(* ========================================================================== *)

(* Typeclasses can be used as a mean to overload constants like "+", "-", etc *)

val _ = Hol_datatype `
(*  'a *) NumNegate_class= <| 
  numNegate_method : 'a -> 'a 
|>`;


val _ = Hol_datatype `
(*  'a *) NumAbs_class= <| 
  abs_method : 'a -> 'a 
|>`;


val _ = Hol_datatype `
(*  'a *) NumAdd_class= <| 
  numAdd_method : 'a -> 'a -> 'a
|>`;


val _ = Hol_datatype `
(*  'a *) NumMinus_class= <| 
  numMinus_method : 'a -> 'a -> 'a
|>`;


val _ = Hol_datatype `
(*  'a *) NumMult_class= <| 
  numMult_method : 'a -> 'a -> 'a
|>`;


val _ = Hol_datatype `
(*  'a *) NumPow_class= <| 
  numPow_method : 'a -> num -> 'a
|>`;


val _ = Hol_datatype `
(*  'a *) NumDivision_class= <| 
  numDivision_method : 'a -> 'a -> 'a
|>`;


val _ = Hol_datatype `
(*  'a *) NumIntegerDivision_class= <| 
  div_method : 'a -> 'a -> 'a
|>`;



val _ = Hol_datatype `
(*  'a *) NumRemainder_class= <| 
  mod_method : 'a -> 'a -> 'a
|>`;


val _ = Hol_datatype `
(*  'a *) NumSucc_class= <| 
  succ_method : 'a -> 'a
|>`;


val _ = Hol_datatype `
(*  'a *) NumPred_class= <| 
  pred_method : 'a -> 'a
|>`;
 


(* ----------------------- *)
(* natural                 *)
(* ----------------------- *)

(* unbounded size natural numbers *)
(*type natural*)


(* ----------------------- *)
(* int                     *)
(* ----------------------- *)

(* bounded size integers with uncertain length *)

(*type int*)


(* ----------------------- *)
(* integer                 *)
(* ----------------------- *)

(* unbounded size integers *)

(*type integer*)

(* ----------------------- *)
(* bint                    *)
(* ----------------------- *)

(* TODO the bounded ints are only partially implemented, use with care. *)

(* 32 bit integers *)
(*type int32*) 

(* 64 bit integers *)
(*type int64*) 


(* ----------------------- *)
(* rational                *)
(* ----------------------- *)

(* unbounded size and precision rational numbers *)

(*type rational*) (* ???: better type for this in HOL? *)


(* ----------------------- *)
(* real                    *)
(* ----------------------- *)

(* real numbers *)
(* Note that for OCaml, this is mapped to floats with 64 bits. *)

(*type real*) (* ???: better type for this in HOL? *)


(* ----------------------- *)
(* double                  *)
(* ----------------------- *)

(* double precision floating point (64 bits) *)

(*type float64*) (* ???: better type for this in HOL? *)

(*type float32*) (* ???: better type for this in HOL? *)


(* ========================================================================== *)
(* Binding the standard operations for the number types                       *)
(* ========================================================================== *)


(* ----------------------- *)
(* nat                     *)
(* ----------------------- *)

(*val natFromNumeral : numeral -> nat*)

(*val natEq : nat -> nat -> bool*)

(*val natLess : nat -> nat -> bool*)
(*val natLessEqual : nat -> nat -> bool*)
(*val natGreater : nat -> nat -> bool*)
(*val natGreaterEqual : nat -> nat -> bool*)

(*val natCompare : nat -> nat -> ordering*)

val _ = Define `
((instance_Basic_classes_Ord_nat_dict:(num)Ord_class)= (<|

  compare_method := (genericCompare (<) (=));

  isLess_method := (<);

  isLessEqual_method := (<=);

  isGreater_method := (>);

  isGreaterEqual_method := (>=)|>))`;


(*val natAdd : nat -> nat -> nat*)

val _ = Define `
((instance_Num_NumAdd_nat_dict:(num)NumAdd_class)= (<|

  numAdd_method := (+)|>))`;


(*val natMinus : nat -> nat -> nat*)

val _ = Define `
((instance_Num_NumMinus_nat_dict:(num)NumMinus_class)= (<|

  numMinus_method := (-)|>))`;


(*val natSucc : nat -> nat*)
(*let natSucc n=  (Instance_Num_NumAdd_nat.+) n 1*)
val _ = Define `
((instance_Num_NumSucc_nat_dict:(num)NumSucc_class)= (<|

  succ_method := SUC|>))`;


(*val natPred : nat -> nat*)
val _ = Define `
((instance_Num_NumPred_nat_dict:(num)NumPred_class)= (<|

  pred_method := PRE|>))`;


(*val natMult : nat -> nat -> nat*)

val _ = Define `
((instance_Num_NumMult_nat_dict:(num)NumMult_class)= (<|

  numMult_method := ( * )|>))`;


(*val natDiv : nat -> nat -> nat*)

val _ = Define `
((instance_Num_NumIntegerDivision_nat_dict:(num)NumIntegerDivision_class)= (<|

  div_method := (DIV)|>))`;


val _ = Define `
((instance_Num_NumDivision_nat_dict:(num)NumDivision_class)= (<|

  numDivision_method := (DIV)|>))`;


(*val natMod : nat -> nat -> nat*)

val _ = Define `
((instance_Num_NumRemainder_nat_dict:(num)NumRemainder_class)= (<|

  mod_method := (MOD)|>))`;



(*val gen_pow_aux : forall 'a. ('a -> 'a -> 'a) -> 'a -> 'a -> nat -> 'a*)
 val _ = Define `
 ((gen_pow_aux:('a -> 'a -> 'a) -> 'a -> 'a -> num -> 'a) (mul : 'a -> 'a -> 'a) (a : 'a) (b : 'a) (e : num)=
    ((case e of
       0 => a (* cannot happen, call discipline guarentees e >= 1 *)
     | (SUC 0) => mul a b
     | (  (SUC(SUC e'))) => let e'' = (e DIV( 2 : num)) in
                   let a' = (if (e MOD( 2 : num)) =( 0 : num) then a else mul a b) in
                   gen_pow_aux mul a' (mul b b) e''
   )))`;

       
val _ = Define `
 ((gen_pow:'a ->('a -> 'a -> 'a) -> 'a -> num -> 'a) (one1 : 'a) (mul : 'a -> 'a -> 'a) (b : 'a) (e : num) : 'a= 
   (if e <( 0 : num) then one1 else 
  if (e =( 0 : num)) then one1 else gen_pow_aux mul one1 b e))`;


(*val natPow : nat -> nat -> nat*)

val _ = Define `
((instance_Num_NumPow_nat_dict:(num)NumPow_class)= (<|

  numPow_method := ( ** )|>))`;


(*val natMin : nat -> nat -> nat*)

(*val natMax : nat -> nat -> nat*)

val _ = Define `
((instance_Basic_classes_OrdMaxMin_nat_dict:(num)OrdMaxMin_class)= (<|

  max_method := MAX;

  min_method := MIN|>))`;



(* ----------------------- *)
(* natural                 *)
(* ----------------------- *)

(*val naturalFromNumeral : numeral -> natural*)

(*val naturalEq : natural -> natural -> bool*)

(*val naturalLess : natural -> natural -> bool*)
(*val naturalLessEqual : natural -> natural -> bool*)
(*val naturalGreater : natural -> natural -> bool*)
(*val naturalGreaterEqual : natural -> natural -> bool*)

(*val naturalCompare : natural -> natural -> ordering*)

val _ = Define `
((instance_Basic_classes_Ord_Num_natural_dict:(num)Ord_class)= (<|

  compare_method := (genericCompare (<) (=));

  isLess_method := (<);

  isLessEqual_method := (<=);

  isGreater_method := (>);

  isGreaterEqual_method := (>=)|>))`;


(*val naturalAdd : natural -> natural -> natural*)

val _ = Define `
((instance_Num_NumAdd_Num_natural_dict:(num)NumAdd_class)= (<|

  numAdd_method := (+)|>))`;


(*val naturalMinus : natural -> natural -> natural*)

val _ = Define `
((instance_Num_NumMinus_Num_natural_dict:(num)NumMinus_class)= (<|

  numMinus_method := (-)|>))`;


(*val naturalSucc : natural -> natural*)
(*let naturalSucc n=  (Instance_Num_NumAdd_Num_natural.+) n 1*)
val _ = Define `
((instance_Num_NumSucc_Num_natural_dict:(num)NumSucc_class)= (<|

  succ_method := SUC|>))`;


(*val naturalPred : natural -> natural*)
val _ = Define `
((instance_Num_NumPred_Num_natural_dict:(num)NumPred_class)= (<|

  pred_method := PRE|>))`;


(*val naturalMult : natural -> natural -> natural*)

val _ = Define `
((instance_Num_NumMult_Num_natural_dict:(num)NumMult_class)= (<|

  numMult_method := ( * )|>))`;



(*val naturalPow : natural -> nat -> natural*)

val _ = Define `
((instance_Num_NumPow_Num_natural_dict:(num)NumPow_class)= (<|

  numPow_method := ( ** )|>))`;


(*val naturalDiv : natural -> natural -> natural*)

val _ = Define `
((instance_Num_NumIntegerDivision_Num_natural_dict:(num)NumIntegerDivision_class)= (<|

  div_method := (DIV)|>))`;


val _ = Define `
((instance_Num_NumDivision_Num_natural_dict:(num)NumDivision_class)= (<|

  numDivision_method := (DIV)|>))`;


(*val naturalMod : natural -> natural -> natural*)

val _ = Define `
((instance_Num_NumRemainder_Num_natural_dict:(num)NumRemainder_class)= (<|

  mod_method := (MOD)|>))`;


(*val naturalMin : natural -> natural -> natural*)

(*val naturalMax : natural -> natural -> natural*)

val _ = Define `
((instance_Basic_classes_OrdMaxMin_Num_natural_dict:(num)OrdMaxMin_class)= (<|

  max_method := MAX;

  min_method := MIN|>))`;



(* ----------------------- *)
(* int                     *)
(* ----------------------- *)

(*val intFromNumeral : numeral -> int*)

(*val intEq : int -> int -> bool*)

(*val intLess : int -> int -> bool*)
(*val intLessEqual : int -> int -> bool*)
(*val intGreater : int -> int -> bool*)
(*val intGreaterEqual : int -> int -> bool*)

(*val intCompare : int -> int -> ordering*)

val _ = Define `
((instance_Basic_classes_Ord_Num_int_dict:(int)Ord_class)= (<|

  compare_method := (genericCompare (<) (=));

  isLess_method := (<);

  isLessEqual_method := (<=);

  isGreater_method := (>);

  isGreaterEqual_method := (>=)|>))`;


(*val intNegate : int -> int*)

val _ = Define `
((instance_Num_NumNegate_Num_int_dict:(int)NumNegate_class)= (<|

  numNegate_method := (\ i. ~ i)|>))`;


(*val intAbs : int -> int*) (* TODO: check *)

val _ = Define `
((instance_Num_NumAbs_Num_int_dict:(int)NumAbs_class)= (<|

  abs_method := ABS|>))`;


(*val intAdd : int -> int -> int*)

val _ = Define `
((instance_Num_NumAdd_Num_int_dict:(int)NumAdd_class)= (<|

  numAdd_method := (+)|>))`;


(*val intMinus : int -> int -> int*)

val _ = Define `
((instance_Num_NumMinus_Num_int_dict:(int)NumMinus_class)= (<|

  numMinus_method := (-)|>))`;


(*val intSucc : int -> int*)
val _ = Define `
((instance_Num_NumSucc_Num_int_dict:(int)NumSucc_class)= (<|

  succ_method := (\ n. n +( 1 : int))|>))`;


(*val intPred : int -> int*)
val _ = Define `
((instance_Num_NumPred_Num_int_dict:(int)NumPred_class)= (<|

  pred_method := (\ n. n -( 1 : int))|>))`;


(*val intMult : int -> int -> int*)

val _ = Define `
((instance_Num_NumMult_Num_int_dict:(int)NumMult_class)= (<|

  numMult_method := ( * )|>))`;



(*val intPow : int -> nat -> int*)

val _ = Define `
((instance_Num_NumPow_Num_int_dict:(int)NumPow_class)= (<|

  numPow_method := ( ** )|>))`;


(*val intDiv : int -> int -> int*)

val _ = Define `
((instance_Num_NumIntegerDivision_Num_int_dict:(int)NumIntegerDivision_class)= (<|

  div_method := (/)|>))`;


val _ = Define `
((instance_Num_NumDivision_Num_int_dict:(int)NumDivision_class)= (<|

  numDivision_method := (/)|>))`;


(*val intMod : int -> int -> int*)

val _ = Define `
((instance_Num_NumRemainder_Num_int_dict:(int)NumRemainder_class)= (<|

  mod_method := (%)|>))`;


(*val intMin : int -> int -> int*)

(*val intMax : int -> int -> int*)

val _ = Define `
((instance_Basic_classes_OrdMaxMin_Num_int_dict:(int)OrdMaxMin_class)= (<|

  max_method := int_max;

  min_method := int_min|>))`;


(* ----------------------- *)
(* int32                   *)
(* ----------------------- *)
(*val int32FromNumeral : numeral -> int32*)

(*val int32Eq : int32 -> int32 -> bool*)

(*val int32Less : int32 -> int32 -> bool*)
(*val int32LessEqual : int32 -> int32 -> bool*)
(*val int32Greater : int32 -> int32 -> bool*)
(*val int32GreaterEqual : int32 -> int32 -> bool*)

(*val int32Compare : int32 -> int32 -> ordering*)

val _ = Define `
((instance_Basic_classes_Ord_Num_int32_dict:(word32)Ord_class)= (<|

  compare_method := (genericCompare (<) (=));

  isLess_method := (<);

  isLessEqual_method := (<=);

  isGreater_method := (>);

  isGreaterEqual_method := (>=)|>))`;


(*val int32Negate : int32 -> int32*)

val _ = Define `
((instance_Num_NumNegate_Num_int32_dict:(word32)NumNegate_class)= (<|

  numNegate_method := (\ i. ((- i) : word32))|>))`;


(*val int32Abs : int32 -> int32*)
val _ = Define `
 ((int32Abs:word32 -> word32) i=  (if((n2w 0) : word32) <= i then i else ((- i) : word32)))`;


val _ = Define `
((instance_Num_NumAbs_Num_int32_dict:(word32)NumAbs_class)= (<|

  abs_method := int32Abs|>))`;



(*val int32Add : int32 -> int32 -> int32*)

val _ = Define `
((instance_Num_NumAdd_Num_int32_dict:(word32)NumAdd_class)= (<|

  numAdd_method := (\ i1 i2. ((word_add i1 i2) : word32))|>))`;


(*val int32Minus : int32 -> int32 -> int32*)

val _ = Define `
((instance_Num_NumMinus_Num_int32_dict:(word32)NumMinus_class)= (<|

  numMinus_method := (\ i1 i2. ((word_sub i1 i2) : word32))|>))`;


(*val int32Succ : int32 -> int32*)

val _ = Define `
((instance_Num_NumSucc_Num_int32_dict:(word32)NumSucc_class)= (<|

  succ_method := (\ n.  ((word_add n (((n2w 1) : word32))) : word32))|>))`;


(*val int32Pred : int32 -> int32*)
val _ = Define `
((instance_Num_NumPred_Num_int32_dict:(word32)NumPred_class)= (<|

  pred_method := (\ n.  ((word_sub n (((n2w 1) : word32))) : word32))|>))`;


(*val int32Mult : int32 -> int32 -> int32*)

val _ = Define `
((instance_Num_NumMult_Num_int32_dict:(word32)NumMult_class)= (<|

  numMult_method := (\ i1 i2. ((word_mul i1 i2) : word32))|>))`;



(*val int32Pow : int32 -> nat -> int32*)
val _ = Define `
 ((int32Pow:word32 -> num -> word32)=  (gen_pow(((n2w 1) : word32)) (\ i1 i2. ((word_mul i1 i2) : word32))))`;


val _ = Define `
((instance_Num_NumPow_Num_int32_dict:(word32)NumPow_class)= (<|

  numPow_method := int32Pow|>))`;


(*val int32Div : int32 -> int32 -> int32*)

val _ = Define `
((instance_Num_NumIntegerDivision_Num_int32_dict:(word32)NumIntegerDivision_class)= (<|

  div_method := (\ i1 i2. ((word_div i1 i2) : word32))|>))`;


val _ = Define `
((instance_Num_NumDivision_Num_int32_dict:(word32)NumDivision_class)= (<|

  numDivision_method := (\ i1 i2. ((word_div i1 i2) : word32))|>))`;


(*val int32Mod : int32 -> int32 -> int32*)

val _ = Define `
((instance_Num_NumRemainder_Num_int32_dict:(word32)NumRemainder_class)= (<|

  mod_method := (\ i1 i2. ((word_mod i1 i2) : word32))|>))`;


(*val int32Min : int32 -> int32 -> int32*)

(*val int32Max : int32 -> int32 -> int32*)

val _ = Define `
((instance_Basic_classes_OrdMaxMin_Num_int32_dict:(word32)OrdMaxMin_class)= (<|

  max_method := word_smax;

  min_method := word_smin|>))`;




(* ----------------------- *)
(* int64                   *)
(* ----------------------- *)
(*val int64FromNumeral : numeral -> int64*)

(*val int64Eq : int64 -> int64 -> bool*)

(*val int64Less : int64 -> int64 -> bool*)
(*val int64LessEqual : int64 -> int64 -> bool*)
(*val int64Greater : int64 -> int64 -> bool*)
(*val int64GreaterEqual : int64 -> int64 -> bool*)

(*val int64Compare : int64 -> int64 -> ordering*)

val _ = Define `
((instance_Basic_classes_Ord_Num_int64_dict:(word64)Ord_class)= (<|

  compare_method := (genericCompare (<) (=));

  isLess_method := (<);

  isLessEqual_method := (<=);

  isGreater_method := (>);

  isGreaterEqual_method := (>=)|>))`;


(*val int64Negate : int64 -> int64*)

val _ = Define `
((instance_Num_NumNegate_Num_int64_dict:(word64)NumNegate_class)= (<|

  numNegate_method := (\ i. ((- i) : word64))|>))`;


(*val int64Abs : int64 -> int64*)
val _ = Define `
 ((int64Abs:word64 -> word64) i=  (if((n2w 0) : word64) <= i then i else ((- i) : word64)))`;


val _ = Define `
((instance_Num_NumAbs_Num_int64_dict:(word64)NumAbs_class)= (<|

  abs_method := int64Abs|>))`;



(*val int64Add : int64 -> int64 -> int64*)

val _ = Define `
((instance_Num_NumAdd_Num_int64_dict:(word64)NumAdd_class)= (<|

  numAdd_method := (\ i1 i2. ((word_add i1 i2) : word64))|>))`;


(*val int64Minus : int64 -> int64 -> int64*)

val _ = Define `
((instance_Num_NumMinus_Num_int64_dict:(word64)NumMinus_class)= (<|

  numMinus_method := (\ i1 i2. ((word_sub i1 i2) : word64))|>))`;


(*val int64Succ : int64 -> int64*)

val _ = Define `
((instance_Num_NumSucc_Num_int64_dict:(word64)NumSucc_class)= (<|

  succ_method := (\ n.  ((word_add n (((n2w 1) : word64))) : word64))|>))`;


(*val int64Pred : int64 -> int64*)
val _ = Define `
((instance_Num_NumPred_Num_int64_dict:(word64)NumPred_class)= (<|

  pred_method := (\ n.  ((word_sub n (((n2w 1) : word64))) : word64))|>))`;


(*val int64Mult : int64 -> int64 -> int64*)

val _ = Define `
((instance_Num_NumMult_Num_int64_dict:(word64)NumMult_class)= (<|

  numMult_method := (\ i1 i2. ((word_mul i1 i2) : word64))|>))`;



(*val int64Pow : int64 -> nat -> int64*)
val _ = Define `
 ((int64Pow:word64 -> num -> word64)=  (gen_pow(((n2w 1) : word64)) (\ i1 i2. ((word_mul i1 i2) : word64))))`;


val _ = Define `
((instance_Num_NumPow_Num_int64_dict:(word64)NumPow_class)= (<|

  numPow_method := int64Pow|>))`;


(*val int64Div : int64 -> int64 -> int64*)

val _ = Define `
((instance_Num_NumIntegerDivision_Num_int64_dict:(word64)NumIntegerDivision_class)= (<|

  div_method := (\ i1 i2. ((word_div i1 i2) : word64))|>))`;


val _ = Define `
((instance_Num_NumDivision_Num_int64_dict:(word64)NumDivision_class)= (<|

  numDivision_method := (\ i1 i2. ((word_div i1 i2) : word64))|>))`;


(*val int64Mod : int64 -> int64 -> int64*)

val _ = Define `
((instance_Num_NumRemainder_Num_int64_dict:(word64)NumRemainder_class)= (<|

  mod_method := (\ i1 i2. ((word_mod i1 i2) : word64))|>))`;


(*val int64Min : int64 -> int64 -> int64*)

(*val int64Max : int64 -> int64 -> int64*)

val _ = Define `
((instance_Basic_classes_OrdMaxMin_Num_int64_dict:(word64)OrdMaxMin_class)= (<|

  max_method := word_smax;

  min_method := word_smin|>))`;



(* ----------------------- *)
(* integer                 *)
(* ----------------------- *)

(*val integerFromNumeral : numeral -> integer*)

(*val integerFromNat : nat -> integer*) (* TODO: check *)

(*val integerEq : integer -> integer -> bool*)

(*val integerLess : integer -> integer -> bool*)
(*val integerLessEqual : integer -> integer -> bool*)
(*val integerGreater : integer -> integer -> bool*)
(*val integerGreaterEqual : integer -> integer -> bool*)

(*val integerCompare : integer -> integer -> ordering*)

val _ = Define `
((instance_Basic_classes_Ord_Num_integer_dict:(int)Ord_class)= (<|

  compare_method := (genericCompare (<) (=));

  isLess_method := (<);

  isLessEqual_method := (<=);

  isGreater_method := (>);

  isGreaterEqual_method := (>=)|>))`;


(*val integerNegate : integer -> integer*)

val _ = Define `
((instance_Num_NumNegate_Num_integer_dict:(int)NumNegate_class)= (<|

  numNegate_method := (\ i. ~ i)|>))`;


(*val integerAbs : integer -> integer*) (* TODO: check *)

val _ = Define `
((instance_Num_NumAbs_Num_integer_dict:(int)NumAbs_class)= (<|

  abs_method := ABS|>))`;


(*val integerAdd : integer -> integer -> integer*)

val _ = Define `
((instance_Num_NumAdd_Num_integer_dict:(int)NumAdd_class)= (<|

  numAdd_method := (+)|>))`;


(*val integerMinus : integer -> integer -> integer*)

val _ = Define `
((instance_Num_NumMinus_Num_integer_dict:(int)NumMinus_class)= (<|

  numMinus_method := (-)|>))`;


(*val integerSucc : integer -> integer*)
val _ = Define `
((instance_Num_NumSucc_Num_integer_dict:(int)NumSucc_class)= (<|

  succ_method := (\ n. n +( 1 : int))|>))`;


(*val integerPred : integer -> integer*)
val _ = Define `
((instance_Num_NumPred_Num_integer_dict:(int)NumPred_class)= (<|

  pred_method := (\ n. n -( 1 : int))|>))`;


(*val integerMult : integer -> integer -> integer*)

val _ = Define `
((instance_Num_NumMult_Num_integer_dict:(int)NumMult_class)= (<|

  numMult_method := ( * )|>))`;



(*val integerPow : integer -> nat -> integer*)

val _ = Define `
((instance_Num_NumPow_Num_integer_dict:(int)NumPow_class)= (<|

  numPow_method := ( ** )|>))`;


(*val integerDiv : integer -> integer -> integer*)

val _ = Define `
((instance_Num_NumIntegerDivision_Num_integer_dict:(int)NumIntegerDivision_class)= (<|

  div_method := (/)|>))`;


val _ = Define `
((instance_Num_NumDivision_Num_integer_dict:(int)NumDivision_class)= (<|

  numDivision_method := (/)|>))`;


(*val integerMod : integer -> integer -> integer*)

val _ = Define `
((instance_Num_NumRemainder_Num_integer_dict:(int)NumRemainder_class)= (<|

  mod_method := (%)|>))`;


(*val integerMin : integer -> integer -> integer*)

(*val integerMax : integer -> integer -> integer*)

val _ = Define `
((instance_Basic_classes_OrdMaxMin_Num_integer_dict:(int)OrdMaxMin_class)= (<|

  max_method := int_max;

  min_method := int_min|>))`;




(* ----------------------- *)
(* rational                *)
(* ----------------------- *)

(*val rationalFromNumeral : numeral -> rational*)

(*val rationalFromInt : int -> rational*)

(*val rationalEq : rational -> rational -> bool*)

(*val rationalLess : rational -> rational -> bool*)
(*val rationalLessEqual : rational -> rational -> bool*)
(*val rationalGreater : rational -> rational -> bool*)
(*val rationalGreaterEqual : rational -> rational -> bool*)

(*val rationalCompare : rational -> rational -> ordering*)

val _ = Define `
((instance_Basic_classes_Ord_Num_rational_dict:(rat)Ord_class)= (<|

  compare_method := (genericCompare (<) (=));

  isLess_method := (<);

  isLessEqual_method := (<=);

  isGreater_method := (>);

  isGreaterEqual_method := (>=)|>))`;


(*val rationalAdd : rational -> rational -> rational*)

val _ = Define `
((instance_Num_NumAdd_Num_rational_dict:(rat)NumAdd_class)= (<|

  numAdd_method := (+)|>))`;


(*val rationalMinus : rational -> rational -> rational*)

val _ = Define `
((instance_Num_NumMinus_Num_rational_dict:(rat)NumMinus_class)= (<|

  numMinus_method := (-)|>))`;


(*val rationalNegate : rational -> rational*)

val _ = Define `
((instance_Num_NumNegate_Num_rational_dict:(rat)NumNegate_class)= (<|

  numNegate_method := (\ n. ( 0 : rat) - n)|>))`;


(*val rationalAbs : rational -> rational*)

val _ = Define `
((instance_Num_NumAbs_Num_rational_dict:(rat)NumAbs_class)= (<|

  abs_method := (\ n. (if n >( 0 : rat) then n else( 0 : rat) - n))|>))`;


(*val rationalSucc : rational -> rational*)
val _ = Define `
((instance_Num_NumSucc_Num_rational_dict:(rat)NumSucc_class)= (<|

  succ_method := (\ n. n +( 1 : rat))|>))`;


(*val rationalPred : rational -> rational*)
val _ = Define `
((instance_Num_NumPred_Num_rational_dict:(rat)NumPred_class)= (<|

  pred_method := (\ n. n -( 1 : rat))|>))`;


(*val rationalMult : rational -> rational -> rational*)

val _ = Define `
((instance_Num_NumMult_Num_rational_dict:(rat)NumMult_class)= (<|

  numMult_method := ( * )|>))`;


(*val rationalDiv : rational -> rational -> rational*)

val _ = Define `
((instance_Num_NumDivision_Num_rational_dict:(rat)NumDivision_class)= (<|

  numDivision_method := (/)|>))`;


(*val rationalFromFrac : int -> int -> rational*)
(*let rationalFromFrac n d=  (Instance_Num_NumDivision_Num_rational./) (rationalFromInt n) (rationalFromInt d)*)

(*val rationalPowInteger : rational -> integer -> rational*)
 val rationalPowInteger_defn = Hol_defn "rationalPowInteger" `
 ((rationalPowInteger:rat -> int -> rat) b e=
   (if e =( 0 : int) then( 1 : rat) else
  if e >( 0 : int) then rationalPowInteger b (e -( 1 : int)) * b else
  rationalPowInteger b (e +( 1 : int)) / b))`;

val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn rationalPowInteger_defn;

(*val rationalPowNat : rational -> nat -> rational*)
val _ = Define `
 ((rationalPowNat:rat -> num -> rat) r e=  (rationalPowInteger r (int_of_num e)))`;


val _ = Define `
((instance_Num_NumPow_Num_rational_dict:(rat)NumPow_class)= (<|

  numPow_method := rationalPowNat|>))`;


(*val rationalMin : rational -> rational -> rational*)

(*val rationalMax : rational -> rational -> rational*)

val _ = Define `
((instance_Basic_classes_OrdMaxMin_Num_rational_dict:(rat)OrdMaxMin_class)= (<|

  max_method := (maxByLessEqual (<=));

  min_method := (minByLessEqual (<=))|>))`;




(* ----------------------- *)
(* real                    *)
(* ----------------------- *)

(*val realFromNumeral : numeral -> real*)

(*val realFromInteger : integer -> real*)

(*val realEq : real -> real -> bool*)

(*val realLess : real -> real -> bool*)
(*val realLessEqual : real -> real -> bool*)
(*val realGreater : real -> real -> bool*)
(*val realGreaterEqual : real -> real -> bool*)

(*val realCompare : real -> real -> ordering*)

val _ = Define `
((instance_Basic_classes_Ord_Num_real_dict:(real)Ord_class)= (<|

  compare_method := (genericCompare (<) (=));

  isLess_method := (<);

  isLessEqual_method := (<=);

  isGreater_method := (>);

  isGreaterEqual_method := (>=)|>))`;


(*val realAdd : real -> real -> real*)

val _ = Define `
((instance_Num_NumAdd_Num_real_dict:(real)NumAdd_class)= (<|

  numAdd_method := (+)|>))`;


(*val realMinus : real -> real -> real*)

val _ = Define `
((instance_Num_NumMinus_Num_real_dict:(real)NumMinus_class)= (<|

  numMinus_method := (-)|>))`;


(*val realNegate : real -> real*)

val _ = Define `
((instance_Num_NumNegate_Num_real_dict:(real)NumNegate_class)= (<|

  numNegate_method := (\ n. (real_of_num 0) - n)|>))`;


(*val realAbs : real -> real*)

val _ = Define `
((instance_Num_NumAbs_Num_real_dict:(real)NumAbs_class)= (<|

  abs_method := (\ n. (if n >(real_of_num 0) then n else(real_of_num 0) - n))|>))`;


(*val realSucc : real -> real*)
val _ = Define `
((instance_Num_NumSucc_Num_real_dict:(real)NumSucc_class)= (<|

  succ_method := (\ n. n +(real_of_num 1))|>))`;


(*val realPred : real -> real*)
val _ = Define `
((instance_Num_NumPred_Num_real_dict:(real)NumPred_class)= (<|

  pred_method := (\ n. n -(real_of_num 1))|>))`;


(*val realMult : real -> real -> real*)

val _ = Define `
((instance_Num_NumMult_Num_real_dict:(real)NumMult_class)= (<|

  numMult_method := ( * )|>))`;


(*val realDiv : real -> real -> real*)

val _ = Define `
((instance_Num_NumDivision_Num_real_dict:(real)NumDivision_class)= (<|

  numDivision_method := (/)|>))`;


(*val realFromFrac : integer -> integer -> real*)
val _ = Define `
 ((realFromFrac:int -> int -> real) n d=  (((real_of_int n)) / ((real_of_int d))))`;


(*val realPowInteger : real -> integer -> real*)
 val realPowInteger_defn = Hol_defn "realPowInteger" `
 ((realPowInteger:real -> int -> real) b e=
   (if e =( 0 : int) then(real_of_num 1) else
  if e >( 0 : int) then realPowInteger b (e -( 1 : int)) * b else
  realPowInteger b (e +( 1 : int)) / b))`;

val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn realPowInteger_defn;

(*val realPowNat : real -> nat -> real*)
(*let realPowNat r e=  realPowInteger r (integerFromNat e)*)

val _ = Define `
((instance_Num_NumPow_Num_real_dict:(real)NumPow_class)= (<|

  numPow_method := (pow)|>))`;


(*val realSqrt : real -> real*)

(*val realMin : real -> real -> real*)

(*val realMax : real -> real -> real*)

val _ = Define `
((instance_Basic_classes_OrdMaxMin_Num_real_dict:(real)OrdMaxMin_class)= (<|

  max_method := max;

  min_method := min|>))`;


(*val realCeiling : real -> integer*)

(*val realFloor : real -> integer*)

(* ========================================================================== *)
(* Translation between number types                                           *)
(* ========================================================================== *)

(******************)
(* integerFrom... *)
(******************)

(*val integerFromInt : int -> integer*)

(*val integerFromNatural : natural -> integer*)


(*val integerFromInt32 : int32 -> integer*)


(*val integerFromInt64 : int64 -> integer*)


(******************)
(* naturalFrom... *)
(******************)

(*val naturalFromNat : nat -> natural*)

(*val naturalFromInteger : integer -> natural*)


(******************)
(* intFrom ...    *)
(******************)

(*val intFromInteger : integer -> int*)

(*val intFromNat : nat -> int*)


(******************)
(* natFrom ...    *)
(******************)

(*val natFromNatural : natural -> nat*)

(*val natFromInt : int -> nat*)


(******************)
(* int32From ...  *)
(******************)

(*val int32FromNat : nat -> int32*)

(*val int32FromNatural : natural -> int32*)

(*val int32FromInteger : integer -> int32*)
val _ = Define `
 ((int32FromInteger:int -> word32) i=  (
  let abs_int32 = (((n2w (Num (ABS i))) : word32)) in
  if (i <( 0 : int)) then (((- abs_int32) : word32)) else abs_int32 
))`;


(*val int32FromInt : int -> int32*)
val _ = Define `
 ((int32FromInt:int -> word32) i=  (int32FromInteger ( i)))`;



(*val int32FromInt64 : int64 -> int32*)
(*let int32FromInt64 i=  int32FromInteger (integerFromInt64 i)*)




(******************)
(* int64From ...  *)
(******************)

(*val int64FromNat : nat -> int64*)

(*val int64FromNatural : natural -> int64*)

(*val int64FromInteger : integer -> int64*)
val _ = Define `
 ((int64FromInteger:int -> word64) i=  (
  let abs_int64 = (((n2w (Num (ABS i))) : word64)) in
  if (i <( 0 : int)) then (((- abs_int64) : word64)) else abs_int64 
))`;


(*val int64FromInt : int -> int64*)
val _ = Define `
 ((int64FromInt:int -> word64) i=  (int64FromInteger ( i)))`;



(*val int64FromInt32 : int32 -> int64*)
(*let int64FromInt32 i=  int64FromInteger (integerFromInt32 i)*)


(******************)
(* what's missing *)
(******************)

(*val naturalFromInt : int -> natural*)
(*val naturalFromInt32 : int32 -> natural*)
(*val naturalFromInt64 : int64 -> natural*)


(*val intFromNatural : natural -> int*)
(*val intFromInt32 : int32 -> int*)
(*val intFromInt64 : int64 -> int*)

(*val natFromInteger : integer -> nat*)
(*val natFromInt32 : int32 -> nat*)
(*val natFromInt64 : int64 -> nat*)
val _ = export_theory()