Duck Source Code:
Implementing Sets with Lists


title:> Implementing Sets with Lists
spec:> /net/beowulf/grad/klin/tmp/set2.obj
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>
:> exp /net/beowulf/grad/klin/he/bset-g0-exp.html
:> 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>
:> exp /net/beowulf/grad/klin/he/bset-g1-exp.html
:> 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> 
:> exp /net/beowulf/grad/klin/he/bset-g2-exp.html
:> 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> 
:> exp /net/beowulf/grad/klin/he/bset-g3-exp.html
:> 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>
:> exp /net/beowulf/grad/klin/he/bset-g4-exp.html
:> 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