Implementing Sets with Lists
De Morgen laws
We want to prove
S1,S2:Set
(neg (S1 U S2) = neg(S1) & neg (S2) and
neg (S1 & S2) = neg(S1) U neg (S2) )
.
We use attribute coinduction to prove this is a behavorial property of the input specification.
- First, we prove the attribute coherence of the input specification.
- Introduce the
lemma
coherence(SET)
.
- This goal is true because
coherence(SET)
is in the hypothesis.
- Then we prove
S1,S2:Set
(N:Nat ( N in neg (S1 U S2) = N in neg(S1) & neg (S2) ) and
N:Nat ( N in neg (S1 & S2) = N in neg(S1) U neg (S2) ) )
Implementing Sets with Lists
Distributive law for union and intersection
We want to prove
S1,S2,S3:Set
(S1 U (S2 & S3) = (S1 U S2) & (S1 U S3) and
S1 & (S2 U S3) = (S1 & S2) U (S1 & S3) )
.
We use attribute coinduction to prove this is a behavorial property of the input specification.
- First, we prove the attribute coherence of the input specification.
- Introduce the
lemma
coherence(SET)
.
- This goal is true because
coherence(SET)
is in the hypothesis.
- Then we prove
S1,S2,S3:Set
(N:Nat ( N in S1 U (S2 & S3) = N in (S1 U S2) & (S1 U S3) ) and
N:Nat ( N in S1 & (S2 U S3) = N in (S1 & S2) U (S1 & S3) ) )
This page was generated
by Kumo on
Mon Jun 15 13:46:12 PDT 1998
from code written by Grigore Rosu,