25 \<^medskip> |
25 \<^medskip> |
26 Contexts and derivations are linked by the following key |
26 Contexts and derivations are linked by the following key |
27 principles: |
27 principles: |
28 |
28 |
29 \<^item> Transfer: monotonicity of derivations admits results to be |
29 \<^item> Transfer: monotonicity of derivations admits results to be |
30 transferred into a \emph{larger} context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> |
30 transferred into a \<^emph>\<open>larger\<close> context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> |
31 \<phi>"} implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>' |
31 \<phi>"} implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>' |
32 \<supseteq> \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}. |
32 \<supseteq> \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}. |
33 |
33 |
34 \<^item> Export: discharge of hypotheses admits results to be exported |
34 \<^item> Export: discharge of hypotheses admits results to be exported |
35 into a \emph{smaller} context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"} |
35 into a \<^emph>\<open>smaller\<close> context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"} |
36 implies @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and |
36 implies @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and |
37 @{text "\<Delta> = \<Gamma>' - \<Gamma>"}. Note that @{text "\<Theta>"} remains unchanged here, |
37 @{text "\<Delta> = \<Gamma>' - \<Gamma>"}. Note that @{text "\<Theta>"} remains unchanged here, |
38 only the @{text "\<Gamma>"} part is affected. |
38 only the @{text "\<Gamma>"} part is affected. |
39 |
39 |
40 |
40 |
41 \<^medskip> |
41 \<^medskip> |
42 By modeling the main characteristics of the primitive |
42 By modeling the main characteristics of the primitive |
43 @{text "\<Theta>"} and @{text "\<Gamma>"} above, and abstracting over any |
43 @{text "\<Theta>"} and @{text "\<Gamma>"} above, and abstracting over any |
44 particular logical content, we arrive at the fundamental notions of |
44 particular logical content, we arrive at the fundamental notions of |
45 \emph{theory context} and \emph{proof context} in Isabelle/Isar. |
45 \<^emph>\<open>theory context\<close> and \<^emph>\<open>proof context\<close> in Isabelle/Isar. |
46 These implement a certain policy to manage arbitrary \emph{context |
46 These implement a certain policy to manage arbitrary \<^emph>\<open>context |
47 data}. There is a strongly-typed mechanism to declare new kinds of |
47 data\<close>. There is a strongly-typed mechanism to declare new kinds of |
48 data at compile time. |
48 data at compile time. |
49 |
49 |
50 The internal bootstrap process of Isabelle/Pure eventually reaches a |
50 The internal bootstrap process of Isabelle/Pure eventually reaches a |
51 stage where certain data slots provide the logical content of @{text |
51 stage where certain data slots provide the logical content of @{text |
52 "\<Theta>"} and @{text "\<Gamma>"} sketched above, but this does not stop there! |
52 "\<Theta>"} and @{text "\<Gamma>"} sketched above, but this does not stop there! |
71 \<close> |
71 \<close> |
72 |
72 |
73 |
73 |
74 subsection \<open>Theory context \label{sec:context-theory}\<close> |
74 subsection \<open>Theory context \label{sec:context-theory}\<close> |
75 |
75 |
76 text \<open>A \emph{theory} is a data container with explicit name and |
76 text \<open>A \<^emph>\<open>theory\<close> is a data container with explicit name and |
77 unique identifier. Theories are related by a (nominal) sub-theory |
77 unique identifier. Theories are related by a (nominal) sub-theory |
78 relation, which corresponds to the dependency graph of the original |
78 relation, which corresponds to the dependency graph of the original |
79 construction; each theory is derived from a certain sub-graph of |
79 construction; each theory is derived from a certain sub-graph of |
80 ancestor theories. To this end, the system maintains a set of |
80 ancestor theories. To this end, the system maintains a set of |
81 symbolic ``identification stamps'' within each theory. |
81 symbolic ``identification stamps'' within each theory. |
225 text %mlantiq \<open> |
225 text %mlantiq \<open> |
226 \begin{matharray}{rcl} |
226 \begin{matharray}{rcl} |
227 @{ML_antiquotation_def "context"} & : & @{text ML_antiquotation} \\ |
227 @{ML_antiquotation_def "context"} & : & @{text ML_antiquotation} \\ |
228 \end{matharray} |
228 \end{matharray} |
229 |
229 |
230 \<^descr> @{text "@{context}"} refers to \emph{the} context at |
230 \<^descr> @{text "@{context}"} refers to \<^emph>\<open>the\<close> context at |
231 compile-time --- as abstract value. Independently of (local) theory |
231 compile-time --- as abstract value. Independently of (local) theory |
232 or proof mode, this always produces a meaningful result. |
232 or proof mode, this always produces a meaningful result. |
233 |
233 |
234 This is probably the most common antiquotation in interactive |
234 This is probably the most common antiquotation in interactive |
235 experimentation with ML inside Isar. |
235 experimentation with ML inside Isar. |
292 @{text "\<val> extend: T \<rightarrow> T"} & re-initialize on import \\ |
292 @{text "\<val> extend: T \<rightarrow> T"} & re-initialize on import \\ |
293 @{text "\<val> merge: T \<times> T \<rightarrow> T"} & join on import \\ |
293 @{text "\<val> merge: T \<times> T \<rightarrow> T"} & join on import \\ |
294 \end{tabular} |
294 \end{tabular} |
295 \<^medskip> |
295 \<^medskip> |
296 |
296 |
297 The @{text "empty"} value acts as initial default for \emph{any} |
297 The @{text "empty"} value acts as initial default for \<^emph>\<open>any\<close> |
298 theory that does not declare actual data content; @{text "extend"} |
298 theory that does not declare actual data content; @{text "extend"} |
299 is acts like a unitary version of @{text "merge"}. |
299 is acts like a unitary version of @{text "merge"}. |
300 |
300 |
301 Implementing @{text "merge"} can be tricky. The general idea is |
301 Implementing @{text "merge"} can be tricky. The general idea is |
302 that @{text "merge (data\<^sub>1, data\<^sub>2)"} inserts those parts of @{text |
302 that @{text "merge (data\<^sub>1, data\<^sub>2)"} inserts those parts of @{text |
320 |
320 |
321 The @{text "init"} operation is supposed to produce a pure value |
321 The @{text "init"} operation is supposed to produce a pure value |
322 from the given background theory and should be somehow |
322 from the given background theory and should be somehow |
323 ``immediate''. Whenever a proof context is initialized, which |
323 ``immediate''. Whenever a proof context is initialized, which |
324 happens frequently, the the system invokes the @{text "init"} |
324 happens frequently, the the system invokes the @{text "init"} |
325 operation of \emph{all} theory data slots ever declared. This also |
325 operation of \<^emph>\<open>all\<close> theory data slots ever declared. This also |
326 means that one needs to be economic about the total number of proof |
326 means that one needs to be economic about the total number of proof |
327 data declarations in the system, i.e.\ each ML module should declare |
327 data declarations in the system, i.e.\ each ML module should declare |
328 at most one, sometimes two data slots for its internal use. |
328 at most one, sometimes two data slots for its internal use. |
329 Repeated data declarations to simulate a record type should be |
329 Repeated data declarations to simulate a record type should be |
330 avoided! |
330 avoided! |
454 \<close> |
454 \<close> |
455 |
455 |
456 |
456 |
457 subsection \<open>Configuration options \label{sec:config-options}\<close> |
457 subsection \<open>Configuration options \label{sec:config-options}\<close> |
458 |
458 |
459 text \<open>A \emph{configuration option} is a named optional value of |
459 text \<open>A \<^emph>\<open>configuration option\<close> is a named optional value of |
460 some basic type (Boolean, integer, string) that is stored in the |
460 some basic type (Boolean, integer, string) that is stored in the |
461 context. It is a simple application of general context data |
461 context. It is a simple application of general context data |
462 (\secref{sec:context-data}) that is sufficiently common to justify |
462 (\secref{sec:context-data}) that is sufficiently common to justify |
463 customized setup, which includes some concrete declarations for |
463 customized setup, which includes some concrete declarations for |
464 end-users using existing notation for attributes (cf.\ |
464 end-users using existing notation for attributes (cf.\ |
602 |
602 |
603 |
603 |
604 subsection \<open>Basic names \label{sec:basic-name}\<close> |
604 subsection \<open>Basic names \label{sec:basic-name}\<close> |
605 |
605 |
606 text \<open> |
606 text \<open> |
607 A \emph{basic name} essentially consists of a single Isabelle |
607 A \<^emph>\<open>basic name\<close> essentially consists of a single Isabelle |
608 identifier. There are conventions to mark separate classes of basic |
608 identifier. There are conventions to mark separate classes of basic |
609 names, by attaching a suffix of underscores: one underscore means |
609 names, by attaching a suffix of underscores: one underscore means |
610 \emph{internal name}, two underscores means \emph{Skolem name}, |
610 \<^emph>\<open>internal name\<close>, two underscores means \<^emph>\<open>Skolem name\<close>, |
611 three underscores means \emph{internal Skolem name}. |
611 three underscores means \<^emph>\<open>internal Skolem name\<close>. |
612 |
612 |
613 For example, the basic name @{text "foo"} has the internal version |
613 For example, the basic name @{text "foo"} has the internal version |
614 @{text "foo_"}, with Skolem versions @{text "foo__"} and @{text |
614 @{text "foo_"}, with Skolem versions @{text "foo__"} and @{text |
615 "foo___"}, respectively. |
615 "foo___"}, respectively. |
616 |
616 |
620 as internal, which prevents mysterious names like @{text "xaa"} to |
620 as internal, which prevents mysterious names like @{text "xaa"} to |
621 appear in human-readable text. |
621 appear in human-readable text. |
622 |
622 |
623 \<^medskip> |
623 \<^medskip> |
624 Manipulating binding scopes often requires on-the-fly |
624 Manipulating binding scopes often requires on-the-fly |
625 renamings. A \emph{name context} contains a collection of already |
625 renamings. A \<^emph>\<open>name context\<close> contains a collection of already |
626 used names. The @{text "declare"} operation adds names to the |
626 used names. The @{text "declare"} operation adds names to the |
627 context. |
627 context. |
628 |
628 |
629 The @{text "invents"} operation derives a number of fresh names from |
629 The @{text "invents"} operation derives a number of fresh names from |
630 a given starting point. For example, the first three names derived |
630 a given starting point. For example, the first three names derived |
716 |
716 |
717 |
717 |
718 subsection \<open>Indexed names \label{sec:indexname}\<close> |
718 subsection \<open>Indexed names \label{sec:indexname}\<close> |
719 |
719 |
720 text \<open> |
720 text \<open> |
721 An \emph{indexed name} (or @{text "indexname"}) is a pair of a basic |
721 An \<^emph>\<open>indexed name\<close> (or @{text "indexname"}) is a pair of a basic |
722 name and a natural number. This representation allows efficient |
722 name and a natural number. This representation allows efficient |
723 renaming by incrementing the second component only. The canonical |
723 renaming by incrementing the second component only. The canonical |
724 way to rename two collections of indexnames apart from each other is |
724 way to rename two collections of indexnames apart from each other is |
725 this: determine the maximum index @{text "maxidx"} of the first |
725 this: determine the maximum index @{text "maxidx"} of the first |
726 collection, then increment all indexes of the second collection by |
726 collection, then increment all indexes of the second collection by |
763 \<close> |
763 \<close> |
764 |
764 |
765 |
765 |
766 subsection \<open>Long names \label{sec:long-name}\<close> |
766 subsection \<open>Long names \label{sec:long-name}\<close> |
767 |
767 |
768 text \<open>A \emph{long name} consists of a sequence of non-empty name |
768 text \<open>A \<^emph>\<open>long name\<close> consists of a sequence of non-empty name |
769 components. The packed representation uses a dot as separator, as |
769 components. The packed representation uses a dot as separator, as |
770 in ``@{text "A.b.c"}''. The last component is called \emph{base |
770 in ``@{text "A.b.c"}''. The last component is called \<^emph>\<open>base |
771 name}, the remaining prefix is called \emph{qualifier} (which may be |
771 name\<close>, the remaining prefix is called \<^emph>\<open>qualifier\<close> (which may be |
772 empty). The qualifier can be understood as the access path to the |
772 empty). The qualifier can be understood as the access path to the |
773 named entity while passing through some nested block-structure, |
773 named entity while passing through some nested block-structure, |
774 although our free-form long names do not really enforce any strict |
774 although our free-form long names do not really enforce any strict |
775 discipline. |
775 discipline. |
776 |
776 |