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