library Basic/Numbers version 0.5 %% authors: M.Roggenbach, T.Mossakowski, L.Schröder %% copyright: 5.5.00 from Basic/RelationsAndOrders version 0.5 get SigOrder, ExtTotalOrder from Basic/PreNumbers version 0.5 get SigPreNumbers, PreNat, TotalOrder_in_PreNat, PreInt, TotalOrder_in_PreInt, PreRat, TotalOrder_in_PreRat from Basic/Algebra_I version 0.5 get SigPowerBinAlg,ExtCommutativeMonoid, CommutativeMonoid_in_PreNat_Mult, CommutativeMonoid_in_PreNat_Add, EuclidianRing, ExtEuclidianRing, EuclidianRing_in_PreInt, Field, ExtField, Field_in_PreRat spec SigNumbers[sort Elem][sort NonNeg][sort Exponent] = SigPreNumbers[sort Elem][sort NonNeg] then SigPowerBinAlg[sort Exponent] then %def sorts NonZero[Elem] = { x: Elem . not x = 0 }; Pos[Elem] = { x: Elem . x > 0 }; Pos[Elem] < NonZero[Elem] ops +__: Elem -> Elem; abs: NonZero[Elem] -> Pos[Elem] %prec {+__} <> {__ ^ __} var x: Elem . %[plus_def] + x = x end spec Nat = ExtCommutativeMonoid [view CommutativeMonoid_in_PreNat_Mult] with sorts Nat, Pos, preds __ <= __, __ >= __, __ < __, __ > __, ops suc, pre, __+__, __*__, abs, __ ^ __ and ExtCommutativeMonoid [view CommutativeMonoid_in_PreNat_Add] with op __ ^ __ |-> __ times __ and ExtTotalOrder [PreNat reveal sort Nat, pred __ <= __ ] with ops min, max and SigNumbers[sort Nat][sort Nat][sort Nat] then sorts NonZero[Nat]=Pos; Pos[Nat]=Pos preds odd, even: Nat ops __! : Nat -> Nat; __ -?__: Nat × Nat ->? Nat ops __ /? __: Nat × Nat ->? Nat; __ div __, __ mod __ , __ quot __, __ rem __ :Nat × Nat ->? Nat; __ div __, __ mod __ , __ quot __, __ rem __ : Nat × Pos -> Nat; %prec { __ -? __ , __ + __ } < { __ * __, __ /? __ } %prec { __ -? __ , __ + __ } < { __ div __, __ mod __, __ quot __, __rem __ } %prec { __ /? __, __div__, __mod__, __ quot __, __ rem __ } < { __ ^ __} %% Operations to represent natural numbers as digits: ops 1,2,3,4,5,6,7,8,9: Nat; __ @@ __ : Nat × Nat -> Nat %left assoc %number __@@__ vars m,n,r,s: Nat; p: Pos . %[Nat_divide_0] not def(m /? 0) . %[Nat_divide_Pos] ( m /? n = r <=> m = r * n ) if n>0 . %[Nat_odd_def] odd(m) <=> not even(m) . %[Nat_even_zero] even(0) . %[Nat_even_suc] even(suc(m)) <=> odd(m) . %[Nat_factorial_zero] 0! =1 . %[Nat_factorial_suc] suc(n)! =suc(n)*n! . %[Nat_sub_def] m -? n = r <=> m = r + n . %[Nat_div_partial] m div n = r <=> (exists s: Nat . m = n*r + s /\ s < n) . %[Nat_mod_partial] m mod n = s <=> (exists r: Nat . m = n*r + s /\ s < n) . %[Nat_quot_partial] m quot n = m div n . %[Nat_rem_partial] m rem n = m mod n . %[Nat_1_def] 1 = suc (0) . %[Nat_2_def] 2 = suc (1) . %[Nat_3_def] 3 = suc (2) . %[Nat_4_def] 4 = suc (3) . %[Nat_5_def] 5 = suc (4) . %[Nat_6_def] 6 = suc (5) . %[Nat_7_def] 7 = suc (6) . %[Nat_8_def] 8 = suc (7) . %[Nat_9_def] 9 = suc (8) . %[Nat_decimal_def] m @@ n = (m * suc(9)) + n then %implies vars m,n,r,s,t: Nat; p: Pos . %[Nat_sub_dom] def(m-?n) <=> m >= n . %[Nat_divide_dom] def(m /? n) <=> m mod n = 0 . %[Nat_div_total] m div p = r <=> (exists s: Nat . m = p*r + s /\ s < p) . %[Nat_div_dom] def ( m div n ) <=> not (n=0) . %[Nat_mod_total] m mod p = s <=> (exists r: Nat . m = p*r + s /\ s < p) . %[Nat_mod_dom] def ( m mod n ) <=> not (n=0) . %[Nat_quot_total] m quot p = m div p . %[Nat_quot_dom] def ( m quot n ) <=> not (n=0) . %[Nat_rem_total] m rem p = m mod p . %[Nat_rem_dom] def ( m rem n ) <=> not (n=0) . %[Nat_max_unit] max(m,0) = m . %[Nat_distr] (r + s) * t = (r * t) + (s * t) end spec Int = ExtEuclidianRing [view EuclidianRing_in_PreInt] with sorts Int, Nat, Pos, Neg, NonZero[Int], preds __ <= __, __ >= __, __ < __, __ > __, ops suc, pre, __+__, __*__, abs, __-__, -__, __ ^ __ and ExtTotalOrder [PreInt reveal sort Int, pred __<=__ fit sort Elem |-> Int] with ops min, max then %def Nat and SigNumbers[sort Int] [sort Nat] [sort Nat] then %def sort Pos = Pos[Int] free type NonZero[Int] ::= Pos | Neg preds odd, even: Int ops __ /? __, __ div __, __ mod __ , __ quot __, __ rem __ : Int × Int ->? Int; __ div __, __ mod __ , __ quot __, __ rem __ : Int × NonZero[Int] -> Int; sign: Int -> Int %prec { __ * __ } <> { __ /? __, __ div __, __ mod __, __ quot __, __ rem __ } vars m,n,s: Nat; p,q: Pos; x,y,r,z: Int . %[Int_divide] x /? y = z <=> ( x = z * y /\ not y=0) . %[Int_even_def] even(minus(p)) <=> even(p) . %[Int_odd_def] odd(minus(p)) <=> odd(p) . %[Int_div_partial1] minus(p) div n = - (p div n) when p mod n = 0 else - (p div n) + 1 . %[Int_div_partial2] x div minus(q) = - (x div q) . %[Int_mod_partial] x mod y = x - y * (x div y) . %[Int_quot_partial1] minus(p) quot n = - (p quot n) . %[Int_quot_partial2] x quot minus(q) = - (x quot q) . %[Int_rem_partial] x rem y = x - y * (x quot y) . %[Int_sign_pos] sign(p) = 1 . %[Int_sign_zero] sign(0) = 0 . %[Int_sign_neg] sign(minus(p)) = minus(1) then %implies vars n : NonZero[Int]; x,y,r: Int; s: Nat; p: Pos . %[Int_minus] minus(p) = - p . %[Int_times] x times y = x * y . %[Int_divide_dom] def (x /? y) <=> x mod y = 0 . %[Int_div_total] x div n = r <=> (exists s: Nat . x = r*n + s /\ s < abs(n)) . %[Int_div_dom] def (x div y) <=> not y=0 . %[Int_mod_total] x mod n = s <=> (exists r: Int . x = r*n + s /\ s < abs(n)) . %[Int_mod_dom] def (x mod y) <=> not y=0 . %[Int_quot_total1] x quot n = abs(x) div abs(n) if (x >= 0 /\ n > 0) \/ (x < 0 /\ n < 0) . %[Int_quot_total2] x quot n = - (abs(x) div abs(n)) if (x >= 0 /\ n < 0) \/ (x < 0 /\ n > 0) . %[Int_quot_dom] def (x quot y) <=> not y=0 . %[Int_rem_total1] x rem n = abs(x) mod abs(n) if x >= 0 . %[Int_rem_total2] x rem n = - (abs(x) mod abs(n)) if x < 0 . %[Int_rem_dom] def (x rem y) <=> not y=0 end spec Rat = ExtField [view Field_in_PreRat] with sorts Rat, NonZero[Rat], NonNeg[Rat], preds __ <= __, __ >= __, __ < __, __ > __, ops __+__, __*__, abs, __ ^ __, -__, __ - __, __ / __ : Rat × NonZero[Rat] -> Rat, __ / __ : Rat × Rat ->? Rat then %prec { __ - __, -__ } < { __ frac __ } then %def ExtTotalOrder [PreRat reveal sort Rat, pred __ <= __ fit sort Elem |-> Rat] with ops min, max and Int and SigNumbers[sort Rat] [sort NonNeg[Rat]] [sort Int] then %def sort NonZero[Int] < NonZero[Rat] generated types NonZero[Rat] ::= __ frac __ (NonZero[Int];Pos); Pos[Rat] ::= __ frac __ (Pos;Pos) then %implies var r,s: Rat; n,m: Int; p,q: Pos; u: NonZero[Int] . %[Rat_frac] n frac p = n / p . %[Rat_neg] - n frac p = (-n) frac p . %[Rat_sub] n frac p - m frac q = (n * q - m * p) frac (p * q) . %[Rat_div_total] (n frac p) / (u frac q) = (n * q * sign (u)) frac (p * abs(u) as Pos) end