# HG changeset patch
# User wenzelm
# Date 1234907239 -3600
# Node ID b0b6d34388e9e6f46da04d0f1d6bb3d4a2a4fae8
# Parent  c0f2c8424848cc2a98403b511bd51263e09dde8d
some text on local theory specifications;

diff -r c0f2c8424848 -r b0b6d34388e9 doc-src/IsarImplementation/Thy/Local_Theory.thy
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Tue Feb 17 22:46:41 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Tue Feb 17 22:47:19 2009 +0100
@@ -4,10 +4,113 @@
 
 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 simpler and more
+  abstract than the underlying primitives for raw theories.
+
+  Many definitional packages for local theories are available in
+  Isabelle/Pure and Isabelle/HOL.  Even though a few old packages that
+  only work for global theories might still persists, the local theory
+  interface is already the standard way of implementing definitional
+  packages in Isabelle.
+*}
+
+
 section {* Definitional elements *}
 
 text {*
-  FIXME
+  There are separate definitional 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 some @{text "\<lambda>"}-bindings.  Thus we gain
+  \emph{dependent definitions}, relatively 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,
+  prove the monotonicity of the functor involved here and @{text
+  "\<NOTE>"} the result, 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 will be 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 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 LocalTheory.define}~@{text FIXME}
+
+  \item @{ML LocalTheory.note}~@{text FIXME}
+
+  \end{description}
 *}