examples_in_progress/2wp_gen/choice.mlw

   1 (* Axiom of choice *)
   2 module Choice
   3
   4   use fn.Fun
   5   use option.Option
   6
   7   constant witness : 'a
   8   function choice ('a -> bool) : 'a
   9   axiom choice_def : forall p,x:'a. p x -> p (choice p)
  10
  11   let ghost choose (p:{'a} -> bool) : {'a}
  12     requires { exists x. p x }
  13     ensures { p result }
  14   = {choice} p
  15
  16   let ghost choose_if (p:{'a} -> bool) : option {'a}
  17     returns { None -> forall x. not p x
  18             | Some u -> p u }
  19   = let u = {choice} p in if p u then Some u else None
  20
  21 end