From 054f3dcee39ff5d031b0235070b2ab7f6a64a4fc Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Sun, 18 Sep 2011 19:34:08 +0200 Subject: [PATCH] new lemmas for theory NumOf --- theories/int.why | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/theories/int.why b/theories/int.why index b35596250..f0dda3836 100644 --- a/theories/int.why +++ b/theories/int.why @@ -174,8 +174,8 @@ theory NumOfParam forall p : param, a b : int. a < b -> pr p (b-1) -> num_of p a b = 1 + num_of p a (b-1) - lemma Num_of_non_negative : - forall p : param, a b : int. 0 <= num_of p a b + lemma Num_of_bounds : + forall p : param, a b : int. a < b -> 0 <= num_of p a b <= b - a (* direct when a>=b, by induction on b when a <= b *) lemma Num_of_append : @@ -197,6 +197,11 @@ theory NumOfParam (forall n : int. a <= n < b -> not pr p n) -> num_of p a b = 0 (* by induction on b *) + lemma Full : + forall p : param, a b : int. a < b -> + (forall n : int. a <= n < b -> pr p n) -> num_of p a b = b - a + (* by induction on b *) + lemma num_of_increasing: forall p : param, i j k : int. i <= j <= k -> num_of p i j <= num_of p i k -- 2.26.2