author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 52422  93f3f9a2ae91 
permissions  rwrr 
29755  1 
theory Local_Theory 
2 
imports Base 

3 
begin 

18537  4 

34927
c4c02ac736a6
more details on long names, binding/naming, name space;
wenzelm
parents:
33834
diff
changeset

5 
chapter {* Local theory specifications \label{ch:localtheory} *} 
29759  6 

29764  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 nonlogical context data (e.g.\ a special 

18 
typechecking 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 targetspecific way, but the programming interface 

22 
hides such details. 

23 

24 
Isabelle/Pure provides target mechanisms for locales, typeclasses, 

25 
typeclass 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 

29765  29 
theory context is quite easy: the interfaces are even simpler and 
30 
more abstract than the underlying primitives for raw theories. 

29764  31 

32 
Many definitional packages for local theories are available in 

29765  33 
Isabelle. Although a few old packages only work for global 
39839  34 
theories, the standard way of implementing definitional packages in 
35 
Isabelle is via the local theory interface. 

29764  36 
*} 
37 

38 

29759  39 
section {* Definitional elements *} 
18537  40 

29759  41 
text {* 
29765  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 HindleyMilner discipline (cf.\ 

29764  45 
\secref{sec:variables}). These definitional primitives essentially 
46 
act like @{text "let"}bindings within a local context that may 

29765  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: 

29764  52 

53 
\begin{center} 

54 
\begin{tabular}{lll} 

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 fixedpoint construction, 

29765  69 
then @{text "\<NOTE>"} a proven result about monotonicity of the 
70 
functor involved here, and then produce further derived concepts via 

29764  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 

39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39849
diff
changeset

89 
When a definitional package is finished, the auxiliary context is 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39849
diff
changeset

90 
reset to the target context. The target now holds definitions for 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39849
diff
changeset

91 
terms and theorems that stem from the hypothetical @{text 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39849
diff
changeset

92 
"\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by the 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39849
diff
changeset

93 
particular target policy (see \cite[\S45]{HaftmannWenzel:2009} 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39849
diff
changeset

94 
for details). *} 
29764  95 

96 
text %mlref {* 

97 
\begin{mldecls} 

29765  98 
@{index_ML_type local_theory: Proof.context} \\ 
41621  99 
@{index_ML Named_Target.init: "(local_theory > local_theory) > 
100 
string > theory > local_theory"} \\[1ex] 

33834
7c06e19f717c
adapted local theory operations  eliminated odd kind;
wenzelm
parents:
33672
diff
changeset

101 
@{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) > 
7c06e19f717c
adapted local theory operations  eliminated odd kind;
wenzelm
parents:
33672
diff
changeset

102 
local_theory > (term * (string * thm)) * local_theory"} \\ 
33672  103 
@{index_ML Local_Theory.note: "Attrib.binding * thm list > 
104 
local_theory > (string * thm list) * local_theory"} \\ 

29764  105 
\end{mldecls} 
106 

107 
\begin{description} 

108 

39864  109 
\item Type @{ML_type local_theory} represents local theories. 
110 
Although this is merely an alias for @{ML_type Proof.context}, it is 

29765  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 

41621  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 
nonempty name refers to a @{command locale} or @{command class} 

121 
context (a fullyqualified 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. 

29764  126 

33834
7c06e19f717c
adapted local theory operations  eliminated odd kind;
wenzelm
parents:
33672
diff
changeset

127 
\item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs)) 
29765  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 

29766  131 
from the auxiliary context, or hypothetical parameters from the 
29765  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 

29766  140 
\emph{and} in any transformed versions stemming from targetspecific 
29765  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 nontrivial rules like 

145 
@{attribute simplified} are better avoided. 

146 

33672  147 
\item @{ML Local_Theory.note}~@{text "(a, ths) lthy"} is 
148 
analogous to @{ML Local_Theory.define}, but defines facts instead of 

29765  149 
terms. There is also a slightly more general variant @{ML 
33672  150 
Local_Theory.notes} that defines several facts (with attribute 
29765  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. 

29764  155 

156 
\end{description} 

29759  157 
*} 
18537  158 

20451  159 

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

52422  162 
text {* 
163 
%FIXME 

39877  164 

52422  165 
See also \cite{ChaiebWenzel:2007}. 
39877  166 
*} 
30272  167 

18537  168 
end 