# Re: [ProofPower] Proving properties of Z types.

On Tuesday 16 June 2009 14:47:55 Frank Zeyda wrote:
>Dear ProofPower Users,
>
>I have a little observation which I would like to confirm. The problem
>is as follows. I defined a new Z type NAME by
>
>[NAME]
>
>and then introduced a set ALPHABET to refer to the subsets of NAME by
>
>ALPHABET == P NAME

It seems odd for an alphabet to be a set of names,
it sounds more like a set of characters from which
one might form names as sequences.

>At some point it showed to be necessary to construct fresh names for any
>given alphabet, i.e. which are not in the alphabet. In that, I attempted
>to prove the following theorem.
>
>FORALL a : ALPHABET @ (EXISTS n : NAME @ n \not \in a)
>
>I assumed it would be sufficient to restrict the set alphabet to finite
>subsets of name, for instance using the following definition for
>
>ALPHABET == F NAME
>
>but I think this is not the case. For a new Z type, the defining axiom
>we obtain is that the Z type constant (i.e. NAME) is equal to the
>universe over a certain, newly introduced, HOL type (here z'NAME); a HOL
>constant "Universe" is used to refer to the carrier set of a HOL type.
>It guarantees that any x of the correct (HOL) type is an element of the
>respective (type-instantiated) Universe, that x is not an element of the
>empty set which I suppose excludes the case of an empty universe, and a
>property regarding the Insert functions to reason about enumerated sets.

I'm puzzled where this came from.
In ProofPower when you introduce a given set NAME you get a
new HOL type z'NAME (as you say) about which nothing is specified
(but all types are non-empty), and you get a new Z constant NAME
defined by NAME = BBU.
BBU (the double bold U symbol) is difficult to unpick because
for Z it behaves as a primitive, but it is in fact the set of
all elements of the type x'NAME.  The proof system knows enough
about BBU that you should not need to think about what's happening
underneath but simply understand that it is the set of all elements
of some type, and the type will be determined by type inference.

> From this alone one cannot prove that the corresponding Universe is
>infinite.

yes, it might be finite, for all anyone knows.

>The underlying HOL type of the new Z type, i.e. here "z'NAME
>SET" I think defines a representation function that equates the type of
>a set with functions over some new HOL type into BOOL, but again I think
>this cannot be used to prove that "z'NAME SET" is infinite unless
>"z'NAME" is (?!).

Yes. The HOL type constructor SET, which is used also for sets in
Z, is represented by propositional functions.  In HOL SETs are
just different ways of talking about propositional functions.
(though you can introduce other kinds of set if you like)>

>In that, I suppose if we want a Z type to be infinite,
>we need to explicitly state it, that is by an axiom along the lines of
>
>EXISTS f : z'NAME -> z'NAME @ (OneOne f) /\ ¬ Onto f
>
>(Similar to the infinity_axiom in the HOL theory init.)

Though it might be better in this case to use

F NAME propersubsetof P NAME

>Or alternatively (maybe more useful when doing the proofs in Z rather
>than HOL) that there exists an injective Z function from N to the
>carrier set of the new type. The only type in ProofPower-Z that
>explicitly claims its infinite seems to be the type IND.

Though there are many others which are easily seen to be.
e.g. N or seq T for any type T.

>However, there
>seems no way to prove that for a newly introduce HOL type there is an
>injective function from IND to the elements of that. Even further, it
>seems not possible to prove that there are two distinct elements in a
>newly introduced Z type. For example, the consistency axioms for
>
>| x, y : NAME
>
>-------------
>
>| x =/= y
>
>Appear not to be provable by the defining axiom for NAME, unless we
>introduce some axiom stating properties of the cardinality of NAME.

All this is consistent (I believe) with the Z standard.

>If someone could confirm or refute the above that would be great.

Yes.  However, you should not really need to know any of the
stuff about how this is done in HOL.
The given sets are implemented as they should be in Z
and U is well understood by the Z proof contexts.

>As a side-issue, I realised the automatic proof support for finite sets
>is not as well developed as that for (possibly infinite) sets. I proved
>a couple of theorems that could be useful, for instance discharging that
>every enumerated set is finite. It may be worth introducing a new Z
>component proof context for finite sets.

The place to look for theorems about finiteness is in
the maths examples, wrk073.pdf, not part of the standard
distribution.
However, this is all HOL, so to use it in Z you will need
to understand the relations between HOL and Z.

However, I'm not convinced that you need it for the purposes
described.  If you just add the constraint I mentioned above
then you should always be able to find new elements (I suppose
you need to know that the union of two finite sets is finite).

A proof context would be nice!

Roger Jones

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com