(* $Id$ *)
theory Examples1
imports Examples
begin
section {* Use of Locales in Theories and Proofs *}
text {* Locales enable to prove theorems abstractly, relative to
sets of assumptions. These theorems can then be used in other
contexts where the assumptions themselves, or
instances of the assumptions, are theorems. This form of theorem
reuse is called \emph{interpretation}.
The changes of the locale
hierarchy from the previous sections are examples of
interpretations. The command \isakeyword{interpretation} $l_1
\subseteq l_2$ is said to \emph{interpret} locale $l_2$ in the
context of $l_1$. It causes all theorems of $l_2$ to be made
available in $l_1$. The interpretation is \emph{dynamic}: not only
theorems already present in $l_2$ are available in $l_1$. Theorems
that will be added to $l_2$ in future will automatically be
propagated to $l_1$.
Locales can also be interpreted in the contexts of theories and
structured proofs. These interpretations are dynamic, too.
Theorems added to locales will be propagated to theories.
In this section the interpretation in
theories is illustrated; interpretation in proofs is analogous.
As an example consider, the type of natural numbers @{typ nat}. The
order relation @{text \<le>} is a total order over @{typ nat},
divisibility @{text dvd} is a distributive lattice.
We start with the
interpretation that @{text \<le>} is a partial order. The facilities of
the interpretation command are explored in three versions.
*}
subsection {* First Version: Replacement of Parameters Only \label{sec:po-first} *}
text {*
In the most basic form, interpretation just replaces the locale
parameters by terms. The following command interprets the locale
@{text partial_order} in the global context of the theory. The
parameter @{term le} is replaced by @{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"}. *}
interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
txt {* The locale name is succeeded by a \emph{parameter
instantiation}. In general, this is a list of terms, which refer to
the parameters in the order of declaration in the locale. The
locale name is preceded by an optional \emph{interpretation prefix},
which is used to qualify names from the locale in the global
context.
The command creates the goal @{subgoals [display]} which can be shown
easily:%
\footnote{Note that @{text op} binds tighter than functions
application: parentheses around @{text "op \<le>"} are not necessary.}
*}
by unfold_locales auto
text {* Now theorems from the locale are available in the theory,
interpreted for natural numbers, for example @{thm [source]
nat.trans}: @{thm [display, indent=2] nat.trans}
In order to avoid unwanted hiding of theorems, interpretation
accepts a qualifier, @{text nat} in the example, which is applied to
all names processed by the
interpretation. If present the qualifier is mandatory --- that is,
the above theorem cannot be referred to simply as @{text trans}.
*}
subsection {* Second Version: Replacement of Definitions *}
text {* The above interpretation also creates the theorem
@{thm [source] nat.less_le_trans}: @{thm [display, indent=2]
nat.less_le_trans}
Here, @{term "partial_order.less (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"}
represents the strict order, although @{text "<"} is defined on
@{typ nat}. Interpretation enables to map concepts
introduced in locales through definitions to the corresponding
concepts of the theory.%
\footnote{This applies not only to \isakeyword{definition} but also to
\isakeyword{inductive}, \isakeyword{fun} and \isakeyword{function}.}
*}
end