[ProofPower] proof support for sequences in z

[Rob Arthan]

On Tuesday 31 Jan 2006 8:49 pm, Gift Nuka wrote:
> i have not been able to use the theorems in theory z_sequences1.  for
> example i would expect the following to be proved using
> z_^_singleton_thm or z_^_singleton_thm1, where x and y are all singletons
>      <x>^<y> = <x,y>

The following does the job:

set_goal([], %SZT% %lseq%x%rseq% %cat% %lseq%y%rseq% = %lseq%x, y%rseq% %>%);
a(rewrite_tac[z_seqd_%cat%_rw_thm, z_seqd_%cat%_%lseq%%rseq%_clauses]);
val thm = pop_thm();

The theorems you were trying would only apply to the right-hand side of your 
equation and have a condition implicit in the declaration, something like "s 
: (seq _)". The theorems with "seqd" in the name are tuned for working with 
sequence displays (which are automatically known to be sequences).

Regards,

Rob.