doc-src/Locales/Locales/Examples1.thy

tuned import order

(* $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