equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 chapter \<open>Local theory specifications \label{ch:local-theory}\<close> |
5 chapter \<open>Local theory specifications \label{ch:local-theory}\<close> |
6 |
6 |
7 text \<open> |
7 text \<open> |
8 A \emph{local theory} combines aspects of both theory and proof |
8 A \<^emph>\<open>local theory\<close> combines aspects of both theory and proof |
9 context (cf.\ \secref{sec:context}), such that definitional |
9 context (cf.\ \secref{sec:context}), such that definitional |
10 specifications may be given relatively to parameters and |
10 specifications may be given relatively to parameters and |
11 assumptions. A local theory is represented as a regular proof |
11 assumptions. A local theory is represented as a regular proof |
12 context, augmented by administrative data about the \emph{target |
12 context, augmented by administrative data about the \<^emph>\<open>target |
13 context}. |
13 context\<close>. |
14 |
14 |
15 The target is usually derived from the background theory by adding |
15 The target is usually derived from the background theory by adding |
16 local @{text "\<FIX>"} and @{text "\<ASSUME>"} elements, plus |
16 local @{text "\<FIX>"} and @{text "\<ASSUME>"} elements, plus |
17 suitable modifications of non-logical context data (e.g.\ a special |
17 suitable modifications of non-logical context data (e.g.\ a special |
18 type-checking discipline). Once initialized, the target is ready to |
18 type-checking discipline). Once initialized, the target is ready to |
43 @{text "\<NOTE> b = thm"} for theorems. Types are treated |
43 @{text "\<NOTE> b = thm"} for theorems. Types are treated |
44 implicitly, according to Hindley-Milner discipline (cf.\ |
44 implicitly, according to Hindley-Milner discipline (cf.\ |
45 \secref{sec:variables}). These definitional primitives essentially |
45 \secref{sec:variables}). These definitional primitives essentially |
46 act like @{text "let"}-bindings within a local context that may |
46 act like @{text "let"}-bindings within a local context that may |
47 already contain earlier @{text "let"}-bindings and some initial |
47 already contain earlier @{text "let"}-bindings and some initial |
48 @{text "\<lambda>"}-bindings. Thus we gain \emph{dependent definitions} |
48 @{text "\<lambda>"}-bindings. Thus we gain \<^emph>\<open>dependent definitions\<close> |
49 that are relative to an initial axiomatic context. The following |
49 that are relative to an initial axiomatic context. The following |
50 diagram illustrates this idea of axiomatic elements versus |
50 diagram illustrates this idea of axiomatic elements versus |
51 definitional elements: |
51 definitional elements: |
52 |
52 |
53 \begin{center} |
53 \begin{center} |
70 functor involved here, and then produce further derived concepts via |
70 functor involved here, and then produce further derived concepts via |
71 additional @{text "\<DEFINE>"} and @{text "\<NOTE>"} elements. |
71 additional @{text "\<DEFINE>"} and @{text "\<NOTE>"} elements. |
72 |
72 |
73 The cumulative sequence of @{text "\<DEFINE>"} and @{text "\<NOTE>"} |
73 The cumulative sequence of @{text "\<DEFINE>"} and @{text "\<NOTE>"} |
74 produced at package runtime is managed by the local theory |
74 produced at package runtime is managed by the local theory |
75 infrastructure by means of an \emph{auxiliary context}. Thus the |
75 infrastructure by means of an \<^emph>\<open>auxiliary context\<close>. Thus the |
76 system holds up the impression of working within a fully abstract |
76 system holds up the impression of working within a fully abstract |
77 situation with hypothetical entities: @{text "\<DEFINE> c \<equiv> t"} |
77 situation with hypothetical entities: @{text "\<DEFINE> c \<equiv> t"} |
78 always results in a literal fact @{text "\<^BG>c \<equiv> t\<^EN>"}, where |
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 |
79 @{text "c"} is a fixed variable @{text "c"}. The details about |
80 global constants, name spaces etc. are handled internally. |
80 global constants, name spaces etc. are handled internally. |
111 with operations on expecting a regular @{text "ctxt:"}~@{ML_type |
111 with operations on expecting a regular @{text "ctxt:"}~@{ML_type |
112 Proof.context}. |
112 Proof.context}. |
113 |
113 |
114 \<^descr> @{ML Named_Target.init}~@{text "before_exit name thy"} |
114 \<^descr> @{ML Named_Target.init}~@{text "before_exit name thy"} |
115 initializes a local theory derived from the given background theory. |
115 initializes a local theory derived from the given background theory. |
116 An empty name refers to a \emph{global theory} context, and a |
116 An empty name refers to a \<^emph>\<open>global theory\<close> context, and a |
117 non-empty name refers to a @{command locale} or @{command class} |
117 non-empty name refers to a @{command locale} or @{command class} |
118 context (a fully-qualified internal name is expected here). This is |
118 context (a fully-qualified internal name is expected here). This is |
119 useful for experimentation --- normally the Isar toplevel already |
119 useful for experimentation --- normally the Isar toplevel already |
120 takes care to initialize the local theory context. |
120 takes care to initialize the local theory context. |
121 |
121 |
130 definition as a hypothetical fact. |
130 definition as a hypothetical fact. |
131 |
131 |
132 Unless an explicit name binding is given for the RHS, the resulting |
132 Unless an explicit name binding is given for the RHS, the resulting |
133 fact will be called @{text "b_def"}. Any given attributes are |
133 fact will be called @{text "b_def"}. Any given attributes are |
134 applied to that same fact --- immediately in the auxiliary context |
134 applied to that same fact --- immediately in the auxiliary context |
135 \emph{and} in any transformed versions stemming from target-specific |
135 \<^emph>\<open>and\<close> in any transformed versions stemming from target-specific |
136 policies or any later interpretations of results from the target |
136 policies or any later interpretations of results from the target |
137 context (think of @{command locale} and @{command interpretation}, |
137 context (think of @{command locale} and @{command interpretation}, |
138 for example). This means that attributes should be usually plain |
138 for example). This means that attributes should be usually plain |
139 declarations such as @{attribute simp}, while non-trivial rules like |
139 declarations such as @{attribute simp}, while non-trivial rules like |
140 @{attribute simplified} are better avoided. |
140 @{attribute simplified} are better avoided. |