A Framework for Reasoning on Component Composition - Formal Methods for Components and Objects - page 13

constdefs CorrectComponentWeak:: Component ⇒ bool
CorrectComponentWeak c == CorrectComponentStructure c
∧ distinct (RqIdList c) ∧ distinct (map getName(cpList c))

constdefs CorrectComponentWeakList:: Component list ⇒ bool
CorrectComponentWeakList CL == (CorrectComponentStructureList CL)
∧ distinct (RqIdListList CL) ∧ distinct (map getName (cpListlist CL))

3.5 Basic Properties on Component Structure and Manipulation

In this section, we present a few properties that we proved. They deal with
the constructs presented in Section 3.2, and are unrelated to our definition of
states presented in the last section. Those lemmas are the basic building blocks
on which most of our proofs rely. On the set of more than 80 lemmas dealing
with cpSets and cpLists , we focus on the most useful and significant ones. In
particular, we choose to show rather lemmas dealing with the cpSet construct
because it is a higher-level one and thus reasoning on sets of components is
often preferable, when possible. Note however that most of the proofs dealing
with distinctness of component names will rather use cpLists .
We start by an easy lemma quite heavily used and very easy to prove. It states
that C is always in cpSet(C) (it is proved by cases on C ).

lemma cpSetFirst: C ∈ cpSet C

The set of components inside a composite one can be decomposed as follows. It
can be separated into the composite itself plus all the components in the cpSet
of each sub-component.

lemma cpSetcomposite:
cpSet (Composite N itfs sub b s)={Composite N itfs sub b s}
∪ {C. ∃ C' ∈ set sub. C ∈ cpSet C'}

This lemma is proved by an induction on lists of subcomponents. Conversely, we
can prove that, if a component is in the cpSet of a subcomponent of a composite,
it is in the cpSet of the composite. We also present a more general variant of
this lemma stating that if C'' is inside C' and C' is inside C then C'' is inside C .

lemma cpSetcomposite_rev:

C ∈ set sub; C' ∈ cpSet C

= ⇒ C' ∈ cpSet (Composite N itfs sub b s)

lemma cpSetcpSet: C'' ∈ cpSet C';C' ∈ cpSet C = ⇒ C'' ∈ cpSet C

Although those two lemmas are very easy to prove (by induction on the compo-
nent structure), they are massively used in the other proofs.
Another theorem almost automatically proved by Isabelle, but exceedingly
useful is the following one. It gives another formulation of the getCp construct.

lemma getCp_inlist: CL^N=Some C = ⇒ C ∈ set CL ∧ getName C=N