Z into Isabelle

Question

I am trying to input and prove Z specifications in Isabelle.

Say I have a vending machine specification written in the LaTeX format:

\begin{zed}
    price:\nat
    \end{zed}

\begin{schema}{VMSTATE}
    stock, takings: \nat
    \end{schema}

\begin{schema}{VM\_operation}
    \Delta VMSTATE \\
    cash\_tendered?, cash\_refunded!: \nat \\
    bars\_delivered! : \nat
    \end{schema}

\begin{schema}{exact\_cash}
    cash\_tendered?: \nat
    \where
    cash\_tendered? = price
    \end{schema}

I don't know if I should put the schema's as lemmas or functions?

This is what i have so far:

theory vendingmachine
imports
Main Fact "~~/src/HOL/Hoare/Hoare_Logic"

begin
type_synonym price = nat

type_synonym stock = nat

type_synonym takings = nat

type_synonym cash_tendered = nat

function exact_cash "(cash_tendered:nat)"
where
cash_tendered ≡ price;
end

The type synonyms work fine however when I get to the exact cash schema which I have translated as an exact_cash functions I keep getting errors.

So in summary I would just like to know how to input schema's into isabelle.

Answer 1

Some people developed frameworks for Z-specifications in Isabelle/HOL (other link) a decade ago. (As far as I know, they are not maintained anymore – but maybe they can still be of some help to you.)

Usually, Z-specifications can be rewritten into TLA specifications quite easily. So, you could also try to use the actively maintained HOL-TLA-session of Isabelle.

But let's first stick with common Isabelle/HOL.

Encoding your Z-specification fragment in plain Isabelle/HOL would look something like:

theory VendingMachine
imports
  Main
begin

--"record datatype for the state variables"
record VMSTATE =
  stock :: nat
  takings :: nat

--"a vending machine is parameterized over a price constant"
locale VendingMachine =
fixes price :: nat
begin

definition VM_operation ::
  "VMSTATE ⇒ VMSTATE ⇒ nat ⇒ nat ⇒ nat ⇒ bool"
where "VM_operation vmstate vmstate' cash_tendered cash_refunded bars_delivered ≡
  True" --"TODO: specify predicate"

definition exact_cash ::
  "nat ⇒ bool"
where "exact_cash cash_tendered ≡
  cash_tendered = price"

end

end

Notice that I dropped the distinction between in- and output variables. The Delta-variable VMSTATE in VM_operation is split into vmstate and vmstate'.

To really work with such a specification, you would need some more auxiliary definitions. For instance, the state space of the specification could then be defined as an inductive predicate like, e.g.:

inductive_set state_space :: "VMSTATE set"
where 
  Init: "⦇ stock = 10, takings = 0 ⦈ ∈ state_space"
    --"some initial state for the sake of a meaningful definition...."
| Step: "vmstate ∈ state_space
∧ (∃ cash_tendered cash_refunded bars_delivered .
   VM_operation vmstate vmstate' cash_tendered cash_refunded bars_delivered)
⟹ vmstate' ∈ state_space"