[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
enrich
decimal-simple-ops
with
functions . / . : decimal × decimal → decimal prio 11 right;
comment: precise result if a decimal, truncated to maximum
scale otherwise. This means 1 / 3 = 0.;
div : decimal × decimal × int → decimal;
comment: int is precision if result is not a decimal.
E.g. div(1.0, 3.0, 2) = 0.33
If result is a decimal then precision is ignored.;
sqrt : decimal → decimal;
sqrt : decimal × int → decimal;
comment: sqrt(dec, i) with precision i.
If dec is a square the result is exact.
Otherwise the result will have i (or i+1) more digits than dec.
Specific if dec is an integer then the result
will have i fractional digits;
predicates . | . : decimal × decimal;
comment: divides (exactly), i.e. result of division is a decimal.
false for 3 | 1, but true for 20 | 5.;
isSquare : decimal;
axioms divides-def : ⊦ dec_j | dec_i ↔ (∃ dec_j0. dec_j * dec_j0 = dec_i);
div-def : ⊦ dec_i / dec_j = div(dec_i, dec_j, 0);
div-exact-def : ⊦ dec_j | dec_i → div(dec_i, dec_j, i) * dec_j = dec_i;
div-precision-def
: ⊦ ¬ dec_j | dec_i
→ div(dec_i, dec_j, i)
= mkDecimal
((dec_i.int * 10 ^ (dec_j.scale + abs(i))) / dec_j.int / 10 ^ maxScale(dec_j.int), dec_i.scale + abs(i) + maxScale(dec_j.int));
isSquare-def : ⊦ isSquare(dec_i) ↔ (∃ dec. dec * dec = dec_i);
sqrt-def : ⊦ sqrt(dec) = sqrt(dec, 0);
sqrt-even-precision-def : ⊦ even(dec_i.scale) → sqrt(dec_i, i) = mkDecimal(sqrt(dec_i.int * 10 ^ (2 * abs(i))), dec_i.scale / 2 + abs(i));
sqrt-odd-precision-def
: ⊦ odd(dec_i.scale) → sqrt(dec_i, i) = mkDecimal(sqrt(dec_i.int * 10 ^ (2 * abs(i) + 1)), (dec_i.scale + 1) / 2 + abs(i));
end enrich