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) ) )
Quantifier elimination introduces new
constants s1 s2 :Set
.
Conjunction elimination introduces subgoals as follows:
forall N:Nat ( N in neg (s1 U s2) = N in neg(s1) & neg (s2) )
.
Quantifier elimination introduces new
constant n :Nat
.
Show
( n in neg (s1 U s2) = n in neg(s1) & neg (s2) )
by reduction.
forall N:Nat ( N in neg (s1 & s2) = N in neg(s1) U neg (s2) )
.
Quantifier elimination introduces new
constant n :Nat
.
Show
( n in neg (s1 & s2) = n in neg(s1) U neg (s2) )
by reduction.
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) ) )
Quantifier elimination introduces new
constants s1 s2 s3 :Set
.
Conjunction elimination introduces subgoals as follows:
forall N:Nat ( N in s1 U (s2 & s3) = N in (s1 U s2) & (s1 U s3) )
.
Quantifier elimination introduces new
constant n :Nat
.
Show
( n in s1 U (s2 & s3) = n in (s1 U s2) & (s1 U s3) )
by reduction.
forall N:Nat ( N in s1 & (s2 U s3) = N in (s1 & s2) U (s1 & s3) )
.
Quantifier elimination introduces new
constant n :Nat
.
Show
( n in s1 & (s2 U s3) = n in (s1 & s2) U (s1 & s3) )
by reduction.
This page was generated
by Kumo on
Mon Jun 15 13:46:12 PDT 1998
from code written by Grigore Rosu,