for_drivers.mlw 704 Bytes
Newer Older
1 2
theory ComputerOfEuclideanDivision

3 4 5
  use int.Int
  use int.EuclideanDivision as ED
  use int.ComputerDivision as CD
6 7 8 9 10 11 12 13 14 15 16 17 18 19

  lemma cdiv_cases : forall n d:int [CD.div n d].
    ((n >= 0) -> (d > 0) -> CD.div n d = ED.div n d) /\
    ((n <= 0) -> (d > 0) -> CD.div n d = -(ED.div (-n) d)) /\
    ((n >= 0) -> (d < 0) -> CD.div n d = -(ED.div n (-d))) /\
    ((n <= 0) -> (d < 0) -> CD.div n d = ED.div (-n) (-d))

  lemma cmod_cases : forall n d:int [CD.mod n d].
    ((n >= 0) -> (d > 0) -> CD.mod n d = ED.mod n d) /\
    ((n <= 0) -> (d > 0) -> CD.mod n d = -(ED.mod (-n) d)) /\
    ((n >= 0) -> (d < 0) -> CD.mod n d = (ED.mod n (-d))) /\
    ((n <= 0) -> (d < 0) -> CD.mod n d = -(ED.mod (-n) (-d)))

end