doc-src/IsarImplementation/Thy/Local_Theory.thy

+theory Local_Theory
+imports Base
+begin
+
+chapter {* Local theory specifications *}
+
+text {*
+  A \emph{local theory} combines aspects of both theory and proof
+  context (cf.\ \secref{sec:context}), such that definitional
+  specifications may be given relatively to parameters and
+  assumptions.  A local theory is represented as a regular proof
+  context, augmented by administrative data about the \emph{target
+  context}.
+
+  The target is usually derived from the background theory by adding
+  local @{text "\<FIX>"} and @{text "\<ASSUME>"} elements, plus
+  suitable modifications of non-logical context data (e.g.\ a special
+  type-checking discipline).  Once initialized, the target is ready to
+  absorb definitional primitives: @{text "\<DEFINE>"} for terms and
+  @{text "\<NOTE>"} for theorems.  Such definitions may get
+  transformed in a target-specific way, but the programming interface
+  hides such details.
+
+  Isabelle/Pure provides target mechanisms for locales, type-classes,
+  type-class instantiations, and general overloading.  In principle,
+  users can implement new targets as well, but this rather arcane
+  discipline is beyond the scope of this manual.  In contrast,
+  implementing derived definitional packages to be used within a local
+  theory context is quite easy: the interfaces are even simpler and
+  more abstract than the underlying primitives for raw theories.
+
+  Many definitional packages for local theories are available in
+  Isabelle.  Although a few old packages only work for global
+  theories, the local theory interface is already the standard way of
+  implementing definitional packages in Isabelle.
+*}
+
+
+section {* Definitional elements *}
+
+text {*
+  There are separate elements @{text "\<DEFINE> c \<equiv> t"} for terms, and
+  @{text "\<NOTE> b = thm"} for theorems.  Types are treated
+  implicitly, according to Hindley-Milner discipline (cf.\
+  \secref{sec:variables}).  These definitional primitives essentially
+  act like @{text "let"}-bindings within a local context that may
+  already contain earlier @{text "let"}-bindings and some initial
+  @{text "\<lambda>"}-bindings.  Thus we gain \emph{dependent definitions}
+  that are relative to an initial axiomatic context.  The following
+  diagram illustrates this idea of axiomatic elements versus
+  definitional elements:
+
+  \begin{center}
+  \begin{tabular}{|l|l|l|}
+  \hline
+  & @{text "\<lambda>"}-binding & @{text "let"}-binding \\
+  \hline
+  types & fixed @{text "\<alpha>"} & arbitrary @{text "\<beta>"} \\
+  terms & @{text "\<FIX> x :: \<tau>"} & @{text "\<DEFINE> c \<equiv> t"} \\
+  theorems & @{text "\<ASSUME> a: A"} & @{text "\<NOTE> b = \<^BG>B\<^EN>"} \\
+  \hline
+  \end{tabular}
+  \end{center}
+
+  A user package merely needs to produce suitable @{text "\<DEFINE>"}
+  and @{text "\<NOTE>"} elements according to the application.  For
+  example, a package for inductive definitions might first @{text
+  "\<DEFINE>"} a certain predicate as some fixed-point construction,
+  then @{text "\<NOTE>"} a proven result about monotonicity of the
+  functor involved here, and then produce further derived concepts via
+  additional @{text "\<DEFINE>"} and @{text "\<NOTE>"} elements.
+
+  The cumulative sequence of @{text "\<DEFINE>"} and @{text "\<NOTE>"}
+  produced at package runtime is managed by the local theory
+  infrastructure by means of an \emph{auxiliary context}.  Thus the
+  system holds up the impression of working within a fully abstract
+  situation with hypothetical entities: @{text "\<DEFINE> c \<equiv> t"}
+  always results in a literal fact @{text "\<^BG>c \<equiv> t\<^EN>"}, where
+  @{text "c"} is a fixed variable @{text "c"}.  The details about
+  global constants, name spaces etc. are handled internally.
+
+  So the general structure of a local theory is a sandwich of three
+  layers:
+
+  \begin{center}
+  \framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}}
+  \end{center}
+
+  \noindent When a definitional package is finished, the auxiliary
+  context is reset to the target context.  The target now holds
+  definitions for terms and theorems that stem from the hypothetical
+  @{text "\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by
+  the particular target policy (see
+  \cite[\S4--5]{Haftmann-Wenzel:2009} for details).
+*}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML_type local_theory: Proof.context} \\
+  @{index_ML TheoryTarget.init: "string option -> theory -> local_theory"} \\[1ex]
+  @{index_ML LocalTheory.define: "string ->
+    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+    (term * (string * thm)) * local_theory"} \\
+  @{index_ML LocalTheory.note: "string ->
+    Attrib.binding * thm list -> local_theory ->
+    (string * thm list) * local_theory"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML_type local_theory} represents local theories.  Although
+  this is merely an alias for @{ML_type Proof.context}, it is
+  semantically a subtype of the same: a @{ML_type local_theory} holds
+  target information as special context data.  Subtyping means that
+  any value @{text "lthy:"}~@{ML_type local_theory} can be also used
+  with operations on expecting a regular @{text "ctxt:"}~@{ML_type
+  Proof.context}.
+
+  \item @{ML TheoryTarget.init}~@{text "NONE thy"} initializes a
+  trivial local theory from the given background theory.
+  Alternatively, @{text "SOME name"} may be given to initialize a
+  @{command locale} or @{command class} context (a fully-qualified
+  internal name is expected here).  This is useful for experimentation
+  --- normally the Isar toplevel already takes care to initialize the
+  local theory context.
+
+  \item @{ML LocalTheory.define}~@{text "kind ((b, mx), (a, rhs))
+  lthy"} defines a local entity according to the specification that is
+  given relatively to the current @{text "lthy"} context.  In
+  particular the term of the RHS may refer to earlier local entities
+  from the auxiliary context, or hypothetical parameters from the
+  target context.  The result is the newly defined term (which is
+  always a fixed variable with exactly the same name as specified for
+  the LHS), together with an equational theorem that states the
+  definition as a hypothetical fact.
+
+  Unless an explicit name binding is given for the RHS, the resulting
+  fact will be called @{text "b_def"}.  Any given attributes are
+  applied to that same fact --- immediately in the auxiliary context
+  \emph{and} in any transformed versions stemming from target-specific
+  policies or any later interpretations of results from the target
+  context (think of @{command locale} and @{command interpretation},
+  for example).  This means that attributes should be usually plain
+  declarations such as @{attribute simp}, while non-trivial rules like
+  @{attribute simplified} are better avoided.
+
+  The @{text kind} determines the theorem kind tag of the resulting
+  fact.  Typical examples are @{ML Thm.definitionK}, @{ML
+  Thm.theoremK}, or @{ML Thm.internalK}.
+
+  \item @{ML LocalTheory.note}~@{text "kind (a, ths) lthy"} is
+  analogous to @{ML LocalTheory.define}, but defines facts instead of
+  terms.  There is also a slightly more general variant @{ML
+  LocalTheory.notes} that defines several facts (with attribute
+  expressions) simultaneously.
+
+  This is essentially the internal version of the @{command lemmas}
+  command, or @{command declare} if an empty name binding is given.
+
+  \end{description}
+*}
+
+
+section {* Morphisms and declarations *}
+
+text FIXME
+
+end