diff options
Diffstat (limited to 'snapshots/hol4/lem/hol-lib/lem_numScript.sml')
| -rw-r--r-- | snapshots/hol4/lem/hol-lib/lem_numScript.sml | 1317 |
1 files changed, 1317 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lem_numScript.sml b/snapshots/hol4/lem/hol-lib/lem_numScript.sml new file mode 100644 index 00000000..9dcd0554 --- /dev/null +++ b/snapshots/hol4/lem/hol-lib/lem_numScript.sml @@ -0,0 +1,1317 @@ +(*Generated by Lem from num.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_boolTheory lem_basic_classesTheory integerTheory intReduce wordsTheory wordsLib ratTheory realTheory intrealTheory; + +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`*) +(*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.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 -> Basic_classes.ordering*) + +val _ = Define ` +((instance_Basic_classes_Ord_nat_dict:(num)lem_basic_classes$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)lem_basic_classes$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 -> Basic_classes.ordering*) + +val _ = Define ` +((instance_Basic_classes_Ord_Num_natural_dict:(num)lem_basic_classes$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)lem_basic_classes$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 -> Basic_classes.ordering*) + +val _ = Define ` +((instance_Basic_classes_Ord_Num_int_dict:(int)lem_basic_classes$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)lem_basic_classes$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 -> Basic_classes.ordering*) + +val _ = Define ` +((instance_Basic_classes_Ord_Num_int32_dict:(word32)lem_basic_classes$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)lem_basic_classes$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 -> Basic_classes.ordering*) + +val _ = Define ` +((instance_Basic_classes_Ord_Num_int64_dict:(word64)lem_basic_classes$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)lem_basic_classes$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 -> Basic_classes.ordering*) + +val _ = Define ` +((instance_Basic_classes_Ord_Num_integer_dict:(int)lem_basic_classes$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)lem_basic_classes$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 -> Basic_classes.ordering*) + +val _ = Define ` +((instance_Basic_classes_Ord_Num_rational_dict:(rat)lem_basic_classes$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)lem_basic_classes$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 -> Basic_classes.ordering*) + +val _ = Define ` +((instance_Basic_classes_Ord_Num_real_dict:(real)lem_basic_classes$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)lem_basic_classes$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() + |