doc-src/IsarImplementation/Thy/Local_Theory.thy
author wenzelm
Fri Aug 12 22:10:49 2011 +0200 (2011-08-12)
changeset 44163 32e0c150c010
parent 41621 55b16bd82142
permissions -rw-r--r--
normalized theory dependencies wrt. file_store;
     1 theory Local_Theory
     2 imports Base
     3 begin
     4 
     5 chapter {* Local theory specifications \label{ch:local-theory} *}
     6 
     7 text {*
     8   A \emph{local theory} combines aspects of both theory and proof
     9   context (cf.\ \secref{sec:context}), such that definitional
    10   specifications may be given relatively to parameters and
    11   assumptions.  A local theory is represented as a regular proof
    12   context, augmented by administrative data about the \emph{target
    13   context}.
    14 
    15   The target is usually derived from the background theory by adding
    16   local @{text "\<FIX>"} and @{text "\<ASSUME>"} elements, plus
    17   suitable modifications of non-logical context data (e.g.\ a special
    18   type-checking discipline).  Once initialized, the target is ready to
    19   absorb definitional primitives: @{text "\<DEFINE>"} for terms and
    20   @{text "\<NOTE>"} for theorems.  Such definitions may get
    21   transformed in a target-specific way, but the programming interface
    22   hides such details.
    23 
    24   Isabelle/Pure provides target mechanisms for locales, type-classes,
    25   type-class instantiations, and general overloading.  In principle,
    26   users can implement new targets as well, but this rather arcane
    27   discipline is beyond the scope of this manual.  In contrast,
    28   implementing derived definitional packages to be used within a local
    29   theory context is quite easy: the interfaces are even simpler and
    30   more abstract than the underlying primitives for raw theories.
    31 
    32   Many definitional packages for local theories are available in
    33   Isabelle.  Although a few old packages only work for global
    34   theories, the standard way of implementing definitional packages in
    35   Isabelle is via the local theory interface.
    36 *}
    37 
    38 
    39 section {* Definitional elements *}
    40 
    41 text {*
    42   There are separate elements @{text "\<DEFINE> c \<equiv> t"} for terms, and
    43   @{text "\<NOTE> b = thm"} for theorems.  Types are treated
    44   implicitly, according to Hindley-Milner discipline (cf.\
    45   \secref{sec:variables}).  These definitional primitives essentially
    46   act like @{text "let"}-bindings within a local context that may
    47   already contain earlier @{text "let"}-bindings and some initial
    48   @{text "\<lambda>"}-bindings.  Thus we gain \emph{dependent definitions}
    49   that are relative to an initial axiomatic context.  The following
    50   diagram illustrates this idea of axiomatic elements versus
    51   definitional elements:
    52 
    53   \begin{center}
    54   \begin{tabular}{|l|l|l|}
    55   \hline
    56   & @{text "\<lambda>"}-binding & @{text "let"}-binding \\
    57   \hline
    58   types & fixed @{text "\<alpha>"} & arbitrary @{text "\<beta>"} \\
    59   terms & @{text "\<FIX> x :: \<tau>"} & @{text "\<DEFINE> c \<equiv> t"} \\
    60   theorems & @{text "\<ASSUME> a: A"} & @{text "\<NOTE> b = \<^BG>B\<^EN>"} \\
    61   \hline
    62   \end{tabular}
    63   \end{center}
    64 
    65   A user package merely needs to produce suitable @{text "\<DEFINE>"}
    66   and @{text "\<NOTE>"} elements according to the application.  For
    67   example, a package for inductive definitions might first @{text
    68   "\<DEFINE>"} a certain predicate as some fixed-point construction,
    69   then @{text "\<NOTE>"} a proven result about monotonicity of the
    70   functor involved here, and then produce further derived concepts via
    71   additional @{text "\<DEFINE>"} and @{text "\<NOTE>"} elements.
    72 
    73   The cumulative sequence of @{text "\<DEFINE>"} and @{text "\<NOTE>"}
    74   produced at package runtime is managed by the local theory
    75   infrastructure by means of an \emph{auxiliary context}.  Thus the
    76   system holds up the impression of working within a fully abstract
    77   situation with hypothetical entities: @{text "\<DEFINE> c \<equiv> t"}
    78   always results in a literal fact @{text "\<^BG>c \<equiv> t\<^EN>"}, where
    79   @{text "c"} is a fixed variable @{text "c"}.  The details about
    80   global constants, name spaces etc. are handled internally.
    81 
    82   So the general structure of a local theory is a sandwich of three
    83   layers:
    84 
    85   \begin{center}
    86   \framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}}
    87   \end{center}
    88 
    89   When a definitional package is finished, the auxiliary context is
    90   reset to the target context.  The target now holds definitions for
    91   terms and theorems that stem from the hypothetical @{text
    92   "\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by the
    93   particular target policy (see \cite[\S4--5]{Haftmann-Wenzel:2009}
    94   for details).  *}
    95 
    96 text %mlref {*
    97   \begin{mldecls}
    98   @{index_ML_type local_theory: Proof.context} \\
    99   @{index_ML Named_Target.init: "(local_theory -> local_theory) ->
   100     string -> theory -> local_theory"} \\[1ex]
   101   @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
   102     local_theory -> (term * (string * thm)) * local_theory"} \\
   103   @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
   104     local_theory -> (string * thm list) * local_theory"} \\
   105   \end{mldecls}
   106 
   107   \begin{description}
   108 
   109   \item Type @{ML_type local_theory} represents local theories.
   110   Although this is merely an alias for @{ML_type Proof.context}, it is
   111   semantically a subtype of the same: a @{ML_type local_theory} holds
   112   target information as special context data.  Subtyping means that
   113   any value @{text "lthy:"}~@{ML_type local_theory} can be also used
   114   with operations on expecting a regular @{text "ctxt:"}~@{ML_type
   115   Proof.context}.
   116 
   117   \item @{ML Named_Target.init}~@{text "before_exit name thy"}
   118   initializes a local theory derived from the given background theory.
   119   An empty name refers to a \emph{global theory} context, and a
   120   non-empty name refers to a @{command locale} or @{command class}
   121   context (a fully-qualified internal name is expected here).  This is
   122   useful for experimentation --- normally the Isar toplevel already
   123   takes care to initialize the local theory context.  The given @{text
   124   "before_exit"} function is invoked before leaving the context; in
   125   most situations plain identity @{ML I} is sufficient.
   126 
   127   \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
   128   lthy"} defines a local entity according to the specification that is
   129   given relatively to the current @{text "lthy"} context.  In
   130   particular the term of the RHS may refer to earlier local entities
   131   from the auxiliary context, or hypothetical parameters from the
   132   target context.  The result is the newly defined term (which is
   133   always a fixed variable with exactly the same name as specified for
   134   the LHS), together with an equational theorem that states the
   135   definition as a hypothetical fact.
   136 
   137   Unless an explicit name binding is given for the RHS, the resulting
   138   fact will be called @{text "b_def"}.  Any given attributes are
   139   applied to that same fact --- immediately in the auxiliary context
   140   \emph{and} in any transformed versions stemming from target-specific
   141   policies or any later interpretations of results from the target
   142   context (think of @{command locale} and @{command interpretation},
   143   for example).  This means that attributes should be usually plain
   144   declarations such as @{attribute simp}, while non-trivial rules like
   145   @{attribute simplified} are better avoided.
   146 
   147   \item @{ML Local_Theory.note}~@{text "(a, ths) lthy"} is
   148   analogous to @{ML Local_Theory.define}, but defines facts instead of
   149   terms.  There is also a slightly more general variant @{ML
   150   Local_Theory.notes} that defines several facts (with attribute
   151   expressions) simultaneously.
   152 
   153   This is essentially the internal version of the @{command lemmas}
   154   command, or @{command declare} if an empty name binding is given.
   155 
   156   \end{description}
   157 *}
   158 
   159 
   160 section {* Morphisms and declarations \label{sec:morphisms} *}
   161 
   162 text {* FIXME
   163 
   164   \medskip See also \cite{Chaieb-Wenzel:2007}.
   165 *}
   166 
   167 end