On 27/09/11 13:25, Roger Bishop Jones wrote:
On Sunday 25 Sep 2011 16:20, Phil Clayton wrote:
Although the Z'SchemaPred semantic constant enables
renaming to be avoided, Z'SchemaPred HOL terms are not
Z when the schema components are decorated
inconsistently. So perhaps renaming is useful?
On 28/09/11 13:40, Phil Clayton wrote:
On 27/09/11 13:25, Roger Bishop Jones wrote:
On Sunday 25 Sep 2011 16:20, Phil Clayton wrote:
Although the Z'SchemaPred semantic constant enables
renaming to be avoided, Z'SchemaPred HOL terms are not
Z when the schema components are decorated
On Wednesday 28 Sep 2011 13:52, Phil Clayton wrote:
I wondered whether the original design intended to map
decoration differently for predicates and expressions?
Then the user could determine the mapping of e.g. S'
as either
mk_z_schema_pred (S, ')
mk_z_schema_pred (mk_z_decor%down%s
On Sunday 25 Sep 2011 16:20, Phil Clayton wrote:
Although the Z'SchemaPred semantic constant enables
renaming to be avoided, Z'SchemaPred HOL terms are not
Z when the schema components are decorated
inconsistently. So perhaps renaming is useful?
I'm sure it is.
But I doubt that it is
On Saturday 24 Sep 2011 22:53, Roger Bishop Jones wrote:
On Saturday 24 Sep 2011 13:09, Rob Arthan wrote:
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
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
On 25/09/11 10:04, Roger Bishop Jones wrote:
On Saturday 24 Sep 2011 22:53, Roger Bishop Jones wrote:
On Saturday 24 Sep 2011 13:09, Rob Arthan wrote:
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
On Saturday 24 Sep 2011 13:09, Rob Arthan wrote:
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
