## Duck Source Code: Implementing Sets with Lists

```title:> Implementing Sets with Lists
dir:> /net/cs/htdocs/groups/tatami/demos/bset
homepage:> /net/cs/htdocs/users/goguen/ktext/bset.hp
author:> Grigore Rosu
<>
****************************************************************************************
goal:> coherence(SET)
****************************************************************************************
:> subtitle: We prove coherence of the theory <font color=blue> SET </font>. <hr>
:> Coherence
:> Simplify
:> Simplify
:> Simplify
:> Simplify
<>
*******************************************************************************************
goal:> (forall L:List  forall N:Nat  N in nil = false) and
(forall L:List  forall M:Nat  forall N:Nat  \$ N in cons(M, L) = N == M or N in L \$)
********************************************************************************************
:> subtitle:  <font color=blue> LIST </font>is a refinement of <font color=blue>SET</font>. <hr>
:> Conjunction-Eli
:> Quantifier-Eli-All
:> Reduction(LIST)
:> Quantifier-Eli-All
:> Reduction(LIST)
<>
*********************************************************************************
goal:> forall S1:Set forall S2:Set forall S3:Set S1 U (S2 U S3) = (S1 U S2) U S3
*********************************************************************************
:> subtitle: <b>Associativity of union</b> <hr>
:> A-Coinduction(SET)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/bset/g0
:> Direct-Check
:> Simplify
******************************************************************************************
goal:> forall S1:Set  empty U S1 =  S1
******************************************************************************************
:> subtitle: <hr><b>The empty set is the unit of union.</b> <hr>
:> A-Coinduction(SET)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/bset/g0
:> Direct-Check
:> Simplify
********************************************************************************************
goal:> forall S1:Set S1 U S1 = S1
********************************************************************************************
:> subtitle:  <hr><b>Idemopotency of union</b><hr>
:> A-Coinduction(SET)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/bset/g0
:> Direct-Check
:> Simplify
*********************************************************************************
goal:> forall S1:Set forall S2:Set S1 U S2 = S2 U S1
*********************************************************************************
:> subtitle:  <hr><b>Commutativity of union </b><hr>
:> A-Coinduction(SET)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/bset/g0
:> Direct-Check
:> Simplify
<>
*********************************************************************************
goal:> forall S1:Set forall S2:Set forall S3:Set S1 & (S2 & S3) = (S1 & S2) & S3
*********************************************************************************
:> subtitle: <b>Associativity of intersection</b> <hr>
:> A-Coinduction(SET)
:> Lemma-Introduction    http://www.cs.ucsd.edu/groups/tatami/demos/bset/g0
:> Direct-Check
:> Simplify
*********************************************************************************
goal:> forall S1:Set forall S2:Set S1 & S2 = S2 & S1
*********************************************************************************
:> subtitle: <hr><b>Commutativity of intersection</b> <hr>
:> A-Coinduction(SET)
:> Lemma-Introduction    http://www.cs.ucsd.edu/groups/tatami/demos/bset/g0
:> Direct-Check
:> Simplify
*********************************************************************************
goal:> forall S1:Set  S1 & S1 = S1
*********************************************************************************
:> subtitle: <hr><b>Idempotency  of intersection</b> <hr>
:> A-Coinduction(SET)
:> Lemma-Introduction   http://www.cs.ucsd.edu/groups/tatami/demos/bset/g0
:> Direct-Check
:> Simplify
<>
*********************************************************************************
goal:> forall S1:Set  forall S2:Set  (
neg (S1 U S2) = neg(S1) & neg (S2) and
neg (S1 & S2) = neg(S1) U neg (S2)  )
*********************************************************************************
:> subtitle: <b>De Morgen laws</b> <hr>
:> A-Coinduction(SET)
:> Lemma-Introduction   http://www.cs.ucsd.edu/groups/tatami/demos/bset/g0
:> Direct-Check
:> Simplify
*********************************************************************************
goal:> forall S1:Set  forall S2:Set forall S3:Set (
S1 U (S2 & S3) = (S1 U S2) & (S1 U S3) and
S1 & (S2 U S3) = (S1 & S2) U (S1 & S3) )
*********************************************************************************
:> subtitle: <hr><b> Distributive law for union and intersection </b><hr>
:> A-Coinduction(SET)
:> Lemma-Introduction   http://www.cs.ucsd.edu/groups/tatami/demos/bset/g0
:> Direct-Check
:> Simplify
<>

```

[Back]
Mon Jun 15 13:44:10 PDT 1998