--- a/doc-src/IsarRef/conversion.tex Wed Jan 02 21:52:54 2002 +0100
+++ b/doc-src/IsarRef/conversion.tex Wed Jan 02 21:53:50 2002 +0100
@@ -255,7 +255,7 @@
qed_spec_mp "\(name\)";
\end{ttbox}
The operation performed by \texttt{qed_spec_mp} is also performed by the Isar
-attribute ``$rule_format$'', see also \S\ref{sec:rule-format}. Thus the
+attribute ``$rule_format$'', see also \S\ref{sec:object-logic}. Thus the
corresponding Isar text may look like this:
\begin{matharray}{l}
\LEMMA{name~[rule_format]}{\texttt"{\phi}\texttt"} \\
@@ -310,7 +310,7 @@
single or multiple arguments. Although it is more convenient in most cases to
use the plain $rule$ method (see \S\ref{sec:pure-meth-att}), or any of its
``improper'' variants $erule$, $drule$, $frule$ (see
-\S\ref{sec:misc-methods}). Note that explicit goal addressing is only
+\S\ref{sec:misc-meth-att}). Note that explicit goal addressing is only
supported by the actual $rule_tac$ version.
With this in mind, plain resolution tactics may be ported as follows.
--- a/doc-src/IsarRef/generic.tex Wed Jan 02 21:52:54 2002 +0100
+++ b/doc-src/IsarRef/generic.tex Wed Jan 02 21:53:50 2002 +0100
@@ -1,7 +1,9 @@
\chapter{Generic Tools and Packages}\label{ch:gen-tools}
-\section{Axiomatic Type Classes}\label{sec:axclass}
+\section{Theory commands}
+
+\subsection{Axiomatic type classes}\label{sec:axclass}
%FIXME
% - qualified names
@@ -51,7 +53,14 @@
\end{descr}
-\section{Calculational proof}\label{sec:calculation}
+\subsection{Locales and local contexts}\label{sec:locale}
+
+FIXME
+
+
+\section{Proof commands}
+
+\subsection{Calculational Reasoning}\label{sec:calculation}
\indexisarcmd{also}\indexisarcmd{finally}
\indexisarcmd{moreover}\indexisarcmd{ultimately}
@@ -141,110 +150,24 @@
\end{descr}
-\section{Named local contexts (cases)}\label{sec:cases}
-
-\indexisarcmd{case}\indexisarcmd{print-cases}
-\indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
-\begin{matharray}{rcl}
- \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
- \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
- case_names & : & \isaratt \\
- params & : & \isaratt \\
- consumes & : & \isaratt \\
-\end{matharray}
-
-Basically, Isar proof contexts are built up explicitly using commands like
-$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical
-verification tasks this can become hard to manage, though. In particular, a
-large number of local contexts may emerge from case analysis or induction over
-inductive sets and types.
-
-\medskip
-
-The $\CASENAME$ command provides a shorthand to refer to certain parts of
-logical context symbolically. Proof methods may provide an environment of
-named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of
-$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
-
-It is important to note that $\CASENAME$ does \emph{not} provide any means to
-peek at the current goal state, which is treated as strictly non-observable in
-Isar! Instead, the cases considered here usually emerge in a canonical way
-from certain pieces of specification that appear in the theory somewhere else
-(e.g.\ in an inductive definition, or recursive function). See also
-\S\ref{sec:induct-method} for more details of how this works in HOL.
-
-\medskip
-
-Named cases may be exhibited in the current proof context only if both the
-proof method and the rules involved support this. Case names and parameters
-of basic rules may be declared by hand as well, by using appropriate
-attributes. Thus variant versions of rules that have been derived manually
-may be used in advanced case analysis later.
-
-\railalias{casenames}{case\_names}
-\railterm{casenames}
-
-\begin{rail}
- 'case' nameref attributes?
- ;
- casenames (name + )
- ;
- 'params' ((name * ) + 'and')
- ;
- 'consumes' nat?
- ;
-\end{rail}
-%FIXME bug in rail
-
-\begin{descr}
-\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$,
- as provided by an appropriate proof method (such as $cases$ and $induct$ in
- Isabelle/HOL, see \S\ref{sec:induct-method}). The command $\CASE{c}$
- abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
-\item [$\isarkeyword{print_cases}$] prints all local contexts of the current
- state, using Isar proof language notation. This is a diagnostic command;
- $undo$ does not apply.
-\item [$case_names~\vec c$] declares names for the local contexts of premises
- of some theorem; $\vec c$ refers to the \emph{suffix} of the list of
- premises.
-\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
- premises $1, \dots, n$ of some theorem. An empty list of names may be given
- to skip positions, leaving the present parameters unchanged.
-
- Note that the default usage of case rules does \emph{not} directly expose
- parameters to the proof context (see also \S\ref{sec:induct-method-proper}).
-\item [$consumes~n$] declares the number of ``major premises'' of a rule,
- i.e.\ the number of facts to be consumed when it is applied by an
- appropriate proof method (cf.\ \S\ref{sec:induct-method}). The default
- value of $consumes$ is $n = 1$, which is appropriate for the usual kind of
- cases and induction rules for inductive sets (cf.\ \S\ref{sec:inductive}).
- Rules without any $consumes$ declaration given are treated as if
- $consumes~0$ had been specified.
-
- Note that explicit $consumes$ declarations are only rarely needed; this is
- already taken care of automatically by the higher-level $cases$ and $induct$
- declarations, see also \S\ref{sec:induct-att}.
-\end{descr}
-
-
-\section{Generalized existence}\label{sec:obtain}
+\subsection{Generalized elimination}\label{sec:obtain}
\indexisarcmd{obtain}
\begin{matharray}{rcl}
\isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
\end{matharray}
-Generalized existence means that additional elements with certain properties
-may introduced in the current context. Technically, 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.
+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' (assm comment? + 'and')
+ 'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and')
;
\end{rail}
@@ -277,7 +200,7 @@
where the result is treated as an assumption.
-\section{Miscellaneous methods and attributes}\label{sec:misc-methods}
+\subsection{Miscellaneous methods and attributes}\label{sec:misc-meth-att}
\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert}
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}
@@ -385,7 +308,7 @@
\end{descr}
-\section{Tactic emulations}\label{sec:tactics}
+\subsection{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
@@ -513,6 +436,8 @@
\subsection{Simplification methods}\label{sec:simp}
+\subsubsection{FIXME}
+
\indexisarmeth{simp}\indexisarmeth{simp-all}
\begin{matharray}{rcl}
simp & : & \isarmeth \\
@@ -631,7 +556,7 @@
additional rules). By default the result is fully simplified, including
assumptions and conclusion. The options $no_asm$ etc.\ restrict the
Simplifier in the same way as the for the $simp$ method (see
- \S\ref{sec:simp}).
+ \S\ref{sec:simp}). FIXME args
The $simplified$ operation should be used only very rarely, usually for
experimentation only.
@@ -672,6 +597,7 @@
Note that the $simp$ method already involves repeated application of split
rules as declared in the current context (see \S\ref{sec:simp}).
\item [$symmetric$] applies the symmetry rule of meta or object equality.
+ FIXME sym decl
\end{descr}
@@ -850,13 +776,102 @@
The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only,
and omits the Simplifier declaration. Thus the declaration does not have
any effect on automated proof tools, but only on simple methods such as
- $rule$ (see \S\ref{sec:misc-methods}).
+ $rule$ (see \S\ref{sec:misc-meth-att}).
\end{descr}
-\section{Proof by cases and induction}\label{sec:induct-method}
+\section{Proof by cases and induction}\label{sec:cases-induct}
+
+\subsection{Rule contexts}\label{sec:rule-cases}
+
+\indexisarcmd{case}\indexisarcmd{print-cases}
+\indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
+\begin{matharray}{rcl}
+ \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
+ \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
+ case_names & : & \isaratt \\
+ params & : & \isaratt \\
+ consumes & : & \isaratt \\
+\end{matharray}
+
+Basically, Isar proof contexts are built up explicitly using commands like
+$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical
+verification tasks this can become hard to manage, though. In particular, a
+large number of local contexts may emerge from case analysis or induction over
+inductive sets and types.
+
+\medskip
+
+The $\CASENAME$ command provides a shorthand to refer to certain parts of
+logical context symbolically. Proof methods may provide an environment of
+named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of
+$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
+
+FIXME
+
+It is important to note that $\CASENAME$ does \emph{not} provide any means to
+peek at the current goal state, which is treated as strictly non-observable in
+Isar! Instead, the cases considered here usually emerge in a canonical way
+from certain pieces of specification that appear in the theory somewhere else
+(e.g.\ in an inductive definition, or recursive function).
+
+FIXME
+
+\medskip
+
+Named cases may be exhibited in the current proof context only if both the
+proof method and the rules involved support this. Case names and parameters
+of basic rules may be declared by hand as well, by using appropriate
+attributes. Thus variant versions of rules that have been derived manually
+may be used in advanced case analysis later.
-\subsection{Proof methods}\label{sec:induct-method-proper}
+\railalias{casenames}{case\_names}
+\railterm{casenames}
+
+\begin{rail}
+ 'case' nameref attributes?
+ ;
+ casenames (name + )
+ ;
+ 'params' ((name * ) + 'and')
+ ;
+ 'consumes' nat?
+ ;
+\end{rail}
+%FIXME bug in rail
+
+\begin{descr}
+\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$,
+ as provided by an appropriate proof method (such as $cases$ and $induct$,
+ see \S\ref{sec:cases-induct-meth}). The command $\CASE{c}$ abbreviates
+ $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
+\item [$\isarkeyword{print_cases}$] prints all local contexts of the current
+ state, using Isar proof language notation. This is a diagnostic command;
+ $undo$ does not apply.
+\item [$case_names~\vec c$] declares names for the local contexts of premises
+ of some theorem; $\vec c$ refers to the \emph{suffix} of the list of
+ premises.
+\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
+ premises $1, \dots, n$ of some theorem. An empty list of names may be given
+ to skip positions, leaving the present parameters unchanged.
+
+ Note that the default usage of case rules does \emph{not} directly expose
+ parameters to the proof context (see also \S\ref{sec:cases-induct-meth}).
+\item [$consumes~n$] declares the number of ``major premises'' of a rule,
+ i.e.\ the number of facts to be consumed when it is applied by an
+ appropriate proof method (cf.\ \S\ref{sec:cases-induct-meth}). The default
+ value of $consumes$ is $n = 1$, which is appropriate for the usual kind of
+ cases and induction rules for inductive sets (cf.\
+ \S\ref{sec:hol-inductive}). Rules without any $consumes$ declaration given
+ are treated as if $consumes~0$ had been specified.
+
+ Note that explicit $consumes$ declarations are only rarely needed; this is
+ already taken care of automatically by the higher-level $cases$ and $induct$
+ declarations, see also \S\ref{sec:cases-induct-att}.
+\end{descr}
+
+
+\subsection{Proof methods}\label{sec:cases-induct-meth}
\indexisarmeth{cases}\indexisarmeth{induct}
\begin{matharray}{rcl}
@@ -869,12 +884,13 @@
corresponding rules may be specified and instantiated in a casual manner.
Furthermore, these methods provide named local contexts that may be invoked
via the $\CASENAME$ proof command within the subsequent proof text (cf.\
-\S\ref{sec:cases}). This accommodates compact proof texts even when reasoning
-about large specifications.
+\S\ref{sec:rule-cases}). This accommodates compact proof texts even when
+reasoning about large specifications.
Note that the full spectrum of this generic functionality is currently only
supported by Isabelle/HOL, when used in conjunction with advanced definitional
-packages (see especially \S\ref{sec:datatype} and \S\ref{sec:inductive}).
+packages (see especially \S\ref{sec:hol-datatype} and
+\S\ref{sec:hol-inductive}).
\begin{rail}
'cases' spec
@@ -920,7 +936,7 @@
\S\ref{sec:pure-meth-att}). This feature is rarely needed in practice; a
typical application would be to specify additional arguments for rules
stemming from parameterized inductive definitions (see also
- \S\ref{sec:inductive}).
+ \S\ref{sec:hol-inductive}).
The $open$ option causes the parameters of the new local contexts to be
exposed to the current proof context. Thus local variables stemming from
@@ -949,7 +965,7 @@
way as for $cases$, see above.
\end{descr}
-Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
+Above methods produce named local contexts (cf.\ \S\ref{sec:rule-cases}), as
determined by the instantiated rule \emph{before} it has been applied to the
internal proof state.\footnote{As a general principle, Isar proof text may
never refer to parts of proof states directly.} Thus proper use of symbolic
@@ -961,8 +977,8 @@
term variable $\Var{case}$\indexisarvar{case} --- for each case where it is
fully specified.
-The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
-cases present in the current proof state.
+The $\isarkeyword{print_cases}$ command (\S\ref{sec:rule-cases}) prints all
+named cases present in the current proof state.
\medskip
@@ -984,12 +1000,11 @@
\medskip
Facts presented to either method are consumed according to the number of
-``major premises'' of the rule involved (see also \S\ref{sec:induct-att} and
-\S\ref{sec:cases}), which is usually $0$ for plain cases and induction rules
-of datatypes etc.\ and $1$ for rules of inductive sets and the like. The
-remaining facts are inserted into the goal verbatim before the actual $cases$
-or $induct$ rule is applied (thus facts may be even passed through an
-induction).
+``major premises'' of the rule involved (see also \S\ref{sec:cases-induct}),
+which is usually $0$ for plain cases and induction rules of datatypes etc.\
+and $1$ for rules of inductive sets and the like. The remaining facts are
+inserted into the goal verbatim before the actual $cases$ or $induct$ rule is
+applied (thus facts may be even passed through an induction).
Note that whenever facts are present, the default rule selection scheme would
provide a ``set'' rule only, with the first fact consumed and the rest
@@ -998,7 +1013,7 @@
``$type: name$'' to the method argument.
-\subsection{Declaring rules}\label{sec:induct-att}
+\subsection{Declaring rules}\label{sec:cases-induct-att}
\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
\begin{matharray}{rcl}
@@ -1022,14 +1037,90 @@
declared by advanced definitional packages. For special applications, these
may be replaced manually by variant versions.
-Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:cases}) to
+Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:rule-cases}) to
adjust names of cases and parameters of a rule.
-The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of
+The $consumes$ declaration (cf.\ \S\ref{sec:rule-cases}) is taken care of
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 Wed Jan 02 21:52:54 2002 +0100
+++ b/doc-src/IsarRef/hol.tex Wed Jan 02 21:53:50 2002 +0100
@@ -1,36 +1,24 @@
-\chapter{Isabelle/HOL Tools and Packages}\label{ch:hol-tools}
+\chapter{Isabelle/HOL specific elements}\label{ch:hol-tools}
-\section{Miscellaneous attributes}\label{sec:rule-format}
+\section{Miscellaneous attributes}
-\indexisaratt{rule-format}\indexisaratt{split-format}
+\indexisarattof{HOL}{split-format}
\begin{matharray}{rcl}
- rule_format & : & \isaratt \\
split_format^* & : & \isaratt \\
\end{matharray}
-\railalias{ruleformat}{rule\_format}
-\railterm{ruleformat}
-
\railalias{splitformat}{split\_format}
\railterm{splitformat}
\railterm{complete}
\begin{rail}
- ruleformat ('(' noasm ')')?
- ;
splitformat (((name * ) + 'and') | ('(' complete ')'))
;
\end{rail}
\begin{descr}
-\item [$rule_format$] causes a theorem to be put into standard object-rule
- form, replacing implication and (bounded) universal quantification of HOL by
- the corresponding meta-logical connectives. 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.
-
\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
@@ -45,7 +33,7 @@
\section{Primitive types}\label{sec:typedef}
-\indexisarcmd{typedecl}\indexisarcmd{typedef}
+\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
\begin{matharray}{rcl}
\isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
\isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
@@ -68,14 +56,16 @@
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:record}) and
- $\isarkeyword{datatype}$ (see \S\ref{sec:datatype}).
+ 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:record}
+\section{Records}\label{sec:hol-record}
-\indexisarcmd{record}
+FIXME proof tools (simp, cases/induct; no split!?);
+
+\indexisarcmdof{HOL}{record}
\begin{matharray}{rcl}
\isarcmd{record} & : & \isartrans{theory}{theory} \\
\end{matharray}
@@ -97,9 +87,9 @@
\end{descr}
-\section{Datatypes}\label{sec:datatype}
+\section{Datatypes}\label{sec:hol-datatype}
-\indexisarcmd{datatype}\indexisarcmd{rep-datatype}
+\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
\begin{matharray}{rcl}
\isarcmd{datatype} & : & \isartrans{theory}{theory} \\
\isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
@@ -130,7 +120,7 @@
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:induct-method}).
+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
@@ -142,7 +132,7 @@
\section{Recursive functions}\label{sec:recursion}
-\indexisarcmd{primrec}\indexisarcmd{recdef}\indexisarcmd{recdef-tc}
+\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
\begin{matharray}{rcl}
\isarcmd{primrec} & : & \isartrans{theory}{theory} \\
\isarcmd{recdef} & : & \isartrans{theory}{theory} \\
@@ -204,9 +194,9 @@
\end{descr}
Both kinds of recursive definitions accommodate reasoning by induction (cf.\
-\S\ref{sec:induct-method}): 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
+\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$).
@@ -219,7 +209,7 @@
\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
the following attributes.
-\indexisaratt{recdef-simp}\indexisaratt{recdef-cong}\indexisaratt{recdef-wf}
+\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
\begin{matharray}{rcl}
recdef_simp & : & \isaratt \\
recdef_cong & : & \isaratt \\
@@ -241,9 +231,9 @@
\end{rail}
-\section{(Co)Inductive sets}\label{sec:inductive}
+\section{(Co)Inductive sets}\label{sec:hol-inductive}
-\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono}
+\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}
\begin{matharray}{rcl}
\isarcmd{inductive} & : & \isartrans{theory}{theory} \\
\isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
@@ -280,7 +270,7 @@
\section{Arithmetic}
-\indexisarmeth{arith}\indexisaratt{arith-split}
+\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
\begin{matharray}{rcl}
arith & : & \isarmeth \\
arith_split & : & \isaratt \\
@@ -306,8 +296,8 @@
The following important tactical tools of Isabelle/HOL have been ported to
Isar. These should be never used in proper proof texts!
-\indexisarmeth{case-tac}\indexisarmeth{induct-tac}
-\indexisarmeth{ind-cases}\indexisarcmd{inductive-cases}
+\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 \\
@@ -346,10 +336,9 @@
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 local
- contexts (see \S\ref{sec:cases}) are \emph{not} provided as would be by the
- proper $induct$ and $cases$ proof methods (see
- \S\ref{sec:induct-method-proper}).
+ 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
--- a/doc-src/IsarRef/intro.tex Wed Jan 02 21:52:54 2002 +0100
+++ b/doc-src/IsarRef/intro.tex Wed Jan 02 21:53:50 2002 +0100
@@ -1,6 +1,55 @@
\chapter{Introduction}
+\section{Overview}
+
+The \emph{Isabelle} system essentially provides a generic infrastructure for
+building deductive systems (programmed in Standard ML), with a special focus
+on interactive theorem proving in higher-order logics. In the olden days even
+end-users would refer to certain ML functions (goal commands, tactics,
+tacticals etc.) to pursue their everyday theorem proving needs
+\cite{isabelle-intro,isabelle-ref}.
+
+In contrast \emph{Isar} provides an interpreted language environment of its
+own, which has been specifically tailored for the needs of theory and proof
+development. Compared to raw ML, the Isabelle/Isar top-level provides a more
+robust and comfortable development platform, with proper support for theory
+development graphs, single-step evaluation with unlimited undo, etc. The
+Isabelle/Isar version of the \emph{Proof~General} user interface
+\cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for
+interactive theory and proof development.
+
+\medskip Apart from these technical advances over bare-bones ML programming,
+the main intention of Isar is to provide a conceptually different view on
+machine-checked proofs \cite{Wenzel:1999:TPHOL, Wenzel-PhD} --- ``Isar''
+stands for ``Intelligible semi-automated reasoning''. Drawing from both the
+traditions of informal mathematical proof texts and high-level programming
+languages, Isar provides a versatile environment for structured formal proof
+documents. Thus properly written Isar proof texts become accessible to a
+broader audience than unstructured tactic scripts (which typically only
+provide operational information for the machine). Writing human-readable
+proof texts certainly requires some additional efforts by the writer in order
+to achieve a good presentation --- both of formal and informal parts of the
+text. On the other hand, human-readable formal texts gain some value in their
+own right, independently of the mechanic proof-checking process.
+
+Despite its grand design of structured proof texts, Isar is able to assimilate
+the old-style tactical as an ``improper'' sub-language. This provides an easy
+upgrade path for existing tactic scripts, as well as additional means for
+experimentation and debugging of interactive proofs. Isabelle/Isar freely
+supports a broad range of proof styles, including unreadable ones.
+
+\medskip The Isabelle/Isar framework generic and should work for reasonably
+well for any object-logic that directly conforms to the view of natural
+deduction according to the Isabelle/Pure framework. Major Isabelle logics
+(HOL \cite{isabelle-HOL}, HOLCF, FOL \cite{isabelle-logics}, ZF
+\cite{isabelle-ZF}) have already been setup for immediate use by end-users.
+
+Note that much of the existing body of theories still consist of old-style
+theory files with accompanied ML code for proof scripts. This legacy will be
+converted as time goes by.
+
+
\section{Quick start}
\subsection{Terminal sessions}
--- a/doc-src/IsarRef/isar-ref.tex Wed Jan 02 21:52:54 2002 +0100
+++ b/doc-src/IsarRef/isar-ref.tex Wed Jan 02 21:53:50 2002 +0100
@@ -67,42 +67,6 @@
\maketitle
-\begin{abstract}
- \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic
- approach to readable formal proof documents. It sets out to bridge the
- semantic gap between any internal notions of proof based on primitive
- inferences and tactics, and an appropriate level of abstraction for
- user-level work. The Isar formal proof language has been designed to
- satisfy quite contradictory requirements, being both ``declarative'' and
- immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter.
-
- The Isabelle/Isar system provides an interpreter for the Isar formal proof
- language. The input may consist either of proper document constructors, or
- improper auxiliary commands (for diagnostics, exploration etc.). Proof
- texts consisting of proper elements only admit a purely static reading, thus
- being intelligible later without requiring dynamic replay that is so typical
- for traditional proof scripts. Any of the Isabelle/Isar commands may be
- executed in single-steps, so basically the interpreter has a proof text
- debugger already built-in.
-
- Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs
- interface for interactive proof assistants, we arrive at a reasonable
- environment for \emph{live document editing}. Thus proof texts may be
- developed incrementally by issuing proof commands, including forward and
- backward tracing of partial documents; intermediate states may be inspected
- by diagnostic commands.
-
- The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
- implementation. Theories, theorems, proof procedures etc.\ may be used
- interchangeably between classic Isabelle proof scripts and Isabelle/Isar
- documents. Even more, Isar provides a set of emulation commands and methods
- for simulating traditional tactic scripts within new-style theory documents.
-
- The Isar framework is as generic as Isabelle, able to support a wide range
- of object-logics. Currently, the end-user working environment is most
- complete for Isabelle/HOL.
-\end{abstract}
-
\pagenumbering{roman} \tableofcontents \clearfirst
%FIXME
@@ -126,6 +90,7 @@
\include{pure}
\include{generic}
\include{hol}
+\include{zf}
\appendix
\include{refcard}
--- a/doc-src/IsarRef/pure.tex Wed Jan 02 21:52:54 2002 +0100
+++ b/doc-src/IsarRef/pure.tex Wed Jan 02 21:53:50 2002 +0100
@@ -1,5 +1,5 @@
-\chapter{Basic Isar Language Elements}\label{ch:pure-syntax}
+\chapter{Basic Language Elements}\label{ch:pure-syntax}
Subsequently, we introduce the main part of Pure Isar theory and proof
commands, together with fundamental proof methods and attributes.
@@ -13,14 +13,14 @@
Isar commands may be either \emph{proper} document constructors, or
\emph{improper commands}. Some proof methods and attributes introduced later
are classified as improper as well. Improper Isar language elements, which
-are subsequently marked by $^*$, are often helpful when developing proof
+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.
-\section{Theory commands}
+\section{Theory specification commands}
\subsection{Defining theories}\label{sec:begin-thy}
@@ -119,16 +119,10 @@
$\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter
and section headings.
\item [$\TEXT$] specifies paragraphs of plain text, including references to
- formal entities.\footnote{The latter feature is not yet supported.
- Nevertheless, any source text of the form
- ``\texttt{\at\ttlbrace$\dots$\ttrbrace}'' should be considered as reserved
- for future use.}
+ formal entities (see also \S\ref{sec:antiq} on ``antiquotations'').
\item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output,
without additional markup. Thus the full range of document manipulations
- becomes available. A typical application would be to emit
- \verb,\begin{comment}, and \verb,\end{comment}, commands to exclude certain
- parts from the final document.\footnote{This requires the \texttt{comment}
- package to be included in {\LaTeX}, of course.}
+ becomes available.
\end{descr}
Any of these markup elements corresponds to a {\LaTeX} command with the name
@@ -305,17 +299,17 @@
\subsection{Axioms and theorems}\label{sec:axms-thms}
-\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}
+\indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems}
\begin{matharray}{rcl}
\isarcmd{axioms} & : & \isartrans{theory}{theory} \\
+ \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
\isarcmd{theorems} & : & \isartrans{theory}{theory} \\
- \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
'axioms' (axmdecl prop comment? +)
;
- ('theorems' | 'lemmas') (thmdef? thmrefs comment? + 'and')
+ ('lemmas' | 'theorems') (thmdef? thmrefs comment? + 'and')
;
\end{rail}
@@ -327,11 +321,11 @@
Axioms are usually only introduced when declaring new logical systems.
Everyday work is typically done the hard way, with proper definitions and
actual proven theorems.
-\item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems.
- Typical applications would also involve attributes, to declare Simplifier
- rules, for example.
-\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
- tags the results as ``lemma''.
+\item [$\isarkeyword{lemmas}~a = \vec b$] stores existing facts. Typical
+ applications would also involve attributes, to declare Simplifier rules, for
+ example.
+\item [$\isarkeyword{theorems}$] is essentially the same as
+ $\isarkeyword{lemmas}$, but marks the result as a different kind of facts.
\end{descr}
@@ -444,7 +438,8 @@
Method.no_args (Method.METHOD (fn facts => foobar_tac))
Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
- Method.thms_ctxt_args (fn thms => fn ctxt => Method.METHOD (fn facts => foobar_tac))
+ Method.thms_ctxt_args (fn thms => fn ctxt =>
+ Method.METHOD (fn facts => foobar_tac))
\end{verbatim}
}
@@ -555,6 +550,7 @@
goal claimed next.
\end{descr}
+%FIXME diagram?
\subsection{Proof markup commands}\label{sec:markup-prf}
@@ -619,19 +615,12 @@
\railterm{equiv}
\begin{rail}
- 'fix' (vars + 'and') comment?
+ 'fix' (vars comment? + 'and')
;
- ('assume' | 'presume') (assm comment? + 'and')
+ ('assume' | 'presume') (props comment? + 'and')
;
'def' thmdecl? \\ name ('==' | equiv) term termpat? comment?
;
-
- var: name ('::' type)?
- ;
- vars: (name+) ('::' type)?
- ;
- assm: thmdecl? (prop proppat? +)
- ;
\end{rail}
\begin{descr}
@@ -715,43 +704,78 @@
\subsection{Goal statements}
-\indexisarcmd{theorem}\indexisarcmd{lemma}
+\indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary}
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
\begin{matharray}{rcl}
+ \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
\isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
- \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
+ \isarcmd{corollary} & : & \isartrans{theory}{proof(prove)} \\
\isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
\isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
\isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
\end{matharray}
-Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
-and $\LEMMANAME$. New local goals may be claimed within proof mode 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 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.
+
+Goals may consist of multiple statements, resulting in a list of facts
+eventually. A pending multi-goal is internally represented as a meta-level
+conjunction (printed as \verb,&&,), which is automatically split into the
+corresponding number of sub-goals prior to any initial method application, via
+$\PROOFNAME$ (\S\ref{sec:proof-steps}) or $\APPLYNAME$
+(\S\ref{sec:tactic-commands}).\footnote{Deviating from the latter principle,
+ the $induct$ method covered in \S\ref{sec:cases-induct-meth} acts on
+ multiple claims simultaneously.}
+
+%FIXME define locale, context
\begin{rail}
- ('theorem' | 'lemma') goal
+ ('lemma' | 'theorem' | 'corollary') locale context goal
;
('have' | 'show' | 'hence' | 'thus') goal
;
- goal: thmdecl? prop proppat? comment?
+ goal: (props comment? + 'and')
;
\end{rail}
\begin{descr}
-\item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
- eventually resulting in some theorem $\turn \phi$ to be put back into the
- theory.
-\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as
- ``lemma''.
-\item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
- theorem with the current assumption context as hypotheses.
-\item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some
- pending goal with the result \emph{exported} into the corresponding context
- (cf.\ \S\ref{sec:proof-context}).
+\item [$\LEMMA{a}{\vec\phi}$] enters proof mode with $\vec\phi$ as main goal,
+ eventually resulting in some fact $\turn \vec\phi$ to be put back into the
+ 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.
+
+\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
+ being of a different kind. This discrimination acts like a formal comment.
+
+\item [$\HAVE{a}{\vec\phi}$] claims a local goal, eventually resulting in a
+ fact within the current logical context. This operation is completely
+ independent of any pending sub-goals of an enclosing goal statements, so
+ $\HAVENAME$ may be freely used for experimental exploration of potential
+ results within a proof body.
+
+\item [$\SHOW{a}{\vec\phi}$] is like $\HAVE{a}{\vec\phi}$ plus a second stage
+ to refine some pending sub-goal for each one of the finished result, after
+ having been exported into the corresponding context (at the head of the
+ sub-proof that the $\SHOWNAME$ command belongs to).
+
+ To accommodate interactive debugging, resulting rules are printed before
+ being applied internally. Even more, interactive execution of $\SHOWNAME$
+ predicts potential failure after finishing its proof, and displays the
+ resulting error message as a warning beforehand, adding this header:
+
+ \begin{ttbox}
+ Problem! Local statement will fail to solve any pending goal
+ \end{ttbox}
+
\item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal
to be proven by forward chaining the current facts. Note that $\HENCENAME$
is also equivalent to $\FROM{this}~\HAVENAME$.
@@ -762,7 +786,8 @@
Any goal statement causes some term abbreviations (such as $\Var{thesis}$,
$\dots$) to be bound automatically, see also \S\ref{sec:term-abbrev}.
Furthermore, the local context of a (non-atomic) goal is provided via the
-$rule_context$\indexisarcase{rule-context} case, see also \S\ref{sec:cases}.
+$rule_context$\indexisarcase{rule-context} case, see also
+\S\ref{sec:rule-cases}.
\medskip
@@ -775,12 +800,11 @@
that most semi-automated methods heavily depend on several kinds of implicit
rule declarations within the current theory context. As this would also
result in non-compositional checking of sub-proofs, \emph{local goals} are
- not allowed to be schematic at all.
-
- Nevertheless, schematic goals do have their use in Prolog-style interactive
- synthesis of proven results, usually by stepwise refinement via emulation of
- traditional Isabelle tactic scripts (see also \S\ref{sec:tactic-commands}).
- In any case, users should know what they are doing!
+ not allowed to be schematic at all. Nevertheless, schematic goals do have
+ their use in Prolog-style interactive synthesis of proven results, usually
+ by stepwise refinement via emulation of traditional Isabelle tactic scripts
+ (see also \S\ref{sec:tactic-commands}). In any case, users should know what
+ they are doing.
\end{warn}
@@ -862,12 +886,15 @@
abbreviates $\BY{rule}$.
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
abbreviates $\BY{this}$.
-\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake}; provided that the
- \texttt{quick_and_dirty} flag is enabled, $\SORRY$ pretends to solve the
- goal without further ado. Of course, the result would be a fake theorem
- only, involving some oracle in its internal derivation object (this is
- indicated as ``$[!]$'' in the printed result). The main application of
- $\SORRY$ is to support experimentation and top-down proof development.
+\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake} pretending to solve
+ the pending claim without further ado. This only works in interactive
+ development, or if the \texttt{quick_and_dirty} flag is enabled. Certainly,
+ any facts emerging from fake proofs are not the real thing. Internally,
+ each theorem container is tainted by an oracle invocation, which is
+ indicated as ``$[!]$'' in the printed result.
+
+ The most important application of $\SORRY$ is to support experimentation and
+ top-down proof development in a simple manner.
\end{descr}
@@ -985,7 +1012,7 @@
\end{rail}
The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
-\railnonterm{proppat} (see \S\ref{sec:term-pats}).
+\railnonterm{proppat} (see \S\ref{sec:term-decls}).
\begin{descr}
\item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$
@@ -1006,25 +1033,6 @@
application of the latter are calculational proofs (see
\S\ref{sec:calculation}).
-%FIXME !?
-
-% A few \emph{automatic} term abbreviations\index{term abbreviations} for goals
-% and facts are available as well. For any open goal,
-% $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
-% (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
-% (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
-% object-level statement. The latter two abstract over any meta-level
-% parameters.
-
-% Fact statements resulting from assumptions or finished goals are bound as
-% $\Var{this_prop}$\indexisarvar{this-prop},
-% $\Var{this_concl}$\indexisarvar{this-concl}, and
-% $\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case
-% $\Var{this}$ refers to an object-logic statement that is an application
-% $f(t)$, then $t$ is bound to the special text variable
-% ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of
-% the latter are calculational proofs (see \S\ref{sec:calculation}).
-
\subsection{Block structure}
@@ -1181,7 +1189,7 @@
macros can be easily adapted to print something like ``$\dots$'' instead of an
``$\OOPS$'' keyword.
-\medskip The $\OOPS$ command is undoable, unlike $\isarkeyword{kill}$ (see
+\medskip The $\OOPS$ command is undo-able, unlike $\isarkeyword{kill}$ (see
\S\ref{sec:history}). The effect is to get back to the theory \emph{before}
the opening of the proof.
@@ -1306,9 +1314,8 @@
theory context containing all of the constants occurring in the terms $\vec
t$. Note that giving the empty list yields \emph{all} theorems of the
current theory.
-\item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of theorems
- and lemmas, using Isabelle's graph browser tool (see also
- \cite{isabelle-sys}).
+\item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts,
+ using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
\item [$\isarkeyword{print_facts}$] prints any named facts of the current
context, including assumptions and local results.
\item [$\isarkeyword{print_binds}$] prints all term abbreviations present in
@@ -1332,7 +1339,7 @@
$\isarkeyword{undo}$ step has crossed the beginning of a proof or theory. The
$\isarkeyword{kill}$ command aborts the current history node altogether,
discontinuing a proof or even the whole theory. This operation is \emph{not}
-undoable.
+undo-able.
\begin{warn}
History commands should never be used with user interfaces such as
--- a/doc-src/IsarRef/syntax.tex Wed Jan 02 21:52:54 2002 +0100
+++ b/doc-src/IsarRef/syntax.tex Wed Jan 02 21:53:50 2002 +0100
@@ -1,52 +1,72 @@
-\chapter{Isar Syntax Primitives}
+\chapter{Syntax primitives}
-We give a complete reference of all basic syntactic entities underlying the
-Isabelle/Isar document syntax. Actual theory and proof commands will be
-introduced later on.
+The rather generic framework of Isabelle/Isar syntax emerges from three main
+syntactic categories: \emph{commands} of the top-level Isar engine (covering
+theory and proof elements), \emph{methods} for general goal refinements
+(analogous to traditional ``tactics''), and \emph{attributes} for operations
+on facts (within a certain context). Here we give a reference of basic
+syntactic entities underlying Isabelle/Isar syntax in a bottom-up manner.
+Concrete theory and proof language elements will be introduced later on.
\medskip
In order to get started with writing well-formed Isabelle/Isar documents, the
most important aspect to be noted is the difference of \emph{inner} versus
\emph{outer} syntax. Inner syntax is that of Isabelle types and terms of the
-logic, while outer syntax is that of Isabelle/Isar theories (including
+logic, while outer syntax is that of Isabelle/Isar theory sources (including
proofs). As a general rule, inner syntax entities may occur only as
\emph{atomic entities} within outer syntax. For example, the string
\texttt{"x + y"} and identifier \texttt{z} are legal term specifications
within a theory, while \texttt{x + y} is not.
\begin{warn}
- Note that classic Isabelle theories used to fake parts of the inner syntax
- of types, with rather complicated rules when quotes may be omitted. Despite
- the minor drawback of requiring quotes more often, the syntax of
- Isabelle/Isar is much simpler and more robust in that respect.
+ Old-style Isabelle theories used to fake parts of the inner syntax of types,
+ with rather complicated rules when quotes may be omitted. Despite the minor
+ drawback of requiring quotes more often, the syntax of Isabelle/Isar is
+ somewhat simpler and more robust in that respect.
\end{warn}
+Printed theory documents usually omit quotes to gain readability (this is a
+matter of {\LaTeX} macro setup, say via \verb,\isabellestyle,, see also
+\cite{isabelle-sys}). Experienced users of Isabelle/Isar may easily
+reconstruct the lost technical information, while mere readers need not care
+about quotes at all.
+
\medskip
Isabelle/Isar input may contain any number of input termination characters
-``\texttt{;}'' (semicolon) to separate commands explicitly. This may be
+``\texttt{;}'' (semicolon) to separate commands explicitly. This is
particularly useful in interactive shell sessions to make clear where the
-current command is intended to end. Otherwise, the interactive loop will
-continue until end-of-command is clearly indicated from the input syntax,
-e.g.\ encounter of the next command keyword.
+current command is intended to end. Otherwise, the interpreter loop will
+continue to issue a secondary prompt ``\verb,#,'' until an end-of-command is
+clearly indicated from the input syntax, e.g.\ encounter of the next command
+keyword.
Advanced interfaces such as Proof~General \cite{proofgeneral} do not require
explicit semicolons, the amount of input text is determined automatically by
-inspecting the Emacs text buffer. Also note that in the presentation of
-Isabelle/Isar documents, semicolons are omitted in any case to gain
+inspecting the present content of the Emacs text buffer. In the printed
+presentation of Isabelle/Isar documents semicolons are omitted altogether for
readability.
+\begin{warn}
+ Proof~General requires certain syntax classification tables in order to
+ achieve properly synchronized interaction with the Isabelle/Isar process.
+ These tables need to be consistent with the Isabelle version and particular
+ logic image to be used in a running session (common object-logics may well
+ change the outer syntax). The standard setup should work correctly with any
+ of the ``official'' logic images derived from Isabelle/HOL (including HOLCF
+ etc.). Users of alternative logics may need to tell Proof~General
+ explicitly, e.g.\ by giving an option \verb,-k ZF, (in conjunction with
+ \verb,-l ZF, to specify the default logic image).
+\end{warn}
\section{Lexical matters}\label{sec:lex-syntax}
The Isabelle/Isar outer syntax provides token classes as presented below.
Note that some of these coincide (by full intention) with the inner lexical
-syntax as presented in \cite{isabelle-ref}. These different levels of syntax
-should not be confused, though.
+syntax as presented in \cite{isabelle-ref}.
-%FIXME keyword, command
\indexoutertoken{ident}\indexoutertoken{longident}\indexoutertoken{symident}
\indexoutertoken{nat}\indexoutertoken{var}\indexoutertoken{typefree}
\indexoutertoken{typevar}\indexoutertoken{string}\indexoutertoken{verbatim}
@@ -69,24 +89,38 @@
\verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \\
& & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
\verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
- symbol & = & {\forall} ~|~ {\exists} ~|~ \dots
+ symbol & = & {\forall} ~|~ {\exists} ~|~ {\land} ~|~ {\lor} ~|~ \dots
\end{matharray}
-The syntax of \texttt{string} admits any characters, including newlines;
-``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) have to be escaped by
-a backslash; newlines need not be escaped. Note that ML-style control
-characters are \emph{not} supported. The body of \texttt{verbatim} may
-consist of any text not containing ``\verb|*}|''.
+The syntax of \railtoken{string} admits any characters, including newlines;
+``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) need to be escaped by
+a backslash. Note that ML-style control characters are \emph{not} supported.
+The body of \railtoken{verbatim} may consist of any text not containing
+``\verb|*}|''; this allows handsome inclusion of quotes without further
+escapes.
-Comments take the form \texttt{(*~\dots~*)} and may be
-nested\footnote{Proof~General may occasionally get confused by nested
- comments.}, just as in ML. Note that these are \emph{source} comments only,
-which are stripped after lexical analysis of the input. The Isar document
-syntax also provides \emph{formal comments} that are actually part of the text
-(see \S\ref{sec:comments}).
+Comments take the form \texttt{(*~\dots~*)} and may in principle be nested,
+just as in ML. Note that these are \emph{source} comments only, which are
+stripped after lexical analysis of the input. The Isar document syntax also
+provides \emph{formal comments} that are actually part of the text (see
+\S\ref{sec:comments}).
+
+\begin{warn}
+ Proof~General does not handle nested comments properly; it is also unable to
+ keep \verb,(*,\,/\,\verb,{*, and \verb,*),\,/\,\verb,*}, apart, despite
+ their rather different meaning. These are inherent problems of Emacs
+ legacy.
+\end{warn}
+
+\medskip
Mathematical symbols such as ``$\forall$'' are represented in plain ASCII as
-``\verb,\<forall>,''.
+``\verb,\<forall>,''. Concerning Isabelle itself, any sequence of the form
+\verb,\<,$ident$\verb,>, (or \verb,\\<,$ident$\verb,>,) is a legal symbol.
+Display of appropriate glyphs is a matter of front-end tools, say the
+user-interface of Proof~General plus the X-Symbol package, or the {\LaTeX}
+macro setup of document output. A list of predefined Isabelle symbols is
+given in \cite[Appendix~A]{isabelle-sys}.
\section{Common syntax entities}
@@ -98,7 +132,7 @@
Note that some of the basic syntactic entities introduced below (e.g.\
\railqtoken{name}) act much like tokens rather than plain nonterminals (e.g.\
\railnonterm{sort}), especially for the sake of error messages. E.g.\ syntax
-elements such as $\CONSTS$ referring to \railqtoken{name} or \railqtoken{type}
+elements like $\CONSTS$ referring to \railqtoken{name} or \railqtoken{type}
would really report a missing name or type rather than any of the constituent
primitive tokens such as \railtoken{ident} or \railtoken{string}.
@@ -131,15 +165,18 @@
Large chunks of plain \railqtoken{text} are usually given
\railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|. For
convenience, any of the smaller text units conforming to \railqtoken{nameref}
-are admitted as well. Almost any of the Isar commands may be annotated by
+are admitted as well. Almost any of the Isar commands may be annotated by a
marginal \railnonterm{comment} of the form \texttt{--} \railqtoken{text}.
Note that the latter kind of comment is actually part of the language, while
source level comments \verb|(*|~\dots~\verb|*)| are stripped at the lexical
-level. A few commands such as $\PROOFNAME$ admit additional markup with a
-``level of interest'': \texttt{\%} followed by an optional number $n$ (default
-$n = 1$) indicates that the respective part of the document becomes $n$ levels
-more obscure; \texttt{\%\%} means that interest drops by $\infty$ --- abandon
-every hope, who enter here.
+level.
+
+A few commands such as $\PROOFNAME$ admit additional markup with a ``level of
+interest'': \texttt{\%} followed by an optional number $n$ (default $n = 1$)
+indicates that the respective part of the document becomes $n$ levels more
+obscure; \texttt{\%\%} means that interest drops by $\infty$ --- abandon every
+hope, who enter here. So far the Isabelle tool-chain (for document output
+etc.) does not yet treat interest levels specifically.
\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
\begin{rail}
@@ -184,9 +221,10 @@
token (the parsing and type-checking is performed internally later). For
convenience, a slightly more liberal convention is adopted: quotes may be
omitted for any type or term that is already \emph{atomic} at the outer level.
-For example, one may write just \texttt{x} instead of \texttt{"x"}. Note that
+For example, one may just write \texttt{x} instead of \texttt{"x"}. Note that
symbolic identifiers (e.g.\ \texttt{++} or $\forall$) are available as well,
-provided these are not superseded by commands or keywords (e.g.\ \texttt{+}).
+provided these have not been superseded by commands or other keywords already
+(e.g.\ \texttt{=} or \texttt{+}).
\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
\begin{rail}
@@ -221,30 +259,13 @@
\end{rail}
-\subsection{Term patterns}\label{sec:term-pats}
-
-Assumptions and goal statements usually admit casual binding of schematic term
-variables by giving (optional) patterns of the form $\ISS{p@1\;\dots}{p@n}$.
-There are separate versions available for \railqtoken{term}s and
-\railqtoken{prop}s. The latter provides a $\CONCLNAME$ part with patterns
-referring the (atomic) conclusion of a rule.
-
-\indexouternonterm{termpat}\indexouternonterm{proppat}
-\begin{rail}
- termpat: '(' ('is' term +) ')'
- ;
- proppat: '(' (('is' prop +) | 'concl' ('is' prop +) | ('is' prop +) 'concl' ('is' prop +)) ')'
- ;
-\end{rail}
-
-
\subsection{Mixfix annotations}
Mixfix annotations specify concrete \emph{inner} syntax of Isabelle types and
-terms (see also \cite{isabelle-ref}). Some commands such as $\TYPES$ (see
-\S\ref{sec:types-pure}) admit infixes only, while $\CONSTS$ (see
-\S\ref{sec:consts}) and $\isarkeyword{syntax}$ (see \S\ref{sec:syn-trans})
-support the full range of general mixfixes and binders.
+terms. Some commands such as $\TYPES$ (see \S\ref{sec:types-pure}) admit
+infixes only, while $\CONSTS$ (see \S\ref{sec:consts}) and
+$\isarkeyword{syntax}$ (see \S\ref{sec:syn-trans}) support the full range of
+general mixfixes and binders.
\indexouternonterm{infix}\indexouternonterm{mixfix}
\begin{rail}
@@ -257,6 +278,46 @@
;
\end{rail}
+Here the \railtoken{string} specifications refer to the actual mixfix template
+(see also \cite{isabelle-ref}), which may include literal text, spacing,
+blocks, and arguments (denoted by ``$_$''); the special symbol \verb,\<index>,
+(printed as ``\i'') represents an index argument that specifies an implicit
+structure reference (see also \S\ref{sec:locale}). Infix and binder
+declarations provide common abbreviations for particular mixfix declarations.
+So in practice, mixfix templates mostly degenerate to literal text for
+concrete syntax, such as ``\verb,++,'' for an infix symbol, or ``\verb,++,\i''
+for an infix of an implicit structure.
+
+
+
+\subsection{Proof methods}\label{sec:syn-meth}
+
+Proof methods are either basic ones, or expressions composed of methods via
+``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
+``\texttt{?}'' (try), ``\texttt{+}'' (repeat at least once). In practice,
+proof methods are usually just a comma separated list of
+\railqtoken{nameref}~\railnonterm{args} specifications. Note that parentheses
+may be dropped for single method specifications (with no arguments).
+
+\indexouternonterm{method}
+\begin{rail}
+ method: (nameref | '(' methods ')') (() | '?' | '+')
+ ;
+ methods: (nameref args | method) + (',' | '|')
+ ;
+\end{rail}
+
+Proper use of Isar proof methods does \emph{not} involve goal addressing.
+Nevertheless, specifying goal ranges may occasionally come in handy in
+emulating tactic scripts. Note that $[n-]$ refers to all goals, starting from
+$n$. All goals may be specified by $[!]$, which is the same as $[1-]$.
+
+\indexouternonterm{goalspec}
+\begin{rail}
+ goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
+ ;
+\end{rail}
+
\subsection{Attributes and theorems}\label{sec:syn-att}
@@ -309,34 +370,45 @@
\end{rail}
-\subsection{Proof methods}\label{sec:syn-meth}
+\subsection{Term patterns and declarations}\label{sec:term-decls}
-Proof methods are either basic ones, or expressions composed of methods via
-``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
-``\texttt{?}'' (try), ``\texttt{+}'' (repeat at least once). In practice,
-proof methods are usually just a comma separated list of
-\railqtoken{nameref}~\railnonterm{args} specifications. Note that parentheses
-may be dropped for single method specifications (with no arguments).
+Wherever explicit propositions (or term fragments) occur in a proof text,
+casual binding of schematic term variables may be given specified via patterns
+of the form $\ISS{p@1\;\dots}{p@n}$. There are separate versions available
+for \railqtoken{term}s and \railqtoken{prop}s. The latter provides a
+$\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule.
-\indexouternonterm{method}
+\indexouternonterm{termpat}\indexouternonterm{proppat}
\begin{rail}
- method: (nameref | '(' methods ')') (() | '?' | '+')
+ termpat: '(' ('is' term +) ')'
;
- methods: (nameref args | method) + (',' | '|')
+ proppat: '(' (('is' prop +) | 'concl' ('is' prop +) | ('is' prop +) 'concl' ('is' prop +)) ')'
;
\end{rail}
-Proper use of Isar proof methods does \emph{not} involve goal addressing.
-Nevertheless, specifying goal ranges may occasionally come in handy in
-emulating tactic scripts. Note that $[n-]$ refers to all goals, starting from
-$n$. All goals may be specified by $[!]$, which is the same as $[1-]$.
+Declarations of local variables $x :: \tau$ and logical propositions $a :
+\phi$ represent different views on the same principle of introducing a local
+scope. In practice, one may usually omit the typing of $vars$ (due to
+type-inference), and the naming of propositions (due to implicit chaining of
+emerging facts). In any case, Isar proof elements usually admit to introduce
+multiple such items simultaneously.
-\indexouternonterm{goalspec}
+\indexouternonterm{vars}\indexouternonterm{props}
\begin{rail}
- goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
+ vars: (name+) ('::' type)?
+ ;
+ props: thmdecl? (prop proppat? +)
;
\end{rail}
+The treatment of multiple declarations corresponds to the complementary focus
+of $vars$ versus $props$: in ``$x@1~\dots~x@n :: \tau$'' the typing refers to
+all variables, while in $a\colon \phi@1~\dots~\phi@n$ the naming refers to all
+propositions collectively. Isar language elements that refer to $vars$ or
+$props$ typically admit separate typings or namings via another level of
+iteration, with explicit $\AND$ separators; e.g.\ see $\FIXNAME$ and
+$\ASSUMENAME$ in \S\ref{sec:proof-context}.
+
\subsection{Antiquotations}\label{sec:antiq}
@@ -363,7 +435,7 @@
antiquotations may involve attributes as well. For example,
\texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print the
statement where all schematic variables have been replaced by fixed ones,
-which are better readable.
+which are easier to read.
\indexisarant{thm}\indexisarant{prop}\indexisarant{term}
\indexisarant{typ}\indexisarant{text}\indexisarant{goals}\indexisarant{subgoals}
@@ -392,7 +464,7 @@
\begin{descr}
\item [$\at\{thm~\vec a\}$] prints theorems $\vec a$. Note that attribute
specifications may be included as well (see also \S\ref{sec:syn-att}); the
- $no_vars$ operation (see \S\ref{sec:misc-methods}) would be particularly
+ $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly
useful to suppress printing of schematic variables.
\item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$.
\item [$\at\{term~t\}$] prints a well-typed term $t$.