1.1 --- a/doc-src/IsarRef/Makefile Thu Jan 03 17:01:59 2002 +0100
1.2 +++ b/doc-src/IsarRef/Makefile Thu Jan 03 17:48:02 2002 +0100
1.3 @@ -14,7 +14,7 @@
1.4 NAME = isar-ref
1.5
1.6 FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
1.7 - generic.tex hol.tex zf.tex refcard.tex conversion.tex \
1.8 + generic.tex logics.tex refcard.tex conversion.tex \
1.9 ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \
1.10 ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
1.11
2.1 --- a/doc-src/IsarRef/conversion.tex Thu Jan 03 17:01:59 2002 +0100
2.2 +++ b/doc-src/IsarRef/conversion.tex Thu Jan 03 17:48:02 2002 +0100
2.3 @@ -508,7 +508,7 @@
2.4 declare the theorem otherwise later (e.g.\ as $[simp~del]$).
2.5
2.6
2.7 -\section{Converting to actual Isar proof texts}
2.8 +\section{Writing actual Isar proof texts}
2.9
2.10 Porting legacy ML proof scripts into Isar tactic emulation scripts (see
2.11 \S\ref{sec:port-scripts}) is mainly a technical issue, since the basic
3.1 --- a/doc-src/IsarRef/generic.tex Thu Jan 03 17:01:59 2002 +0100
3.2 +++ b/doc-src/IsarRef/generic.tex Thu Jan 03 17:48:02 2002 +0100
3.3 @@ -1,7 +1,7 @@
3.4
3.5 \chapter{Generic Tools and Packages}\label{ch:gen-tools}
3.6
3.7 -\section{Theory commands}
3.8 +\section{Theory specification commands}
3.9
3.10 \subsection{Axiomatic type classes}\label{sec:axclass}
3.11
3.12 @@ -57,10 +57,62 @@
3.13
3.14 FIXME
3.15
3.16 +\indexouternonterm{contextelem}
3.17
3.18 -\section{Proof commands}
3.19
3.20 -\subsection{Calculational Reasoning}\label{sec:calculation}
3.21 +\section{Derived proof schemes}
3.22 +
3.23 +\subsection{Generalized elimination}\label{sec:obtain}
3.24 +
3.25 +\indexisarcmd{obtain}
3.26 +\begin{matharray}{rcl}
3.27 + \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
3.28 +\end{matharray}
3.29 +
3.30 +Generalized elimination means that additional elements with certain properties
3.31 +may introduced in the current context, by virtue of a locally proven
3.32 +``soundness statement''. Technically speaking, the $\OBTAINNAME$ language
3.33 +element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see
3.34 +\S\ref{sec:proof-context}), together with a soundness proof of its additional
3.35 +claim. According to the nature of existential reasoning, assumptions get
3.36 +eliminated from any result exported from the context later, provided that the
3.37 +corresponding parameters do \emph{not} occur in the conclusion.
3.38 +
3.39 +\begin{rail}
3.40 + 'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and')
3.41 + ;
3.42 +\end{rail}
3.43 +
3.44 +$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
3.45 +shall refer to (optional) facts indicated for forward chaining.
3.46 +\begin{matharray}{l}
3.47 + \langle facts~\vec b\rangle \\
3.48 + \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
3.49 + \quad \BG \\
3.50 + \qquad \FIX{thesis} \\
3.51 + \qquad \ASSUME{that~[simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
3.52 + \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
3.53 + \quad \EN \\
3.54 + \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
3.55 +\end{matharray}
3.56 +
3.57 +Typically, the soundness proof is relatively straight-forward, often just by
3.58 +canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
3.59 +$\BY{blast}$ (see \S\ref{sec:classical-auto}). Accordingly, the ``$that$''
3.60 +reduction above is declared as simplification and introduction rule.
3.61 +
3.62 +\medskip
3.63 +
3.64 +In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
3.65 +meta-logical existential quantifiers and conjunctions. This concept has a
3.66 +broad range of useful applications, ranging from plain elimination (or even
3.67 +introduction) of object-level existentials and conjunctions, to elimination
3.68 +over results of symbolic evaluation of recursive definitions, for example.
3.69 +Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
3.70 +where the result is treated as an assumption.
3.71 +
3.72 +
3.73 +\subsection{Calculational reasoning}\label{sec:calculation}
3.74
3.75 \indexisarcmd{also}\indexisarcmd{finally}
3.76 \indexisarcmd{moreover}\indexisarcmd{ultimately}
3.77 @@ -150,55 +202,7 @@
3.78 \end{descr}
3.79
3.80
3.81 -\subsection{Generalized elimination}\label{sec:obtain}
3.82 -
3.83 -\indexisarcmd{obtain}
3.84 -\begin{matharray}{rcl}
3.85 - \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
3.86 -\end{matharray}
3.87 -
3.88 -Generalized elimination means that additional elements with certain properties
3.89 -may introduced in the current context, by virtue of a locally proven
3.90 -``soundness statement''. Technically speaking, the $\OBTAINNAME$ language
3.91 -element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see
3.92 -\S\ref{sec:proof-context}), together with a soundness proof of its additional
3.93 -claim. According to the nature of existential reasoning, assumptions get
3.94 -eliminated from any result exported from the context later, provided that the
3.95 -corresponding parameters do \emph{not} occur in the conclusion.
3.96 -
3.97 -\begin{rail}
3.98 - 'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and')
3.99 - ;
3.100 -\end{rail}
3.101 -
3.102 -$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
3.103 -shall refer to (optional) facts indicated for forward chaining.
3.104 -\begin{matharray}{l}
3.105 - \langle facts~\vec b\rangle \\
3.106 - \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
3.107 - \quad \BG \\
3.108 - \qquad \FIX{thesis} \\
3.109 - \qquad \ASSUME{that~[simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
3.110 - \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
3.111 - \quad \EN \\
3.112 - \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
3.113 -\end{matharray}
3.114 -
3.115 -Typically, the soundness proof is relatively straight-forward, often just by
3.116 -canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
3.117 -$\BY{blast}$ (see \S\ref{sec:classical-auto}). Accordingly, the ``$that$''
3.118 -reduction above is declared as simplification and introduction rule.
3.119 -
3.120 -\medskip
3.121 -
3.122 -In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
3.123 -meta-logical existential quantifiers and conjunctions. This concept has a
3.124 -broad range of useful applications, ranging from plain elimination (or even
3.125 -introduction) of object-level existentials and conjunctions, to elimination
3.126 -over results of symbolic evaluation of recursive definitions, for example.
3.127 -Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
3.128 -where the result is treated as an assumption.
3.129 -
3.130 +\section{Specific proof tools}
3.131
3.132 \subsection{Miscellaneous methods and attributes}\label{sec:misc-meth-att}
3.133
3.134 @@ -308,7 +312,7 @@
3.135 \end{descr}
3.136
3.137
3.138 -\subsection{Tactic emulations}\label{sec:tactics}
3.139 +\subsection{Further tactic emulations}\label{sec:tactics}
3.140
3.141 The following improper proof methods emulate traditional tactics. These admit
3.142 direct access to the goal state, which is normally considered harmful! In
3.143 @@ -432,11 +436,13 @@
3.144 \end{descr}
3.145
3.146
3.147 -\section{The Simplifier}\label{sec:simplifier}
3.148 +\subsection{The Simplifier}\label{sec:simplifier}
3.149
3.150 -\subsection{Simplification methods}\label{sec:simp}
3.151 +\subsubsection{Basic equational reasoning}
3.152
3.153 -\subsubsection{FIXME}
3.154 +FIXME
3.155 +
3.156 +\subsubsection{Simplification methods}\label{sec:simp}
3.157
3.158 \indexisarmeth{simp}\indexisarmeth{simp-all}
3.159 \begin{matharray}{rcl}
3.160 @@ -509,7 +515,7 @@
3.161 method available for single-step case splitting, see \S\ref{sec:basic-eq}.
3.162
3.163
3.164 -\subsection{Declaring rules}
3.165 +\subsubsection{Declaring rules}
3.166
3.167 \indexisarcmd{print-simpset}
3.168 \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
3.169 @@ -535,7 +541,9 @@
3.170 \end{descr}
3.171
3.172
3.173 -\subsection{Forward simplification}
3.174 +\subsubsection{Forward simplification}
3.175 +
3.176 +FIXME thmargs
3.177
3.178 \indexisaratt{simplified}
3.179 \begin{matharray}{rcl}
3.180 @@ -563,7 +571,9 @@
3.181 \end{descr}
3.182
3.183
3.184 -\section{Basic equational reasoning}\label{sec:basic-eq}
3.185 +\subsubsection{Basic equational reasoning}\label{sec:basic-eq}
3.186 +
3.187 +FIXME move?
3.188
3.189 \indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric}
3.190 \begin{matharray}{rcl}
3.191 @@ -601,9 +611,9 @@
3.192 \end{descr}
3.193
3.194
3.195 -\section{The Classical Reasoner}\label{sec:classical}
3.196 +\subsection{The Classical Reasoner}\label{sec:classical}
3.197
3.198 -\subsection{Basic methods}\label{sec:classical-basic}
3.199 +\subsubsection{Basic methods}\label{sec:classical-basic}
3.200
3.201 \indexisarmeth{rule}\indexisarmeth{intro}
3.202 \indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}
3.203 @@ -642,7 +652,7 @@
3.204 \end{descr}
3.205
3.206
3.207 -\subsection{Automated methods}\label{sec:classical-auto}
3.208 +\subsubsection{Automated methods}\label{sec:classical-auto}
3.209
3.210 \indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
3.211 \indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
3.212 @@ -686,7 +696,7 @@
3.213 \S\ref{sec:simp}).
3.214
3.215
3.216 -\subsection{Combined automated methods}\label{sec:clasimp}
3.217 +\subsubsection{Combined automated methods}\label{sec:clasimp}
3.218
3.219 \indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp}
3.220 \indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp}
3.221 @@ -728,7 +738,7 @@
3.222 \end{descr}
3.223
3.224
3.225 -\subsection{Declaring rules}\label{sec:classical-mod}
3.226 +\subsubsection{Declaring rules}\label{sec:classical-mod}
3.227
3.228 \indexisarcmd{print-claset}
3.229 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
3.230 @@ -780,9 +790,9 @@
3.231 \end{descr}
3.232
3.233
3.234 -\section{Proof by cases and induction}\label{sec:cases-induct}
3.235 +\subsection{Proof by cases and induction}\label{sec:cases-induct}
3.236
3.237 -\subsection{Rule contexts}\label{sec:rule-cases}
3.238 +\subsubsection{Rule contexts}\label{sec:rule-cases}
3.239
3.240 \indexisarcmd{case}\indexisarcmd{print-cases}
3.241 \indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
3.242 @@ -871,7 +881,7 @@
3.243 \end{descr}
3.244
3.245
3.246 -\subsection{Proof methods}\label{sec:cases-induct-meth}
3.247 +\subsubsection{Proof methods}\label{sec:cases-induct-meth}
3.248
3.249 \indexisarmeth{cases}\indexisarmeth{induct}
3.250 \begin{matharray}{rcl}
3.251 @@ -1013,7 +1023,7 @@
3.252 ``$type: name$'' to the method argument.
3.253
3.254
3.255 -\subsection{Declaring rules}\label{sec:cases-induct-att}
3.256 +\subsubsection{Declaring rules}\label{sec:cases-induct-att}
3.257
3.258 \indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
3.259 \begin{matharray}{rcl}
3.260 @@ -1044,83 +1054,6 @@
3.261 automatically (if none had been given already): $consumes~0$ is specified for
3.262 ``type'' rules and $consumes~1$ for ``set'' rules.
3.263
3.264 -
3.265 -\section{Object-logic setup}\label{sec:object-logic}
3.266 -
3.267 -The very starting point for any Isabelle object-logic is a ``truth judgment''
3.268 -that links object-level statements to the meta-logic (with its minimal
3.269 -language of $prop$ that covers universal quantification $\Forall$ and
3.270 -implication $\Imp$). Common object-logics are sufficiently expressive to
3.271 -\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own
3.272 -language. This is useful in certain situations where a rule needs to be
3.273 -viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x
3.274 -\in A \Imp P(x)$ versus $\forall x \in A. P(x)$).
3.275 -
3.276 -From the following language elements, only the $atomize$ method and
3.277 -$rule_format$ attribute are occasionally required by end-users, the rest is
3.278 -mainly for those who need to setup their own object-logic. In the latter case
3.279 -existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as
3.280 -realistic examples.
3.281 -
3.282 -Further generic tools may refer to the information provided by object-logic
3.283 -declarations internally (such as locales \S\ref{sec:locale}, or the Classical
3.284 -Reasoner \S\ref{sec:classical}).
3.285 -
3.286 -\indexisarcmd{judgment}
3.287 -\indexisarmeth{atomize}\indexisaratt{atomize}
3.288 -\indexisaratt{rule-format}\indexisaratt{rulify}
3.289 -
3.290 -\begin{matharray}{rcl}
3.291 - \isarcmd{judgment} & : & \isartrans{theory}{theory} \\
3.292 - atomize & : & \isarmeth \\
3.293 - atomize & : & \isaratt \\
3.294 - rule_format & : & \isaratt \\
3.295 - rulify & : & \isaratt \\
3.296 -\end{matharray}
3.297 -
3.298 -\railalias{ruleformat}{rule\_format}
3.299 -\railterm{ruleformat}
3.300 -
3.301 -\begin{rail}
3.302 - 'judgment' constdecl
3.303 - ;
3.304 - ruleformat ('(' noasm ')')?
3.305 - ;
3.306 -\end{rail}
3.307 -
3.308 -\begin{descr}
3.309 -
3.310 -\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the
3.311 - truth judgment of the current object-logic. Its type $\sigma$ should
3.312 - specify a coercion of the category of object-level propositions to $prop$ of
3.313 - the Pure meta-logic; the mixfix annotation $syn$ would typically just link
3.314 - the object language (internally of syntactic category $logic$) with that of
3.315 - $prop$. Only one $\isarkeyword{judgment}$ declaration may be given in any
3.316 - theory development.
3.317 -
3.318 -\item [$atomize$] (as a method) rewrites any non-atomic premises of a
3.319 - sub-goal, using the meta-level equations that have been declared via
3.320 - $atomize$ (as an attribute) beforehand. As a result, heavily nested goals
3.321 - become amenable to fundamental operations such as resolution (cf.\ the
3.322 - $rule$ method) and proof-by-assumption (cf.\ $assumption$).
3.323 -
3.324 - A typical collection of $atomize$ rules for a particular object-logic would
3.325 - provide an internalization for each of the connectives of $\Forall$, $\Imp$,
3.326 - $\equiv$; meta-level conjunction expressed as $\All{\PROP\,C} (A \Imp B \Imp
3.327 - \PROP\,C) \Imp PROP\,C$ should be covered as well.
3.328 -
3.329 -\item [$rule_format$] rewrites a theorem by the equalities declared as
3.330 - $rulify$ rules in the current object-logic. By default, the result is fully
3.331 - normalized, including assumptions and conclusions at any depth. The
3.332 - $no_asm$ option restricts the transformation to the conclusion of a rule.
3.333 -
3.334 - In common object logics (HOL, FOL, ZF), the effect of $rule_format$ is to
3.335 - replace (bounded) universal quantification ($\forall$) and implication
3.336 - ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.
3.337 -
3.338 -\end{descr}
3.339 -
3.340 -
3.341 %%% Local Variables:
3.342 %%% mode: latex
3.343 %%% TeX-master: "isar-ref"
4.1 --- a/doc-src/IsarRef/hol.tex Thu Jan 03 17:01:59 2002 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,356 +0,0 @@
4.4 -
4.5 -\chapter{Isabelle/HOL specific elements}\label{ch:hol-tools}
4.6 -
4.7 -\section{Miscellaneous attributes}
4.8 -
4.9 -\indexisarattof{HOL}{split-format}
4.10 -\begin{matharray}{rcl}
4.11 - split_format^* & : & \isaratt \\
4.12 -\end{matharray}
4.13 -
4.14 -\railalias{splitformat}{split\_format}
4.15 -\railterm{splitformat}
4.16 -\railterm{complete}
4.17 -
4.18 -\begin{rail}
4.19 - splitformat (((name * ) + 'and') | ('(' complete ')'))
4.20 - ;
4.21 -\end{rail}
4.22 -
4.23 -\begin{descr}
4.24 -
4.25 -\item [$split_format~\vec p@1 \dots \vec p@n$] puts tuple objects into
4.26 - canonical form as specified by the arguments given; $\vec p@i$ refers to
4.27 - occurrences in premise $i$ of the rule. The $split_format~(complete)$ form
4.28 - causes \emph{all} arguments in function applications to be represented
4.29 - canonically according to their tuple type structure.
4.30 -
4.31 - Note that these operations tend to invent funny names for new local
4.32 - parameters to be introduced.
4.33 -
4.34 -\end{descr}
4.35 -
4.36 -
4.37 -\section{Primitive types}\label{sec:typedef}
4.38 -
4.39 -\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
4.40 -\begin{matharray}{rcl}
4.41 - \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
4.42 - \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
4.43 -\end{matharray}
4.44 -
4.45 -\begin{rail}
4.46 - 'typedecl' typespec infix? comment?
4.47 - ;
4.48 - 'typedef' parname? typespec infix? \\ '=' term comment?
4.49 - ;
4.50 -\end{rail}
4.51 -
4.52 -\begin{descr}
4.53 -\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
4.54 - $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
4.55 - also declares type arity $t :: (term, \dots, term) term$, making $t$ an
4.56 - actual HOL type constructor.
4.57 -\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
4.58 - non-emptiness of the set $A$. After finishing the proof, the theory will be
4.59 - augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL}
4.60 - for more information. Note that user-level theories usually do not directly
4.61 - refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
4.62 - packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and
4.63 - $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
4.64 -\end{descr}
4.65 -
4.66 -
4.67 -\section{Records}\label{sec:hol-record}
4.68 -
4.69 -FIXME proof tools (simp, cases/induct; no split!?);
4.70 -
4.71 -\indexisarcmdof{HOL}{record}
4.72 -\begin{matharray}{rcl}
4.73 - \isarcmd{record} & : & \isartrans{theory}{theory} \\
4.74 -\end{matharray}
4.75 -
4.76 -\begin{rail}
4.77 - 'record' typespec '=' (type '+')? (field +)
4.78 - ;
4.79 -
4.80 - field: name '::' type comment?
4.81 - ;
4.82 -\end{rail}
4.83 -
4.84 -\begin{descr}
4.85 -\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
4.86 - defines extensible record type $(\vec\alpha)t$, derived from the optional
4.87 - parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
4.88 - See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on
4.89 - simply-typed extensible records.
4.90 -\end{descr}
4.91 -
4.92 -
4.93 -\section{Datatypes}\label{sec:hol-datatype}
4.94 -
4.95 -\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
4.96 -\begin{matharray}{rcl}
4.97 - \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
4.98 - \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
4.99 -\end{matharray}
4.100 -
4.101 -\railalias{repdatatype}{rep\_datatype}
4.102 -\railterm{repdatatype}
4.103 -
4.104 -\begin{rail}
4.105 - 'datatype' (dtspec + 'and')
4.106 - ;
4.107 - repdatatype (name * ) dtrules
4.108 - ;
4.109 -
4.110 - dtspec: parname? typespec infix? '=' (cons + '|')
4.111 - ;
4.112 - cons: name (type * ) mixfix? comment?
4.113 - ;
4.114 - dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
4.115 -\end{rail}
4.116 -
4.117 -\begin{descr}
4.118 -\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
4.119 -\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
4.120 - ones, generating the standard infrastructure of derived concepts (primitive
4.121 - recursion etc.).
4.122 -\end{descr}
4.123 -
4.124 -The induction and exhaustion theorems generated provide case names according
4.125 -to the constructors involved, while parameters are named after the types (see
4.126 -also \S\ref{sec:cases-induct}).
4.127 -
4.128 -See \cite{isabelle-HOL} for more details on datatypes. Note that the theory
4.129 -syntax above has been slightly simplified over the old version, usually
4.130 -requiring more quotes and less parentheses. Apart from proper proof methods
4.131 -for case-analysis and induction, there are also emulations of ML tactics
4.132 -\texttt{case_tac} and \texttt{induct_tac} available, see
4.133 -\S\ref{sec:induct_tac}.
4.134 -
4.135 -
4.136 -\section{Recursive functions}\label{sec:recursion}
4.137 -
4.138 -\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
4.139 -\begin{matharray}{rcl}
4.140 - \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
4.141 - \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
4.142 - \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
4.143 -%FIXME
4.144 -% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
4.145 -\end{matharray}
4.146 -
4.147 -\railalias{recdefsimp}{recdef\_simp}
4.148 -\railterm{recdefsimp}
4.149 -
4.150 -\railalias{recdefcong}{recdef\_cong}
4.151 -\railterm{recdefcong}
4.152 -
4.153 -\railalias{recdefwf}{recdef\_wf}
4.154 -\railterm{recdefwf}
4.155 -
4.156 -\railalias{recdeftc}{recdef\_tc}
4.157 -\railterm{recdeftc}
4.158 -
4.159 -\begin{rail}
4.160 - 'primrec' parname? (equation + )
4.161 - ;
4.162 - 'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
4.163 - ;
4.164 - recdeftc thmdecl? tc comment?
4.165 - ;
4.166 -
4.167 - equation: thmdecl? eqn
4.168 - ;
4.169 - eqn: prop comment?
4.170 - ;
4.171 - hints: '(' 'hints' (recdefmod * ) ')'
4.172 - ;
4.173 - recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
4.174 - ;
4.175 - tc: nameref ('(' nat ')')?
4.176 - ;
4.177 -\end{rail}
4.178 -
4.179 -\begin{descr}
4.180 -\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
4.181 - datatypes, see also \cite{isabelle-HOL}.
4.182 -\item [$\isarkeyword{recdef}$] defines general well-founded recursive
4.183 - functions (using the TFL package), see also \cite{isabelle-HOL}. The
4.184 - $(permissive)$ option tells TFL to recover from failed proof attempts,
4.185 - returning unfinished results. The $recdef_simp$, $recdef_cong$, and
4.186 - $recdef_wf$ hints refer to auxiliary rules to be used in the internal
4.187 - automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\
4.188 - \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
4.189 - (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
4.190 - \S\ref{sec:classical}).
4.191 -\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
4.192 - termination condition number $i$ (default $1$) as generated by a
4.193 - $\isarkeyword{recdef}$ definition of constant $c$.
4.194 -
4.195 - Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
4.196 - internal proofs without manual intervention.
4.197 -\end{descr}
4.198 -
4.199 -Both kinds of recursive definitions accommodate reasoning by induction (cf.\
4.200 -\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
4.201 -the function definition) refers to a specific induction rule, with parameters
4.202 -named according to the user-specified equations. Case names of
4.203 -$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
4.204 -$\isarkeyword{recdef}$ are numbered (starting from $1$).
4.205 -
4.206 -The equations provided by these packages may be referred later as theorem list
4.207 -$f\mathord.simps$, where $f$ is the (collective) name of the functions
4.208 -defined. Individual equations may be named explicitly as well; note that for
4.209 -$\isarkeyword{recdef}$ each specification given by the user may result in
4.210 -several theorems.
4.211 -
4.212 -\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
4.213 -the following attributes.
4.214 -
4.215 -\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
4.216 -\begin{matharray}{rcl}
4.217 - recdef_simp & : & \isaratt \\
4.218 - recdef_cong & : & \isaratt \\
4.219 - recdef_wf & : & \isaratt \\
4.220 -\end{matharray}
4.221 -
4.222 -\railalias{recdefsimp}{recdef\_simp}
4.223 -\railterm{recdefsimp}
4.224 -
4.225 -\railalias{recdefcong}{recdef\_cong}
4.226 -\railterm{recdefcong}
4.227 -
4.228 -\railalias{recdefwf}{recdef\_wf}
4.229 -\railterm{recdefwf}
4.230 -
4.231 -\begin{rail}
4.232 - (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
4.233 - ;
4.234 -\end{rail}
4.235 -
4.236 -
4.237 -\section{(Co)Inductive sets}\label{sec:hol-inductive}
4.238 -
4.239 -\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}
4.240 -\begin{matharray}{rcl}
4.241 - \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
4.242 - \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
4.243 - mono & : & \isaratt \\
4.244 -\end{matharray}
4.245 -
4.246 -\railalias{condefs}{con\_defs}
4.247 -\railterm{condefs}
4.248 -
4.249 -\begin{rail}
4.250 - ('inductive' | 'coinductive') sets intros monos?
4.251 - ;
4.252 - 'mono' (() | 'add' | 'del')
4.253 - ;
4.254 -
4.255 - sets: (term comment? +)
4.256 - ;
4.257 - intros: 'intros' (thmdecl? prop comment? +)
4.258 - ;
4.259 - monos: 'monos' thmrefs comment?
4.260 - ;
4.261 -\end{rail}
4.262 -
4.263 -\begin{descr}
4.264 -\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
4.265 - (co)inductive sets from the given introduction rules.
4.266 -\item [$mono$] declares monotonicity rules. These rule are involved in the
4.267 - automated monotonicity proof of $\isarkeyword{inductive}$.
4.268 -\end{descr}
4.269 -
4.270 -See \cite{isabelle-HOL} for further information on inductive definitions in
4.271 -HOL.
4.272 -
4.273 -
4.274 -\section{Arithmetic}
4.275 -
4.276 -\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
4.277 -\begin{matharray}{rcl}
4.278 - arith & : & \isarmeth \\
4.279 - arith_split & : & \isaratt \\
4.280 -\end{matharray}
4.281 -
4.282 -\begin{rail}
4.283 - 'arith' '!'?
4.284 - ;
4.285 -\end{rail}
4.286 -
4.287 -The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
4.288 -$real$). Any current facts are inserted into the goal before running the
4.289 -procedure. The ``!''~argument causes the full context of assumptions to be
4.290 -included. The $arith_split$ attribute declares case split rules to be
4.291 -expanded before the arithmetic procedure is invoked.
4.292 -
4.293 -Note that a simpler (but faster) version of arithmetic reasoning is already
4.294 -performed by the Simplifier.
4.295 -
4.296 -
4.297 -\section{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
4.298 -
4.299 -The following important tactical tools of Isabelle/HOL have been ported to
4.300 -Isar. These should be never used in proper proof texts!
4.301 -
4.302 -\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
4.303 -\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
4.304 -\begin{matharray}{rcl}
4.305 - case_tac^* & : & \isarmeth \\
4.306 - induct_tac^* & : & \isarmeth \\
4.307 - ind_cases^* & : & \isarmeth \\
4.308 - \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
4.309 -\end{matharray}
4.310 -
4.311 -\railalias{casetac}{case\_tac}
4.312 -\railterm{casetac}
4.313 -
4.314 -\railalias{inducttac}{induct\_tac}
4.315 -\railterm{inducttac}
4.316 -
4.317 -\railalias{indcases}{ind\_cases}
4.318 -\railterm{indcases}
4.319 -
4.320 -\railalias{inductivecases}{inductive\_cases}
4.321 -\railterm{inductivecases}
4.322 -
4.323 -\begin{rail}
4.324 - casetac goalspec? term rule?
4.325 - ;
4.326 - inducttac goalspec? (insts * 'and') rule?
4.327 - ;
4.328 - indcases (prop +)
4.329 - ;
4.330 - inductivecases thmdecl? (prop +) comment?
4.331 - ;
4.332 -
4.333 - rule: ('rule' ':' thmref)
4.334 - ;
4.335 -\end{rail}
4.336 -
4.337 -\begin{descr}
4.338 -\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
4.339 - only (unless an alternative rule is given explicitly). Furthermore,
4.340 - $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
4.341 - variables to be given as instantiation. These tactic emulations feature
4.342 - both goal addressing and dynamic instantiation. Note that named rule cases
4.343 - are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
4.344 - methods (see \S\ref{sec:cases-induct}).
4.345 -
4.346 -\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
4.347 - to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted
4.348 - forward manner.
4.349 -
4.350 - While $ind_cases$ is a proof method to apply the result immediately as
4.351 - elimination rules, $\isarkeyword{inductive_cases}$ provides case split
4.352 - theorems at the theory level for later use,
4.353 -\end{descr}
4.354 -
4.355 -
4.356 -%%% Local Variables:
4.357 -%%% mode: latex
4.358 -%%% TeX-master: "isar-ref"
4.359 -%%% End:
5.1 --- a/doc-src/IsarRef/intro.tex Thu Jan 03 17:01:59 2002 +0100
5.2 +++ b/doc-src/IsarRef/intro.tex Thu Jan 03 17:48:02 2002 +0100
5.3 @@ -265,6 +265,8 @@
5.4
5.5 \subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
5.6
5.7 +%FIXME tune
5.8 +
5.9 This is one of the key questions, of course. Isar offers a rather different
5.10 approach to formal proof documents than plain old tactic scripts. Experienced
5.11 users of existing interactive theorem proving systems may have to learn
6.1 --- a/doc-src/IsarRef/isar-ref.tex Thu Jan 03 17:01:59 2002 +0100
6.2 +++ b/doc-src/IsarRef/isar-ref.tex Thu Jan 03 17:48:02 2002 +0100
6.3 @@ -89,8 +89,7 @@
6.4 \include{syntax}
6.5 \include{pure}
6.6 \include{generic}
6.7 -\include{hol}
6.8 -\include{zf}
6.9 +\include{logics}
6.10
6.11 \appendix
6.12 \include{refcard}
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/doc-src/IsarRef/logics.tex Thu Jan 03 17:48:02 2002 +0100
7.3 @@ -0,0 +1,500 @@
7.4 +
7.5 +\chapter{Object-logic specific elements}\label{ch:logics}
7.6 +
7.7 +\section{General logic setup}\label{sec:object-logic}
7.8 +
7.9 +\indexisarcmd{judgment}
7.10 +\indexisarmeth{atomize}\indexisaratt{atomize}
7.11 +\indexisaratt{rule-format}\indexisaratt{rulify}
7.12 +
7.13 +\begin{matharray}{rcl}
7.14 + \isarcmd{judgment} & : & \isartrans{theory}{theory} \\
7.15 + atomize & : & \isarmeth \\
7.16 + atomize & : & \isaratt \\
7.17 + rule_format & : & \isaratt \\
7.18 + rulify & : & \isaratt \\
7.19 +\end{matharray}
7.20 +
7.21 +The very starting point for any Isabelle object-logic is a ``truth judgment''
7.22 +that links object-level statements to the meta-logic (with its minimal
7.23 +language of $prop$ that covers universal quantification $\Forall$ and
7.24 +implication $\Imp$). Common object-logics are sufficiently expressive to
7.25 +\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own
7.26 +language. This is useful in certain situations where a rule needs to be
7.27 +viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x
7.28 +\in A \Imp P(x)$ versus $\forall x \in A. P(x)$).
7.29 +
7.30 +From the following language elements, only the $atomize$ method and
7.31 +$rule_format$ attribute are occasionally required by end-users, the rest is
7.32 +for those who need to setup their own object-logic. In the latter case
7.33 +existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as
7.34 +realistic examples.
7.35 +
7.36 +Generic tools may refer to the information provided by object-logic
7.37 +declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical
7.38 +Reasoner \S\ref{sec:classical}).
7.39 +
7.40 +\railalias{ruleformat}{rule\_format}
7.41 +\railterm{ruleformat}
7.42 +
7.43 +\begin{rail}
7.44 + 'judgment' constdecl
7.45 + ;
7.46 + ruleformat ('(' noasm ')')?
7.47 + ;
7.48 +\end{rail}
7.49 +
7.50 +\begin{descr}
7.51 +
7.52 +\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the
7.53 + truth judgment of the current object-logic. Its type $\sigma$ should
7.54 + specify a coercion of the category of object-level propositions to $prop$ of
7.55 + the Pure meta-logic; the mixfix annotation $syn$ would typically just link
7.56 + the object language (internally of syntactic category $logic$) with that of
7.57 + $prop$. Only one $\isarkeyword{judgment}$ declaration may be given in any
7.58 + theory development.
7.59 +
7.60 +\item [$atomize$] (as a method) rewrites any non-atomic premises of a
7.61 + sub-goal, using the meta-level equations declared via $atomize$ (as an
7.62 + attribute) beforehand. As a result, heavily nested goals become amenable to
7.63 + fundamental operations such as resolution (cf.\ the $rule$ method) and
7.64 + proof-by-assumption (cf.\ $assumption$).
7.65 +
7.66 + A typical collection of $atomize$ rules for a particular object-logic would
7.67 + provide an internalization for each of the connectives of $\Forall$, $\Imp$,
7.68 + and $\equiv$. Meta-level conjunction expressed in the manner of minimal
7.69 + higher-order logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$
7.70 + should be covered as well (this is particularly important for locales, see
7.71 + \S\ref{sec:locale}).
7.72 +
7.73 +\item [$rule_format$] rewrites a theorem by the equalities declared as
7.74 + $rulify$ rules in the current object-logic. By default, the result is fully
7.75 + normalized, including assumptions and conclusions at any depth. The
7.76 + $no_asm$ option restricts the transformation to the conclusion of a rule.
7.77 +
7.78 + In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to
7.79 + replace (bounded) universal quantification ($\forall$) and implication
7.80 + ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.
7.81 +
7.82 +\end{descr}
7.83 +
7.84 +
7.85 +\section{HOL}
7.86 +
7.87 +\subsection{Primitive types}\label{sec:typedef}
7.88 +
7.89 +\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
7.90 +\begin{matharray}{rcl}
7.91 + \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
7.92 + \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
7.93 +\end{matharray}
7.94 +
7.95 +\begin{rail}
7.96 + 'typedecl' typespec infix? comment?
7.97 + ;
7.98 + 'typedef' parname? typespec infix? \\ '=' term comment?
7.99 + ;
7.100 +\end{rail}
7.101 +
7.102 +\begin{descr}
7.103 +\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
7.104 + $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
7.105 + also declares type arity $t :: (term, \dots, term) term$, making $t$ an
7.106 + actual HOL type constructor.
7.107 +\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
7.108 + non-emptiness of the set $A$. After finishing the proof, the theory will be
7.109 + augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL}
7.110 + for more information. Note that user-level theories usually do not directly
7.111 + refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
7.112 + packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and
7.113 + $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
7.114 +\end{descr}
7.115 +
7.116 +
7.117 +\subsection{Low-level tuples}
7.118 +
7.119 +\indexisarattof{HOL}{split-format}
7.120 +\begin{matharray}{rcl}
7.121 + split_format^* & : & \isaratt \\
7.122 +\end{matharray}
7.123 +
7.124 +\railalias{splitformat}{split\_format}
7.125 +\railterm{splitformat}
7.126 +\railterm{complete}
7.127 +
7.128 +\begin{rail}
7.129 + splitformat (((name * ) + 'and') | ('(' complete ')'))
7.130 + ;
7.131 +\end{rail}
7.132 +
7.133 +\begin{descr}
7.134 +
7.135 +\item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
7.136 + tuple types into canonical form as specified by the arguments given; $\vec
7.137 + p@i$ refers to occurrences in premise $i$ of the rule. The
7.138 + $split_format~(complete)$ form causes \emph{all} arguments in function
7.139 + applications to be represented canonically according to their tuple type
7.140 + structure.
7.141 +
7.142 + Note that these operations tend to invent funny names for new local
7.143 + parameters to be introduced.
7.144 +
7.145 +\end{descr}
7.146 +
7.147 +
7.148 +\subsection{Records}\label{sec:hol-record}
7.149 +
7.150 +FIXME proof tools (simp, cases/induct; no split!?);
7.151 +
7.152 +FIXME mixfix syntax;
7.153 +
7.154 +\indexisarcmdof{HOL}{record}
7.155 +\begin{matharray}{rcl}
7.156 + \isarcmd{record} & : & \isartrans{theory}{theory} \\
7.157 +\end{matharray}
7.158 +
7.159 +\begin{rail}
7.160 + 'record' typespec '=' (type '+')? (constdecl +)
7.161 + ;
7.162 +\end{rail}
7.163 +
7.164 +\begin{descr}
7.165 +\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
7.166 + defines extensible record type $(\vec\alpha)t$, derived from the optional
7.167 + parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
7.168 + See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on
7.169 + simply-typed extensible records.
7.170 +\end{descr}
7.171 +
7.172 +
7.173 +\subsection{Datatypes}\label{sec:hol-datatype}
7.174 +
7.175 +\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
7.176 +\begin{matharray}{rcl}
7.177 + \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
7.178 + \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
7.179 +\end{matharray}
7.180 +
7.181 +\railalias{repdatatype}{rep\_datatype}
7.182 +\railterm{repdatatype}
7.183 +
7.184 +\begin{rail}
7.185 + 'datatype' (dtspec + 'and')
7.186 + ;
7.187 + repdatatype (name * ) dtrules
7.188 + ;
7.189 +
7.190 + dtspec: parname? typespec infix? '=' (cons + '|')
7.191 + ;
7.192 + cons: name (type * ) mixfix? comment?
7.193 + ;
7.194 + dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
7.195 +\end{rail}
7.196 +
7.197 +\begin{descr}
7.198 +\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
7.199 +\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
7.200 + ones, generating the standard infrastructure of derived concepts (primitive
7.201 + recursion etc.).
7.202 +\end{descr}
7.203 +
7.204 +The induction and exhaustion theorems generated provide case names according
7.205 +to the constructors involved, while parameters are named after the types (see
7.206 +also \S\ref{sec:cases-induct}).
7.207 +
7.208 +See \cite{isabelle-HOL} for more details on datatypes. Note that the theory
7.209 +syntax above has been slightly simplified over the old version, usually
7.210 +requiring more quotes and less parentheses. Apart from proper proof methods
7.211 +for case-analysis and induction, there are also emulations of ML tactics
7.212 +\texttt{case_tac} and \texttt{induct_tac} available, see
7.213 +\S\ref{sec:induct_tac}.
7.214 +
7.215 +
7.216 +\subsection{Recursive functions}\label{sec:recursion}
7.217 +
7.218 +\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
7.219 +\begin{matharray}{rcl}
7.220 + \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
7.221 + \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
7.222 + \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
7.223 +%FIXME
7.224 +% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
7.225 +\end{matharray}
7.226 +
7.227 +\railalias{recdefsimp}{recdef\_simp}
7.228 +\railterm{recdefsimp}
7.229 +
7.230 +\railalias{recdefcong}{recdef\_cong}
7.231 +\railterm{recdefcong}
7.232 +
7.233 +\railalias{recdefwf}{recdef\_wf}
7.234 +\railterm{recdefwf}
7.235 +
7.236 +\railalias{recdeftc}{recdef\_tc}
7.237 +\railterm{recdeftc}
7.238 +
7.239 +\begin{rail}
7.240 + 'primrec' parname? (equation + )
7.241 + ;
7.242 + 'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
7.243 + ;
7.244 + recdeftc thmdecl? tc comment?
7.245 + ;
7.246 +
7.247 + equation: thmdecl? eqn
7.248 + ;
7.249 + eqn: prop comment?
7.250 + ;
7.251 + hints: '(' 'hints' (recdefmod * ) ')'
7.252 + ;
7.253 + recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
7.254 + ;
7.255 + tc: nameref ('(' nat ')')?
7.256 + ;
7.257 +\end{rail}
7.258 +
7.259 +\begin{descr}
7.260 +\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
7.261 + datatypes, see also \cite{isabelle-HOL}.
7.262 +\item [$\isarkeyword{recdef}$] defines general well-founded recursive
7.263 + functions (using the TFL package), see also \cite{isabelle-HOL}. The
7.264 + $(permissive)$ option tells TFL to recover from failed proof attempts,
7.265 + returning unfinished results. The $recdef_simp$, $recdef_cong$, and
7.266 + $recdef_wf$ hints refer to auxiliary rules to be used in the internal
7.267 + automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\
7.268 + \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
7.269 + (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
7.270 + \S\ref{sec:classical}).
7.271 +\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
7.272 + termination condition number $i$ (default $1$) as generated by a
7.273 + $\isarkeyword{recdef}$ definition of constant $c$.
7.274 +
7.275 + Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
7.276 + internal proofs without manual intervention.
7.277 +\end{descr}
7.278 +
7.279 +Both kinds of recursive definitions accommodate reasoning by induction (cf.\
7.280 +\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
7.281 +the function definition) refers to a specific induction rule, with parameters
7.282 +named according to the user-specified equations. Case names of
7.283 +$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
7.284 +$\isarkeyword{recdef}$ are numbered (starting from $1$).
7.285 +
7.286 +The equations provided by these packages may be referred later as theorem list
7.287 +$f\mathord.simps$, where $f$ is the (collective) name of the functions
7.288 +defined. Individual equations may be named explicitly as well; note that for
7.289 +$\isarkeyword{recdef}$ each specification given by the user may result in
7.290 +several theorems.
7.291 +
7.292 +\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
7.293 +the following attributes.
7.294 +
7.295 +\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
7.296 +\begin{matharray}{rcl}
7.297 + recdef_simp & : & \isaratt \\
7.298 + recdef_cong & : & \isaratt \\
7.299 + recdef_wf & : & \isaratt \\
7.300 +\end{matharray}
7.301 +
7.302 +\railalias{recdefsimp}{recdef\_simp}
7.303 +\railterm{recdefsimp}
7.304 +
7.305 +\railalias{recdefcong}{recdef\_cong}
7.306 +\railterm{recdefcong}
7.307 +
7.308 +\railalias{recdefwf}{recdef\_wf}
7.309 +\railterm{recdefwf}
7.310 +
7.311 +\begin{rail}
7.312 + (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
7.313 + ;
7.314 +\end{rail}
7.315 +
7.316 +
7.317 +\subsection{(Co)Inductive sets}\label{sec:hol-inductive}
7.318 +
7.319 +\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}
7.320 +\begin{matharray}{rcl}
7.321 + \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
7.322 + \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
7.323 + mono & : & \isaratt \\
7.324 +\end{matharray}
7.325 +
7.326 +\railalias{condefs}{con\_defs}
7.327 +\railterm{condefs}
7.328 +
7.329 +\begin{rail}
7.330 + ('inductive' | 'coinductive') sets intros monos?
7.331 + ;
7.332 + 'mono' (() | 'add' | 'del')
7.333 + ;
7.334 +
7.335 + sets: (term comment? +)
7.336 + ;
7.337 + intros: 'intros' (thmdecl? prop comment? +)
7.338 + ;
7.339 + monos: 'monos' thmrefs comment?
7.340 + ;
7.341 +\end{rail}
7.342 +
7.343 +\begin{descr}
7.344 +\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
7.345 + (co)inductive sets from the given introduction rules.
7.346 +\item [$mono$] declares monotonicity rules. These rule are involved in the
7.347 + automated monotonicity proof of $\isarkeyword{inductive}$.
7.348 +\end{descr}
7.349 +
7.350 +See \cite{isabelle-HOL} for further information on inductive definitions in
7.351 +HOL.
7.352 +
7.353 +
7.354 +\subsection{Arithmetic proof support}
7.355 +
7.356 +\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
7.357 +\begin{matharray}{rcl}
7.358 + arith & : & \isarmeth \\
7.359 + arith_split & : & \isaratt \\
7.360 +\end{matharray}
7.361 +
7.362 +\begin{rail}
7.363 + 'arith' '!'?
7.364 + ;
7.365 +\end{rail}
7.366 +
7.367 +The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
7.368 +$real$). Any current facts are inserted into the goal before running the
7.369 +procedure. The ``!''~argument causes the full context of assumptions to be
7.370 +included. The $arith_split$ attribute declares case split rules to be
7.371 +expanded before the arithmetic procedure is invoked.
7.372 +
7.373 +Note that a simpler (but faster) version of arithmetic reasoning is already
7.374 +performed by the Simplifier.
7.375 +
7.376 +
7.377 +\subsection{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
7.378 +
7.379 +The following important tactical tools of Isabelle/HOL have been ported to
7.380 +Isar. These should be never used in proper proof texts!
7.381 +
7.382 +\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
7.383 +\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
7.384 +\begin{matharray}{rcl}
7.385 + case_tac^* & : & \isarmeth \\
7.386 + induct_tac^* & : & \isarmeth \\
7.387 + ind_cases^* & : & \isarmeth \\
7.388 + \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
7.389 +\end{matharray}
7.390 +
7.391 +\railalias{casetac}{case\_tac}
7.392 +\railterm{casetac}
7.393 +
7.394 +\railalias{inducttac}{induct\_tac}
7.395 +\railterm{inducttac}
7.396 +
7.397 +\railalias{indcases}{ind\_cases}
7.398 +\railterm{indcases}
7.399 +
7.400 +\railalias{inductivecases}{inductive\_cases}
7.401 +\railterm{inductivecases}
7.402 +
7.403 +\begin{rail}
7.404 + casetac goalspec? term rule?
7.405 + ;
7.406 + inducttac goalspec? (insts * 'and') rule?
7.407 + ;
7.408 + indcases (prop +)
7.409 + ;
7.410 + inductivecases thmdecl? (prop +) comment?
7.411 + ;
7.412 +
7.413 + rule: ('rule' ':' thmref)
7.414 + ;
7.415 +\end{rail}
7.416 +
7.417 +\begin{descr}
7.418 +\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
7.419 + only (unless an alternative rule is given explicitly). Furthermore,
7.420 + $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
7.421 + variables to be given as instantiation. These tactic emulations feature
7.422 + both goal addressing and dynamic instantiation. Note that named rule cases
7.423 + are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
7.424 + methods (see \S\ref{sec:cases-induct}).
7.425 +
7.426 +\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
7.427 + to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted
7.428 + forward manner.
7.429 +
7.430 + While $ind_cases$ is a proof method to apply the result immediately as
7.431 + elimination rules, $\isarkeyword{inductive_cases}$ provides case split
7.432 + theorems at the theory level for later use,
7.433 +\end{descr}
7.434 +
7.435 +
7.436 +\section{HOLCF}
7.437 +
7.438 +\subsection{Mixfix syntax for continuous operations}
7.439 +
7.440 +\indexisarcmdof{HOLCF}{consts}\indexisarcmdof{HOLCF}{constdefs}
7.441 +
7.442 +\begin{matharray}{rcl}
7.443 + \isarcmd{consts} & : & \isartrans{theory}{theory} \\
7.444 + \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
7.445 +\end{matharray}
7.446 +
7.447 +HOLCF provides a separate type for continuous functions $\alpha \rightarrow
7.448 +\beta$, with an explicit application operator $f \cdot x$. Isabelle mixfix
7.449 +syntax normally refers directly to the pure meta-level function type $\alpha
7.450 +\To \beta$, with application $f\,x$.
7.451 +
7.452 +The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ have the same outer syntax as
7.453 +the pure versions (cf.\ \S\ref{sec:consts}). Internally, declarations
7.454 +involving continuous function types are treated specifically, transforming the
7.455 +syntax template accordingly and generating syntax translation rules for the
7.456 +abstract and concrete representation of application.
7.457 +
7.458 +The behavior for plain meta-level function types is unchanged. Mixed
7.459 +continuous and meta-level application is \emph{not} supported.
7.460 +
7.461 +\subsection{Recursive domains}
7.462 +
7.463 +\indexisarcmdof{HOLCF}{domain}
7.464 +\begin{matharray}{rcl}
7.465 + \isarcmd{domain} & : & \isartrans{theory}{theory} \\
7.466 +\end{matharray}
7.467 +
7.468 +\begin{rail}
7.469 + 'domain' parname? (dmspec + 'and')
7.470 + ;
7.471 +
7.472 + dmspec: typespec '=' (cons + '|')
7.473 + ;
7.474 + cons: name (type * ) mixfix? comment?
7.475 + ;
7.476 + dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
7.477 +\end{rail}
7.478 +
7.479 +Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\
7.480 +\S\ref{sec:hol-datatype}). Mutual recursive is supported, but no nesting nor
7.481 +arbitrary branching. Domain constructors may be strict (default) or lazy, the
7.482 +latter admits to introduce infinitary objects in the typical LCF manner (lazy
7.483 +lists etc.).
7.484 +
7.485 +See also \cite{MuellerNvOS99} for further information HOLCF domains in
7.486 +general.
7.487 +
7.488 +
7.489 +\section{ZF}
7.490 +
7.491 +\subsection{Type checking}
7.492 +
7.493 +FIXME
7.494 +
7.495 +\subsection{Inductive sets and datatypes}
7.496 +
7.497 +FIXME
7.498 +
7.499 +
7.500 +%%% Local Variables:
7.501 +%%% mode: latex
7.502 +%%% TeX-master: "isar-ref"
7.503 +%%% End:
8.1 --- a/doc-src/IsarRef/pure.tex Thu Jan 03 17:01:59 2002 +0100
8.2 +++ b/doc-src/IsarRef/pure.tex Thu Jan 03 17:48:02 2002 +0100
8.3 @@ -5,8 +5,8 @@
8.4 commands, together with fundamental proof methods and attributes.
8.5 Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic
8.6 tools and packages (such as the Simplifier) that are either part of Pure
8.7 -Isabelle or pre-installed by most object logics. Chapter~\ref{ch:hol-tools}
8.8 -refers to actual object-logic specific elements of Isabelle/HOL.
8.9 +Isabelle or pre-installed by most object logics. Chapter~\ref{ch:logics}
8.10 +refers to object-logic specific elements (mainly for HOL and ZF).
8.11
8.12 \medskip
8.13
8.14 @@ -16,15 +16,14 @@
8.15 are subsequently marked by ``$^*$'', are often helpful when developing proof
8.16 documents, while their use is discouraged for the final outcome. Typical
8.17 examples are diagnostic commands that print terms or theorems according to the
8.18 -current context; other commands even emulate old-style tactical theorem
8.19 -proving.
8.20 +current context; other commands emulate old-style tactical theorem proving.
8.21
8.22
8.23 -\section{Theory specification commands}
8.24 +\section{Theory commands}
8.25
8.26 \subsection{Defining theories}\label{sec:begin-thy}
8.27
8.28 -\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
8.29 +\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{context}\indexisarcmd{end}
8.30 \begin{matharray}{rcl}
8.31 \isarcmd{header} & : & \isarkeep{toplevel} \\
8.32 \isarcmd{theory} & : & \isartrans{toplevel}{theory} \\
8.33 @@ -38,14 +37,14 @@
8.34 proof as well. In contrast, ``old-style'' Isabelle theories support batch
8.35 processing only, with the proof scripts collected in separate ML files.
8.36
8.37 -The first actual command of any theory has to be $\THEORY$, starting a new
8.38 -theory based on the merge of existing ones. Just preceding $\THEORY$, there
8.39 -may be an optional $\isarkeyword{header}$ declaration, which is relevant to
8.40 -document preparation only; it acts very much like a special pre-theory markup
8.41 -command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The theory
8.42 -context may be also changed by $\CONTEXT$ without creating a new theory. In
8.43 -both cases, $\END$ concludes the theory development; it has to be the very
8.44 -last command of any theory file.
8.45 +The first ``real'' command of any theory has to be $\THEORY$, which starts a
8.46 +new theory based on the merge of existing ones. Just preceding $\THEORY$,
8.47 +there may be an optional $\isarkeyword{header}$ declaration, which is relevant
8.48 +to document preparation only; it acts very much like a special pre-theory
8.49 +markup command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The
8.50 +$\END$ commands concludes a theory development; it has to be the very last
8.51 +command of any theory file to loaded in batch-mode. The theory context may be
8.52 +also changed interactively by $\CONTEXT$ without creating a new theory.
8.53
8.54 \begin{rail}
8.55 'header' text
8.56 @@ -54,8 +53,6 @@
8.57 ;
8.58 'context' name
8.59 ;
8.60 - 'end'
8.61 - ;;
8.62
8.63 filespecs: 'files' ((name | parname) +);
8.64 \end{rail}
8.65 @@ -67,28 +64,42 @@
8.66 produce chapter or section headings. See also \S\ref{sec:markup-thy} and
8.67 \S\ref{sec:markup-prf} for further markup commands.
8.68
8.69 -\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] commences a new theory $A$
8.70 - based on existing ones $B@1 + \cdots + B@n$. Isabelle's theory loader
8.71 - system ensures that any of the base theories are properly loaded (and fully
8.72 - up-to-date when $\THEORY$ is executed interactively). The optional
8.73 - $\isarkeyword{files}$ specification declares additional dependencies on ML
8.74 - files. Unless put in parentheses, any file will be loaded immediately via
8.75 - $\isarcmd{use}$ (see also \S\ref{sec:ML}). The optional ML file
8.76 - \texttt{$A$.ML} that may be associated with any theory should \emph{not} be
8.77 - included in $\isarkeyword{files}$, though.
8.78 +\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] starts a new theory $A$ based
8.79 + on the merge of existing theories $B@1, \dots, B@n$.
8.80 +
8.81 + Due to inclusion of several ancestors, the overall theory structure emerging
8.82 + in an Isabelle session forms a directed acyclic graph (DAG). Isabelle's
8.83 + theory loader ensures that the sources contributing to the development graph
8.84 + are always up-to-date. Changed files are automatically reloaded when
8.85 + processing theory headers interactively; batch-mode explicitly distinguishes
8.86 + \verb,update_thy, from \verb,use_thy,, see also \cite{isabelle-ref}.
8.87 +
8.88 + The optional $\isarkeyword{files}$ specification declares additional
8.89 + dependencies on ML files. Files will be loaded immediately, unless the name
8.90 + is put in parentheses, which merely documents the dependency to be resolved
8.91 + later in the text (typically via explicit $\isarcmd{use}$ in the body text,
8.92 + see \S\ref{sec:ML}). In reminiscence of the old-style theory system of
8.93 + Isabelle, \texttt{$A$.thy} may be also accompanied by an additional file
8.94 + \texttt{$A$.ML} consisting of ML code that is executed in the context of the
8.95 + \emph{finished} theory $A$. That file should not be included in the
8.96 + $\isarkeyword{files}$ dependency declaration, though.
8.97
8.98 \item [$\CONTEXT~B$] enters an existing theory context, basically in read-only
8.99 mode, so only a limited set of commands may be performed without destroying
8.100 the theory. Just as for $\THEORY$, the theory loader ensures that $B$ is
8.101 loaded and up-to-date.
8.102
8.103 + This command is occasionally useful for quick interactive experiments;
8.104 + normally one should always commence a new context via $\THEORY$.
8.105 +
8.106 \item [$\END$] concludes the current theory definition or context switch.
8.107 -Note that this command cannot be undone, but the whole theory definition has
8.108 -to be retracted.
8.109 + Note that this command cannot be undone, but the whole theory definition has
8.110 + to be retracted.
8.111 +
8.112 \end{descr}
8.113
8.114
8.115 -\subsection{Theory markup commands}\label{sec:markup-thy}
8.116 +\subsection{Markup commands}\label{sec:markup-thy}
8.117
8.118 \indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
8.119 \indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw}
8.120 @@ -144,9 +155,9 @@
8.121 \subsection{Type classes and sorts}\label{sec:classes}
8.122
8.123 \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
8.124 -\begin{matharray}{rcl}
8.125 +\begin{matharray}{rcll}
8.126 \isarcmd{classes} & : & \isartrans{theory}{theory} \\
8.127 - \isarcmd{classrel} & : & \isartrans{theory}{theory} \\
8.128 + \isarcmd{classrel} & : & \isartrans{theory}{theory} & (axiomatic!) \\
8.129 \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
8.130 \end{matharray}
8.131
8.132 @@ -169,18 +180,18 @@
8.133 proven class relations.
8.134 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
8.135 any type variables given without sort constraints. Usually, the default
8.136 - sort would be only changed when defining new object-logics.
8.137 + sort would be only changed when defining a new object-logic.
8.138 \end{descr}
8.139
8.140
8.141 \subsection{Primitive types and type abbreviations}\label{sec:types-pure}
8.142
8.143 \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
8.144 -\begin{matharray}{rcl}
8.145 +\begin{matharray}{rcll}
8.146 \isarcmd{types} & : & \isartrans{theory}{theory} \\
8.147 \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
8.148 \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
8.149 - \isarcmd{arities} & : & \isartrans{theory}{theory} \\
8.150 + \isarcmd{arities} & : & \isartrans{theory}{theory} & (axiomatic!) \\
8.151 \end{matharray}
8.152
8.153 \begin{rail}
8.154 @@ -247,10 +258,9 @@
8.155 Unless this option is given, a warning message would be issued for any
8.156 definitional equation with a more special type than that of the
8.157 corresponding constant declaration.
8.158 -
8.159 -\item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and
8.160 - definitions of constants, using the canonical name $c_def$ for the
8.161 - definitional axiom.
8.162 +
8.163 +\item [$\CONSTDEFS~c::\sigma~eqn$] combines declarations and definitions of
8.164 + constants, using the canonical name $c_def$ for the definitional axiom.
8.165 \end{descr}
8.166
8.167
8.168 @@ -300,8 +310,8 @@
8.169 \subsection{Axioms and theorems}\label{sec:axms-thms}
8.170
8.171 \indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems}
8.172 -\begin{matharray}{rcl}
8.173 - \isarcmd{axioms} & : & \isartrans{theory}{theory} \\
8.174 +\begin{matharray}{rcll}
8.175 + \isarcmd{axioms} & : & \isartrans{theory}{theory} & (axiomatic!) \\
8.176 \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
8.177 \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
8.178 \end{matharray}
8.179 @@ -366,9 +376,7 @@
8.180 name space (which may be $class$, $type$, or $const$). Hidden objects
8.181 remain valid within the logic, but are inaccessible from user input. In
8.182 output, the special qualifier ``$\mathord?\mathord?$'' is prefixed to the
8.183 - full internal name.
8.184 -
8.185 - Unqualified (global) names may not be hidden deliberately.
8.186 + full internal name. Unqualified (global) names may not be hidden.
8.187 \end{descr}
8.188
8.189
8.190 @@ -550,9 +558,15 @@
8.191 goal claimed next.
8.192 \end{descr}
8.193
8.194 -%FIXME diagram?
8.195 +The proof mode indicator may be read as a verb telling the writer what kind of
8.196 +operation may be performed next. The corresponding typings of proof commands
8.197 +restricts the shape of well-formed proof texts to particular command
8.198 +sequences. So dynamic arrangements of commands eventually turn out as static
8.199 +texts. Appendix~\ref{ap:refcard} gives a simplified grammar of the overall
8.200 +(extensible) language emerging that way.
8.201
8.202 -\subsection{Proof markup commands}\label{sec:markup-prf}
8.203 +
8.204 +\subsection{Markup commands}\label{sec:markup-prf}
8.205
8.206 \indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
8.207 \indexisarcmd{txt}\indexisarcmd{txt-raw}
8.208 @@ -576,7 +590,7 @@
8.209 \end{rail}
8.210
8.211
8.212 -\subsection{Proof context}\label{sec:proof-context}
8.213 +\subsection{Context elements}\label{sec:proof-context}
8.214
8.215 \indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
8.216 \begin{matharray}{rcl}
8.217 @@ -699,7 +713,7 @@
8.218
8.219 Forward chaining with an empty list of theorems is the same as not chaining.
8.220 Thus $\FROM{nothing}$ has no effect apart from entering $prove(chain)$ mode,
8.221 -since $nothing$\indexisarthm{nothing} is bound to the empty list of facts.
8.222 +since $nothing$\indexisarthm{nothing} is bound to the empty list of theorems.
8.223
8.224
8.225 \subsection{Goal statements}
8.226 @@ -716,11 +730,11 @@
8.227 \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
8.228 \end{matharray}
8.229
8.230 -From a theory context, proof mode is entered from theory mode by initial goal
8.231 -commands $\LEMMANAME$, $\THEOREMNAME$, and $\COROLLARYNAME$. Within a proof,
8.232 -new claims may be introduced locally as well; four variants are available,
8.233 -indicating whether the result is meant to solve some pending goal or whether
8.234 -forward chaining is indicated.
8.235 +From a theory context, proof mode is entered by an initial goal command such
8.236 +as $\LEMMANAME$, $\THEOREMNAME$, $\COROLLARYNAME$. Within a proof, new claims
8.237 +may be introduced locally as well; four variants are available here to
8.238 +indicate whether forward chaining of facts should be performed initially (via
8.239 +$\THEN$), and whether the emerging result is meant to solve some pending goal.
8.240
8.241 Goals may consist of multiple statements, resulting in a list of facts
8.242 eventually. A pending multi-goal is internally represented as a meta-level
8.243 @@ -731,16 +745,21 @@
8.244 the $induct$ method covered in \S\ref{sec:cases-induct-meth} acts on
8.245 multiple claims simultaneously.}
8.246
8.247 -%FIXME define locale, context
8.248 -
8.249 \begin{rail}
8.250 - ('lemma' | 'theorem' | 'corollary') locale context goal
8.251 + ('lemma' | 'theorem' | 'corollary') goalprefix goal
8.252 ;
8.253 ('have' | 'show' | 'hence' | 'thus') goal
8.254 ;
8.255
8.256 goal: (props comment? + 'and')
8.257 ;
8.258 +
8.259 + goalprefix: thmdecl? locale? context?
8.260 + ;
8.261 + locale: '(' 'in' name ')'
8.262 + ;
8.263 + context: '(' (contextelem +) ')'
8.264 + ;
8.265 \end{rail}
8.266
8.267 \begin{descr}
8.268 @@ -749,8 +768,8 @@
8.269 theory context, and optionally into the specified locale, cf.\
8.270 \S\ref{sec:locale}. An additional \railnonterm{context} specification may
8.271 build an initial proof context for the subsequent claim; this may include
8.272 - local definitions and syntax as well, see \S\ref{sec:locale} for more
8.273 - information.
8.274 + local definitions and syntax as well, see the definition of $contextelem$ in
8.275 + \S\ref{sec:locale}.
8.276
8.277 \item [$\THEOREM{a}{\vec\phi}$ and $\COROLLARY{a}{\vec\phi}$] are essentially
8.278 the same as $\LEMMA{a}{\vec\phi}$, but the facts are internally marked as
8.279 @@ -832,18 +851,19 @@
8.280 remaining goals. No facts are passed to $m@2$.
8.281 \end{enumerate}
8.282
8.283 -The only other proper way to affect pending goals is by $\SHOWNAME$, which
8.284 -involves an explicit statement of what is to be solved.
8.285 +The only other proper way to affect pending goals in a proof body is by
8.286 +$\SHOWNAME$, which involves an explicit statement of what is to be solved
8.287 +eventually. Thus we avoid the fundamental problem of unstructured tactic
8.288 +scripts that consist of numerous consecutive goal transformations, with
8.289 +invisible effects.
8.290
8.291 \medskip
8.292
8.293 -Also note that initial proof methods should either solve the goal completely,
8.294 -or constitute some well-understood reduction to new sub-goals. Arbitrary
8.295 -automatic proof tools that are prone leave a large number of badly structured
8.296 -sub-goals are no help in continuing the proof document in any intelligible
8.297 -way.
8.298 -
8.299 -\medskip
8.300 +As a general rule of thumb for good proof style, initial proof methods should
8.301 +either solve the goal completely, or constitute some well-understood reduction
8.302 +to new sub-goals. Arbitrary automatic proof tools that are prone leave a
8.303 +large number of badly structured sub-goals are no help in continuing the proof
8.304 +document in any intelligible way.
8.305
8.306 Unless given explicitly by the user, the default initial method is ``$rule$'',
8.307 which applies a single standard elimination or introduction rule according to
8.308 @@ -903,11 +923,12 @@
8.309 The following proof methods and attributes refer to basic logical operations
8.310 of Isar. Further methods and attributes are provided by several generic and
8.311 object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
8.312 -\ref{ch:hol-tools}).
8.313 +\ref{ch:logics}).
8.314
8.315 \indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$}
8.316 -\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{rule}
8.317 \indexisaratt{OF}\indexisaratt{of}
8.318 +\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
8.319 +\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
8.320 \begin{matharray}{rcl}
8.321 assumption & : & \isarmeth \\
8.322 this & : & \isarmeth \\
8.323 @@ -921,6 +942,8 @@
8.324 rule & : & \isaratt \\
8.325 \end{matharray}
8.326
8.327 +%FIXME intro!, intro, intro?
8.328 +
8.329 \begin{rail}
8.330 'rule' thmrefs?
8.331 ;
8.332 @@ -990,8 +1013,8 @@
8.333 patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
8.334 postfix position.
8.335
8.336 -Polymorphism of term bindings is handled in Hindley-Milner style, as in ML.
8.337 -Type variables referring to local assumptions or open goal statements are
8.338 +Polymorphism of term bindings is handled in Hindley-Milner style, similar to
8.339 +ML. Type variables referring to local assumptions or open goal statements are
8.340 \emph{fixed}, while those of finished results or bound by $\LETNAME$ may occur
8.341 in \emph{arbitrary} instances later. Even though actual polymorphism should
8.342 be rarely used in practice, this mechanism is essential to achieve proper
9.1 --- a/doc-src/IsarRef/zf.tex Thu Jan 03 17:01:59 2002 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,13 +0,0 @@
9.4 -
9.5 -\chapter{Isabelle/ZF specific elements}\label{ch:zf-tools}
9.6 -
9.7 -\section{Type checking}
9.8 -
9.9 -FIXME
9.10 -
9.11 -
9.12 -
9.13 -%%% Local Variables:
9.14 -%%% mode: latex
9.15 -%%% TeX-master: "isar-ref"
9.16 -%%% End: