Commit a6798d63 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
parents ab2dbb1a 17784ab0
......@@ -86,6 +86,13 @@ theory int.Abs
end
theory int.MinMax
syntax logic min "(Zmin %1 %2)"
syntax logic max "(Zmax %1 %2)"
end
theory int.EuclideanDivision
prelude "Require Import Zdiv."
......
......@@ -48,6 +48,15 @@ theory TestSplit
end
theory TestMinMax
use import int.Int
use import int.MinMax
goal G1: min 1 2 = 1
end
theory TestDiv
use import int.Int
......
......@@ -31,13 +31,13 @@ theory MinMax
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
(*
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_y : forall x y:t. ge x y -> min x y = y
axiom Min_x : forall x y:t. ge y x -> min x y = x
*)
axiom Min_y : forall x y:t. ge x y -> min x y = y
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
(*
logic min (x y : t) : t
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment