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