1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/IsarImplementation/Thy/Base.thy Thu Mar 05 02:32:46 2009 +0100
1.3 @@ -0,0 +1,6 @@
1.4 +theory Base
1.5 +imports Pure
1.6 +uses "../../antiquote_setup.ML"
1.7 +begin
1.8 +
1.9 +end
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/IsarImplementation/Thy/Integration.thy Thu Mar 05 02:32:46 2009 +0100
2.3 @@ -0,0 +1,425 @@
2.4 +theory Integration
2.5 +imports Base
2.6 +begin
2.7 +
2.8 +chapter {* System integration *}
2.9 +
2.10 +section {* Isar toplevel \label{sec:isar-toplevel} *}
2.11 +
2.12 +text {* The Isar toplevel may be considered the centeral hub of the
2.13 + Isabelle/Isar system, where all key components and sub-systems are
2.14 + integrated into a single read-eval-print loop of Isar commands. We
2.15 + shall even incorporate the existing {\ML} toplevel of the compiler
2.16 + and run-time system (cf.\ \secref{sec:ML-toplevel}).
2.17 +
2.18 + Isabelle/Isar departs from the original ``LCF system architecture''
2.19 + where {\ML} was really The Meta Language for defining theories and
2.20 + conducting proofs. Instead, {\ML} now only serves as the
2.21 + implementation language for the system (and user extensions), while
2.22 + the specific Isar toplevel supports the concepts of theory and proof
2.23 + development natively. This includes the graph structure of theories
2.24 + and the block structure of proofs, support for unlimited undo,
2.25 + facilities for tracing, debugging, timing, profiling etc.
2.26 +
2.27 + \medskip The toplevel maintains an implicit state, which is
2.28 + transformed by a sequence of transitions -- either interactively or
2.29 + in batch-mode. In interactive mode, Isar state transitions are
2.30 + encapsulated as safe transactions, such that both failure and undo
2.31 + are handled conveniently without destroying the underlying draft
2.32 + theory (cf.~\secref{sec:context-theory}). In batch mode,
2.33 + transitions operate in a linear (destructive) fashion, such that
2.34 + error conditions abort the present attempt to construct a theory or
2.35 + proof altogether.
2.36 +
2.37 + The toplevel state is a disjoint sum of empty @{text toplevel}, or
2.38 + @{text theory}, or @{text proof}. On entering the main Isar loop we
2.39 + start with an empty toplevel. A theory is commenced by giving a
2.40 + @{text \<THEORY>} header; within a theory we may issue theory
2.41 + commands such as @{text \<DEFINITION>}, or state a @{text
2.42 + \<THEOREM>} to be proven. Now we are within a proof state, with a
2.43 + rich collection of Isar proof commands for structured proof
2.44 + composition, or unstructured proof scripts. When the proof is
2.45 + concluded we get back to the theory, which is then updated by
2.46 + storing the resulting fact. Further theory declarations or theorem
2.47 + statements with proofs may follow, until we eventually conclude the
2.48 + theory development by issuing @{text \<END>}. The resulting theory
2.49 + is then stored within the theory database and we are back to the
2.50 + empty toplevel.
2.51 +
2.52 + In addition to these proper state transformations, there are also
2.53 + some diagnostic commands for peeking at the toplevel state without
2.54 + modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
2.55 + \isakeyword{print-cases}).
2.56 +*}
2.57 +
2.58 +text %mlref {*
2.59 + \begin{mldecls}
2.60 + @{index_ML_type Toplevel.state} \\
2.61 + @{index_ML Toplevel.UNDEF: "exn"} \\
2.62 + @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
2.63 + @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
2.64 + @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
2.65 + @{index_ML Toplevel.debug: "bool ref"} \\
2.66 + @{index_ML Toplevel.timing: "bool ref"} \\
2.67 + @{index_ML Toplevel.profiling: "int ref"} \\
2.68 + \end{mldecls}
2.69 +
2.70 + \begin{description}
2.71 +
2.72 + \item @{ML_type Toplevel.state} represents Isar toplevel states,
2.73 + which are normally manipulated through the concept of toplevel
2.74 + transitions only (\secref{sec:toplevel-transition}). Also note that
2.75 + a raw toplevel state is subject to the same linearity restrictions
2.76 + as a theory context (cf.~\secref{sec:context-theory}).
2.77 +
2.78 + \item @{ML Toplevel.UNDEF} is raised for undefined toplevel
2.79 + operations. Many operations work only partially for certain cases,
2.80 + since @{ML_type Toplevel.state} is a sum type.
2.81 +
2.82 + \item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty
2.83 + toplevel state.
2.84 +
2.85 + \item @{ML Toplevel.theory_of}~@{text "state"} selects the theory of
2.86 + a theory or proof (!), otherwise raises @{ML Toplevel.UNDEF}.
2.87 +
2.88 + \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
2.89 + state if available, otherwise raises @{ML Toplevel.UNDEF}.
2.90 +
2.91 + \item @{ML "set Toplevel.debug"} makes the toplevel print further
2.92 + details about internal error conditions, exceptions being raised
2.93 + etc.
2.94 +
2.95 + \item @{ML "set Toplevel.timing"} makes the toplevel print timing
2.96 + information for each Isar command being executed.
2.97 +
2.98 + \item @{ML Toplevel.profiling}~@{verbatim ":="}~@{text "n"} controls
2.99 + low-level profiling of the underlying {\ML} runtime system. For
2.100 + Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
2.101 + profiling.
2.102 +
2.103 + \end{description}
2.104 +*}
2.105 +
2.106 +
2.107 +subsection {* Toplevel transitions \label{sec:toplevel-transition} *}
2.108 +
2.109 +text {*
2.110 + An Isar toplevel transition consists of a partial function on the
2.111 + toplevel state, with additional information for diagnostics and
2.112 + error reporting: there are fields for command name, source position,
2.113 + optional source text, as well as flags for interactive-only commands
2.114 + (which issue a warning in batch-mode), printing of result state,
2.115 + etc.
2.116 +
2.117 + The operational part is represented as the sequential union of a
2.118 + list of partial functions, which are tried in turn until the first
2.119 + one succeeds. This acts like an outer case-expression for various
2.120 + alternative state transitions. For example, \isakeyword{qed} acts
2.121 + differently for a local proofs vs.\ the global ending of the main
2.122 + proof.
2.123 +
2.124 + Toplevel transitions are composed via transition transformers.
2.125 + Internally, Isar commands are put together from an empty transition
2.126 + extended by name and source position (and optional source text). It
2.127 + is then left to the individual command parser to turn the given
2.128 + concrete syntax into a suitable transition transformer that adjoins
2.129 + actual operations on a theory or proof state etc.
2.130 +*}
2.131 +
2.132 +text %mlref {*
2.133 + \begin{mldecls}
2.134 + @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
2.135 + @{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\
2.136 + @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
2.137 + Toplevel.transition -> Toplevel.transition"} \\
2.138 + @{index_ML Toplevel.theory: "(theory -> theory) ->
2.139 + Toplevel.transition -> Toplevel.transition"} \\
2.140 + @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->
2.141 + Toplevel.transition -> Toplevel.transition"} \\
2.142 + @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
2.143 + Toplevel.transition -> Toplevel.transition"} \\
2.144 + @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) ->
2.145 + Toplevel.transition -> Toplevel.transition"} \\
2.146 + @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) ->
2.147 + Toplevel.transition -> Toplevel.transition"} \\
2.148 + \end{mldecls}
2.149 +
2.150 + \begin{description}
2.151 +
2.152 + \item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which
2.153 + causes the toplevel loop to echo the result state (in interactive
2.154 + mode).
2.155 +
2.156 + \item @{ML Toplevel.no_timing}~@{text "tr"} indicates that the
2.157 + transition should never show timing information, e.g.\ because it is
2.158 + a diagnostic command.
2.159 +
2.160 + \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
2.161 + function.
2.162 +
2.163 + \item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory
2.164 + transformer.
2.165 +
2.166 + \item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global
2.167 + goal function, which turns a theory into a proof state. The theory
2.168 + may be changed before entering the proof; the generic Isar goal
2.169 + setup includes an argument that specifies how to apply the proven
2.170 + result to the theory, when the proof is finished.
2.171 +
2.172 + \item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic
2.173 + proof command, with a singleton result.
2.174 +
2.175 + \item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof
2.176 + command, with zero or more result states (represented as a lazy
2.177 + list).
2.178 +
2.179 + \item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding
2.180 + proof command, that returns the resulting theory, after storing the
2.181 + resulting facts in the context etc.
2.182 +
2.183 + \end{description}
2.184 +*}
2.185 +
2.186 +
2.187 +subsection {* Toplevel control *}
2.188 +
2.189 +text {*
2.190 + There are a few special control commands that modify the behavior
2.191 + the toplevel itself, and only make sense in interactive mode. Under
2.192 + normal circumstances, the user encounters these only implicitly as
2.193 + part of the protocol between the Isabelle/Isar system and a
2.194 + user-interface such as ProofGeneral.
2.195 +
2.196 + \begin{description}
2.197 +
2.198 + \item \isacommand{undo} follows the three-level hierarchy of empty
2.199 + toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
2.200 + previous proof context, undo after a proof reverts to the theory
2.201 + before the initial goal statement, undo of a theory command reverts
2.202 + to the previous theory value, undo of a theory header discontinues
2.203 + the current theory development and removes it from the theory
2.204 + database (\secref{sec:theory-database}).
2.205 +
2.206 + \item \isacommand{kill} aborts the current level of development:
2.207 + kill in a proof context reverts to the theory before the initial
2.208 + goal statement, kill in a theory context aborts the current theory
2.209 + development, removing it from the database.
2.210 +
2.211 + \item \isacommand{exit} drops out of the Isar toplevel into the
2.212 + underlying {\ML} toplevel (\secref{sec:ML-toplevel}). The Isar
2.213 + toplevel state is preserved and may be continued later.
2.214 +
2.215 + \item \isacommand{quit} terminates the Isabelle/Isar process without
2.216 + saving.
2.217 +
2.218 + \end{description}
2.219 +*}
2.220 +
2.221 +
2.222 +section {* ML toplevel \label{sec:ML-toplevel} *}
2.223 +
2.224 +text {*
2.225 + The {\ML} toplevel provides a read-compile-eval-print loop for {\ML}
2.226 + values, types, structures, and functors. {\ML} declarations operate
2.227 + on the global system state, which consists of the compiler
2.228 + environment plus the values of {\ML} reference variables. There is
2.229 + no clean way to undo {\ML} declarations, except for reverting to a
2.230 + previously saved state of the whole Isabelle process. {\ML} input
2.231 + is either read interactively from a TTY, or from a string (usually
2.232 + within a theory text), or from a source file (usually loaded from a
2.233 + theory).
2.234 +
2.235 + Whenever the {\ML} toplevel is active, the current Isabelle theory
2.236 + context is passed as an internal reference variable. Thus {\ML}
2.237 + code may access the theory context during compilation, it may even
2.238 + change the value of a theory being under construction --- while
2.239 + observing the usual linearity restrictions
2.240 + (cf.~\secref{sec:context-theory}).
2.241 +*}
2.242 +
2.243 +text %mlref {*
2.244 + \begin{mldecls}
2.245 + @{index_ML the_context: "unit -> theory"} \\
2.246 + @{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\
2.247 + \end{mldecls}
2.248 +
2.249 + \begin{description}
2.250 +
2.251 + \item @{ML "the_context ()"} refers to the theory context of the
2.252 + {\ML} toplevel --- at compile time! {\ML} code needs to take care
2.253 + to refer to @{ML "the_context ()"} correctly. Recall that
2.254 + evaluation of a function body is delayed until actual runtime.
2.255 + Moreover, persistent {\ML} toplevel bindings to an unfinished theory
2.256 + should be avoided: code should either project out the desired
2.257 + information immediately, or produce an explicit @{ML_type
2.258 + theory_ref} (cf.\ \secref{sec:context-theory}).
2.259 +
2.260 + \item @{ML "Context.>>"}~@{text f} applies context transformation
2.261 + @{text f} to the implicit context of the {\ML} toplevel.
2.262 +
2.263 + \end{description}
2.264 +
2.265 + It is very important to note that the above functions are really
2.266 + restricted to the compile time, even though the {\ML} compiler is
2.267 + invoked at runtime! The majority of {\ML} code uses explicit
2.268 + functional arguments of a theory or proof context instead. Thus it
2.269 + may be invoked for an arbitrary context later on, without having to
2.270 + worry about any operational details.
2.271 +
2.272 + \bigskip
2.273 +
2.274 + \begin{mldecls}
2.275 + @{index_ML Isar.main: "unit -> unit"} \\
2.276 + @{index_ML Isar.loop: "unit -> unit"} \\
2.277 + @{index_ML Isar.state: "unit -> Toplevel.state"} \\
2.278 + @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
2.279 + @{index_ML Isar.context: "unit -> Proof.context"} \\
2.280 + @{index_ML Isar.goal: "unit -> thm"} \\
2.281 + \end{mldecls}
2.282 +
2.283 + \begin{description}
2.284 +
2.285 + \item @{ML "Isar.main ()"} invokes the Isar toplevel from {\ML},
2.286 + initializing an empty toplevel state.
2.287 +
2.288 + \item @{ML "Isar.loop ()"} continues the Isar toplevel with the
2.289 + current state, after having dropped out of the Isar toplevel loop.
2.290 +
2.291 + \item @{ML "Isar.state ()"} and @{ML "Isar.exn ()"} get current
2.292 + toplevel state and error condition, respectively. This only works
2.293 + after having dropped out of the Isar toplevel loop.
2.294 +
2.295 + \item @{ML "Isar.context ()"} produces the proof context from @{ML
2.296 + "Isar.state ()"}, analogous to @{ML Context.proof_of}
2.297 + (\secref{sec:generic-context}).
2.298 +
2.299 + \item @{ML "Isar.goal ()"} picks the tactical goal from @{ML
2.300 + "Isar.state ()"}, represented as a theorem according to
2.301 + \secref{sec:tactical-goals}.
2.302 +
2.303 + \end{description}
2.304 +*}
2.305 +
2.306 +
2.307 +section {* Theory database \label{sec:theory-database} *}
2.308 +
2.309 +text {*
2.310 + The theory database maintains a collection of theories, together
2.311 + with some administrative information about their original sources,
2.312 + which are held in an external store (i.e.\ some directory within the
2.313 + regular file system).
2.314 +
2.315 + The theory database is organized as a directed acyclic graph;
2.316 + entries are referenced by theory name. Although some additional
2.317 + interfaces allow to include a directory specification as well, this
2.318 + is only a hint to the underlying theory loader. The internal theory
2.319 + name space is flat!
2.320 +
2.321 + Theory @{text A} is associated with the main theory file @{text
2.322 + A}\verb,.thy,, which needs to be accessible through the theory
2.323 + loader path. Any number of additional {\ML} source files may be
2.324 + associated with each theory, by declaring these dependencies in the
2.325 + theory header as @{text \<USES>}, and loading them consecutively
2.326 + within the theory context. The system keeps track of incoming {\ML}
2.327 + sources and associates them with the current theory. The file
2.328 + @{text A}\verb,.ML, is loaded after a theory has been concluded, in
2.329 + order to support legacy proof {\ML} proof scripts.
2.330 +
2.331 + The basic internal actions of the theory database are @{text
2.332 + "update"}, @{text "outdate"}, and @{text "remove"}:
2.333 +
2.334 + \begin{itemize}
2.335 +
2.336 + \item @{text "update A"} introduces a link of @{text "A"} with a
2.337 + @{text "theory"} value of the same name; it asserts that the theory
2.338 + sources are now consistent with that value;
2.339 +
2.340 + \item @{text "outdate A"} invalidates the link of a theory database
2.341 + entry to its sources, but retains the present theory value;
2.342 +
2.343 + \item @{text "remove A"} deletes entry @{text "A"} from the theory
2.344 + database.
2.345 +
2.346 + \end{itemize}
2.347 +
2.348 + These actions are propagated to sub- or super-graphs of a theory
2.349 + entry as expected, in order to preserve global consistency of the
2.350 + state of all loaded theories with the sources of the external store.
2.351 + This implies certain causalities between actions: @{text "update"}
2.352 + or @{text "outdate"} of an entry will @{text "outdate"} all
2.353 + descendants; @{text "remove"} will @{text "remove"} all descendants.
2.354 +
2.355 + \medskip There are separate user-level interfaces to operate on the
2.356 + theory database directly or indirectly. The primitive actions then
2.357 + just happen automatically while working with the system. In
2.358 + particular, processing a theory header @{text "\<THEORY> A
2.359 + \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensures that the
2.360 + sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"}
2.361 + is up-to-date, too. Earlier theories are reloaded as required, with
2.362 + @{text update} actions proceeding in topological order according to
2.363 + theory dependencies. There may be also a wave of implied @{text
2.364 + outdate} actions for derived theory nodes until a stable situation
2.365 + is achieved eventually.
2.366 +*}
2.367 +
2.368 +text %mlref {*
2.369 + \begin{mldecls}
2.370 + @{index_ML theory: "string -> theory"} \\
2.371 + @{index_ML use_thy: "string -> unit"} \\
2.372 + @{index_ML use_thys: "string list -> unit"} \\
2.373 + @{index_ML ThyInfo.touch_thy: "string -> unit"} \\
2.374 + @{index_ML ThyInfo.remove_thy: "string -> unit"} \\[1ex]
2.375 + @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
2.376 + @{index_ML ThyInfo.end_theory: "theory -> unit"} \\
2.377 + @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
2.378 + @{verbatim "datatype action = Update | Outdate | Remove"} \\
2.379 + @{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\
2.380 + \end{mldecls}
2.381 +
2.382 + \begin{description}
2.383 +
2.384 + \item @{ML theory}~@{text A} retrieves the theory value presently
2.385 + associated with name @{text A}. Note that the result might be
2.386 + outdated.
2.387 +
2.388 + \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
2.389 + up-to-date wrt.\ the external file store, reloading outdated
2.390 + ancestors as required.
2.391 +
2.392 + \item @{ML use_thys} is similar to @{ML use_thy}, but handles
2.393 + several theories simultaneously. Thus it acts like processing the
2.394 + import header of a theory, without performing the merge of the
2.395 + result, though.
2.396 +
2.397 + \item @{ML ThyInfo.touch_thy}~@{text A} performs and @{text outdate} action
2.398 + on theory @{text A} and all descendants.
2.399 +
2.400 + \item @{ML ThyInfo.remove_thy}~@{text A} deletes theory @{text A} and all
2.401 + descendants from the theory database.
2.402 +
2.403 + \item @{ML ThyInfo.begin_theory} is the basic operation behind a
2.404 + @{text \<THEORY>} header declaration. This is {\ML} functions is
2.405 + normally not invoked directly.
2.406 +
2.407 + \item @{ML ThyInfo.end_theory} concludes the loading of a theory
2.408 + proper and stores the result in the theory database.
2.409 +
2.410 + \item @{ML ThyInfo.register_theory}~@{text "text thy"} registers an
2.411 + existing theory value with the theory loader database. There is no
2.412 + management of associated sources.
2.413 +
2.414 + \item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text
2.415 + f} as a hook for theory database actions. The function will be
2.416 + invoked with the action and theory name being involved; thus derived
2.417 + actions may be performed in associated system components, e.g.\
2.418 + maintaining the state of an editor for the theory sources.
2.419 +
2.420 + The kind and order of actions occurring in practice depends both on
2.421 + user interactions and the internal process of resolving theory
2.422 + imports. Hooks should not rely on a particular policy here! Any
2.423 + exceptions raised by the hook are ignored.
2.424 +
2.425 + \end{description}
2.426 +*}
2.427 +
2.428 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/IsarImplementation/Thy/Isar.thy Thu Mar 05 02:32:46 2009 +0100
3.3 @@ -0,0 +1,37 @@
3.4 +theory Isar
3.5 +imports Base
3.6 +begin
3.7 +
3.8 +chapter {* Isar language elements *}
3.9 +
3.10 +text {*
3.11 + The primary Isar language consists of three main categories of
3.12 + language elements:
3.13 +
3.14 + \begin{enumerate}
3.15 +
3.16 + \item Proof commands
3.17 +
3.18 + \item Proof methods
3.19 +
3.20 + \item Attributes
3.21 +
3.22 + \end{enumerate}
3.23 +*}
3.24 +
3.25 +
3.26 +section {* Proof commands *}
3.27 +
3.28 +text FIXME
3.29 +
3.30 +
3.31 +section {* Proof methods *}
3.32 +
3.33 +text FIXME
3.34 +
3.35 +
3.36 +section {* Attributes *}
3.37 +
3.38 +text FIXME
3.39 +
3.40 +end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Thu Mar 05 02:32:46 2009 +0100
4.3 @@ -0,0 +1,909 @@
4.4 +theory Logic
4.5 +imports Base
4.6 +begin
4.7 +
4.8 +chapter {* Primitive logic \label{ch:logic} *}
4.9 +
4.10 +text {*
4.11 + The logical foundations of Isabelle/Isar are that of the Pure logic,
4.12 + which has been introduced as a Natural Deduction framework in
4.13 + \cite{paulson700}. This is essentially the same logic as ``@{text
4.14 + "\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)
4.15 + \cite{Barendregt-Geuvers:2001}, although there are some key
4.16 + differences in the specific treatment of simple types in
4.17 + Isabelle/Pure.
4.18 +
4.19 + Following type-theoretic parlance, the Pure logic consists of three
4.20 + levels of @{text "\<lambda>"}-calculus with corresponding arrows, @{text
4.21 + "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text
4.22 + "\<And>"} for universal quantification (proofs depending on terms), and
4.23 + @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).
4.24 +
4.25 + Derivations are relative to a logical theory, which declares type
4.26 + constructors, constants, and axioms. Theory declarations support
4.27 + schematic polymorphism, which is strictly speaking outside the
4.28 + logic.\footnote{This is the deeper logical reason, why the theory
4.29 + context @{text "\<Theta>"} is separate from the proof context @{text "\<Gamma>"}
4.30 + of the core calculus.}
4.31 +*}
4.32 +
4.33 +
4.34 +section {* Types \label{sec:types} *}
4.35 +
4.36 +text {*
4.37 + The language of types is an uninterpreted order-sorted first-order
4.38 + algebra; types are qualified by ordered type classes.
4.39 +
4.40 + \medskip A \emph{type class} is an abstract syntactic entity
4.41 + declared in the theory context. The \emph{subclass relation} @{text
4.42 + "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
4.43 + generating relation; the transitive closure is maintained
4.44 + internally. The resulting relation is an ordering: reflexive,
4.45 + transitive, and antisymmetric.
4.46 +
4.47 + A \emph{sort} is a list of type classes written as @{text "s =
4.48 + {c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic
4.49 + intersection. Notationally, the curly braces are omitted for
4.50 + singleton intersections, i.e.\ any class @{text "c"} may be read as
4.51 + a sort @{text "{c}"}. The ordering on type classes is extended to
4.52 + sorts according to the meaning of intersections: @{text
4.53 + "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff
4.54 + @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}. The empty intersection
4.55 + @{text "{}"} refers to the universal sort, which is the largest
4.56 + element wrt.\ the sort order. The intersections of all (finitely
4.57 + many) classes declared in the current theory are the minimal
4.58 + elements wrt.\ the sort order.
4.59 +
4.60 + \medskip A \emph{fixed type variable} is a pair of a basic name
4.61 + (starting with a @{text "'"} character) and a sort constraint, e.g.\
4.62 + @{text "('a, s)"} which is usually printed as @{text "\<alpha>\<^isub>s"}.
4.63 + A \emph{schematic type variable} is a pair of an indexname and a
4.64 + sort constraint, e.g.\ @{text "(('a, 0), s)"} which is usually
4.65 + printed as @{text "?\<alpha>\<^isub>s"}.
4.66 +
4.67 + Note that \emph{all} syntactic components contribute to the identity
4.68 + of type variables, including the sort constraint. The core logic
4.69 + handles type variables with the same name but different sorts as
4.70 + different, although some outer layers of the system make it hard to
4.71 + produce anything like this.
4.72 +
4.73 + A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
4.74 + on types declared in the theory. Type constructor application is
4.75 + written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}. For
4.76 + @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text "prop"}
4.77 + instead of @{text "()prop"}. For @{text "k = 1"} the parentheses
4.78 + are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.
4.79 + Further notation is provided for specific constructors, notably the
4.80 + right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
4.81 + \<beta>)fun"}.
4.82 +
4.83 + A \emph{type} is defined inductively over type variables and type
4.84 + constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
4.85 + (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"}.
4.86 +
4.87 + A \emph{type abbreviation} is a syntactic definition @{text
4.88 + "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over
4.89 + variables @{text "\<^vec>\<alpha>"}. Type abbreviations appear as type
4.90 + constructors in the syntax, but are expanded before entering the
4.91 + logical core.
4.92 +
4.93 + A \emph{type arity} declares the image behavior of a type
4.94 + constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,
4.95 + s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is
4.96 + of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is
4.97 + of sort @{text "s\<^isub>i"}. Arity declarations are implicitly
4.98 + completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::
4.99 + (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
4.100 +
4.101 + \medskip The sort algebra is always maintained as \emph{coregular},
4.102 + which means that type arities are consistent with the subclass
4.103 + relation: for any type constructor @{text "\<kappa>"}, and classes @{text
4.104 + "c\<^isub>1 \<subseteq> c\<^isub>2"}, and arities @{text "\<kappa> ::
4.105 + (\<^vec>s\<^isub>1)c\<^isub>1"} and @{text "\<kappa> ::
4.106 + (\<^vec>s\<^isub>2)c\<^isub>2"} holds @{text "\<^vec>s\<^isub>1 \<subseteq>
4.107 + \<^vec>s\<^isub>2"} component-wise.
4.108 +
4.109 + The key property of a coregular order-sorted algebra is that sort
4.110 + constraints can be solved in a most general fashion: for each type
4.111 + constructor @{text "\<kappa>"} and sort @{text "s"} there is a most general
4.112 + vector of argument sorts @{text "(s\<^isub>1, \<dots>, s\<^isub>k)"} such
4.113 + that a type scheme @{text "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>,
4.114 + \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is of sort @{text "s"}.
4.115 + Consequently, type unification has most general solutions (modulo
4.116 + equivalence of sorts), so type-inference produces primary types as
4.117 + expected \cite{nipkow-prehofer}.
4.118 +*}
4.119 +
4.120 +text %mlref {*
4.121 + \begin{mldecls}
4.122 + @{index_ML_type class} \\
4.123 + @{index_ML_type sort} \\
4.124 + @{index_ML_type arity} \\
4.125 + @{index_ML_type typ} \\
4.126 + @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\
4.127 + @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
4.128 + \end{mldecls}
4.129 + \begin{mldecls}
4.130 + @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
4.131 + @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
4.132 + @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
4.133 + @{index_ML Sign.add_tyabbrs_i: "
4.134 + (string * string list * typ * mixfix) list -> theory -> theory"} \\
4.135 + @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
4.136 + @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
4.137 + @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
4.138 + \end{mldecls}
4.139 +
4.140 + \begin{description}
4.141 +
4.142 + \item @{ML_type class} represents type classes; this is an alias for
4.143 + @{ML_type string}.
4.144 +
4.145 + \item @{ML_type sort} represents sorts; this is an alias for
4.146 + @{ML_type "class list"}.
4.147 +
4.148 + \item @{ML_type arity} represents type arities; this is an alias for
4.149 + triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::
4.150 + (\<^vec>s)s"} described above.
4.151 +
4.152 + \item @{ML_type typ} represents types; this is a datatype with
4.153 + constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
4.154 +
4.155 + \item @{ML map_atyps}~@{text "f \<tau>"} applies the mapping @{text "f"}
4.156 + to all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text
4.157 + "\<tau>"}.
4.158 +
4.159 + \item @{ML fold_atyps}~@{text "f \<tau>"} iterates the operation @{text
4.160 + "f"} over all occurrences of atomic types (@{ML TFree}, @{ML TVar})
4.161 + in @{text "\<tau>"}; the type structure is traversed from left to right.
4.162 +
4.163 + \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
4.164 + tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
4.165 +
4.166 + \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type
4.167 + @{text "\<tau>"} is of sort @{text "s"}.
4.168 +
4.169 + \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares a new
4.170 + type constructors @{text "\<kappa>"} with @{text "k"} arguments and
4.171 + optional mixfix syntax.
4.172 +
4.173 + \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
4.174 + defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with
4.175 + optional mixfix syntax.
4.176 +
4.177 + \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
4.178 + c\<^isub>n])"} declares a new class @{text "c"}, together with class
4.179 + relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
4.180 +
4.181 + \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
4.182 + c\<^isub>2)"} declares the class relation @{text "c\<^isub>1 \<subseteq>
4.183 + c\<^isub>2"}.
4.184 +
4.185 + \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
4.186 + the arity @{text "\<kappa> :: (\<^vec>s)s"}.
4.187 +
4.188 + \end{description}
4.189 +*}
4.190 +
4.191 +
4.192 +section {* Terms \label{sec:terms} *}
4.193 +
4.194 +text {*
4.195 + The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
4.196 + with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
4.197 + or \cite{paulson-ml2}), with the types being determined by the
4.198 + corresponding binders. In contrast, free variables and constants
4.199 + are have an explicit name and type in each occurrence.
4.200 +
4.201 + \medskip A \emph{bound variable} is a natural number @{text "b"},
4.202 + which accounts for the number of intermediate binders between the
4.203 + variable occurrence in the body and its binding position. For
4.204 + example, the de-Bruijn term @{text
4.205 + "\<lambda>\<^bsub>nat\<^esub>. \<lambda>\<^bsub>nat\<^esub>. 1 + 0"} would
4.206 + correspond to @{text
4.207 + "\<lambda>x\<^bsub>nat\<^esub>. \<lambda>y\<^bsub>nat\<^esub>. x + y"} in a named
4.208 + representation. Note that a bound variable may be represented by
4.209 + different de-Bruijn indices at different occurrences, depending on
4.210 + the nesting of abstractions.
4.211 +
4.212 + A \emph{loose variable} is a bound variable that is outside the
4.213 + scope of local binders. The types (and names) for loose variables
4.214 + can be managed as a separate context, that is maintained as a stack
4.215 + of hypothetical binders. The core logic operates on closed terms,
4.216 + without any loose variables.
4.217 +
4.218 + A \emph{fixed variable} is a pair of a basic name and a type, e.g.\
4.219 + @{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"}. A
4.220 + \emph{schematic variable} is a pair of an indexname and a type,
4.221 + e.g.\ @{text "((x, 0), \<tau>)"} which is usually printed as @{text
4.222 + "?x\<^isub>\<tau>"}.
4.223 +
4.224 + \medskip A \emph{constant} is a pair of a basic name and a type,
4.225 + e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text
4.226 + "c\<^isub>\<tau>"}. Constants are declared in the context as polymorphic
4.227 + families @{text "c :: \<sigma>"}, meaning that all substitution instances
4.228 + @{text "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.
4.229 +
4.230 + The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"}
4.231 + wrt.\ the declaration @{text "c :: \<sigma>"} is defined as the codomain of
4.232 + the matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>,
4.233 + ?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in canonical order @{text
4.234 + "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}. Within a given theory context,
4.235 + there is a one-to-one correspondence between any constant @{text
4.236 + "c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1, \<dots>,
4.237 + \<tau>\<^isub>n)"} of its type arguments. For example, with @{text "plus
4.238 + :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow>
4.239 + nat\<^esub>"} corresponds to @{text "plus(nat)"}.
4.240 +
4.241 + Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
4.242 + for type variables in @{text "\<sigma>"}. These are observed by
4.243 + type-inference as expected, but \emph{ignored} by the core logic.
4.244 + This means the primitive logic is able to reason with instances of
4.245 + polymorphic constants that the user-level type-checker would reject
4.246 + due to violation of type class restrictions.
4.247 +
4.248 + \medskip An \emph{atomic} term is either a variable or constant. A
4.249 + \emph{term} is defined inductively over atomic terms, with
4.250 + abstraction and application as follows: @{text "t = b | x\<^isub>\<tau> |
4.251 + ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.
4.252 + Parsing and printing takes care of converting between an external
4.253 + representation with named bound variables. Subsequently, we shall
4.254 + use the latter notation instead of internal de-Bruijn
4.255 + representation.
4.256 +
4.257 + The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a
4.258 + term according to the structure of atomic terms, abstractions, and
4.259 + applicatins:
4.260 + \[
4.261 + \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{}
4.262 + \qquad
4.263 + \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}}
4.264 + \qquad
4.265 + \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}}
4.266 + \]
4.267 + A \emph{well-typed term} is a term that can be typed according to these rules.
4.268 +
4.269 + Typing information can be omitted: type-inference is able to
4.270 + reconstruct the most general type of a raw term, while assigning
4.271 + most general types to all of its variables and constants.
4.272 + Type-inference depends on a context of type constraints for fixed
4.273 + variables, and declarations for polymorphic constants.
4.274 +
4.275 + The identity of atomic terms consists both of the name and the type
4.276 + component. This means that different variables @{text
4.277 + "x\<^bsub>\<tau>\<^isub>1\<^esub>"} and @{text
4.278 + "x\<^bsub>\<tau>\<^isub>2\<^esub>"} may become the same after type
4.279 + instantiation. Some outer layers of the system make it hard to
4.280 + produce variables of the same name, but different types. In
4.281 + contrast, mixed instances of polymorphic constants occur frequently.
4.282 +
4.283 + \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
4.284 + is the set of type variables occurring in @{text "t"}, but not in
4.285 + @{text "\<sigma>"}. This means that the term implicitly depends on type
4.286 + arguments that are not accounted in the result type, i.e.\ there are
4.287 + different type instances @{text "t\<vartheta> :: \<sigma>"} and @{text
4.288 + "t\<vartheta>' :: \<sigma>"} with the same type. This slightly
4.289 + pathological situation notoriously demands additional care.
4.290 +
4.291 + \medskip A \emph{term abbreviation} is a syntactic definition @{text
4.292 + "c\<^isub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"},
4.293 + without any hidden polymorphism. A term abbreviation looks like a
4.294 + constant in the syntax, but is expanded before entering the logical
4.295 + core. Abbreviations are usually reverted when printing terms, using
4.296 + @{text "t \<rightarrow> c\<^isub>\<sigma>"} as rules for higher-order rewriting.
4.297 +
4.298 + \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text
4.299 + "\<alpha>\<beta>\<eta>"}-conversion: @{text "\<alpha>"}-conversion refers to capture-free
4.300 + renaming of bound variables; @{text "\<beta>"}-conversion contracts an
4.301 + abstraction applied to an argument term, substituting the argument
4.302 + in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text
4.303 + "\<eta>"}-conversion contracts vacuous application-abstraction: @{text
4.304 + "\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable
4.305 + does not occur in @{text "f"}.
4.306 +
4.307 + Terms are normally treated modulo @{text "\<alpha>"}-conversion, which is
4.308 + implicit in the de-Bruijn representation. Names for bound variables
4.309 + in abstractions are maintained separately as (meaningless) comments,
4.310 + mostly for parsing and printing. Full @{text "\<alpha>\<beta>\<eta>"}-conversion is
4.311 + commonplace in various standard operations (\secref{sec:obj-rules})
4.312 + that are based on higher-order unification and matching.
4.313 +*}
4.314 +
4.315 +text %mlref {*
4.316 + \begin{mldecls}
4.317 + @{index_ML_type term} \\
4.318 + @{index_ML "op aconv": "term * term -> bool"} \\
4.319 + @{index_ML map_types: "(typ -> typ) -> term -> term"} \\
4.320 + @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
4.321 + @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
4.322 + @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
4.323 + \end{mldecls}
4.324 + \begin{mldecls}
4.325 + @{index_ML fastype_of: "term -> typ"} \\
4.326 + @{index_ML lambda: "term -> term -> term"} \\
4.327 + @{index_ML betapply: "term * term -> term"} \\
4.328 + @{index_ML Sign.declare_const: "Properties.T -> (binding * typ) * mixfix ->
4.329 + theory -> term * theory"} \\
4.330 + @{index_ML Sign.add_abbrev: "string -> Properties.T -> binding * term ->
4.331 + theory -> (term * term) * theory"} \\
4.332 + @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
4.333 + @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
4.334 + \end{mldecls}
4.335 +
4.336 + \begin{description}
4.337 +
4.338 + \item @{ML_type term} represents de-Bruijn terms, with comments in
4.339 + abstractions, and explicitly named free variables and constants;
4.340 + this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
4.341 + Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}.
4.342 +
4.343 + \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text
4.344 + "\<alpha>"}-equivalence of two terms. This is the basic equality relation
4.345 + on type @{ML_type term}; raw datatype equality should only be used
4.346 + for operations related to parsing or printing!
4.347 +
4.348 + \item @{ML map_types}~@{text "f t"} applies the mapping @{text
4.349 + "f"} to all types occurring in @{text "t"}.
4.350 +
4.351 + \item @{ML fold_types}~@{text "f t"} iterates the operation @{text
4.352 + "f"} over all occurrences of types in @{text "t"}; the term
4.353 + structure is traversed from left to right.
4.354 +
4.355 + \item @{ML map_aterms}~@{text "f t"} applies the mapping @{text "f"}
4.356 + to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML
4.357 + Const}) occurring in @{text "t"}.
4.358 +
4.359 + \item @{ML fold_aterms}~@{text "f t"} iterates the operation @{text
4.360 + "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML Free},
4.361 + @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is
4.362 + traversed from left to right.
4.363 +
4.364 + \item @{ML fastype_of}~@{text "t"} determines the type of a
4.365 + well-typed term. This operation is relatively slow, despite the
4.366 + omission of any sanity checks.
4.367 +
4.368 + \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
4.369 + "\<lambda>a. b"}, where occurrences of the atomic term @{text "a"} in the
4.370 + body @{text "b"} are replaced by bound variables.
4.371 +
4.372 + \item @{ML betapply}~@{text "(t, u)"} produces an application @{text
4.373 + "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
4.374 + abstraction.
4.375 +
4.376 + \item @{ML Sign.declare_const}~@{text "properties ((c, \<sigma>), mx)"}
4.377 + declares a new constant @{text "c :: \<sigma>"} with optional mixfix
4.378 + syntax.
4.379 +
4.380 + \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}
4.381 + introduces a new term abbreviation @{text "c \<equiv> t"}.
4.382 +
4.383 + \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
4.384 + Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
4.385 + convert between two representations of polymorphic constants: full
4.386 + type instance vs.\ compact type arguments form.
4.387 +
4.388 + \end{description}
4.389 +*}
4.390 +
4.391 +
4.392 +section {* Theorems \label{sec:thms} *}
4.393 +
4.394 +text {*
4.395 + A \emph{proposition} is a well-typed term of type @{text "prop"}, a
4.396 + \emph{theorem} is a proven proposition (depending on a context of
4.397 + hypotheses and the background theory). Primitive inferences include
4.398 + plain Natural Deduction rules for the primary connectives @{text
4.399 + "\<And>"} and @{text "\<Longrightarrow>"} of the framework. There is also a builtin
4.400 + notion of equality/equivalence @{text "\<equiv>"}.
4.401 +*}
4.402 +
4.403 +
4.404 +subsection {* Primitive connectives and rules \label{sec:prim-rules} *}
4.405 +
4.406 +text {*
4.407 + The theory @{text "Pure"} contains constant declarations for the
4.408 + primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of
4.409 + the logical framework, see \figref{fig:pure-connectives}. The
4.410 + derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
4.411 + defined inductively by the primitive inferences given in
4.412 + \figref{fig:prim-rules}, with the global restriction that the
4.413 + hypotheses must \emph{not} contain any schematic variables. The
4.414 + builtin equality is conceptually axiomatized as shown in
4.415 + \figref{fig:pure-equality}, although the implementation works
4.416 + directly with derived inferences.
4.417 +
4.418 + \begin{figure}[htb]
4.419 + \begin{center}
4.420 + \begin{tabular}{ll}
4.421 + @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
4.422 + @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
4.423 + @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
4.424 + \end{tabular}
4.425 + \caption{Primitive connectives of Pure}\label{fig:pure-connectives}
4.426 + \end{center}
4.427 + \end{figure}
4.428 +
4.429 + \begin{figure}[htb]
4.430 + \begin{center}
4.431 + \[
4.432 + \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}
4.433 + \qquad
4.434 + \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}
4.435 + \]
4.436 + \[
4.437 + \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}
4.438 + \qquad
4.439 + \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}
4.440 + \]
4.441 + \[
4.442 + \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
4.443 + \qquad
4.444 + \infer[@{text "(\<Longrightarrow>_elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}
4.445 + \]
4.446 + \caption{Primitive inferences of Pure}\label{fig:prim-rules}
4.447 + \end{center}
4.448 + \end{figure}
4.449 +
4.450 + \begin{figure}[htb]
4.451 + \begin{center}
4.452 + \begin{tabular}{ll}
4.453 + @{text "\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]"} & @{text "\<beta>"}-conversion \\
4.454 + @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
4.455 + @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
4.456 + @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
4.457 + @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\
4.458 + \end{tabular}
4.459 + \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
4.460 + \end{center}
4.461 + \end{figure}
4.462 +
4.463 + The introduction and elimination rules for @{text "\<And>"} and @{text
4.464 + "\<Longrightarrow>"} are analogous to formation of dependently typed @{text
4.465 + "\<lambda>"}-terms representing the underlying proof objects. Proof terms
4.466 + are irrelevant in the Pure logic, though; they cannot occur within
4.467 + propositions. The system provides a runtime option to record
4.468 + explicit proof terms for primitive inferences. Thus all three
4.469 + levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for
4.470 + terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\
4.471 + \cite{Berghofer-Nipkow:2000:TPHOL}).
4.472 +
4.473 + Observe that locally fixed parameters (as in @{text "\<And>_intro"}) need
4.474 + not be recorded in the hypotheses, because the simple syntactic
4.475 + types of Pure are always inhabitable. ``Assumptions'' @{text "x ::
4.476 + \<tau>"} for type-membership are only present as long as some @{text
4.477 + "x\<^isub>\<tau>"} occurs in the statement body.\footnote{This is the key
4.478 + difference to ``@{text "\<lambda>HOL"}'' in the PTS framework
4.479 + \cite{Barendregt-Geuvers:2001}, where hypotheses @{text "x : A"} are
4.480 + treated uniformly for propositions and types.}
4.481 +
4.482 + \medskip The axiomatization of a theory is implicitly closed by
4.483 + forming all instances of type and term variables: @{text "\<turnstile>
4.484 + A\<vartheta>"} holds for any substitution instance of an axiom
4.485 + @{text "\<turnstile> A"}. By pushing substitutions through derivations
4.486 + inductively, we also get admissible @{text "generalize"} and @{text
4.487 + "instance"} rules as shown in \figref{fig:subst-rules}.
4.488 +
4.489 + \begin{figure}[htb]
4.490 + \begin{center}
4.491 + \[
4.492 + \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}
4.493 + \quad
4.494 + \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}
4.495 + \]
4.496 + \[
4.497 + \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}
4.498 + \quad
4.499 + \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}
4.500 + \]
4.501 + \caption{Admissible substitution rules}\label{fig:subst-rules}
4.502 + \end{center}
4.503 + \end{figure}
4.504 +
4.505 + Note that @{text "instantiate"} does not require an explicit
4.506 + side-condition, because @{text "\<Gamma>"} may never contain schematic
4.507 + variables.
4.508 +
4.509 + In principle, variables could be substituted in hypotheses as well,
4.510 + but this would disrupt the monotonicity of reasoning: deriving
4.511 + @{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is
4.512 + correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:
4.513 + the result belongs to a different proof context.
4.514 +
4.515 + \medskip An \emph{oracle} is a function that produces axioms on the
4.516 + fly. Logically, this is an instance of the @{text "axiom"} rule
4.517 + (\figref{fig:prim-rules}), but there is an operational difference.
4.518 + The system always records oracle invocations within derivations of
4.519 + theorems by a unique tag.
4.520 +
4.521 + Axiomatizations should be limited to the bare minimum, typically as
4.522 + part of the initial logical basis of an object-logic formalization.
4.523 + Later on, theories are usually developed in a strictly definitional
4.524 + fashion, by stating only certain equalities over new constants.
4.525 +
4.526 + A \emph{simple definition} consists of a constant declaration @{text
4.527 + "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t
4.528 + :: \<sigma>"} is a closed term without any hidden polymorphism. The RHS
4.529 + may depend on further defined constants, but not @{text "c"} itself.
4.530 + Definitions of functions may be presented as @{text "c \<^vec>x \<equiv>
4.531 + t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}.
4.532 +
4.533 + An \emph{overloaded definition} consists of a collection of axioms
4.534 + for the same constant, with zero or one equations @{text
4.535 + "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for
4.536 + distinct variables @{text "\<^vec>\<alpha>"}). The RHS may mention
4.537 + previously defined constants as above, or arbitrary constants @{text
4.538 + "d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text
4.539 + "\<^vec>\<alpha>"}. Thus overloaded definitions essentially work by
4.540 + primitive recursion over the syntactic structure of a single type
4.541 + argument.
4.542 +*}
4.543 +
4.544 +text %mlref {*
4.545 + \begin{mldecls}
4.546 + @{index_ML_type ctyp} \\
4.547 + @{index_ML_type cterm} \\
4.548 + @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
4.549 + @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
4.550 + \end{mldecls}
4.551 + \begin{mldecls}
4.552 + @{index_ML_type thm} \\
4.553 + @{index_ML proofs: "int ref"} \\
4.554 + @{index_ML Thm.assume: "cterm -> thm"} \\
4.555 + @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
4.556 + @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
4.557 + @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
4.558 + @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
4.559 + @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
4.560 + @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
4.561 + @{index_ML Thm.axiom: "theory -> string -> thm"} \\
4.562 + @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
4.563 + -> (string * ('a -> thm)) * theory"} \\
4.564 + \end{mldecls}
4.565 + \begin{mldecls}
4.566 + @{index_ML Theory.add_axioms_i: "(binding * term) list -> theory -> theory"} \\
4.567 + @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
4.568 + @{index_ML Theory.add_defs_i: "bool -> bool -> (binding * term) list -> theory -> theory"} \\
4.569 + \end{mldecls}
4.570 +
4.571 + \begin{description}
4.572 +
4.573 + \item @{ML_type ctyp} and @{ML_type cterm} represent certified types
4.574 + and terms, respectively. These are abstract datatypes that
4.575 + guarantee that its values have passed the full well-formedness (and
4.576 + well-typedness) checks, relative to the declarations of type
4.577 + constructors, constants etc. in the theory.
4.578 +
4.579 + \item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML
4.580 + Thm.cterm_of}~@{text "thy t"} explicitly checks types and terms,
4.581 + respectively. This also involves some basic normalizations, such
4.582 + expansion of type and term abbreviations from the theory context.
4.583 +
4.584 + Re-certification is relatively slow and should be avoided in tight
4.585 + reasoning loops. There are separate operations to decompose
4.586 + certified entities (including actual theorems).
4.587 +
4.588 + \item @{ML_type thm} represents proven propositions. This is an
4.589 + abstract datatype that guarantees that its values have been
4.590 + constructed by basic principles of the @{ML_struct Thm} module.
4.591 + Every @{ML thm} value contains a sliding back-reference to the
4.592 + enclosing theory, cf.\ \secref{sec:context-theory}.
4.593 +
4.594 + \item @{ML proofs} determines the detail of proof recording within
4.595 + @{ML_type thm} values: @{ML 0} records only the names of oracles,
4.596 + @{ML 1} records oracle names and propositions, @{ML 2} additionally
4.597 + records full proof terms. Officially named theorems that contribute
4.598 + to a result are always recorded.
4.599 +
4.600 + \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
4.601 + Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
4.602 + correspond to the primitive inferences of \figref{fig:prim-rules}.
4.603 +
4.604 + \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}
4.605 + corresponds to the @{text "generalize"} rules of
4.606 + \figref{fig:subst-rules}. Here collections of type and term
4.607 + variables are generalized simultaneously, specified by the given
4.608 + basic names.
4.609 +
4.610 + \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,
4.611 + \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules
4.612 + of \figref{fig:subst-rules}. Type variables are substituted before
4.613 + term variables. Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
4.614 + refer to the instantiated versions.
4.615 +
4.616 + \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named
4.617 + axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
4.618 +
4.619 + \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named
4.620 + oracle rule, essentially generating arbitrary axioms on the fly,
4.621 + cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
4.622 +
4.623 + \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
4.624 + arbitrary propositions as axioms.
4.625 +
4.626 + \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
4.627 + \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
4.628 + for constant @{text "c\<^isub>\<tau>"}, relative to existing
4.629 + specifications for constants @{text "\<^vec>d\<^isub>\<sigma>"}.
4.630 +
4.631 + \item @{ML Theory.add_defs_i}~@{text "unchecked overloaded [(name, c
4.632 + \<^vec>x \<equiv> t), \<dots>]"} states a definitional axiom for an existing
4.633 + constant @{text "c"}. Dependencies are recorded (cf.\ @{ML
4.634 + Theory.add_deps}), unless the @{text "unchecked"} option is set.
4.635 +
4.636 + \end{description}
4.637 +*}
4.638 +
4.639 +
4.640 +subsection {* Auxiliary definitions *}
4.641 +
4.642 +text {*
4.643 + Theory @{text "Pure"} provides a few auxiliary definitions, see
4.644 + \figref{fig:pure-aux}. These special constants are normally not
4.645 + exposed to the user, but appear in internal encodings.
4.646 +
4.647 + \begin{figure}[htb]
4.648 + \begin{center}
4.649 + \begin{tabular}{ll}
4.650 + @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\
4.651 + @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex]
4.652 + @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\
4.653 + @{text "#A \<equiv> A"} \\[1ex]
4.654 + @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
4.655 + @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
4.656 + @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
4.657 + @{text "(unspecified)"} \\
4.658 + \end{tabular}
4.659 + \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
4.660 + \end{center}
4.661 + \end{figure}
4.662 +
4.663 + Derived conjunction rules include introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A &
4.664 + B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}.
4.665 + Conjunction allows to treat simultaneous assumptions and conclusions
4.666 + uniformly. For example, multiple claims are intermediately
4.667 + represented as explicit conjunction, but this is refined into
4.668 + separate sub-goals before the user continues the proof; the final
4.669 + result is projected into a list of theorems (cf.\
4.670 + \secref{sec:tactical-goals}).
4.671 +
4.672 + The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex
4.673 + propositions appear as atomic, without changing the meaning: @{text
4.674 + "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are interchangeable. See
4.675 + \secref{sec:tactical-goals} for specific operations.
4.676 +
4.677 + The @{text "term"} marker turns any well-typed term into a derivable
4.678 + proposition: @{text "\<turnstile> TERM t"} holds unconditionally. Although
4.679 + this is logically vacuous, it allows to treat terms and proofs
4.680 + uniformly, similar to a type-theoretic framework.
4.681 +
4.682 + The @{text "TYPE"} constructor is the canonical representative of
4.683 + the unspecified type @{text "\<alpha> itself"}; it essentially injects the
4.684 + language of types into that of terms. There is specific notation
4.685 + @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>
4.686 + itself\<^esub>"}.
4.687 + Although being devoid of any particular meaning, the @{text
4.688 + "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term
4.689 + language. In particular, @{text "TYPE(\<alpha>)"} may be used as formal
4.690 + argument in primitive definitions, in order to circumvent hidden
4.691 + polymorphism (cf.\ \secref{sec:terms}). For example, @{text "c
4.692 + TYPE(\<alpha>) \<equiv> A[\<alpha>]"} defines @{text "c :: \<alpha> itself \<Rightarrow> prop"} in terms of
4.693 + a proposition @{text "A"} that depends on an additional type
4.694 + argument, which is essentially a predicate on types.
4.695 +*}
4.696 +
4.697 +text %mlref {*
4.698 + \begin{mldecls}
4.699 + @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\
4.700 + @{index_ML Conjunction.elim: "thm -> thm * thm"} \\
4.701 + @{index_ML Drule.mk_term: "cterm -> thm"} \\
4.702 + @{index_ML Drule.dest_term: "thm -> cterm"} \\
4.703 + @{index_ML Logic.mk_type: "typ -> term"} \\
4.704 + @{index_ML Logic.dest_type: "term -> typ"} \\
4.705 + \end{mldecls}
4.706 +
4.707 + \begin{description}
4.708 +
4.709 + \item @{ML Conjunction.intr} derives @{text "A & B"} from @{text
4.710 + "A"} and @{text "B"}.
4.711 +
4.712 + \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}
4.713 + from @{text "A & B"}.
4.714 +
4.715 + \item @{ML Drule.mk_term} derives @{text "TERM t"}.
4.716 +
4.717 + \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text
4.718 + "TERM t"}.
4.719 +
4.720 + \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text
4.721 + "TYPE(\<tau>)"}.
4.722 +
4.723 + \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type
4.724 + @{text "\<tau>"}.
4.725 +
4.726 + \end{description}
4.727 +*}
4.728 +
4.729 +
4.730 +section {* Object-level rules \label{sec:obj-rules} *}
4.731 +
4.732 +text {*
4.733 + The primitive inferences covered so far mostly serve foundational
4.734 + purposes. User-level reasoning usually works via object-level rules
4.735 + that are represented as theorems of Pure. Composition of rules
4.736 + involves \emph{backchaining}, \emph{higher-order unification} modulo
4.737 + @{text "\<alpha>\<beta>\<eta>"}-conversion of @{text "\<lambda>"}-terms, and so-called
4.738 + \emph{lifting} of rules into a context of @{text "\<And>"} and @{text
4.739 + "\<Longrightarrow>"} connectives. Thus the full power of higher-order Natural
4.740 + Deduction in Isabelle/Pure becomes readily available.
4.741 +*}
4.742 +
4.743 +
4.744 +subsection {* Hereditary Harrop Formulae *}
4.745 +
4.746 +text {*
4.747 + The idea of object-level rules is to model Natural Deduction
4.748 + inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow
4.749 + arbitrary nesting similar to \cite{extensions91}. The most basic
4.750 + rule format is that of a \emph{Horn Clause}:
4.751 + \[
4.752 + \infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\<dots>"} & @{text "A\<^sub>n"}}
4.753 + \]
4.754 + where @{text "A, A\<^sub>1, \<dots>, A\<^sub>n"} are atomic propositions
4.755 + of the framework, usually of the form @{text "Trueprop B"}, where
4.756 + @{text "B"} is a (compound) object-level statement. This
4.757 + object-level inference corresponds to an iterated implication in
4.758 + Pure like this:
4.759 + \[
4.760 + @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"}
4.761 + \]
4.762 + As an example consider conjunction introduction: @{text "A \<Longrightarrow> B \<Longrightarrow> A \<and>
4.763 + B"}. Any parameters occurring in such rule statements are
4.764 + conceptionally treated as arbitrary:
4.765 + \[
4.766 + @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. A\<^sub>1 x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> \<dots> A\<^sub>n x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> A x\<^sub>1 \<dots> x\<^sub>m"}
4.767 + \]
4.768 +
4.769 + Nesting of rules means that the positions of @{text "A\<^sub>i"} may
4.770 + again hold compound rules, not just atomic propositions.
4.771 + Propositions of this format are called \emph{Hereditary Harrop
4.772 + Formulae} in the literature \cite{Miller:1991}. Here we give an
4.773 + inductive characterization as follows:
4.774 +
4.775 + \medskip
4.776 + \begin{tabular}{ll}
4.777 + @{text "\<^bold>x"} & set of variables \\
4.778 + @{text "\<^bold>A"} & set of atomic propositions \\
4.779 + @{text "\<^bold>H = \<And>\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \<Longrightarrow> \<^bold>A"} & set of Hereditary Harrop Formulas \\
4.780 + \end{tabular}
4.781 + \medskip
4.782 +
4.783 + \noindent Thus we essentially impose nesting levels on propositions
4.784 + formed from @{text "\<And>"} and @{text "\<Longrightarrow>"}. At each level there is a
4.785 + prefix of parameters and compound premises, concluding an atomic
4.786 + proposition. Typical examples are @{text "\<longrightarrow>"}-introduction @{text
4.787 + "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n
4.788 + \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"}. Even deeper nesting occurs in well-founded
4.789 + induction @{text "(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"}, but this
4.790 + already marks the limit of rule complexity seen in practice.
4.791 +
4.792 + \medskip Regular user-level inferences in Isabelle/Pure always
4.793 + maintain the following canonical form of results:
4.794 +
4.795 + \begin{itemize}
4.796 +
4.797 + \item Normalization by @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"},
4.798 + which is a theorem of Pure, means that quantifiers are pushed in
4.799 + front of implication at each level of nesting. The normal form is a
4.800 + Hereditary Harrop Formula.
4.801 +
4.802 + \item The outermost prefix of parameters is represented via
4.803 + schematic variables: instead of @{text "\<And>\<^vec>x. \<^vec>H \<^vec>x
4.804 + \<Longrightarrow> A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \<Longrightarrow> A ?\<^vec>x"}.
4.805 + Note that this representation looses information about the order of
4.806 + parameters, and vacuous quantifiers vanish automatically.
4.807 +
4.808 + \end{itemize}
4.809 +*}
4.810 +
4.811 +text %mlref {*
4.812 + \begin{mldecls}
4.813 + @{index_ML MetaSimplifier.norm_hhf: "thm -> thm"} \\
4.814 + \end{mldecls}
4.815 +
4.816 + \begin{description}
4.817 +
4.818 + \item @{ML MetaSimplifier.norm_hhf}~@{text thm} normalizes the given
4.819 + theorem according to the canonical form specified above. This is
4.820 + occasionally helpful to repair some low-level tools that do not
4.821 + handle Hereditary Harrop Formulae properly.
4.822 +
4.823 + \end{description}
4.824 +*}
4.825 +
4.826 +
4.827 +subsection {* Rule composition *}
4.828 +
4.829 +text {*
4.830 + The rule calculus of Isabelle/Pure provides two main inferences:
4.831 + @{inference resolution} (i.e.\ back-chaining of rules) and
4.832 + @{inference assumption} (i.e.\ closing a branch), both modulo
4.833 + higher-order unification. There are also combined variants, notably
4.834 + @{inference elim_resolution} and @{inference dest_resolution}.
4.835 +
4.836 + To understand the all-important @{inference resolution} principle,
4.837 + we first consider raw @{inference_def composition} (modulo
4.838 + higher-order unification with substitution @{text "\<vartheta>"}):
4.839 + \[
4.840 + \infer[(@{inference_def composition})]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}
4.841 + {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}
4.842 + \]
4.843 + Here the conclusion of the first rule is unified with the premise of
4.844 + the second; the resulting rule instance inherits the premises of the
4.845 + first and conclusion of the second. Note that @{text "C"} can again
4.846 + consist of iterated implications. We can also permute the premises
4.847 + of the second rule back-and-forth in order to compose with @{text
4.848 + "B'"} in any position (subsequently we shall always refer to
4.849 + position 1 w.l.o.g.).
4.850 +
4.851 + In @{inference composition} the internal structure of the common
4.852 + part @{text "B"} and @{text "B'"} is not taken into account. For
4.853 + proper @{inference resolution} we require @{text "B"} to be atomic,
4.854 + and explicitly observe the structure @{text "\<And>\<^vec>x. \<^vec>H
4.855 + \<^vec>x \<Longrightarrow> B' \<^vec>x"} of the premise of the second rule. The
4.856 + idea is to adapt the first rule by ``lifting'' it into this context,
4.857 + by means of iterated application of the following inferences:
4.858 + \[
4.859 + \infer[(@{inference_def imp_lift})]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}
4.860 + \]
4.861 + \[
4.862 + \infer[(@{inference_def all_lift})]{@{text "(\<And>\<^vec>x. \<^vec>A (?\<^vec>a \<^vec>x)) \<Longrightarrow> (\<And>\<^vec>x. B (?\<^vec>a \<^vec>x))"}}{@{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"}}
4.863 + \]
4.864 + By combining raw composition with lifting, we get full @{inference
4.865 + resolution} as follows:
4.866 + \[
4.867 + \infer[(@{inference_def resolution})]
4.868 + {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
4.869 + {\begin{tabular}{l}
4.870 + @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\
4.871 + @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
4.872 + @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
4.873 + \end{tabular}}
4.874 + \]
4.875 +
4.876 + Continued resolution of rules allows to back-chain a problem towards
4.877 + more and sub-problems. Branches are closed either by resolving with
4.878 + a rule of 0 premises, or by producing a ``short-circuit'' within a
4.879 + solved situation (again modulo unification):
4.880 + \[
4.881 + \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}
4.882 + {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}}
4.883 + \]
4.884 +
4.885 + FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
4.886 +*}
4.887 +
4.888 +text %mlref {*
4.889 + \begin{mldecls}
4.890 + @{index_ML "op RS": "thm * thm -> thm"} \\
4.891 + @{index_ML "op OF": "thm * thm list -> thm"} \\
4.892 + \end{mldecls}
4.893 +
4.894 + \begin{description}
4.895 +
4.896 + \item @{text "rule\<^sub>1 RS rule\<^sub>2"} resolves @{text
4.897 + "rule\<^sub>1"} with @{text "rule\<^sub>2"} according to the
4.898 + @{inference resolution} principle explained above. Note that the
4.899 + corresponding attribute in the Isar language is called @{attribute
4.900 + THEN}.
4.901 +
4.902 + \item @{text "rule OF rules"} resolves a list of rules with the
4.903 + first rule, addressing its premises @{text "1, \<dots>, length rules"}
4.904 + (operating from last to first). This means the newly emerging
4.905 + premises are all concatenated, without interfering. Also note that
4.906 + compared to @{text "RS"}, the rule argument order is swapped: @{text
4.907 + "rule\<^sub>1 RS rule\<^sub>2 = rule\<^sub>2 OF [rule\<^sub>1]"}.
4.908 +
4.909 + \end{description}
4.910 +*}
4.911 +
4.912 +end
5.1 --- a/doc-src/IsarImplementation/Thy/ML.thy Wed Mar 04 17:12:23 2009 -0800
5.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy Thu Mar 05 02:32:46 2009 +0100
5.3 @@ -631,4 +631,4 @@
5.4 Most table functions correspond to those of association lists.
5.5 *}
5.6
5.7 -end
5.8 +end
5.9 \ No newline at end of file
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Thu Mar 05 02:32:46 2009 +0100
6.3 @@ -0,0 +1,764 @@
6.4 +theory Prelim
6.5 +imports Base
6.6 +begin
6.7 +
6.8 +chapter {* Preliminaries *}
6.9 +
6.10 +section {* Contexts \label{sec:context} *}
6.11 +
6.12 +text {*
6.13 + A logical context represents the background that is required for
6.14 + formulating statements and composing proofs. It acts as a medium to
6.15 + produce formal content, depending on earlier material (declarations,
6.16 + results etc.).
6.17 +
6.18 + For example, derivations within the Isabelle/Pure logic can be
6.19 + described as a judgment @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}, which means that a
6.20 + proposition @{text "\<phi>"} is derivable from hypotheses @{text "\<Gamma>"}
6.21 + within the theory @{text "\<Theta>"}. There are logical reasons for
6.22 + keeping @{text "\<Theta>"} and @{text "\<Gamma>"} separate: theories can be
6.23 + liberal about supporting type constructors and schematic
6.24 + polymorphism of constants and axioms, while the inner calculus of
6.25 + @{text "\<Gamma> \<turnstile> \<phi>"} is strictly limited to Simple Type Theory (with
6.26 + fixed type variables in the assumptions).
6.27 +
6.28 + \medskip Contexts and derivations are linked by the following key
6.29 + principles:
6.30 +
6.31 + \begin{itemize}
6.32 +
6.33 + \item Transfer: monotonicity of derivations admits results to be
6.34 + transferred into a \emph{larger} context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta>
6.35 + \<phi>"} implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>'
6.36 + \<supseteq> \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.
6.37 +
6.38 + \item Export: discharge of hypotheses admits results to be exported
6.39 + into a \emph{smaller} context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"}
6.40 + implies @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and
6.41 + @{text "\<Delta> = \<Gamma>' - \<Gamma>"}. Note that @{text "\<Theta>"} remains unchanged here,
6.42 + only the @{text "\<Gamma>"} part is affected.
6.43 +
6.44 + \end{itemize}
6.45 +
6.46 + \medskip By modeling the main characteristics of the primitive
6.47 + @{text "\<Theta>"} and @{text "\<Gamma>"} above, and abstracting over any
6.48 + particular logical content, we arrive at the fundamental notions of
6.49 + \emph{theory context} and \emph{proof context} in Isabelle/Isar.
6.50 + These implement a certain policy to manage arbitrary \emph{context
6.51 + data}. There is a strongly-typed mechanism to declare new kinds of
6.52 + data at compile time.
6.53 +
6.54 + The internal bootstrap process of Isabelle/Pure eventually reaches a
6.55 + stage where certain data slots provide the logical content of @{text
6.56 + "\<Theta>"} and @{text "\<Gamma>"} sketched above, but this does not stop there!
6.57 + Various additional data slots support all kinds of mechanisms that
6.58 + are not necessarily part of the core logic.
6.59 +
6.60 + For example, there would be data for canonical introduction and
6.61 + elimination rules for arbitrary operators (depending on the
6.62 + object-logic and application), which enables users to perform
6.63 + standard proof steps implicitly (cf.\ the @{text "rule"} method
6.64 + \cite{isabelle-isar-ref}).
6.65 +
6.66 + \medskip Thus Isabelle/Isar is able to bring forth more and more
6.67 + concepts successively. In particular, an object-logic like
6.68 + Isabelle/HOL continues the Isabelle/Pure setup by adding specific
6.69 + components for automated reasoning (classical reasoner, tableau
6.70 + prover, structured induction etc.) and derived specification
6.71 + mechanisms (inductive predicates, recursive functions etc.). All of
6.72 + this is ultimately based on the generic data management by theory
6.73 + and proof contexts introduced here.
6.74 +*}
6.75 +
6.76 +
6.77 +subsection {* Theory context \label{sec:context-theory} *}
6.78 +
6.79 +text {*
6.80 + A \emph{theory} is a data container with explicit name and unique
6.81 + identifier. Theories are related by a (nominal) sub-theory
6.82 + relation, which corresponds to the dependency graph of the original
6.83 + construction; each theory is derived from a certain sub-graph of
6.84 + ancestor theories.
6.85 +
6.86 + The @{text "merge"} operation produces the least upper bound of two
6.87 + theories, which actually degenerates into absorption of one theory
6.88 + into the other (due to the nominal sub-theory relation).
6.89 +
6.90 + The @{text "begin"} operation starts a new theory by importing
6.91 + several parent theories and entering a special @{text "draft"} mode,
6.92 + which is sustained until the final @{text "end"} operation. A draft
6.93 + theory acts like a linear type, where updates invalidate earlier
6.94 + versions. An invalidated draft is called ``stale''.
6.95 +
6.96 + The @{text "checkpoint"} operation produces an intermediate stepping
6.97 + stone that will survive the next update: both the original and the
6.98 + changed theory remain valid and are related by the sub-theory
6.99 + relation. Checkpointing essentially recovers purely functional
6.100 + theory values, at the expense of some extra internal bookkeeping.
6.101 +
6.102 + The @{text "copy"} operation produces an auxiliary version that has
6.103 + the same data content, but is unrelated to the original: updates of
6.104 + the copy do not affect the original, neither does the sub-theory
6.105 + relation hold.
6.106 +
6.107 + \medskip The example in \figref{fig:ex-theory} below shows a theory
6.108 + graph derived from @{text "Pure"}, with theory @{text "Length"}
6.109 + importing @{text "Nat"} and @{text "List"}. The body of @{text
6.110 + "Length"} consists of a sequence of updates, working mostly on
6.111 + drafts. Intermediate checkpoints may occur as well, due to the
6.112 + history mechanism provided by the Isar top-level, cf.\
6.113 + \secref{sec:isar-toplevel}.
6.114 +
6.115 + \begin{figure}[htb]
6.116 + \begin{center}
6.117 + \begin{tabular}{rcccl}
6.118 + & & @{text "Pure"} \\
6.119 + & & @{text "\<down>"} \\
6.120 + & & @{text "FOL"} \\
6.121 + & $\swarrow$ & & $\searrow$ & \\
6.122 + @{text "Nat"} & & & & @{text "List"} \\
6.123 + & $\searrow$ & & $\swarrow$ \\
6.124 + & & @{text "Length"} \\
6.125 + & & \multicolumn{3}{l}{~~@{keyword "imports"}} \\
6.126 + & & \multicolumn{3}{l}{~~@{keyword "begin"}} \\
6.127 + & & $\vdots$~~ \\
6.128 + & & @{text "\<bullet>"}~~ \\
6.129 + & & $\vdots$~~ \\
6.130 + & & @{text "\<bullet>"}~~ \\
6.131 + & & $\vdots$~~ \\
6.132 + & & \multicolumn{3}{l}{~~@{command "end"}} \\
6.133 + \end{tabular}
6.134 + \caption{A theory definition depending on ancestors}\label{fig:ex-theory}
6.135 + \end{center}
6.136 + \end{figure}
6.137 +
6.138 + \medskip There is a separate notion of \emph{theory reference} for
6.139 + maintaining a live link to an evolving theory context: updates on
6.140 + drafts are propagated automatically. Dynamic updating stops after
6.141 + an explicit @{text "end"} only.
6.142 +
6.143 + Derived entities may store a theory reference in order to indicate
6.144 + the context they belong to. This implicitly assumes monotonic
6.145 + reasoning, because the referenced context may become larger without
6.146 + further notice.
6.147 +*}
6.148 +
6.149 +text %mlref {*
6.150 + \begin{mldecls}
6.151 + @{index_ML_type theory} \\
6.152 + @{index_ML Theory.subthy: "theory * theory -> bool"} \\
6.153 + @{index_ML Theory.merge: "theory * theory -> theory"} \\
6.154 + @{index_ML Theory.checkpoint: "theory -> theory"} \\
6.155 + @{index_ML Theory.copy: "theory -> theory"} \\
6.156 + \end{mldecls}
6.157 + \begin{mldecls}
6.158 + @{index_ML_type theory_ref} \\
6.159 + @{index_ML Theory.deref: "theory_ref -> theory"} \\
6.160 + @{index_ML Theory.check_thy: "theory -> theory_ref"} \\
6.161 + \end{mldecls}
6.162 +
6.163 + \begin{description}
6.164 +
6.165 + \item @{ML_type theory} represents theory contexts. This is
6.166 + essentially a linear type! Most operations destroy the original
6.167 + version, which then becomes ``stale''.
6.168 +
6.169 + \item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"}
6.170 + compares theories according to the inherent graph structure of the
6.171 + construction. This sub-theory relation is a nominal approximation
6.172 + of inclusion (@{text "\<subseteq>"}) of the corresponding content.
6.173 +
6.174 + \item @{ML "Theory.merge"}~@{text "(thy\<^sub>1, thy\<^sub>2)"}
6.175 + absorbs one theory into the other. This fails for unrelated
6.176 + theories!
6.177 +
6.178 + \item @{ML "Theory.checkpoint"}~@{text "thy"} produces a safe
6.179 + stepping stone in the linear development of @{text "thy"}. The next
6.180 + update will result in two related, valid theories.
6.181 +
6.182 + \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text
6.183 + "thy"} that holds a copy of the same data. The result is not
6.184 + related to the original; the original is unchanged.
6.185 +
6.186 + \item @{ML_type theory_ref} represents a sliding reference to an
6.187 + always valid theory; updates on the original are propagated
6.188 + automatically.
6.189 +
6.190 + \item @{ML "Theory.deref"}~@{text "thy_ref"} turns a @{ML_type
6.191 + "theory_ref"} into an @{ML_type "theory"} value. As the referenced
6.192 + theory evolves monotonically over time, later invocations of @{ML
6.193 + "Theory.deref"} may refer to a larger context.
6.194 +
6.195 + \item @{ML "Theory.check_thy"}~@{text "thy"} produces a @{ML_type
6.196 + "theory_ref"} from a valid @{ML_type "theory"} value.
6.197 +
6.198 + \end{description}
6.199 +*}
6.200 +
6.201 +
6.202 +subsection {* Proof context \label{sec:context-proof} *}
6.203 +
6.204 +text {*
6.205 + A proof context is a container for pure data with a back-reference
6.206 + to the theory it belongs to. The @{text "init"} operation creates a
6.207 + proof context from a given theory. Modifications to draft theories
6.208 + are propagated to the proof context as usual, but there is also an
6.209 + explicit @{text "transfer"} operation to force resynchronization
6.210 + with more substantial updates to the underlying theory. The actual
6.211 + context data does not require any special bookkeeping, thanks to the
6.212 + lack of destructive features.
6.213 +
6.214 + Entities derived in a proof context need to record inherent logical
6.215 + requirements explicitly, since there is no separate context
6.216 + identification as for theories. For example, hypotheses used in
6.217 + primitive derivations (cf.\ \secref{sec:thms}) are recorded
6.218 + separately within the sequent @{text "\<Gamma> \<turnstile> \<phi>"}, just to make double
6.219 + sure. Results could still leak into an alien proof context due to
6.220 + programming errors, but Isabelle/Isar includes some extra validity
6.221 + checks in critical positions, notably at the end of a sub-proof.
6.222 +
6.223 + Proof contexts may be manipulated arbitrarily, although the common
6.224 + discipline is to follow block structure as a mental model: a given
6.225 + context is extended consecutively, and results are exported back
6.226 + into the original context. Note that the Isar proof states model
6.227 + block-structured reasoning explicitly, using a stack of proof
6.228 + contexts internally.
6.229 +*}
6.230 +
6.231 +text %mlref {*
6.232 + \begin{mldecls}
6.233 + @{index_ML_type Proof.context} \\
6.234 + @{index_ML ProofContext.init: "theory -> Proof.context"} \\
6.235 + @{index_ML ProofContext.theory_of: "Proof.context -> theory"} \\
6.236 + @{index_ML ProofContext.transfer: "theory -> Proof.context -> Proof.context"} \\
6.237 + \end{mldecls}
6.238 +
6.239 + \begin{description}
6.240 +
6.241 + \item @{ML_type Proof.context} represents proof contexts. Elements
6.242 + of this type are essentially pure values, with a sliding reference
6.243 + to the background theory.
6.244 +
6.245 + \item @{ML ProofContext.init}~@{text "thy"} produces a proof context
6.246 + derived from @{text "thy"}, initializing all data.
6.247 +
6.248 + \item @{ML ProofContext.theory_of}~@{text "ctxt"} selects the
6.249 + background theory from @{text "ctxt"}, dereferencing its internal
6.250 + @{ML_type theory_ref}.
6.251 +
6.252 + \item @{ML ProofContext.transfer}~@{text "thy ctxt"} promotes the
6.253 + background theory of @{text "ctxt"} to the super theory @{text
6.254 + "thy"}.
6.255 +
6.256 + \end{description}
6.257 +*}
6.258 +
6.259 +
6.260 +subsection {* Generic contexts \label{sec:generic-context} *}
6.261 +
6.262 +text {*
6.263 + A generic context is the disjoint sum of either a theory or proof
6.264 + context. Occasionally, this enables uniform treatment of generic
6.265 + context data, typically extra-logical information. Operations on
6.266 + generic contexts include the usual injections, partial selections,
6.267 + and combinators for lifting operations on either component of the
6.268 + disjoint sum.
6.269 +
6.270 + Moreover, there are total operations @{text "theory_of"} and @{text
6.271 + "proof_of"} to convert a generic context into either kind: a theory
6.272 + can always be selected from the sum, while a proof context might
6.273 + have to be constructed by an ad-hoc @{text "init"} operation.
6.274 +*}
6.275 +
6.276 +text %mlref {*
6.277 + \begin{mldecls}
6.278 + @{index_ML_type Context.generic} \\
6.279 + @{index_ML Context.theory_of: "Context.generic -> theory"} \\
6.280 + @{index_ML Context.proof_of: "Context.generic -> Proof.context"} \\
6.281 + \end{mldecls}
6.282 +
6.283 + \begin{description}
6.284 +
6.285 + \item @{ML_type Context.generic} is the direct sum of @{ML_type
6.286 + "theory"} and @{ML_type "Proof.context"}, with the datatype
6.287 + constructors @{ML "Context.Theory"} and @{ML "Context.Proof"}.
6.288 +
6.289 + \item @{ML Context.theory_of}~@{text "context"} always produces a
6.290 + theory from the generic @{text "context"}, using @{ML
6.291 + "ProofContext.theory_of"} as required.
6.292 +
6.293 + \item @{ML Context.proof_of}~@{text "context"} always produces a
6.294 + proof context from the generic @{text "context"}, using @{ML
6.295 + "ProofContext.init"} as required (note that this re-initializes the
6.296 + context data with each invocation).
6.297 +
6.298 + \end{description}
6.299 +*}
6.300 +
6.301 +
6.302 +subsection {* Context data \label{sec:context-data} *}
6.303 +
6.304 +text {*
6.305 + The main purpose of theory and proof contexts is to manage arbitrary
6.306 + data. New data types can be declared incrementally at compile time.
6.307 + There are separate declaration mechanisms for any of the three kinds
6.308 + of contexts: theory, proof, generic.
6.309 +
6.310 + \paragraph{Theory data} may refer to destructive entities, which are
6.311 + maintained in direct correspondence to the linear evolution of
6.312 + theory values, including explicit copies.\footnote{Most existing
6.313 + instances of destructive theory data are merely historical relics
6.314 + (e.g.\ the destructive theorem storage, and destructive hints for
6.315 + the Simplifier and Classical rules).} A theory data declaration
6.316 + needs to implement the following SML signature:
6.317 +
6.318 + \medskip
6.319 + \begin{tabular}{ll}
6.320 + @{text "\<type> T"} & representing type \\
6.321 + @{text "\<val> empty: T"} & empty default value \\
6.322 + @{text "\<val> copy: T \<rightarrow> T"} & refresh impure data \\
6.323 + @{text "\<val> extend: T \<rightarrow> T"} & re-initialize on import \\
6.324 + @{text "\<val> merge: T \<times> T \<rightarrow> T"} & join on import \\
6.325 + \end{tabular}
6.326 + \medskip
6.327 +
6.328 + \noindent The @{text "empty"} value acts as initial default for
6.329 + \emph{any} theory that does not declare actual data content; @{text
6.330 + "copy"} maintains persistent integrity for impure data, it is just
6.331 + the identity for pure values; @{text "extend"} is acts like a
6.332 + unitary version of @{text "merge"}, both operations should also
6.333 + include the functionality of @{text "copy"} for impure data.
6.334 +
6.335 + \paragraph{Proof context data} is purely functional. A declaration
6.336 + needs to implement the following SML signature:
6.337 +
6.338 + \medskip
6.339 + \begin{tabular}{ll}
6.340 + @{text "\<type> T"} & representing type \\
6.341 + @{text "\<val> init: theory \<rightarrow> T"} & produce initial value \\
6.342 + \end{tabular}
6.343 + \medskip
6.344 +
6.345 + \noindent The @{text "init"} operation is supposed to produce a pure
6.346 + value from the given background theory.
6.347 +
6.348 + \paragraph{Generic data} provides a hybrid interface for both theory
6.349 + and proof data. The declaration is essentially the same as for
6.350 + (pure) theory data, without @{text "copy"}. The @{text "init"}
6.351 + operation for proof contexts merely selects the current data value
6.352 + from the background theory.
6.353 +
6.354 + \bigskip A data declaration of type @{text "T"} results in the
6.355 + following interface:
6.356 +
6.357 + \medskip
6.358 + \begin{tabular}{ll}
6.359 + @{text "init: theory \<rightarrow> T"} \\
6.360 + @{text "get: context \<rightarrow> T"} \\
6.361 + @{text "put: T \<rightarrow> context \<rightarrow> context"} \\
6.362 + @{text "map: (T \<rightarrow> T) \<rightarrow> context \<rightarrow> context"} \\
6.363 + \end{tabular}
6.364 + \medskip
6.365 +
6.366 + \noindent Here @{text "init"} is only applicable to impure theory
6.367 + data to install a fresh copy persistently (destructive update on
6.368 + uninitialized has no permanent effect). The other operations provide
6.369 + access for the particular kind of context (theory, proof, or generic
6.370 + context). Note that this is a safe interface: there is no other way
6.371 + to access the corresponding data slot of a context. By keeping
6.372 + these operations private, a component may maintain abstract values
6.373 + authentically, without other components interfering.
6.374 +*}
6.375 +
6.376 +text %mlref {*
6.377 + \begin{mldecls}
6.378 + @{index_ML_functor TheoryDataFun} \\
6.379 + @{index_ML_functor ProofDataFun} \\
6.380 + @{index_ML_functor GenericDataFun} \\
6.381 + \end{mldecls}
6.382 +
6.383 + \begin{description}
6.384 +
6.385 + \item @{ML_functor TheoryDataFun}@{text "(spec)"} declares data for
6.386 + type @{ML_type theory} according to the specification provided as
6.387 + argument structure. The resulting structure provides data init and
6.388 + access operations as described above.
6.389 +
6.390 + \item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous to
6.391 + @{ML_functor TheoryDataFun} for type @{ML_type Proof.context}.
6.392 +
6.393 + \item @{ML_functor GenericDataFun}@{text "(spec)"} is analogous to
6.394 + @{ML_functor TheoryDataFun} for type @{ML_type Context.generic}.
6.395 +
6.396 + \end{description}
6.397 +*}
6.398 +
6.399 +
6.400 +section {* Names \label{sec:names} *}
6.401 +
6.402 +text {*
6.403 + In principle, a name is just a string, but there are various
6.404 + convention for encoding additional structure. For example, ``@{text
6.405 + "Foo.bar.baz"}'' is considered as a qualified name consisting of
6.406 + three basic name components. The individual constituents of a name
6.407 + may have further substructure, e.g.\ the string
6.408 + ``\verb,\,\verb,<alpha>,'' encodes as a single symbol.
6.409 +*}
6.410 +
6.411 +
6.412 +subsection {* Strings of symbols *}
6.413 +
6.414 +text {*
6.415 + A \emph{symbol} constitutes the smallest textual unit in Isabelle
6.416 + --- raw characters are normally not encountered at all. Isabelle
6.417 + strings consist of a sequence of symbols, represented as a packed
6.418 + string or a list of strings. Each symbol is in itself a small
6.419 + string, which has either one of the following forms:
6.420 +
6.421 + \begin{enumerate}
6.422 +
6.423 + \item a single ASCII character ``@{text "c"}'', for example
6.424 + ``\verb,a,'',
6.425 +
6.426 + \item a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
6.427 + for example ``\verb,\,\verb,<alpha>,'',
6.428 +
6.429 + \item a control symbol ``\verb,\,\verb,<^,@{text "ident"}\verb,>,'',
6.430 + for example ``\verb,\,\verb,<^bold>,'',
6.431 +
6.432 + \item a raw symbol ``\verb,\,\verb,<^raw:,@{text text}\verb,>,''
6.433 + where @{text text} constists of printable characters excluding
6.434 + ``\verb,.,'' and ``\verb,>,'', for example
6.435 + ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
6.436 +
6.437 + \item a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
6.438 + n}\verb,>, where @{text n} consists of digits, for example
6.439 + ``\verb,\,\verb,<^raw42>,''.
6.440 +
6.441 + \end{enumerate}
6.442 +
6.443 + \noindent The @{text "ident"} syntax for symbol names is @{text
6.444 + "letter (letter | digit)\<^sup>*"}, where @{text "letter =
6.445 + A..Za..z"} and @{text "digit = 0..9"}. There are infinitely many
6.446 + regular symbols and control symbols, but a fixed collection of
6.447 + standard symbols is treated specifically. For example,
6.448 + ``\verb,\,\verb,<alpha>,'' is classified as a letter, which means it
6.449 + may occur within regular Isabelle identifiers.
6.450 +
6.451 + Since the character set underlying Isabelle symbols is 7-bit ASCII
6.452 + and 8-bit characters are passed through transparently, Isabelle may
6.453 + also process Unicode/UCS data in UTF-8 encoding. Unicode provides
6.454 + its own collection of mathematical symbols, but there is no built-in
6.455 + link to the standard collection of Isabelle.
6.456 +
6.457 + \medskip Output of Isabelle symbols depends on the print mode
6.458 + (\secref{print-mode}). For example, the standard {\LaTeX} setup of
6.459 + the Isabelle document preparation system would present
6.460 + ``\verb,\,\verb,<alpha>,'' as @{text "\<alpha>"}, and
6.461 + ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
6.462 + "\<^bold>\<alpha>"}.
6.463 +*}
6.464 +
6.465 +text %mlref {*
6.466 + \begin{mldecls}
6.467 + @{index_ML_type "Symbol.symbol"} \\
6.468 + @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
6.469 + @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
6.470 + @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
6.471 + @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
6.472 + @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
6.473 + \end{mldecls}
6.474 + \begin{mldecls}
6.475 + @{index_ML_type "Symbol.sym"} \\
6.476 + @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
6.477 + \end{mldecls}
6.478 +
6.479 + \begin{description}
6.480 +
6.481 + \item @{ML_type "Symbol.symbol"} represents individual Isabelle
6.482 + symbols; this is an alias for @{ML_type "string"}.
6.483 +
6.484 + \item @{ML "Symbol.explode"}~@{text "str"} produces a symbol list
6.485 + from the packed form. This function supercedes @{ML
6.486 + "String.explode"} for virtually all purposes of manipulating text in
6.487 + Isabelle!
6.488 +
6.489 + \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
6.490 + "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify standard
6.491 + symbols according to fixed syntactic conventions of Isabelle, cf.\
6.492 + \cite{isabelle-isar-ref}.
6.493 +
6.494 + \item @{ML_type "Symbol.sym"} is a concrete datatype that represents
6.495 + the different kinds of symbols explicitly, with constructors @{ML
6.496 + "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, @{ML
6.497 + "Symbol.Raw"}.
6.498 +
6.499 + \item @{ML "Symbol.decode"} converts the string representation of a
6.500 + symbol into the datatype version.
6.501 +
6.502 + \end{description}
6.503 +*}
6.504 +
6.505 +
6.506 +subsection {* Basic names \label{sec:basic-names} *}
6.507 +
6.508 +text {*
6.509 + A \emph{basic name} essentially consists of a single Isabelle
6.510 + identifier. There are conventions to mark separate classes of basic
6.511 + names, by attaching a suffix of underscores: one underscore means
6.512 + \emph{internal name}, two underscores means \emph{Skolem name},
6.513 + three underscores means \emph{internal Skolem name}.
6.514 +
6.515 + For example, the basic name @{text "foo"} has the internal version
6.516 + @{text "foo_"}, with Skolem versions @{text "foo__"} and @{text
6.517 + "foo___"}, respectively.
6.518 +
6.519 + These special versions provide copies of the basic name space, apart
6.520 + from anything that normally appears in the user text. For example,
6.521 + system generated variables in Isar proof contexts are usually marked
6.522 + as internal, which prevents mysterious name references like @{text
6.523 + "xaa"} to appear in the text.
6.524 +
6.525 + \medskip Manipulating binding scopes often requires on-the-fly
6.526 + renamings. A \emph{name context} contains a collection of already
6.527 + used names. The @{text "declare"} operation adds names to the
6.528 + context.
6.529 +
6.530 + The @{text "invents"} operation derives a number of fresh names from
6.531 + a given starting point. For example, the first three names derived
6.532 + from @{text "a"} are @{text "a"}, @{text "b"}, @{text "c"}.
6.533 +
6.534 + The @{text "variants"} operation produces fresh names by
6.535 + incrementing tentative names as base-26 numbers (with digits @{text
6.536 + "a..z"}) until all clashes are resolved. For example, name @{text
6.537 + "foo"} results in variants @{text "fooa"}, @{text "foob"}, @{text
6.538 + "fooc"}, \dots, @{text "fooaa"}, @{text "fooab"} etc.; each renaming
6.539 + step picks the next unused variant from this sequence.
6.540 +*}
6.541 +
6.542 +text %mlref {*
6.543 + \begin{mldecls}
6.544 + @{index_ML Name.internal: "string -> string"} \\
6.545 + @{index_ML Name.skolem: "string -> string"} \\
6.546 + \end{mldecls}
6.547 + \begin{mldecls}
6.548 + @{index_ML_type Name.context} \\
6.549 + @{index_ML Name.context: Name.context} \\
6.550 + @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
6.551 + @{index_ML Name.invents: "Name.context -> string -> int -> string list"} \\
6.552 + @{index_ML Name.variants: "string list -> Name.context -> string list * Name.context"} \\
6.553 + \end{mldecls}
6.554 +
6.555 + \begin{description}
6.556 +
6.557 + \item @{ML Name.internal}~@{text "name"} produces an internal name
6.558 + by adding one underscore.
6.559 +
6.560 + \item @{ML Name.skolem}~@{text "name"} produces a Skolem name by
6.561 + adding two underscores.
6.562 +
6.563 + \item @{ML_type Name.context} represents the context of already used
6.564 + names; the initial value is @{ML "Name.context"}.
6.565 +
6.566 + \item @{ML Name.declare}~@{text "name"} enters a used name into the
6.567 + context.
6.568 +
6.569 + \item @{ML Name.invents}~@{text "context name n"} produces @{text
6.570 + "n"} fresh names derived from @{text "name"}.
6.571 +
6.572 + \item @{ML Name.variants}~@{text "names context"} produces fresh
6.573 + variants of @{text "names"}; the result is entered into the context.
6.574 +
6.575 + \end{description}
6.576 +*}
6.577 +
6.578 +
6.579 +subsection {* Indexed names *}
6.580 +
6.581 +text {*
6.582 + An \emph{indexed name} (or @{text "indexname"}) is a pair of a basic
6.583 + name and a natural number. This representation allows efficient
6.584 + renaming by incrementing the second component only. The canonical
6.585 + way to rename two collections of indexnames apart from each other is
6.586 + this: determine the maximum index @{text "maxidx"} of the first
6.587 + collection, then increment all indexes of the second collection by
6.588 + @{text "maxidx + 1"}; the maximum index of an empty collection is
6.589 + @{text "-1"}.
6.590 +
6.591 + Occasionally, basic names and indexed names are injected into the
6.592 + same pair type: the (improper) indexname @{text "(x, -1)"} is used
6.593 + to encode basic names.
6.594 +
6.595 + \medskip Isabelle syntax observes the following rules for
6.596 + representing an indexname @{text "(x, i)"} as a packed string:
6.597 +
6.598 + \begin{itemize}
6.599 +
6.600 + \item @{text "?x"} if @{text "x"} does not end with a digit and @{text "i = 0"},
6.601 +
6.602 + \item @{text "?xi"} if @{text "x"} does not end with a digit,
6.603 +
6.604 + \item @{text "?x.i"} otherwise.
6.605 +
6.606 + \end{itemize}
6.607 +
6.608 + Indexnames may acquire large index numbers over time. Results are
6.609 + normalized towards @{text "0"} at certain checkpoints, notably at
6.610 + the end of a proof. This works by producing variants of the
6.611 + corresponding basic name components. For example, the collection
6.612 + @{text "?x1, ?x7, ?x42"} becomes @{text "?x, ?xa, ?xb"}.
6.613 +*}
6.614 +
6.615 +text %mlref {*
6.616 + \begin{mldecls}
6.617 + @{index_ML_type indexname} \\
6.618 + \end{mldecls}
6.619 +
6.620 + \begin{description}
6.621 +
6.622 + \item @{ML_type indexname} represents indexed names. This is an
6.623 + abbreviation for @{ML_type "string * int"}. The second component is
6.624 + usually non-negative, except for situations where @{text "(x, -1)"}
6.625 + is used to embed basic names into this type.
6.626 +
6.627 + \end{description}
6.628 +*}
6.629 +
6.630 +
6.631 +subsection {* Qualified names and name spaces *}
6.632 +
6.633 +text {*
6.634 + A \emph{qualified name} consists of a non-empty sequence of basic
6.635 + name components. The packed representation uses a dot as separator,
6.636 + as in ``@{text "A.b.c"}''. The last component is called \emph{base}
6.637 + name, the remaining prefix \emph{qualifier} (which may be empty).
6.638 + The idea of qualified names is to encode nested structures by
6.639 + recording the access paths as qualifiers. For example, an item
6.640 + named ``@{text "A.b.c"}'' may be understood as a local entity @{text
6.641 + "c"}, within a local structure @{text "b"}, within a global
6.642 + structure @{text "A"}. Typically, name space hierarchies consist of
6.643 + 1--2 levels of qualification, but this need not be always so.
6.644 +
6.645 + The empty name is commonly used as an indication of unnamed
6.646 + entities, whenever this makes any sense. The basic operations on
6.647 + qualified names are smart enough to pass through such improper names
6.648 + unchanged.
6.649 +
6.650 + \medskip A @{text "naming"} policy tells how to turn a name
6.651 + specification into a fully qualified internal name (by the @{text
6.652 + "full"} operation), and how fully qualified names may be accessed
6.653 + externally. For example, the default naming policy is to prefix an
6.654 + implicit path: @{text "full x"} produces @{text "path.x"}, and the
6.655 + standard accesses for @{text "path.x"} include both @{text "x"} and
6.656 + @{text "path.x"}. Normally, the naming is implicit in the theory or
6.657 + proof context; there are separate versions of the corresponding.
6.658 +
6.659 + \medskip A @{text "name space"} manages a collection of fully
6.660 + internalized names, together with a mapping between external names
6.661 + and internal names (in both directions). The corresponding @{text
6.662 + "intern"} and @{text "extern"} operations are mostly used for
6.663 + parsing and printing only! The @{text "declare"} operation augments
6.664 + a name space according to the accesses determined by the naming
6.665 + policy.
6.666 +
6.667 + \medskip As a general principle, there is a separate name space for
6.668 + each kind of formal entity, e.g.\ logical constant, type
6.669 + constructor, type class, theorem. It is usually clear from the
6.670 + occurrence in concrete syntax (or from the scope) which kind of
6.671 + entity a name refers to. For example, the very same name @{text
6.672 + "c"} may be used uniformly for a constant, type constructor, and
6.673 + type class.
6.674 +
6.675 + There are common schemes to name theorems systematically, according
6.676 + to the name of the main logical entity involved, e.g.\ @{text
6.677 + "c.intro"} for a canonical theorem related to constant @{text "c"}.
6.678 + This technique of mapping names from one space into another requires
6.679 + some care in order to avoid conflicts. In particular, theorem names
6.680 + derived from a type constructor or type class are better suffixed in
6.681 + addition to the usual qualification, e.g.\ @{text "c_type.intro"}
6.682 + and @{text "c_class.intro"} for theorems related to type @{text "c"}
6.683 + and class @{text "c"}, respectively.
6.684 +*}
6.685 +
6.686 +text %mlref {*
6.687 + \begin{mldecls}
6.688 + @{index_ML NameSpace.base: "string -> string"} \\
6.689 + @{index_ML NameSpace.qualifier: "string -> string"} \\
6.690 + @{index_ML NameSpace.append: "string -> string -> string"} \\
6.691 + @{index_ML NameSpace.implode: "string list -> string"} \\
6.692 + @{index_ML NameSpace.explode: "string -> string list"} \\
6.693 + \end{mldecls}
6.694 + \begin{mldecls}
6.695 + @{index_ML_type NameSpace.naming} \\
6.696 + @{index_ML NameSpace.default_naming: NameSpace.naming} \\
6.697 + @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
6.698 + @{index_ML NameSpace.full_name: "NameSpace.naming -> binding -> string"} \\
6.699 + \end{mldecls}
6.700 + \begin{mldecls}
6.701 + @{index_ML_type NameSpace.T} \\
6.702 + @{index_ML NameSpace.empty: NameSpace.T} \\
6.703 + @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
6.704 + @{index_ML NameSpace.declare: "NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T"} \\
6.705 + @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\
6.706 + @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\
6.707 + \end{mldecls}
6.708 +
6.709 + \begin{description}
6.710 +
6.711 + \item @{ML NameSpace.base}~@{text "name"} returns the base name of a
6.712 + qualified name.
6.713 +
6.714 + \item @{ML NameSpace.qualifier}~@{text "name"} returns the qualifier
6.715 + of a qualified name.
6.716 +
6.717 + \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}
6.718 + appends two qualified names.
6.719 +
6.720 + \item @{ML NameSpace.implode}~@{text "name"} and @{ML
6.721 + NameSpace.explode}~@{text "names"} convert between the packed string
6.722 + representation and the explicit list form of qualified names.
6.723 +
6.724 + \item @{ML_type NameSpace.naming} represents the abstract concept of
6.725 + a naming policy.
6.726 +
6.727 + \item @{ML NameSpace.default_naming} is the default naming policy.
6.728 + In a theory context, this is usually augmented by a path prefix
6.729 + consisting of the theory name.
6.730 +
6.731 + \item @{ML NameSpace.add_path}~@{text "path naming"} augments the
6.732 + naming policy by extending its path component.
6.733 +
6.734 + \item @{ML NameSpace.full_name}@{text "naming binding"} turns a name
6.735 + binding (usually a basic name) into the fully qualified
6.736 + internal name, according to the given naming policy.
6.737 +
6.738 + \item @{ML_type NameSpace.T} represents name spaces.
6.739 +
6.740 + \item @{ML NameSpace.empty} and @{ML NameSpace.merge}~@{text
6.741 + "(space\<^isub>1, space\<^isub>2)"} are the canonical operations for
6.742 + maintaining name spaces according to theory data management
6.743 + (\secref{sec:context-data}).
6.744 +
6.745 + \item @{ML NameSpace.declare}~@{text "naming bindings space"} enters a
6.746 + name binding as fully qualified internal name into the name space,
6.747 + with external accesses determined by the naming policy.
6.748 +
6.749 + \item @{ML NameSpace.intern}~@{text "space name"} internalizes a
6.750 + (partially qualified) external name.
6.751 +
6.752 + This operation is mostly for parsing! Note that fully qualified
6.753 + names stemming from declarations are produced via @{ML
6.754 + "NameSpace.full_name"} and @{ML "NameSpace.declare"}
6.755 + (or their derivatives for @{ML_type theory} and
6.756 + @{ML_type Proof.context}).
6.757 +
6.758 + \item @{ML NameSpace.extern}~@{text "space name"} externalizes a
6.759 + (fully qualified) internal name.
6.760 +
6.761 + This operation is mostly for printing! Note unqualified names are
6.762 + produced via @{ML NameSpace.base}.
6.763 +
6.764 + \end{description}
6.765 +*}
6.766 +
6.767 +end
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/doc-src/IsarImplementation/Thy/Proof.thy Thu Mar 05 02:32:46 2009 +0100
7.3 @@ -0,0 +1,330 @@
7.4 +theory Proof
7.5 +imports Base
7.6 +begin
7.7 +
7.8 +chapter {* Structured proofs *}
7.9 +
7.10 +section {* Variables \label{sec:variables} *}
7.11 +
7.12 +text {*
7.13 + Any variable that is not explicitly bound by @{text "\<lambda>"}-abstraction
7.14 + is considered as ``free''. Logically, free variables act like
7.15 + outermost universal quantification at the sequent level: @{text
7.16 + "A\<^isub>1(x), \<dots>, A\<^isub>n(x) \<turnstile> B(x)"} means that the result
7.17 + holds \emph{for all} values of @{text "x"}. Free variables for
7.18 + terms (not types) can be fully internalized into the logic: @{text
7.19 + "\<turnstile> B(x)"} and @{text "\<turnstile> \<And>x. B(x)"} are interchangeable, provided
7.20 + that @{text "x"} does not occur elsewhere in the context.
7.21 + Inspecting @{text "\<turnstile> \<And>x. B(x)"} more closely, we see that inside the
7.22 + quantifier, @{text "x"} is essentially ``arbitrary, but fixed'',
7.23 + while from outside it appears as a place-holder for instantiation
7.24 + (thanks to @{text "\<And>"} elimination).
7.25 +
7.26 + The Pure logic represents the idea of variables being either inside
7.27 + or outside the current scope by providing separate syntactic
7.28 + categories for \emph{fixed variables} (e.g.\ @{text "x"}) vs.\
7.29 + \emph{schematic variables} (e.g.\ @{text "?x"}). Incidently, a
7.30 + universal result @{text "\<turnstile> \<And>x. B(x)"} has the HHF normal form @{text
7.31 + "\<turnstile> B(?x)"}, which represents its generality nicely without requiring
7.32 + an explicit quantifier. The same principle works for type
7.33 + variables: @{text "\<turnstile> B(?\<alpha>)"} represents the idea of ``@{text "\<turnstile>
7.34 + \<forall>\<alpha>. B(\<alpha>)"}'' without demanding a truly polymorphic framework.
7.35 +
7.36 + \medskip Additional care is required to treat type variables in a
7.37 + way that facilitates type-inference. In principle, term variables
7.38 + depend on type variables, which means that type variables would have
7.39 + to be declared first. For example, a raw type-theoretic framework
7.40 + would demand the context to be constructed in stages as follows:
7.41 + @{text "\<Gamma> = \<alpha>: type, x: \<alpha>, a: A(x\<^isub>\<alpha>)"}.
7.42 +
7.43 + We allow a slightly less formalistic mode of operation: term
7.44 + variables @{text "x"} are fixed without specifying a type yet
7.45 + (essentially \emph{all} potential occurrences of some instance
7.46 + @{text "x\<^isub>\<tau>"} are fixed); the first occurrence of @{text "x"}
7.47 + within a specific term assigns its most general type, which is then
7.48 + maintained consistently in the context. The above example becomes
7.49 + @{text "\<Gamma> = x: term, \<alpha>: type, A(x\<^isub>\<alpha>)"}, where type @{text
7.50 + "\<alpha>"} is fixed \emph{after} term @{text "x"}, and the constraint
7.51 + @{text "x :: \<alpha>"} is an implicit consequence of the occurrence of
7.52 + @{text "x\<^isub>\<alpha>"} in the subsequent proposition.
7.53 +
7.54 + This twist of dependencies is also accommodated by the reverse
7.55 + operation of exporting results from a context: a type variable
7.56 + @{text "\<alpha>"} is considered fixed as long as it occurs in some fixed
7.57 + term variable of the context. For example, exporting @{text "x:
7.58 + term, \<alpha>: type \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} produces in the first step
7.59 + @{text "x: term \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} for fixed @{text "\<alpha>"},
7.60 + and only in the second step @{text "\<turnstile> ?x\<^isub>?\<^isub>\<alpha> =
7.61 + ?x\<^isub>?\<^isub>\<alpha>"} for schematic @{text "?x"} and @{text "?\<alpha>"}.
7.62 +
7.63 + \medskip The Isabelle/Isar proof context manages the gory details of
7.64 + term vs.\ type variables, with high-level principles for moving the
7.65 + frontier between fixed and schematic variables.
7.66 +
7.67 + The @{text "add_fixes"} operation explictly declares fixed
7.68 + variables; the @{text "declare_term"} operation absorbs a term into
7.69 + a context by fixing new type variables and adding syntactic
7.70 + constraints.
7.71 +
7.72 + The @{text "export"} operation is able to perform the main work of
7.73 + generalizing term and type variables as sketched above, assuming
7.74 + that fixing variables and terms have been declared properly.
7.75 +
7.76 + There @{text "import"} operation makes a generalized fact a genuine
7.77 + part of the context, by inventing fixed variables for the schematic
7.78 + ones. The effect can be reversed by using @{text "export"} later,
7.79 + potentially with an extended context; the result is equivalent to
7.80 + the original modulo renaming of schematic variables.
7.81 +
7.82 + The @{text "focus"} operation provides a variant of @{text "import"}
7.83 + for nested propositions (with explicit quantification): @{text
7.84 + "\<And>x\<^isub>1 \<dots> x\<^isub>n. B(x\<^isub>1, \<dots>, x\<^isub>n)"} is
7.85 + decomposed by inventing fixed variables @{text "x\<^isub>1, \<dots>,
7.86 + x\<^isub>n"} for the body.
7.87 +*}
7.88 +
7.89 +text %mlref {*
7.90 + \begin{mldecls}
7.91 + @{index_ML Variable.add_fixes: "
7.92 + string list -> Proof.context -> string list * Proof.context"} \\
7.93 + @{index_ML Variable.variant_fixes: "
7.94 + string list -> Proof.context -> string list * Proof.context"} \\
7.95 + @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
7.96 + @{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
7.97 + @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
7.98 + @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
7.99 + @{index_ML Variable.import_thms: "bool -> thm list -> Proof.context ->
7.100 + ((ctyp list * cterm list) * thm list) * Proof.context"} \\
7.101 + @{index_ML Variable.focus: "cterm -> Proof.context -> (cterm list * cterm) * Proof.context"} \\
7.102 + \end{mldecls}
7.103 +
7.104 + \begin{description}
7.105 +
7.106 + \item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term
7.107 + variables @{text "xs"}, returning the resulting internal names. By
7.108 + default, the internal representation coincides with the external
7.109 + one, which also means that the given variables must not be fixed
7.110 + already. There is a different policy within a local proof body: the
7.111 + given names are just hints for newly invented Skolem variables.
7.112 +
7.113 + \item @{ML Variable.variant_fixes} is similar to @{ML
7.114 + Variable.add_fixes}, but always produces fresh variants of the given
7.115 + names.
7.116 +
7.117 + \item @{ML Variable.declare_term}~@{text "t ctxt"} declares term
7.118 + @{text "t"} to belong to the context. This automatically fixes new
7.119 + type variables, but not term variables. Syntactic constraints for
7.120 + type and term variables are declared uniformly, though.
7.121 +
7.122 + \item @{ML Variable.declare_constraints}~@{text "t ctxt"} declares
7.123 + syntactic constraints from term @{text "t"}, without making it part
7.124 + of the context yet.
7.125 +
7.126 + \item @{ML Variable.export}~@{text "inner outer thms"} generalizes
7.127 + fixed type and term variables in @{text "thms"} according to the
7.128 + difference of the @{text "inner"} and @{text "outer"} context,
7.129 + following the principles sketched above.
7.130 +
7.131 + \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type
7.132 + variables in @{text "ts"} as far as possible, even those occurring
7.133 + in fixed term variables. The default policy of type-inference is to
7.134 + fix newly introduced type variables, which is essentially reversed
7.135 + with @{ML Variable.polymorphic}: here the given terms are detached
7.136 + from the context as far as possible.
7.137 +
7.138 + \item @{ML Variable.import_thms}~@{text "open thms ctxt"} invents fixed
7.139 + type and term variables for the schematic ones occurring in @{text
7.140 + "thms"}. The @{text "open"} flag indicates whether the fixed names
7.141 + should be accessible to the user, otherwise newly introduced names
7.142 + are marked as ``internal'' (\secref{sec:names}).
7.143 +
7.144 + \item @{ML Variable.focus}~@{text B} decomposes the outermost @{text
7.145 + "\<And>"} prefix of proposition @{text "B"}.
7.146 +
7.147 + \end{description}
7.148 +*}
7.149 +
7.150 +
7.151 +section {* Assumptions \label{sec:assumptions} *}
7.152 +
7.153 +text {*
7.154 + An \emph{assumption} is a proposition that it is postulated in the
7.155 + current context. Local conclusions may use assumptions as
7.156 + additional facts, but this imposes implicit hypotheses that weaken
7.157 + the overall statement.
7.158 +
7.159 + Assumptions are restricted to fixed non-schematic statements, i.e.\
7.160 + all generality needs to be expressed by explicit quantifiers.
7.161 + Nevertheless, the result will be in HHF normal form with outermost
7.162 + quantifiers stripped. For example, by assuming @{text "\<And>x :: \<alpha>. P
7.163 + x"} we get @{text "\<And>x :: \<alpha>. P x \<turnstile> P ?x"} for schematic @{text "?x"}
7.164 + of fixed type @{text "\<alpha>"}. Local derivations accumulate more and
7.165 + more explicit references to hypotheses: @{text "A\<^isub>1, \<dots>,
7.166 + A\<^isub>n \<turnstile> B"} where @{text "A\<^isub>1, \<dots>, A\<^isub>n"} needs to
7.167 + be covered by the assumptions of the current context.
7.168 +
7.169 + \medskip The @{text "add_assms"} operation augments the context by
7.170 + local assumptions, which are parameterized by an arbitrary @{text
7.171 + "export"} rule (see below).
7.172 +
7.173 + The @{text "export"} operation moves facts from a (larger) inner
7.174 + context into a (smaller) outer context, by discharging the
7.175 + difference of the assumptions as specified by the associated export
7.176 + rules. Note that the discharged portion is determined by the
7.177 + difference contexts, not the facts being exported! There is a
7.178 + separate flag to indicate a goal context, where the result is meant
7.179 + to refine an enclosing sub-goal of a structured proof state.
7.180 +
7.181 + \medskip The most basic export rule discharges assumptions directly
7.182 + by means of the @{text "\<Longrightarrow>"} introduction rule:
7.183 + \[
7.184 + \infer[(@{text "\<Longrightarrow>_intro"})]{@{text "\<Gamma> \\ A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
7.185 + \]
7.186 +
7.187 + The variant for goal refinements marks the newly introduced
7.188 + premises, which causes the canonical Isar goal refinement scheme to
7.189 + enforce unification with local premises within the goal:
7.190 + \[
7.191 + \infer[(@{text "#\<Longrightarrow>_intro"})]{@{text "\<Gamma> \\ A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
7.192 + \]
7.193 +
7.194 + \medskip Alternative versions of assumptions may perform arbitrary
7.195 + transformations on export, as long as the corresponding portion of
7.196 + hypotheses is removed from the given facts. For example, a local
7.197 + definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"},
7.198 + with the following export rule to reverse the effect:
7.199 + \[
7.200 + \infer[(@{text "\<equiv>-expand"})]{@{text "\<Gamma> \\ x \<equiv> t \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
7.201 + \]
7.202 + This works, because the assumption @{text "x \<equiv> t"} was introduced in
7.203 + a context with @{text "x"} being fresh, so @{text "x"} does not
7.204 + occur in @{text "\<Gamma>"} here.
7.205 +*}
7.206 +
7.207 +text %mlref {*
7.208 + \begin{mldecls}
7.209 + @{index_ML_type Assumption.export} \\
7.210 + @{index_ML Assumption.assume: "cterm -> thm"} \\
7.211 + @{index_ML Assumption.add_assms:
7.212 + "Assumption.export ->
7.213 + cterm list -> Proof.context -> thm list * Proof.context"} \\
7.214 + @{index_ML Assumption.add_assumes: "
7.215 + cterm list -> Proof.context -> thm list * Proof.context"} \\
7.216 + @{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
7.217 + \end{mldecls}
7.218 +
7.219 + \begin{description}
7.220 +
7.221 + \item @{ML_type Assumption.export} represents arbitrary export
7.222 + rules, which is any function of type @{ML_type "bool -> cterm list -> thm -> thm"},
7.223 + where the @{ML_type "bool"} indicates goal mode, and the @{ML_type
7.224 + "cterm list"} the collection of assumptions to be discharged
7.225 + simultaneously.
7.226 +
7.227 + \item @{ML Assumption.assume}~@{text "A"} turns proposition @{text
7.228 + "A"} into a raw assumption @{text "A \<turnstile> A'"}, where the conclusion
7.229 + @{text "A'"} is in HHF normal form.
7.230 +
7.231 + \item @{ML Assumption.add_assms}~@{text "r As"} augments the context
7.232 + by assumptions @{text "As"} with export rule @{text "r"}. The
7.233 + resulting facts are hypothetical theorems as produced by the raw
7.234 + @{ML Assumption.assume}.
7.235 +
7.236 + \item @{ML Assumption.add_assumes}~@{text "As"} is a special case of
7.237 + @{ML Assumption.add_assms} where the export rule performs @{text
7.238 + "\<Longrightarrow>_intro"} or @{text "#\<Longrightarrow>_intro"}, depending on goal mode.
7.239 +
7.240 + \item @{ML Assumption.export}~@{text "is_goal inner outer thm"}
7.241 + exports result @{text "thm"} from the the @{text "inner"} context
7.242 + back into the @{text "outer"} one; @{text "is_goal = true"} means
7.243 + this is a goal context. The result is in HHF normal form. Note
7.244 + that @{ML "ProofContext.export"} combines @{ML "Variable.export"}
7.245 + and @{ML "Assumption.export"} in the canonical way.
7.246 +
7.247 + \end{description}
7.248 +*}
7.249 +
7.250 +
7.251 +section {* Results \label{sec:results} *}
7.252 +
7.253 +text {*
7.254 + Local results are established by monotonic reasoning from facts
7.255 + within a context. This allows common combinations of theorems,
7.256 + e.g.\ via @{text "\<And>/\<Longrightarrow>"} elimination, resolution rules, or equational
7.257 + reasoning, see \secref{sec:thms}. Unaccounted context manipulations
7.258 + should be avoided, notably raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc
7.259 + references to free variables or assumptions not present in the proof
7.260 + context.
7.261 +
7.262 + \medskip The @{text "SUBPROOF"} combinator allows to structure a
7.263 + tactical proof recursively by decomposing a selected sub-goal:
7.264 + @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"}
7.265 + after fixing @{text "x"} and assuming @{text "A(x)"}. This means
7.266 + the tactic needs to solve the conclusion, but may use the premise as
7.267 + a local fact, for locally fixed variables.
7.268 +
7.269 + The @{text "prove"} operation provides an interface for structured
7.270 + backwards reasoning under program control, with some explicit sanity
7.271 + checks of the result. The goal context can be augmented by
7.272 + additional fixed variables (cf.\ \secref{sec:variables}) and
7.273 + assumptions (cf.\ \secref{sec:assumptions}), which will be available
7.274 + as local facts during the proof and discharged into implications in
7.275 + the result. Type and term variables are generalized as usual,
7.276 + according to the context.
7.277 +
7.278 + The @{text "obtain"} operation produces results by eliminating
7.279 + existing facts by means of a given tactic. This acts like a dual
7.280 + conclusion: the proof demonstrates that the context may be augmented
7.281 + by certain fixed variables and assumptions. See also
7.282 + \cite{isabelle-isar-ref} for the user-level @{text "\<OBTAIN>"} and
7.283 + @{text "\<GUESS>"} elements. Final results, which may not refer to
7.284 + the parameters in the conclusion, need to exported explicitly into
7.285 + the original context.
7.286 +*}
7.287 +
7.288 +text %mlref {*
7.289 + \begin{mldecls}
7.290 + @{index_ML SUBPROOF:
7.291 + "({context: Proof.context, schematics: ctyp list * cterm list,
7.292 + params: cterm list, asms: cterm list, concl: cterm,
7.293 + prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} \\
7.294 + \end{mldecls}
7.295 + \begin{mldecls}
7.296 + @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
7.297 + ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
7.298 + @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
7.299 + ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
7.300 + \end{mldecls}
7.301 + \begin{mldecls}
7.302 + @{index_ML Obtain.result: "(Proof.context -> tactic) ->
7.303 + thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} \\
7.304 + \end{mldecls}
7.305 +
7.306 + \begin{description}
7.307 +
7.308 + \item @{ML SUBPROOF}~@{text "tac ctxt i"} decomposes the structure
7.309 + of the specified sub-goal, producing an extended context and a
7.310 + reduced goal, which needs to be solved by the given tactic. All
7.311 + schematic parameters of the goal are imported into the context as
7.312 + fixed ones, which may not be instantiated in the sub-proof.
7.313 +
7.314 + \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
7.315 + "C"} in the context augmented by fixed variables @{text "xs"} and
7.316 + assumptions @{text "As"}, and applies tactic @{text "tac"} to solve
7.317 + it. The latter may depend on the local assumptions being presented
7.318 + as facts. The result is in HHF normal form.
7.319 +
7.320 + \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
7.321 + states several conclusions simultaneously. The goal is encoded by
7.322 + means of Pure conjunction; @{ML Goal.conjunction_tac} will turn this
7.323 + into a collection of individual subgoals.
7.324 +
7.325 + \item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the
7.326 + given facts using a tactic, which results in additional fixed
7.327 + variables and assumptions in the context. Final results need to be
7.328 + exported explicitly.
7.329 +
7.330 + \end{description}
7.331 +*}
7.332 +
7.333 +end
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Thu Mar 05 02:32:46 2009 +0100
8.3 @@ -0,0 +1,405 @@
8.4 +theory Tactic
8.5 +imports Base
8.6 +begin
8.7 +
8.8 +chapter {* Tactical reasoning *}
8.9 +
8.10 +text {*
8.11 + Tactical reasoning works by refining the initial claim in a
8.12 + backwards fashion, until a solved form is reached. A @{text "goal"}
8.13 + consists of several subgoals that need to be solved in order to
8.14 + achieve the main statement; zero subgoals means that the proof may
8.15 + be finished. A @{text "tactic"} is a refinement operation that maps
8.16 + a goal to a lazy sequence of potential successors. A @{text
8.17 + "tactical"} is a combinator for composing tactics.
8.18 +*}
8.19 +
8.20 +
8.21 +section {* Goals \label{sec:tactical-goals} *}
8.22 +
8.23 +text {*
8.24 + Isabelle/Pure represents a goal as a theorem stating that the
8.25 + subgoals imply the main goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow>
8.26 + C"}. The outermost goal structure is that of a Horn Clause: i.e.\
8.27 + an iterated implication without any quantifiers\footnote{Recall that
8.28 + outermost @{text "\<And>x. \<phi>[x]"} is always represented via schematic
8.29 + variables in the body: @{text "\<phi>[?x]"}. These variables may get
8.30 + instantiated during the course of reasoning.}. For @{text "n = 0"}
8.31 + a goal is called ``solved''.
8.32 +
8.33 + The structure of each subgoal @{text "A\<^sub>i"} is that of a
8.34 + general Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots>
8.35 + \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"}. Here @{text
8.36 + "x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\
8.37 + arbitrary-but-fixed entities of certain types, and @{text
8.38 + "H\<^sub>1, \<dots>, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may
8.39 + be assumed locally. Together, this forms the goal context of the
8.40 + conclusion @{text B} to be established. The goal hypotheses may be
8.41 + again arbitrary Hereditary Harrop Formulas, although the level of
8.42 + nesting rarely exceeds 1--2 in practice.
8.43 +
8.44 + The main conclusion @{text C} is internally marked as a protected
8.45 + proposition, which is represented explicitly by the notation @{text
8.46 + "#C"}. This ensures that the decomposition into subgoals and main
8.47 + conclusion is well-defined for arbitrarily structured claims.
8.48 +
8.49 + \medskip Basic goal management is performed via the following
8.50 + Isabelle/Pure rules:
8.51 +
8.52 + \[
8.53 + \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
8.54 + \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}
8.55 + \]
8.56 +
8.57 + \medskip The following low-level variants admit general reasoning
8.58 + with protected propositions:
8.59 +
8.60 + \[
8.61 + \infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad
8.62 + \infer[@{text "(conclude)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}
8.63 + \]
8.64 +*}
8.65 +
8.66 +text %mlref {*
8.67 + \begin{mldecls}
8.68 + @{index_ML Goal.init: "cterm -> thm"} \\
8.69 + @{index_ML Goal.finish: "thm -> thm"} \\
8.70 + @{index_ML Goal.protect: "thm -> thm"} \\
8.71 + @{index_ML Goal.conclude: "thm -> thm"} \\
8.72 + \end{mldecls}
8.73 +
8.74 + \begin{description}
8.75 +
8.76 + \item @{ML "Goal.init"}~@{text C} initializes a tactical goal from
8.77 + the well-formed proposition @{text C}.
8.78 +
8.79 + \item @{ML "Goal.finish"}~@{text "thm"} checks whether theorem
8.80 + @{text "thm"} is a solved goal (no subgoals), and concludes the
8.81 + result by removing the goal protection.
8.82 +
8.83 + \item @{ML "Goal.protect"}~@{text "thm"} protects the full statement
8.84 + of theorem @{text "thm"}.
8.85 +
8.86 + \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal
8.87 + protection, even if there are pending subgoals.
8.88 +
8.89 + \end{description}
8.90 +*}
8.91 +
8.92 +
8.93 +section {* Tactics *}
8.94 +
8.95 +text {* A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that
8.96 + maps a given goal state (represented as a theorem, cf.\
8.97 + \secref{sec:tactical-goals}) to a lazy sequence of potential
8.98 + successor states. The underlying sequence implementation is lazy
8.99 + both in head and tail, and is purely functional in \emph{not}
8.100 + supporting memoing.\footnote{The lack of memoing and the strict
8.101 + nature of SML requires some care when working with low-level
8.102 + sequence operations, to avoid duplicate or premature evaluation of
8.103 + results.}
8.104 +
8.105 + An \emph{empty result sequence} means that the tactic has failed: in
8.106 + a compound tactic expressions other tactics might be tried instead,
8.107 + or the whole refinement step might fail outright, producing a
8.108 + toplevel error message. When implementing tactics from scratch, one
8.109 + should take care to observe the basic protocol of mapping regular
8.110 + error conditions to an empty result; only serious faults should
8.111 + emerge as exceptions.
8.112 +
8.113 + By enumerating \emph{multiple results}, a tactic can easily express
8.114 + the potential outcome of an internal search process. There are also
8.115 + combinators for building proof tools that involve search
8.116 + systematically, see also \secref{sec:tacticals}.
8.117 +
8.118 + \medskip As explained in \secref{sec:tactical-goals}, a goal state
8.119 + essentially consists of a list of subgoals that imply the main goal
8.120 + (conclusion). Tactics may operate on all subgoals or on a
8.121 + particularly specified subgoal, but must not change the main
8.122 + conclusion (apart from instantiating schematic goal variables).
8.123 +
8.124 + Tactics with explicit \emph{subgoal addressing} are of the form
8.125 + @{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal
8.126 + (counting from 1). If the subgoal number is out of range, the
8.127 + tactic should fail with an empty result sequence, but must not raise
8.128 + an exception!
8.129 +
8.130 + Operating on a particular subgoal means to replace it by an interval
8.131 + of zero or more subgoals in the same place; other subgoals must not
8.132 + be affected, apart from instantiating schematic variables ranging
8.133 + over the whole goal state.
8.134 +
8.135 + A common pattern of composing tactics with subgoal addressing is to
8.136 + try the first one, and then the second one only if the subgoal has
8.137 + not been solved yet. Special care is required here to avoid bumping
8.138 + into unrelated subgoals that happen to come after the original
8.139 + subgoal. Assuming that there is only a single initial subgoal is a
8.140 + very common error when implementing tactics!
8.141 +
8.142 + Tactics with internal subgoal addressing should expose the subgoal
8.143 + index as @{text "int"} argument in full generality; a hardwired
8.144 + subgoal 1 inappropriate.
8.145 +
8.146 + \medskip The main well-formedness conditions for proper tactics are
8.147 + summarized as follows.
8.148 +
8.149 + \begin{itemize}
8.150 +
8.151 + \item General tactic failure is indicated by an empty result, only
8.152 + serious faults may produce an exception.
8.153 +
8.154 + \item The main conclusion must not be changed, apart from
8.155 + instantiating schematic variables.
8.156 +
8.157 + \item A tactic operates either uniformly on all subgoals, or
8.158 + specifically on a selected subgoal (without bumping into unrelated
8.159 + subgoals).
8.160 +
8.161 + \item Range errors in subgoal addressing produce an empty result.
8.162 +
8.163 + \end{itemize}
8.164 +
8.165 + Some of these conditions are checked by higher-level goal
8.166 + infrastructure (\secref{sec:results}); others are not checked
8.167 + explicitly, and violating them merely results in ill-behaved tactics
8.168 + experienced by the user (e.g.\ tactics that insist in being
8.169 + applicable only to singleton goals, or disallow composition with
8.170 + basic tacticals).
8.171 +*}
8.172 +
8.173 +text %mlref {*
8.174 + \begin{mldecls}
8.175 + @{index_ML_type tactic: "thm -> thm Seq.seq"} \\
8.176 + @{index_ML no_tac: tactic} \\
8.177 + @{index_ML all_tac: tactic} \\
8.178 + @{index_ML print_tac: "string -> tactic"} \\[1ex]
8.179 + @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
8.180 + @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
8.181 + @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
8.182 + \end{mldecls}
8.183 +
8.184 + \begin{description}
8.185 +
8.186 + \item @{ML_type tactic} represents tactics. The well-formedness
8.187 + conditions described above need to be observed. See also @{"file"
8.188 + "~~/src/Pure/General/seq.ML"} for the underlying implementation of
8.189 + lazy sequences.
8.190 +
8.191 + \item @{ML_type "int -> tactic"} represents tactics with explicit
8.192 + subgoal addressing, with well-formedness conditions as described
8.193 + above.
8.194 +
8.195 + \item @{ML no_tac} is a tactic that always fails, returning the
8.196 + empty sequence.
8.197 +
8.198 + \item @{ML all_tac} is a tactic that always succeeds, returning a
8.199 + singleton sequence with unchanged goal state.
8.200 +
8.201 + \item @{ML print_tac}~@{text "message"} is like @{ML all_tac}, but
8.202 + prints a message together with the goal state on the tracing
8.203 + channel.
8.204 +
8.205 + \item @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule
8.206 + into a tactic with unique result. Exception @{ML THM} is considered
8.207 + a regular tactic failure and produces an empty result; other
8.208 + exceptions are passed through.
8.209 +
8.210 + \item @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the
8.211 + most basic form to produce a tactic with subgoal addressing. The
8.212 + given abstraction over the subgoal term and subgoal number allows to
8.213 + peek at the relevant information of the full goal state. The
8.214 + subgoal range is checked as required above.
8.215 +
8.216 + \item @{ML CSUBGOAL} is similar to @{ML SUBGOAL}, but passes the
8.217 + subgoal as @{ML_type cterm} instead of raw @{ML_type term}. This
8.218 + avoids expensive re-certification in situations where the subgoal is
8.219 + used directly for primitive inferences.
8.220 +
8.221 + \end{description}
8.222 +*}
8.223 +
8.224 +
8.225 +subsection {* Resolution and assumption tactics \label{sec:resolve-assume-tac} *}
8.226 +
8.227 +text {* \emph{Resolution} is the most basic mechanism for refining a
8.228 + subgoal using a theorem as object-level rule.
8.229 + \emph{Elim-resolution} is particularly suited for elimination rules:
8.230 + it resolves with a rule, proves its first premise by assumption, and
8.231 + finally deletes that assumption from any new subgoals.
8.232 + \emph{Destruct-resolution} is like elim-resolution, but the given
8.233 + destruction rules are first turned into canonical elimination
8.234 + format. \emph{Forward-resolution} is like destruct-resolution, but
8.235 + without deleting the selected assumption. The @{text "r/e/d/f"}
8.236 + naming convention is maintained for several different kinds of
8.237 + resolution rules and tactics.
8.238 +
8.239 + Assumption tactics close a subgoal by unifying some of its premises
8.240 + against its conclusion.
8.241 +
8.242 + \medskip All the tactics in this section operate on a subgoal
8.243 + designated by a positive integer. Other subgoals might be affected
8.244 + indirectly, due to instantiation of schematic variables.
8.245 +
8.246 + There are various sources of non-determinism, the tactic result
8.247 + sequence enumerates all possibilities of the following choices (if
8.248 + applicable):
8.249 +
8.250 + \begin{enumerate}
8.251 +
8.252 + \item selecting one of the rules given as argument to the tactic;
8.253 +
8.254 + \item selecting a subgoal premise to eliminate, unifying it against
8.255 + the first premise of the rule;
8.256 +
8.257 + \item unifying the conclusion of the subgoal to the conclusion of
8.258 + the rule.
8.259 +
8.260 + \end{enumerate}
8.261 +
8.262 + Recall that higher-order unification may produce multiple results
8.263 + that are enumerated here.
8.264 +*}
8.265 +
8.266 +text %mlref {*
8.267 + \begin{mldecls}
8.268 + @{index_ML resolve_tac: "thm list -> int -> tactic"} \\
8.269 + @{index_ML eresolve_tac: "thm list -> int -> tactic"} \\
8.270 + @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\
8.271 + @{index_ML forward_tac: "thm list -> int -> tactic"} \\[1ex]
8.272 + @{index_ML assume_tac: "int -> tactic"} \\
8.273 + @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
8.274 + @{index_ML match_tac: "thm list -> int -> tactic"} \\
8.275 + @{index_ML ematch_tac: "thm list -> int -> tactic"} \\
8.276 + @{index_ML dmatch_tac: "thm list -> int -> tactic"} \\
8.277 + \end{mldecls}
8.278 +
8.279 + \begin{description}
8.280 +
8.281 + \item @{ML resolve_tac}~@{text "thms i"} refines the goal state
8.282 + using the given theorems, which should normally be introduction
8.283 + rules. The tactic resolves a rule's conclusion with subgoal @{text
8.284 + i}, replacing it by the corresponding versions of the rule's
8.285 + premises.
8.286 +
8.287 + \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution
8.288 + with the given theorems, which should normally be elimination rules.
8.289 +
8.290 + \item @{ML dresolve_tac}~@{text "thms i"} performs
8.291 + destruct-resolution with the given theorems, which should normally
8.292 + be destruction rules. This replaces an assumption by the result of
8.293 + applying one of the rules.
8.294 +
8.295 + \item @{ML forward_tac} is like @{ML dresolve_tac} except that the
8.296 + selected assumption is not deleted. It applies a rule to an
8.297 + assumption, adding the result as a new assumption.
8.298 +
8.299 + \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}
8.300 + by assumption (modulo higher-order unification).
8.301 +
8.302 + \item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks
8.303 + only for immediate @{text "\<alpha>"}-convertibility instead of using
8.304 + unification. It succeeds (with a unique next state) if one of the
8.305 + assumptions is equal to the subgoal's conclusion. Since it does not
8.306 + instantiate variables, it cannot make other subgoals unprovable.
8.307 +
8.308 + \item @{ML match_tac}, @{ML ematch_tac}, and @{ML dmatch_tac} are
8.309 + similar to @{ML resolve_tac}, @{ML eresolve_tac}, and @{ML
8.310 + dresolve_tac}, respectively, but do not instantiate schematic
8.311 + variables in the goal state.
8.312 +
8.313 + Flexible subgoals are not updated at will, but are left alone.
8.314 + Strictly speaking, matching means to treat the unknowns in the goal
8.315 + state as constants; these tactics merely discard unifiers that would
8.316 + update the goal state.
8.317 +
8.318 + \end{description}
8.319 +*}
8.320 +
8.321 +
8.322 +subsection {* Explicit instantiation within a subgoal context *}
8.323 +
8.324 +text {* The main resolution tactics (\secref{sec:resolve-assume-tac})
8.325 + use higher-order unification, which works well in many practical
8.326 + situations despite its daunting theoretical properties.
8.327 + Nonetheless, there are important problem classes where unguided
8.328 + higher-order unification is not so useful. This typically involves
8.329 + rules like universal elimination, existential introduction, or
8.330 + equational substitution. Here the unification problem involves
8.331 + fully flexible @{text "?P ?x"} schemes, which are hard to manage
8.332 + without further hints.
8.333 +
8.334 + By providing a (small) rigid term for @{text "?x"} explicitly, the
8.335 + remaining unification problem is to assign a (large) term to @{text
8.336 + "?P"}, according to the shape of the given subgoal. This is
8.337 + sufficiently well-behaved in most practical situations.
8.338 +
8.339 + \medskip Isabelle provides separate versions of the standard @{text
8.340 + "r/e/d/f"} resolution tactics that allow to provide explicit
8.341 + instantiations of unknowns of the given rule, wrt.\ terms that refer
8.342 + to the implicit context of the selected subgoal.
8.343 +
8.344 + An instantiation consists of a list of pairs of the form @{text
8.345 + "(?x, t)"}, where @{text ?x} is a schematic variable occurring in
8.346 + the given rule, and @{text t} is a term from the current proof
8.347 + context, augmented by the local goal parameters of the selected
8.348 + subgoal; cf.\ the @{text "focus"} operation described in
8.349 + \secref{sec:variables}.
8.350 +
8.351 + Entering the syntactic context of a subgoal is a brittle operation,
8.352 + because its exact form is somewhat accidental, and the choice of
8.353 + bound variable names depends on the presence of other local and
8.354 + global names. Explicit renaming of subgoal parameters prior to
8.355 + explicit instantiation might help to achieve a bit more robustness.
8.356 +
8.357 + Type instantiations may be given as well, via pairs like @{text
8.358 + "(?'a, \<tau>)"}. Type instantiations are distinguished from term
8.359 + instantiations by the syntactic form of the schematic variable.
8.360 + Types are instantiated before terms are. Since term instantiation
8.361 + already performs type-inference as expected, explicit type
8.362 + instantiations are seldom necessary.
8.363 +*}
8.364 +
8.365 +text %mlref {*
8.366 + \begin{mldecls}
8.367 + @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
8.368 + @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
8.369 + @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
8.370 + @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\[1ex]
8.371 + @{index_ML rename_tac: "string list -> int -> tactic"} \\
8.372 + \end{mldecls}
8.373 +
8.374 + \begin{description}
8.375 +
8.376 + \item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the
8.377 + rule @{text thm} with the instantiations @{text insts}, as described
8.378 + above, and then performs resolution on subgoal @{text i}.
8.379 +
8.380 + \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs
8.381 + elim-resolution.
8.382 +
8.383 + \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs
8.384 + destruct-resolution.
8.385 +
8.386 + \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that
8.387 + the selected assumption is not deleted.
8.388 +
8.389 + \item @{ML rename_tac}~@{text "names i"} renames the innermost
8.390 + parameters of subgoal @{text i} according to the provided @{text
8.391 + names} (which need to be distinct indentifiers).
8.392 +
8.393 + \end{description}
8.394 +*}
8.395 +
8.396 +
8.397 +section {* Tacticals \label{sec:tacticals} *}
8.398 +
8.399 +text {*
8.400 + A \emph{tactical} is a functional combinator for building up complex
8.401 + tactics from simpler ones. Typical tactical perform sequential
8.402 + composition, disjunction (choice), iteration, or goal addressing.
8.403 + Various search strategies may be expressed via tacticals.
8.404 +
8.405 + \medskip FIXME
8.406 +*}
8.407 +
8.408 +end
9.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex Wed Mar 04 17:12:23 2009 -0800
9.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu Mar 05 02:32:46 2009 +0100
9.3 @@ -785,7 +785,6 @@
9.4 \isadelimtheory
9.5 %
9.6 \endisadelimtheory
9.7 -\isanewline
9.8 \end{isabellebody}%
9.9 %%% Local Variables:
9.10 %%% mode: latex
10.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex Wed Mar 04 17:12:23 2009 -0800
10.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Thu Mar 05 02:32:46 2009 +0100
10.3 @@ -503,7 +503,7 @@
10.4 \item \hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}} defines a named simplification
10.5 procedure that is invoked by the Simplifier whenever any of the
10.6 given term patterns match the current redex. The implementation,
10.7 - which is provided as ML source text, needs to be of type \verb|"morphism -> simpset -> cterm -> thm option"|, where the \verb|cterm| represents the current redex \isa{r} and the result is
10.8 + which is provided as ML source text, needs to be of type \verb|morphism -> simpset -> cterm -> thm option|, where the \verb|cterm| represents the current redex \isa{r} and the result is
10.9 supposed to be some proven rewrite rule \isa{{\isachardoublequote}r\ {\isasymequiv}\ r{\isacharprime}{\isachardoublequote}} (or a
10.10 generalized version), or \verb|NONE| to indicate failure. The
10.11 \verb|simpset| argument holds the full context of the current