Basic Theory of Sets

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key

@@ -24,6 +24,7 @@
     permission,
     reach,
     seq,
+    set,
     map,
     freeADT,
     wellfound,

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/set.key

@@ -0,0 +1,27 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+
+\sorts {
+    \generic T;
+    Set<[T]>;
+}
+
+\functions {
+    \unique Set<[T]> sEmpty<[T]>;
+
+    // other constructors
+    Set<[T]> sSingleton<[T]>(T);
+    Set<[T]> sUnion<[T]>(Set<[T]>, Set<[T]>);
+    Set<[T]> sIntersect<[T]>(Set<[T]>, Set<[T]>);
+    Set<[T]> sSetMinus<[T]>(Set<[T]>, Set<[T]>);
+    Set<[T]> sInfiniteUnion<[T]>{true}(Set<[T]>);
+
+    int sCard<[T]>(Set<[T]>);
+}
+
+\predicates {
+    sElementOf<[T]>(T, Set<[T]>);
+    sSubset<[T]>(Set<[T]>, Set<[T]>);
+    sDisjoint<[T]>(Set<[T]>, Set<[T]>);
+}

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/setRules.key

@@ -0,0 +1,170 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+
+\schemaVariables {
+    \term T a, b;
+    \term Set<[T]> s, t, EQ;
+}
+
+\rules {
+
+    // --------------------------------------------------------------------------
+    // axioms for sElementOf
+    // --------------------------------------------------------------------------
+
+    sElementOfSEmpty {
+        \find(sElementOf<[T]>(a, sEmpty<[T]>))
+        \replacewith(false)
+        \heuristics(concrete)
+    };
+
+    sElementOfSSingleton {
+        \find(sElementOf<[T]>(a, sSingleton<[T]>(b)))
+        \replacewith(a = b)
+        \heuristics(simplify)
+    };
+
+    sElementOfSUnion {
+        \find(sElementOf<[T]>(a, sUnion<[T]>(s, t)))
+        \replacewith(sElementOf<[T]>(a, s) | sElementOf<[T]>(a, t))
+        \heuristics(simplify_enlarging)
+    };
+
+    sElementOfSIntersect {
+        \find(sElementOf<[T]>(a, sIntersect<[T]>(s, t)))
+        \replacewith(sElementOf<[T]>(a, s) & sElementOf<[T]>(a, t))
+        \heuristics(simplify_enlarging)
+    };
+
+    sElementOfSSetMinus {
+        \find(sElementOf<[T]>(a, sSetMinus<[T]>(s, t)))
+        \replacewith(sElementOf<[T]>(a, s) & !sElementOf<[T]>(a, t))
+        \heuristics(simplify_enlarging)
+    };
+
+    sElementOfSInfiniteUnion {
+        // TODO: alpha or any (was like this already in locSetsRules)?
+        \schemaVar \variables alpha av;
+        \find(sElementOf<[T]>(a, sInfiniteUnion<[T]>{av;}(s)))
+        \varcond(\notFreeIn(av, a))
+        \replacewith(\exists av; sElementOf<[T]>(a, s))
+        \heuristics(simplify)
+    };
+
+    // --------------------------------------------------------------------------
+    // EQ versions of axioms (these are lemmata)
+    // --------------------------------------------------------------------------
+    sElementOfSUnionEQ {
+        \assumes(sUnion<[T]>(s, t) = EQ ==>)
+        \find(sElementOf<[T]>(a, EQ))
+        \sameUpdateLevel
+        \replacewith(sElementOf<[T]>(a, s) | sElementOf<[T]>(a, t))
+        \heuristics(simplify_enlarging)
+    };
+
+    sElementOfSIntersectEQ {
+        \assumes(sIntersect<[T]>(s, t) = EQ ==>)
+        \find(sElementOf<[T]>(a, EQ))
+        \sameUpdateLevel
+        \replacewith(sElementOf<[T]>(a, s) & sElementOf<[T]>(a, t))
+        \heuristics(simplify_enlarging)
+    };
+
+    sElementOfSetMinusEQ {
+        \assumes(sSetMinus<[T]>(s, t) = EQ ==>)
+        \find(sElementOf<[T]>(a, EQ))
+        \sameUpdateLevel
+        \replacewith(sElementOf<[T]>(a, s) & !sElementOf<[T]>(a, t))
+        \heuristics(simplify_enlarging)
+    };
+
+    sElementOfSInfiniteUnionEQ {
+        // TODO: alpha or any (was like this already in locSetsRules)?
+        \schemaVar \variables alpha av;
+        \assumes(sInfiniteUnion<[T]>{av;}(s) = EQ ==>)
+        \find(sElementOf<[T]>(a, EQ))
+        \sameUpdateLevel
+        \varcond(\notFreeIn(av, a))
+        \replacewith(\exists av; sElementOf<[T]>(a, s))
+        \heuristics(simplify)
+    };
+
+    // --------------------------------------------------------------------------
+    // axioms for cardinality
+    // --------------------------------------------------------------------------
+    sCardNonNegative {
+        \find(sCard<[T]>(s))
+        \sameUpdateLevel
+        \add(sCard<[T]>(s) >= 0 ==>)
+        \heuristics(inReachableStateImplication)
+    };
+
+    sCardSEmpty {
+        \find(sCard<[T]>(sEmpty<[T]>))
+        \replacewith(0)
+        \heuristics(concrete)
+    };
+
+    sCardSSingleton {
+        \find(sCard<[T]>(sSingleton<[T]>(b)))
+        \replacewith(1)
+        \heuristics(simplify)
+    };
+
+    // --------------------------------------------------------------------------
+    // axioms for set predicates (reduce to sElementOf)
+    // --------------------------------------------------------------------------
+
+    sEmptyEqualsSSingleton {
+        \find(sEmpty<[T]> = sSingleton<[T]>(a))
+        \replacewith(false)
+        \heuristics(concrete)
+    };
+
+    sSingletonEqualsSEmpty {
+        \find(sSingleton<[T]>(a) = sEmpty<[T]>)
+        \replacewith(false)
+        \heuristics(concrete)
+    };
+
+    sUnionWithSSingletonEqualsSUnionWithSSingleton {
+        \find(sUnion<[T]>(s, sSingleton<[T]>(a)) = sUnion<[T]>(t, sSingleton<[T]>(a)))
+
+        \replacewith(sSetMinus<[T]>(s, sSingleton<[T]>(a)) = sSetMinus<[T]>(t, sSingleton<[T]>(a)))
+        \heuristics(simplify)
+    };
+
+    sUnionWithSSingletonEqualsSUnionWithSSingleton_2 {
+        \find(sUnion<[T]>(sSingleton<[T]>(a), s) = sUnion<[T]>(sSingleton<[T]>(a), t))
+        \replacewith(sSetMinus<[T]>(s, sSingleton<[T]>(a)) = sSetMinus<[T]>(t, sSingleton<[T]>(a)))
+        \heuristics(simplify)
+    };
+
+    equalityToSElementOf {
+        \schemaVar \variables T av;
+        \find(s = t)
+        \varcond(\notFreeIn(av, s, t))
+        \replacewith(\forall av; (sElementOf<[T]>(av, s) <-> sElementOf<[T]>(av, t)))
+        //\heuristics(semantics_blasting)
+        \heuristics(simplify_enlarging)
+    };
+
+    sSubsetToSElementOf {
+        \schemaVar \variables T av;
+        \find(sSubset<[T]>(s, t))
+        \varcond(\notFreeIn(av, s, t))
+        \replacewith(\forall av; (sElementOf<[T]>(av, s) -> sElementOf<[T]>(av, t)))
+        //\heuristics(semantics_blasting)
+        \heuristics(simplify_enlarging)
+    };
+
+    sDisjointToSElementOf {
+        \schemaVar \variables T av;
+        \find(sDisjoint<[T]>(s, t))
+        \varcond(\notFreeIn(av, s, t))
+        \replacewith(\forall av; (!sElementOf<[T]>(av, s) | !sElementOf<[T]>(av, t)))
+//        \heuristics(semantics_blasting)
+        \heuristics(simplify_enlarging)
+    };
+}

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key

@@ -47,6 +47,7 @@
 \include seqCoreRules, seqRules;
 \include seqPerm;
 \include seqPerm2;
+\include setRules;
 
 // rules for Java (order does not matter, since not provable anyway)
 \include javaRules;

key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java

@@ -1003,6 +1003,7 @@ public static ProofCollection automaticJavaDL() throws IOException {
 
         g = c.group("PolymorphicSorts");
         g.loadable("standard_key/polymorphic/pseq.key");
+        g.provable("standard_key/polymorphic/setExample.key");
 
         // use for debugging purposes.
         // c.keep("VSTTE10");

key.ui/examples/standard_key/polymorphic/setExample.key

@@ -0,0 +1,9 @@
+\sorts {
+    T;
+}
+
+\problem {
+  \forall Set<[T]> s1; (\forall Set<[T]> s2;
+    (sIntersect<[T]>(s1, s2) = sEmpty<[T]> <->
+      (\forall T a; (sElementOf<[T]>(a, s1) -> !sElementOf<[T]>(a, s2)))))
+}