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