Skip to content

Commit d68e7db

Browse files
wadoonwadoon
authored
Basic Theory of Sets (#3777)
2 parents c3a6418 + 8819422 commit d68e7db

6 files changed

Lines changed: 209 additions & 0 deletions

File tree

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@
2525
"./permission/permission.key",
2626
reach,
2727
"./sequence/seq.key",
28+
"./set/set.key",
2829
stringDef,
2930
map,
3031
freeADT,

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
4+
5+
\sorts {
6+
\generic T;
7+
Set<[T]>;
8+
}
9+
10+
\functions {
11+
\unique Set<[T]> sEmpty<[T]>;
12+
13+
// other constructors
14+
Set<[T]> sSingleton<[T]>(T);
15+
Set<[T]> sUnion<[T]>(Set<[T]>, Set<[T]>);
16+
Set<[T]> sIntersect<[T]>(Set<[T]>, Set<[T]>);
17+
Set<[T]> sSetMinus<[T]>(Set<[T]>, Set<[T]>);
18+
Set<[T]> sInfiniteUnion<[T]>{true}(Set<[T]>);
19+
20+
int sCard<[T]>(Set<[T]>);
21+
}
22+
23+
\predicates {
24+
sElementOf<[T]>(T, Set<[T]>);
25+
sSubset<[T]>(Set<[T]>, Set<[T]>);
26+
sDisjoint<[T]>(Set<[T]>, Set<[T]>);
27+
}

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

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
4+
5+
\schemaVariables {
6+
\term T a, b;
7+
\term Set<[T]> s, t, EQ;
8+
}
9+
10+
\rules {
11+
12+
// --------------------------------------------------------------------------
13+
// axioms for sElementOf
14+
// --------------------------------------------------------------------------
15+
16+
sElementOfSEmpty {
17+
\find(sElementOf<[T]>(a, sEmpty<[T]>))
18+
\replacewith(false)
19+
\heuristics(concrete)
20+
};
21+
22+
sElementOfSSingleton {
23+
\find(sElementOf<[T]>(a, sSingleton<[T]>(b)))
24+
\replacewith(a = b)
25+
\heuristics(simplify)
26+
};
27+
28+
sElementOfSUnion {
29+
\find(sElementOf<[T]>(a, sUnion<[T]>(s, t)))
30+
\replacewith(sElementOf<[T]>(a, s) | sElementOf<[T]>(a, t))
31+
\heuristics(simplify_enlarging)
32+
};
33+
34+
sElementOfSIntersect {
35+
\find(sElementOf<[T]>(a, sIntersect<[T]>(s, t)))
36+
\replacewith(sElementOf<[T]>(a, s) & sElementOf<[T]>(a, t))
37+
\heuristics(simplify_enlarging)
38+
};
39+
40+
sElementOfSSetMinus {
41+
\find(sElementOf<[T]>(a, sSetMinus<[T]>(s, t)))
42+
\replacewith(sElementOf<[T]>(a, s) & !sElementOf<[T]>(a, t))
43+
\heuristics(simplify_enlarging)
44+
};
45+
46+
sElementOfSInfiniteUnion {
47+
// TODO: alpha or any (was like this already in locSetsRules)?
48+
\schemaVar \variables alpha av;
49+
\find(sElementOf<[T]>(a, sInfiniteUnion<[T]>{av;}(s)))
50+
\varcond(\notFreeIn(av, a))
51+
\replacewith(\exists av; sElementOf<[T]>(a, s))
52+
\heuristics(simplify)
53+
};
54+
55+
// --------------------------------------------------------------------------
56+
// EQ versions of axioms (these are lemmata)
57+
// --------------------------------------------------------------------------
58+
sElementOfSUnionEQ {
59+
\assumes(sUnion<[T]>(s, t) = EQ ==>)
60+
\find(sElementOf<[T]>(a, EQ))
61+
\sameUpdateLevel
62+
\replacewith(sElementOf<[T]>(a, s) | sElementOf<[T]>(a, t))
63+
\heuristics(simplify_enlarging)
64+
};
65+
66+
sElementOfSIntersectEQ {
67+
\assumes(sIntersect<[T]>(s, t) = EQ ==>)
68+
\find(sElementOf<[T]>(a, EQ))
69+
\sameUpdateLevel
70+
\replacewith(sElementOf<[T]>(a, s) & sElementOf<[T]>(a, t))
71+
\heuristics(simplify_enlarging)
72+
};
73+
74+
sElementOfSetMinusEQ {
75+
\assumes(sSetMinus<[T]>(s, t) = EQ ==>)
76+
\find(sElementOf<[T]>(a, EQ))
77+
\sameUpdateLevel
78+
\replacewith(sElementOf<[T]>(a, s) & !sElementOf<[T]>(a, t))
79+
\heuristics(simplify_enlarging)
80+
};
81+
82+
sElementOfSInfiniteUnionEQ {
83+
// TODO: alpha or any (was like this already in locSetsRules)?
84+
\schemaVar \variables alpha av;
85+
\assumes(sInfiniteUnion<[T]>{av;}(s) = EQ ==>)
86+
\find(sElementOf<[T]>(a, EQ))
87+
\sameUpdateLevel
88+
\varcond(\notFreeIn(av, a))
89+
\replacewith(\exists av; sElementOf<[T]>(a, s))
90+
\heuristics(simplify)
91+
};
92+
93+
// --------------------------------------------------------------------------
94+
// axioms for cardinality
95+
// --------------------------------------------------------------------------
96+
sCardNonNegative {
97+
\find(sCard<[T]>(s))
98+
\sameUpdateLevel
99+
\add(sCard<[T]>(s) >= 0 ==>)
100+
\heuristics(inReachableStateImplication)
101+
};
102+
103+
sCardSEmpty {
104+
\find(sCard<[T]>(sEmpty<[T]>))
105+
\replacewith(0)
106+
\heuristics(concrete)
107+
};
108+
109+
sCardSSingleton {
110+
\find(sCard<[T]>(sSingleton<[T]>(b)))
111+
\replacewith(1)
112+
\heuristics(simplify)
113+
};
114+
115+
// --------------------------------------------------------------------------
116+
// axioms for set predicates (reduce to sElementOf)
117+
// --------------------------------------------------------------------------
118+
119+
sEmptyEqualsSSingleton {
120+
\find(sEmpty<[T]> = sSingleton<[T]>(a))
121+
\replacewith(false)
122+
\heuristics(concrete)
123+
};
124+
125+
sSingletonEqualsSEmpty {
126+
\find(sSingleton<[T]>(a) = sEmpty<[T]>)
127+
\replacewith(false)
128+
\heuristics(concrete)
129+
};
130+
131+
sUnionWithSSingletonEqualsSUnionWithSSingleton {
132+
\find(sUnion<[T]>(s, sSingleton<[T]>(a)) = sUnion<[T]>(t, sSingleton<[T]>(a)))
133+
134+
\replacewith(sSetMinus<[T]>(s, sSingleton<[T]>(a)) = sSetMinus<[T]>(t, sSingleton<[T]>(a)))
135+
\heuristics(simplify)
136+
};
137+
138+
sUnionWithSSingletonEqualsSUnionWithSSingleton_2 {
139+
\find(sUnion<[T]>(sSingleton<[T]>(a), s) = sUnion<[T]>(sSingleton<[T]>(a), t))
140+
\replacewith(sSetMinus<[T]>(s, sSingleton<[T]>(a)) = sSetMinus<[T]>(t, sSingleton<[T]>(a)))
141+
\heuristics(simplify)
142+
};
143+
144+
equalityToSElementOf {
145+
\schemaVar \variables T av;
146+
\find(s = t)
147+
\varcond(\notFreeIn(av, s, t))
148+
\replacewith(\forall av; (sElementOf<[T]>(av, s) <-> sElementOf<[T]>(av, t)))
149+
//\heuristics(semantics_blasting)
150+
\heuristics(simplify_enlarging)
151+
};
152+
153+
sSubsetToSElementOf {
154+
\schemaVar \variables T av;
155+
\find(sSubset<[T]>(s, t))
156+
\varcond(\notFreeIn(av, s, t))
157+
\replacewith(\forall av; (sElementOf<[T]>(av, s) -> sElementOf<[T]>(av, t)))
158+
//\heuristics(semantics_blasting)
159+
\heuristics(simplify_enlarging)
160+
};
161+
162+
sDisjointToSElementOf {
163+
\schemaVar \variables T av;
164+
\find(sDisjoint<[T]>(s, t))
165+
\varcond(\notFreeIn(av, s, t))
166+
\replacewith(\forall av; (!sElementOf<[T]>(av, s) | !sElementOf<[T]>(av, t)))
167+
// \heuristics(semantics_blasting)
168+
\heuristics(simplify_enlarging)
169+
};
170+
}

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,7 @@
4747
\include "./sequence/seqCoreRules.key", "./sequence/seqRules.key";
4848
\include "./sequence/seqPerm.key";
4949
\include "./sequence/seqPerm2.key";
50+
\include "./set/setRules.key";
5051

5152
// rules for Java (order does not matter, since not provable anyway)
5253
\include javaRules;

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1017,6 +1017,7 @@ public static ProofCollection automaticJavaDL() throws IOException {
10171017

10181018
g = c.group("PolymorphicSorts");
10191019
g.loadable("standard_key/polymorphic/pseq.key");
1020+
g.provable("standard_key/polymorphic/setExample.key");
10201021

10211022
g = c.group("JavaFeatures");
10221023
g.loadable("Java/TextBlockLiterals/project.key");

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
\sorts {
2+
T;
3+
}
4+
5+
\problem {
6+
\forall Set<[T]> s1; (\forall Set<[T]> s2;
7+
(sIntersect<[T]>(s1, s2) = sEmpty<[T]> <->
8+
(\forall T a; (sElementOf<[T]>(a, s1) -> !sElementOf<[T]>(a, s2)))))
9+
}

0 commit comments

Comments
 (0)