From c5e4ff677e0b5bb13438a3a0129ac808516d1a6d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?M=C3=A1rio=20Pereira?= Date: Tue, 21 Jul 2015 12:46:35 +0200 Subject: [PATCH] Added new lemmas to seq theory: permut_refl, permut_sym, permut_all_mem --- theories/seq.why | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/theories/seq.why b/theories/seq.why index 03c33d079..04a0cf8f3 100644 --- a/theories/seq.why +++ b/theories/seq.why @@ -328,8 +328,14 @@ theory Permut (** {2 Lemmas about permut} *) + lemma permut_refl: forall s: seq 'a, l u: int. + permut s s l u + + lemma permut_sym: forall s1 s2: seq 'a, l u: int. + permut s1 s2 l u -> permut s2 s1 l u + lemma permut_trans: - forall s1 s2 s3: seq 'a. forall l u: int. + forall s1 s2 s3: seq 'a, l u: int. permut s1 s2 l u -> permut s2 s3 l u -> permut s1 s3 l u lemma permut_exists: @@ -339,6 +345,11 @@ theory Permut (** {2 Lemmas about permut_all} *) + use import Mem + + lemma permut_all_mem: forall s1 s2: seq 'a. permut_all s1 s2 -> + forall x. mem x s1 <-> mem x s2 + lemma exchange_permut_all: forall s1 s2: seq 'a, i j: int. exchange s1 s2 i j -> permut_all s1 s2 -- GitLab