stdlib/for_drivers.mlw

   1 theory ComputerOfEuclideanDivision
   2
   3   use int.Int
   4   use int.EuclideanDivision as ED
   5   use int.ComputerDivision as CD
   6
   7   lemma cdiv_cases : forall n d:int [CD.div n d].
   8     ((n >= 0) -> (d > 0) -> CD.div n d = ED.div n d) /\
   9     ((n <= 0) -> (d > 0) -> CD.div n d = -(ED.div (-n) d)) /\
  10     ((n >= 0) -> (d < 0) -> CD.div n d = -(ED.div n (-d))) /\
  11     ((n <= 0) -> (d < 0) -> CD.div n d = ED.div (-n) (-d))
  12
  13   lemma cmod_cases : forall n d:int [CD.mod n d].
  14     ((n >= 0) -> (d > 0) -> CD.mod n d = ED.mod n d) /\
  15     ((n <= 0) -> (d > 0) -> CD.mod n d = -(ED.mod (-n) d)) /\
  16     ((n >= 0) -> (d < 0) -> CD.mod n d = (ED.mod n (-d))) /\
  17     ((n <= 0) -> (d < 0) -> CD.mod n d = -(ED.mod (-n) (-d)))
  18
  19 end