chapter \Generated by Lem from \num.lem\.\ theory "Lem_num" imports Main "Lem_bool" "Lem_basic_classes" "HOL-Word.Word" "Complex_Main" begin (*open import Bool Basic_classes*) (*open import {isabelle} `HOL-Word.Word` `Complex_Main`*) (*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 *) record 'a NumNegate_class= numNegate_method ::" 'a \ 'a " record 'a NumAbs_class= abs_method ::" 'a \ 'a " record 'a NumAdd_class= numAdd_method ::" 'a \ 'a \ 'a " record 'a NumMinus_class= numMinus_method ::" 'a \ 'a \ 'a " record 'a NumMult_class= numMult_method ::" 'a \ 'a \ 'a " record 'a NumPow_class= numPow_method ::" 'a \ nat \ 'a " record 'a NumDivision_class= numDivision_method ::" 'a \ 'a \ 'a " record 'a NumIntegerDivision_class= div_method ::" 'a \ 'a \ 'a " record 'a NumRemainder_class= mod_method ::" 'a \ 'a \ 'a " record 'a NumSucc_class= succ_method ::" 'a \ 'a " record '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*) definition instance_Basic_classes_Ord_nat_dict :: "(nat)Ord_class " where " instance_Basic_classes_Ord_nat_dict = ((| compare_method = (genericCompare (<) (=)), isLess_method = (<), isLessEqual_method = (\), isGreater_method = (>), isGreaterEqual_method = (\)|) )" (*val natAdd : nat -> nat -> nat*) definition instance_Num_NumAdd_nat_dict :: "(nat)NumAdd_class " where " instance_Num_NumAdd_nat_dict = ((| numAdd_method = (+)|) )" (*val natMinus : nat -> nat -> nat*) definition instance_Num_NumMinus_nat_dict :: "(nat)NumMinus_class " where " instance_Num_NumMinus_nat_dict = ((| numMinus_method = (-)|) )" (*val natSucc : nat -> nat*) (*let natSucc n= (Instance_Num_NumAdd_nat.+) n 1*) definition instance_Num_NumSucc_nat_dict :: "(nat)NumSucc_class " where " instance_Num_NumSucc_nat_dict = ((| succ_method = Suc |) )" (*val natPred : nat -> nat*) definition instance_Num_NumPred_nat_dict :: "(nat)NumPred_class " where " instance_Num_NumPred_nat_dict = ((| pred_method = (\ n. n -( 1 :: nat))|) )" (*val natMult : nat -> nat -> nat*) definition instance_Num_NumMult_nat_dict :: "(nat)NumMult_class " where " instance_Num_NumMult_nat_dict = ((| numMult_method = ( * )|) )" (*val natDiv : nat -> nat -> nat*) definition instance_Num_NumIntegerDivision_nat_dict :: "(nat)NumIntegerDivision_class " where " instance_Num_NumIntegerDivision_nat_dict = ((| div_method = (div)|) )" definition instance_Num_NumDivision_nat_dict :: "(nat)NumDivision_class " where " instance_Num_NumDivision_nat_dict = ((| numDivision_method = (div)|) )" (*val natMod : nat -> nat -> nat*) definition instance_Num_NumRemainder_nat_dict :: "(nat)NumRemainder_class " where " instance_Num_NumRemainder_nat_dict = ((| mod_method = (mod)|) )" (*val gen_pow_aux : forall 'a. ('a -> 'a -> 'a) -> 'a -> 'a -> nat -> 'a*) fun gen_pow_aux :: "('a \ 'a \ 'a)\ 'a \ 'a \ nat \ 'a " where " gen_pow_aux (mul :: 'a \ 'a \ 'a) (a :: 'a) (b :: 'a) (e :: nat) = ( (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 :: nat)) in (let a' = (if (e mod( 2 :: nat)) =( 0 :: nat) then a else mul a b) in gen_pow_aux mul a' (mul b b) e'')) ))" definition gen_pow :: " 'a \('a \ 'a \ 'a)\ 'a \ nat \ 'a " where " gen_pow (one :: 'a) (mul :: 'a \ 'a \ 'a) (b :: 'a) (e :: nat) = ( if e <( 0 :: nat) then one else if (e =( 0 :: nat)) then one else gen_pow_aux mul one b e )" (*val natPow : nat -> nat -> nat*) definition instance_Num_NumPow_nat_dict :: "(nat)NumPow_class " where " instance_Num_NumPow_nat_dict = ((| numPow_method = (^)|) )" (*val natMin : nat -> nat -> nat*) (*val natMax : nat -> nat -> nat*) definition instance_Basic_classes_OrdMaxMin_nat_dict :: "(nat)OrdMaxMin_class " where " instance_Basic_classes_OrdMaxMin_nat_dict = ((| 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*) definition instance_Basic_classes_Ord_Num_natural_dict :: "(nat)Ord_class " where " instance_Basic_classes_Ord_Num_natural_dict = ((| compare_method = (genericCompare (<) (=)), isLess_method = (<), isLessEqual_method = (\), isGreater_method = (>), isGreaterEqual_method = (\)|) )" (*val naturalAdd : natural -> natural -> natural*) definition instance_Num_NumAdd_Num_natural_dict :: "(nat)NumAdd_class " where " instance_Num_NumAdd_Num_natural_dict = ((| numAdd_method = (+)|) )" (*val naturalMinus : natural -> natural -> natural*) definition instance_Num_NumMinus_Num_natural_dict :: "(nat)NumMinus_class " where " instance_Num_NumMinus_Num_natural_dict = ((| numMinus_method = (-)|) )" (*val naturalSucc : natural -> natural*) (*let naturalSucc n= (Instance_Num_NumAdd_Num_natural.+) n 1*) definition instance_Num_NumSucc_Num_natural_dict :: "(nat)NumSucc_class " where " instance_Num_NumSucc_Num_natural_dict = ((| succ_method = Suc |) )" (*val naturalPred : natural -> natural*) definition instance_Num_NumPred_Num_natural_dict :: "(nat)NumPred_class " where " instance_Num_NumPred_Num_natural_dict = ((| pred_method = (\ n. n -( 1 :: nat))|) )" (*val naturalMult : natural -> natural -> natural*) definition instance_Num_NumMult_Num_natural_dict :: "(nat)NumMult_class " where " instance_Num_NumMult_Num_natural_dict = ((| numMult_method = ( * )|) )" (*val naturalPow : natural -> nat -> natural*) definition instance_Num_NumPow_Num_natural_dict :: "(nat)NumPow_class " where " instance_Num_NumPow_Num_natural_dict = ((| numPow_method = (^)|) )" (*val naturalDiv : natural -> natural -> natural*) definition instance_Num_NumIntegerDivision_Num_natural_dict :: "(nat)NumIntegerDivision_class " where " instance_Num_NumIntegerDivision_Num_natural_dict = ((| div_method = (div)|) )" definition instance_Num_NumDivision_Num_natural_dict :: "(nat)NumDivision_class " where " instance_Num_NumDivision_Num_natural_dict = ((| numDivision_method = (div)|) )" (*val naturalMod : natural -> natural -> natural*) definition instance_Num_NumRemainder_Num_natural_dict :: "(nat)NumRemainder_class " where " instance_Num_NumRemainder_Num_natural_dict = ((| mod_method = (mod)|) )" (*val naturalMin : natural -> natural -> natural*) (*val naturalMax : natural -> natural -> natural*) definition instance_Basic_classes_OrdMaxMin_Num_natural_dict :: "(nat)OrdMaxMin_class " where " instance_Basic_classes_OrdMaxMin_Num_natural_dict = ((| 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*) definition instance_Basic_classes_Ord_Num_int_dict :: "(int)Ord_class " where " instance_Basic_classes_Ord_Num_int_dict = ((| compare_method = (genericCompare (<) (=)), isLess_method = (<), isLessEqual_method = (\), isGreater_method = (>), isGreaterEqual_method = (\)|) )" (*val intNegate : int -> int*) definition instance_Num_NumNegate_Num_int_dict :: "(int)NumNegate_class " where " instance_Num_NumNegate_Num_int_dict = ((| numNegate_method = (\ i. - i)|) )" (*val intAbs : int -> int*) (* TODO: check *) definition instance_Num_NumAbs_Num_int_dict :: "(int)NumAbs_class " where " instance_Num_NumAbs_Num_int_dict = ((| abs_method = abs |) )" (*val intAdd : int -> int -> int*) definition instance_Num_NumAdd_Num_int_dict :: "(int)NumAdd_class " where " instance_Num_NumAdd_Num_int_dict = ((| numAdd_method = (+)|) )" (*val intMinus : int -> int -> int*) definition instance_Num_NumMinus_Num_int_dict :: "(int)NumMinus_class " where " instance_Num_NumMinus_Num_int_dict = ((| numMinus_method = (-)|) )" (*val intSucc : int -> int*) definition instance_Num_NumSucc_Num_int_dict :: "(int)NumSucc_class " where " instance_Num_NumSucc_Num_int_dict = ((| succ_method = (\ n. n +( 1 :: int))|) )" (*val intPred : int -> int*) definition instance_Num_NumPred_Num_int_dict :: "(int)NumPred_class " where " instance_Num_NumPred_Num_int_dict = ((| pred_method = (\ n. n -( 1 :: int))|) )" (*val intMult : int -> int -> int*) definition instance_Num_NumMult_Num_int_dict :: "(int)NumMult_class " where " instance_Num_NumMult_Num_int_dict = ((| numMult_method = ( * )|) )" (*val intPow : int -> nat -> int*) definition instance_Num_NumPow_Num_int_dict :: "(int)NumPow_class " where " instance_Num_NumPow_Num_int_dict = ((| numPow_method = (^)|) )" (*val intDiv : int -> int -> int*) definition instance_Num_NumIntegerDivision_Num_int_dict :: "(int)NumIntegerDivision_class " where " instance_Num_NumIntegerDivision_Num_int_dict = ((| div_method = (div)|) )" definition instance_Num_NumDivision_Num_int_dict :: "(int)NumDivision_class " where " instance_Num_NumDivision_Num_int_dict = ((| numDivision_method = (div)|) )" (*val intMod : int -> int -> int*) definition instance_Num_NumRemainder_Num_int_dict :: "(int)NumRemainder_class " where " instance_Num_NumRemainder_Num_int_dict = ((| mod_method = (mod)|) )" (*val intMin : int -> int -> int*) (*val intMax : int -> int -> int*) definition instance_Basic_classes_OrdMaxMin_Num_int_dict :: "(int)OrdMaxMin_class " where " instance_Basic_classes_OrdMaxMin_Num_int_dict = ((| max_method = max, min_method = 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*) definition instance_Basic_classes_Ord_Num_int32_dict :: "( 32 word)Ord_class " where " instance_Basic_classes_Ord_Num_int32_dict = ((| compare_method = (genericCompare word_sless (=)), isLess_method = word_sless, isLessEqual_method = word_sle, isGreater_method = (\ x y. word_sless y x), isGreaterEqual_method = (\ x y. word_sle y x)|) )" (*val int32Negate : int32 -> int32*) definition instance_Num_NumNegate_Num_int32_dict :: "( 32 word)NumNegate_class " where " instance_Num_NumNegate_Num_int32_dict = ((| numNegate_method = (\ i. - i)|) )" (*val int32Abs : int32 -> int32*) definition int32Abs :: " 32 word \ 32 word " where " int32Abs i = ( (if word_sle(((word_of_int 0) :: 32 word)) i then i else - i))" definition instance_Num_NumAbs_Num_int32_dict :: "( 32 word)NumAbs_class " where " instance_Num_NumAbs_Num_int32_dict = ((| abs_method = int32Abs |) )" (*val int32Add : int32 -> int32 -> int32*) definition instance_Num_NumAdd_Num_int32_dict :: "( 32 word)NumAdd_class " where " instance_Num_NumAdd_Num_int32_dict = ((| numAdd_method = (+)|) )" (*val int32Minus : int32 -> int32 -> int32*) definition instance_Num_NumMinus_Num_int32_dict :: "( 32 word)NumMinus_class " where " instance_Num_NumMinus_Num_int32_dict = ((| numMinus_method = (-)|) )" (*val int32Succ : int32 -> int32*) definition instance_Num_NumSucc_Num_int32_dict :: "( 32 word)NumSucc_class " where " instance_Num_NumSucc_Num_int32_dict = ((| succ_method = (\ n. n +((word_of_int 1) :: 32 word))|) )" (*val int32Pred : int32 -> int32*) definition instance_Num_NumPred_Num_int32_dict :: "( 32 word)NumPred_class " where " instance_Num_NumPred_Num_int32_dict = ((| pred_method = (\ n. n -((word_of_int 1) :: 32 word))|) )" (*val int32Mult : int32 -> int32 -> int32*) definition instance_Num_NumMult_Num_int32_dict :: "( 32 word)NumMult_class " where " instance_Num_NumMult_Num_int32_dict = ((| numMult_method = ( * )|) )" (*val int32Pow : int32 -> nat -> int32*) definition instance_Num_NumPow_Num_int32_dict :: "( 32 word)NumPow_class " where " instance_Num_NumPow_Num_int32_dict = ((| numPow_method = (^)|) )" (*val int32Div : int32 -> int32 -> int32*) definition instance_Num_NumIntegerDivision_Num_int32_dict :: "( 32 word)NumIntegerDivision_class " where " instance_Num_NumIntegerDivision_Num_int32_dict = ((| div_method = (div)|) )" definition instance_Num_NumDivision_Num_int32_dict :: "( 32 word)NumDivision_class " where " instance_Num_NumDivision_Num_int32_dict = ((| numDivision_method = (div)|) )" (*val int32Mod : int32 -> int32 -> int32*) definition instance_Num_NumRemainder_Num_int32_dict :: "( 32 word)NumRemainder_class " where " instance_Num_NumRemainder_Num_int32_dict = ((| mod_method = (mod)|) )" (*val int32Min : int32 -> int32 -> int32*) (*val int32Max : int32 -> int32 -> int32*) definition instance_Basic_classes_OrdMaxMin_Num_int32_dict :: "( 32 word)OrdMaxMin_class " where " instance_Basic_classes_OrdMaxMin_Num_int32_dict = ((| max_method = ((\ x y. if (word_sle y x) then x else y)), min_method = ((\ x y. if (word_sle x y) then x else y))|) )" (* ----------------------- *) (* 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*) definition instance_Basic_classes_Ord_Num_int64_dict :: "( 64 word)Ord_class " where " instance_Basic_classes_Ord_Num_int64_dict = ((| compare_method = (genericCompare word_sless (=)), isLess_method = word_sless, isLessEqual_method = word_sle, isGreater_method = (\ x y. word_sless y x), isGreaterEqual_method = (\ x y. word_sle y x)|) )" (*val int64Negate : int64 -> int64*) definition instance_Num_NumNegate_Num_int64_dict :: "( 64 word)NumNegate_class " where " instance_Num_NumNegate_Num_int64_dict = ((| numNegate_method = (\ i. - i)|) )" (*val int64Abs : int64 -> int64*) definition int64Abs :: " 64 word \ 64 word " where " int64Abs i = ( (if word_sle(((word_of_int 0) :: 64 word)) i then i else - i))" definition instance_Num_NumAbs_Num_int64_dict :: "( 64 word)NumAbs_class " where " instance_Num_NumAbs_Num_int64_dict = ((| abs_method = int64Abs |) )" (*val int64Add : int64 -> int64 -> int64*) definition instance_Num_NumAdd_Num_int64_dict :: "( 64 word)NumAdd_class " where " instance_Num_NumAdd_Num_int64_dict = ((| numAdd_method = (+)|) )" (*val int64Minus : int64 -> int64 -> int64*) definition instance_Num_NumMinus_Num_int64_dict :: "( 64 word)NumMinus_class " where " instance_Num_NumMinus_Num_int64_dict = ((| numMinus_method = (-)|) )" (*val int64Succ : int64 -> int64*) definition instance_Num_NumSucc_Num_int64_dict :: "( 64 word)NumSucc_class " where " instance_Num_NumSucc_Num_int64_dict = ((| succ_method = (\ n. n +((word_of_int 1) :: 64 word))|) )" (*val int64Pred : int64 -> int64*) definition instance_Num_NumPred_Num_int64_dict :: "( 64 word)NumPred_class " where " instance_Num_NumPred_Num_int64_dict = ((| pred_method = (\ n. n -((word_of_int 1) :: 64 word))|) )" (*val int64Mult : int64 -> int64 -> int64*) definition instance_Num_NumMult_Num_int64_dict :: "( 64 word)NumMult_class " where " instance_Num_NumMult_Num_int64_dict = ((| numMult_method = ( * )|) )" (*val int64Pow : int64 -> nat -> int64*) definition instance_Num_NumPow_Num_int64_dict :: "( 64 word)NumPow_class " where " instance_Num_NumPow_Num_int64_dict = ((| numPow_method = (^)|) )" (*val int64Div : int64 -> int64 -> int64*) definition instance_Num_NumIntegerDivision_Num_int64_dict :: "( 64 word)NumIntegerDivision_class " where " instance_Num_NumIntegerDivision_Num_int64_dict = ((| div_method = (div)|) )" definition instance_Num_NumDivision_Num_int64_dict :: "( 64 word)NumDivision_class " where " instance_Num_NumDivision_Num_int64_dict = ((| numDivision_method = (div)|) )" (*val int64Mod : int64 -> int64 -> int64*) definition instance_Num_NumRemainder_Num_int64_dict :: "( 64 word)NumRemainder_class " where " instance_Num_NumRemainder_Num_int64_dict = ((| mod_method = (mod)|) )" (*val int64Min : int64 -> int64 -> int64*) (*val int64Max : int64 -> int64 -> int64*) definition instance_Basic_classes_OrdMaxMin_Num_int64_dict :: "( 64 word)OrdMaxMin_class " where " instance_Basic_classes_OrdMaxMin_Num_int64_dict = ((| max_method = ((\ x y. if (word_sle y x) then x else y)), min_method = ((\ x y. if (word_sle x y) then x else y))|) )" (* ----------------------- *) (* 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*) definition instance_Basic_classes_Ord_Num_integer_dict :: "(int)Ord_class " where " instance_Basic_classes_Ord_Num_integer_dict = ((| compare_method = (genericCompare (<) (=)), isLess_method = (<), isLessEqual_method = (\), isGreater_method = (>), isGreaterEqual_method = (\)|) )" (*val integerNegate : integer -> integer*) definition instance_Num_NumNegate_Num_integer_dict :: "(int)NumNegate_class " where " instance_Num_NumNegate_Num_integer_dict = ((| numNegate_method = (\ i. - i)|) )" (*val integerAbs : integer -> integer*) (* TODO: check *) definition instance_Num_NumAbs_Num_integer_dict :: "(int)NumAbs_class " where " instance_Num_NumAbs_Num_integer_dict = ((| abs_method = abs |) )" (*val integerAdd : integer -> integer -> integer*) definition instance_Num_NumAdd_Num_integer_dict :: "(int)NumAdd_class " where " instance_Num_NumAdd_Num_integer_dict = ((| numAdd_method = (+)|) )" (*val integerMinus : integer -> integer -> integer*) definition instance_Num_NumMinus_Num_integer_dict :: "(int)NumMinus_class " where " instance_Num_NumMinus_Num_integer_dict = ((| numMinus_method = (-)|) )" (*val integerSucc : integer -> integer*) definition instance_Num_NumSucc_Num_integer_dict :: "(int)NumSucc_class " where " instance_Num_NumSucc_Num_integer_dict = ((| succ_method = (\ n. n +( 1 :: int))|) )" (*val integerPred : integer -> integer*) definition instance_Num_NumPred_Num_integer_dict :: "(int)NumPred_class " where " instance_Num_NumPred_Num_integer_dict = ((| pred_method = (\ n. n -( 1 :: int))|) )" (*val integerMult : integer -> integer -> integer*) definition instance_Num_NumMult_Num_integer_dict :: "(int)NumMult_class " where " instance_Num_NumMult_Num_integer_dict = ((| numMult_method = ( * )|) )" (*val integerPow : integer -> nat -> integer*) definition instance_Num_NumPow_Num_integer_dict :: "(int)NumPow_class " where " instance_Num_NumPow_Num_integer_dict = ((| numPow_method = (^)|) )" (*val integerDiv : integer -> integer -> integer*) definition instance_Num_NumIntegerDivision_Num_integer_dict :: "(int)NumIntegerDivision_class " where " instance_Num_NumIntegerDivision_Num_integer_dict = ((| div_method = (div)|) )" definition instance_Num_NumDivision_Num_integer_dict :: "(int)NumDivision_class " where " instance_Num_NumDivision_Num_integer_dict = ((| numDivision_method = (div)|) )" (*val integerMod : integer -> integer -> integer*) definition instance_Num_NumRemainder_Num_integer_dict :: "(int)NumRemainder_class " where " instance_Num_NumRemainder_Num_integer_dict = ((| mod_method = (mod)|) )" (*val integerMin : integer -> integer -> integer*) (*val integerMax : integer -> integer -> integer*) definition instance_Basic_classes_OrdMaxMin_Num_integer_dict :: "(int)OrdMaxMin_class " where " instance_Basic_classes_OrdMaxMin_Num_integer_dict = ((| max_method = max, min_method = 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*) definition instance_Basic_classes_Ord_Num_rational_dict :: "(rat)Ord_class " where " instance_Basic_classes_Ord_Num_rational_dict = ((| compare_method = (genericCompare (<) (=)), isLess_method = (<), isLessEqual_method = (\), isGreater_method = (>), isGreaterEqual_method = (\)|) )" (*val rationalAdd : rational -> rational -> rational*) definition instance_Num_NumAdd_Num_rational_dict :: "(rat)NumAdd_class " where " instance_Num_NumAdd_Num_rational_dict = ((| numAdd_method = (+)|) )" (*val rationalMinus : rational -> rational -> rational*) definition instance_Num_NumMinus_Num_rational_dict :: "(rat)NumMinus_class " where " instance_Num_NumMinus_Num_rational_dict = ((| numMinus_method = (-)|) )" (*val rationalNegate : rational -> rational*) definition instance_Num_NumNegate_Num_rational_dict :: "(rat)NumNegate_class " where " instance_Num_NumNegate_Num_rational_dict = ((| numNegate_method = (\ i. - i)|) )" (*val rationalAbs : rational -> rational*) definition instance_Num_NumAbs_Num_rational_dict :: "(rat)NumAbs_class " where " instance_Num_NumAbs_Num_rational_dict = ((| abs_method = abs |) )" (*val rationalSucc : rational -> rational*) definition instance_Num_NumSucc_Num_rational_dict :: "(rat)NumSucc_class " where " instance_Num_NumSucc_Num_rational_dict = ((| succ_method = (\ n. n +(Fract ( 1 :: int) (1 :: int)))|) )" (*val rationalPred : rational -> rational*) definition instance_Num_NumPred_Num_rational_dict :: "(rat)NumPred_class " where " instance_Num_NumPred_Num_rational_dict = ((| pred_method = (\ n. n -(Fract ( 1 :: int) (1 :: int)))|) )" (*val rationalMult : rational -> rational -> rational*) definition instance_Num_NumMult_Num_rational_dict :: "(rat)NumMult_class " where " instance_Num_NumMult_Num_rational_dict = ((| numMult_method = ( * )|) )" (*val rationalDiv : rational -> rational -> rational*) definition instance_Num_NumDivision_Num_rational_dict :: "(rat)NumDivision_class " where " instance_Num_NumDivision_Num_rational_dict = ((| numDivision_method = (div)|) )" (*val rationalFromFrac : int -> int -> rational*) (*let rationalFromFrac n d= (Instance_Num_NumDivision_Num_rational./) (rationalFromInt n) (rationalFromInt d)*) (*val rationalPowInteger : rational -> integer -> rational*) fun rationalPowInteger :: " rat \ int \ rat " where " rationalPowInteger b e = ( if e =( 0 :: int) then(Fract ( 1 :: int) (1 :: int)) else if e >( 0 :: int) then rationalPowInteger b (e -( 1 :: int)) * b else rationalPowInteger b (e +( 1 :: int)) div b )" (*val rationalPowNat : rational -> nat -> rational*) (*let rationalPowNat r e= rationalPowInteger r (integerFromNat e)*) definition instance_Num_NumPow_Num_rational_dict :: "(rat)NumPow_class " where " instance_Num_NumPow_Num_rational_dict = ((| numPow_method = power |) )" (*val rationalMin : rational -> rational -> rational*) (*val rationalMax : rational -> rational -> rational*) definition instance_Basic_classes_OrdMaxMin_Num_rational_dict :: "(rat)OrdMaxMin_class " where " instance_Basic_classes_OrdMaxMin_Num_rational_dict = ((| max_method = max, min_method = min |) )" (* ----------------------- *) (* 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*) definition instance_Basic_classes_Ord_Num_real_dict :: "(real)Ord_class " where " instance_Basic_classes_Ord_Num_real_dict = ((| compare_method = (genericCompare (<) (=)), isLess_method = (<), isLessEqual_method = (\), isGreater_method = (>), isGreaterEqual_method = (\)|) )" (*val realAdd : real -> real -> real*) definition instance_Num_NumAdd_Num_real_dict :: "(real)NumAdd_class " where " instance_Num_NumAdd_Num_real_dict = ((| numAdd_method = (+)|) )" (*val realMinus : real -> real -> real*) definition instance_Num_NumMinus_Num_real_dict :: "(real)NumMinus_class " where " instance_Num_NumMinus_Num_real_dict = ((| numMinus_method = (-)|) )" (*val realNegate : real -> real*) definition instance_Num_NumNegate_Num_real_dict :: "(real)NumNegate_class " where " instance_Num_NumNegate_Num_real_dict = ((| numNegate_method = (\ i. - i)|) )" (*val realAbs : real -> real*) definition instance_Num_NumAbs_Num_real_dict :: "(real)NumAbs_class " where " instance_Num_NumAbs_Num_real_dict = ((| abs_method = abs |) )" (*val realSucc : real -> real*) definition instance_Num_NumSucc_Num_real_dict :: "(real)NumSucc_class " where " instance_Num_NumSucc_Num_real_dict = ((| succ_method = (\ n. n +( 1 :: real))|) )" (*val realPred : real -> real*) definition instance_Num_NumPred_Num_real_dict :: "(real)NumPred_class " where " instance_Num_NumPred_Num_real_dict = ((| pred_method = (\ n. n -( 1 :: real))|) )" (*val realMult : real -> real -> real*) definition instance_Num_NumMult_Num_real_dict :: "(real)NumMult_class " where " instance_Num_NumMult_Num_real_dict = ((| numMult_method = ( * )|) )" (*val realDiv : real -> real -> real*) definition instance_Num_NumDivision_Num_real_dict :: "(real)NumDivision_class " where " instance_Num_NumDivision_Num_real_dict = ((| numDivision_method = (div)|) )" (*val realFromFrac : integer -> integer -> real*) definition realFromFrac :: " int \ int \ real " where " realFromFrac n d = ( ((real_of_int n)) div ((real_of_int d)))" (*val realPowInteger : real -> integer -> real*) fun realPowInteger :: " real \ int \ real " where " realPowInteger b e = ( if e =( 0 :: int) then( 1 :: real) else if e >( 0 :: int) then realPowInteger b (e -( 1 :: int)) * b else realPowInteger b (e +( 1 :: int)) div b )" (*val realPowNat : real -> nat -> real*) (*let realPowNat r e= realPowInteger r (integerFromNat e)*) definition instance_Num_NumPow_Num_real_dict :: "(real)NumPow_class " where " instance_Num_NumPow_Num_real_dict = ((| numPow_method = power |) )" (*val realSqrt : real -> real*) (*val realMin : real -> real -> real*) (*val realMax : real -> real -> real*) definition instance_Basic_classes_OrdMaxMin_Num_real_dict :: "(real)OrdMaxMin_class " where " instance_Basic_classes_OrdMaxMin_Num_real_dict = ((| 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*) (*let int32FromInteger i= ( let abs_int32 = int32FromNatural (naturalFromInteger i) in if ((Instance_Basic_classes_Ord_Num_integer.<) i 0) then (Instance_Num_NumNegate_Num_int32.~ abs_int32) else abs_int32 )*) (*val int32FromInt : int -> int32*) (*let int32FromInt i= int32FromInteger (integerFromInt i)*) (*val int32FromInt64 : int64 -> int32*) (*let int32FromInt64 i= int32FromInteger (integerFromInt64 i)*) (******************) (* int64From ... *) (******************) (*val int64FromNat : nat -> int64*) (*val int64FromNatural : natural -> int64*) (*val int64FromInteger : integer -> int64*) (*let int64FromInteger i= ( let abs_int64 = int64FromNatural (naturalFromInteger i) in if ((Instance_Basic_classes_Ord_Num_integer.<) i 0) then (Instance_Num_NumNegate_Num_int64.~ abs_int64) else abs_int64 )*) (*val int64FromInt : int -> int64*) (*let int64FromInt i= int64FromInteger (integerFromInt 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*) end