comparison.why 1.24 KB
Newer Older
1 2 3 4

theory Abs

  type t
5 6
  logic ge t t
  logic neg t : t
7 8
  logic zero : t

9
  logic abs t : t
10

11 12
  axiom Pos: forall x:t. ge x zero -> abs x = x
  axiom Neg: forall x:t. not ge x zero -> abs x = neg x
13 14 15

(*
  logic abs(x : t) : t 
16
  axiom Abs_def : if ge x zero then abs x = x else abs x = neg x
17 18 19
*)
end

MARCHE Claude's avatar
MARCHE Claude committed
20

21 22 23
theory MinMax

  type t
24
  logic ge t t
25

26 27
  logic min t t : t
  logic max t t : t
28

29 30 31 32
  axiom Max_is_ge   : forall x y:t. ge (max x y) x and ge (max x y) y
  axiom Max_is_some : forall x y:t. max x y = x or max x y = y
  axiom Min_is_le   : forall x y:t. ge x (min x y) and ge y (min x y)
  axiom Min_is_some : forall x y:t. min x y = x or min x y = y
33

34 35 36
  axiom Max_x : forall x y:t. ge x y -> max x y = x
  axiom Max_y : forall x y:t. ge y x -> max x y = y
  axiom Min_x : forall x y:t. ge y x -> min x y = x
37
  axiom Min_y : forall x y:t. ge x y -> min x y = y
38

39 40
  lemma Max_sym: forall x y:t. ge x y -> max x y = max y x
  lemma Min_sym: forall x y:t. ge x y -> min x y = min y x
41 42

(*
43 44
  logic min (x y : t) : t
  axiom Min_def : if ge x y then min x y = y else min x y = x
45
  logic max (x y : t) : t
46
  axiom Max_def : if ge x y then max x y = x else max x y = y
47 48
*)

49 50 51 52 53 54
(*
  logic min (x y : t) : t = if ge x y then y else x
  logic max (x y : t) : t = if ge x y then x else y
*)


55
end