(*T* 

\usection{A State Space with Typed Variables}\label{sect-ssvars}

While the state space in the previous section and in fact most of the
modules of the temporal logic libray are kept as abstract as possible,
we describe here an instantiation of the abstract frame to a a state
space of a more specific kind. In what we call a {\em state space with
typed variables} we define a state as a function assigning values to
variables which are equipped with types in CIC. A state space with
variables is not only used for UNITY programs \cite{ChandyMisra88} and
in other approaches such as \cite{MannaPnueli92}, but it can also
serve as the state space of places/transition nets or high-level Petri
nets if places are regarded as variables containing natural numbers or
multisets, respectively. Our state space is strictly typed, in the
sense that each variable has a well defined type and type correctness
of the values of a variable is enforced by the type theory. Reasoning
about such state spaces in an abstract setting becomes possible here
due to the use of dependent types and universes in CIC.

The following should be understood as a modification of the module
|abstract| given in the previous section. The modification is obtained
by replacing the abstract declaration of |st| by a more concrete
definition and by adding what we describe below.  To emphasize that
the present module is an instantiation of |abstract| we call it
|var_abstract|.
 
We begin by declaring a type |var| of system variables.  For a
particular system this type contains the names of variables used. It
is important not to confuse these variables with the variables of the
temporal logic which will directly be represented as variables of
CIC. 

\begin{verbatim}
Variable var:Type. 
\end{verbatim}

Since we need an induction principle for variables we assume
finiteness of |var| by requiring that every variable |v| has an index
w.r.t. to some enumeration |ith_var| which is smaller than a constant
|vars|.

\begin{verbatim}
Variable vars : nat. 
Variable ith_var : nat->var.
Hypothesis var_finite : (v:var)
  (Ex [i:nat] (lt i vars) /\ (ith_var i)==v).
\end{verbatim}

Moreover, in order to define standard operations such as assignment as
type-theoretic functions, we assume that equality of variables is
decidable, that is that there is an operation |var_eq_dec| such that for each two
variables |v| and |v'|, |(var_eq_dec v v')| returns an object of a
disjoint union type which is a tagged proof of |(v==v')| or
|~(v==v')|.

\begin{verbatim}
Hypothesis var_eq_dec:(v,v':var){(v==v')}+{~(v==v')}.
\end{verbatim}

We furthermore introduce a type |type_name| of type names and an operation |type|
that associates a CIC type with each type name. It is a good example
of the use of universes, which allow us to use CIC types in system
specifications and to deal with them as first class citizens.

\begin{verbatim}
Variable type_name:Type.
Variable type:type_name->Type.
\end{verbatim}

Now by the operation |var_type_name| we associate a type name to each
variable and we define |var_type| as a convenient abbreviation to
refer to the type of a variable directly. We often do not distinguish
type names and their associated types in informal explanations.
 
\begin{verbatim}
Variable var_type_name:var->type_name.

Definition var_type := [v:var] (type (var_type_name v)).
\end{verbatim}

Finally, we introduce |st| as the type of states by means of a
definition which replaces the declaration of |st| in |abstract|. A
state associates a value of the variable's type to each variable.

\begin{verbatim}
Definition st := (v:var)(var_type v).
\end{verbatim}

Notice that the dependent function space allows us to define this
state space with typed variables in a concise way, which precisely
corresponds to the usual set-theoretic definition. In contrast to set
theory, the fact that a term denotes a state can be verified by
automatic typechecking, thereby avoiding the need for an explicit
proof.

At the present state of the development the temporal logic library
contains the following three modules to support the notion of a state
space with typed variables: The module |var_state_ops|, which is
explained in the next section, introduces equality and assignment
operators and related theorems for a state space with typed variables.
The module |var_state_pred| formalizes the (in)dependence of a state
property from a variable, provides a notion of substitution of
variables, and proves some elemantary theorems. The module |var_elim|
demonstrates its use by proving Misra's elimination theorem, which in
fact presupposes a notion of state with variables.

\begin{verbatim}
Load var_state_ops. 
Load var_state_pred. 
Load var_elim.
\end{verbatim}

*T*)

(*BEGIN-H*)

Load init. 

Variable var:Type. 

Variable vars : nat. 
Variable ith_var : nat->var.

Hypothesis var_finite : (v:var)
  (Ex [i:nat] (lt i vars) /\ (ith_var i)==v).

Hypothesis var_eq_dec:(v,v':var){(v==v')}+{~(v==v')}.

Variable type_name:Type.

Hypothesis type_name_eq_dec:
  (n,n':type_name){(n==n')}+{~(n==n')}.

Variable type:type_name->Type.

Variable var_type_name:var->type_name.

Definition var_type := [v:var] (type (var_type_name v)).

Definition st := (v:var)(var_type v).

Load var_state_ops.

Variable act:Type.

Hypothesis act_eq_dec:(e,e':act){(e==e')}+{~(e==e')}.

Variable trans : act->st->st->Prop .

Definition view := act->Prop.

Load state_pred. 

Load safety.

Variable wf : (set (set act)).

Hypothesis wf_contains_empty_set : 
  (In (set act) wf (Empty_set act)).

Load liveness.

Load composition.

Load var_state_pred. 
Load var_elim.

(*END-H*)