comparison.why 1.24 KB
 1 2 3 4 `````` theory Abs type t `````` Andrei Paskevich committed Jun 24, 2010 5 6 `````` logic ge t t logic neg t : t `````` 7 8 `````` logic zero : t `````` Andrei Paskevich committed Jun 24, 2010 9 `````` logic abs t : t `````` 10 `````` `````` Andrei Paskevich committed Jun 21, 2010 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 `````` Andrei Paskevich committed Jun 21, 2010 16 `````` axiom Abs_def : if ge x zero then abs x = x else abs x = neg x `````` 17 18 19 ``````*) end `````` MARCHE Claude committed Mar 25, 2010 20 `````` `````` 21 22 23 ``````theory MinMax type t `````` Andrei Paskevich committed Jun 24, 2010 24 `````` logic ge t t `````` 25 `````` `````` Andrei Paskevich committed Jun 24, 2010 26 27 `````` logic min t t : t logic max t t : t `````` 28 `````` `````` Andrei Paskevich committed Jun 21, 2010 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 `````` `````` Andrei Paskevich committed Jun 21, 2010 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 `````` MARCHE Claude committed Dec 15, 2010 37 `````` axiom Min_y : forall x y:t. ge x y -> min x y = y `````` 38 `````` `````` MARCHE Claude committed Dec 15, 2010 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 `````` (* `````` François Bobot committed Dec 16, 2010 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 `````` Andrei Paskevich committed Jun 24, 2010 45 `````` logic max (x y : t) : t `````` François Bobot committed Dec 16, 2010 46 `````` axiom Max_def : if ge x y then max x y = x else max x y = y `````` 47 48 ``````*) `````` François Bobot committed Dec 16, 2010 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``