doc-src/IsarImplementation/Thy/prelim.thy
 author wenzelm Tue May 08 15:37:19 2007 +0200 (2007-05-08) changeset 22869 9f915d44a666 parent 22438 96e650157b1e child 24137 8d7896398147 permissions -rw-r--r--
simplified context data;
     1

     2 (* $Id$ *)

     3

     4 theory prelim imports base begin

     5

     6 chapter {* Preliminaries *}

     7

     8 section {* Contexts \label{sec:context} *}

     9

    10 text {*

    11   A logical context represents the background that is required for

    12   formulating statements and composing proofs.  It acts as a medium to

    13   produce formal content, depending on earlier material (declarations,

    14   results etc.).

    15

    16   For example, derivations within the Isabelle/Pure logic can be

    17   described as a judgment @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}, which means that a

    18   proposition @{text "\<phi>"} is derivable from hypotheses @{text "\<Gamma>"}

    19   within the theory @{text "\<Theta>"}.  There are logical reasons for

    20   keeping @{text "\<Theta>"} and @{text "\<Gamma>"} separate: theories can be

    21   liberal about supporting type constructors and schematic

    22   polymorphism of constants and axioms, while the inner calculus of

    23   @{text "\<Gamma> \<turnstile> \<phi>"} is strictly limited to Simple Type Theory (with

    24   fixed type variables in the assumptions).

    25

    26   \medskip Contexts and derivations are linked by the following key

    27   principles:

    28

    29   \begin{itemize}

    30

    31   \item Transfer: monotonicity of derivations admits results to be

    32   transferred into a \emph{larger} context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta>

    33   \<phi>"} implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>'

    34   \<supseteq> \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.

    35

    36   \item Export: discharge of hypotheses admits results to be exported

    37   into a \emph{smaller} context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"}

    38   implies @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and

    39   @{text "\<Delta> = \<Gamma>' - \<Gamma>"}.  Note that @{text "\<Theta>"} remains unchanged here,

    40   only the @{text "\<Gamma>"} part is affected.

    41

    42   \end{itemize}

    43

    44   \medskip By modeling the main characteristics of the primitive

    45   @{text "\<Theta>"} and @{text "\<Gamma>"} above, and abstracting over any

    46   particular logical content, we arrive at the fundamental notions of

    47   \emph{theory context} and \emph{proof context} in Isabelle/Isar.

    48   These implement a certain policy to manage arbitrary \emph{context

    49   data}.  There is a strongly-typed mechanism to declare new kinds of

    50   data at compile time.

    51

    52   The internal bootstrap process of Isabelle/Pure eventually reaches a

    53   stage where certain data slots provide the logical content of @{text

    54   "\<Theta>"} and @{text "\<Gamma>"} sketched above, but this does not stop there!

    55   Various additional data slots support all kinds of mechanisms that

    56   are not necessarily part of the core logic.

    57

    58   For example, there would be data for canonical introduction and

    59   elimination rules for arbitrary operators (depending on the

    60   object-logic and application), which enables users to perform

    61   standard proof steps implicitly (cf.\ the @{text "rule"} method

    62   \cite{isabelle-isar-ref}).

    63

    64   \medskip Thus Isabelle/Isar is able to bring forth more and more

    65   concepts successively.  In particular, an object-logic like

    66   Isabelle/HOL continues the Isabelle/Pure setup by adding specific

    67   components for automated reasoning (classical reasoner, tableau

    68   prover, structured induction etc.) and derived specification

    69   mechanisms (inductive predicates, recursive functions etc.).  All of

    70   this is ultimately based on the generic data management by theory

    71   and proof contexts introduced here.

    72 *}

    73

    74

    75 subsection {* Theory context \label{sec:context-theory} *}

    76

    77 text {*

    78   \glossary{Theory}{FIXME}

    79

    80   A \emph{theory} is a data container with explicit named and unique

    81   identifier.  Theories are related by a (nominal) sub-theory

    82   relation, which corresponds to the dependency graph of the original

    83   construction; each theory is derived from a certain sub-graph of

    84   ancestor theories.

    85

    86   The @{text "merge"} operation produces the least upper bound of two

    87   theories, which actually degenerates into absorption of one theory

    88   into the other (due to the nominal sub-theory relation).

    89

    90   The @{text "begin"} operation starts a new theory by importing

    91   several parent theories and entering a special @{text "draft"} mode,

    92   which is sustained until the final @{text "end"} operation.  A draft

    93   theory acts like a linear type, where updates invalidate earlier

    94   versions.  An invalidated draft is called stale''.

    95

    96   The @{text "checkpoint"} operation produces an intermediate stepping

    97   stone that will survive the next update: both the original and the

    98   changed theory remain valid and are related by the sub-theory

    99   relation.  Checkpointing essentially recovers purely functional

   100   theory values, at the expense of some extra internal bookkeeping.

   101

   102   The @{text "copy"} operation produces an auxiliary version that has

   103   the same data content, but is unrelated to the original: updates of

   104   the copy do not affect the original, neither does the sub-theory

   105   relation hold.

   106

   107   \medskip The example in \figref{fig:ex-theory} below shows a theory

   108   graph derived from @{text "Pure"}, with theory @{text "Length"}

   109   importing @{text "Nat"} and @{text "List"}.  The body of @{text

   110   "Length"} consists of a sequence of updates, working mostly on

   111   drafts.  Intermediate checkpoints may occur as well, due to the

   112   history mechanism provided by the Isar top-level, cf.\

   113   \secref{sec:isar-toplevel}.

   114

   115   \begin{figure}[htb]

   116   \begin{center}

   117   \begin{tabular}{rcccl}

   118         &            & @{text "Pure"} \\

   119         &            & @{text "\<down>"} \\

   120         &            & @{text "FOL"} \\

   121         & $\swarrow$ &              & $\searrow$ & \\

   122   @{text "Nat"} &    &              &            & @{text "List"} \\

   123         & $\searrow$ &              & $\swarrow$ \\

   124         &            & @{text "Length"} \\

   125         &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\

   126         &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\

   127         &            & $\vdots$~~ \\

   128         &            & @{text "\<bullet>"}~~ \\

   129         &            & $\vdots$~~ \\

   130         &            & @{text "\<bullet>"}~~ \\

   131         &            & $\vdots$~~ \\

   132         &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\

   133   \end{tabular}

   134   \caption{A theory definition depending on ancestors}\label{fig:ex-theory}

   135   \end{center}

   136   \end{figure}

   137

   138   \medskip There is a separate notion of \emph{theory reference} for

   139   maintaining a live link to an evolving theory context: updates on

   140   drafts are propagated automatically.  Dynamic updating stops after

   141   an explicit @{text "end"} only.

   142

   143   Derived entities may store a theory reference in order to indicate

   144   the context they belong to.  This implicitly assumes monotonic

   145   reasoning, because the referenced context may become larger without

   146   further notice.

   147 *}

   148

   149 text %mlref {*

   150   \begin{mldecls}

   151   @{index_ML_type theory} \\

   152   @{index_ML Theory.subthy: "theory * theory -> bool"} \\

   153   @{index_ML Theory.merge: "theory * theory -> theory"} \\

   154   @{index_ML Theory.checkpoint: "theory -> theory"} \\

   155   @{index_ML Theory.copy: "theory -> theory"} \\

   156   \end{mldecls}

   157   \begin{mldecls}

   158   @{index_ML_type theory_ref} \\

   159   @{index_ML Theory.self_ref: "theory -> theory_ref"} \\

   160   @{index_ML Theory.deref: "theory_ref -> theory"} \\

   161   \end{mldecls}

   162

   163   \begin{description}

   164

   165   \item @{ML_type theory} represents theory contexts.  This is

   166   essentially a linear type!  Most operations destroy the original

   167   version, which then becomes stale''.

   168

   169   \item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"}

   170   compares theories according to the inherent graph structure of the

   171   construction.  This sub-theory relation is a nominal approximation

   172   of inclusion (@{text "\<subseteq>"}) of the corresponding content.

   173

   174   \item @{ML "Theory.merge"}~@{text "(thy\<^sub>1, thy\<^sub>2)"}

   175   absorbs one theory into the other.  This fails for unrelated

   176   theories!

   177

   178   \item @{ML "Theory.checkpoint"}~@{text "thy"} produces a safe

   179   stepping stone in the linear development of @{text "thy"}.  The next

   180   update will result in two related, valid theories.

   181

   182   \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text

   183   "thy"} that holds a copy of the same data.  The result is not

   184   related to the original; the original is unchanched.

   185

   186   \item @{ML_type theory_ref} represents a sliding reference to an

   187   always valid theory; updates on the original are propagated

   188   automatically.

   189

   190   \item @{ML "Theory.self_ref"}~@{text "thy"} and @{ML

   191   "Theory.deref"}~@{text "thy_ref"} convert between @{ML_type

   192   "theory"} and @{ML_type "theory_ref"}.  As the referenced theory

   193   evolves monotonically over time, later invocations of @{ML

   194   "Theory.deref"} may refer to a larger context.

   195

   196   \end{description}

   197 *}

   198

   199

   200 subsection {* Proof context \label{sec:context-proof} *}

   201

   202 text {*

   203   \glossary{Proof context}{The static context of a structured proof,

   204   acts like a local theory'' of the current portion of Isar proof

   205   text, generalizes the idea of local hypotheses @{text "\<Gamma>"} in

   206   judgments @{text "\<Gamma> \<turnstile> \<phi>"} of natural deduction calculi.  There is a

   207   generic notion of introducing and discharging hypotheses.

   208   Arbritrary auxiliary context data may be adjoined.}

   209

   210   A proof context is a container for pure data with a back-reference

   211   to the theory it belongs to.  The @{text "init"} operation creates a

   212   proof context from a given theory.  Modifications to draft theories

   213   are propagated to the proof context as usual, but there is also an

   214   explicit @{text "transfer"} operation to force resynchronization

   215   with more substantial updates to the underlying theory.  The actual

   216   context data does not require any special bookkeeping, thanks to the

   217   lack of destructive features.

   218

   219   Entities derived in a proof context need to record inherent logical

   220   requirements explicitly, since there is no separate context

   221   identification as for theories.  For example, hypotheses used in

   222   primitive derivations (cf.\ \secref{sec:thms}) are recorded

   223   separately within the sequent @{text "\<Gamma> \<turnstile> \<phi>"}, just to make double

   224   sure.  Results could still leak into an alien proof context do to

   225   programming errors, but Isabelle/Isar includes some extra validity

   226   checks in critical positions, notably at the end of a sub-proof.

   227

   228   Proof contexts may be manipulated arbitrarily, although the common

   229   discipline is to follow block structure as a mental model: a given

   230   context is extended consecutively, and results are exported back

   231   into the original context.  Note that the Isar proof states model

   232   block-structured reasoning explicitly, using a stack of proof

   233   contexts internally, cf.\ \secref{sec:isar-proof-state}.

   234 *}

   235

   236 text %mlref {*

   237   \begin{mldecls}

   238   @{index_ML_type Proof.context} \\

   239   @{index_ML ProofContext.init: "theory -> Proof.context"} \\

   240   @{index_ML ProofContext.theory_of: "Proof.context -> theory"} \\

   241   @{index_ML ProofContext.transfer: "theory -> Proof.context -> Proof.context"} \\

   242   \end{mldecls}

   243

   244   \begin{description}

   245

   246   \item @{ML_type Proof.context} represents proof contexts.  Elements

   247   of this type are essentially pure values, with a sliding reference

   248   to the background theory.

   249

   250   \item @{ML ProofContext.init}~@{text "thy"} produces a proof context

   251   derived from @{text "thy"}, initializing all data.

   252

   253   \item @{ML ProofContext.theory_of}~@{text "ctxt"} selects the

   254   background theory from @{text "ctxt"}, dereferencing its internal

   255   @{ML_type theory_ref}.

   256

   257   \item @{ML ProofContext.transfer}~@{text "thy ctxt"} promotes the

   258   background theory of @{text "ctxt"} to the super theory @{text

   259   "thy"}.

   260

   261   \end{description}

   262 *}

   263

   264

   265 subsection {* Generic contexts \label{sec:generic-context} *}

   266

   267 text {*

   268   A generic context is the disjoint sum of either a theory or proof

   269   context.  Occasionally, this enables uniform treatment of generic

   270   context data, typically extra-logical information.  Operations on

   271   generic contexts include the usual injections, partial selections,

   272   and combinators for lifting operations on either component of the

   273   disjoint sum.

   274

   275   Moreover, there are total operations @{text "theory_of"} and @{text

   276   "proof_of"} to convert a generic context into either kind: a theory

   277   can always be selected from the sum, while a proof context might

   278   have to be constructed by an ad-hoc @{text "init"} operation.

   279 *}

   280

   281 text %mlref {*

   282   \begin{mldecls}

   283   @{index_ML_type Context.generic} \\

   284   @{index_ML Context.theory_of: "Context.generic -> theory"} \\

   285   @{index_ML Context.proof_of: "Context.generic -> Proof.context"} \\

   286   \end{mldecls}

   287

   288   \begin{description}

   289

   290   \item @{ML_type Context.generic} is the direct sum of @{ML_type

   291   "theory"} and @{ML_type "Proof.context"}, with the datatype

   292   constructors @{ML "Context.Theory"} and @{ML "Context.Proof"}.

   293

   294   \item @{ML Context.theory_of}~@{text "context"} always produces a

   295   theory from the generic @{text "context"}, using @{ML

   296   "ProofContext.theory_of"} as required.

   297

   298   \item @{ML Context.proof_of}~@{text "context"} always produces a

   299   proof context from the generic @{text "context"}, using @{ML

   300   "ProofContext.init"} as required (note that this re-initializes the

   301   context data with each invocation).

   302

   303   \end{description}

   304 *}

   305

   306

   307 subsection {* Context data \label{sec:context-data} *}

   308

   309 text {*

   310   The main purpose of theory and proof contexts is to manage arbitrary

   311   data.  New data types can be declared incrementally at compile time.

   312   There are separate declaration mechanisms for any of the three kinds

   313   of contexts: theory, proof, generic.

   314

   315   \paragraph{Theory data} may refer to destructive entities, which are

   316   maintained in direct correspondence to the linear evolution of

   317   theory values, including explicit copies.\footnote{Most existing

   318   instances of destructive theory data are merely historical relics

   319   (e.g.\ the destructive theorem storage, and destructive hints for

   320   the Simplifier and Classical rules).}  A theory data declaration

   321   needs to implement the following SML signature:

   322

   323   \medskip

   324   \begin{tabular}{ll}

   325   @{text "\<type> T"} & representing type \\

   326   @{text "\<val> empty: T"} & empty default value \\

   327   @{text "\<val> copy: T \<rightarrow> T"} & refresh impure data \\

   328   @{text "\<val> extend: T \<rightarrow> T"} & re-initialize on import \\

   329   @{text "\<val> merge: T \<times> T \<rightarrow> T"} & join on import \\

   330   \end{tabular}

   331   \medskip

   332

   333   \noindent The @{text "empty"} value acts as initial default for

   334   \emph{any} theory that does not declare actual data content; @{text

   335   "copy"} maintains persistent integrity for impure data, it is just

   336   the identity for pure values; @{text "extend"} is acts like a

   337   unitary version of @{text "merge"}, both operations should also

   338   include the functionality of @{text "copy"} for impure data.

   339

   340   \paragraph{Proof context data} is purely functional.  A declaration

   341   needs to implement the following SML signature:

   342

   343   \medskip

   344   \begin{tabular}{ll}

   345   @{text "\<type> T"} & representing type \\

   346   @{text "\<val> init: theory \<rightarrow> T"} & produce initial value \\

   347   \end{tabular}

   348   \medskip

   349

   350   \noindent The @{text "init"} operation is supposed to produce a pure

   351   value from the given background theory.

   352

   353   \paragraph{Generic data} provides a hybrid interface for both theory

   354   and proof data.  The declaration is essentially the same as for

   355   (pure) theory data, without @{text "copy"}.  The @{text "init"}

   356   operation for proof contexts merely selects the current data value

   357   from the background theory.

   358

   359   \bigskip A data declaration of type @{text "T"} results in the

   360   following interface:

   361

   362   \medskip

   363   \begin{tabular}{ll}

   364   @{text "init: theory \<rightarrow> theory"} \\

   365   @{text "get: context \<rightarrow> T"} \\

   366   @{text "put: T \<rightarrow> context \<rightarrow> context"} \\

   367   @{text "map: (T \<rightarrow> T) \<rightarrow> context \<rightarrow> context"} \\

   368   \end{tabular}

   369   \medskip

   370

   371   \noindent Here @{text "init"} is only applicable to impure theory

   372   data to install a fresh copy persistently (destructive update on

   373   uninitialized has no permanent effect).  The other operations provide

   374   access for the particular kind of context (theory, proof, or generic

   375   context).  Note that this is a safe interface: there is no other way

   376   to access the corresponding data slot of a context.  By keeping

   377   these operations private, a component may maintain abstract values

   378   authentically, without other components interfering.

   379 *}

   380

   381 text %mlref {*

   382   \begin{mldecls}

   383   @{index_ML_functor TheoryDataFun} \\

   384   @{index_ML_functor ProofDataFun} \\

   385   @{index_ML_functor GenericDataFun} \\

   386   \end{mldecls}

   387

   388   \begin{description}

   389

   390   \item @{ML_functor TheoryDataFun}@{text "(spec)"} declares data for

   391   type @{ML_type theory} according to the specification provided as

   392   argument structure.  The resulting structure provides data init and

   393   access operations as described above.

   394

   395   \item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous to

   396   @{ML_functor TheoryDataFun} for type @{ML_type Proof.context}.

   397

   398   \item @{ML_functor GenericDataFun}@{text "(spec)"} is analogous to

   399   @{ML_functor TheoryDataFun} for type @{ML_type Context.generic}.

   400

   401   \end{description}

   402 *}

   403

   404

   405 section {* Names *}

   406

   407 text {*

   408   In principle, a name is just a string, but there are various

   409   convention for encoding additional structure.  For example, @{text

   410   "Foo.bar.baz"}'' is considered as a qualified name consisting of

   411   three basic name components.  The individual constituents of a name

   412   may have further substructure, e.g.\ the string

   413   \verb,\,\verb,<alpha>,'' encodes as a single symbol.

   414 *}

   415

   416

   417 subsection {* Strings of symbols *}

   418

   419 text {*

   420   \glossary{Symbol}{The smallest unit of text in Isabelle, subsumes

   421   plain ASCII characters as well as an infinite collection of named

   422   symbols (for greek, math etc.).}

   423

   424   A \emph{symbol} constitutes the smallest textual unit in Isabelle

   425   --- raw characters are normally not encountered at all.  Isabelle

   426   strings consist of a sequence of symbols, represented as a packed

   427   string or a list of strings.  Each symbol is in itself a small

   428   string, which has either one of the following forms:

   429

   430   \begin{enumerate}

   431

   432   \item a single ASCII character @{text "c"}'', for example

   433   \verb,a,'',

   434

   435   \item a regular symbol \verb,\,\verb,<,@{text "ident"}\verb,>,'',

   436   for example \verb,\,\verb,<alpha>,'',

   437

   438   \item a control symbol \verb,\,\verb,<^,@{text "ident"}\verb,>,'',

   439   for example \verb,\,\verb,<^bold>,'',

   440

   441   \item a raw symbol \verb,\,\verb,<^raw:,@{text text}\verb,>,''

   442   where @{text text} constists of printable characters excluding

   443   \verb,.,'' and \verb,>,'', for example

   444   \verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',

   445

   446   \item a numbered raw control symbol \verb,\,\verb,<^raw,@{text

   447   n}\verb,>, where @{text n} consists of digits, for example

   448   \verb,\,\verb,<^raw42>,''.

   449

   450   \end{enumerate}

   451

   452   \noindent The @{text "ident"} syntax for symbol names is @{text

   453   "letter (letter | digit)\<^sup>*"}, where @{text "letter =

   454   A..Za..z"} and @{text "digit = 0..9"}.  There are infinitely many

   455   regular symbols and control symbols, but a fixed collection of

   456   standard symbols is treated specifically.  For example,

   457   \verb,\,\verb,<alpha>,'' is classified as a letter, which means it

   458   may occur within regular Isabelle identifiers.

   459

   460   Since the character set underlying Isabelle symbols is 7-bit ASCII

   461   and 8-bit characters are passed through transparently, Isabelle may

   462   also process Unicode/UCS data in UTF-8 encoding.  Unicode provides

   463   its own collection of mathematical symbols, but there is no built-in

   464   link to the standard collection of Isabelle.

   465

   466   \medskip Output of Isabelle symbols depends on the print mode

   467   (\secref{FIXME}).  For example, the standard {\LaTeX} setup of the

   468   Isabelle document preparation system would present

   469   \verb,\,\verb,<alpha>,'' as @{text "\<alpha>"}, and

   470   \verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text

   471   "\<^bold>\<alpha>"}.

   472 *}

   473

   474 text %mlref {*

   475   \begin{mldecls}

   476   @{index_ML_type "Symbol.symbol"} \\

   477   @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\

   478   @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\

   479   @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\

   480   @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\

   481   @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\

   482   \end{mldecls}

   483   \begin{mldecls}

   484   @{index_ML_type "Symbol.sym"} \\

   485   @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\

   486   \end{mldecls}

   487

   488   \begin{description}

   489

   490   \item @{ML_type "Symbol.symbol"} represents individual Isabelle

   491   symbols; this is an alias for @{ML_type "string"}.

   492

   493   \item @{ML "Symbol.explode"}~@{text "str"} produces a symbol list

   494   from the packed form.  This function supercedes @{ML

   495   "String.explode"} for virtually all purposes of manipulating text in

   496   Isabelle!

   497

   498   \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML

   499   "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify standard

   500   symbols according to fixed syntactic conventions of Isabelle, cf.\

   501   \cite{isabelle-isar-ref}.

   502

   503   \item @{ML_type "Symbol.sym"} is a concrete datatype that represents

   504   the different kinds of symbols explicitly, with constructors @{ML

   505   "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, @{ML

   506   "Symbol.Raw"}.

   507

   508   \item @{ML "Symbol.decode"} converts the string representation of a

   509   symbol into the datatype version.

   510

   511   \end{description}

   512 *}

   513

   514

   515 subsection {* Basic names \label{sec:basic-names} *}

   516

   517 text {*

   518   A \emph{basic name} essentially consists of a single Isabelle

   519   identifier.  There are conventions to mark separate classes of basic

   520   names, by attaching a suffix of underscores (@{text "_"}): one

   521   underscore means \emph{internal name}, two underscores means

   522   \emph{Skolem name}, three underscores means \emph{internal Skolem

   523   name}.

   524

   525   For example, the basic name @{text "foo"} has the internal version

   526   @{text "foo_"}, with Skolem versions @{text "foo__"} and @{text

   527   "foo___"}, respectively.

   528

   529   These special versions provide copies of the basic name space, apart

   530   from anything that normally appears in the user text.  For example,

   531   system generated variables in Isar proof contexts are usually marked

   532   as internal, which prevents mysterious name references like @{text

   533   "xaa"} to appear in the text.

   534

   535   \medskip Manipulating binding scopes often requires on-the-fly

   536   renamings.  A \emph{name context} contains a collection of already

   537   used names.  The @{text "declare"} operation adds names to the

   538   context.

   539

   540   The @{text "invents"} operation derives a number of fresh names from

   541   a given starting point.  For example, the first three names derived

   542   from @{text "a"} are @{text "a"}, @{text "b"}, @{text "c"}.

   543

   544   The @{text "variants"} operation produces fresh names by

   545   incrementing tentative names as base-26 numbers (with digits @{text

   546   "a..z"}) until all clashes are resolved.  For example, name @{text

   547   "foo"} results in variants @{text "fooa"}, @{text "foob"}, @{text

   548   "fooc"}, \dots, @{text "fooaa"}, @{text "fooab"} etc.; each renaming

   549   step picks the next unused variant from this sequence.

   550 *}

   551

   552 text %mlref {*

   553   \begin{mldecls}

   554   @{index_ML Name.internal: "string -> string"} \\

   555   @{index_ML Name.skolem: "string -> string"} \\

   556   \end{mldecls}

   557   \begin{mldecls}

   558   @{index_ML_type Name.context} \\

   559   @{index_ML Name.context: Name.context} \\

   560   @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\

   561   @{index_ML Name.invents: "Name.context -> string -> int -> string list"} \\

   562   @{index_ML Name.variants: "string list -> Name.context -> string list * Name.context"} \\

   563   \end{mldecls}

   564

   565   \begin{description}

   566

   567   \item @{ML Name.internal}~@{text "name"} produces an internal name

   568   by adding one underscore.

   569

   570   \item @{ML Name.skolem}~@{text "name"} produces a Skolem name by

   571   adding two underscores.

   572

   573   \item @{ML_type Name.context} represents the context of already used

   574   names; the initial value is @{ML "Name.context"}.

   575

   576   \item @{ML Name.declare}~@{text "name"} enters a used name into the

   577   context.

   578

   579   \item @{ML Name.invents}~@{text "context name n"} produces @{text

   580   "n"} fresh names derived from @{text "name"}.

   581

   582   \item @{ML Name.variants}~@{text "names context"} produces fresh

   583   varians of @{text "names"}; the result is entered into the context.

   584

   585   \end{description}

   586 *}

   587

   588

   589 subsection {* Indexed names *}

   590

   591 text {*

   592   An \emph{indexed name} (or @{text "indexname"}) is a pair of a basic

   593   name and a natural number.  This representation allows efficient

   594   renaming by incrementing the second component only.  The canonical

   595   way to rename two collections of indexnames apart from each other is

   596   this: determine the maximum index @{text "maxidx"} of the first

   597   collection, then increment all indexes of the second collection by

   598   @{text "maxidx + 1"}; the maximum index of an empty collection is

   599   @{text "-1"}.

   600

   601   Occasionally, basic names and indexed names are injected into the

   602   same pair type: the (improper) indexname @{text "(x, -1)"} is used

   603   to encode basic names.

   604

   605   \medskip Isabelle syntax observes the following rules for

   606   representing an indexname @{text "(x, i)"} as a packed string:

   607

   608   \begin{itemize}

   609

   610   \item @{text "?x"} if @{text "x"} does not end with a digit and @{text "i = 0"},

   611

   612   \item @{text "?xi"} if @{text "x"} does not end with a digit,

   613

   614   \item @{text "?x.i"} otherwise.

   615

   616   \end{itemize}

   617

   618   Indexnames may acquire large index numbers over time.  Results are

   619   normalized towards @{text "0"} at certain checkpoints, notably at

   620   the end of a proof.  This works by producing variants of the

   621   corresponding basic name components.  For example, the collection

   622   @{text "?x1, ?x7, ?x42"} becomes @{text "?x, ?xa, ?xb"}.

   623 *}

   624

   625 text %mlref {*

   626   \begin{mldecls}

   627   @{index_ML_type indexname} \\

   628   \end{mldecls}

   629

   630   \begin{description}

   631

   632   \item @{ML_type indexname} represents indexed names.  This is an

   633   abbreviation for @{ML_type "string * int"}.  The second component is

   634   usually non-negative, except for situations where @{text "(x, -1)"}

   635   is used to embed basic names into this type.

   636

   637   \end{description}

   638 *}

   639

   640

   641 subsection {* Qualified names and name spaces *}

   642

   643 text {*

   644   A \emph{qualified name} consists of a non-empty sequence of basic

   645   name components.  The packed representation uses a dot as separator,

   646   as in @{text "A.b.c"}''.  The last component is called \emph{base}

   647   name, the remaining prefix \emph{qualifier} (which may be empty).

   648   The idea of qualified names is to encode nested structures by

   649   recording the access paths as qualifiers.  For example, an item

   650   named @{text "A.b.c"}'' may be understood as a local entity @{text

   651   "c"}, within a local structure @{text "b"}, within a global

   652   structure @{text "A"}.  Typically, name space hierarchies consist of

   653   1--2 levels of qualification, but this need not be always so.

   654

   655   The empty name is commonly used as an indication of unnamed

   656   entities, whenever this makes any sense.  The basic operations on

   657   qualified names are smart enough to pass through such improper names

   658   unchanged.

   659

   660   \medskip A @{text "naming"} policy tells how to turn a name

   661   specification into a fully qualified internal name (by the @{text

   662   "full"} operation), and how fully qualified names may be accessed

   663   externally.  For example, the default naming policy is to prefix an

   664   implicit path: @{text "full x"} produces @{text "path.x"}, and the

   665   standard accesses for @{text "path.x"} include both @{text "x"} and

   666   @{text "path.x"}.  Normally, the naming is implicit in the theory or

   667   proof context; there are separate versions of the corresponding.

   668

   669   \medskip A @{text "name space"} manages a collection of fully

   670   internalized names, together with a mapping between external names

   671   and internal names (in both directions).  The corresponding @{text

   672   "intern"} and @{text "extern"} operations are mostly used for

   673   parsing and printing only!  The @{text "declare"} operation augments

   674   a name space according to the accesses determined by the naming

   675   policy.

   676

   677   \medskip As a general principle, there is a separate name space for

   678   each kind of formal entity, e.g.\ logical constant, type

   679   constructor, type class, theorem.  It is usually clear from the

   680   occurrence in concrete syntax (or from the scope) which kind of

   681   entity a name refers to.  For example, the very same name @{text

   682   "c"} may be used uniformly for a constant, type constructor, and

   683   type class.

   684

   685   There are common schemes to name theorems systematically, according

   686   to the name of the main logical entity involved, e.g.\ @{text

   687   "c.intro"} for a canonical theorem related to constant @{text "c"}.

   688   This technique of mapping names from one space into another requires

   689   some care in order to avoid conflicts.  In particular, theorem names

   690   derived from a type constructor or type class are better suffixed in

   691   addition to the usual qualification, e.g.\ @{text "c_type.intro"}

   692   and @{text "c_class.intro"} for theorems related to type @{text "c"}

   693   and class @{text "c"}, respectively.

   694 *}

   695

   696 text %mlref {*

   697   \begin{mldecls}

   698   @{index_ML NameSpace.base: "string -> string"} \\

   699   @{index_ML NameSpace.qualifier: "string -> string"} \\

   700   @{index_ML NameSpace.append: "string -> string -> string"} \\

   701   @{index_ML NameSpace.implode: "string list -> string"} \\

   702   @{index_ML NameSpace.explode: "string -> string list"} \\

   703   \end{mldecls}

   704   \begin{mldecls}

   705   @{index_ML_type NameSpace.naming} \\

   706   @{index_ML NameSpace.default_naming: NameSpace.naming} \\

   707   @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\

   708   @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\

   709   \end{mldecls}

   710   \begin{mldecls}

   711   @{index_ML_type NameSpace.T} \\

   712   @{index_ML NameSpace.empty: NameSpace.T} \\

   713   @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\

   714   @{index_ML NameSpace.declare: "NameSpace.naming -> string -> NameSpace.T -> NameSpace.T"} \\

   715   @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\

   716   @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\

   717   \end{mldecls}

   718

   719   \begin{description}

   720

   721   \item @{ML NameSpace.base}~@{text "name"} returns the base name of a

   722   qualified name.

   723

   724   \item @{ML NameSpace.qualifier}~@{text "name"} returns the qualifier

   725   of a qualified name.

   726

   727   \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}

   728   appends two qualified names.

   729

   730   \item @{ML NameSpace.implode}~@{text "name"} and @{ML

   731   NameSpace.explode}~@{text "names"} convert between the packed string

   732   representation and the explicit list form of qualified names.

   733

   734   \item @{ML_type NameSpace.naming} represents the abstract concept of

   735   a naming policy.

   736

   737   \item @{ML NameSpace.default_naming} is the default naming policy.

   738   In a theory context, this is usually augmented by a path prefix

   739   consisting of the theory name.

   740

   741   \item @{ML NameSpace.add_path}~@{text "path naming"} augments the

   742   naming policy by extending its path component.

   743

   744   \item @{ML NameSpace.full}@{text "naming name"} turns a name

   745   specification (usually a basic name) into the fully qualified

   746   internal version, according to the given naming policy.

   747

   748   \item @{ML_type NameSpace.T} represents name spaces.

   749

   750   \item @{ML NameSpace.empty} and @{ML NameSpace.merge}~@{text

   751   "(space\<^isub>1, space\<^isub>2)"} are the canonical operations for

   752   maintaining name spaces according to theory data management

   753   (\secref{sec:context-data}).

   754

   755   \item @{ML NameSpace.declare}~@{text "naming name space"} enters a

   756   fully qualified name into the name space, with external accesses

   757   determined by the naming policy.

   758

   759   \item @{ML NameSpace.intern}~@{text "space name"} internalizes a

   760   (partially qualified) external name.

   761

   762   This operation is mostly for parsing!  Note that fully qualified

   763   names stemming from declarations are produced via @{ML

   764   "NameSpace.full"} (or its derivatives for @{ML_type theory} and

   765   @{ML_type Proof.context}).

   766

   767   \item @{ML NameSpace.extern}~@{text "space name"} externalizes a

   768   (fully qualified) internal name.

   769

   770   This operation is mostly for printing!  Note unqualified names are

   771   produced via @{ML NameSpace.base}.

   772

   773   \end{description}

   774 *}

   775

   776 end