Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <22814-0@swan.cl.cam.ac.uk>; Thu, 25 Jun 1992 20:29:43 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02781;
          Thu, 25 Jun 92 12:17:59 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from snake.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) id AA02773;
          Thu, 25 Jun 92 12:17:54 -0700
Received: by snake.cs.uidaho.edu id AA03966 (5.65c/IDA-1.4.4 
          for info-hol@ted.cs.uidaho.edu); Thu, 25 Jun 1992 12:18:47 -0700
From: Phil Weiss <weiss872@edu.uidaho.cs.snake>
Message-Id: <199206251918.AA03966@snake.cs.uidaho.edu>
Subject: Looking for someone with experience translating Z to HOL
To: info-hol@edu.uidaho.cs.ted
Date: Thu, 25 Jun 92 12:18:46 PDT
Cc: weiss@edu.uidaho.cs.leopard
X-Mailer: ELM [version 2.3 PL11]

I have a Z spec I am translating to HOL.  I have chosen to model
the system state as a type in HOL.

  \begin{schema}{State}
    Function : X -> Y
    Set : X
  \end{schema}

An operation on this state is specified as such:

  \begin{schema}{Oper}
    \Delta State
  \where
    \exists_1 n: X @
      n \in Set \land n \in \dom Function
  \end{schema}

The state becomes a type in HOL, with selectors Function and Set, so that

    HOL                  Z
  (Function x)    =    (x.Function)
  (Set x)         =    (x.Set)

are used to extract the components.

My gut instinct is to define Oper (using HOL's new_specification)
so that

  \forall ts' ts @
   (ts' = Oper ts) \implies (*** predicate from Oper schema ***)

but I am not sure that this can be done, because HOL does not support
partial functions.  It occurred to me that I can define Oper so that

  \forall ts' ts @
   (*** predicate from Oper schema ***) ==> (ts' = Oper ts)

but I don't think that this is correct.

I would appreciate anyone who has any experience giving me some help
with this.  Thanks.

Phil.