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`

## Advertising

[NAME] and then introduced a set ALPHABET to refer to the subsets of NAME by ALPHABET == P NAME

`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 instead.`

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.`

`From this alone one cannot prove that the corresponding Universe is`

`infinite. 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 (?!). 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.)

`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. 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.`

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

`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.`

Many Thanks, Frank -- Dr Dipl.-Inform. Frank Zeyda Research Associate High Integrity Systems Engineering Group Department of Computer Science University of York (UK) Email: ze...@cs.york.ac.uk Phone: 0044-(0)1904-433244 WWW: http://www-users.cs.york.ac.uk/~zeyda/ -- Dr Dipl.-Inform. Frank Zeyda Research Associate High Integrity Systems Engineering Group Department of Computer Science University of York (UK) Email: ze...@cs.york.ac.uk Phone: 0044-(0)1904-433244 WWW: http://www-users.cs.york.ac.uk/~zeyda/ _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com