Additional rule for sequences: Swap of sequence is a permutation

[WolframPfeifer]

Intended Change

This PR adds a new rule to KeY that has been proven useful (and is needed) in the upcoming tutorial: A sequence where two elements are swapped is a permutation of the original sequence. The new taclet is a lemma and marked as such. It is proven.

Type of pull request

• New feature (non-breaking change which adds functionality)

Ensuring quality

The taclet has been proven, the corresponding taclet proof (sliced to a minimal version) has been added to the taclet proof directory such that it is checked in the corresponding test.

Additional information and contact(s)

Co-authors of the taclet: @wadoon @unp1 @Drodt @mattulbrich @flo2702

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[WolframPfeifer]

Note by @mattulbrich: Maybe we need an EQ version of the taclet as well.

At the moment, the permutation rules for sequences do not have EQ rules at all. I am not sure whether there is a reason for this. However, the EQ taclet would look like this, right?

    \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)
    };

[mattulbrich]

Looks plausible. ...