Additional rule for sequences: Swap of sequence is a permutation (#3485)

KeYProject · Jun 21, 2024 · 4babbbe · 4babbbe
2 parents c8b5d84 + 63d108a
commit 4babbbe
Show file tree

Hide file tree

Showing 3 changed files with 515 additions and 0 deletions.
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seqPerm.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seqPerm.key
@@ -558,6 +558,30 @@
                 s1 = seqSwap(s2, iv, jv)))
     };
 
+    \lemma
+    seqSwapPreservesSeqPerm {
+        \schemaVar \term Seq s;
+        \schemaVar \term int x;
+        \schemaVar \term int y;
+
+        \find(==> seqPerm(s, seqSwap(s, x, y)))
+        \add( ==> 0 <= x & x < seqLen(s) & 0 <= y & y < seqLen(s))
+        \heuristics(simplify_enlarging)
+    };
+
+    \lemma
+    seqSwapPreservesSeqPermEQ {
+        \schemaVar \term Seq s;
+        \schemaVar \term Seq EQ;
+        \schemaVar \term int x;
+        \schemaVar \term int y;
+
+        \assumes (seqSwap(s, x, y) = EQ ==>)
+        \find(==> seqPerm(s, EQ))
+        \add( ==> 0 <= x & x < seqLen(s) & 0 <= y & y < seqLen(s))
+        \heuristics(simplify_enlarging)
+    };
+
     /* seqPermOrder {
      \schemaVar \term Seq commEqLeft, commEqRight;
      \find(seqPerm(commEqLeft, commEqRight))