Theory UML_Types
chapter‹Formalization I: OCL Types and Core Definitions \label{sec:focl-types}›
theory UML_Types
imports HOL.Transcendental
keywords "Assert" :: thy_decl
and "Assert_local" :: thy_decl
begin
section‹Preliminaries›
subsection‹Notations for the Option Type›
text‹
First of all, we will use a more compact notation for the library
option type which occur all over in our definitions and which will make
the presentation more like a textbook:
›
no_notation ceiling ("⌈_⌉")
no_notation floor ("⌊_⌋")
type_notation option ("⟨_⟩⇩⊥")
notation Some ("⌊(_)⌋")
notation None ("⊥")
text‹These commands introduce an alternative, more compact notation for the type constructor
@{typ "'α option"}, namely @{typ "⟨'α⟩⇩⊥"}. Furthermore, the constructors @{term "Some X"} and
@{term "None"} of the type @{typ "'α option"}, namely @{term "⌊X⌋"} and @{term "⊥"}.›
text‹
The following function (corresponding to @{term the} in the Isabelle/HOL library)
is defined as the inverse of the injection @{term Some}.
›
fun drop :: "'α option ⇒ 'α" ("⌈(_)⌉")
where drop_lift[simp]: "⌈⌊v⌋⌉ = v"
text‹The definitions for the constants and operations based on functions
will be geared towards a format that Isabelle can check to be a ``conservative''
(\ie, logically safe) axiomatic definition. By introducing an explicit
interpretation function (which happens to be defined just as the identity
since we are using a shallow embedding of OCL into HOL), all these definitions
can be rewritten into the conventional semantic textbook format.
To say it in other words: The interpretation function ‹Sem› as defined
below is just a textual marker for presentation purposes, i.e. intended for readers
used to conventional textbook notations on semantics. Since we use a ``shallow embedding'',
i.e. since we represent the syntax of OCL directly by HOL constants, the interpretation function
is semantically not only superfluous, but from an Isabelle perspective strictly in
the way for certain consistency checks performed by the definitional packages.
›
definition Sem :: "'a ⇒ 'a" ("I⟦_⟧")
where "I⟦x⟧ ≡ x"
subsection‹Common Infrastructure for all OCL Types \label{sec:focl-common-types}›
text ‹In order to have the possibility to nest collection types,
such that we can give semantics to expressions like ‹Set{Set{𝟮},null}›,
it is necessary to introduce a uniform interface for types having
the ‹invalid› (= bottom) element. The reason is that we impose
a data-invariant on raw-collection \inlineisar|types_code| which assures
that the ‹invalid› element is not allowed inside the collection;
all raw-collections of this form were identified with the ‹invalid› element
itself. The construction requires that the new collection type is
not comparable with the raw-types (consisting of nested option type constructions),
such that the data-invariant must be expressed in terms of the interface.
In a second step, our base-types will be shown to be instances of this interface.
›
text‹
This uniform interface consists in a type class requiring the existence
of a bot and a null element. The construction proceeds by
abstracting the null (defined by ‹⌊ ⊥ ⌋› on
‹'a option option›) to a ‹null› element, which may
have an arbitrary semantic structure, and an undefinedness element ‹⊥›
to an abstract undefinedness element ‹bot› (also written
‹⊥› whenever no confusion arises). As a consequence, it is necessary
to redefine the notions of invalid, defined, valuation etc.
on top of this interface.›
text‹
This interface consists in two abstract type classes ‹bot›
and ‹null› for the class of all types comprising a bot and a
distinct null element.›
class bot =
fixes bot :: "'a"
assumes nonEmpty : "∃ x. x ≠ bot"
class null = bot +
fixes null :: "'a"
assumes null_is_valid : "null ≠ bot"
subsection‹Accommodation of Basic Types to the Abstract Interface›
text‹
In the following it is shown that the ``option-option'' type is
in fact in the ‹null› class and that function spaces over these
classes again ``live'' in these classes. This motivates the default construction
of the semantic domain for the basic types (\inlineocl{Boolean},
\inlineocl{Integer}, \inlineocl{Real}, \ldots).
›
instantiation option :: (type)bot
begin
definition bot_option_def: "(bot::'a option) ≡ (None::'a option)"
instance proof show "∃x::'a option. x ≠ bot"
by(rule_tac x="Some x" in exI, simp add:bot_option_def)
qed
end
instantiation option :: (bot)null
begin
definition null_option_def: "(null::'a::bot option) ≡ ⌊ bot ⌋"
instance proof show "(null::'a::bot option) ≠ bot"
by( simp add : null_option_def bot_option_def)
qed
end
instantiation "fun" :: (type,bot) bot
begin
definition bot_fun_def: "bot ≡ (λ x. bot)"
instance proof show "∃(x::'a ⇒ 'b). x ≠ bot"
apply(rule_tac x="λ _. (SOME y. y ≠ bot)" in exI, auto)
apply(drule_tac x=x in fun_cong,auto simp:bot_fun_def)
apply(erule contrapos_pp, simp)
apply(rule some_eq_ex[THEN iffD2])
apply(simp add: nonEmpty)
done
qed
end
instantiation "fun" :: (type,null) null
begin
definition null_fun_def: "(null::'a ⇒ 'b::null) ≡ (λ x. null)"
instance proof
show "(null::'a ⇒ 'b::null) ≠ bot"
apply(auto simp: null_fun_def bot_fun_def)
apply(drule_tac x=x in fun_cong)
apply(erule contrapos_pp, simp add: null_is_valid)
done
qed
end
text‹A trivial consequence of this adaption of the interface is that
abstract and concrete versions of null are the same on base types
(as could be expected).›
subsection‹The Common Infrastructure of Object Types (Class Types) and States.›
text‹Recall that OCL is a textual extension of the UML; in particular, we use OCL as means to
annotate UML class models. Thus, OCL inherits a notion of \emph{data} in the UML: UML class
models provide classes, inheritance, types of objects, and subtypes connecting them along
the inheritance hierarchie.
›
text‹For the moment, we formalize the most common notions of objects, in particular
the existance of object-identifiers (oid) for each object under which it can
be referenced in a \emph{state}.›
type_synonym oid = nat
text‹We refrained from the alternative:
\begin{isar}[mathescape]
$\text{\textbf{type-synonym}}$ $\mathit{oid = ind}$
\end{isar}
which is slightly more abstract but non-executable.
›
text‹\emph{States} in UML/OCL are a pair of
\begin{itemize}
\item a partial map from oid's to elements of an \emph{object universe},
\ie{} the set of all possible object representations.
\item and an oid-indexed family of \emph{associations}, \ie{} finite relations between
objects living in a state. These relations can be n-ary which we model by nested lists.
\end{itemize}
For the moment we do not have to describe the concrete structure of the object universe and denote
it by the polymorphic variable ‹'𝔄›.›
record ('𝔄)state =
heap :: "oid ⇀ '𝔄 "
assocs :: "oid ⇀ ((oid list) list) list"
text‹In general, OCL operations are functions implicitly depending on a pair
of pre- and post-state, \ie{} \emph{state transitions}. Since this will be reflected in our
representation of OCL Types within HOL, we need to introduce the foundational concept of an
object id (oid), which is just some infinite set, and some abstract notion of state.›
type_synonym ('𝔄)st = "'𝔄 state × '𝔄 state"
text‹We will require for all objects that there is a function that
projects the oid of an object in the state (we will settle the question how to define
this function later). We will use the Isabelle type class mechanism~\<^cite>‹"haftmann.ea:constructive:2006"›
to capture this:›
class object = fixes oid_of :: "'a ⇒ oid"
text‹Thus, if needed, we can constrain the object universe to objects by adding
the following type class constraint:›
typ "'𝔄 :: object"
text‹The major instance needed are instances constructed over options: once an object,
options of objects are also objects.›
instantiation option :: (object)object
begin
definition oid_of_option_def: "oid_of x = oid_of (the x)"
instance ..
end
subsection‹Common Infrastructure for all OCL Types (II): Valuations as OCL Types›
text‹Since OCL operations in general depend on pre- and post-states, we will
represent OCL types as \emph{functions} from pre- and post-state to some
HOL raw-type that contains exactly the data in the OCL type --- see below.
This gives rise to the idea that we represent OCL types by \emph{Valuations}.
›
text‹Valuations are functions from a state pair (built upon
data universe @{typ "'𝔄"}) to an arbitrary null-type (\ie, containing
at least a destinguished ‹null› and ‹invalid› element).›
type_synonym ('𝔄,'α) val = "'𝔄 st ⇒ 'α::null"
text‹The definitions for the constants and operations based on valuations
will be geared towards a format that Isabelle can check to be a ``conservative''
(\ie, logically safe) axiomatic definition. By introducing an explicit
interpretation function (which happens to be defined just as the identity
since we are using a shallow embedding of OCL into HOL), all these definitions
can be rewritten into the conventional semantic textbook format as follows:›
subsection‹The fundamental constants 'invalid' and 'null' in all OCL Types›
text‹As a consequence of semantic domain definition, any OCL type will
have the two semantic constants ‹invalid› (for exceptional, aborted
computation) and ‹null›:
›
definition invalid :: "('𝔄,'α::bot) val"
where "invalid ≡ λ τ. bot"
text‹This conservative Isabelle definition of the polymorphic constant
@{const invalid} is equivalent with the textbook definition:›
lemma textbook_invalid: "I⟦invalid⟧τ = bot"
by(simp add: invalid_def Sem_def)
text ‹Note that the definition :
{\small
\begin{isar}[mathescape]
definition null :: "('$\mathfrak{A}$,'α::null) val"
where "null ≡ λ τ. null"
\end{isar}
} is not necessary since we defined the entire function space over null types
again as null-types; the crucial definition is @{thm "null_fun_def"}.
Thus, the polymorphic constant @{const null} is simply the result of
a general type class construction. Nevertheless, we can derive the
semantic textbook definition for the OCL null constant based on the
abstract null:
›
lemma textbook_null_fun: "I⟦null::('𝔄,'α::null) val⟧ τ = (null::('α::null))"
by(simp add: null_fun_def Sem_def)
section‹Basic OCL Value Types›
text ‹The structure of this section roughly follows the structure of Chapter
11 of the OCL standard~\<^cite>‹"omg:ocl:2012"›, which introduces the OCL
Library.›
text‹The semantic domain of the (basic) boolean type is now defined as the Standard:
the space of valuation to @{typ "bool option option"}, \ie{} the Boolean base type:›
type_synonym Boolean⇩b⇩a⇩s⇩e = "bool option option"
type_synonym ('𝔄)Boolean = "('𝔄,Boolean⇩b⇩a⇩s⇩e) val"
text‹Because of the previous class definitions, Isabelle type-inference establishes that
@{typ "('𝔄)Boolean"} lives actually both in the type class @{term bot} and @{term null};
this type is sufficiently rich to contain at least these two elements.
Analogously we build:›
type_synonym Integer⇩b⇩a⇩s⇩e = "int option option"
type_synonym ('𝔄)Integer = "('𝔄,Integer⇩b⇩a⇩s⇩e) val"
type_synonym String⇩b⇩a⇩s⇩e = "string option option"
type_synonym ('𝔄)String = "('𝔄,String⇩b⇩a⇩s⇩e) val"
type_synonym Real⇩b⇩a⇩s⇩e = "real option option"
type_synonym ('𝔄)Real = "('𝔄,Real⇩b⇩a⇩s⇩e) val"
text‹Since @{term "Real"} is again a basic type, we define its semantic domain
as the valuations over ‹real option option› --- i.e. the mathematical type of real numbers.
The HOL-theory for ‹real› ``Real'' transcendental numbers such as $\pi$ and $e$ as well as
infrastructure to reason over infinite convergent Cauchy-sequences (it is thus possible, in principle,
to reason in Featherweight OCL that the sum of inverted two-s exponentials is actually 2.
If needed, a code-generator to compile ‹Real› to floating-point
numbers can be added; this allows for mapping reals to an efficient machine representation;
of course, this feature would be logically unsafe.›
text‹For technical reasons related to the Isabelle type inference for type-classes
(we don't get the properties in the right order that class instantiation provides them,
if we would follow the previous scheme), we give a slightly atypic definition:›
typedef Void⇩b⇩a⇩s⇩e = "{X::unit option option. X = bot ∨ X = null }" by(rule_tac x="bot" in exI, simp)
type_synonym ('𝔄)Void = "('𝔄,Void⇩b⇩a⇩s⇩e) val"
section‹Some OCL Collection Types›
text‹For the semantic construction of the collection types, we have two goals:
\begin{enumerate}
\item we want the types to be \emph{fully abstract}, \ie, the type should not
contain junk-elements that are not representable by OCL expressions, and
\item we want a possibility to nest collection types (so, we want the
potential of talking about ‹Set(Set(Sequences(Pairs(X,Y))))›).
\end{enumerate}
The former principle rules out the option to define ‹'α Set› just by
‹('𝔄, ('α option option) set) val›. This would allow sets to contain
junk elements such as ‹{⊥}› which we need to identify with undefinedness
itself. Abandoning fully abstractness of rules would later on produce all sorts
of problems when quantifying over the elements of a type.
However, if we build an own type, then it must conform to our abstract interface
in order to have nested types: arguments of type-constructors must conform to our
abstract interface, and the result type too.
›
subsection‹The Construction of the Pair Type (Tuples)›
text‹The core of an own type construction is done via a type
definition which provides the base-type ‹('α, 'β) Pair⇩b⇩a⇩s⇩e›. It
is shown that this type ``fits'' indeed into the abstract type
interface discussed in the previous section.›
typedef (overloaded) ('α, 'β) Pair⇩b⇩a⇩s⇩e = "{X::('α::null × 'β::null) option option.
X = bot ∨ X = null ∨ (fst⌈⌈X⌉⌉ ≠ bot ∧ snd⌈⌈X⌉⌉ ≠ bot)}"
by (rule_tac x="bot" in exI, simp)
text‹We ``carve'' out from the concrete type @{typ "('α::null × 'β::null) option option"}
the new fully abstract type, which will not contain representations like @{term "⌊⌊(⊥,a)⌋⌋"}
or @{term "⌊⌊(b,⊥)⌋⌋"}. The type constuctor ‹Pair{x,y}› to be defined later will
identify these with @{term "invalid"}.
›
instantiation Pair⇩b⇩a⇩s⇩e :: (null,null)bot
begin
definition bot_Pair⇩b⇩a⇩s⇩e_def: "(bot_class.bot :: ('a::null,'b::null) Pair⇩b⇩a⇩s⇩e) ≡ Abs_Pair⇩b⇩a⇩s⇩e None"
instance proof show "∃x::('a,'b) Pair⇩b⇩a⇩s⇩e. x ≠ bot"
apply(rule_tac x="Abs_Pair⇩b⇩a⇩s⇩e ⌊None⌋" in exI)
by(simp add: bot_Pair⇩b⇩a⇩s⇩e_def Abs_Pair⇩b⇩a⇩s⇩e_inject null_option_def bot_option_def)
qed
end
instantiation Pair⇩b⇩a⇩s⇩e :: (null,null)null
begin
definition null_Pair⇩b⇩a⇩s⇩e_def: "(null::('a::null,'b::null) Pair⇩b⇩a⇩s⇩e) ≡ Abs_Pair⇩b⇩a⇩s⇩e ⌊ None ⌋"
instance proof show "(null::('a::null,'b::null) Pair⇩b⇩a⇩s⇩e) ≠ bot"
by(simp add: bot_Pair⇩b⇩a⇩s⇩e_def null_Pair⇩b⇩a⇩s⇩e_def Abs_Pair⇩b⇩a⇩s⇩e_inject
null_option_def bot_option_def)
qed
end
text‹... and lifting this type to the format of a valuation gives us:›
type_synonym ('𝔄,'α,'β) Pair = "('𝔄, ('α,'β) Pair⇩b⇩a⇩s⇩e) val"
type_notation Pair⇩b⇩a⇩s⇩e ("Pair'(_,_')")
subsection‹The Construction of the Set Type›
text‹The core of an own type construction is done via a type
definition which provides the raw-type ‹'α Set⇩b⇩a⇩s⇩e›. It
is shown that this type ``fits'' indeed into the abstract type
interface discussed in the previous section. Note that we make
no restriction whatsoever to \emph{finite} sets; while with
the standards type-constructors only finite sets can be denoted,
there is the possibility to define in fact infinite
type constructors in \FOCL (c.f. \autoref{sec:type-extensions}).›
typedef (overloaded) 'α Set⇩b⇩a⇩s⇩e ="{X::('α::null) set option option. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
by (rule_tac x="bot" in exI, simp)
instantiation Set⇩b⇩a⇩s⇩e :: (null)bot
begin
definition bot_Set⇩b⇩a⇩s⇩e_def: "(bot::('a::null) Set⇩b⇩a⇩s⇩e) ≡ Abs_Set⇩b⇩a⇩s⇩e None"
instance proof show "∃x::'a Set⇩b⇩a⇩s⇩e. x ≠ bot"
apply(rule_tac x="Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋" in exI)
by(simp add: bot_Set⇩b⇩a⇩s⇩e_def Abs_Set⇩b⇩a⇩s⇩e_inject null_option_def bot_option_def)
qed
end
instantiation Set⇩b⇩a⇩s⇩e :: (null)null
begin
definition null_Set⇩b⇩a⇩s⇩e_def: "(null::('a::null) Set⇩b⇩a⇩s⇩e) ≡ Abs_Set⇩b⇩a⇩s⇩e ⌊ None ⌋"
instance proof show "(null::('a::null) Set⇩b⇩a⇩s⇩e) ≠ bot"
by(simp add:null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def Abs_Set⇩b⇩a⇩s⇩e_inject
null_option_def bot_option_def)
qed
end
text‹... and lifting this type to the format of a valuation gives us:›
type_synonym ('𝔄,'α) Set = "('𝔄, 'α Set⇩b⇩a⇩s⇩e) val"
type_notation Set⇩b⇩a⇩s⇩e ("Set'(_')")
subsection‹The Construction of the Bag Type›
text‹The core of an own type construction is done via a type
definition which provides the raw-type ‹'α Bag⇩b⇩a⇩s⇩e›
based on multi-sets from the \HOL library. As in Sets, it
is shown that this type ``fits'' indeed into the abstract type
interface discussed in the previous section, and as in sets, we make
no restriction whatsoever to \emph{finite} multi-sets; while with
the standards type-constructors only finite sets can be denoted,
there is the possibility to define in fact infinite
type constructors in \FOCL (c.f. \autoref{sec:type-extensions}).
However, while several ‹null› elements are possible in a Bag, there
can't be no bottom (invalid) element in them.
›
typedef (overloaded) 'α Bag⇩b⇩a⇩s⇩e ="{X::('α::null ⇒ nat) option option. X = bot ∨ X = null ∨ ⌈⌈X⌉⌉ bot = 0 }"
by (rule_tac x="bot" in exI, simp)
instantiation Bag⇩b⇩a⇩s⇩e :: (null)bot
begin
definition bot_Bag⇩b⇩a⇩s⇩e_def: "(bot::('a::null) Bag⇩b⇩a⇩s⇩e) ≡ Abs_Bag⇩b⇩a⇩s⇩e None"
instance proof show "∃x::'a Bag⇩b⇩a⇩s⇩e. x ≠ bot"
apply(rule_tac x="Abs_Bag⇩b⇩a⇩s⇩e ⌊None⌋" in exI)
by(simp add: bot_Bag⇩b⇩a⇩s⇩e_def Abs_Bag⇩b⇩a⇩s⇩e_inject
null_option_def bot_option_def)
qed
end
instantiation Bag⇩b⇩a⇩s⇩e :: (null)null
begin
definition null_Bag⇩b⇩a⇩s⇩e_def: "(null::('a::null) Bag⇩b⇩a⇩s⇩e) ≡ Abs_Bag⇩b⇩a⇩s⇩e ⌊ None ⌋"
instance proof show "(null::('a::null) Bag⇩b⇩a⇩s⇩e) ≠ bot"
by(simp add:null_Bag⇩b⇩a⇩s⇩e_def bot_Bag⇩b⇩a⇩s⇩e_def Abs_Bag⇩b⇩a⇩s⇩e_inject
null_option_def bot_option_def)
qed
end
text‹... and lifting this type to the format of a valuation gives us:›
type_synonym ('𝔄,'α) Bag = "('𝔄, 'α Bag⇩b⇩a⇩s⇩e) val"
type_notation Bag⇩b⇩a⇩s⇩e ("Bag'(_')")
subsection‹The Construction of the Sequence Type›
text‹The core of an own type construction is done via a type
definition which provides the base-type ‹'α Sequence⇩b⇩a⇩s⇩e›. It
is shown that this type ``fits'' indeed into the abstract type
interface discussed in the previous section.›
typedef (overloaded) 'α Sequence⇩b⇩a⇩s⇩e ="{X::('α::null) list option option.
X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ bot)}"
by (rule_tac x="bot" in exI, simp)
instantiation Sequence⇩b⇩a⇩s⇩e :: (null)bot
begin
definition bot_Sequence⇩b⇩a⇩s⇩e_def: "(bot::('a::null) Sequence⇩b⇩a⇩s⇩e) ≡ Abs_Sequence⇩b⇩a⇩s⇩e None"
instance proof show "∃x::'a Sequence⇩b⇩a⇩s⇩e. x ≠ bot"
apply(rule_tac x="Abs_Sequence⇩b⇩a⇩s⇩e ⌊None⌋" in exI)
by(auto simp:bot_Sequence⇩b⇩a⇩s⇩e_def Abs_Sequence⇩b⇩a⇩s⇩e_inject
null_option_def bot_option_def)
qed
end
instantiation Sequence⇩b⇩a⇩s⇩e :: (null)null
begin
definition null_Sequence⇩b⇩a⇩s⇩e_def: "(null::('a::null) Sequence⇩b⇩a⇩s⇩e) ≡ Abs_Sequence⇩b⇩a⇩s⇩e ⌊ None ⌋"
instance proof show "(null::('a::null) Sequence⇩b⇩a⇩s⇩e) ≠ bot"
by(auto simp:bot_Sequence⇩b⇩a⇩s⇩e_def null_Sequence⇩b⇩a⇩s⇩e_def Abs_Sequence⇩b⇩a⇩s⇩e_inject
null_option_def bot_option_def)
qed
end
text‹... and lifting this type to the format of a valuation gives us:›
type_synonym ('𝔄,'α) Sequence = "('𝔄, 'α Sequence⇩b⇩a⇩s⇩e) val"
type_notation Sequence⇩b⇩a⇩s⇩e ("Sequence'(_')")
subsection‹Discussion: The Representation of UML/OCL Types in Featherweight OCL›
text‹In the introduction, we mentioned that there is an ``injective representation
mapping'' between the types of OCL and the types of Featherweight OCL (and its
meta-language: HOL). This injectivity is at the heart of our representation technique
--- a so-called \emph{shallow embedding} --- and means: OCL types were mapped one-to-one
to types in HOL, ruling out a resentation where
everything is mapped on some common HOL-type, say ``OCL-expression'', in which we
would have to sort out the typing of OCL and its impact on the semantic representation
function in an own, quite heavy side-calculus.
›
text‹After the previous sections, we are now able to exemplify this representation as follows:
\begin{table}[htbp]
\centering
\begin{tabu}{lX[,c,]}
\toprule
OCL Type & HOL Type \\
\midrule
\inlineocl|Boolean| & @{typ "('𝔄)Boolean"} \\
\inlineocl|Boolean -> Boolean| & @{typ "('𝔄)Boolean ⇒ ('𝔄)Boolean"} \\
\inlineocl|(Integer,Integer) -> Boolean| & @{typ "('𝔄)Integer ⇒ ('𝔄)Integer ⇒ ('𝔄)Boolean"} \\
\inlineocl|Set(Integer)| & @{typ "('𝔄,Integer⇩b⇩a⇩s⇩e)Set"} \\
\inlineocl|Set(Integer)-> Real| & @{typ "('𝔄,Integer⇩b⇩a⇩s⇩e)Set ⇒ ('𝔄)Real"} \\
\inlineocl|Set(Pair(Integer,Boolean))| & @{typ "('𝔄,(Integer⇩b⇩a⇩s⇩e, Boolean⇩b⇩a⇩s⇩e)Pair⇩b⇩a⇩s⇩e)Set"} \\
\inlineocl|Set(<T>)| & @{typ "('𝔄,'α::null)Set"} \\
\bottomrule
\end{tabu}
\caption{Correspondance between \OCL types and \HOL types}
\label{tab:types}
\end{table}
We do not formalize the representation map here; however, its principles are quite straight-forward:
\begin{enumerate}
\item cartesion products of arguments were curried,
\item constants of type \inlineocl{T} were mapped to valuations over the
HOL-type for \inlineocl{T},
\item functions \inlineocl{T -> T'} were mapped to functions in HOL, where
\inlineocl{T} and \inlineocl{T'} were mapped to the valuations for them, and
\item the arguments of type constructors \inlineocl{Set(T)} remain corresponding HOL base-types.
\end{enumerate}
›
text‹Note, furthermore, that our construction of ``fully abstract types'' (no junk, no confusion)
assures that the logical equality to be defined in the next section works correctly and comes
as element of the ``lingua franca'', \ie{} HOL.›
section‹Miscelleaneous: ML assertions›
text‹We introduce here a new command \emph{Assert} similar as \emph{value} for proving
that the given term in argument is a true proposition. The difference with \emph{value} is that
\emph{Assert} fails if the normal form of the term evaluated is not equal to @{term True}.
Moreover, in case \emph{value} could not normalize the given term, as another strategy of reduction
we try to prove it with a single ``simp'' tactic.›
ML‹
fun disp_msg title msg status = title ^ ": '" ^ msg ^ "' " ^ status
fun lemma msg specification_theorem concl in_local thy =
SOME
(in_local (fn lthy =>
specification_theorem Thm.theoremK NONE (K I) Binding.empty_atts [] []
(Element.Shows [(Binding.empty_atts, [(concl lthy, [])])])
false lthy
|> Proof.global_terminal_proof
((Method.Combinator ( Method.no_combinator_info
, Method.Then
, [Method.Basic (fn ctxt => SIMPLE_METHOD (asm_full_simp_tac ctxt 1))]),
(Position.none, Position.none)), NONE))
thy)
handle ERROR s =>
(warning s; writeln (disp_msg "KO" msg "failed to normalize"); NONE)
fun outer_syntax_command command_spec theory in_local =
Outer_Syntax.command command_spec "assert that the given specification is true"
(Parse.term >> (fn elems_concl => theory (fn thy =>
case
lemma "nbe" (Specification.theorem true)
(fn lthy =>
let val expr = Nbe.dynamic_value lthy (Syntax.read_term lthy elems_concl)
val thy = Proof_Context.theory_of lthy
open HOLogic in
if Sign.typ_equiv thy (fastype_of expr, @{typ "prop"}) then
expr
else mk_Trueprop (mk_eq (@{term "True"}, expr))
end)
in_local
thy
of NONE =>
let val attr_simp = "simp" in
case lemma attr_simp (Specification.theorem_cmd true) (K elems_concl) in_local thy of
NONE => raise (ERROR "Assertion failed")
| SOME thy =>
(writeln (disp_msg "OK" "simp" "finished the normalization");
thy)
end
| SOME thy => thy)))
val () = outer_syntax_command @{command_keyword Assert} Toplevel.theory Named_Target.theory_map
val () = outer_syntax_command @{command_keyword Assert_local} (Toplevel.local_theory NONE NONE) I
›
end