enrich
   int-gcd

with
   

   sorts decimal;
   
   functions  mkDecimal : int × int → decimal;
             comment: mkDecimal(i, j) represents i / 10^j. i can be negative, for j the
                                             absolute value is taken. Examples: 
                                             mkDecimal(13, 0) = 13, mkDecimal(13, 1) = 1.3, mkDecimal(13, 2) = 0.13,
                                             mkDecimal(100, 0) = 100, mkDecimal(100, 1) = mkDecimal(10, 0) = 10;
              . .int : decimal → int;
             comment: the integer (or integral) part.;
              . .scale : decimal → int;
             comment: the scale, i.e. power of 10 as denumerator (j in i / 10^j), always ≥ 0.;
              dec2int : decimal → int;
             comment: discard fractional part.;
              maxScale : int → int;
             comment: maximum j with i % 10^j = 0 in maxScale(i) = j;
              truncate : decimal × int → decimal;
             comment: truncate fractional part to i digits, e.g.
                                                 truncate(3.14159265358979323844, 2) = 3.14;
              inc : decimal → decimal;
             comment: increment last digit by one, e.g.
                                           inc(0.003) = 0.004, inc(0.99) = 1;
   
   
   variables  dec : decimal;
              dec0 : decimal;
              dec1 : decimal;
              dec2 : decimal;
              dec_i : decimal;
              dec_i0 : decimal;
              dec_j : decimal;
              dec_j0 : decimal;
   
   

   induction decimal generated by mkDecimal;

   axioms Equality :  ⊦ dec_i = dec_j ↔ dec_i.int = dec_j.int ∧ dec_i.scale = dec_j.scale;
          comment: this axiom together with the intvalue-... and scale-... axioms
                    precisely characterize the decimals.;
          intvalue-zero :  ⊦ mkDecimal(0, j).int = 0;
          used for: s, ls;
          intvalue-base :  ⊦ ¬(i % 10 = 0 ∧ j ≠ 0 ∧ i ≠ 0) → mkDecimal(i, j).int = i;
          intvalue-rec :  ⊦ i % 10 = 0 ∧ j ≠ 0 ∧ i ≠ 0 → mkDecimal(i, j).int = mkDecimal(i / 10, abs(j) - 1).int;
          scale-zero :  ⊦ mkDecimal(0, j).scale = 0;
          used for: s, ls;
          scale-base :  ⊦ ¬(i % 10 = 0 ∧ j ≠ 0 ∧ i ≠ 0) → mkDecimal(i, j).scale = abs(j);
          scale-rec :  ⊦ i % 10 = 0 ∧ j ≠ 0 ∧ i ≠ 0 → mkDecimal(i, j).scale = mkDecimal(i / 10, abs(j) - 1).scale;
          maxScale-zero :  ⊦ maxScale(0) = 0;
          used for: s, ls;
          maxScale-base :  ⊦ i % 10 ≠ 0 ∧ i ≠ 0 → maxScale(i) = 0;
          used for: s, ls;
          maxScale-rec :  ⊦ i % 10 = 0 ∧ i ≠ 0 → maxScale(i) = maxScale(i / 10) + 1;
          dec2int-def :  ⊦ dec2int(dec) = dec.int / 10 ^ dec.scale;
          truncate-really-def :  ⊦ abs(i) < dec.scale → truncate(dec, i) = mkDecimal(dec.int / 10 ^ (dec.scale - abs(i)), abs(i));
          truncate-nothing-def :  ⊦ dec.scale ≤ abs(i) → truncate(dec, i) = dec;
          inc-def :  ⊦ inc(dec) = mkDecimal(dec.int + 1, dec.scale);

   

   
end enrich