--- a/doc-src/IsarRef/Makefile Thu Jan 03 17:01:59 2002 +0100
+++ b/doc-src/IsarRef/Makefile Thu Jan 03 17:48:02 2002 +0100
@@ -14,7 +14,7 @@
NAME = isar-ref
FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
- generic.tex hol.tex zf.tex refcard.tex conversion.tex \
+ generic.tex logics.tex refcard.tex conversion.tex \
../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \
../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
--- a/doc-src/IsarRef/conversion.tex Thu Jan 03 17:01:59 2002 +0100
+++ b/doc-src/IsarRef/conversion.tex Thu Jan 03 17:48:02 2002 +0100
@@ -508,7 +508,7 @@
declare the theorem otherwise later (e.g.\ as $[simp~del]$).
-\section{Converting to actual Isar proof texts}
+\section{Writing actual Isar proof texts}
Porting legacy ML proof scripts into Isar tactic emulation scripts (see
\S\ref{sec:port-scripts}) is mainly a technical issue, since the basic
--- a/doc-src/IsarRef/generic.tex Thu Jan 03 17:01:59 2002 +0100
+++ b/doc-src/IsarRef/generic.tex Thu Jan 03 17:48:02 2002 +0100
@@ -1,7 +1,7 @@
\chapter{Generic Tools and Packages}\label{ch:gen-tools}
-\section{Theory commands}
+\section{Theory specification commands}
\subsection{Axiomatic type classes}\label{sec:axclass}
@@ -57,10 +57,62 @@
FIXME
+\indexouternonterm{contextelem}
-\section{Proof commands}
+
+\section{Derived proof schemes}
+
+\subsection{Generalized elimination}\label{sec:obtain}
+
+\indexisarcmd{obtain}
+\begin{matharray}{rcl}
+ \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
+\end{matharray}
+
+Generalized elimination means that additional elements with certain properties
+may introduced in the current context, by virtue of a locally proven
+``soundness statement''. Technically speaking, the $\OBTAINNAME$ language
+element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see
+\S\ref{sec:proof-context}), together with a soundness proof of its additional
+claim. According to the nature of existential reasoning, assumptions get
+eliminated from any result exported from the context later, provided that the
+corresponding parameters do \emph{not} occur in the conclusion.
+
+\begin{rail}
+ 'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and')
+ ;
+\end{rail}
-\subsection{Calculational Reasoning}\label{sec:calculation}
+$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
+shall refer to (optional) facts indicated for forward chaining.
+\begin{matharray}{l}
+ \langle facts~\vec b\rangle \\
+ \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
+ \quad \BG \\
+ \qquad \FIX{thesis} \\
+ \qquad \ASSUME{that~[simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
+ \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
+ \quad \EN \\
+ \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
+\end{matharray}
+
+Typically, the soundness proof is relatively straight-forward, often just by
+canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
+$\BY{blast}$ (see \S\ref{sec:classical-auto}). Accordingly, the ``$that$''
+reduction above is declared as simplification and introduction rule.
+
+\medskip
+
+In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
+meta-logical existential quantifiers and conjunctions. This concept has a
+broad range of useful applications, ranging from plain elimination (or even
+introduction) of object-level existentials and conjunctions, to elimination
+over results of symbolic evaluation of recursive definitions, for example.
+Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
+where the result is treated as an assumption.
+
+
+\subsection{Calculational reasoning}\label{sec:calculation}
\indexisarcmd{also}\indexisarcmd{finally}
\indexisarcmd{moreover}\indexisarcmd{ultimately}
@@ -150,55 +202,7 @@
\end{descr}
-\subsection{Generalized elimination}\label{sec:obtain}
-
-\indexisarcmd{obtain}
-\begin{matharray}{rcl}
- \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
-\end{matharray}
-
-Generalized elimination means that additional elements with certain properties
-may introduced in the current context, by virtue of a locally proven
-``soundness statement''. Technically speaking, the $\OBTAINNAME$ language
-element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see
-\S\ref{sec:proof-context}), together with a soundness proof of its additional
-claim. According to the nature of existential reasoning, assumptions get
-eliminated from any result exported from the context later, provided that the
-corresponding parameters do \emph{not} occur in the conclusion.
-
-\begin{rail}
- 'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and')
- ;
-\end{rail}
-
-$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
-shall refer to (optional) facts indicated for forward chaining.
-\begin{matharray}{l}
- \langle facts~\vec b\rangle \\
- \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
- \quad \BG \\
- \qquad \FIX{thesis} \\
- \qquad \ASSUME{that~[simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
- \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
- \quad \EN \\
- \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
-\end{matharray}
-
-Typically, the soundness proof is relatively straight-forward, often just by
-canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
-$\BY{blast}$ (see \S\ref{sec:classical-auto}). Accordingly, the ``$that$''
-reduction above is declared as simplification and introduction rule.
-
-\medskip
-
-In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
-meta-logical existential quantifiers and conjunctions. This concept has a
-broad range of useful applications, ranging from plain elimination (or even
-introduction) of object-level existentials and conjunctions, to elimination
-over results of symbolic evaluation of recursive definitions, for example.
-Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
-where the result is treated as an assumption.
-
+\section{Specific proof tools}
\subsection{Miscellaneous methods and attributes}\label{sec:misc-meth-att}
@@ -308,7 +312,7 @@
\end{descr}
-\subsection{Tactic emulations}\label{sec:tactics}
+\subsection{Further tactic emulations}\label{sec:tactics}
The following improper proof methods emulate traditional tactics. These admit
direct access to the goal state, which is normally considered harmful! In
@@ -432,11 +436,13 @@
\end{descr}
-\section{The Simplifier}\label{sec:simplifier}
+\subsection{The Simplifier}\label{sec:simplifier}
+
+\subsubsection{Basic equational reasoning}
-\subsection{Simplification methods}\label{sec:simp}
+FIXME
-\subsubsection{FIXME}
+\subsubsection{Simplification methods}\label{sec:simp}
\indexisarmeth{simp}\indexisarmeth{simp-all}
\begin{matharray}{rcl}
@@ -509,7 +515,7 @@
method available for single-step case splitting, see \S\ref{sec:basic-eq}.
-\subsection{Declaring rules}
+\subsubsection{Declaring rules}
\indexisarcmd{print-simpset}
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
@@ -535,7 +541,9 @@
\end{descr}
-\subsection{Forward simplification}
+\subsubsection{Forward simplification}
+
+FIXME thmargs
\indexisaratt{simplified}
\begin{matharray}{rcl}
@@ -563,7 +571,9 @@
\end{descr}
-\section{Basic equational reasoning}\label{sec:basic-eq}
+\subsubsection{Basic equational reasoning}\label{sec:basic-eq}
+
+FIXME move?
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric}
\begin{matharray}{rcl}
@@ -601,9 +611,9 @@
\end{descr}
-\section{The Classical Reasoner}\label{sec:classical}
+\subsection{The Classical Reasoner}\label{sec:classical}
-\subsection{Basic methods}\label{sec:classical-basic}
+\subsubsection{Basic methods}\label{sec:classical-basic}
\indexisarmeth{rule}\indexisarmeth{intro}
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}
@@ -642,7 +652,7 @@
\end{descr}
-\subsection{Automated methods}\label{sec:classical-auto}
+\subsubsection{Automated methods}\label{sec:classical-auto}
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
@@ -686,7 +696,7 @@
\S\ref{sec:simp}).
-\subsection{Combined automated methods}\label{sec:clasimp}
+\subsubsection{Combined automated methods}\label{sec:clasimp}
\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp}
\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp}
@@ -728,7 +738,7 @@
\end{descr}
-\subsection{Declaring rules}\label{sec:classical-mod}
+\subsubsection{Declaring rules}\label{sec:classical-mod}
\indexisarcmd{print-claset}
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
@@ -780,9 +790,9 @@
\end{descr}
-\section{Proof by cases and induction}\label{sec:cases-induct}
+\subsection{Proof by cases and induction}\label{sec:cases-induct}
-\subsection{Rule contexts}\label{sec:rule-cases}
+\subsubsection{Rule contexts}\label{sec:rule-cases}
\indexisarcmd{case}\indexisarcmd{print-cases}
\indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
@@ -871,7 +881,7 @@
\end{descr}
-\subsection{Proof methods}\label{sec:cases-induct-meth}
+\subsubsection{Proof methods}\label{sec:cases-induct-meth}
\indexisarmeth{cases}\indexisarmeth{induct}
\begin{matharray}{rcl}
@@ -1013,7 +1023,7 @@
``$type: name$'' to the method argument.
-\subsection{Declaring rules}\label{sec:cases-induct-att}
+\subsubsection{Declaring rules}\label{sec:cases-induct-att}
\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
\begin{matharray}{rcl}
@@ -1044,83 +1054,6 @@
automatically (if none had been given already): $consumes~0$ is specified for
``type'' rules and $consumes~1$ for ``set'' rules.
-
-\section{Object-logic setup}\label{sec:object-logic}
-
-The very starting point for any Isabelle object-logic is a ``truth judgment''
-that links object-level statements to the meta-logic (with its minimal
-language of $prop$ that covers universal quantification $\Forall$ and
-implication $\Imp$). Common object-logics are sufficiently expressive to
-\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own
-language. This is useful in certain situations where a rule needs to be
-viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x
-\in A \Imp P(x)$ versus $\forall x \in A. P(x)$).
-
-From the following language elements, only the $atomize$ method and
-$rule_format$ attribute are occasionally required by end-users, the rest is
-mainly for those who need to setup their own object-logic. In the latter case
-existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as
-realistic examples.
-
-Further generic tools may refer to the information provided by object-logic
-declarations internally (such as locales \S\ref{sec:locale}, or the Classical
-Reasoner \S\ref{sec:classical}).
-
-\indexisarcmd{judgment}
-\indexisarmeth{atomize}\indexisaratt{atomize}
-\indexisaratt{rule-format}\indexisaratt{rulify}
-
-\begin{matharray}{rcl}
- \isarcmd{judgment} & : & \isartrans{theory}{theory} \\
- atomize & : & \isarmeth \\
- atomize & : & \isaratt \\
- rule_format & : & \isaratt \\
- rulify & : & \isaratt \\
-\end{matharray}
-
-\railalias{ruleformat}{rule\_format}
-\railterm{ruleformat}
-
-\begin{rail}
- 'judgment' constdecl
- ;
- ruleformat ('(' noasm ')')?
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the
- truth judgment of the current object-logic. Its type $\sigma$ should
- specify a coercion of the category of object-level propositions to $prop$ of
- the Pure meta-logic; the mixfix annotation $syn$ would typically just link
- the object language (internally of syntactic category $logic$) with that of
- $prop$. Only one $\isarkeyword{judgment}$ declaration may be given in any
- theory development.
-
-\item [$atomize$] (as a method) rewrites any non-atomic premises of a
- sub-goal, using the meta-level equations that have been declared via
- $atomize$ (as an attribute) beforehand. As a result, heavily nested goals
- become amenable to fundamental operations such as resolution (cf.\ the
- $rule$ method) and proof-by-assumption (cf.\ $assumption$).
-
- A typical collection of $atomize$ rules for a particular object-logic would
- provide an internalization for each of the connectives of $\Forall$, $\Imp$,
- $\equiv$; meta-level conjunction expressed as $\All{\PROP\,C} (A \Imp B \Imp
- \PROP\,C) \Imp PROP\,C$ should be covered as well.
-
-\item [$rule_format$] rewrites a theorem by the equalities declared as
- $rulify$ rules in the current object-logic. By default, the result is fully
- normalized, including assumptions and conclusions at any depth. The
- $no_asm$ option restricts the transformation to the conclusion of a rule.
-
- In common object logics (HOL, FOL, ZF), the effect of $rule_format$ is to
- replace (bounded) universal quantification ($\forall$) and implication
- ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.
-
-\end{descr}
-
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"
--- a/doc-src/IsarRef/hol.tex Thu Jan 03 17:01:59 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,356 +0,0 @@
-
-\chapter{Isabelle/HOL specific elements}\label{ch:hol-tools}
-
-\section{Miscellaneous attributes}
-
-\indexisarattof{HOL}{split-format}
-\begin{matharray}{rcl}
- split_format^* & : & \isaratt \\
-\end{matharray}
-
-\railalias{splitformat}{split\_format}
-\railterm{splitformat}
-\railterm{complete}
-
-\begin{rail}
- splitformat (((name * ) + 'and') | ('(' complete ')'))
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$split_format~\vec p@1 \dots \vec p@n$] puts tuple objects into
- canonical form as specified by the arguments given; $\vec p@i$ refers to
- occurrences in premise $i$ of the rule. The $split_format~(complete)$ form
- causes \emph{all} arguments in function applications to be represented
- canonically according to their tuple type structure.
-
- Note that these operations tend to invent funny names for new local
- parameters to be introduced.
-
-\end{descr}
-
-
-\section{Primitive types}\label{sec:typedef}
-
-\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
-\begin{matharray}{rcl}
- \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
- \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
-\end{matharray}
-
-\begin{rail}
- 'typedecl' typespec infix? comment?
- ;
- 'typedef' parname? typespec infix? \\ '=' term comment?
- ;
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
- $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
- also declares type arity $t :: (term, \dots, term) term$, making $t$ an
- actual HOL type constructor.
-\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
- non-emptiness of the set $A$. After finishing the proof, the theory will be
- augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL}
- for more information. Note that user-level theories usually do not directly
- refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
- packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and
- $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
-\end{descr}
-
-
-\section{Records}\label{sec:hol-record}
-
-FIXME proof tools (simp, cases/induct; no split!?);
-
-\indexisarcmdof{HOL}{record}
-\begin{matharray}{rcl}
- \isarcmd{record} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-\begin{rail}
- 'record' typespec '=' (type '+')? (field +)
- ;
-
- field: name '::' type comment?
- ;
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
- defines extensible record type $(\vec\alpha)t$, derived from the optional
- parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
- See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on
- simply-typed extensible records.
-\end{descr}
-
-
-\section{Datatypes}\label{sec:hol-datatype}
-
-\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
-\begin{matharray}{rcl}
- \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
- \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-\railalias{repdatatype}{rep\_datatype}
-\railterm{repdatatype}
-
-\begin{rail}
- 'datatype' (dtspec + 'and')
- ;
- repdatatype (name * ) dtrules
- ;
-
- dtspec: parname? typespec infix? '=' (cons + '|')
- ;
- cons: name (type * ) mixfix? comment?
- ;
- dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
-\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
- ones, generating the standard infrastructure of derived concepts (primitive
- recursion etc.).
-\end{descr}
-
-The induction and exhaustion theorems generated provide case names according
-to the constructors involved, while parameters are named after the types (see
-also \S\ref{sec:cases-induct}).
-
-See \cite{isabelle-HOL} for more details on datatypes. Note that the theory
-syntax above has been slightly simplified over the old version, usually
-requiring more quotes and less parentheses. Apart from proper proof methods
-for case-analysis and induction, there are also emulations of ML tactics
-\texttt{case_tac} and \texttt{induct_tac} available, see
-\S\ref{sec:induct_tac}.
-
-
-\section{Recursive functions}\label{sec:recursion}
-
-\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
-\begin{matharray}{rcl}
- \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
- \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
- \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
-%FIXME
-% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-\railalias{recdefsimp}{recdef\_simp}
-\railterm{recdefsimp}
-
-\railalias{recdefcong}{recdef\_cong}
-\railterm{recdefcong}
-
-\railalias{recdefwf}{recdef\_wf}
-\railterm{recdefwf}
-
-\railalias{recdeftc}{recdef\_tc}
-\railterm{recdeftc}
-
-\begin{rail}
- 'primrec' parname? (equation + )
- ;
- 'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
- ;
- recdeftc thmdecl? tc comment?
- ;
-
- equation: thmdecl? eqn
- ;
- eqn: prop comment?
- ;
- hints: '(' 'hints' (recdefmod * ) ')'
- ;
- recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
- ;
- tc: nameref ('(' nat ')')?
- ;
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
- datatypes, see also \cite{isabelle-HOL}.
-\item [$\isarkeyword{recdef}$] defines general well-founded recursive
- functions (using the TFL package), see also \cite{isabelle-HOL}. The
- $(permissive)$ option tells TFL to recover from failed proof attempts,
- returning unfinished results. The $recdef_simp$, $recdef_cong$, and
- $recdef_wf$ hints refer to auxiliary rules to be used in the internal
- automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\
- \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
- (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
- \S\ref{sec:classical}).
-\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
- termination condition number $i$ (default $1$) as generated by a
- $\isarkeyword{recdef}$ definition of constant $c$.
-
- Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
- internal proofs without manual intervention.
-\end{descr}
-
-Both kinds of recursive definitions accommodate reasoning by induction (cf.\
-\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
-the function definition) refers to a specific induction rule, with parameters
-named according to the user-specified equations. Case names of
-$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
-$\isarkeyword{recdef}$ are numbered (starting from $1$).
-
-The equations provided by these packages may be referred later as theorem list
-$f\mathord.simps$, where $f$ is the (collective) name of the functions
-defined. Individual equations may be named explicitly as well; note that for
-$\isarkeyword{recdef}$ each specification given by the user may result in
-several theorems.
-
-\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
-the following attributes.
-
-\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
-\begin{matharray}{rcl}
- recdef_simp & : & \isaratt \\
- recdef_cong & : & \isaratt \\
- recdef_wf & : & \isaratt \\
-\end{matharray}
-
-\railalias{recdefsimp}{recdef\_simp}
-\railterm{recdefsimp}
-
-\railalias{recdefcong}{recdef\_cong}
-\railterm{recdefcong}
-
-\railalias{recdefwf}{recdef\_wf}
-\railterm{recdefwf}
-
-\begin{rail}
- (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
- ;
-\end{rail}
-
-
-\section{(Co)Inductive sets}\label{sec:hol-inductive}
-
-\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}
-\begin{matharray}{rcl}
- \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
- \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
- mono & : & \isaratt \\
-\end{matharray}
-
-\railalias{condefs}{con\_defs}
-\railterm{condefs}
-
-\begin{rail}
- ('inductive' | 'coinductive') sets intros monos?
- ;
- 'mono' (() | 'add' | 'del')
- ;
-
- sets: (term comment? +)
- ;
- intros: 'intros' (thmdecl? prop comment? +)
- ;
- monos: 'monos' thmrefs comment?
- ;
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
- (co)inductive sets from the given introduction rules.
-\item [$mono$] declares monotonicity rules. These rule are involved in the
- automated monotonicity proof of $\isarkeyword{inductive}$.
-\end{descr}
-
-See \cite{isabelle-HOL} for further information on inductive definitions in
-HOL.
-
-
-\section{Arithmetic}
-
-\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
-\begin{matharray}{rcl}
- arith & : & \isarmeth \\
- arith_split & : & \isaratt \\
-\end{matharray}
-
-\begin{rail}
- 'arith' '!'?
- ;
-\end{rail}
-
-The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
-$real$). Any current facts are inserted into the goal before running the
-procedure. The ``!''~argument causes the full context of assumptions to be
-included. The $arith_split$ attribute declares case split rules to be
-expanded before the arithmetic procedure is invoked.
-
-Note that a simpler (but faster) version of arithmetic reasoning is already
-performed by the Simplifier.
-
-
-\section{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
-
-The following important tactical tools of Isabelle/HOL have been ported to
-Isar. These should be never used in proper proof texts!
-
-\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
-\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
-\begin{matharray}{rcl}
- case_tac^* & : & \isarmeth \\
- induct_tac^* & : & \isarmeth \\
- ind_cases^* & : & \isarmeth \\
- \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-\railalias{casetac}{case\_tac}
-\railterm{casetac}
-
-\railalias{inducttac}{induct\_tac}
-\railterm{inducttac}
-
-\railalias{indcases}{ind\_cases}
-\railterm{indcases}
-
-\railalias{inductivecases}{inductive\_cases}
-\railterm{inductivecases}
-
-\begin{rail}
- casetac goalspec? term rule?
- ;
- inducttac goalspec? (insts * 'and') rule?
- ;
- indcases (prop +)
- ;
- inductivecases thmdecl? (prop +) comment?
- ;
-
- rule: ('rule' ':' thmref)
- ;
-\end{rail}
-
-\begin{descr}
-\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
- only (unless an alternative rule is given explicitly). Furthermore,
- $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
- variables to be given as instantiation. These tactic emulations feature
- both goal addressing and dynamic instantiation. Note that named rule cases
- are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
- methods (see \S\ref{sec:cases-induct}).
-
-\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
- to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted
- forward manner.
-
- While $ind_cases$ is a proof method to apply the result immediately as
- elimination rules, $\isarkeyword{inductive_cases}$ provides case split
- theorems at the theory level for later use,
-\end{descr}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "isar-ref"
-%%% End:
--- a/doc-src/IsarRef/intro.tex Thu Jan 03 17:01:59 2002 +0100
+++ b/doc-src/IsarRef/intro.tex Thu Jan 03 17:48:02 2002 +0100
@@ -265,6 +265,8 @@
\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
+%FIXME tune
+
This is one of the key questions, of course. Isar offers a rather different
approach to formal proof documents than plain old tactic scripts. Experienced
users of existing interactive theorem proving systems may have to learn
--- a/doc-src/IsarRef/isar-ref.tex Thu Jan 03 17:01:59 2002 +0100
+++ b/doc-src/IsarRef/isar-ref.tex Thu Jan 03 17:48:02 2002 +0100
@@ -89,8 +89,7 @@
\include{syntax}
\include{pure}
\include{generic}
-\include{hol}
-\include{zf}
+\include{logics}
\appendix
\include{refcard}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/logics.tex Thu Jan 03 17:48:02 2002 +0100
@@ -0,0 +1,500 @@
+
+\chapter{Object-logic specific elements}\label{ch:logics}
+
+\section{General logic setup}\label{sec:object-logic}
+
+\indexisarcmd{judgment}
+\indexisarmeth{atomize}\indexisaratt{atomize}
+\indexisaratt{rule-format}\indexisaratt{rulify}
+
+\begin{matharray}{rcl}
+ \isarcmd{judgment} & : & \isartrans{theory}{theory} \\
+ atomize & : & \isarmeth \\
+ atomize & : & \isaratt \\
+ rule_format & : & \isaratt \\
+ rulify & : & \isaratt \\
+\end{matharray}
+
+The very starting point for any Isabelle object-logic is a ``truth judgment''
+that links object-level statements to the meta-logic (with its minimal
+language of $prop$ that covers universal quantification $\Forall$ and
+implication $\Imp$). Common object-logics are sufficiently expressive to
+\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own
+language. This is useful in certain situations where a rule needs to be
+viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x
+\in A \Imp P(x)$ versus $\forall x \in A. P(x)$).
+
+From the following language elements, only the $atomize$ method and
+$rule_format$ attribute are occasionally required by end-users, the rest is
+for those who need to setup their own object-logic. In the latter case
+existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as
+realistic examples.
+
+Generic tools may refer to the information provided by object-logic
+declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical
+Reasoner \S\ref{sec:classical}).
+
+\railalias{ruleformat}{rule\_format}
+\railterm{ruleformat}
+
+\begin{rail}
+ 'judgment' constdecl
+ ;
+ ruleformat ('(' noasm ')')?
+ ;
+\end{rail}
+
+\begin{descr}
+
+\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the
+ truth judgment of the current object-logic. Its type $\sigma$ should
+ specify a coercion of the category of object-level propositions to $prop$ of
+ the Pure meta-logic; the mixfix annotation $syn$ would typically just link
+ the object language (internally of syntactic category $logic$) with that of
+ $prop$. Only one $\isarkeyword{judgment}$ declaration may be given in any
+ theory development.
+
+\item [$atomize$] (as a method) rewrites any non-atomic premises of a
+ sub-goal, using the meta-level equations declared via $atomize$ (as an
+ attribute) beforehand. As a result, heavily nested goals become amenable to
+ fundamental operations such as resolution (cf.\ the $rule$ method) and
+ proof-by-assumption (cf.\ $assumption$).
+
+ A typical collection of $atomize$ rules for a particular object-logic would
+ provide an internalization for each of the connectives of $\Forall$, $\Imp$,
+ and $\equiv$. Meta-level conjunction expressed in the manner of minimal
+ higher-order logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$
+ should be covered as well (this is particularly important for locales, see
+ \S\ref{sec:locale}).
+
+\item [$rule_format$] rewrites a theorem by the equalities declared as
+ $rulify$ rules in the current object-logic. By default, the result is fully
+ normalized, including assumptions and conclusions at any depth. The
+ $no_asm$ option restricts the transformation to the conclusion of a rule.
+
+ In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to
+ replace (bounded) universal quantification ($\forall$) and implication
+ ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.
+
+\end{descr}
+
+
+\section{HOL}
+
+\subsection{Primitive types}\label{sec:typedef}
+
+\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
+\begin{matharray}{rcl}
+ \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
+ \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
+\end{matharray}
+
+\begin{rail}
+ 'typedecl' typespec infix? comment?
+ ;
+ 'typedef' parname? typespec infix? \\ '=' term comment?
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
+ $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
+ also declares type arity $t :: (term, \dots, term) term$, making $t$ an
+ actual HOL type constructor.
+\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
+ non-emptiness of the set $A$. After finishing the proof, the theory will be
+ augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL}
+ for more information. Note that user-level theories usually do not directly
+ refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
+ packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and
+ $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
+\end{descr}
+
+
+\subsection{Low-level tuples}
+
+\indexisarattof{HOL}{split-format}
+\begin{matharray}{rcl}
+ split_format^* & : & \isaratt \\
+\end{matharray}
+
+\railalias{splitformat}{split\_format}
+\railterm{splitformat}
+\railterm{complete}
+
+\begin{rail}
+ splitformat (((name * ) + 'and') | ('(' complete ')'))
+ ;
+\end{rail}
+
+\begin{descr}
+
+\item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
+ tuple types into canonical form as specified by the arguments given; $\vec
+ p@i$ refers to occurrences in premise $i$ of the rule. The
+ $split_format~(complete)$ form causes \emph{all} arguments in function
+ applications to be represented canonically according to their tuple type
+ structure.
+
+ Note that these operations tend to invent funny names for new local
+ parameters to be introduced.
+
+\end{descr}
+
+
+\subsection{Records}\label{sec:hol-record}
+
+FIXME proof tools (simp, cases/induct; no split!?);
+
+FIXME mixfix syntax;
+
+\indexisarcmdof{HOL}{record}
+\begin{matharray}{rcl}
+ \isarcmd{record} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\begin{rail}
+ 'record' typespec '=' (type '+')? (constdecl +)
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
+ defines extensible record type $(\vec\alpha)t$, derived from the optional
+ parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
+ See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on
+ simply-typed extensible records.
+\end{descr}
+
+
+\subsection{Datatypes}\label{sec:hol-datatype}
+
+\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
+\begin{matharray}{rcl}
+ \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
+ \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\railalias{repdatatype}{rep\_datatype}
+\railterm{repdatatype}
+
+\begin{rail}
+ 'datatype' (dtspec + 'and')
+ ;
+ repdatatype (name * ) dtrules
+ ;
+
+ dtspec: parname? typespec infix? '=' (cons + '|')
+ ;
+ cons: name (type * ) mixfix? comment?
+ ;
+ dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
+\end{rail}
+
+\begin{descr}
+\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
+\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
+ ones, generating the standard infrastructure of derived concepts (primitive
+ recursion etc.).
+\end{descr}
+
+The induction and exhaustion theorems generated provide case names according
+to the constructors involved, while parameters are named after the types (see
+also \S\ref{sec:cases-induct}).
+
+See \cite{isabelle-HOL} for more details on datatypes. Note that the theory
+syntax above has been slightly simplified over the old version, usually
+requiring more quotes and less parentheses. Apart from proper proof methods
+for case-analysis and induction, there are also emulations of ML tactics
+\texttt{case_tac} and \texttt{induct_tac} available, see
+\S\ref{sec:induct_tac}.
+
+
+\subsection{Recursive functions}\label{sec:recursion}
+
+\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
+\begin{matharray}{rcl}
+ \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
+ \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
+ \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
+%FIXME
+% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\railalias{recdefsimp}{recdef\_simp}
+\railterm{recdefsimp}
+
+\railalias{recdefcong}{recdef\_cong}
+\railterm{recdefcong}
+
+\railalias{recdefwf}{recdef\_wf}
+\railterm{recdefwf}
+
+\railalias{recdeftc}{recdef\_tc}
+\railterm{recdeftc}
+
+\begin{rail}
+ 'primrec' parname? (equation + )
+ ;
+ 'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
+ ;
+ recdeftc thmdecl? tc comment?
+ ;
+
+ equation: thmdecl? eqn
+ ;
+ eqn: prop comment?
+ ;
+ hints: '(' 'hints' (recdefmod * ) ')'
+ ;
+ recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
+ ;
+ tc: nameref ('(' nat ')')?
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
+ datatypes, see also \cite{isabelle-HOL}.
+\item [$\isarkeyword{recdef}$] defines general well-founded recursive
+ functions (using the TFL package), see also \cite{isabelle-HOL}. The
+ $(permissive)$ option tells TFL to recover from failed proof attempts,
+ returning unfinished results. The $recdef_simp$, $recdef_cong$, and
+ $recdef_wf$ hints refer to auxiliary rules to be used in the internal
+ automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\
+ \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
+ (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
+ \S\ref{sec:classical}).
+\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
+ termination condition number $i$ (default $1$) as generated by a
+ $\isarkeyword{recdef}$ definition of constant $c$.
+
+ Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
+ internal proofs without manual intervention.
+\end{descr}
+
+Both kinds of recursive definitions accommodate reasoning by induction (cf.\
+\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
+the function definition) refers to a specific induction rule, with parameters
+named according to the user-specified equations. Case names of
+$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
+$\isarkeyword{recdef}$ are numbered (starting from $1$).
+
+The equations provided by these packages may be referred later as theorem list
+$f\mathord.simps$, where $f$ is the (collective) name of the functions
+defined. Individual equations may be named explicitly as well; note that for
+$\isarkeyword{recdef}$ each specification given by the user may result in
+several theorems.
+
+\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
+the following attributes.
+
+\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
+\begin{matharray}{rcl}
+ recdef_simp & : & \isaratt \\
+ recdef_cong & : & \isaratt \\
+ recdef_wf & : & \isaratt \\
+\end{matharray}
+
+\railalias{recdefsimp}{recdef\_simp}
+\railterm{recdefsimp}
+
+\railalias{recdefcong}{recdef\_cong}
+\railterm{recdefcong}
+
+\railalias{recdefwf}{recdef\_wf}
+\railterm{recdefwf}
+
+\begin{rail}
+ (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
+ ;
+\end{rail}
+
+
+\subsection{(Co)Inductive sets}\label{sec:hol-inductive}
+
+\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}
+\begin{matharray}{rcl}
+ \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
+ \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
+ mono & : & \isaratt \\
+\end{matharray}
+
+\railalias{condefs}{con\_defs}
+\railterm{condefs}
+
+\begin{rail}
+ ('inductive' | 'coinductive') sets intros monos?
+ ;
+ 'mono' (() | 'add' | 'del')
+ ;
+
+ sets: (term comment? +)
+ ;
+ intros: 'intros' (thmdecl? prop comment? +)
+ ;
+ monos: 'monos' thmrefs comment?
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
+ (co)inductive sets from the given introduction rules.
+\item [$mono$] declares monotonicity rules. These rule are involved in the
+ automated monotonicity proof of $\isarkeyword{inductive}$.
+\end{descr}
+
+See \cite{isabelle-HOL} for further information on inductive definitions in
+HOL.
+
+
+\subsection{Arithmetic proof support}
+
+\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
+\begin{matharray}{rcl}
+ arith & : & \isarmeth \\
+ arith_split & : & \isaratt \\
+\end{matharray}
+
+\begin{rail}
+ 'arith' '!'?
+ ;
+\end{rail}
+
+The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
+$real$). Any current facts are inserted into the goal before running the
+procedure. The ``!''~argument causes the full context of assumptions to be
+included. The $arith_split$ attribute declares case split rules to be
+expanded before the arithmetic procedure is invoked.
+
+Note that a simpler (but faster) version of arithmetic reasoning is already
+performed by the Simplifier.
+
+
+\subsection{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
+
+The following important tactical tools of Isabelle/HOL have been ported to
+Isar. These should be never used in proper proof texts!
+
+\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
+\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
+\begin{matharray}{rcl}
+ case_tac^* & : & \isarmeth \\
+ induct_tac^* & : & \isarmeth \\
+ ind_cases^* & : & \isarmeth \\
+ \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\railalias{casetac}{case\_tac}
+\railterm{casetac}
+
+\railalias{inducttac}{induct\_tac}
+\railterm{inducttac}
+
+\railalias{indcases}{ind\_cases}
+\railterm{indcases}
+
+\railalias{inductivecases}{inductive\_cases}
+\railterm{inductivecases}
+
+\begin{rail}
+ casetac goalspec? term rule?
+ ;
+ inducttac goalspec? (insts * 'and') rule?
+ ;
+ indcases (prop +)
+ ;
+ inductivecases thmdecl? (prop +) comment?
+ ;
+
+ rule: ('rule' ':' thmref)
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
+ only (unless an alternative rule is given explicitly). Furthermore,
+ $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
+ variables to be given as instantiation. These tactic emulations feature
+ both goal addressing and dynamic instantiation. Note that named rule cases
+ are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
+ methods (see \S\ref{sec:cases-induct}).
+
+\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
+ to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted
+ forward manner.
+
+ While $ind_cases$ is a proof method to apply the result immediately as
+ elimination rules, $\isarkeyword{inductive_cases}$ provides case split
+ theorems at the theory level for later use,
+\end{descr}
+
+
+\section{HOLCF}
+
+\subsection{Mixfix syntax for continuous operations}
+
+\indexisarcmdof{HOLCF}{consts}\indexisarcmdof{HOLCF}{constdefs}
+
+\begin{matharray}{rcl}
+ \isarcmd{consts} & : & \isartrans{theory}{theory} \\
+ \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+HOLCF provides a separate type for continuous functions $\alpha \rightarrow
+\beta$, with an explicit application operator $f \cdot x$. Isabelle mixfix
+syntax normally refers directly to the pure meta-level function type $\alpha
+\To \beta$, with application $f\,x$.
+
+The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ have the same outer syntax as
+the pure versions (cf.\ \S\ref{sec:consts}). Internally, declarations
+involving continuous function types are treated specifically, transforming the
+syntax template accordingly and generating syntax translation rules for the
+abstract and concrete representation of application.
+
+The behavior for plain meta-level function types is unchanged. Mixed
+continuous and meta-level application is \emph{not} supported.
+
+\subsection{Recursive domains}
+
+\indexisarcmdof{HOLCF}{domain}
+\begin{matharray}{rcl}
+ \isarcmd{domain} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\begin{rail}
+ 'domain' parname? (dmspec + 'and')
+ ;
+
+ dmspec: typespec '=' (cons + '|')
+ ;
+ cons: name (type * ) mixfix? comment?
+ ;
+ dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
+\end{rail}
+
+Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\
+\S\ref{sec:hol-datatype}). Mutual recursive is supported, but no nesting nor
+arbitrary branching. Domain constructors may be strict (default) or lazy, the
+latter admits to introduce infinitary objects in the typical LCF manner (lazy
+lists etc.).
+
+See also \cite{MuellerNvOS99} for further information HOLCF domains in
+general.
+
+
+\section{ZF}
+
+\subsection{Type checking}
+
+FIXME
+
+\subsection{Inductive sets and datatypes}
+
+FIXME
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "isar-ref"
+%%% End:
--- a/doc-src/IsarRef/pure.tex Thu Jan 03 17:01:59 2002 +0100
+++ b/doc-src/IsarRef/pure.tex Thu Jan 03 17:48:02 2002 +0100
@@ -5,8 +5,8 @@
commands, together with fundamental proof methods and attributes.
Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic
tools and packages (such as the Simplifier) that are either part of Pure
-Isabelle or pre-installed by most object logics. Chapter~\ref{ch:hol-tools}
-refers to actual object-logic specific elements of Isabelle/HOL.
+Isabelle or pre-installed by most object logics. Chapter~\ref{ch:logics}
+refers to object-logic specific elements (mainly for HOL and ZF).
\medskip
@@ -16,15 +16,14 @@
are subsequently marked by ``$^*$'', are often helpful when developing proof
documents, while their use is discouraged for the final outcome. Typical
examples are diagnostic commands that print terms or theorems according to the
-current context; other commands even emulate old-style tactical theorem
-proving.
+current context; other commands emulate old-style tactical theorem proving.
-\section{Theory specification commands}
+\section{Theory commands}
\subsection{Defining theories}\label{sec:begin-thy}
-\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
+\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{context}\indexisarcmd{end}
\begin{matharray}{rcl}
\isarcmd{header} & : & \isarkeep{toplevel} \\
\isarcmd{theory} & : & \isartrans{toplevel}{theory} \\
@@ -38,14 +37,14 @@
proof as well. In contrast, ``old-style'' Isabelle theories support batch
processing only, with the proof scripts collected in separate ML files.
-The first actual command of any theory has to be $\THEORY$, starting a new
-theory based on the merge of existing ones. Just preceding $\THEORY$, there
-may be an optional $\isarkeyword{header}$ declaration, which is relevant to
-document preparation only; it acts very much like a special pre-theory markup
-command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The theory
-context may be also changed by $\CONTEXT$ without creating a new theory. In
-both cases, $\END$ concludes the theory development; it has to be the very
-last command of any theory file.
+The first ``real'' command of any theory has to be $\THEORY$, which starts a
+new theory based on the merge of existing ones. Just preceding $\THEORY$,
+there may be an optional $\isarkeyword{header}$ declaration, which is relevant
+to document preparation only; it acts very much like a special pre-theory
+markup command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The
+$\END$ commands concludes a theory development; it has to be the very last
+command of any theory file to loaded in batch-mode. The theory context may be
+also changed interactively by $\CONTEXT$ without creating a new theory.
\begin{rail}
'header' text
@@ -54,8 +53,6 @@
;
'context' name
;
- 'end'
- ;;
filespecs: 'files' ((name | parname) +);
\end{rail}
@@ -67,28 +64,42 @@
produce chapter or section headings. See also \S\ref{sec:markup-thy} and
\S\ref{sec:markup-prf} for further markup commands.
-\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] commences a new theory $A$
- based on existing ones $B@1 + \cdots + B@n$. Isabelle's theory loader
- system ensures that any of the base theories are properly loaded (and fully
- up-to-date when $\THEORY$ is executed interactively). The optional
- $\isarkeyword{files}$ specification declares additional dependencies on ML
- files. Unless put in parentheses, any file will be loaded immediately via
- $\isarcmd{use}$ (see also \S\ref{sec:ML}). The optional ML file
- \texttt{$A$.ML} that may be associated with any theory should \emph{not} be
- included in $\isarkeyword{files}$, though.
+\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] starts a new theory $A$ based
+ on the merge of existing theories $B@1, \dots, B@n$.
+
+ Due to inclusion of several ancestors, the overall theory structure emerging
+ in an Isabelle session forms a directed acyclic graph (DAG). Isabelle's
+ theory loader ensures that the sources contributing to the development graph
+ are always up-to-date. Changed files are automatically reloaded when
+ processing theory headers interactively; batch-mode explicitly distinguishes
+ \verb,update_thy, from \verb,use_thy,, see also \cite{isabelle-ref}.
+
+ The optional $\isarkeyword{files}$ specification declares additional
+ dependencies on ML files. Files will be loaded immediately, unless the name
+ is put in parentheses, which merely documents the dependency to be resolved
+ later in the text (typically via explicit $\isarcmd{use}$ in the body text,
+ see \S\ref{sec:ML}). In reminiscence of the old-style theory system of
+ Isabelle, \texttt{$A$.thy} may be also accompanied by an additional file
+ \texttt{$A$.ML} consisting of ML code that is executed in the context of the
+ \emph{finished} theory $A$. That file should not be included in the
+ $\isarkeyword{files}$ dependency declaration, though.
\item [$\CONTEXT~B$] enters an existing theory context, basically in read-only
mode, so only a limited set of commands may be performed without destroying
the theory. Just as for $\THEORY$, the theory loader ensures that $B$ is
loaded and up-to-date.
+ This command is occasionally useful for quick interactive experiments;
+ normally one should always commence a new context via $\THEORY$.
+
\item [$\END$] concludes the current theory definition or context switch.
-Note that this command cannot be undone, but the whole theory definition has
-to be retracted.
+ Note that this command cannot be undone, but the whole theory definition has
+ to be retracted.
+
\end{descr}
-\subsection{Theory markup commands}\label{sec:markup-thy}
+\subsection{Markup commands}\label{sec:markup-thy}
\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
\indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw}
@@ -144,9 +155,9 @@
\subsection{Type classes and sorts}\label{sec:classes}
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
-\begin{matharray}{rcl}
+\begin{matharray}{rcll}
\isarcmd{classes} & : & \isartrans{theory}{theory} \\
- \isarcmd{classrel} & : & \isartrans{theory}{theory} \\
+ \isarcmd{classrel} & : & \isartrans{theory}{theory} & (axiomatic!) \\
\isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
\end{matharray}
@@ -169,18 +180,18 @@
proven class relations.
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
any type variables given without sort constraints. Usually, the default
- sort would be only changed when defining new object-logics.
+ sort would be only changed when defining a new object-logic.
\end{descr}
\subsection{Primitive types and type abbreviations}\label{sec:types-pure}
\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
-\begin{matharray}{rcl}
+\begin{matharray}{rcll}
\isarcmd{types} & : & \isartrans{theory}{theory} \\
\isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
\isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
- \isarcmd{arities} & : & \isartrans{theory}{theory} \\
+ \isarcmd{arities} & : & \isartrans{theory}{theory} & (axiomatic!) \\
\end{matharray}
\begin{rail}
@@ -247,10 +258,9 @@
Unless this option is given, a warning message would be issued for any
definitional equation with a more special type than that of the
corresponding constant declaration.
-
-\item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and
- definitions of constants, using the canonical name $c_def$ for the
- definitional axiom.
+
+\item [$\CONSTDEFS~c::\sigma~eqn$] combines declarations and definitions of
+ constants, using the canonical name $c_def$ for the definitional axiom.
\end{descr}
@@ -300,8 +310,8 @@
\subsection{Axioms and theorems}\label{sec:axms-thms}
\indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems}
-\begin{matharray}{rcl}
- \isarcmd{axioms} & : & \isartrans{theory}{theory} \\
+\begin{matharray}{rcll}
+ \isarcmd{axioms} & : & \isartrans{theory}{theory} & (axiomatic!) \\
\isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
\isarcmd{theorems} & : & \isartrans{theory}{theory} \\
\end{matharray}
@@ -366,9 +376,7 @@
name space (which may be $class$, $type$, or $const$). Hidden objects
remain valid within the logic, but are inaccessible from user input. In
output, the special qualifier ``$\mathord?\mathord?$'' is prefixed to the
- full internal name.
-
- Unqualified (global) names may not be hidden deliberately.
+ full internal name. Unqualified (global) names may not be hidden.
\end{descr}
@@ -550,9 +558,15 @@
goal claimed next.
\end{descr}
-%FIXME diagram?
+The proof mode indicator may be read as a verb telling the writer what kind of
+operation may be performed next. The corresponding typings of proof commands
+restricts the shape of well-formed proof texts to particular command
+sequences. So dynamic arrangements of commands eventually turn out as static
+texts. Appendix~\ref{ap:refcard} gives a simplified grammar of the overall
+(extensible) language emerging that way.
-\subsection{Proof markup commands}\label{sec:markup-prf}
+
+\subsection{Markup commands}\label{sec:markup-prf}
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
\indexisarcmd{txt}\indexisarcmd{txt-raw}
@@ -576,7 +590,7 @@
\end{rail}
-\subsection{Proof context}\label{sec:proof-context}
+\subsection{Context elements}\label{sec:proof-context}
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
\begin{matharray}{rcl}
@@ -699,7 +713,7 @@
Forward chaining with an empty list of theorems is the same as not chaining.
Thus $\FROM{nothing}$ has no effect apart from entering $prove(chain)$ mode,
-since $nothing$\indexisarthm{nothing} is bound to the empty list of facts.
+since $nothing$\indexisarthm{nothing} is bound to the empty list of theorems.
\subsection{Goal statements}
@@ -716,11 +730,11 @@
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
\end{matharray}
-From a theory context, proof mode is entered from theory mode by initial goal
-commands $\LEMMANAME$, $\THEOREMNAME$, and $\COROLLARYNAME$. Within a proof,
-new claims may be introduced locally as well; four variants are available,
-indicating whether the result is meant to solve some pending goal or whether
-forward chaining is indicated.
+From a theory context, proof mode is entered by an initial goal command such
+as $\LEMMANAME$, $\THEOREMNAME$, $\COROLLARYNAME$. Within a proof, new claims
+may be introduced locally as well; four variants are available here to
+indicate whether forward chaining of facts should be performed initially (via
+$\THEN$), and whether the emerging result is meant to solve some pending goal.
Goals may consist of multiple statements, resulting in a list of facts
eventually. A pending multi-goal is internally represented as a meta-level
@@ -731,16 +745,21 @@
the $induct$ method covered in \S\ref{sec:cases-induct-meth} acts on
multiple claims simultaneously.}
-%FIXME define locale, context
-
\begin{rail}
- ('lemma' | 'theorem' | 'corollary') locale context goal
+ ('lemma' | 'theorem' | 'corollary') goalprefix goal
;
('have' | 'show' | 'hence' | 'thus') goal
;
goal: (props comment? + 'and')
;
+
+ goalprefix: thmdecl? locale? context?
+ ;
+ locale: '(' 'in' name ')'
+ ;
+ context: '(' (contextelem +) ')'
+ ;
\end{rail}
\begin{descr}
@@ -749,8 +768,8 @@
theory context, and optionally into the specified locale, cf.\
\S\ref{sec:locale}. An additional \railnonterm{context} specification may
build an initial proof context for the subsequent claim; this may include
- local definitions and syntax as well, see \S\ref{sec:locale} for more
- information.
+ local definitions and syntax as well, see the definition of $contextelem$ in
+ \S\ref{sec:locale}.
\item [$\THEOREM{a}{\vec\phi}$ and $\COROLLARY{a}{\vec\phi}$] are essentially
the same as $\LEMMA{a}{\vec\phi}$, but the facts are internally marked as
@@ -832,18 +851,19 @@
remaining goals. No facts are passed to $m@2$.
\end{enumerate}
-The only other proper way to affect pending goals is by $\SHOWNAME$, which
-involves an explicit statement of what is to be solved.
+The only other proper way to affect pending goals in a proof body is by
+$\SHOWNAME$, which involves an explicit statement of what is to be solved
+eventually. Thus we avoid the fundamental problem of unstructured tactic
+scripts that consist of numerous consecutive goal transformations, with
+invisible effects.
\medskip
-Also note that initial proof methods should either solve the goal completely,
-or constitute some well-understood reduction to new sub-goals. Arbitrary
-automatic proof tools that are prone leave a large number of badly structured
-sub-goals are no help in continuing the proof document in any intelligible
-way.
-
-\medskip
+As a general rule of thumb for good proof style, initial proof methods should
+either solve the goal completely, or constitute some well-understood reduction
+to new sub-goals. Arbitrary automatic proof tools that are prone leave a
+large number of badly structured sub-goals are no help in continuing the proof
+document in any intelligible way.
Unless given explicitly by the user, the default initial method is ``$rule$'',
which applies a single standard elimination or introduction rule according to
@@ -903,11 +923,12 @@
The following proof methods and attributes refer to basic logical operations
of Isar. Further methods and attributes are provided by several generic and
object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
-\ref{ch:hol-tools}).
+\ref{ch:logics}).
\indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$}
-\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{rule}
\indexisaratt{OF}\indexisaratt{of}
+\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
+\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
\begin{matharray}{rcl}
assumption & : & \isarmeth \\
this & : & \isarmeth \\
@@ -921,6 +942,8 @@
rule & : & \isaratt \\
\end{matharray}
+%FIXME intro!, intro, intro?
+
\begin{rail}
'rule' thmrefs?
;
@@ -990,8 +1013,8 @@
patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
postfix position.
-Polymorphism of term bindings is handled in Hindley-Milner style, as in ML.
-Type variables referring to local assumptions or open goal statements are
+Polymorphism of term bindings is handled in Hindley-Milner style, similar to
+ML. Type variables referring to local assumptions or open goal statements are
\emph{fixed}, while those of finished results or bound by $\LETNAME$ may occur
in \emph{arbitrary} instances later. Even though actual polymorphism should
be rarely used in practice, this mechanism is essential to achieve proper
--- a/doc-src/IsarRef/zf.tex Thu Jan 03 17:01:59 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-
-\chapter{Isabelle/ZF specific elements}\label{ch:zf-tools}
-
-\section{Type checking}
-
-FIXME
-
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "isar-ref"
-%%% End: