removed parts of the manual that are clearly obsolete, or covered by
newer manuals already (notably "isar-ref" or "implementation");
--- a/doc-src/Ref/Makefile Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/Makefile Sun Mar 01 13:48:17 2009 +0100
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
@@ -12,16 +9,15 @@
include ../Makefile.in
NAME = ref
-FILES = ref.tex introduction.tex goals.tex tactic.tex tctical.tex \
- thm.tex theories.tex defining.tex syntax.tex substitution.tex \
- simplifier.tex classical.tex theory-syntax.tex \
- ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
+FILES = ref.tex introduction.tex tactic.tex tctical.tex thm.tex \
+ theories.tex defining.tex syntax.tex substitution.tex \
+ simplifier.tex classical.tex ../proof.sty ../iman.sty \
+ ../extra.sty ../ttbox.sty ../manual.bib
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES) isabelle.eps
$(LATEX) $(NAME)
- $(RAIL) $(NAME)
$(BIBTEX) $(NAME)
$(LATEX) $(NAME)
$(LATEX) $(NAME)
@@ -32,7 +28,6 @@
$(NAME).pdf: $(FILES) isabelle.pdf
$(PDFLATEX) $(NAME)
- $(RAIL) $(NAME)
$(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
$(PDFLATEX) $(NAME)
--- a/doc-src/Ref/classical.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/classical.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,4 +1,4 @@
-%% $Id$
+
\chapter{The Classical Reasoner}\label{chap:classical}
\index{classical reasoner|(}
\newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
@@ -28,29 +28,6 @@
be traced, and their components can be called directly; in this manner,
any proof can be viewed interactively.
-The simplest way to apply the classical reasoner (to subgoal~$i$) is to type
-\begin{ttbox}
-by (Blast_tac \(i\));
-\end{ttbox}
-This command quickly proves most simple formulas of the predicate calculus or
-set theory. To attempt to prove subgoals using a combination of
-rewriting and classical reasoning, try
-\begin{ttbox}
-auto(); \emph{\textrm{applies to all subgoals}}
-force i; \emph{\textrm{applies to one subgoal}}
-\end{ttbox}
-To do all obvious logical steps, even if they do not prove the
-subgoal, type one of the following:
-\begin{ttbox}
-by Safe_tac; \emph{\textrm{applies to all subgoals}}
-by (Clarify_tac \(i\)); \emph{\textrm{applies to one subgoal}}
-\end{ttbox}
-
-
-You need to know how the classical reasoner works in order to use it
-effectively. There are many tactics to choose from, including
-{\tt Fast_tac} and \texttt{Best_tac}.
-
We shall first discuss the underlying principles, then present the classical
reasoner. Finally, we shall see how to instantiate it for new logics. The
logics FOL, ZF, HOL and HOLCF have it already installed.
--- a/doc-src/Ref/defining.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/defining.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,376 +1,5 @@
-%% $Id$
+
\chapter{Defining Logics} \label{Defining-Logics}
-This chapter explains how to define new formal systems --- in particular,
-their concrete syntax. While Isabelle can be regarded as a theorem prover
-for set theory, higher-order logic or the sequent calculus, its
-distinguishing feature is support for the definition of new logics.
-
-Isabelle logics are hierarchies of theories, which are described and
-illustrated in
-\iflabelundefined{sec:defining-theories}{{\em Introduction to Isabelle}}%
-{\S\ref{sec:defining-theories}}. That material, together with the theory
-files provided in the examples directories, should suffice for all simple
-applications. The easiest way to define a new theory is by modifying a
-copy of an existing theory.
-
-This chapter documents the meta-logic syntax, mixfix declarations and
-pretty printing. The extended examples in \S\ref{sec:min_logics}
-demonstrate the logical aspects of the definition of theories.
-
-
-\section{Priority grammars} \label{sec:priority_grammars}
-\index{priority grammars|(}
-
-A context-free grammar contains a set of {\bf nonterminal symbols}, a set of
-{\bf terminal symbols} and a set of {\bf productions}\index{productions}.
-Productions have the form ${A=\gamma}$, where $A$ is a nonterminal and
-$\gamma$ is a string of terminals and nonterminals. One designated
-nonterminal is called the {\bf start symbol}. The language defined by the
-grammar consists of all strings of terminals that can be derived from the
-start symbol by applying productions as rewrite rules.
-
-The syntax of an Isabelle logic is specified by a {\bf priority
- grammar}.\index{priorities} Each nonterminal is decorated by an integer
-priority, as in~$A^{(p)}$. A nonterminal $A^{(p)}$ in a derivation may be
-rewritten using a production $A^{(q)} = \gamma$ only if~$p \leq q$. Any
-priority grammar can be translated into a normal context free grammar by
-introducing new nonterminals and productions.
-
-Formally, a set of context free productions $G$ induces a derivation
-relation $\longrightarrow@G$. Let $\alpha$ and $\beta$ denote strings of
-terminal or nonterminal symbols. Then
-\[ \alpha\, A^{(p)}\, \beta ~\longrightarrow@G~ \alpha\,\gamma\,\beta \]
-if and only if $G$ contains some production $A^{(q)}=\gamma$ for~$p \leq q$.
-
-The following simple grammar for arithmetic expressions demonstrates how
-binding power and associativity of operators can be enforced by priorities.
-\begin{center}
-\begin{tabular}{rclr}
- $A^{(9)}$ & = & {\tt0} \\
- $A^{(9)}$ & = & {\tt(} $A^{(0)}$ {\tt)} \\
- $A^{(0)}$ & = & $A^{(0)}$ {\tt+} $A^{(1)}$ \\
- $A^{(2)}$ & = & $A^{(3)}$ {\tt*} $A^{(2)}$ \\
- $A^{(3)}$ & = & {\tt-} $A^{(3)}$
-\end{tabular}
-\end{center}
-The choice of priorities determines that {\tt -} binds tighter than {\tt *},
-which binds tighter than {\tt +}. Furthermore {\tt +} associates to the
-left and {\tt *} to the right.
-
-For clarity, grammars obey these conventions:
-\begin{itemize}
-\item All priorities must lie between~0 and \ttindex{max_pri}, which is a
- some fixed integer. Sometimes {\tt max_pri} is written as $\infty$.
-\item Priority 0 on the right-hand side and priority \ttindex{max_pri} on
- the left-hand side may be omitted.
-\item The production $A^{(p)} = \alpha$ is written as $A = \alpha~(p)$; the
- priority of the left-hand side actually appears in a column on the far
- right.
-\item Alternatives are separated by~$|$.
-\item Repetition is indicated by dots~(\dots) in an informal but obvious
- way.
-\end{itemize}
-
-Using these conventions and assuming $\infty=9$, the grammar
-takes the form
-\begin{center}
-\begin{tabular}{rclc}
-$A$ & = & {\tt0} & \hspace*{4em} \\
- & $|$ & {\tt(} $A$ {\tt)} \\
- & $|$ & $A$ {\tt+} $A^{(1)}$ & (0) \\
- & $|$ & $A^{(3)}$ {\tt*} $A^{(2)}$ & (2) \\
- & $|$ & {\tt-} $A^{(3)}$ & (3)
-\end{tabular}
-\end{center}
-\index{priority grammars|)}
-
-
-\begin{figure}\small
-\begin{center}
-\begin{tabular}{rclc}
-$any$ &=& $prop$ ~~$|$~~ $logic$ \\\\
-$prop$ &=& {\tt(} $prop$ {\tt)} \\
- &$|$& $prop^{(4)}$ {\tt::} $type$ & (3) \\
- &$|$& {\tt PROP} $aprop$ \\
- &$|$& $any^{(3)}$ {\tt ==} $any^{(2)}$ & (2) \\
- &$|$& $any^{(3)}$ {\tt =?=} $any^{(2)}$ & (2) \\
- &$|$& $prop^{(2)}$ {\tt ==>} $prop^{(1)}$ & (1) \\
- &$|$& {\tt[|} $prop$ {\tt;} \dots {\tt;} $prop$ {\tt|]} {\tt==>} $prop^{(1)}$ & (1) \\
- &$|$& {\tt!!} $idts$ {\tt.} $prop$ & (0) \\
- &$|$& {\tt OFCLASS} {\tt(} $type$ {\tt,} $logic$ {\tt)} \\\\
-$aprop$ &=& $id$ ~~$|$~~ $longid$ ~~$|$~~ $var$
- ~~$|$~~ $logic^{(\infty)}$ {\tt(} $any$ {\tt,} \dots {\tt,} $any$ {\tt)} \\\\
-$logic$ &=& {\tt(} $logic$ {\tt)} \\
- &$|$& $logic^{(4)}$ {\tt::} $type$ & (3) \\
- &$|$& $id$ ~~$|$~~ $longid$ ~~$|$~~ $var$
- ~~$|$~~ $logic^{(\infty)}$ {\tt(} $any$ {\tt,} \dots {\tt,} $any$ {\tt)} \\
- &$|$& {\tt \%} $pttrns$ {\tt.} $any^{(3)}$ & (3) \\
- &$|$& {\tt TYPE} {\tt(} $type$ {\tt)} \\\\
-$idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
-$idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
- &$|$& $id$ {\tt ::} $type$ & (0) \\\\
-$pttrns$ &=& $pttrn$ ~~$|$~~ $pttrn^{(1)}$ $pttrns$ \\\\
-$pttrn$ &=& $idt$ \\\\
-$type$ &=& {\tt(} $type$ {\tt)} \\
- &$|$& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$
- ~~$|$~~ $tvar$ {\tt::} $sort$ \\
- &$|$& $id$ ~~$|$~~ $type^{(\infty)}$ $id$
- ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\
- &$|$& $longid$ ~~$|$~~ $type^{(\infty)}$ $longid$
- ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $longid$ \\
- &$|$& $type^{(1)}$ {\tt =>} $type$ & (0) \\
- &$|$& {\tt[} $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0) \\\\
-$sort$ &=& $id$ ~~$|$~~ $longid$ ~~$|$~~ {\tt\ttlbrace\ttrbrace} ~~$|$~~
- {\tt\ttlbrace} $id$ ~$|$~ $longid${\tt,}\dots{\tt,} $id$ ~$|$~$longid$ {\tt\ttrbrace}
-\end{tabular}
-\index{*PROP symbol}
-\index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
-\index{*:: symbol}\index{*=> symbol}
-\index{sort constraints}
-%the index command: a percent is permitted, but braces must match!
-\index{%@{\tt\%} symbol}
-\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
-\index{*[ symbol}\index{*] symbol}
-\index{*"!"! symbol}
-\index{*"["| symbol}
-\index{*"|"] symbol}
-\end{center}
-\caption{Meta-logic syntax}\label{fig:pure_gram}
-\end{figure}
-
-
-\section{The Pure syntax} \label{sec:basic_syntax}
-\index{syntax!Pure|(}
-
-At the root of all object-logics lies the theory \thydx{Pure}. It
-contains, among many other things, the Pure syntax. An informal account of
-this basic syntax (types, terms and formulae) appears in
-\iflabelundefined{sec:forward}{{\em Introduction to Isabelle}}%
-{\S\ref{sec:forward}}. A more precise description using a priority grammar
-appears in Fig.\ts\ref{fig:pure_gram}. It defines the following
-nonterminals:
-\begin{ttdescription}
- \item[\ndxbold{any}] denotes any term.
-
- \item[\ndxbold{prop}] denotes terms of type {\tt prop}. These are formulae
- of the meta-logic. Note that user constants of result type {\tt prop}
- (i.e.\ $c :: \ldots \To prop$) should always provide concrete syntax.
- Otherwise atomic propositions with head $c$ may be printed incorrectly.
-
- \item[\ndxbold{aprop}] denotes atomic propositions.
-
-%% FIXME huh!?
-% These typically
-% include the judgement forms of the object-logic; its definition
-% introduces a meta-level predicate for each judgement form.
-
- \item[\ndxbold{logic}] denotes terms whose type belongs to class
- \cldx{logic}, excluding type \tydx{prop}.
-
- \item[\ndxbold{idts}] denotes a list of identifiers, possibly constrained
- by types.
-
- \item[\ndxbold{pttrn}, \ndxbold{pttrns}] denote patterns for
- abstraction, cases etc. Initially the same as $idt$ and $idts$,
- these are intended to be augmented by user extensions.
-
- \item[\ndxbold{type}] denotes types of the meta-logic.
-
- \item[\ndxbold{sort}] denotes meta-level sorts.
-\end{ttdescription}
-
-\begin{warn}
- In {\tt idts}, note that \verb|x::nat y| is parsed as \verb|x::(nat y)|,
- treating {\tt y} like a type constructor applied to {\tt nat}. The
- likely result is an error message. To avoid this interpretation, use
- parentheses and write \verb|(x::nat) y|.
- \index{type constraints}\index{*:: symbol}
-
- Similarly, \verb|x::nat y::nat| is parsed as \verb|x::(nat y::nat)| and
- yields an error. The correct form is \verb|(x::nat) (y::nat)|.
-\end{warn}
-
-\begin{warn}
- Type constraints bind very weakly. For example, \verb!x<y::nat! is normally
- parsed as \verb!(x<y)::nat!, unless \verb$<$ has priority of 3 or less, in
- which case the string is likely to be ambiguous. The correct form is
- \verb!x<(y::nat)!.
-\end{warn}
-
-\subsection{Logical types and default syntax}\label{logical-types}
-\index{lambda calc@$\lambda$-calculus}
-
-Isabelle's representation of mathematical languages is based on the
-simply typed $\lambda$-calculus. All logical types, namely those of
-class \cldx{logic}, are automatically equipped with a basic syntax of
-types, identifiers, variables, parentheses, $\lambda$-abstraction and
-application.
-\begin{warn}
- Isabelle combines the syntaxes for all types of class \cldx{logic} by
- mapping all those types to the single nonterminal $logic$. Thus all
- productions of $logic$, in particular $id$, $var$ etc, become available.
-\end{warn}
-
-
-\subsection{Lexical matters}
-The parser does not process input strings directly. It operates on token
-lists provided by Isabelle's \bfindex{lexer}. There are two kinds of
-tokens: \bfindex{delimiters} and \bfindex{name tokens}.
-
-\index{reserved words}
-Delimiters can be regarded as reserved words of the syntax. You can
-add new ones when extending theories. In Fig.\ts\ref{fig:pure_gram} they
-appear in typewriter font, for example {\tt ==}, {\tt =?=} and
-{\tt PROP}\@.
-
-Name tokens have a predefined syntax. The lexer distinguishes six disjoint
-classes of names: \rmindex{identifiers}, \rmindex{unknowns}, type
-identifiers\index{type identifiers}, type unknowns\index{type unknowns},
-\rmindex{numerals}, \rmindex{strings}. They are denoted by \ndxbold{id},
-\ndxbold{var}, \ndxbold{tid}, \ndxbold{tvar}, \ndxbold{num}, \ndxbold{xnum},
-\ndxbold{xstr}, respectively. Typical examples are {\tt x}, {\tt ?x7}, {\tt
- 'a}, {\tt ?'a3}, {\tt \#42}, {\tt ''foo bar''}. Here is the precise syntax:
-\begin{eqnarray*}
-id & = & letter\,quasiletter^* \\
-longid & = & id (\mbox{\tt .}id)^+ \\
-var & = & \mbox{\tt ?}id ~~|~~ \mbox{\tt ?}id\mbox{\tt .}nat \\
-tid & = & \mbox{\tt '}id \\
-tvar & = & \mbox{\tt ?}tid ~~|~~
- \mbox{\tt ?}tid\mbox{\tt .}nat \\
-num & = & nat ~~|~~ \mbox{\tt-}nat ~~|~~ \verb,0x,\,hex^+ ~~|~~ \verb,0b,\,bin^+ \\
-xnum & = & \mbox{\tt \#}num \\
-xstr & = & \mbox{\tt ''~\dots~\tt ''} \\[1ex]
-letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek ~| \\
- & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
-quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
-latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
-digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
-nat & = & digit^+ \\
-bin & = & \verb,0, ~|~ \verb,1, \\
-hex & = & digit ~|~ \verb,a, ~|~ \dots ~|~ \verb,f, ~|~ \verb,A, ~|~ \dots ~|~ \verb,F, \\
-greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
- & & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
- & & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
- & & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~| \\
- & & \verb,\<tau>, ~|~ \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<psi>, ~| \\
- & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
- & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
- & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
-\end{eqnarray*}
-The lexer repeatedly takes the longest prefix of the input string that
-forms a valid token. A maximal prefix that is both a delimiter and a
-name is treated as a delimiter. Spaces, tabs, newlines and formfeeds
-are separators; they never occur within tokens, except those of class
-$xstr$.
-
-\medskip
-Delimiters need not be separated by white space. For example, if {\tt -}
-is a delimiter but {\tt --} is not, then the string {\tt --} is treated as
-two consecutive occurrences of the token~{\tt -}. In contrast, \ML\
-treats {\tt --} as a single symbolic name. The consequence of Isabelle's
-more liberal scheme is that the same string may be parsed in different ways
-after extending the syntax: after adding {\tt --} as a delimiter, the input
-{\tt --} is treated as a single token.
-
-A \ndxbold{var} or \ndxbold{tvar} describes an unknown, which is internally
-a pair of base name and index (\ML\ type \mltydx{indexname}). These
-components are either separated by a dot as in {\tt ?x.1} or {\tt ?x7.3} or
-run together as in {\tt ?x1}. The latter form is possible if the base name
-does not end with digits. If the index is 0, it may be dropped altogether:
-{\tt ?x} abbreviates both {\tt ?x0} and {\tt ?x.0}.
-
-Tokens of class $num$, $xnum$ or $xstr$ are not used by the meta-logic.
-Object-logics may provide numerals and string constants by adding appropriate
-productions and translation functions.
-
-\medskip
-Although name tokens are returned from the lexer rather than the parser, it
-is more logical to regard them as nonterminals. Delimiters, however, are
-terminals; they are just syntactic sugar and contribute nothing to the
-abstract syntax tree.
-
-
-\subsection{*Inspecting the syntax} \label{pg:print_syn}
-\begin{ttbox}
-syn_of : theory -> Syntax.syntax
-print_syntax : theory -> unit
-Syntax.print_syntax : Syntax.syntax -> unit
-Syntax.print_gram : Syntax.syntax -> unit
-Syntax.print_trans : Syntax.syntax -> unit
-\end{ttbox}
-The abstract type \mltydx{Syntax.syntax} allows manipulation of syntaxes
-in \ML. You can display values of this type by calling the following
-functions:
-\begin{ttdescription}
-\item[\ttindexbold{syn_of} {\it thy}] returns the syntax of the Isabelle
- theory~{\it thy} as an \ML\ value.
-
-\item[\ttindexbold{print_syntax} $thy$] uses {\tt Syntax.print_syntax}
- to display the syntax part of theory $thy$.
-
-\item[\ttindexbold{Syntax.print_syntax} {\it syn}] shows virtually all
- information contained in the syntax {\it syn}. The displayed output can
- be large. The following two functions are more selective.
-
-\item[\ttindexbold{Syntax.print_gram} {\it syn}] shows the grammar part
- of~{\it syn}, namely the lexicon, logical types and productions. These are
- discussed below.
-
-\item[\ttindexbold{Syntax.print_trans} {\it syn}] shows the translation
- part of~{\it syn}, namely the constants, parse/print macros and
- parse/print translations.
-\end{ttdescription}
-
-The output of the above print functions is divided into labelled sections.
-The grammar is represented by {\tt lexicon}, {\tt logtypes} and {\tt prods}.
-The rest refers to syntactic translations and macro expansion. Here is an
-explanation of the various sections.
-\begin{description}
- \item[{\tt lexicon}] lists the delimiters used for lexical
- analysis.\index{delimiters}
-
- \item[{\tt logtypes}] lists the types that are regarded the same as {\tt
- logic} syntactically. Thus types of object-logics (e.g.\ {\tt nat}, say)
- will be automatically equipped with the standard syntax of
- $\lambda$-calculus.
-
- \item[{\tt prods}] lists the \rmindex{productions} of the priority grammar.
- The nonterminal $A^{(n)}$ is rendered in {\sc ascii} as {\tt $A$[$n$]}.
- Each delimiter is quoted. Some productions are shown with {\tt =>} and
- an attached string. These strings later become the heads of parse
- trees; they also play a vital role when terms are printed (see
- \S\ref{sec:asts}).
-
- Productions with no strings attached are called {\bf copy
- productions}\indexbold{productions!copy}. Their right-hand side must
- have exactly one nonterminal symbol (or name token). The parser does
- not create a new parse tree node for copy productions, but simply
- returns the parse tree of the right-hand symbol.
-
- If the right-hand side consists of a single nonterminal with no
- delimiters, then the copy production is called a {\bf chain
- production}. Chain productions act as abbreviations:
- conceptually, they are removed from the grammar by adding new
- productions. Priority information attached to chain productions is
- ignored; only the dummy value $-1$ is displayed.
-
- \item[\ttindex{print_modes}] lists the alternative print modes
- provided by this syntax (see \S\ref{sec:prmodes}).
-
- \item[{\tt consts}, {\tt parse_rules}, {\tt print_rules}]
- relate to macros (see \S\ref{sec:macros}).
-
- \item[{\tt parse_ast_translation}, {\tt print_ast_translation}]
- list sets of constants that invoke translation functions for abstract
- syntax trees. Section \S\ref{sec:asts} below discusses this obscure
- matter.\index{constants!for translations}
-
- \item[{\tt parse_translation}, {\tt print_translation}] list the sets
- of constants that invoke translation functions for terms (see
- \S\ref{sec:tr_funs}).
-\end{description}
-\index{syntax!Pure|)}
-
\section{Mixfix declarations} \label{sec:mixfix}
\index{mixfix declarations|(}
@@ -515,49 +144,6 @@
syntax}. Try this as an exercise and study the changes in the
grammar.
-\subsection{The mixfix template}
-Let us now take a closer look at the string $template$ appearing in mixfix
-annotations. This string specifies a list of parsing and printing
-directives: delimiters\index{delimiters}, arguments, spaces, blocks of
-indentation and line breaks. These are encoded by the following character
-sequences:
-\index{pretty printing|(}
-\begin{description}
-\item[~$d$~] is a delimiter, namely a non-empty sequence of characters
- other than the special characters {\tt _}, {\tt(}, {\tt)} and~{\tt/}.
- Even these characters may appear if escaped; this means preceding it with
- a~{\tt '} (single quote). Thus you have to write {\tt ''} if you really
- want a single quote. Furthermore, a~{\tt '} followed by a space separates
- delimiters without extra white space being added for printing.
-
-\item[~{\tt_}~] is an argument position, which stands for a nonterminal symbol
- or name token.
-
-\item[~$s$~] is a non-empty sequence of spaces for printing. This and the
- following specifications do not affect parsing at all.
-
-\item[~{\tt(}$n$~] opens a pretty printing block. The optional number $n$
- specifies how much indentation to add when a line break occurs within the
- block. If {\tt(} is not followed by digits, the indentation defaults
- to~0.
-
-\item[~{\tt)}~] closes a pretty printing block.
-
-\item[~{\tt//}~] forces a line break.
-
-\item[~{\tt/}$s$~] allows a line break. Here $s$ stands for the string of
- spaces (zero or more) right after the {\tt /} character. These spaces
- are printed if the break is not taken.
-\end{description}
-For example, the template {\tt"(_ +/ _)"} specifies an infix operator.
-There are two argument positions; the delimiter~{\tt+} is preceded by a
-space and followed by a space or line break; the entire phrase is a pretty
-printing block. Other examples appear in Fig.\ts\ref{fig:set_trans} below.
-Isabelle's pretty printer resembles the one described in
-Paulson~\cite{paulson-ml2}.
-
-\index{pretty printing|)}
-
\subsection{Infixes}
\indexbold{infixes}
@@ -723,141 +309,6 @@
ambiguity should be eliminated by changing the grammar or the rule.
-\section{Example: some minimal logics} \label{sec:min_logics}
-\index{examples!of logic definitions}
-
-This section presents some examples that have a simple syntax. They
-demonstrate how to define new object-logics from scratch.
-
-First we must define how an object-logic syntax is embedded into the
-meta-logic. Since all theorems must conform to the syntax for~\ndx{prop}
-(see Fig.\ts\ref{fig:pure_gram}), that syntax has to be extended with the
-object-level syntax. Assume that the syntax of your object-logic defines a
-meta-type~\tydx{o} of formulae which refers to the nonterminal {\tt logic}.
-These formulae can now appear in axioms and theorems wherever \ndx{prop} does
-if you add the production
-\[ prop ~=~ logic. \]
-This is not supposed to be a copy production but an implicit coercion from
-formulae to propositions:
-\begin{ttbox}
-Base = Pure +
-types
- o
-arities
- o :: logic
-consts
- Trueprop :: o => prop ("_" 5)
-end
-\end{ttbox}
-The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible
-coercion function. Assuming this definition resides in a file {\tt Base.thy},
-you have to load it with the command {\tt use_thy "Base"}.
-
-One of the simplest nontrivial logics is {\bf minimal logic} of
-implication. Its definition in Isabelle needs no advanced features but
-illustrates the overall mechanism nicely:
-\begin{ttbox}
-Hilbert = Base +
-consts
- "-->" :: [o, o] => o (infixr 10)
-rules
- K "P --> Q --> P"
- S "(P --> Q --> R) --> (P --> Q) --> P --> R"
- MP "[| P --> Q; P |] ==> Q"
-end
-\end{ttbox}
-After loading this definition from the file {\tt Hilbert.thy}, you can
-start to prove theorems in the logic:
-\begin{ttbox}
-Goal "P --> P";
-{\out Level 0}
-{\out P --> P}
-{\out 1. P --> P}
-\ttbreak
-by (resolve_tac [Hilbert.MP] 1);
-{\out Level 1}
-{\out P --> P}
-{\out 1. ?P --> P --> P}
-{\out 2. ?P}
-\ttbreak
-by (resolve_tac [Hilbert.MP] 1);
-{\out Level 2}
-{\out P --> P}
-{\out 1. ?P1 --> ?P --> P --> P}
-{\out 2. ?P1}
-{\out 3. ?P}
-\ttbreak
-by (resolve_tac [Hilbert.S] 1);
-{\out Level 3}
-{\out P --> P}
-{\out 1. P --> ?Q2 --> P}
-{\out 2. P --> ?Q2}
-\ttbreak
-by (resolve_tac [Hilbert.K] 1);
-{\out Level 4}
-{\out P --> P}
-{\out 1. P --> ?Q2}
-\ttbreak
-by (resolve_tac [Hilbert.K] 1);
-{\out Level 5}
-{\out P --> P}
-{\out No subgoals!}
-\end{ttbox}
-As we can see, this Hilbert-style formulation of minimal logic is easy to
-define but difficult to use. The following natural deduction formulation is
-better:
-\begin{ttbox}
-MinI = Base +
-consts
- "-->" :: [o, o] => o (infixr 10)
-rules
- impI "(P ==> Q) ==> P --> Q"
- impE "[| P --> Q; P |] ==> Q"
-end
-\end{ttbox}
-Note, however, that although the two systems are equivalent, this fact
-cannot be proved within Isabelle. Axioms {\tt S} and {\tt K} can be
-derived in {\tt MinI} (exercise!), but {\tt impI} cannot be derived in {\tt
- Hilbert}. The reason is that {\tt impI} is only an {\bf admissible} rule
-in {\tt Hilbert}, something that can only be shown by induction over all
-possible proofs in {\tt Hilbert}.
-
-We may easily extend minimal logic with falsity:
-\begin{ttbox}
-MinIF = MinI +
-consts
- False :: o
-rules
- FalseE "False ==> P"
-end
-\end{ttbox}
-On the other hand, we may wish to introduce conjunction only:
-\begin{ttbox}
-MinC = Base +
-consts
- "&" :: [o, o] => o (infixr 30)
-\ttbreak
-rules
- conjI "[| P; Q |] ==> P & Q"
- conjE1 "P & Q ==> P"
- conjE2 "P & Q ==> Q"
-end
-\end{ttbox}
-And if we want to have all three connectives together, we create and load a
-theory file consisting of a single line:
-\begin{ttbox}
-MinIFC = MinIF + MinC
-\end{ttbox}
-Now we can prove mixed theorems like
-\begin{ttbox}
-Goal "P & False --> Q";
-by (resolve_tac [MinI.impI] 1);
-by (dresolve_tac [MinC.conjE2] 1);
-by (eresolve_tac [MinIF.FalseE] 1);
-\end{ttbox}
-Try this as an exercise!
-
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"
--- a/doc-src/Ref/goals.tex Sun Mar 01 12:37:59 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,722 +0,0 @@
-%% $Id$
-\chapter{Proof Management: The Subgoal Module}
-\index{proofs|(}
-\index{subgoal module|(}
-\index{reading!goals|see{proofs, starting}}
-
-The subgoal module stores the current proof state\index{proof state} and
-many previous states; commands can produce new states or return to previous
-ones. The {\em state list\/} at level $n$ is a list of pairs
-\[ [(\psi@n,\Psi@n),\; (\psi@{n-1},\Psi@{n-1}),\; \ldots,\; (\psi@0,[])] \]
-where $\psi@n$ is the current proof state, $\psi@{n-1}$ is the previous
-one, \ldots, and $\psi@0$ is the initial proof state. The $\Psi@i$ are
-sequences (lazy lists) of proof states, storing branch points where a
-tactic returned a list longer than one. The state lists permit various
-forms of backtracking.
-
-Chopping elements from the state list reverts to previous proof states.
-Besides this, the \ttindex{undo} command keeps a list of state lists. The
-module actually maintains a stack of state lists, to support several
-proofs at the same time.
-
-The subgoal module always contains some proof state. At the start of the
-Isabelle session, this state consists of a dummy formula.
-
-
-\section{Basic commands}
-Most proofs begin with \texttt{Goal} or \texttt{Goalw} and require no other
-commands than \texttt{by}, \texttt{chop} and \texttt{undo}. They typically end
-with a call to \texttt{qed}.
-\subsection{Starting a backward proof}
-\index{proofs!starting}
-\begin{ttbox}
-Goal : string -> thm list
-Goalw : thm list -> string -> thm list
-goal : theory -> string -> thm list
-goalw : theory -> thm list -> string -> thm list
-goalw_cterm : thm list -> cterm -> thm list
-premises : unit -> thm list
-\end{ttbox}
-
-The goal commands start a new proof by setting the goal. They replace
-the current state list by a new one consisting of the initial proof
-state. They also empty the \ttindex{undo} list; this command cannot
-be undone!
-
-They all return a list of meta-hypotheses taken from the main goal. If
-this list is non-empty, bind its value to an \ML{} identifier by typing
-something like
-\begin{ttbox}
-val prems = goal{\it theory\/ formula};
-\end{ttbox}\index{assumptions!of main goal}
-These assumptions typically serve as the premises when you are
-deriving a rule. They are also stored internally and can be retrieved
-later by the function \texttt{premises}. When the proof is finished,
-\texttt{qed} compares the stored assumptions with the actual
-assumptions in the proof state.
-
-The capital versions of \texttt{Goal} are the basic user level
-commands and should be preferred over the more primitive lowercase
-\texttt{goal} commands. Apart from taking the current theory context
-as implicit argument, the former ones try to be smart in handling
-meta-hypotheses when deriving rules. Thus \texttt{prems} have to be
-seldom bound explicitly, the effect is as if \texttt{cut_facts_tac}
-had been called automatically.
-
-\index{definitions!unfolding}
-Some of the commands unfold definitions using meta-rewrite rules. This
-expansion affects both the initial subgoal and the premises, which would
-otherwise require use of \texttt{rewrite_goals_tac} and
-\texttt{rewrite_rule}.
-
-\begin{ttdescription}
-\item[\ttindexbold{Goal} {\it formula};] begins a new proof, where
- {\it formula\/} is written as an \ML\ string.
-
-\item[\ttindexbold{Goalw} {\it defs} {\it formula};] is like
- \texttt{Goal} but also applies the list of {\it defs\/} as
- meta-rewrite rules to the first subgoal and the premises.
- \index{meta-rewriting}
-
-\item[\ttindexbold{goal} {\it theory} {\it formula};]
-begins a new proof, where {\it theory} is usually an \ML\ identifier
-and the {\it formula\/} is written as an \ML\ string.
-
-\item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula};]
-is like \texttt{goal} but also applies the list of {\it defs\/} as
-meta-rewrite rules to the first subgoal and the premises.
-\index{meta-rewriting}
-
-\item[\ttindexbold{goalw_cterm} {\it defs} {\it ct};] is
- a version of \texttt{goalw} intended for programming. The main
- goal is supplied as a cterm, not as a string. See also
- \texttt{prove_goalw_cterm}, \S\ref{sec:executing-batch}.
-
-\item[\ttindexbold{premises}()]
-returns the list of meta-hypotheses associated with the current proof (in
-case you forgot to bind them to an \ML{} identifier).
-\end{ttdescription}
-
-
-\subsection{Applying a tactic}
-\index{tactics!commands for applying}
-\begin{ttbox}
-by : tactic -> unit
-byev : tactic list -> unit
-\end{ttbox}
-These commands extend the state list. They apply a tactic to the current
-proof state. If the tactic succeeds, it returns a non-empty sequence of
-next states. The head of the sequence becomes the next state, while the
-tail is retained for backtracking (see~\texttt{back}).
-\begin{ttdescription} \item[\ttindexbold{by} {\it tactic};]
-applies the {\it tactic\/} to the proof state.
-
-\item[\ttindexbold{byev} {\it tactics};]
-applies the list of {\it tactics}, one at a time. It is useful for testing
-calls to \texttt{prove_goal}, and abbreviates \texttt{by (EVERY {\it
-tactics})}.
-\end{ttdescription}
-
-\noindent{\it Error indications:}\nobreak
-\begin{itemize}
-\item {\footnotesize\tt "by:\ tactic failed"} means that the tactic
- returned an empty sequence when applied to the current proof state.
-\item {\footnotesize\tt "Warning:\ same as previous level"} means that the
- new proof state is identical to the previous state.
-\item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
- means that some rule was applied whose theory is outside the theory of
- the initial proof state. This could signify a mistake such as expressing
- the goal in intuitionistic logic and proving it using classical logic.
-\end{itemize}
-
-\subsection{Extracting and storing the proved theorem}
-\label{ExtractingAndStoringTheProvedTheorem}
-\index{theorems!extracting proved}
-\begin{ttbox}
-qed : string -> unit
-no_qed : unit -> unit
-result : unit -> thm
-uresult : unit -> thm
-bind_thm : string * thm -> unit
-bind_thms : string * thm list -> unit
-store_thm : string * thm -> thm
-store_thms : string * thm list -> thm list
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{qed} $name$;] is the usual way of ending a proof.
- It combines \texttt{result} and \texttt{bind_thm}: it gets the theorem
- using \texttt{result()} and stores it the theorem database associated
- with its theory. See below for details.
-
-\item[\ttindexbold{no_qed}();] indicates that the proof is not concluded by a
- proper \texttt{qed} command. This is a do-nothing operation, it merely
- helps user interfaces such as Proof~General \cite{proofgeneral} to figure
- out the structure of the {\ML} text.
-
-\item[\ttindexbold{result}()]\index{assumptions!of main goal}
- returns the final theorem, after converting the free variables to
- schematics. It discharges the assumptions supplied to the matching
- \texttt{goal} command.
-
- It raises an exception unless the proof state passes certain checks. There
- must be no assumptions other than those supplied to \texttt{goal}. There
- must be no subgoals. The theorem proved must be a (first-order) instance
- of the original goal, as stated in the \texttt{goal} command. This allows
- {\bf answer extraction} --- instantiation of variables --- but no other
- changes to the main goal. The theorem proved must have the same signature
- as the initial proof state.
-
- These checks are needed because an Isabelle tactic can return any proof
- state at all.
-
-\item[\ttindexbold{uresult}()] is like \texttt{result()} but omits the checks.
- It is needed when the initial goal contains function unknowns, when
- definitions are unfolded in the main goal (by calling
- \ttindex{rewrite_tac}),\index{definitions!unfolding} or when
- \ttindex{assume_ax} has been used.
-
-\item[\ttindexbold{bind_thm} ($name$, $thm$);]\index{theorems!storing}
- stores \texttt{standard $thm$} (see \S\ref{MiscellaneousForwardRules})
- in the theorem database associated with its theory and in the {\ML}
- variable $name$. The theorem can be retrieved from the database
- using \texttt{get_thm} (see \S\ref{BasicOperationsOnTheories}).
-
-\item[\ttindexbold{store_thm} ($name$, $thm$)]\index{theorems!storing}
- stores $thm$ in the theorem database associated with its theory and
- returns that theorem.
-
-\item[\ttindexbold{bind_thms} \textrm{and} \ttindexbold{store_thms}] are similar to
- \texttt{bind_thm} and \texttt{store_thm}, but store lists of theorems.
-
-\end{ttdescription}
-
-The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be the empty
-string as well; in that case the result is \emph{not} stored, but proper
-checks and presentation of the result still apply.
-
-
-\subsection{Extracting axioms and stored theorems}
-\index{theories!axioms of}\index{axioms!extracting}
-\index{theories!theorems of}\index{theorems!extracting}
-\begin{ttbox}
-thm : xstring -> thm
-thms : xstring -> thm list
-get_axiom : theory -> xstring -> thm
-get_thm : theory -> xstring -> thm
-get_thms : theory -> xstring -> thm list
-axioms_of : theory -> (string * thm) list
-thms_of : theory -> (string * thm) list
-assume_ax : theory -> string -> thm
-\end{ttbox}
-\begin{ttdescription}
-
-\item[\ttindexbold{thm} $name$] is the basic user function for
- extracting stored theorems from the current theory context.
-
-\item[\ttindexbold{thms} $name$] is like \texttt{thm}, but returns a
- whole list associated with $name$ rather than a single theorem.
- Typically this will be collections stored by packages, e.g.\
- \verb|list.simps|.
-
-\item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the
- given $name$ from $thy$ or any of its ancestors, raising exception
- \xdx{THEORY} if none exists. Merging theories can cause several
- axioms to have the same name; {\tt get_axiom} returns an arbitrary
- one. Usually, axioms are also stored as theorems and may be
- retrieved via \texttt{get_thm} as well.
-
-\item[\ttindexbold{get_thm} $thy$ $name$] is analogous to {\tt
- get_axiom}, but looks for a theorem stored in the theory's
- database. Like {\tt get_axiom} it searches all parents of a theory
- if the theorem is not found directly in $thy$.
-
-\item[\ttindexbold{get_thms} $thy$ $name$] is like \texttt{get_thm}
- for retrieving theorem lists stored within the theory. It returns a
- singleton list if $name$ actually refers to a theorem rather than a
- theorem list.
-
-\item[\ttindexbold{axioms_of} $thy$] returns the axioms of this theory
- node, not including the ones of its ancestors.
-
-\item[\ttindexbold{thms_of} $thy$] returns all theorems stored within
- the database of this theory node, not including the ones of its
- ancestors.
-
-\item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula}
- using the syntax of $thy$, following the same conventions as axioms
- in a theory definition. You can thus pretend that {\it formula} is
- an axiom and use the resulting theorem like an axiom. Actually {\tt
- assume_ax} returns an assumption; \ttindex{qed} and
- \ttindex{result} complain about additional assumptions, but
- \ttindex{uresult} does not.
-
-For example, if {\it formula} is
-\hbox{\tt a=b ==> b=a} then the resulting theorem has the form
-\hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'}
-\end{ttdescription}
-
-
-\subsection{Retrieving theorems}
-\index{theorems!retrieving}
-
-The following functions retrieve theorems (together with their names)
-from the theorem database that is associated with the current proof
-state's theory. They can only find theorems that have explicitly been
-stored in the database using \ttindex{qed}, \ttindex{bind_thm} or
-related functions.
-\begin{ttbox}
-findI : int -> (string * thm) list
-findE : int -> int -> (string * thm) list
-findEs : int -> (string * thm) list
-thms_containing : xstring list -> (string * thm) list
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{findI} $i$]\index{assumptions!of main goal}
- returns all ``introduction rules'' applicable to subgoal $i$ --- all
- theorems whose conclusion matches (rather than unifies with) subgoal
- $i$. Useful in connection with \texttt{resolve_tac}.
-
-\item[\ttindexbold{findE} $n$ $i$] returns all ``elimination rules''
- applicable to premise $n$ of subgoal $i$ --- all those theorems whose
- first premise matches premise $n$ of subgoal $i$. Useful in connection with
- \texttt{eresolve_tac} and \texttt{dresolve_tac}.
-
-\item[\ttindexbold{findEs} $i$] returns all ``elimination rules'' applicable
- to subgoal $i$ --- all those theorems whose first premise matches some
- premise of subgoal $i$. Useful in connection with \texttt{eresolve_tac} and
- \texttt{dresolve_tac}.
-
-\item[\ttindexbold{thms_containing} $consts$] returns all theorems that
- contain \emph{all} of the given constants.
-\end{ttdescription}
-
-
-\subsection{Undoing and backtracking}
-\begin{ttbox}
-chop : unit -> unit
-choplev : int -> unit
-back : unit -> unit
-undo : unit -> unit
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{chop}();]
-deletes the top level of the state list, cancelling the last \ttindex{by}
-command. It provides a limited undo facility, and the \texttt{undo} command
-can cancel it.
-
-\item[\ttindexbold{choplev} {\it n};]
-truncates the state list to level~{\it n}, if $n\geq0$. A negative value
-of~$n$ refers to the $n$th previous level:
-\hbox{\verb|choplev ~1|} has the same effect as \texttt{chop}.
-
-\item[\ttindexbold{back}();]
-searches the state list for a non-empty branch point, starting from the top
-level. The first one found becomes the current proof state --- the most
-recent alternative branch is taken. This is a form of interactive
-backtracking.
-
-\item[\ttindexbold{undo}();]
-cancels the most recent change to the proof state by the commands \ttindex{by},
-\texttt{chop}, \texttt{choplev}, and~\texttt{back}. It {\bf cannot}
-cancel \texttt{goal} or \texttt{undo} itself. It can be repeated to
-cancel a series of commands.
-\end{ttdescription}
-
-\goodbreak
-\noindent{\it Error indications for {\tt back}:}\par\nobreak
-\begin{itemize}
-\item{\footnotesize\tt"Warning:\ same as previous choice at this level"}
- means \texttt{back} found a non-empty branch point, but that it contained
- the same proof state as the current one.
-\item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
- means the signature of the alternative proof state differs from that of
- the current state.
-\item {\footnotesize\tt "back:\ no alternatives"} means \texttt{back} could
- find no alternative proof state.
-\end{itemize}
-
-\subsection{Printing the proof state}\label{sec:goals-printing}
-\index{proof state!printing of}
-\begin{ttbox}
-pr : unit -> unit
-prlev : int -> unit
-prlim : int -> unit
-goals_limit: int ref \hfill{\bf initially 10}
-\end{ttbox}
-See also the printing control options described
-in~\S\ref{sec:printing-control}.
-\begin{ttdescription}
-\item[\ttindexbold{pr}();]
-prints the current proof state.
-
-\item[\ttindexbold{prlev} {\it n};]
-prints the proof state at level {\it n}, if $n\geq0$. A negative value
-of~$n$ refers to the $n$th previous level. This command allows
-you to review earlier stages of the proof.
-
-\item[\ttindexbold{prlim} {\it k};]
-prints the current proof state, limiting the number of subgoals to~$k$. It
-updates \texttt{goals_limit} (see below) and is helpful when there are many
-subgoals.
-
-\item[\ttindexbold{goals_limit} := {\it k};]
-specifies~$k$ as the maximum number of subgoals to print.
-\end{ttdescription}
-
-
-\subsection{Timing}
-\index{timing statistics}\index{proofs!timing}
-\begin{ttbox}
-timing: bool ref \hfill{\bf initially false}
-\end{ttbox}
-
-\begin{ttdescription}
-\item[set \ttindexbold{timing};] enables global timing in Isabelle. In
- particular, this makes the \ttindex{by} and \ttindex{prove_goal} commands
- display how much processor time was spent. This information is
- compiler-dependent.
-\end{ttdescription}
-
-
-\section{Shortcuts for applying tactics}
-\index{shortcuts!for \texttt{by} commands}
-These commands call \ttindex{by} with common tactics. Their chief purpose
-is to minimise typing, although the scanning shortcuts are useful in their
-own right. Chapter~\ref{tactics} explains the tactics themselves.
-
-\subsection{Refining a given subgoal}
-\begin{ttbox}
-ba : int -> unit
-br : thm -> int -> unit
-be : thm -> int -> unit
-bd : thm -> int -> unit
-brs : thm list -> int -> unit
-bes : thm list -> int -> unit
-bds : thm list -> int -> unit
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{ba} {\it i};]
-performs \texttt{by (assume_tac {\it i});}
-
-\item[\ttindexbold{br} {\it thm} {\it i};]
-performs \texttt{by (resolve_tac [{\it thm}] {\it i});}
-
-\item[\ttindexbold{be} {\it thm} {\it i};]
-performs \texttt{by (eresolve_tac [{\it thm}] {\it i});}
-
-\item[\ttindexbold{bd} {\it thm} {\it i};]
-performs \texttt{by (dresolve_tac [{\it thm}] {\it i});}
-
-\item[\ttindexbold{brs} {\it thms} {\it i};]
-performs \texttt{by (resolve_tac {\it thms} {\it i});}
-
-\item[\ttindexbold{bes} {\it thms} {\it i};]
-performs \texttt{by (eresolve_tac {\it thms} {\it i});}
-
-\item[\ttindexbold{bds} {\it thms} {\it i};]
-performs \texttt{by (dresolve_tac {\it thms} {\it i});}
-\end{ttdescription}
-
-
-\subsection{Scanning shortcuts}
-These shortcuts scan for a suitable subgoal (starting from subgoal~1).
-They refine the first subgoal for which the tactic succeeds. Thus, they
-require less typing than \texttt{br}, etc. They display the selected
-subgoal's number; please watch this, for it may not be what you expect!
-
-\begin{ttbox}
-fa : unit -> unit
-fr : thm -> unit
-fe : thm -> unit
-fd : thm -> unit
-frs : thm list -> unit
-fes : thm list -> unit
-fds : thm list -> unit
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{fa}();]
-solves some subgoal by assumption.
-
-\item[\ttindexbold{fr} {\it thm};]
-refines some subgoal using \texttt{resolve_tac [{\it thm}]}
-
-\item[\ttindexbold{fe} {\it thm};]
-refines some subgoal using \texttt{eresolve_tac [{\it thm}]}
-
-\item[\ttindexbold{fd} {\it thm};]
-refines some subgoal using \texttt{dresolve_tac [{\it thm}]}
-
-\item[\ttindexbold{frs} {\it thms};]
-refines some subgoal using \texttt{resolve_tac {\it thms}}
-
-\item[\ttindexbold{fes} {\it thms};]
-refines some subgoal using \texttt{eresolve_tac {\it thms}}
-
-\item[\ttindexbold{fds} {\it thms};]
-refines some subgoal using \texttt{dresolve_tac {\it thms}}
-\end{ttdescription}
-
-\subsection{Other shortcuts}
-\begin{ttbox}
-bw : thm -> unit
-bws : thm list -> unit
-ren : string -> int -> unit
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{bw} {\it def};] performs \texttt{by
- (rewrite_goals_tac [{\it def}]);} It unfolds definitions in the
- subgoals (but not the main goal), by meta-rewriting with the given
- definition (see also \S\ref{sec:rewrite_goals}).
- \index{meta-rewriting}
-
-\item[\ttindexbold{bws}]
-is like \texttt{bw} but takes a list of definitions.
-
-\item[\ttindexbold{ren} {\it names} {\it i};]
-performs \texttt{by (rename_tac {\it names} {\it i});} it renames
-parameters in subgoal~$i$. (Ignore the message {\footnotesize\tt Warning:\
- same as previous level}.)
-\index{parameters!renaming}
-\end{ttdescription}
-
-
-\section{Executing batch proofs}\label{sec:executing-batch}
-\index{batch execution}%
-To save space below, let type \texttt{tacfn} abbreviate \texttt{thm list ->
- tactic list}, which is the type of a tactical proof.
-\begin{ttbox}
-prove_goal : theory -> string -> tacfn -> thm
-qed_goal : string -> theory -> string -> tacfn -> unit
-prove_goalw: theory -> thm list -> string -> tacfn -> thm
-qed_goalw : string -> theory -> thm list -> string -> tacfn -> unit
-prove_goalw_cterm: thm list -> cterm -> tacfn -> thm
-\end{ttbox}
-These batch functions create an initial proof state, then apply a tactic to
-it, yielding a sequence of final proof states. The head of the sequence is
-returned, provided it is an instance of the theorem originally proposed.
-The forms \texttt{prove_goal}, \texttt{prove_goalw} and
-\texttt{prove_goalw_cterm} are analogous to \texttt{goal}, \texttt{goalw} and
-\texttt{goalw_cterm}.
-
-The tactic is specified by a function from theorem lists to tactic lists.
-The function is applied to the list of meta-assumptions taken from
-the main goal. The resulting tactics are applied in sequence (using {\tt
- EVERY}). For example, a proof consisting of the commands
-\begin{ttbox}
-val prems = goal {\it theory} {\it formula};
-by \(tac@1\); \ldots by \(tac@n\);
-qed "my_thm";
-\end{ttbox}
-can be transformed to an expression as follows:
-\begin{ttbox}
-qed_goal "my_thm" {\it theory} {\it formula}
- (fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]);
-\end{ttbox}
-The methods perform identical processing of the initial {\it formula} and
-the final proof state. But \texttt{prove_goal} executes the tactic as a
-atomic operation, bypassing the subgoal module; the current interactive
-proof is unaffected.
-%
-\begin{ttdescription}
-\item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};]
-executes a proof of the {\it formula\/} in the given {\it theory}, using
-the given tactic function.
-
-\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] acts
- like \texttt{prove_goal} but it also stores the resulting theorem in the
- theorem database associated with its theory and in the {\ML}
- variable $name$ (see \S\ref{ExtractingAndStoringTheProvedTheorem}).
-
-\item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula}
- {\it tacsf};]\index{meta-rewriting}
-is like \texttt{prove_goal} but also applies the list of {\it defs\/} as
-meta-rewrite rules to the first subgoal and the premises.
-
-\item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;]
-is analogous to \texttt{qed_goal}.
-
-\item[\ttindexbold{prove_goalw_cterm} {\it defs} {\it ct}
- {\it tacsf};]
-is a version of \texttt{prove_goalw} intended for programming. The main
-goal is supplied as a cterm, not as a string. A cterm carries a theory with
- it, and can be created from a term~$t$ by
-\begin{ttbox}
-cterm_of (sign_of thy) \(t\)
-\end{ttbox}
- \index{*cterm_of}\index{*sign_of}
-\end{ttdescription}
-
-
-\section{Internal proofs}
-
-\begin{ttbox}
-Tactic.prove: Sign.sg -> string list -> term list -> term ->
- (thm list -> tactic) -> thm
-Tactic.prove_standard: Sign.sg -> string list -> term list -> term ->
- (thm list -> tactic) -> thm
-\end{ttbox}
-
-These functions provide a clean internal interface for programmed proofs. The
-special overhead of top-level statements (cf.\ \verb,prove_goalw_cterm,) is
-omitted. Statements may be established within a local contexts of fixed
-variables and assumptions, which are the only hypotheses to be discharged in
-the result.
-
-\begin{ttdescription}
-\item[\ttindexbold{Tactic.prove}~$sg~xs~As~C~tacf$] establishes the result
- $\Forall xs. As \Imp C$ via the given tactic (which is a function taking the
- assumptions as local premises).
-
-\item[\ttindexbold{Tactic.prove_standard}] is simular to \verb,Tactic.prove,,
- but performs the \verb,standard, operation on the result, essentially
- turning it into a top-level statement. Never do this for local proofs
- within other proof tools!
-
-\end{ttdescription}
-
-
-\section{Managing multiple proofs}
-\index{proofs!managing multiple}
-You may save the current state of the subgoal module and resume work on it
-later. This serves two purposes.
-\begin{enumerate}
-\item At some point, you may be uncertain of the next step, and
-wish to experiment.
-
-\item During a proof, you may see that a lemma should be proved first.
-\end{enumerate}
-Each saved proof state consists of a list of levels; \ttindex{chop} behaves
-independently for each of the saved proofs. In addition, each saved state
-carries a separate \ttindex{undo} list.
-
-\subsection{The stack of proof states}
-\index{proofs!stacking}
-\begin{ttbox}
-push_proof : unit -> unit
-pop_proof : unit -> thm list
-rotate_proof : unit -> thm list
-\end{ttbox}
-The subgoal module maintains a stack of proof states. Most subgoal
-commands affect only the top of the stack. The \ttindex{Goal} command {\em
-replaces\/} the top of the stack; the only command that pushes a proof on the
-stack is \texttt{push_proof}.
-
-To save some point of the proof, call \texttt{push_proof}. You may now
-state a lemma using \texttt{goal}, or simply continue to apply tactics.
-Later, you can return to the saved point by calling \texttt{pop_proof} or
-\texttt{rotate_proof}.
-
-To view the entire stack, call \texttt{rotate_proof} repeatedly; as it rotates
-the stack, it prints the new top element.
-
-\begin{ttdescription}
-\item[\ttindexbold{push_proof}();]
-duplicates the top element of the stack, pushing a copy of the current
-proof state on to the stack.
-
-\item[\ttindexbold{pop_proof}();]
-discards the top element of the stack. It returns the list of
-assumptions associated with the new proof; you should bind these to an
-\ML\ identifier. They can also be obtained by calling \ttindex{premises}.
-
-\item[\ttindexbold{rotate_proof}();]
-\index{assumptions!of main goal}
-rotates the stack, moving the top element to the bottom. It returns the
-list of assumptions associated with the new proof.
-\end{ttdescription}
-
-
-\subsection{Saving and restoring proof states}
-\index{proofs!saving and restoring}
-\begin{ttbox}
-save_proof : unit -> proof
-restore_proof : proof -> thm list
-\end{ttbox}
-States of the subgoal module may be saved as \ML\ values of
-type~\mltydx{proof}, and later restored.
-
-\begin{ttdescription}
-\item[\ttindexbold{save_proof}();]
-returns the current state, which is on top of the stack.
-
-\item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal}
- replaces the top of the stack by~{\it prf}. It returns the list of
- assumptions associated with the new proof.
-\end{ttdescription}
-
-
-\section{*Debugging and inspecting}
-\index{tactics!debugging}
-These functions can be useful when you are debugging a tactic. They refer
-to the current proof state stored in the subgoal module. A tactic
-should never call them; it should operate on the proof state supplied as its
-argument.
-
-\subsection{Reading and printing terms}
-\index{terms!reading of}\index{terms!printing of}\index{types!printing of}
-\begin{ttbox}
-read : string -> term
-prin : term -> unit
-printyp : typ -> unit
-\end{ttbox}
-These read and print terms (or types) using the syntax associated with the
-proof state.
-
-\begin{ttdescription}
-\item[\ttindexbold{read} {\it string}]
-reads the {\it string} as a term, without type-checking.
-
-\item[\ttindexbold{prin} {\it t};]
-prints the term~$t$ at the terminal.
-
-\item[\ttindexbold{printyp} {\it T};]
-prints the type~$T$ at the terminal.
-\end{ttdescription}
-
-\subsection{Inspecting the proof state}
-\index{proofs!inspecting the state}
-\begin{ttbox}
-topthm : unit -> thm
-getgoal : int -> term
-gethyps : int -> thm list
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{topthm}()]
-returns the proof state as an Isabelle theorem. This is what \ttindex{by}
-would supply to a tactic at this point. It omits the post-processing of
-\ttindex{result} and \ttindex{uresult}.
-
-\item[\ttindexbold{getgoal} {\it i}]
-returns subgoal~$i$ of the proof state, as a term. You may print
-this using \texttt{prin}, though you may have to examine the internal
-data structure in order to locate the problem!
-
-\item[\ttindexbold{gethyps} {\it i}]
- returns the hypotheses of subgoal~$i$ as meta-level assumptions. In
- these theorems, the subgoal's parameters become free variables. This
- command is supplied for debugging uses of \ttindex{METAHYPS}.
-\end{ttdescription}
-
-
-\subsection{Filtering lists of rules}
-\begin{ttbox}
-filter_goal: (term*term->bool) -> thm list -> int -> thm list
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}]
-applies \texttt{filter_thms {\it could}} to subgoal~$i$ of the proof
-state and returns the list of theorems that survive the filtering.
-\end{ttdescription}
-
-\index{subgoal module|)}
-\index{proofs|)}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End:
--- a/doc-src/Ref/introduction.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/introduction.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,23 +1,5 @@
-
-%% $Id$
\chapter{Basic Use of Isabelle}\index{sessions|(}
-The Reference Manual is a comprehensive description of Isabelle
-proper, including all \ML{} commands, functions and packages. It
-really is intended for reference, perhaps for browsing, but not for
-reading through. It is not a tutorial, but assumes familiarity with
-the basic logical concepts of Isabelle.
-
-When you are looking for a way of performing some task, scan the Table of
-Contents for a relevant heading. Functions are organized by their purpose,
-by their operands (subgoals, tactics, theorems), and by their usefulness.
-In each section, basic functions appear first, then advanced functions, and
-finally esoteric functions. Use the Index when you are looking for the
-definition of a particular Isabelle function.
-
-A few examples are presented. Many example files are distributed with
-Isabelle, however; please experiment interactively.
-
\section{Basic interaction with Isabelle}
\index{starting up|bold}\nobreak
@@ -217,109 +199,6 @@
value is returned.
-\section{Printing of terms and theorems}\label{sec:printing-control}
-\index{printing control|(}
-Isabelle's pretty printer is controlled by a number of parameters.
-
-\subsection{Printing limits}
-\begin{ttbox}
-Pretty.setdepth : int -> unit
-Pretty.setmargin : int -> unit
-print_depth : int -> unit
-\end{ttbox}
-These set limits for terminal output. See also {\tt goals_limit},
-which limits the number of subgoals printed
-(\S\ref{sec:goals-printing}).
-
-\begin{ttdescription}
-\item[\ttindexbold{Pretty.setdepth} \(d\);] tells Isabelle's pretty printer to
- limit the printing depth to~$d$. This affects the display of theorems and
- terms. The default value is~0, which permits printing to an arbitrary
- depth. Useful values for $d$ are~10 and~20.
-
-\item[\ttindexbold{Pretty.setmargin} \(m\);]
- tells Isabelle's pretty printer to assume a right margin (page width)
- of~$m$. The initial margin is~76.
-
-\item[\ttindexbold{print_depth} \(n\);]
- limits the printing depth of complex \ML{} values, such as theorems and
- terms. This command affects the \ML{} top level and its effect is
- compiler-dependent. Typically $n$ should be less than~10.
-\end{ttdescription}
-
-
-\subsection{Printing of hypotheses, brackets, types etc.}
-\index{meta-assumptions!printing of}
-\index{types!printing of}\index{sorts!printing of}
-\begin{ttbox}
-show_hyps : bool ref \hfill{\bf initially false}
-show_tags : bool ref \hfill{\bf initially false}
-show_brackets : bool ref \hfill{\bf initially false}
-show_types : bool ref \hfill{\bf initially false}
-show_sorts : bool ref \hfill{\bf initially false}
-show_consts : bool ref \hfill{\bf initially false}
-long_names : bool ref \hfill{\bf initially false}
-\end{ttbox}
-These flags allow you to control how much information is displayed for
-types, terms and theorems. The hypotheses of theorems \emph{are}
-normally shown. Superfluous parentheses of types and terms are not.
-Types and sorts of variables are normally hidden.
-
-Note that displaying types and sorts may explain why a polymorphic
-inference rule fails to resolve with some goal, or why a rewrite rule
-does not apply as expected.
-
-\begin{ttdescription}
-
-\item[reset \ttindexbold{show_hyps};] makes Isabelle show each
- meta-level hypothesis as a dot.
-
-\item[set \ttindexbold{show_tags};] makes Isabelle show tags of theorems
- (which are basically just comments that may be attached by some tools).
-
-\item[set \ttindexbold{show_brackets};] makes Isabelle show full
- bracketing. In particular, this reveals the grouping of infix
- operators.
-
-\item[set \ttindexbold{show_types};] makes Isabelle show types when
- printing a term or theorem.
-
-\item[set \ttindexbold{show_sorts};] makes Isabelle show both types
- and the sorts of type variables, independently of the value of
- \texttt{show_types}.
-
-\item[set \ttindexbold{show_consts};] makes Isabelle show types of constants
- when printing proof states. Note that the output can be enormous as
- polymorphic constants often occur at several different type instances.
-
-\item[set \ttindexbold{long_names};] forces names of all objects
- (types, constants, theorems, etc.) to be printed in their fully
- qualified internal form.
-
-\end{ttdescription}
-
-
-\subsection{Eta-contraction before printing}
-\begin{ttbox}
-eta_contract: bool ref
-\end{ttbox}
-The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
-provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of
-functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$. Higher-order
-unification frequently puts terms into a fully $\eta$-expanded form. For
-example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
-$\lambda h.F(\lambda x.h(x))$. By default, the user sees this expanded
-form.
-
-\begin{ttdescription}
-\item[set \ttindexbold{eta_contract};]
-makes Isabelle perform $\eta$-contractions before printing, so that
-$\lambda h.F(\lambda x.h(x))$ appears simply as~$F$. The
-distinction between a term and its $\eta$-expanded form occasionally
-matters.
-\end{ttdescription}
-\index{printing control|)}
-
\section{Diagnostic messages}
\index{error messages}
\index{warnings}
@@ -351,40 +230,16 @@
\ttindex{warning} resume normal program execution.
-\section{Displaying exceptions as error messages}
-\index{exceptions!printing of}
+\section{Timing}
+\index{timing statistics}\index{proofs!timing}
\begin{ttbox}
-print_exn: exn -> 'a
+timing: bool ref \hfill{\bf initially false}
\end{ttbox}
-Certain Isabelle primitives, such as the forward proof functions {\tt RS}
-and {\tt RSN}, are called both interactively and from programs. They
-indicate errors not by printing messages, but by raising exceptions. For
-interactive use, \ML's reporting of an uncaught exception may be
-uninformative. The Poly/ML function {\tt exception_trace} can generate a
-backtrace.\index{Poly/{\ML} compiler}
\begin{ttdescription}
-\item[\ttindexbold{print_exn} $e$]
-displays the exception~$e$ in a readable manner, and then re-raises~$e$.
-Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
-$EXP$ is an expression that may raise an exception.
-
-{\tt print_exn} can display the following common exceptions, which concern
-types, terms, theorems and theories, respectively. Each carries a message
-and related information.
-\begin{ttbox}
-exception TYPE of string * typ list * term list
-exception TERM of string * term list
-exception THM of string * int * thm list
-exception THEORY of string * theory list
-\end{ttbox}
+\item[set \ttindexbold{timing};] enables global timing in Isabelle.
+ This information is compiler-dependent.
\end{ttdescription}
-\begin{warn}
- {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
- pretty printing information from the proof state last stored in the
- subgoal module. The appearance of the output thus depends upon the
- theory used in the last interactive proof.
-\end{warn}
\index{sessions|)}
--- a/doc-src/Ref/ref.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/ref.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,7 +1,6 @@
\documentclass[12pt,a4paper]{report}
-\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,../pdfsetup}
+\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../pdfsetup}
-%% $Id$
%%\includeonly{}
%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1}
%%% to delete old ones: \\indexbold{\*[^}]*}
@@ -22,10 +21,6 @@
\sloppy
\binperiod %%%treat . like a binary operator
-\railalias{lbrace}{\ttlbrace}
-\railalias{rbrace}{\ttrbrace}
-\railterm{lbrace,rbrace}
-
\begin{document}
\underscoreoff
@@ -34,17 +29,10 @@
\index{meta-rules|see{meta-rules}}
\maketitle
-\emph{Note}: this document is part of the earlier Isabelle documentation,
-which is somewhat superseded by the Isabelle/HOL
-\emph{Tutorial}~\cite{isa-tutorial}. Much of it is concerned with
-the old-style theory syntax and the primitives for conducting proofs
-using the ML top level. This style of interaction is largely obsolete:
-most Isabelle proofs are now written using the Isar
-language and the Proof General interface. However, this is the only
-comprehensive Isabelle reference manual.
-
-See also the \emph{Introduction to Isabelle}, which has tutorial examples
-on conducting proofs using the ML top-level.
+\emph{Note}: this document is part of the earlier Isabelle
+documentation and is mostly outdated. Fully obsolete parts of the
+original text have already been removed. The remaining material
+covers some aspects that did not make it into the newer manuals yet.
\subsubsection*{Acknowledgements}
Tobias Nipkow, of T. U. Munich, wrote most of
@@ -62,7 +50,6 @@
\pagenumbering{roman} \tableofcontents \clearfirst
\include{introduction}
-\include{goals}
\include{tactic}
\include{tctical}
\include{thm}
--- a/doc-src/Ref/simplifier.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/simplifier.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,4 +1,4 @@
-%% $Id$
+
\chapter{Simplification}
\label{chap:simplification}
\index{simplification|(}
@@ -810,173 +810,6 @@
\end{warn}
-\section{Examples of using the Simplifier}
-\index{examples!of simplification} Assume we are working within {\tt
- FOL} (see the file \texttt{FOL/ex/Nat}) and that
-\begin{ttdescription}
-\item[Nat.thy]
- is a theory including the constants $0$, $Suc$ and $+$,
-\item[add_0]
- is the rewrite rule $0+\Var{n} = \Var{n}$,
-\item[add_Suc]
- is the rewrite rule $Suc(\Var{m})+\Var{n} = Suc(\Var{m}+\Var{n})$,
-\item[induct]
- is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp
- \Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$.
-\end{ttdescription}
-We augment the implicit simpset inherited from \texttt{Nat} with the
-basic rewrite rules for addition of natural numbers:
-\begin{ttbox}
-Addsimps [add_0, add_Suc];
-\end{ttbox}
-
-\subsection{A trivial example}
-Proofs by induction typically involve simplification. Here is a proof
-that~0 is a right identity:
-\begin{ttbox}
-Goal "m+0 = m";
-{\out Level 0}
-{\out m + 0 = m}
-{\out 1. m + 0 = m}
-\end{ttbox}
-The first step is to perform induction on the variable~$m$. This returns a
-base case and inductive step as two subgoals:
-\begin{ttbox}
-by (res_inst_tac [("n","m")] induct 1);
-{\out Level 1}
-{\out m + 0 = m}
-{\out 1. 0 + 0 = 0}
-{\out 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
-\end{ttbox}
-Simplification solves the first subgoal trivially:
-\begin{ttbox}
-by (Simp_tac 1);
-{\out Level 2}
-{\out m + 0 = m}
-{\out 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
-\end{ttbox}
-The remaining subgoal requires \ttindex{Asm_simp_tac} in order to use the
-induction hypothesis as a rewrite rule:
-\begin{ttbox}
-by (Asm_simp_tac 1);
-{\out Level 3}
-{\out m + 0 = m}
-{\out No subgoals!}
-\end{ttbox}
-
-\subsection{An example of tracing}
-\index{tracing!of simplification|(}\index{*trace_simp}
-
-Let us prove a similar result involving more complex terms. We prove
-that addition is commutative.
-\begin{ttbox}
-Goal "m+Suc(n) = Suc(m+n)";
-{\out Level 0}
-{\out m + Suc(n) = Suc(m + n)}
-{\out 1. m + Suc(n) = Suc(m + n)}
-\end{ttbox}
-Performing induction on~$m$ yields two subgoals:
-\begin{ttbox}
-by (res_inst_tac [("n","m")] induct 1);
-{\out Level 1}
-{\out m + Suc(n) = Suc(m + n)}
-{\out 1. 0 + Suc(n) = Suc(0 + n)}
-{\out 2. !!x. x + Suc(n) = Suc(x + n) ==>}
-{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)}
-\end{ttbox}
-Simplification solves the first subgoal, this time rewriting two
-occurrences of~0:
-\begin{ttbox}
-by (Simp_tac 1);
-{\out Level 2}
-{\out m + Suc(n) = Suc(m + n)}
-{\out 1. !!x. x + Suc(n) = Suc(x + n) ==>}
-{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)}
-\end{ttbox}
-Switching tracing on illustrates how the simplifier solves the remaining
-subgoal:
-\begin{ttbox}
-set trace_simp;
-by (Asm_simp_tac 1);
-\ttbreak
-{\out Adding rewrite rule:}
-{\out .x + Suc n == Suc (.x + n)}
-\ttbreak
-{\out Applying instance of rewrite rule:}
-{\out ?m + Suc ?n == Suc (?m + ?n)}
-{\out Rewriting:}
-{\out Suc .x + Suc n == Suc (Suc .x + n)}
-\ttbreak
-{\out Applying instance of rewrite rule:}
-{\out Suc ?m + ?n == Suc (?m + ?n)}
-{\out Rewriting:}
-{\out Suc .x + n == Suc (.x + n)}
-\ttbreak
-{\out Applying instance of rewrite rule:}
-{\out Suc ?m + ?n == Suc (?m + ?n)}
-{\out Rewriting:}
-{\out Suc .x + n == Suc (.x + n)}
-\ttbreak
-{\out Applying instance of rewrite rule:}
-{\out ?x = ?x == True}
-{\out Rewriting:}
-{\out Suc (Suc (.x + n)) = Suc (Suc (.x + n)) == True}
-\ttbreak
-{\out Level 3}
-{\out m + Suc(n) = Suc(m + n)}
-{\out No subgoals!}
-\end{ttbox}
-Many variations are possible. At Level~1 (in either example) we could have
-solved both subgoals at once using the tactical \ttindex{ALLGOALS}:
-\begin{ttbox}
-by (ALLGOALS Asm_simp_tac);
-{\out Level 2}
-{\out m + Suc(n) = Suc(m + n)}
-{\out No subgoals!}
-\end{ttbox}
-\index{tracing!of simplification|)}
-
-
-\subsection{Free variables and simplification}
-
-Here is a conjecture to be proved for an arbitrary function~$f$
-satisfying the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$:
-\begin{ttbox}
-val [prem] = Goal
- "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
-{\out Level 0}
-{\out f(i + j) = i + f(j)}
-{\out 1. f(i + j) = i + f(j)}
-\ttbreak
-{\out val prem = "f(Suc(?n)) = Suc(f(?n))}
-{\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm}
-\end{ttbox}
-In the theorem~\texttt{prem}, note that $f$ is a free variable while
-$\Var{n}$ is a schematic variable.
-\begin{ttbox}
-by (res_inst_tac [("n","i")] induct 1);
-{\out Level 1}
-{\out f(i + j) = i + f(j)}
-{\out 1. f(0 + j) = 0 + f(j)}
-{\out 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
-\end{ttbox}
-We simplify each subgoal in turn. The first one is trivial:
-\begin{ttbox}
-by (Simp_tac 1);
-{\out Level 2}
-{\out f(i + j) = i + f(j)}
-{\out 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
-\end{ttbox}
-The remaining subgoal requires rewriting by the premise, so we add it
-to the current simpset:
-\begin{ttbox}
-by (asm_simp_tac (simpset() addsimps [prem]) 1);
-{\out Level 3}
-{\out f(i + j) = i + f(j)}
-{\out No subgoals!}
-\end{ttbox}
-
-
\section{Permutative rewrite rules}
\index{rewrite rules!permutative|(}
--- a/doc-src/Ref/substitution.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/substitution.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,4 +1,4 @@
-%% $Id$
+
\chapter{Substitution Tactics} \label{substitution}
\index{tactics!substitution|(}\index{equality|(}
--- a/doc-src/Ref/syntax.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/syntax.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,4 +1,4 @@
-%% $Id$
+
\chapter{Syntax Transformations} \label{chap:syntax}
\newcommand\ttapp{\mathrel{\hbox{\tt\$}}}
\newcommand\mtt[1]{\mbox{\tt #1}}
--- a/doc-src/Ref/tactic.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/tactic.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,235 +1,8 @@
-%% $Id$
+
\chapter{Tactics} \label{tactics}
-\index{tactics|(} Tactics have type \mltydx{tactic}. This is just an
-abbreviation for functions from theorems to theorem sequences, where
-the theorems represent states of a backward proof. Tactics seldom
-need to be coded from scratch, as functions; instead they are
-expressed using basic tactics and tacticals.
-
-This chapter only presents the primitive tactics. Substantial proofs
-require the power of automatic tools like simplification
-(Chapter~\ref{chap:simplification}) and classical tableau reasoning
-(Chapter~\ref{chap:classical}).
-
-\section{Resolution and assumption tactics}
-{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
-a rule. {\bf Elim-resolution} is particularly suited for elimination
-rules, while {\bf destruct-resolution} is particularly suited for
-destruction rules. The {\tt r}, {\tt e}, {\tt d} naming convention is
-maintained for several different kinds of resolution tactics, as well as
-the shortcuts in the subgoal module.
-
-All the tactics in this section act on a subgoal designated by a positive
-integer~$i$. They fail (by returning the empty sequence) if~$i$ is out of
-range.
-
-\subsection{Resolution tactics}
-\index{resolution!tactics}
-\index{tactics!resolution|bold}
-\begin{ttbox}
-resolve_tac : thm list -> int -> tactic
-eresolve_tac : thm list -> int -> tactic
-dresolve_tac : thm list -> int -> tactic
-forward_tac : thm list -> int -> tactic
-\end{ttbox}
-These perform resolution on a list of theorems, $thms$, representing a list
-of object-rules. When generating next states, they take each of the rules
-in the order given. Each rule may yield several next states, or none:
-higher-order resolution may yield multiple resolvents.
-\begin{ttdescription}
-\item[\ttindexbold{resolve_tac} {\it thms} {\it i}]
- refines the proof state using the rules, which should normally be
- introduction rules. It resolves a rule's conclusion with
- subgoal~$i$ of the proof state.
-
-\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}]
- \index{elim-resolution}
- performs elim-resolution with the rules, which should normally be
- elimination rules. It resolves with a rule, proves its first premise by
- assumption, and finally \emph{deletes} that assumption from any new
- subgoals. (To rotate a rule's premises,
- see \texttt{rotate_prems} in~{\S}\ref{MiscellaneousForwardRules}.)
-
-\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}]
- \index{forward proof}\index{destruct-resolution}
- performs destruct-resolution with the rules, which normally should
- be destruction rules. This replaces an assumption by the result of
- applying one of the rules.
-
-\item[\ttindexbold{forward_tac}]\index{forward proof}
- is like {\tt dresolve_tac} except that the selected assumption is not
- deleted. It applies a rule to an assumption, adding the result as a new
- assumption.
-\end{ttdescription}
-
-\subsection{Assumption tactics}
-\index{tactics!assumption|bold}\index{assumptions!tactics for}
-\begin{ttbox}
-assume_tac : int -> tactic
-eq_assume_tac : int -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{assume_tac} {\it i}]
-attempts to solve subgoal~$i$ by assumption.
-
-\item[\ttindexbold{eq_assume_tac}]
-is like {\tt assume_tac} but does not use unification. It succeeds (with a
-\emph{unique} next state) if one of the assumptions is identical to the
-subgoal's conclusion. Since it does not instantiate variables, it cannot
-make other subgoals unprovable. It is intended to be called from proof
-strategies, not interactively.
-\end{ttdescription}
-
-\subsection{Matching tactics} \label{match_tac}
-\index{tactics!matching}
-\begin{ttbox}
-match_tac : thm list -> int -> tactic
-ematch_tac : thm list -> int -> tactic
-dmatch_tac : thm list -> int -> tactic
-\end{ttbox}
-These are just like the resolution tactics except that they never
-instantiate unknowns in the proof state. Flexible subgoals are not updated
-willy-nilly, but are left alone. Matching --- strictly speaking --- means
-treating the unknowns in the proof state as constants; these tactics merely
-discard unifiers that would update the proof state.
-\begin{ttdescription}
-\item[\ttindexbold{match_tac} {\it thms} {\it i}]
-refines the proof state using the rules, matching a rule's
-conclusion with subgoal~$i$ of the proof state.
-
-\item[\ttindexbold{ematch_tac}]
-is like {\tt match_tac}, but performs elim-resolution.
-
-\item[\ttindexbold{dmatch_tac}]
-is like {\tt match_tac}, but performs destruct-resolution.
-\end{ttdescription}
-
-
-\subsection{Explicit instantiation} \label{res_inst_tac}
-\index{tactics!instantiation}\index{instantiation}
-\begin{ttbox}
-res_inst_tac : (string*string)list -> thm -> int -> tactic
-eres_inst_tac : (string*string)list -> thm -> int -> tactic
-dres_inst_tac : (string*string)list -> thm -> int -> tactic
-forw_inst_tac : (string*string)list -> thm -> int -> tactic
-instantiate_tac : (string*string)list -> tactic
-\end{ttbox}
-The first four of these tactics are designed for applying rules by resolution
-such as substitution and induction, which cause difficulties for higher-order
-unification. The tactics accept explicit instantiations for unknowns
-in the rule ---typically, in the rule's conclusion. The last one,
-{\tt instantiate_tac}, may be used to instantiate unknowns in the proof state,
-independently of rule application.
-
-Each instantiation is a pair {\tt($v$,$e$)},
-where $v$ is an unknown \emph{without} its leading question mark!
-\begin{itemize}
-\item If $v$ is the type unknown {\tt'a}, then
-the rule must contain a type unknown \verb$?'a$ of some
-sort~$s$, and $e$ should be a type of sort $s$.
-
-\item If $v$ is the unknown {\tt P}, then
-the rule must contain an unknown \verb$?P$ of some type~$\tau$,
-and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
-$\sigma$ are unifiable. If the unification of $\tau$ and $\sigma$
-instantiates any type unknowns in $\tau$, these instantiations
-are recorded for application to the rule.
-\end{itemize}
-Types are instantiated before terms are. Because type instantiations are
-inferred from term instantiations, explicit type instantiations are seldom
-necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
-\texttt{[("'a","bool"), ("t","True")]} may be simplified to
-\texttt{[("t","True")]}. Type unknowns in the proof state may cause
-failure because the tactics cannot instantiate them.
-
-The first four instantiation tactics act on a given subgoal. Terms in the
-instantiations are type-checked in the context of that subgoal --- in
-particular, they may refer to that subgoal's parameters. Any unknowns in
-the terms receive subscripts and are lifted over the parameters; thus, you
-may not refer to unknowns in the subgoal.
-
-\begin{ttdescription}
-\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
-instantiates the rule {\it thm} with the instantiations {\it insts}, as
-described above, and then performs resolution on subgoal~$i$. Resolution
-typically causes further instantiations; you need not give explicit
-instantiations for every unknown in the rule.
-
-\item[\ttindexbold{eres_inst_tac}]
-is like {\tt res_inst_tac}, but performs elim-resolution.
-
-\item[\ttindexbold{dres_inst_tac}]
-is like {\tt res_inst_tac}, but performs destruct-resolution.
-
-\item[\ttindexbold{forw_inst_tac}]
-is like {\tt dres_inst_tac} except that the selected assumption is not
-deleted. It applies the instantiated rule to an assumption, adding the
-result as a new assumption.
-
-\item[\ttindexbold{instantiate_tac} {\it insts}]
-instantiates unknowns in the proof state. This affects the main goal as
-well as all subgoals.
-\end{ttdescription}
-
+\index{tactics|(}
\section{Other basic tactics}
-\subsection{Tactic shortcuts}
-\index{shortcuts!for tactics}
-\index{tactics!resolution}\index{tactics!assumption}
-\index{tactics!meta-rewriting}
-\begin{ttbox}
-rtac : thm -> int -> tactic
-etac : thm -> int -> tactic
-dtac : thm -> int -> tactic
-ftac : thm -> int -> tactic
-atac : int -> tactic
-eatac : thm -> int -> int -> tactic
-datac : thm -> int -> int -> tactic
-fatac : thm -> int -> int -> tactic
-ares_tac : thm list -> int -> tactic
-rewtac : thm -> tactic
-\end{ttbox}
-These abbreviate common uses of tactics.
-\begin{ttdescription}
-\item[\ttindexbold{rtac} {\it thm} {\it i}]
-abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.
-
-\item[\ttindexbold{etac} {\it thm} {\it i}]
-abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.
-
-\item[\ttindexbold{dtac} {\it thm} {\it i}]
-abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
-destruct-resolution.
-
-\item[\ttindexbold{ftac} {\it thm} {\it i}]
-abbreviates \hbox{\tt forward_tac [{\it thm}] {\it i}}, doing
-destruct-resolution without deleting the assumption.
-
-\item[\ttindexbold{atac} {\it i}]
-abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
-
-\item[\ttindexbold{eatac} {\it thm} {\it j} {\it i}]
-performs \hbox{\tt etac {\it thm}} and then {\it j} times \texttt{atac},
-solving additionally {\it j}~premises of the rule {\it thm} by assumption.
-
-\item[\ttindexbold{datac} {\it thm} {\it j} {\it i}]
-performs \hbox{\tt dtac {\it thm}} and then {\it j} times \texttt{atac},
-solving additionally {\it j}~premises of the rule {\it thm} by assumption.
-
-\item[\ttindexbold{fatac} {\it thm} {\it j} {\it i}]
-performs \hbox{\tt ftac {\it thm}} and then {\it j} times \texttt{atac},
-solving additionally {\it j}~premises of the rule {\it thm} by assumption.
-
-\item[\ttindexbold{ares_tac} {\it thms} {\it i}]
-tries proof by assumption and resolution; it abbreviates
-\begin{ttbox}
-assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
-\end{ttbox}
-
-\item[\ttindexbold{rewtac} {\it def}]
-abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
-\end{ttdescription}
-
\subsection{Inserting premises and facts}\label{cut_facts_tac}
\index{tactics!for inserting facts}\index{assumptions!inserting}
@@ -351,52 +124,6 @@
\section{Obscure tactics}
-\subsection{Renaming parameters in a goal} \index{parameters!renaming}
-\begin{ttbox}
-rename_tac : string -> int -> tactic
-rename_last_tac : string -> string list -> int -> tactic
-Logic.set_rename_prefix : string -> unit
-Logic.auto_rename : bool ref \hfill{\bf initially false}
-\end{ttbox}
-When creating a parameter, Isabelle chooses its name by matching variable
-names via the object-rule. Given the rule $(\forall I)$ formalized as
-$\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that
-the $\Forall$-bound variable in the premise has the same name as the
-$\forall$-bound variable in the conclusion.
-
-Sometimes there is insufficient information and Isabelle chooses an
-arbitrary name. The renaming tactics let you override Isabelle's choice.
-Because renaming parameters has no logical effect on the proof state, the
-{\tt by} command prints the message {\tt Warning:\ same as previous
-level}.
-
-Alternatively, you can suppress the naming mechanism described above and
-have Isabelle generate uniform names for parameters. These names have the
-form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired
-prefix. They are ugly but predictable.
-
-\begin{ttdescription}
-\item[\ttindexbold{rename_tac} {\it str} {\it i}]
-interprets the string {\it str} as a series of blank-separated variable
-names, and uses them to rename the parameters of subgoal~$i$. The names
-must be distinct. If there are fewer names than parameters, then the
-tactic renames the innermost parameters and may modify the remaining ones
-to ensure that all the parameters are distinct.
-
-\item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}]
-generates a list of names by attaching each of the {\it suffixes\/} to the
-{\it prefix}. It is intended for coding structural induction tactics,
-where several of the new parameters should have related names.
-
-\item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};]
-sets the prefix for uniform renaming to~{\it prefix}. The default prefix
-is {\tt"k"}.
-
-\item[set \ttindexbold{Logic.auto_rename};]
-makes Isabelle generate uniform names for parameters.
-\end{ttdescription}
-
-
\subsection{Manipulating assumptions}
\index{assumptions!rotating}
\begin{ttbox}
@@ -594,142 +321,6 @@
is no longer than {\it limit}.
\end{ttdescription}
-
-\section{Programming tools for proof strategies}
-Do not consider using the primitives discussed in this section unless you
-really need to code tactics from scratch.
-
-\subsection{Operations on tactics}
-\index{tactics!primitives for coding} A tactic maps theorems to sequences of
-theorems. The type constructor for sequences (lazy lists) is called
-\mltydx{Seq.seq}. To simplify the types of tactics and tacticals,
-Isabelle defines a type abbreviation:
-\begin{ttbox}
-type tactic = thm -> thm Seq.seq
-\end{ttbox}
-The following operations provide means for coding tactics in a clean style.
-\begin{ttbox}
-PRIMITIVE : (thm -> thm) -> tactic
-SUBGOAL : ((term*int) -> tactic) -> int -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that
- applies $f$ to the proof state and returns the result as a one-element
- sequence. If $f$ raises an exception, then the tactic's result is the empty
- sequence.
-
-\item[\ttindexbold{SUBGOAL} $f$ $i$]
-extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
-tactic by calling~$f(t,i)$. It applies the resulting tactic to the same
-state. The tactic body is expressed using tactics and tacticals, but may
-peek at a particular subgoal:
-\begin{ttbox}
-SUBGOAL (fn (t,i) => {\it tactic-valued expression})
-\end{ttbox}
-\end{ttdescription}
-
-
-\subsection{Tracing}
-\index{tactics!tracing}
-\index{tracing!of tactics}
-\begin{ttbox}
-pause_tac: tactic
-print_tac: string -> tactic
-\end{ttbox}
-These tactics print tracing information when they are applied to a proof
-state. Their output may be difficult to interpret. Note that certain of
-the searching tacticals, such as {\tt REPEAT}, have built-in tracing
-options.
-\begin{ttdescription}
-\item[\ttindexbold{pause_tac}]
-prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line
-from the terminal. If this line is blank then it returns the proof state
-unchanged; otherwise it fails (which may terminate a repetition).
-
-\item[\ttindexbold{print_tac}~$msg$]
-returns the proof state unchanged, with the side effect of printing it at
-the terminal.
-\end{ttdescription}
-
-
-\section{*Sequences}
-\index{sequences (lazy lists)|bold}
-The module {\tt Seq} declares a type of lazy lists. It uses
-Isabelle's type \mltydx{option} to represent the possible presence
-(\ttindexbold{Some}) or absence (\ttindexbold{None}) of
-a value:
-\begin{ttbox}
-datatype 'a option = None | Some of 'a;
-\end{ttbox}
-The {\tt Seq} structure is supposed to be accessed via fully qualified
-names and should not be \texttt{open}.
-
-\subsection{Basic operations on sequences}
-\begin{ttbox}
-Seq.empty : 'a seq
-Seq.make : (unit -> ('a * 'a seq) option) -> 'a seq
-Seq.single : 'a -> 'a seq
-Seq.pull : 'a seq -> ('a * 'a seq) option
-\end{ttbox}
-\begin{ttdescription}
-\item[Seq.empty] is the empty sequence.
-
-\item[\tt Seq.make (fn () => Some ($x$, $xq$))] constructs the
- sequence with head~$x$ and tail~$xq$, neither of which is evaluated.
-
-\item[Seq.single $x$]
-constructs the sequence containing the single element~$x$.
-
-\item[Seq.pull $xq$] returns {\tt None} if the sequence is empty and
- {\tt Some ($x$, $xq'$)} if the sequence has head~$x$ and tail~$xq'$.
- Warning: calling \hbox{Seq.pull $xq$} again will {\it recompute\/}
- the value of~$x$; it is not stored!
-\end{ttdescription}
-
-
-\subsection{Converting between sequences and lists}
-\begin{ttbox}
-Seq.chop : int * 'a seq -> 'a list * 'a seq
-Seq.list_of : 'a seq -> 'a list
-Seq.of_list : 'a list -> 'a seq
-\end{ttbox}
-\begin{ttdescription}
-\item[Seq.chop ($n$, $xq$)] returns the first~$n$ elements of~$xq$ as a
- list, paired with the remaining elements of~$xq$. If $xq$ has fewer
- than~$n$ elements, then so will the list.
-
-\item[Seq.list_of $xq$] returns the elements of~$xq$, which must be
- finite, as a list.
-
-\item[Seq.of_list $xs$] creates a sequence containing the elements
- of~$xs$.
-\end{ttdescription}
-
-
-\subsection{Combining sequences}
-\begin{ttbox}
-Seq.append : 'a seq * 'a seq -> 'a seq
-Seq.interleave : 'a seq * 'a seq -> 'a seq
-Seq.flat : 'a seq seq -> 'a seq
-Seq.map : ('a -> 'b) -> 'a seq -> 'b seq
-Seq.filter : ('a -> bool) -> 'a seq -> 'a seq
-\end{ttbox}
-\begin{ttdescription}
-\item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$.
-
-\item[Seq.interleave ($xq$, $yq$)] joins $xq$ with $yq$ by
- interleaving their elements. The result contains all the elements
- of the sequences, even if both are infinite.
-
-\item[Seq.flat $xqq$] concatenates a sequence of sequences.
-
-\item[Seq.map $f$ $xq$] applies $f$ to every element
- of~$xq=x@1,x@2,\ldots$, yielding the sequence $f(x@1),f(x@2),\ldots$.
-
-\item[Seq.filter $p$ $xq$] returns the sequence consisting of all
- elements~$x$ of~$xq$ such that $p(x)$ is {\tt true}.
-\end{ttdescription}
-
\index{tactics|)}
--- a/doc-src/Ref/tctical.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/tctical.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,4 +1,4 @@
-%% $Id$
+
\chapter{Tacticals}
\index{tacticals|(}
Tacticals are operations on tactics. Their implementation makes use of
--- a/doc-src/Ref/theories.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/theories.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,216 +1,6 @@
-
-%% $Id$
\chapter{Theories, Terms and Types} \label{theories}
-\index{theories|(}\index{signatures|bold}
-\index{reading!axioms|see{\texttt{assume_ax}}} Theories organize the syntax,
-declarations and axioms of a mathematical development. They are built,
-starting from the Pure or CPure theory, by extending and merging existing
-theories. They have the \ML\ type \mltydx{theory}. Theory operations signal
-errors by raising exception \xdx{THEORY}, returning a message and a list of
-theories.
-
-Signatures, which contain information about sorts, types, constants and
-syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each
-signature carries a unique list of \bfindex{stamps}, which are \ML\
-references to strings. The strings serve as human-readable names; the
-references serve as unique identifiers. Each primitive signature has a
-single stamp. When two signatures are merged, their lists of stamps are
-also merged. Every theory carries a unique signature.
-
-Terms and types are the underlying representation of logical syntax. Their
-\ML\ definitions are irrelevant to naive Isabelle users. Programmers who
-wish to extend Isabelle may need to know such details, say to code a tactic
-that looks for subgoals of a particular form. Terms and types may be
-`certified' to be well-formed with respect to a given signature.
-
-
-\section{Defining theories}\label{sec:ref-defining-theories}
-
-Theories are defined via theory files $name$\texttt{.thy} (there are also
-\ML-level interfaces which are only intended for people building advanced
-theory definition packages). Appendix~\ref{app:TheorySyntax} presents the
-concrete syntax for theory files; here follows an explanation of the
-constituent parts.
-\begin{description}
-\item[{\it theoryDef}] is the full definition. The new theory is called $id$.
- It is the union of the named \textbf{parent
- theories}\indexbold{theories!parent}, possibly extended with new
- components. \thydx{Pure} and \thydx{CPure} are the basic theories, which
- contain only the meta-logic. They differ just in their concrete syntax for
- function applications.
-
- The new theory begins as a merge of its parents.
- \begin{ttbox}
- Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
- \end{ttbox}
- This error may especially occur when a theory is redeclared --- say to
- change an inappropriate definition --- and bindings to old versions persist.
- Isabelle ensures that old and new theories of the same name are not involved
- in a proof.
-
-\item[$classes$]
- is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\
- $id@n$} makes $id$ a subclass of the existing classes $id@1\dots
- id@n$. This rules out cyclic class structures. Isabelle automatically
- computes the transitive closure of subclass hierarchies; it is not
- necessary to declare \texttt{c < e} in addition to \texttt{c < d} and \texttt{d <
- e}.
-
-\item[$default$]
- introduces $sort$ as the new default sort for type variables. This applies
- to unconstrained type variables in an input string but not to type
- variables created internally. If omitted, the default sort is the listwise
- union of the default sorts of the parent theories (i.e.\ their logical
- intersection).
-
-\item[$sort$] is a finite set of classes. A single class $id$ abbreviates the
- sort $\{id\}$.
-
-\item[$types$]
- is a series of type declarations. Each declares a new type constructor
- or type synonym. An $n$-place type constructor is specified by
- $(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to
- indicate the number~$n$.
-
- A \textbf{type synonym}\indexbold{type synonyms} is an abbreviation
- $(\alpha@1,\dots,\alpha@n)name = \tau$, where $name$ and $\tau$ can
- be strings.
-
-\item[$infix$]
- declares a type or constant to be an infix operator having priority $nat$
- and associating to the left (\texttt{infixl}) or right (\texttt{infixr}).
- Only 2-place type constructors can have infix status; an example is {\tt
- ('a,'b)~"*"~(infixr~20)}, which may express binary product types.
-
-\item[$arities$] is a series of type arity declarations. Each assigns
- arities to type constructors. The $name$ must be an existing type
- constructor, which is given the additional arity $arity$.
-
-\item[$nonterminals$]\index{*nonterminal symbols} declares purely
- syntactic types to be used as nonterminal symbols of the context
- free grammar.
-
-\item[$consts$] is a series of constant declarations. Each new
- constant $name$ is given the specified type. The optional $mixfix$
- annotations may attach concrete syntax to the constant.
-
-\item[$syntax$] \index{*syntax section}\index{print mode} is a variant
- of $consts$ which adds just syntax without actually declaring
- logical constants. This gives full control over a theory's context
- free grammar. The optional $mode$ specifies the print mode where the
- mixfix productions should be added. If there is no \texttt{output}
- option given, all productions are also added to the input syntax
- (regardless of the print mode).
-
-\item[$mixfix$] \index{mixfix declarations}
- annotations can take three forms:
- \begin{itemize}
- \item A mixfix template given as a $string$ of the form
- {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
- indicates the position where the $i$-th argument should go. The list
- of numbers gives the priority of each argument. The final number gives
- the priority of the whole construct.
-
- \item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf
- infix} status.
-
- \item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf
- binder} status. The declaration \texttt{binder} $\cal Q$ $p$ causes
- ${\cal Q}\,x.F(x)$ to be treated
- like $f(F)$, where $p$ is the priority.
- \end{itemize}
-
-\item[$trans$]
- specifies syntactic translation rules (macros). There are three forms:
- parse rules (\texttt{=>}), print rules (\texttt{<=}), and parse/print rules ({\tt
- ==}).
-
-\item[$rules$]
- is a series of rule declarations. Each has a name $id$ and the formula is
- given by the $string$. Rule names must be distinct within any single
- theory.
-
-\item[$defs$] is a series of definitions. They are just like $rules$, except
- that every $string$ must be a definition (see below for details).
-
-\item[$constdefs$] combines the declaration of constants and their
- definition. The first $string$ is the type, the second the definition.
-
-\item[$axclass$] \index{*axclass section} defines an \rmindex{axiomatic type
- class} \cite{Wenzel:1997:TPHOL} as the intersection of existing classes,
- with additional axioms holding. Class axioms may not contain more than one
- type variable. The class axioms (with implicit sort constraints added) are
- bound to the given names. Furthermore a class introduction rule is
- generated, which is automatically employed by $instance$ to prove
- instantiations of this class.
-
-\item[$instance$] \index{*instance section} proves class inclusions or
- type arities at the logical level and then transfers these to the
- type signature. The instantiation is proven and checked properly.
- The user has to supply sufficient witness information: theorems
- ($longident$), axioms ($string$), or even arbitrary \ML{} tactic
- code $verbatim$.
-
-\item[$oracle$] links the theory to a trusted external reasoner. It is
- allowed to create theorems, but each theorem carries a proof object
- describing the oracle invocation. See \S\ref{sec:oracles} for details.
-
-\item[$local$, $global$] change the current name declaration mode.
- Initially, theories start in $local$ mode, causing all names of
- types, constants, axioms etc.\ to be automatically qualified by the
- theory name. Changing this to $global$ causes all names to be
- declared as short base names only.
-
- The $local$ and $global$ declarations act like switches, affecting
- all following theory sections until changed again explicitly. Also
- note that the final state at the end of the theory will persist. In
- particular, this determines how the names of theorems stored later
- on are handled.
-
-\item[$setup$]\index{*setup!theory} applies a list of ML functions to
- the theory. The argument should denote a value of type
- \texttt{(theory -> theory) list}. Typically, ML packages are
- initialized in this way.
-
-\item[$ml$] \index{*ML section}
- consists of \ML\ code, typically for parse and print translation functions.
-\end{description}
-%
-Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix
-declarations, translation rules and the \texttt{ML} section in more detail.
-
-
-\subsection{*Classes and arities}
-\index{classes!context conditions}\index{arities!context conditions}
-
-In order to guarantee principal types~\cite{nipkow-prehofer},
-arity declarations must obey two conditions:
-\begin{itemize}
-\item There must not be any two declarations $ty :: (\vec{r})c$ and
- $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, this
- excludes the following:
-\begin{ttbox}
-arities
- foo :: (\{logic{\}}) logic
- foo :: (\{{\}})logic
-\end{ttbox}
-
-\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
- (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
- for $i=1,\dots,n$. The relationship $\preceq$, defined as
-\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
-expresses that the set of types represented by $s'$ is a subset of the
-set of types represented by $s$. Assuming $term \preceq logic$, the
-following is forbidden:
-\begin{ttbox}
-arities
- foo :: (\{logic{\}})logic
- foo :: (\{{\}})term
-\end{ttbox}
-
-\end{itemize}
-
+\index{theories|(}
\section{The theory loader}\label{sec:more-theories}
\index{theories!reading}\index{files!reading}
@@ -247,13 +37,6 @@
dispose a large number of theories at once. Note that {\ML} bindings to
theorems etc.\ of removed theories may still persist.
-\item[reset \ttindexbold{delete_tmpfiles};] processing theory files usually
- involves temporary {\ML} files to be created. By default, these are deleted
- afterwards. Resetting the \texttt{delete_tmpfiles} flag inhibits this,
- leaving the generated code for debugging purposes. The basic location for
- temporary files is determined by the \texttt{ISABELLE_TMP} environment
- variable (which is private to the running Isabelle process and may be
- retrieved by \ttindex{getenv} from {\ML}).
\end{ttdescription}
\medskip Theory and {\ML} files are located by skimming through the
@@ -296,224 +79,6 @@
temporarily appended to the load path, too.
-\section{Locales}
-\label{Locales}
-
-Locales \cite{kammueller-locales} are a concept of local proof contexts. They
-are introduced as named syntactic objects within theories and can be
-opened in any descendant theory.
-
-\subsection{Declaring Locales}
-
-A locale is declared in a theory section that starts with the
-keyword \texttt{locale}. It consists typically of three parts, the
-\texttt{fixes} part, the \texttt{assumes} part, and the \texttt{defines} part.
-Appendix \ref{app:TheorySyntax} presents the full syntax.
-
-\subsubsection{Parts of Locales}
-
-The subsection introduced by the keyword \texttt{fixes} declares the locale
-constants in a way that closely resembles a global \texttt{consts}
-declaration. In particular, there may be an optional pretty printing syntax
-for the locale constants.
-
-The subsequent \texttt{assumes} part specifies the locale rules. They are
-defined like \texttt{rules}: by an identifier followed by the rule
-given as a string. Locale rules admit the statement of local assumptions
-about the locale constants. The \texttt{assumes} part is optional. Non-fixed
-variables in locale rules are automatically bound by the universal quantifier
-\texttt{!!} of the meta-logic.
-
-Finally, the \texttt{defines} part introduces the definitions that are
-available in the locale. Locale constants declared in the \texttt{fixes}
-section are defined using the meta-equality \texttt{==}. If the
-locale constant is a functiond then its definition can (as usual) have
-variables on the left-hand side acting as formal parameters; they are
-considered as schematic variables and are automatically generalized by
-universal quantification of the meta-logic. The right hand side of a
-definition must not contain variables that are not already on the left hand
-side. In so far locale definitions behave like theory level definitions.
-However, the locale concept realizes \emph{dependent definitions}: any variable
-that is fixed as a locale constant can occur on the right hand side of
-definitions. For an illustration of these dependent definitions see the
-occurrence of the locale constant \texttt{G} on the right hand side of the
-definitions of the locale \texttt{group} below. Naturally, definitions can
-already use the syntax of the locale constants in the \texttt{fixes}
-subsection. The \texttt{defines} part is, as the \texttt{assumes} part,
-optional.
-
-\subsubsection{Example for Definition}
-The concrete syntax of locale definitions is demonstrated by example below.
-
-Locale \texttt{group} assumes the definition of groups in a theory
-file\footnote{This and other examples are from \texttt{HOL/ex}.}. A locale
-defining a convenient proof environment for group related proofs may be
-added to the theory as follows:
-\begin{ttbox}
- locale group =
- fixes
- G :: "'a grouptype"
- e :: "'a"
- binop :: "'a => 'a => 'a" (infixr "#" 80)
- inv :: "'a => 'a" ("i(_)" [90] 91)
- assumes
- Group_G "G: Group"
- defines
- e_def "e == unit G"
- binop_def "x # y == bin_op G x y"
- inv_def "i(x) == inverse G x"
-\end{ttbox}
-
-\subsubsection{Polymorphism}
-
-In contrast to polymorphic definitions in theories, the use of the
-same type variable for the declaration of different locale constants in the
-fixes part means \emph{the same} type. In other words, the scope of the
-polymorphic variables is extended over all constant declarations of a locale.
-In the above example \texttt{'a} refers to the same type which is fixed inside
-the locale. In an exported theorem (see \S\ref{sec:locale-export}) the
-constructors of locale \texttt{group} are polymorphic, yet only simultaneously
-instantiatable.
-
-\subsubsection{Nested Locales}
-
-A locale can be defined as the extension of a previously defined
-locale. This operation of extension is optional and is syntactically
-expressed as
-\begin{ttbox}
-locale foo = bar + ...
-\end{ttbox}
-The locale \texttt{foo} builds on the constants and syntax of the locale {\tt
-bar}. That is, all contents of the locale \texttt{bar} can be used in
-definitions and rules of the corresponding parts of the locale {\tt
-foo}. Although locale \texttt{foo} assumes the \texttt{fixes} part of \texttt{bar} it
-does not automatically subsume its rules and definitions. Normally, one
-expects to use locale \texttt{foo} only if locale \texttt{bar} is already
-active. These aspects of use and activation of locales are considered in the
-subsequent section.
-
-
-\subsection{Locale Scope}
-
-Locales are by default inactive, but they can be invoked. The list of
-currently active locales is called \emph{scope}. The process of activating
-them is called \emph{opening}; the reverse is \emph{closing}.
-
-\subsubsection{Scope}
-The locale scope is part of each theory. It is a dynamic stack containing
-all active locales at a certain point in an interactive session.
-The scope lives until all locales are explicitly closed. At one time there
-can be more than one locale open. The contents of these various active
-locales are all visible in the scope. In case of nested locales for example,
-the nesting is actually reflected to the scope, which contains the nested
-locales as layers. To check the state of the scope during a development the
-function \texttt{Print\_scope} may be used. It displays the names of all open
-locales on the scope. The function \texttt{print\_locales} applied to a theory
-displays all locales contained in that theory and in addition also the
-current scope.
-
-The scope is manipulated by the commands for opening and closing of locales.
-
-\subsubsection{Opening}
-Locales can be \emph{opened} at any point during a session where
-we want to prove theorems concerning the locale. Opening a locale means
-making its contents visible by pushing it onto the scope of the current
-theory. Inside a scope of opened locales, theorems can use all definitions and
-rules contained in the locales on the scope. The rules and definitions may
-be accessed individually using the function \ttindex{thm}. This function is
-applied to the names assigned to locale rules and definitions as
-strings. The opening command is called \texttt{Open\_locale} and takes the
-name of the locale to be opened as its argument.
-
-If one opens a locale \texttt{foo} that is defined by extension from locale
-\texttt{bar}, the function \texttt{Open\_locale} checks if locale \texttt{bar}
-is open. If so, then it just opens \texttt{foo}, if not, then it prints a
-message and opens \texttt{bar} before opening \texttt{foo}. Naturally, this
-carries on, if \texttt{bar} is again an extension.
-
-\subsubsection{Closing}
-
-\emph{Closing} means to cancel the last opened locale, pushing it out of the
-scope. Theorems proved during the life cycle of this locale will be disabled,
-unless they have been explicitly exported, as described below. However, when
-the same locale is opened again these theorems may be used again as well,
-provided that they were saved as theorems in the first place, using
-\texttt{qed} or ML assignment. The command \texttt{Close\_locale} takes a
-locale name as a string and checks if this locale is actually the topmost
-locale on the scope. If this is the case, it removes this locale, otherwise
-it prints a warning message and does not change the scope.
-
-\subsubsection{Export of Theorems}
-\label{sec:locale-export}
-
-Export of theorems transports theorems out of the scope of locales. Locale
-rules that have been used in the proof of an exported theorem inside the
-locale are carried by the exported form of the theorem as its individual
-meta-assumptions. The locale constants are universally quantified variables
-in these theorems, hence such theorems can be instantiated individually.
-Definitions become unfolded; locale constants that were merely used for
-definitions vanish. Logically, exporting corresponds to a combined
-application of introduction rules for implication and universal
-quantification. Exporting forms a kind of normalization of theorems in a
-locale scope.
-
-According to the possibility of nested locales there are two different forms
-of export. The first one is realized by the function \texttt{export} that
-exports theorems through all layers of opened locales of the scope. Hence,
-the application of export to a theorem yields a theorem of the global level,
-that is, the current theory context without any local assumptions or
-definitions.
-
-When locales are nested we might want to export a theorem, not to the global
-level of the current theory but just to the previous level. The other export
-function, \texttt{Export}, transports theorems one level up in the scope; the
-theorem still uses locale constants, definitions and rules of the locales
-underneath.
-
-\subsection{Functions for Locales}
-\label{Syntax}
-\index{locales!functions}
-
-Here is a quick reference list of locale functions.
-\begin{ttbox}
- Open_locale : xstring -> unit
- Close_locale : xstring -> unit
- export : thm -> thm
- Export : thm -> thm
- thm : xstring -> thm
- Print_scope : unit -> unit
- print_locales: theory -> unit
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{Open_locale} $xstring$]
- opens the locale {\it xstring}, adding it to the scope of the theory of the
- current context. If the opened locale is built by extension, the ancestors
- are opened automatically.
-
-\item[\ttindexbold{Close_locale} $xstring$] eliminates the locale {\it
- xstring} from the scope if it is the topmost item on it, otherwise it does
- not change the scope and produces a warning.
-
-\item[\ttindexbold{export} $thm$] locale definitions become expanded in {\it
- thm} and locale rules that were used in the proof of {\it thm} become part
- of its individual assumptions. This normalization happens with respect to
- \emph{all open locales} on the scope.
-
-\item[\ttindexbold{Export} $thm$] works like \texttt{export} but normalizes
- theorems only up to the previous level of locales on the scope.
-
-\item[\ttindexbold{thm} $xstring$] applied to the name of a locale definition
- or rule it returns the definition as a theorem.
-
-\item[\ttindexbold{Print_scope}()] prints the names of the locales in the
- current scope of the current theory context.
-
-\item[\ttindexbold{print_locale} $theory$] prints all locales that are
- contained in {\it theory} directly or indirectly. It also displays the
- current scope similar to \texttt{Print\_scope}.
-\end{ttdescription}
-
-
\section{Basic operations on theories}\label{BasicOperationsOnTheories}
\subsection{*Theory inclusion}
@@ -905,111 +470,6 @@
\end{ttdescription}
-\section{Oracles: calling trusted external reasoners}
-\label{sec:oracles}
-\index{oracles|(}
-
-Oracles allow Isabelle to take advantage of external reasoners such as
-arithmetic decision procedures, model checkers, fast tautology checkers or
-computer algebra systems. Invoked as an oracle, an external reasoner can
-create arbitrary Isabelle theorems. It is your responsibility to ensure that
-the external reasoner is as trustworthy as your application requires.
-Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem
-depends upon oracle calls.
-
-\begin{ttbox}
-invoke_oracle : theory -> xstring -> Sign.sg * object -> thm
-Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory
- -> theory
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)]
- invokes the oracle $name$ of theory $thy$ passing the information
- contained in the exception value $data$ and creating a theorem
- having signature $sign$. Note that type \ttindex{object} is just an
- abbreviation for \texttt{exn}. Errors arise if $thy$ does not have
- an oracle called $name$, if the oracle rejects its arguments or if
- its result is ill-typed.
-
-\item[\ttindexbold{Theory.add_oracle} $name$ $fun$ $thy$] extends
- $thy$ by oracle $fun$ called $name$. It is seldom called
- explicitly, as there is concrete syntax for oracles in theory files.
-\end{ttdescription}
-
-A curious feature of {\ML} exceptions is that they are ordinary constructors.
-The {\ML} type \texttt{exn} is a datatype that can be extended at any time. (See
-my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially
-page~136.) The oracle mechanism takes advantage of this to allow an oracle to
-take any information whatever.
-
-There must be some way of invoking the external reasoner from \ML, either
-because it is coded in {\ML} or via an operating system interface. Isabelle
-expects the {\ML} function to take two arguments: a signature and an
-exception object.
-\begin{itemize}
-\item The signature will typically be that of a desendant of the theory
- declaring the oracle. The oracle will use it to distinguish constants from
- variables, etc., and it will be attached to the generated theorems.
-
-\item The exception is used to pass arbitrary information to the oracle. This
- information must contain a full description of the problem to be solved by
- the external reasoner, including any additional information that might be
- required. The oracle may raise the exception to indicate that it cannot
- solve the specified problem.
-\end{itemize}
-
-A trivial example is provided in theory \texttt{FOL/ex/IffOracle}. This
-oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with
-an even number of $P$s.
-
-The \texttt{ML} section of \texttt{IffOracle.thy} begins by declaring
-a few auxiliary functions (suppressed below) for creating the
-tautologies. Then it declares a new exception constructor for the
-information required by the oracle: here, just an integer. It finally
-defines the oracle function itself.
-\begin{ttbox}
-exception IffOracleExn of int;\medskip
-fun mk_iff_oracle (sign, IffOracleExn n) =
- if n > 0 andalso n mod 2 = 0
- then Trueprop \$ mk_iff n
- else raise IffOracleExn n;
-\end{ttbox}
-Observe the function's two arguments, the signature \texttt{sign} and the
-exception given as a pattern. The function checks its argument for
-validity. If $n$ is positive and even then it creates a tautology
-containing $n$ occurrences of~$P$. Otherwise it signals error by
-raising its own exception (just by happy coincidence). Errors may be
-signalled by other means, such as returning the theorem \texttt{True}.
-Please ensure that the oracle's result is correctly typed; Isabelle
-will reject ill-typed theorems by raising a cryptic exception at top
-level.
-
-The \texttt{oracle} section of \texttt{IffOracle.thy} installs above
-\texttt{ML} function as follows:
-\begin{ttbox}
-IffOracle = FOL +\medskip
-oracle
- iff = mk_iff_oracle\medskip
-end
-\end{ttbox}
-
-Now in \texttt{IffOracle.ML} we first define a wrapper for invoking
-the oracle:
-\begin{ttbox}
-fun iff_oracle n = invoke_oracle IffOracle.thy "iff"
- (sign_of IffOracle.thy, IffOracleExn n);
-\end{ttbox}
-
-Here are some example applications of the \texttt{iff} oracle. An
-argument of 10 is allowed, but one of 5 is forbidden:
-\begin{ttbox}
-iff_oracle 10;
-{\out "P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P" : thm}
-iff_oracle 5;
-{\out Exception- IffOracleExn 5 raised}
-\end{ttbox}
-
-\index{oracles|)}
\index{theories|)}
--- a/doc-src/Ref/theory-syntax.tex Sun Mar 01 12:37:59 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,178 +0,0 @@
-%% $Id$
-
-\appendix
-\newlinechar=-1 %mathsing.sty sets \newlinechar=`\|, which would cause mayhem
-
-\chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
-
-Below we present the full syntax of theory definition files as provided by
-Pure Isabelle --- object-logics may add their own sections.
-\S\ref{sec:ref-defining-theories} explains the meanings of these constructs.
-The syntax obeys the following conventions:
-\begin{itemize}
-\item {\tt Typewriter font} denotes terminal symbols.
-
-\item $id$, $tid$, $nat$, $string$ and $longident$ are the lexical
- classes of identifiers, type identifiers, natural numbers, quoted
- strings (without the need for \verb$\$\dots\verb$\$ between lines)
- and long qualified \ML{} identifiers.
- The categories $id$, $tid$, $nat$ are fully defined in \iflabelundefined{Defining-Logics}%
- {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%
- {\S\ref{Defining-Logics}}.
-
-\item $text$ is all text from the current position to the end of file,
- $verbatim$ is any text enclosed in \verb.{|.\dots\verb.|}.
-
-\item Comments in theories take the form {\tt (*}\dots{\tt*)} and may
- be nested, just as in \ML.
-\end{itemize}
-
-\begin{rail}
-
-theoryDef : id '=' (name + '+') ('+' extension | ())
- ;
-
-name : id | string
- ;
-
-extension : (section +) 'end' ( () | ml )
- ;
-
-section : classes
- | default
- | types
- | arities
- | nonterminals
- | consts
- | syntax
- | trans
- | defs
- | constdefs
- | rules
- | axclass
- | instance
- | oracle
- | locale
- | local
- | global
- | setup
- ;
-
-classes : 'classes' ( classDecl + )
- ;
-
-classDecl : (id (() | '<' (id + ',')))
- ;
-
-default : 'default' sort
- ;
-
-sort : id
- | lbrace (id * ',') rbrace
- ;
-
-types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
- ;
-
-infix : ( 'infixr' | 'infixl' ) (() | string) nat
- ;
-
-typeDecl : typevarlist name
- ( () | '=' ( string | type ) );
-
-typevarlist : () | tid | '(' ( tid + ',' ) ')';
-
-type : simpleType | '(' type ')' | type '=>' type |
- '[' ( type + "," ) ']' '=>' type;
-
-simpleType: id | ( tid ( () | '::' id ) ) |
- '(' ( type + "," ) ')' id | simpleType id
- ;
-
-arities : 'arities' ((name + ',') '::' arity +)
- ;
-
-arity : ( () | '(' (sort + ',') ')' ) sort
- ;
-
-nonterminals : 'nonterminals' (name+)
- ;
-
-consts : 'consts' ( mixfixConstDecl + )
- ;
-
-syntax : 'syntax' (() | mode) ( mixfixConstDecl + );
-
-mode : '(' name (() | 'output') ')'
- ;
-
-mixfixConstDecl : constDecl (() | ( '(' mixfix ')' ))
- ;
-
-constDecl : ( name + ',') '::' (string | type);
-
-mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat )
- | infix
- | 'binder' string nat ;
-
-trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
- ;
-
-pat : ( () | ( '(' id ')' ) ) string;
-
-rules : 'rules' (( id string ) + )
- ;
-
-defs : 'defs' (( id string ) + )
- ;
-
-constdefs : 'constdefs' (name '::' (string | type) (() | mixfix) string +)
- ;
-
-axclass : 'axclass' classDecl (() | ( id string ) +)
- ;
-
-instance : 'instance' ( name '<' name | name '::' arity) witness
- ;
-
-witness : (() | '(' ((string | id | longident) + ',') ')') (() | verbatim)
- ;
-
-locale : 'locale' name '=' ( () | name '+' ) localeBody
- ;
-
-localeBody : localeConsts ( () | localeAsms ) ( () | localeDefs )
- ;
-
-localeConsts: ( 'fixes' ( ( (name '::' ( string | type )) ( () | '(' mixfix ')' ) ) + ) )
- ;
-
-
-localeAsms: ( 'assumes' ( ( id string ) + ) )
- ;
-
-localeDefs: ( 'defines' ( ( id string ) +) )
- ;
-
-oracle : 'oracle' name '=' name
- ;
-
-local : 'local'
- ;
-
-global : 'global'
- ;
-
-setup : 'setup' (id | longident)
- ;
-
-ml : 'ML' text
- ;
-
-\end{rail}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End:
--- a/doc-src/Ref/thm.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/thm.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,4 +1,4 @@
-%% $Id$
+
\chapter{Theorems and Forward Proof}
\index{theorems|(}
@@ -13,19 +13,6 @@
ignore such complexities --- and skip all but the first section of
this chapter.
-The theorem operations do not print error messages. Instead, they raise
-exception~\xdx{THM}\@. Use \ttindex{print_exn} to display
-exceptions nicely:
-\begin{ttbox}
-allI RS mp handle e => print_exn e;
-{\out Exception THM raised:}
-{\out RSN: no unifiers -- premise 1}
-{\out (!!x. ?P(x)) ==> ALL x. ?P(x)}
-{\out [| ?P --> ?Q; ?P |] ==> ?Q}
-{\out}
-{\out uncaught exception THM}
-\end{ttbox}
-
\section{Basic operations on theorems}
\subsection{Pretty-printing a theorem}