examples_in_progress/ewd650.mlw

   1
   2 (* EWD 650: A Theorem About Odd Powers of Odd Integers *)
   3
   4 module EWD650
   5
   6   use int.Int
   7   use int.Power
   8   use number.Parity
   9   use number.Divisibility
  10   use ref.Refint
  11
  12   let theorem (p: int) (k: int) (r: int)
  13     requires { p >= 1 /\ odd p /\ k >= 1 /\ 1 <= r < power 2 k /\ odd r }
  14     ensures  { 1 <= result < power 2 k }
  15     ensures  { divides (power 2 k) (power result p - r) }
  16     ensures  { odd result }
  17   = let x = ref 1 in
  18     let d = ref 2 in
  19     for i = 1 to k do
  20       invariant { !d = power 2 i /\ 1 <= !x < !d }
  21       invariant { divides !d (power !x p - r) /\ odd !x }
  22       if not (divides (2 * !d) (power !x p - r)) then x := !x + !d;
  23       d := 2 * !d
  24     done;
  25     !x
  26
  27 end