Phil,

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:

http://dl.dropbox.com/u/34693999/zed002.pdf
http://dl.dropbox.com/u/34693999/zed003.pdf
http://dl.dropbox.com/u/34693999/zed005.pdf

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

Regards,

Rob.

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

Reply via email to