Implementing Sets with Lists
Associativity of intersection

We want to prove

S1,S2,S3:Set (S1 & (S2 & S3) = (S1 & S2) & 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 & (S2 & S3) = N in (S1 & S2) & S3
Implementing Sets with Lists

Commutativity of intersection

We want to prove

S1,S2:Set (S1 & S2 = S2 & S1) .
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 S1 & S2 = N in S2 & S1 ))
Implementing Sets with Lists

Idempotency of intersection

We want to prove

S1:Set (S1 & S1 = S1) .
We use attribute coinduction to prove this is a behavorial property of the input specification.


This page was generated
by Kumo on Mon Jun 15 13:45:41 PDT 1998 from code written by Grigore Rosu,