Download Theorem Proving Support - Developers Manual

D33.2b - Theorem Proving Support - Dev. Man. (Public)
inductive vbasic_type_rel ::
"vbasic ⇒ vbasict ⇒ bool" (infix ":b " 50) where
BoolI_type[intro!]: "BoolI x :b BoolBT" |
BotI_type[intro]: "BotI a :b a" |
ChanI_type[intro!]: "ChanI n t :b ChanBT" |
CharI_type[intro!]: "CharI x :b CharBT" |
EvI_type[intro!]: "v :b t =⇒ EvI n t v :b EventBT" |
FinI_type[intro]:
"[[ ∀ x∈set xs. x :b a; sorted xs; distinct xs ]]
=⇒ FinI a xs :b FSetBT a" |
Table 4: CML basic type relation
therefore would support higher-order functions. However, for the purpose of
this project first-order functions are deemed sufficient.
Rather than implementing a host of numeric types, we opt for implementing
just one, NumberI, which carries a real number. All other numeric values can
be injected into this, and this makes numeric subtyping easier. The usual
types such as booleans, characters and lists are implementing using HOL
types. VDM specific types such as quote types (QuoteI) and token types
(TokenI) are also implemented. Records are implemented as tagged types
(TagI). A record is simply encoded as a product type (PairI) together with
a tag string which distinguishes it from other records with the same fields.
Specific to CML we also implement event types (EvI), which consist of a
UTP name, type and value content, and channel types (ChanI). Additionally
we provide the bottom value, BotI, which represents an undefined value of
a particular type.
At this level finite sets (FinI) and finite maps (MapI) are implemented simply
using lists of elements and lists of pairs, respectively. However, we also
provide constructors which allow injection of fset and fmap values directly.
The linear order on values then ensures there is a canonical form. We also
show that our type-sort is countable which is a necessary requirement for its
use in Isabelle/UTP.
69