summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

5 chapter {* Local theory specifications \label{ch:local-theory} *}

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}.

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.

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.

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 *}

39 section {* Definitional elements *}

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:

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}

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.

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.

82 So the general structure of a local theory is a sandwich of three

83 layers:

85 \begin{center}

86 \framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}}

87 \end{center}

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). *}

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}

107 \begin{description}

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}.

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.

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.

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.

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.

153 This is essentially the internal version of the @{command lemmas}

154 command, or @{command declare} if an empty name binding is given.

156 \end{description}

157 *}

160 section {* Morphisms and declarations \label{sec:morphisms} *}

162 text {* FIXME

164 \medskip See also \cite{Chaieb-Wenzel:2007}.

165 *}

167 end