From a93abfeb96437977f2cbd56c0e99610af6f12386 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 2 Apr 2014 18:59:29 -0700 Subject: Improvements in sequence axioms to make checking more automatic. Minor changes in a test file. --- Binaries/DafnyPrelude.bpl | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 0662d12b..224c5ffd 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -410,8 +410,13 @@ axiom (forall s: Seq T, i: int, j: int :: 0 <= i && i < j && j <= Seq#Length(s) ==> Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) < Seq#Rank(s) ); // Additional axioms about common things -axiom Seq#Take(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][..0] == [] -axiom Seq#Drop(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][0..] == [] +axiom (forall s: Seq T, n: int :: { Seq#Drop(s, n) } + n == 0 ==> Seq#Drop(s, n) == s); +axiom (forall s: Seq T, n: int :: { Seq#Take(s, n) } + n == 0 ==> Seq#Take(s, n) == Seq#Empty()); +axiom (forall s: Seq T, m, n: int :: { Seq#Drop(Seq#Drop(s, m), n) } + 0 <= m && 0 <= n && m+n <= Seq#Length(s) ==> + Seq#Drop(Seq#Drop(s, m), n) == Seq#Drop(s, m+n)); // --------------------------------------------------------------- // -- Axiomatization of Maps ------------------------------------- -- cgit v1.2.3