72 |
72 |
73 |
73 |
74 subsection {* Theory context \label{sec:context-theory} *} |
74 subsection {* Theory context \label{sec:context-theory} *} |
75 |
75 |
76 text {* |
76 text {* |
77 A \emph{theory} is a data container with explicit named and unique |
77 A \emph{theory} is a data container with explicit name and unique |
78 identifier. Theories are related by a (nominal) sub-theory |
78 identifier. Theories are related by a (nominal) sub-theory |
79 relation, which corresponds to the dependency graph of the original |
79 relation, which corresponds to the dependency graph of the original |
80 construction; each theory is derived from a certain sub-graph of |
80 construction; each theory is derived from a certain sub-graph of |
81 ancestor theories. |
81 ancestor theories. |
82 |
82 |
176 stepping stone in the linear development of @{text "thy"}. The next |
176 stepping stone in the linear development of @{text "thy"}. The next |
177 update will result in two related, valid theories. |
177 update will result in two related, valid theories. |
178 |
178 |
179 \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text |
179 \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text |
180 "thy"} that holds a copy of the same data. The result is not |
180 "thy"} that holds a copy of the same data. The result is not |
181 related to the original; the original is unchanched. |
181 related to the original; the original is unchanged. |
182 |
182 |
183 \item @{ML_type theory_ref} represents a sliding reference to an |
183 \item @{ML_type theory_ref} represents a sliding reference to an |
184 always valid theory; updates on the original are propagated |
184 always valid theory; updates on the original are propagated |
185 automatically. |
185 automatically. |
186 |
186 |
211 Entities derived in a proof context need to record inherent logical |
211 Entities derived in a proof context need to record inherent logical |
212 requirements explicitly, since there is no separate context |
212 requirements explicitly, since there is no separate context |
213 identification as for theories. For example, hypotheses used in |
213 identification as for theories. For example, hypotheses used in |
214 primitive derivations (cf.\ \secref{sec:thms}) are recorded |
214 primitive derivations (cf.\ \secref{sec:thms}) are recorded |
215 separately within the sequent @{text "\<Gamma> \<turnstile> \<phi>"}, just to make double |
215 separately within the sequent @{text "\<Gamma> \<turnstile> \<phi>"}, just to make double |
216 sure. Results could still leak into an alien proof context do to |
216 sure. Results could still leak into an alien proof context due to |
217 programming errors, but Isabelle/Isar includes some extra validity |
217 programming errors, but Isabelle/Isar includes some extra validity |
218 checks in critical positions, notably at the end of a sub-proof. |
218 checks in critical positions, notably at the end of a sub-proof. |
219 |
219 |
220 Proof contexts may be manipulated arbitrarily, although the common |
220 Proof contexts may be manipulated arbitrarily, although the common |
221 discipline is to follow block structure as a mental model: a given |
221 discipline is to follow block structure as a mental model: a given |
351 \bigskip A data declaration of type @{text "T"} results in the |
351 \bigskip A data declaration of type @{text "T"} results in the |
352 following interface: |
352 following interface: |
353 |
353 |
354 \medskip |
354 \medskip |
355 \begin{tabular}{ll} |
355 \begin{tabular}{ll} |
356 @{text "init: theory \<rightarrow> theory"} \\ |
356 @{text "init: theory \<rightarrow> T"} \\ |
357 @{text "get: context \<rightarrow> T"} \\ |
357 @{text "get: context \<rightarrow> T"} \\ |
358 @{text "put: T \<rightarrow> context \<rightarrow> context"} \\ |
358 @{text "put: T \<rightarrow> context \<rightarrow> context"} \\ |
359 @{text "map: (T \<rightarrow> T) \<rightarrow> context \<rightarrow> context"} \\ |
359 @{text "map: (T \<rightarrow> T) \<rightarrow> context \<rightarrow> context"} \\ |
360 \end{tabular} |
360 \end{tabular} |
361 \medskip |
361 \medskip |
503 subsection {* Basic names \label{sec:basic-names} *} |
503 subsection {* Basic names \label{sec:basic-names} *} |
504 |
504 |
505 text {* |
505 text {* |
506 A \emph{basic name} essentially consists of a single Isabelle |
506 A \emph{basic name} essentially consists of a single Isabelle |
507 identifier. There are conventions to mark separate classes of basic |
507 identifier. There are conventions to mark separate classes of basic |
508 names, by attaching a suffix of underscores (@{text "_"}): one |
508 names, by attaching a suffix of underscores: one underscore means |
509 underscore means \emph{internal name}, two underscores means |
509 \emph{internal name}, two underscores means \emph{Skolem name}, |
510 \emph{Skolem name}, three underscores means \emph{internal Skolem |
510 three underscores means \emph{internal Skolem name}. |
511 name}. |
|
512 |
511 |
513 For example, the basic name @{text "foo"} has the internal version |
512 For example, the basic name @{text "foo"} has the internal version |
514 @{text "foo_"}, with Skolem versions @{text "foo__"} and @{text |
513 @{text "foo_"}, with Skolem versions @{text "foo__"} and @{text |
515 "foo___"}, respectively. |
514 "foo___"}, respectively. |
516 |
515 |