doc-src/IsarImplementation/Thy/Prelim.thy
 author wenzelm Sat Oct 09 21:18:20 2010 +0100 (2010-10-09) changeset 39833 6d54a48c859d parent 39832 1080dee73a53 child 39837 eacb7825025d permissions -rw-r--r--
more examples;
 wenzelm@29755  1 theory Prelim  wenzelm@29755  2 imports Base  wenzelm@29755  3 begin  wenzelm@18537  4 wenzelm@18537  5 chapter {* Preliminaries *}  wenzelm@18537  6 wenzelm@20429  7 section {* Contexts \label{sec:context} *}  wenzelm@18537  8 wenzelm@20429  9 text {*  wenzelm@20451  10  A logical context represents the background that is required for  wenzelm@20451  11  formulating statements and composing proofs. It acts as a medium to  wenzelm@20451  12  produce formal content, depending on earlier material (declarations,  wenzelm@20451  13  results etc.).  wenzelm@18537  14 wenzelm@20451  15  For example, derivations within the Isabelle/Pure logic can be  wenzelm@20451  16  described as a judgment @{text "\ \\<^sub>\ \"}, which means that a  wenzelm@20429  17  proposition @{text "\"} is derivable from hypotheses @{text "\"}  wenzelm@20429  18  within the theory @{text "\"}. There are logical reasons for  wenzelm@20451  19  keeping @{text "\"} and @{text "\"} separate: theories can be  wenzelm@20451  20  liberal about supporting type constructors and schematic  wenzelm@20451  21  polymorphism of constants and axioms, while the inner calculus of  wenzelm@20451  22  @{text "\ \ \"} is strictly limited to Simple Type Theory (with  wenzelm@20451  23  fixed type variables in the assumptions).  wenzelm@18537  24 wenzelm@20429  25  \medskip Contexts and derivations are linked by the following key  wenzelm@20429  26  principles:  wenzelm@20429  27 wenzelm@20429  28  \begin{itemize}  wenzelm@20429  29 wenzelm@20429  30  \item Transfer: monotonicity of derivations admits results to be  wenzelm@20451  31  transferred into a \emph{larger} context, i.e.\ @{text "\ \\<^sub>\  wenzelm@20451  32  \"} implies @{text "\' \\<^sub>\\<^sub>' \"} for contexts @{text "\'  wenzelm@20451  33  \ \"} and @{text "\' \ \"}.  wenzelm@18537  34 wenzelm@20429  35  \item Export: discharge of hypotheses admits results to be exported  wenzelm@20451  36  into a \emph{smaller} context, i.e.\ @{text "\' \\<^sub>\ \"}  wenzelm@20451  37  implies @{text "\ \\<^sub>\ \ \ \"} where @{text "\' \ \"} and  wenzelm@20451  38  @{text "\ = \' - \"}. Note that @{text "\"} remains unchanged here,  wenzelm@20451  39  only the @{text "\"} part is affected.  wenzelm@20429  40 wenzelm@20429  41  \end{itemize}  wenzelm@18537  42 wenzelm@20451  43  \medskip By modeling the main characteristics of the primitive  wenzelm@20451  44  @{text "\"} and @{text "\"} above, and abstracting over any  wenzelm@20451  45  particular logical content, we arrive at the fundamental notions of  wenzelm@20451  46  \emph{theory context} and \emph{proof context} in Isabelle/Isar.  wenzelm@20451  47  These implement a certain policy to manage arbitrary \emph{context  wenzelm@20451  48  data}. There is a strongly-typed mechanism to declare new kinds of  wenzelm@20429  49  data at compile time.  wenzelm@18537  50 wenzelm@20451  51  The internal bootstrap process of Isabelle/Pure eventually reaches a  wenzelm@20451  52  stage where certain data slots provide the logical content of @{text  wenzelm@20451  53  "\"} and @{text "\"} sketched above, but this does not stop there!  wenzelm@20451  54  Various additional data slots support all kinds of mechanisms that  wenzelm@20451  55  are not necessarily part of the core logic.  wenzelm@18537  56 wenzelm@20429  57  For example, there would be data for canonical introduction and  wenzelm@20429  58  elimination rules for arbitrary operators (depending on the  wenzelm@20429  59  object-logic and application), which enables users to perform  wenzelm@20451  60  standard proof steps implicitly (cf.\ the @{text "rule"} method  wenzelm@20451  61  \cite{isabelle-isar-ref}).  wenzelm@18537  62 wenzelm@20451  63  \medskip Thus Isabelle/Isar is able to bring forth more and more  wenzelm@20451  64  concepts successively. In particular, an object-logic like  wenzelm@20451  65  Isabelle/HOL continues the Isabelle/Pure setup by adding specific  wenzelm@20451  66  components for automated reasoning (classical reasoner, tableau  wenzelm@20451  67  prover, structured induction etc.) and derived specification  wenzelm@20451  68  mechanisms (inductive predicates, recursive functions etc.). All of  wenzelm@20451  69  this is ultimately based on the generic data management by theory  wenzelm@20451  70  and proof contexts introduced here.  wenzelm@18537  71 *}  wenzelm@18537  72 wenzelm@18537  73 wenzelm@18537  74 subsection {* Theory context \label{sec:context-theory} *}  wenzelm@18537  75 wenzelm@34921  76 text {* A \emph{theory} is a data container with explicit name and  wenzelm@34921  77  unique identifier. Theories are related by a (nominal) sub-theory  wenzelm@20451  78  relation, which corresponds to the dependency graph of the original  wenzelm@20451  79  construction; each theory is derived from a certain sub-graph of  wenzelm@34921  80  ancestor theories. To this end, the system maintains a set of  wenzelm@34921  81  symbolic identification stamps'' within each theory.  wenzelm@18537  82 wenzelm@34921  83  In order to avoid the full-scale overhead of explicit sub-theory  wenzelm@34921  84  identification of arbitrary intermediate stages, a theory is  wenzelm@34921  85  switched into @{text "draft"} mode under certain circumstances. A  wenzelm@34921  86  draft theory acts like a linear type, where updates invalidate  wenzelm@34921  87  earlier versions. An invalidated draft is called \emph{stale}.  wenzelm@20429  88 wenzelm@34921  89  The @{text "checkpoint"} operation produces a safe stepping stone  wenzelm@34921  90  that will survive the next update without becoming stale: both the  wenzelm@34921  91  old and the new theory remain valid and are related by the  wenzelm@34921  92  sub-theory relation. Checkpointing essentially recovers purely  wenzelm@34921  93  functional theory values, at the expense of some extra internal  wenzelm@34921  94  bookkeeping.  wenzelm@20447  95 wenzelm@20447  96  The @{text "copy"} operation produces an auxiliary version that has  wenzelm@20447  97  the same data content, but is unrelated to the original: updates of  wenzelm@20447  98  the copy do not affect the original, neither does the sub-theory  wenzelm@20447  99  relation hold.  wenzelm@20429  100 wenzelm@34921  101  The @{text "merge"} operation produces the least upper bound of two  wenzelm@34921  102  theories, which actually degenerates into absorption of one theory  wenzelm@34921  103  into the other (according to the nominal sub-theory relation).  wenzelm@34921  104 wenzelm@34921  105  The @{text "begin"} operation starts a new theory by importing  wenzelm@34921  106  several parent theories and entering a special mode of nameless  wenzelm@34921  107  incremental updates, until the final @{text "end"} operation is  wenzelm@34921  108  performed.  wenzelm@34921  109 wenzelm@20447  110  \medskip The example in \figref{fig:ex-theory} below shows a theory  wenzelm@20451  111  graph derived from @{text "Pure"}, with theory @{text "Length"}  wenzelm@20451  112  importing @{text "Nat"} and @{text "List"}. The body of @{text  wenzelm@20451  113  "Length"} consists of a sequence of updates, working mostly on  wenzelm@34921  114  drafts internally, while transaction boundaries of Isar top-level  wenzelm@34921  115  commands (\secref{sec:isar-toplevel}) are guaranteed to be safe  wenzelm@34921  116  checkpoints.  wenzelm@20447  117 wenzelm@20447  118  \begin{figure}[htb]  wenzelm@20447  119  \begin{center}  wenzelm@20429  120  \begin{tabular}{rcccl}  wenzelm@20447  121  & & @{text "Pure"} \\  wenzelm@20447  122  & & @{text "\"} \\  wenzelm@20447  123  & & @{text "FOL"} \\  wenzelm@18537  124  & $\swarrow$ & & $\searrow$ & \\  wenzelm@21852  125  @{text "Nat"} & & & & @{text "List"} \\  wenzelm@18537  126  & $\searrow$ & & $\swarrow$ \\  wenzelm@20447  127  & & @{text "Length"} \\  wenzelm@26864  128  & & \multicolumn{3}{l}{~~@{keyword "imports"}} \\  wenzelm@26864  129  & & \multicolumn{3}{l}{~~@{keyword "begin"}} \\  wenzelm@18537  130  & & $\vdots$~~ \\  wenzelm@20447  131  & & @{text "\"}~~ \\  wenzelm@20447  132  & & $\vdots$~~ \\  wenzelm@20447  133  & & @{text "\"}~~ \\  wenzelm@20447  134  & & $\vdots$~~ \\  wenzelm@26864  135  & & \multicolumn{3}{l}{~~@{command "end"}} \\  wenzelm@20429  136  \end{tabular}  wenzelm@20451  137  \caption{A theory definition depending on ancestors}\label{fig:ex-theory}  wenzelm@20447  138  \end{center}  wenzelm@20447  139  \end{figure}  wenzelm@20451  140 wenzelm@20451  141  \medskip There is a separate notion of \emph{theory reference} for  wenzelm@20451  142  maintaining a live link to an evolving theory context: updates on  wenzelm@39821  143  drafts are propagated automatically. Dynamic updating stops when  wenzelm@39821  144  the next @{text "checkpoint"} is reached.  wenzelm@20451  145 wenzelm@20451  146  Derived entities may store a theory reference in order to indicate  wenzelm@39821  147  the formal context from which they are derived. This implicitly  wenzelm@39821  148  assumes monotonic reasoning, because the referenced context may  wenzelm@39821  149  become larger without further notice.  wenzelm@18537  150 *}  wenzelm@18537  151 wenzelm@20430  152 text %mlref {*  wenzelm@20447  153  \begin{mldecls}  wenzelm@20447  154  @{index_ML_type theory} \\  wenzelm@20447  155  @{index_ML Theory.subthy: "theory * theory -> bool"} \\  wenzelm@20447  156  @{index_ML Theory.checkpoint: "theory -> theory"} \\  wenzelm@20547  157  @{index_ML Theory.copy: "theory -> theory"} \\  wenzelm@34921  158  @{index_ML Theory.merge: "theory * theory -> theory"} \\  wenzelm@34921  159  @{index_ML Theory.begin_theory: "string -> theory list -> theory"} \\  wenzelm@20547  160  \end{mldecls}  wenzelm@20547  161  \begin{mldecls}  wenzelm@20447  162  @{index_ML_type theory_ref} \\  wenzelm@20447  163  @{index_ML Theory.deref: "theory_ref -> theory"} \\  wenzelm@24137  164  @{index_ML Theory.check_thy: "theory -> theory_ref"} \\  wenzelm@20447  165  \end{mldecls}  wenzelm@20447  166 wenzelm@20447  167  \begin{description}  wenzelm@20447  168 wenzelm@20451  169  \item @{ML_type theory} represents theory contexts. This is  wenzelm@39821  170  essentially a linear type, with explicit runtime checking.  wenzelm@39821  171  Primitive theory operations destroy the original version, which then  wenzelm@39821  172  becomes stale''. This can be prevented by explicit checkpointing,  wenzelm@39821  173  which the system does at least at the boundary of toplevel command  wenzelm@39821  174  transactions \secref{sec:isar-toplevel}.  wenzelm@20447  175 wenzelm@34921  176  \item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} compares theories  wenzelm@34921  177  according to the intrinsic graph structure of the construction.  wenzelm@34921  178  This sub-theory relation is a nominal approximation of inclusion  wenzelm@34921  179  (@{text "\"}) of the corresponding content (according to the  wenzelm@34921  180  semantics of the ML modules that implement the data).  wenzelm@20447  181 wenzelm@20447  182  \item @{ML "Theory.checkpoint"}~@{text "thy"} produces a safe  wenzelm@34921  183  stepping stone in the linear development of @{text "thy"}. This  wenzelm@34921  184  changes the old theory, but the next update will result in two  wenzelm@34921  185  related, valid theories.  wenzelm@20447  186 wenzelm@20447  187  \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text  wenzelm@34921  188  "thy"} with the same data. The copy is not related to the original,  wenzelm@34921  189  but the original is unchanged.  wenzelm@34921  190 wenzelm@34921  191  \item @{ML "Theory.merge"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} absorbs one theory  wenzelm@34921  192  into the other, without changing @{text "thy\<^sub>1"} or @{text "thy\<^sub>2"}.  wenzelm@34921  193  This version of ad-hoc theory merge fails for unrelated theories!  wenzelm@34921  194 wenzelm@34921  195  \item @{ML "Theory.begin_theory"}~@{text "name parents"} constructs  wenzelm@39825  196  a new theory based on the given parents. This ML function is  wenzelm@34921  197  normally not invoked directly.  wenzelm@20447  198 wenzelm@20451  199  \item @{ML_type theory_ref} represents a sliding reference to an  wenzelm@20451  200  always valid theory; updates on the original are propagated  wenzelm@20447  201  automatically.  wenzelm@20447  202 wenzelm@24137  203  \item @{ML "Theory.deref"}~@{text "thy_ref"} turns a @{ML_type  wenzelm@24137  204  "theory_ref"} into an @{ML_type "theory"} value. As the referenced  wenzelm@24137  205  theory evolves monotonically over time, later invocations of @{ML  wenzelm@20451  206  "Theory.deref"} may refer to a larger context.  wenzelm@20447  207 wenzelm@24137  208  \item @{ML "Theory.check_thy"}~@{text "thy"} produces a @{ML_type  wenzelm@24137  209  "theory_ref"} from a valid @{ML_type "theory"} value.  wenzelm@24137  210 wenzelm@20447  211  \end{description}  wenzelm@20430  212 *}  wenzelm@20430  213 wenzelm@39832  214 text %mlantiq {*  wenzelm@39832  215  \begin{matharray}{rcl}  wenzelm@39832  216  @{ML_antiquotation_def "theory"} & : & @{text ML_antiquotation} \\  wenzelm@39832  217  @{ML_antiquotation_def "theory_ref"} & : & @{text ML_antiquotation} \\  wenzelm@39832  218  \end{matharray}  wenzelm@39832  219 wenzelm@39832  220  \begin{rail}  wenzelm@39832  221  ('theory' | 'theory\_ref') nameref?  wenzelm@39832  222  ;  wenzelm@39832  223  \end{rail}  wenzelm@39832  224 wenzelm@39832  225  \begin{description}  wenzelm@39832  226 wenzelm@39832  227  \item @{text "@{theory}"} refers to the background theory of the  wenzelm@39832  228  current context --- as abstract value.  wenzelm@39832  229 wenzelm@39832  230  \item @{text "@{theory A}"} refers to an explicitly named ancestor  wenzelm@39832  231  theory @{text "A"} of the background theory of the current context  wenzelm@39832  232  --- as abstract value.  wenzelm@39832  233 wenzelm@39832  234  \item @{text "@{theory_ref}"} is similar to @{text "@{theory}"}, but  wenzelm@39832  235  produces a @{ML_type theory_ref} via @{ML "Theory.check_thy"} as  wenzelm@39832  236  explained above.  wenzelm@39832  237 wenzelm@39832  238  \end{description}  wenzelm@39832  239 *}  wenzelm@39832  240 wenzelm@18537  241 wenzelm@18537  242 subsection {* Proof context \label{sec:context-proof} *}  wenzelm@18537  243 wenzelm@34921  244 text {* A proof context is a container for pure data with a  wenzelm@39821  245  back-reference to the theory from which it is derived. The @{text  wenzelm@39821  246  "init"} operation creates a proof context from a given theory.  wenzelm@34921  247  Modifications to draft theories are propagated to the proof context  wenzelm@34921  248  as usual, but there is also an explicit @{text "transfer"} operation  wenzelm@34921  249  to force resynchronization with more substantial updates to the  wenzelm@34921  250  underlying theory.  wenzelm@20429  251 wenzelm@34921  252  Entities derived in a proof context need to record logical  wenzelm@20447  253  requirements explicitly, since there is no separate context  wenzelm@34921  254  identification or symbolic inclusion as for theories. For example,  wenzelm@34921  255  hypotheses used in primitive derivations (cf.\ \secref{sec:thms})  wenzelm@34921  256  are recorded separately within the sequent @{text "\ \ \"}, just to  wenzelm@34921  257  make double sure. Results could still leak into an alien proof  wenzelm@34921  258  context due to programming errors, but Isabelle/Isar includes some  wenzelm@34921  259  extra validity checks in critical positions, notably at the end of a  wenzelm@34921  260  sub-proof.  wenzelm@20429  261 wenzelm@20451  262  Proof contexts may be manipulated arbitrarily, although the common  wenzelm@20451  263  discipline is to follow block structure as a mental model: a given  wenzelm@20451  264  context is extended consecutively, and results are exported back  wenzelm@34921  265  into the original context. Note that an Isar proof state models  wenzelm@20451  266  block-structured reasoning explicitly, using a stack of proof  wenzelm@34921  267  contexts internally. For various technical reasons, the background  wenzelm@34921  268  theory of an Isar proof state must not be changed while the proof is  wenzelm@34921  269  still under construction!  wenzelm@18537  270 *}  wenzelm@18537  271 wenzelm@20449  272 text %mlref {*  wenzelm@20449  273  \begin{mldecls}  wenzelm@20449  274  @{index_ML_type Proof.context} \\  wenzelm@36611  275  @{index_ML ProofContext.init_global: "theory -> Proof.context"} \\  wenzelm@20449  276  @{index_ML ProofContext.theory_of: "Proof.context -> theory"} \\  wenzelm@20449  277  @{index_ML ProofContext.transfer: "theory -> Proof.context -> Proof.context"} \\  wenzelm@20449  278  \end{mldecls}  wenzelm@20449  279 wenzelm@20449  280  \begin{description}  wenzelm@20449  281 wenzelm@20449  282  \item @{ML_type Proof.context} represents proof contexts. Elements  wenzelm@20449  283  of this type are essentially pure values, with a sliding reference  wenzelm@20449  284  to the background theory.  wenzelm@20449  285 wenzelm@36611  286  \item @{ML ProofContext.init_global}~@{text "thy"} produces a proof context  wenzelm@20449  287  derived from @{text "thy"}, initializing all data.  wenzelm@20449  288 wenzelm@20449  289  \item @{ML ProofContext.theory_of}~@{text "ctxt"} selects the  wenzelm@20451  290  background theory from @{text "ctxt"}, dereferencing its internal  wenzelm@20451  291  @{ML_type theory_ref}.  wenzelm@20449  292 wenzelm@20449  293  \item @{ML ProofContext.transfer}~@{text "thy ctxt"} promotes the  wenzelm@20449  294  background theory of @{text "ctxt"} to the super theory @{text  wenzelm@20449  295  "thy"}.  wenzelm@20449  296 wenzelm@20449  297  \end{description}  wenzelm@20449  298 *}  wenzelm@20449  299 wenzelm@39832  300 text %mlantiq {*  wenzelm@39832  301  \begin{matharray}{rcl}  wenzelm@39832  302  @{ML_antiquotation_def "context"} & : & @{text ML_antiquotation} \\  wenzelm@39832  303  \end{matharray}  wenzelm@39832  304 wenzelm@39832  305  \begin{description}  wenzelm@39832  306 wenzelm@39832  307  \item @{text "@{context}"} refers to \emph{the} context at  wenzelm@39832  308  compile-time --- as abstract value. Independently of (local) theory  wenzelm@39832  309  or proof mode, this always produces a meaningful result.  wenzelm@39832  310 wenzelm@39832  311  This is probably the most common antiquotation in interactive  wenzelm@39832  312  experimentation with ML inside Isar.  wenzelm@39832  313 wenzelm@39832  314  \end{description}  wenzelm@39832  315 *}  wenzelm@39832  316 wenzelm@20430  317 wenzelm@20451  318 subsection {* Generic contexts \label{sec:generic-context} *}  wenzelm@20429  319 wenzelm@20449  320 text {*  wenzelm@20449  321  A generic context is the disjoint sum of either a theory or proof  wenzelm@20451  322  context. Occasionally, this enables uniform treatment of generic  wenzelm@20450  323  context data, typically extra-logical information. Operations on  wenzelm@20449  324  generic contexts include the usual injections, partial selections,  wenzelm@20449  325  and combinators for lifting operations on either component of the  wenzelm@20449  326  disjoint sum.  wenzelm@20449  327 wenzelm@20449  328  Moreover, there are total operations @{text "theory_of"} and @{text  wenzelm@20449  329  "proof_of"} to convert a generic context into either kind: a theory  wenzelm@20451  330  can always be selected from the sum, while a proof context might  wenzelm@34921  331  have to be constructed by an ad-hoc @{text "init"} operation, which  wenzelm@34921  332  incurs a small runtime overhead.  wenzelm@20449  333 *}  wenzelm@20430  334 wenzelm@20449  335 text %mlref {*  wenzelm@20449  336  \begin{mldecls}  wenzelm@20449  337  @{index_ML_type Context.generic} \\  wenzelm@20449  338  @{index_ML Context.theory_of: "Context.generic -> theory"} \\  wenzelm@20449  339  @{index_ML Context.proof_of: "Context.generic -> Proof.context"} \\  wenzelm@20449  340  \end{mldecls}  wenzelm@20449  341 wenzelm@20449  342  \begin{description}  wenzelm@20430  343 wenzelm@20449  344  \item @{ML_type Context.generic} is the direct sum of @{ML_type  wenzelm@20451  345  "theory"} and @{ML_type "Proof.context"}, with the datatype  wenzelm@20451  346  constructors @{ML "Context.Theory"} and @{ML "Context.Proof"}.  wenzelm@20449  347 wenzelm@20449  348  \item @{ML Context.theory_of}~@{text "context"} always produces a  wenzelm@20449  349  theory from the generic @{text "context"}, using @{ML  wenzelm@20449  350  "ProofContext.theory_of"} as required.  wenzelm@20449  351 wenzelm@20449  352  \item @{ML Context.proof_of}~@{text "context"} always produces a  wenzelm@20449  353  proof context from the generic @{text "context"}, using @{ML  wenzelm@36611  354  "ProofContext.init_global"} as required (note that this re-initializes the  wenzelm@20451  355  context data with each invocation).  wenzelm@20449  356 wenzelm@20449  357  \end{description}  wenzelm@20449  358 *}  wenzelm@20437  359 wenzelm@20476  360 wenzelm@20476  361 subsection {* Context data \label{sec:context-data} *}  wenzelm@20447  362 wenzelm@33524  363 text {* The main purpose of theory and proof contexts is to manage  wenzelm@33524  364  arbitrary (pure) data. New data types can be declared incrementally  wenzelm@33524  365  at compile time. There are separate declaration mechanisms for any  wenzelm@33524  366  of the three kinds of contexts: theory, proof, generic.  wenzelm@20449  367 wenzelm@33524  368  \paragraph{Theory data} declarations need to implement the following  wenzelm@33524  369  SML signature:  wenzelm@20449  370 wenzelm@20449  371  \medskip  wenzelm@20449  372  \begin{tabular}{ll}  wenzelm@22869  373  @{text "\ T"} & representing type \\  wenzelm@22869  374  @{text "\ empty: T"} & empty default value \\  wenzelm@22869  375  @{text "\ extend: T \ T"} & re-initialize on import \\  wenzelm@22869  376  @{text "\ merge: T \ T \ T"} & join on import \\  wenzelm@20449  377  \end{tabular}  wenzelm@20449  378  \medskip  wenzelm@20449  379 wenzelm@22869  380  \noindent The @{text "empty"} value acts as initial default for  wenzelm@22869  381  \emph{any} theory that does not declare actual data content; @{text  wenzelm@33524  382  "extend"} is acts like a unitary version of @{text "merge"}.  wenzelm@20449  383 wenzelm@34921  384  Implementing @{text "merge"} can be tricky. The general idea is  wenzelm@34921  385  that @{text "merge (data\<^sub>1, data\<^sub>2)"} inserts those parts of @{text  wenzelm@34921  386  "data\<^sub>2"} into @{text "data\<^sub>1"} that are not yet present, while  wenzelm@34921  387  keeping the general order of things. The @{ML Library.merge}  wenzelm@34921  388  function on plain lists may serve as canonical template.  wenzelm@34921  389 wenzelm@34921  390  Particularly note that shared parts of the data must not be  wenzelm@34921  391  duplicated by naive concatenation, or a theory graph that is like a  wenzelm@34921  392  chain of diamonds would cause an exponential blowup!  wenzelm@34921  393 wenzelm@33524  394  \paragraph{Proof context data} declarations need to implement the  wenzelm@33524  395  following SML signature:  wenzelm@20449  396 wenzelm@20449  397  \medskip  wenzelm@20449  398  \begin{tabular}{ll}  wenzelm@22869  399  @{text "\ T"} & representing type \\  wenzelm@22869  400  @{text "\ init: theory \ T"} & produce initial value \\  wenzelm@20449  401  \end{tabular}  wenzelm@20449  402  \medskip  wenzelm@20449  403 wenzelm@20449  404  \noindent The @{text "init"} operation is supposed to produce a pure  wenzelm@34921  405  value from the given background theory and should be somehow  wenzelm@34921  406  immediate''. Whenever a proof context is initialized, which  wenzelm@34921  407  happens frequently, the the system invokes the @{text "init"}  wenzelm@39821  408  operation of \emph{all} theory data slots ever declared. This also  wenzelm@39821  409  means that one needs to be economic about the total number of proof  wenzelm@39821  410  data declarations in the system, i.e.\ each ML module should declare  wenzelm@39821  411  at most one, sometimes two data slots for its internal use.  wenzelm@39821  412  Repeated data declarations to simulate a record type should be  wenzelm@39821  413  avoided!  wenzelm@20449  414 wenzelm@20451  415  \paragraph{Generic data} provides a hybrid interface for both theory  wenzelm@33524  416  and proof data. The @{text "init"} operation for proof contexts is  wenzelm@33524  417  predefined to select the current data value from the background  wenzelm@33524  418  theory.  wenzelm@20449  419 wenzelm@39821  420  \bigskip Any of the above data declarations over type @{text "T"}  wenzelm@39821  421  result in an ML structure with the following signature:  wenzelm@20449  422 wenzelm@20449  423  \medskip  wenzelm@20449  424  \begin{tabular}{ll}  wenzelm@20449  425  @{text "get: context \ T"} \\  wenzelm@20449  426  @{text "put: T \ context \ context"} \\  wenzelm@20449  427  @{text "map: (T \ T) \ context \ context"} \\  wenzelm@20449  428  \end{tabular}  wenzelm@20449  429  \medskip  wenzelm@20449  430 wenzelm@34921  431  \noindent These other operations provide exclusive access for the  wenzelm@34921  432  particular kind of context (theory, proof, or generic context).  wenzelm@39821  433  This interface observes the ML discipline for types and scopes:  wenzelm@39821  434  there is no other way to access the corresponding data slot of a  wenzelm@39821  435  context. By keeping these operations private, an Isabelle/ML module  wenzelm@39821  436  may maintain abstract values authentically.  wenzelm@20447  437 *}  wenzelm@20447  438 wenzelm@20450  439 text %mlref {*  wenzelm@20450  440  \begin{mldecls}  wenzelm@33524  441  @{index_ML_functor Theory_Data} \\  wenzelm@33524  442  @{index_ML_functor Proof_Data} \\  wenzelm@33524  443  @{index_ML_functor Generic_Data} \\  wenzelm@20450  444  \end{mldecls}  wenzelm@20450  445 wenzelm@20450  446  \begin{description}  wenzelm@20450  447 wenzelm@33524  448  \item @{ML_functor Theory_Data}@{text "(spec)"} declares data for  wenzelm@20450  449  type @{ML_type theory} according to the specification provided as  wenzelm@20451  450  argument structure. The resulting structure provides data init and  wenzelm@20451  451  access operations as described above.  wenzelm@20450  452 wenzelm@33524  453  \item @{ML_functor Proof_Data}@{text "(spec)"} is analogous to  wenzelm@33524  454  @{ML_functor Theory_Data} for type @{ML_type Proof.context}.  wenzelm@20450  455 wenzelm@33524  456  \item @{ML_functor Generic_Data}@{text "(spec)"} is analogous to  wenzelm@33524  457  @{ML_functor Theory_Data} for type @{ML_type Context.generic}.  wenzelm@20450  458 wenzelm@20450  459  \end{description}  wenzelm@20450  460 *}  wenzelm@20450  461 wenzelm@34928  462 text %mlex {*  wenzelm@34928  463  The following artificial example demonstrates theory  wenzelm@34928  464  data: we maintain a set of terms that are supposed to be wellformed  wenzelm@34928  465  wrt.\ the enclosing theory. The public interface is as follows:  wenzelm@34928  466 *}  wenzelm@34928  467 wenzelm@34928  468 ML {*  wenzelm@34928  469  signature WELLFORMED_TERMS =  wenzelm@34928  470  sig  wenzelm@34928  471  val get: theory -> term list  wenzelm@34928  472  val add: term -> theory -> theory  wenzelm@34928  473  end;  wenzelm@34928  474 *}  wenzelm@34928  475 wenzelm@34928  476 text {* \noindent The implementation uses private theory data  wenzelm@34928  477  internally, and only exposes an operation that involves explicit  wenzelm@34928  478  argument checking wrt.\ the given theory. *}  wenzelm@34928  479 wenzelm@34928  480 ML {*  wenzelm@34928  481  structure Wellformed_Terms: WELLFORMED_TERMS =  wenzelm@34928  482  struct  wenzelm@34928  483 wenzelm@34928  484  structure Terms = Theory_Data  wenzelm@34928  485  (  wenzelm@39687  486  type T = term Ord_List.T;  wenzelm@34928  487  val empty = [];  wenzelm@34928  488  val extend = I;  wenzelm@34928  489  fun merge (ts1, ts2) =  wenzelm@39687  490  Ord_List.union Term_Ord.fast_term_ord ts1 ts2;  wenzelm@34928  491  )  wenzelm@34928  492 wenzelm@34928  493  val get = Terms.get;  wenzelm@34928  494 wenzelm@34928  495  fun add raw_t thy =  wenzelm@39821  496  let  wenzelm@39821  497  val t = Sign.cert_term thy raw_t;  wenzelm@39821  498  in  wenzelm@39821  499  Terms.map (Ord_List.insert Term_Ord.fast_term_ord t) thy  wenzelm@39821  500  end;  wenzelm@34928  501 wenzelm@34928  502  end;  wenzelm@34928  503 *}  wenzelm@34928  504 wenzelm@39821  505 text {* \noindent We use @{ML_type "term Ord_List.T"} for reasonably  wenzelm@39821  506  efficient representation of a set of terms: all operations are  wenzelm@39821  507  linear in the number of stored elements. Here we assume that users  wenzelm@39821  508  of this module do not care about the declaration order, since that  wenzelm@39821  509  data structure forces its own arrangement of elements.  wenzelm@34928  510 wenzelm@34928  511  Observe how the @{verbatim merge} operation joins the data slots of  wenzelm@39687  512  the two constituents: @{ML Ord_List.union} prevents duplication of  wenzelm@34928  513  common data from different branches, thus avoiding the danger of  wenzelm@39821  514  exponential blowup. Plain list append etc.\ must never be used for  wenzelm@39821  515  theory data merges!  wenzelm@34928  516 wenzelm@34928  517  \medskip Our intended invariant is achieved as follows:  wenzelm@34928  518  \begin{enumerate}  wenzelm@34928  519 wenzelm@34928  520  \item @{ML Wellformed_Terms.add} only admits terms that have passed  wenzelm@34928  521  the @{ML Sign.cert_term} check of the given theory at that point.  wenzelm@34928  522 wenzelm@34928  523  \item Wellformedness in the sense of @{ML Sign.cert_term} is  wenzelm@34928  524  monotonic wrt.\ the sub-theory relation. So our data can move  wenzelm@34928  525  upwards in the hierarchy (via extension or merges), and maintain  wenzelm@34928  526  wellformedness without further checks.  wenzelm@34928  527 wenzelm@34928  528  \end{enumerate}  wenzelm@34928  529 wenzelm@34928  530  Note that all basic operations of the inference kernel (which  wenzelm@34928  531  includes @{ML Sign.cert_term}) observe this monotonicity principle,  wenzelm@34928  532  but other user-space tools don't. For example, fully-featured  wenzelm@34928  533  type-inference via @{ML Syntax.check_term} (cf.\  wenzelm@34928  534  \secref{sec:term-check}) is not necessarily monotonic wrt.\ the  wenzelm@34928  535  background theory, since constraints of term constants can be  wenzelm@39821  536  modified by later declarations, for example.  wenzelm@34928  537 wenzelm@34928  538  In most cases, user-space context data does not have to take such  wenzelm@34928  539  invariants too seriously. The situation is different in the  wenzelm@34928  540  implementation of the inference kernel itself, which uses the very  wenzelm@34928  541  same data mechanisms for types, constants, axioms etc.  wenzelm@34928  542 *}  wenzelm@34928  543 wenzelm@20447  544 wenzelm@26872  545 section {* Names \label{sec:names} *}  wenzelm@20451  546 wenzelm@34925  547 text {* In principle, a name is just a string, but there are various  wenzelm@34925  548  conventions for representing additional structure. For example,  wenzelm@34927  549  @{text "Foo.bar.baz"}'' is considered as a long name consisting of  wenzelm@34927  550  qualifier @{text "Foo.bar"} and base name @{text "baz"}. The  wenzelm@34927  551  individual constituents of a name may have further substructure,  wenzelm@34927  552  e.g.\ the string \verb,\,\verb,,'' encodes as a single  wenzelm@34927  553  symbol.  wenzelm@34927  554 wenzelm@34927  555  \medskip Subsequently, we shall introduce specific categories of  wenzelm@34927  556  names. Roughly speaking these correspond to logical entities as  wenzelm@34927  557  follows:  wenzelm@34927  558  \begin{itemize}  wenzelm@34927  559 wenzelm@34927  560  \item Basic names (\secref{sec:basic-name}): free and bound  wenzelm@34927  561  variables.  wenzelm@34927  562 wenzelm@34927  563  \item Indexed names (\secref{sec:indexname}): schematic variables.  wenzelm@34927  564 wenzelm@34927  565  \item Long names (\secref{sec:long-name}): constants of any kind  wenzelm@34927  566  (type constructors, term constants, other concepts defined in user  wenzelm@34927  567  space). Such entities are typically managed via name spaces  wenzelm@34927  568  (\secref{sec:name-space}).  wenzelm@34927  569 wenzelm@34927  570  \end{itemize}  wenzelm@20451  571 *}  wenzelm@20437  572 wenzelm@20437  573 wenzelm@20437  574 subsection {* Strings of symbols *}  wenzelm@20437  575 wenzelm@34925  576 text {* A \emph{symbol} constitutes the smallest textual unit in  wenzelm@34925  577  Isabelle --- raw ML characters are normally not encountered at all!  wenzelm@34925  578  Isabelle strings consist of a sequence of symbols, represented as a  wenzelm@34925  579  packed string or an exploded list of strings. Each symbol is in  wenzelm@34925  580  itself a small string, which has either one of the following forms:  wenzelm@20437  581 wenzelm@20451  582  \begin{enumerate}  wenzelm@20437  583 wenzelm@37533  584  \item a single ASCII character @{text "c"}'', for example  wenzelm@37533  585  \verb,a,'',  wenzelm@37533  586 wenzelm@37533  587  \item a codepoint according to UTF8 (non-ASCII byte sequence),  wenzelm@20437  588 wenzelm@20488  589  \item a regular symbol \verb,\,\verb,<,@{text "ident"}\verb,>,'',  wenzelm@20476  590  for example \verb,\,\verb,,'',  wenzelm@20437  591 wenzelm@20488  592  \item a control symbol \verb,\,\verb,<^,@{text "ident"}\verb,>,'',  wenzelm@20476  593  for example \verb,\,\verb,<^bold>,'',  wenzelm@20437  594 wenzelm@20488  595  \item a raw symbol \verb,\,\verb,<^raw:,@{text text}\verb,>,''  wenzelm@34925  596  where @{text text} consists of printable characters excluding  wenzelm@20476  597  \verb,.,'' and \verb,>,'', for example  wenzelm@20476  598  \verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',  wenzelm@20437  599 wenzelm@20488  600  \item a numbered raw control symbol \verb,\,\verb,<^raw,@{text  wenzelm@20476  601  n}\verb,>, where @{text n} consists of digits, for example  wenzelm@20451  602  \verb,\,\verb,<^raw42>,''.  wenzelm@20437  603 wenzelm@20451  604  \end{enumerate}  wenzelm@20437  605 wenzelm@20476  606  \noindent The @{text "ident"} syntax for symbol names is @{text  wenzelm@20476  607  "letter (letter | digit)\<^sup>*"}, where @{text "letter =  wenzelm@20476  608  A..Za..z"} and @{text "digit = 0..9"}. There are infinitely many  wenzelm@20476  609  regular symbols and control symbols, but a fixed collection of  wenzelm@20476  610  standard symbols is treated specifically. For example,  wenzelm@20488  611  \verb,\,\verb,,'' is classified as a letter, which means it  wenzelm@20488  612  may occur within regular Isabelle identifiers.  wenzelm@20437  613 wenzelm@37533  614  The character set underlying Isabelle symbols is 7-bit ASCII, but  wenzelm@37533  615  8-bit character sequences are passed-through unchanged. Unicode/UCS  wenzelm@37533  616  data in UTF-8 encoding is processed in a non-strict fashion, such  wenzelm@37533  617  that well-formed code sequences are recognized  wenzelm@37533  618  accordingly.\footnote{Note that ISO-Latin-1 differs from UTF-8 only  wenzelm@37533  619  in some special punctuation characters that even have replacements  wenzelm@37533  620  within the standard collection of Isabelle symbols. Text consisting  wenzelm@37533  621  of ASCII plus accented letters can be processed in either encoding.}  wenzelm@37533  622  Unicode provides its own collection of mathematical symbols, but  wenzelm@37533  623  within the core Isabelle/ML world there is no link to the standard  wenzelm@37533  624  collection of Isabelle regular symbols.  wenzelm@20476  625 wenzelm@20476  626  \medskip Output of Isabelle symbols depends on the print mode  wenzelm@29758  627  (\secref{print-mode}). For example, the standard {\LaTeX} setup of  wenzelm@29758  628  the Isabelle document preparation system would present  wenzelm@20451  629  \verb,\,\verb,,'' as @{text "\"}, and  wenzelm@20451  630  \verb,\,\verb,<^bold>,\verb,\,\verb,,'' as @{text  wenzelm@34925  631  "\<^bold>\"}. On-screen rendering usually works by mapping a finite  wenzelm@34925  632  subset of Isabelle symbols to suitable Unicode characters.  wenzelm@20451  633 *}  wenzelm@20437  634 wenzelm@20437  635 text %mlref {*  wenzelm@20437  636  \begin{mldecls}  wenzelm@34921  637  @{index_ML_type "Symbol.symbol": string} \\  wenzelm@20437  638  @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\  wenzelm@20437  639  @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\  wenzelm@20437  640  @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\  wenzelm@20437  641  @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\  wenzelm@20547  642  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\  wenzelm@20547  643  \end{mldecls}  wenzelm@20547  644  \begin{mldecls}  wenzelm@20437  645  @{index_ML_type "Symbol.sym"} \\  wenzelm@20437  646  @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\  wenzelm@20437  647  \end{mldecls}  wenzelm@20437  648 wenzelm@20437  649  \begin{description}  wenzelm@20437  650 wenzelm@20488  651  \item @{ML_type "Symbol.symbol"} represents individual Isabelle  wenzelm@34921  652  symbols.  wenzelm@20437  653 wenzelm@20476  654  \item @{ML "Symbol.explode"}~@{text "str"} produces a symbol list  wenzelm@39821  655  from the packed form. This function supersedes @{ML  wenzelm@20476  656  "String.explode"} for virtually all purposes of manipulating text in  wenzelm@34925  657  Isabelle!\footnote{The runtime overhead for exploded strings is  wenzelm@34925  658  mainly that of the list structure: individual symbols that happen to  wenzelm@39821  659  be a singleton string do not require extra memory in Poly/ML.}  wenzelm@20437  660 wenzelm@20437  661  \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML  wenzelm@20476  662  "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify standard  wenzelm@20476  663  symbols according to fixed syntactic conventions of Isabelle, cf.\  wenzelm@20476  664  \cite{isabelle-isar-ref}.  wenzelm@20437  665 wenzelm@20437  666  \item @{ML_type "Symbol.sym"} is a concrete datatype that represents  wenzelm@20488  667  the different kinds of symbols explicitly, with constructors @{ML  wenzelm@37533  668  "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.UTF8"}, @{ML  wenzelm@37533  669  "Symbol.Ctrl"}, @{ML "Symbol.Raw"}.  wenzelm@20437  670 wenzelm@20437  671  \item @{ML "Symbol.decode"} converts the string representation of a  wenzelm@20451  672  symbol into the datatype version.  wenzelm@20437  673 wenzelm@20437  674  \end{description}  wenzelm@34925  675 wenzelm@34925  676  \paragraph{Historical note.} In the original SML90 standard the  wenzelm@34925  677  primitive ML type @{ML_type char} did not exists, and the basic @{ML  wenzelm@34925  678  "explode: string -> string list"} operation would produce a list of  wenzelm@34925  679  singleton strings as in Isabelle/ML today. When SML97 came out,  wenzelm@34927  680  Isabelle did not adopt its slightly anachronistic 8-bit characters,  wenzelm@34927  681  but the idea of exploding a string into a list of small strings was  wenzelm@34925  682  extended to symbols'' as explained above. Thus Isabelle sources  wenzelm@34925  683  can refer to an infinite store of user-defined symbols, without  wenzelm@34925  684  having to worry about the multitude of Unicode encodings.  wenzelm@20437  685 *}  wenzelm@20437  686 wenzelm@20437  687 wenzelm@34927  688 subsection {* Basic names \label{sec:basic-name} *}  wenzelm@20476  689 wenzelm@20476  690 text {*  wenzelm@20476  691  A \emph{basic name} essentially consists of a single Isabelle  wenzelm@20476  692  identifier. There are conventions to mark separate classes of basic  wenzelm@29761  693  names, by attaching a suffix of underscores: one underscore means  wenzelm@29761  694  \emph{internal name}, two underscores means \emph{Skolem name},  wenzelm@29761  695  three underscores means \emph{internal Skolem name}.  wenzelm@20476  696 wenzelm@20476  697  For example, the basic name @{text "foo"} has the internal version  wenzelm@20476  698  @{text "foo_"}, with Skolem versions @{text "foo__"} and @{text  wenzelm@20476  699  "foo___"}, respectively.  wenzelm@20476  700 wenzelm@20488  701  These special versions provide copies of the basic name space, apart  wenzelm@20488  702  from anything that normally appears in the user text. For example,  wenzelm@20488  703  system generated variables in Isar proof contexts are usually marked  wenzelm@34926  704  as internal, which prevents mysterious names like @{text "xaa"} to  wenzelm@34926  705  appear in human-readable text.  wenzelm@20476  706 wenzelm@20488  707  \medskip Manipulating binding scopes often requires on-the-fly  wenzelm@20488  708  renamings. A \emph{name context} contains a collection of already  wenzelm@20488  709  used names. The @{text "declare"} operation adds names to the  wenzelm@20488  710  context.  wenzelm@20476  711 wenzelm@20488  712  The @{text "invents"} operation derives a number of fresh names from  wenzelm@20488  713  a given starting point. For example, the first three names derived  wenzelm@20488  714  from @{text "a"} are @{text "a"}, @{text "b"}, @{text "c"}.  wenzelm@20476  715 wenzelm@20476  716  The @{text "variants"} operation produces fresh names by  wenzelm@20488  717  incrementing tentative names as base-26 numbers (with digits @{text  wenzelm@20488  718  "a..z"}) until all clashes are resolved. For example, name @{text  wenzelm@20488  719  "foo"} results in variants @{text "fooa"}, @{text "foob"}, @{text  wenzelm@20488  720  "fooc"}, \dots, @{text "fooaa"}, @{text "fooab"} etc.; each renaming  wenzelm@20488  721  step picks the next unused variant from this sequence.  wenzelm@20476  722 *}  wenzelm@20476  723 wenzelm@20476  724 text %mlref {*  wenzelm@20476  725  \begin{mldecls}  wenzelm@20476  726  @{index_ML Name.internal: "string -> string"} \\  wenzelm@20547  727  @{index_ML Name.skolem: "string -> string"} \\  wenzelm@20547  728  \end{mldecls}  wenzelm@20547  729  \begin{mldecls}  wenzelm@20476  730  @{index_ML_type Name.context} \\  wenzelm@20476  731  @{index_ML Name.context: Name.context} \\  wenzelm@20476  732  @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\  wenzelm@20476  733  @{index_ML Name.invents: "Name.context -> string -> int -> string list"} \\  wenzelm@20476  734  @{index_ML Name.variants: "string list -> Name.context -> string list * Name.context"} \\  wenzelm@20476  735  \end{mldecls}  wenzelm@34926  736  \begin{mldecls}  wenzelm@34926  737  @{index_ML Variable.names_of: "Proof.context -> Name.context"} \\  wenzelm@34926  738  \end{mldecls}  wenzelm@20476  739 wenzelm@20476  740  \begin{description}  wenzelm@20476  741 wenzelm@20476  742  \item @{ML Name.internal}~@{text "name"} produces an internal name  wenzelm@20476  743  by adding one underscore.  wenzelm@20476  744 wenzelm@20476  745  \item @{ML Name.skolem}~@{text "name"} produces a Skolem name by  wenzelm@20476  746  adding two underscores.  wenzelm@20476  747 wenzelm@20476  748  \item @{ML_type Name.context} represents the context of already used  wenzelm@20476  749  names; the initial value is @{ML "Name.context"}.  wenzelm@20476  750 wenzelm@20488  751  \item @{ML Name.declare}~@{text "name"} enters a used name into the  wenzelm@20488  752  context.  wenzelm@20437  753 wenzelm@20488  754  \item @{ML Name.invents}~@{text "context name n"} produces @{text  wenzelm@20488  755  "n"} fresh names derived from @{text "name"}.  wenzelm@20488  756 wenzelm@20488  757  \item @{ML Name.variants}~@{text "names context"} produces fresh  wenzelm@29761  758  variants of @{text "names"}; the result is entered into the context.  wenzelm@20476  759 wenzelm@34926  760  \item @{ML Variable.names_of}~@{text "ctxt"} retrieves the context  wenzelm@34926  761  of declared type and term variable names. Projecting a proof  wenzelm@34926  762  context down to a primitive name context is occasionally useful when  wenzelm@34926  763  invoking lower-level operations. Regular management of fresh  wenzelm@34926  764  variables'' is done by suitable operations of structure @{ML_struct  wenzelm@34926  765  Variable}, which is also able to provide an official status of  wenzelm@34926  766  locally fixed variable'' within the logical environment (cf.\  wenzelm@34926  767  \secref{sec:variables}).  wenzelm@34926  768 wenzelm@20476  769  \end{description}  wenzelm@20476  770 *}  wenzelm@20476  771 wenzelm@20476  772 wenzelm@34927  773 subsection {* Indexed names \label{sec:indexname} *}  wenzelm@20476  774 wenzelm@20476  775 text {*  wenzelm@20476  776  An \emph{indexed name} (or @{text "indexname"}) is a pair of a basic  wenzelm@20488  777  name and a natural number. This representation allows efficient  wenzelm@20488  778  renaming by incrementing the second component only. The canonical  wenzelm@20488  779  way to rename two collections of indexnames apart from each other is  wenzelm@20488  780  this: determine the maximum index @{text "maxidx"} of the first  wenzelm@20488  781  collection, then increment all indexes of the second collection by  wenzelm@20488  782  @{text "maxidx + 1"}; the maximum index of an empty collection is  wenzelm@20488  783  @{text "-1"}.  wenzelm@20476  784 wenzelm@34927  785  Occasionally, basic names are injected into the same pair type of  wenzelm@34927  786  indexed names: then @{text "(x, -1)"} is used to encode the basic  wenzelm@34927  787  name @{text "x"}.  wenzelm@20488  788 wenzelm@20488  789  \medskip Isabelle syntax observes the following rules for  wenzelm@20488  790  representing an indexname @{text "(x, i)"} as a packed string:  wenzelm@20476  791 wenzelm@20476  792  \begin{itemize}  wenzelm@20476  793 wenzelm@20479  794  \item @{text "?x"} if @{text "x"} does not end with a digit and @{text "i = 0"},  wenzelm@20476  795 wenzelm@20476  796  \item @{text "?xi"} if @{text "x"} does not end with a digit,  wenzelm@20476  797 wenzelm@20488  798  \item @{text "?x.i"} otherwise.  wenzelm@20476  799 wenzelm@20476  800  \end{itemize}  wenzelm@20470  801 wenzelm@34927  802  Indexnames may acquire large index numbers after several maxidx  wenzelm@34927  803  shifts have been applied. Results are usually normalized towards  wenzelm@34927  804  @{text "0"} at certain checkpoints, notably at the end of a proof.  wenzelm@34927  805  This works by producing variants of the corresponding basic name  wenzelm@34927  806  components. For example, the collection @{text "?x1, ?x7, ?x42"}  wenzelm@34927  807  becomes @{text "?x, ?xa, ?xb"}.  wenzelm@20476  808 *}  wenzelm@20476  809 wenzelm@20476  810 text %mlref {*  wenzelm@20476  811  \begin{mldecls}  wenzelm@20476  812  @{index_ML_type indexname} \\  wenzelm@20476  813  \end{mldecls}  wenzelm@20476  814 wenzelm@20476  815  \begin{description}  wenzelm@20476  816 wenzelm@20476  817  \item @{ML_type indexname} represents indexed names. This is an  wenzelm@20476  818  abbreviation for @{ML_type "string * int"}. The second component is  wenzelm@20476  819  usually non-negative, except for situations where @{text "(x, -1)"}  wenzelm@34926  820  is used to inject basic names into this type. Other negative  wenzelm@34926  821  indexes should not be used.  wenzelm@20476  822 wenzelm@20476  823  \end{description}  wenzelm@20476  824 *}  wenzelm@20476  825 wenzelm@20476  826 wenzelm@34927  827 subsection {* Long names \label{sec:long-name} *}  wenzelm@20476  828 wenzelm@34927  829 text {* A \emph{long name} consists of a sequence of non-empty name  wenzelm@34927  830  components. The packed representation uses a dot as separator, as  wenzelm@34927  831  in @{text "A.b.c"}''. The last component is called \emph{base  wenzelm@34927  832  name}, the remaining prefix is called \emph{qualifier} (which may be  wenzelm@34927  833  empty). The qualifier can be understood as the access path to the  wenzelm@34927  834  named entity while passing through some nested block-structure,  wenzelm@34927  835  although our free-form long names do not really enforce any strict  wenzelm@34927  836  discipline.  wenzelm@34927  837 wenzelm@34927  838  For example, an item named @{text "A.b.c"}'' may be understood as  wenzelm@34927  839  a local entity @{text "c"}, within a local structure @{text "b"},  wenzelm@34927  840  within a global structure @{text "A"}. In practice, long names  wenzelm@34927  841  usually represent 1--3 levels of qualification. User ML code should  wenzelm@34927  842  not make any assumptions about the particular structure of long  wenzelm@34927  843  names!  wenzelm@20437  844 wenzelm@20476  845  The empty name is commonly used as an indication of unnamed  wenzelm@34927  846  entities, or entities that are not entered into the corresponding  wenzelm@34927  847  name space, whenever this makes any sense. The basic operations on  wenzelm@34927  848  long names map empty names again to empty names.  wenzelm@20437  849 *}  wenzelm@20437  850 wenzelm@20476  851 text %mlref {*  wenzelm@20476  852  \begin{mldecls}  wenzelm@30365  853  @{index_ML Long_Name.base_name: "string -> string"} \\  wenzelm@30365  854  @{index_ML Long_Name.qualifier: "string -> string"} \\  wenzelm@30365  855  @{index_ML Long_Name.append: "string -> string -> string"} \\  wenzelm@30365  856  @{index_ML Long_Name.implode: "string list -> string"} \\  wenzelm@30365  857  @{index_ML Long_Name.explode: "string -> string list"} \\  wenzelm@20547  858  \end{mldecls}  wenzelm@34927  859 wenzelm@34927  860  \begin{description}  wenzelm@34927  861 wenzelm@34927  862  \item @{ML Long_Name.base_name}~@{text "name"} returns the base name  wenzelm@34927  863  of a long name.  wenzelm@34927  864 wenzelm@34927  865  \item @{ML Long_Name.qualifier}~@{text "name"} returns the qualifier  wenzelm@34927  866  of a long name.  wenzelm@34927  867 wenzelm@34927  868  \item @{ML Long_Name.append}~@{text "name\<^isub>1 name\<^isub>2"} appends two long  wenzelm@34927  869  names.  wenzelm@34927  870 wenzelm@34927  871  \item @{ML Long_Name.implode}~@{text "names"} and @{ML  wenzelm@34927  872  Long_Name.explode}~@{text "name"} convert between the packed string  wenzelm@34927  873  representation and the explicit list form of long names.  wenzelm@34927  874 wenzelm@34927  875  \end{description}  wenzelm@34927  876 *}  wenzelm@34927  877 wenzelm@34927  878 wenzelm@34927  879 subsection {* Name spaces \label{sec:name-space} *}  wenzelm@34927  880 wenzelm@34927  881 text {* A @{text "name space"} manages a collection of long names,  wenzelm@34927  882  together with a mapping between partially qualified external names  wenzelm@34927  883  and fully qualified internal names (in both directions). Note that  wenzelm@34927  884  the corresponding @{text "intern"} and @{text "extern"} operations  wenzelm@34927  885  are mostly used for parsing and printing only! The @{text  wenzelm@34927  886  "declare"} operation augments a name space according to the accesses  wenzelm@34927  887  determined by a given binding, and a naming policy from the context.  wenzelm@34927  888 wenzelm@34927  889  \medskip A @{text "binding"} specifies details about the prospective  wenzelm@34927  890  long name of a newly introduced formal entity. It consists of a  wenzelm@34927  891  base name, prefixes for qualification (separate ones for system  wenzelm@34927  892  infrastructure and user-space mechanisms), a slot for the original  wenzelm@34927  893  source position, and some additional flags.  wenzelm@34927  894 wenzelm@34927  895  \medskip A @{text "naming"} provides some additional details for  wenzelm@34927  896  producing a long name from a binding. Normally, the naming is  wenzelm@34927  897  implicit in the theory or proof context. The @{text "full"}  wenzelm@34927  898  operation (and its variants for different context types) produces a  wenzelm@34927  899  fully qualified internal name to be entered into a name space. The  wenzelm@34927  900  main equation of this chemical reaction'' when binding new  wenzelm@34927  901  entities in a context is as follows:  wenzelm@34927  902 wenzelm@34927  903  \smallskip  wenzelm@34927  904  \begin{tabular}{l}  wenzelm@34927  905  @{text "binding + naming \ long name + name space accesses"}  wenzelm@34927  906  \end{tabular}  wenzelm@34927  907  \smallskip  wenzelm@34927  908 wenzelm@34927  909  \medskip As a general principle, there is a separate name space for  wenzelm@34927  910  each kind of formal entity, e.g.\ fact, logical constant, type  wenzelm@34927  911  constructor, type class. It is usually clear from the occurrence in  wenzelm@34927  912  concrete syntax (or from the scope) which kind of entity a name  wenzelm@34927  913  refers to. For example, the very same name @{text "c"} may be used  wenzelm@34927  914  uniformly for a constant, type constructor, and type class.  wenzelm@34927  915 wenzelm@34927  916  There are common schemes to name derived entities systematically  wenzelm@34927  917  according to the name of the main logical entity involved, e.g.\  wenzelm@34927  918  fact @{text "c.intro"} for a canonical introduction rule related to  wenzelm@34927  919  constant @{text "c"}. This technique of mapping names from one  wenzelm@34927  920  space into another requires some care in order to avoid conflicts.  wenzelm@34927  921  In particular, theorem names derived from a type constructor or type  wenzelm@34927  922  class are better suffixed in addition to the usual qualification,  wenzelm@34927  923  e.g.\ @{text "c_type.intro"} and @{text "c_class.intro"} for  wenzelm@34927  924  theorems related to type @{text "c"} and class @{text "c"},  wenzelm@34927  925  respectively.  wenzelm@34927  926 *}  wenzelm@34927  927 wenzelm@34927  928 text %mlref {*  wenzelm@34927  929  \begin{mldecls}  wenzelm@34927  930  @{index_ML_type binding} \\  wenzelm@34927  931  @{index_ML Binding.empty: binding} \\  wenzelm@34927  932  @{index_ML Binding.name: "string -> binding"} \\  wenzelm@34927  933  @{index_ML Binding.qualify: "bool -> string -> binding -> binding"} \\  wenzelm@34927  934  @{index_ML Binding.prefix: "bool -> string -> binding -> binding"} \\  wenzelm@34927  935  @{index_ML Binding.conceal: "binding -> binding"} \\  wenzelm@34927  936  @{index_ML Binding.str_of: "binding -> string"} \\  wenzelm@34927  937  \end{mldecls}  wenzelm@20547  938  \begin{mldecls}  haftmann@33174  939  @{index_ML_type Name_Space.naming} \\  haftmann@33174  940  @{index_ML Name_Space.default_naming: Name_Space.naming} \\  haftmann@33174  941  @{index_ML Name_Space.add_path: "string -> Name_Space.naming -> Name_Space.naming"} \\  haftmann@33174  942  @{index_ML Name_Space.full_name: "Name_Space.naming -> binding -> string"} \\  wenzelm@20547  943  \end{mldecls}  wenzelm@20547  944  \begin{mldecls}  haftmann@33174  945  @{index_ML_type Name_Space.T} \\  haftmann@33174  946  @{index_ML Name_Space.empty: "string -> Name_Space.T"} \\  haftmann@33174  947  @{index_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\  haftmann@33174  948  @{index_ML Name_Space.declare: "bool -> Name_Space.naming -> binding -> Name_Space.T ->  haftmann@33174  949  string * Name_Space.T"} \\  haftmann@33174  950  @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\  haftmann@33174  951  @{index_ML Name_Space.extern: "Name_Space.T -> string -> string"} \\  wenzelm@34927  952  @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}  wenzelm@20476  953  \end{mldecls}  wenzelm@20437  954 wenzelm@20476  955  \begin{description}  wenzelm@20476  956 wenzelm@34927  957  \item @{ML_type binding} represents the abstract concept of name  wenzelm@34927  958  bindings.  wenzelm@34927  959 wenzelm@34927  960  \item @{ML Binding.empty} is the empty binding.  wenzelm@20476  961 wenzelm@34927  962  \item @{ML Binding.name}~@{text "name"} produces a binding with base  wenzelm@39832  963  name @{text "name"}. Note that this lacks proper source position  wenzelm@39832  964  information; see also the ML antiquotation @{ML_antiquotation  wenzelm@39832  965  binding}.  wenzelm@34927  966 wenzelm@34927  967  \item @{ML Binding.qualify}~@{text "mandatory name binding"}  wenzelm@34927  968  prefixes qualifier @{text "name"} to @{text "binding"}. The @{text  wenzelm@34927  969  "mandatory"} flag tells if this name component always needs to be  wenzelm@34927  970  given in name space accesses --- this is mostly @{text "false"} in  wenzelm@34927  971  practice. Note that this part of qualification is typically used in  wenzelm@34927  972  derived specification mechanisms.  wenzelm@20437  973 wenzelm@34927  974  \item @{ML Binding.prefix} is similar to @{ML Binding.qualify}, but  wenzelm@34927  975  affects the system prefix. This part of extra qualification is  wenzelm@34927  976  typically used in the infrastructure for modular specifications,  wenzelm@34927  977  notably local theory targets'' (see also \chref{ch:local-theory}).  wenzelm@20437  978 wenzelm@34927  979  \item @{ML Binding.conceal}~@{text "binding"} indicates that the  wenzelm@34927  980  binding shall refer to an entity that serves foundational purposes  wenzelm@34927  981  only. This flag helps to mark implementation details of  wenzelm@34927  982  specification mechanism etc. Other tools should not depend on the  wenzelm@34927  983  particulars of concealed entities (cf.\ @{ML  wenzelm@34927  984  Name_Space.is_concealed}).  wenzelm@34927  985 wenzelm@34927  986  \item @{ML Binding.str_of}~@{text "binding"} produces a string  wenzelm@34927  987  representation for human-readable output, together with some formal  wenzelm@34927  988  markup that might get used in GUI front-ends, for example.  wenzelm@20476  989 haftmann@33174  990  \item @{ML_type Name_Space.naming} represents the abstract concept of  wenzelm@20476  991  a naming policy.  wenzelm@20437  992 haftmann@33174  993  \item @{ML Name_Space.default_naming} is the default naming policy.  wenzelm@20476  994  In a theory context, this is usually augmented by a path prefix  wenzelm@20476  995  consisting of the theory name.  wenzelm@20476  996 haftmann@33174  997  \item @{ML Name_Space.add_path}~@{text "path naming"} augments the  wenzelm@20488  998  naming policy by extending its path component.  wenzelm@20437  999 haftmann@33174  1000  \item @{ML Name_Space.full_name}~@{text "naming binding"} turns a  wenzelm@30281  1001  name binding (usually a basic name) into the fully qualified  haftmann@29008  1002  internal name, according to the given naming policy.  wenzelm@20476  1003 haftmann@33174  1004  \item @{ML_type Name_Space.T} represents name spaces.  wenzelm@20476  1005 haftmann@33174  1006  \item @{ML Name_Space.empty}~@{text "kind"} and @{ML Name_Space.merge}~@{text  wenzelm@20488  1007  "(space\<^isub>1, space\<^isub>2)"} are the canonical operations for  wenzelm@20488  1008  maintaining name spaces according to theory data management  haftmann@33174  1009  (\secref{sec:context-data}); @{text "kind"} is a formal comment  haftmann@33174  1010  to characterize the purpose of a name space.  wenzelm@20437  1011 haftmann@33174  1012  \item @{ML Name_Space.declare}~@{text "strict naming bindings  haftmann@33174  1013  space"} enters a name binding as fully qualified internal name into  haftmann@33174  1014  the name space, with external accesses determined by the naming  haftmann@33174  1015  policy.  wenzelm@20476  1016 haftmann@33174  1017  \item @{ML Name_Space.intern}~@{text "space name"} internalizes a  wenzelm@20476  1018  (partially qualified) external name.  wenzelm@20437  1019 wenzelm@20488  1020  This operation is mostly for parsing! Note that fully qualified  wenzelm@20476  1021  names stemming from declarations are produced via @{ML  haftmann@33174  1022  "Name_Space.full_name"} and @{ML "Name_Space.declare"}  haftmann@29008  1023  (or their derivatives for @{ML_type theory} and  wenzelm@20488  1024  @{ML_type Proof.context}).  wenzelm@20437  1025 haftmann@33174  1026  \item @{ML Name_Space.extern}~@{text "space name"} externalizes a  wenzelm@20476  1027  (fully qualified) internal name.  wenzelm@20476  1028 wenzelm@30281  1029  This operation is mostly for printing! User code should not rely on  wenzelm@30281  1030  the precise result too much.  wenzelm@20476  1031 wenzelm@34927  1032  \item @{ML Name_Space.is_concealed}~@{text "space name"} indicates  wenzelm@34927  1033  whether @{text "name"} refers to a strictly private entity that  wenzelm@34927  1034  other tools are supposed to ignore!  wenzelm@34927  1035 wenzelm@20476  1036  \end{description}  wenzelm@20476  1037 *}  wenzelm@30272  1038 wenzelm@39832  1039 text %mlantiq {*  wenzelm@39832  1040  \begin{matharray}{rcl}  wenzelm@39832  1041  @{ML_antiquotation_def "binding"} & : & @{text ML_antiquotation} \\  wenzelm@39832  1042  \end{matharray}  wenzelm@39832  1043 wenzelm@39832  1044  \begin{rail}  wenzelm@39832  1045  'binding' name  wenzelm@39832  1046  ;  wenzelm@39832  1047  \end{rail}  wenzelm@39832  1048 wenzelm@39832  1049  \begin{description}  wenzelm@39832  1050 wenzelm@39832  1051  \item @{text "@{binding name}"} produces a binding with base name  wenzelm@39832  1052  @{text "name"} and the source position taken from the concrete  wenzelm@39832  1053  syntax of this antiquotation. In many situations this is more  wenzelm@39832  1054  appropriate than the more basic @{ML Binding.name} function.  wenzelm@39832  1055 wenzelm@39832  1056  \end{description}  wenzelm@39832  1057 *}  wenzelm@39832  1058 wenzelm@39833  1059 text %mlex {* The following example yields the source position of some  wenzelm@39833  1060  concrete binding inlined into the text.  wenzelm@39833  1061 *}  wenzelm@39833  1062 wenzelm@39833  1063 ML {* Binding.pos_of @{binding here} *}  wenzelm@39833  1064 wenzelm@39833  1065 text {* \medskip That position can be also printed in a message as  wenzelm@39833  1066  follows. *}  wenzelm@39833  1067 wenzelm@39833  1068 ML_command {*  wenzelm@39833  1069  writeln  wenzelm@39833  1070  ("Look here" ^ Position.str_of (Binding.pos_of @{binding here}))  wenzelm@39833  1071 *}  wenzelm@39833  1072 wenzelm@39833  1073 text {* \noindent This illustrates a key virtue of formalized bindings  wenzelm@39833  1074  as opposed to raw specifications of base names: the system can use  wenzelm@39833  1075  this additional information for advanced feedback given to the user. *}  wenzelm@39833  1076 wenzelm@18537  1077 end