Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: David Shepherd <des@uk.co.inmos>
Message-Id: <5768.9206260821@frogland.inmos.co.uk>
Subject: Re: Looking for someone with experience translating Z to HOL
To: weiss872@edu.uidaho.cs.snake (Phil Weiss)
Date: Fri, 26 Jun 92 9:21:40 BST
Cc: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
In-Reply-To: <199206251918.AA03966@snake.cs.uidaho.edu>; from "Phil Weiss" at Jun 25, 92 12:18 pm

Phil Weiss has said:
> 
> 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.

why not just define Oper as a relation. i.e.:

  ! ts ts'. Oper ts ts' = (*** predicate from Oper schema ***)

especially as in the spec you give Oper is NOT a function ... it makes
no restriction on State' (unless your using the Z kludge that things
I don't mention don't change).


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk or des@inmos.com    tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"i speak latin to god,   spanish to men,   french to women 
		 and german to my horse."             - charles v of spain