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

All my attempts result in a term equal to tm2 as follows:

  val tm2 = mk_z_schema_pred (mk_z_decor%down%s (S, "'"), "");

tm1 and tm2 are equivalent so this is hardly an issue for writing Z specifications but can make quoting terms awkward. In the end, I just referred to the assumption by index.

Phil



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

Reply via email to