My guess would be that a non-empty decoration is possible for Z'SchemaPred to allow for variable decoration during proof operations: if all variables in the characteristic binding are consistently decorated, the resulting term is still Z.

However, not all Z proof operations consistently decorate the variables in the characteristic binding, so the semantic constant Z'SchemaPred is exposed fairly often. (This could be avoided with schema renaming as already done recently.)


On 24/09/11 13:09, Rob Arthan wrote:

On 17 Sep 2011, at 15:06, Phil Clayton wrote:

Using the subgoal package, I have just been trying to quote an
assumption (as a term quotation) but couldn't. On the assumption term,
dest_z_term returns the form

ZSchemaPred (..., "'")

Given, e.g.

(* S : P [a, b : Z] *)
val S = %SZT% S %bigcolon% %bbP% [a, b : %bbZ%] %>%;

is there a way to write a Z term quotation equal to tm1 as follows:

val tm1 = mk_z_schema_pred (S, "'");

? (I can do so in HOL using Z'SchemaPred directly.)

The quick answer is no - the term generator (imp063.doc) never calls
mk_z_schema_pred with non-empty decoration. I need to remind myself
exactly what the decoration in mk_z_schema_pred is for (I know what the
semantics is intended to be but I can't recall why we have it). Perhaps
Roger can cast his mind back to this.

This reminds me that I always meant to make the Z specifications of the
Z to HOL mapping available. As a quick fix, I have put the documents here:

I will make sure they typecheck presently and include them in the doc
directory in future builds.



Proofpower mailing list

Proofpower mailing list

Reply via email to