1.1 --- a/NEWS Tue Jun 18 15:15:36 2013 +0200
1.2 +++ b/NEWS Tue Jun 18 15:31:52 2013 +0200
1.3 @@ -29,6 +29,9 @@
1.4 * Discontinued redundant 'use' command, which was superseded by
1.5 'ML_file' in Isabelle2013. Minor INCOMPATIBILITY.
1.6
1.7 +* Updated and extended "isar-ref" and "implementation" manual,
1.8 +eliminated old "ref" manual.
1.9 +
1.10
1.11 *** Prover IDE -- Isabelle/Scala/jEdit ***
1.12
2.1 --- a/doc/Contents Tue Jun 18 15:15:36 2013 +0200
2.2 +++ b/doc/Contents Tue Jun 18 15:31:52 2013 +0200
2.3 @@ -17,7 +17,6 @@
2.4
2.5 Old Manuals (outdated)
2.6 intro Old Introduction to Isabelle
2.7 - ref Old Isabelle Reference Manual
2.8 logics Isabelle's Logics: overview and misc logics
2.9 logics-HOL Isabelle's Logics: HOL
2.10 logics-ZF Isabelle's Logics: FOL and ZF
3.1 --- a/src/Doc/ROOT Tue Jun 18 15:15:36 2013 +0200
3.2 +++ b/src/Doc/ROOT Tue Jun 18 15:31:52 2013 +0200
3.3 @@ -245,19 +245,6 @@
3.4 "document/root.tex"
3.5 "document/svmono.cls"
3.6
3.7 -session Ref (doc) in "Ref" = Pure +
3.8 - options [document_variants = "ref"]
3.9 - theories
3.10 - files
3.11 - "../prepare_document"
3.12 - "../pdfsetup.sty"
3.13 - "../iman.sty"
3.14 - "../extra.sty"
3.15 - "../ttbox.sty"
3.16 - "../manual.bib"
3.17 - "document/build"
3.18 - "document/root.tex"
3.19 -
3.20 session Sledgehammer (doc) in "Sledgehammer" = Pure +
3.21 options [document_variants = "sledgehammer"]
3.22 theories
4.1 --- a/src/Doc/Ref/abstract.txt Tue Jun 18 15:15:36 2013 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,8 +0,0 @@
4.4 -Isabelle Reference Manual. Report 283
4.5 -
4.6 -This manual is a comprehensive description of Isabelle, including all
4.7 -commands, functions and packages. Functions are organized according to the
4.8 -task they perform. In each section, basic functions appear before advanced
4.9 -ones. The Index provides an alphabetical listing. It is intended as a
4.10 -reference, not for casual reading. The manual assumes familiarity with the
4.11 -basic concepts explained in Report 280, Introduction to Isabelle.
5.1 --- a/src/Doc/Ref/document/build Tue Jun 18 15:15:36 2013 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,16 +0,0 @@
5.4 -#!/bin/bash
5.5 -
5.6 -set -e
5.7 -
5.8 -FORMAT="$1"
5.9 -VARIANT="$2"
5.10 -
5.11 -"$ISABELLE_TOOL" logo
5.12 -
5.13 -cp "$ISABELLE_HOME/src/Doc/iman.sty" .
5.14 -cp "$ISABELLE_HOME/src/Doc/extra.sty" .
5.15 -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
5.16 -cp "$ISABELLE_HOME/src/Doc/manual.bib" .
5.17 -
5.18 -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
5.19 -
6.1 --- a/src/Doc/Ref/document/root.tex Tue Jun 18 15:15:36 2013 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,52 +0,0 @@
6.4 -\documentclass[12pt,a4paper]{report}
6.5 -\usepackage{graphicx,iman,extra,ttbox,pdfsetup}
6.6 -
6.7 -\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Isabelle Reference Manual}
6.8 -
6.9 -\author{{\em Lawrence C. Paulson}\\
6.10 - Computer Laboratory \\ University of Cambridge \\
6.11 - \texttt{lcp@cl.cam.ac.uk}\\[3ex]
6.12 - With Contributions by Tobias Nipkow and Markus Wenzel}
6.13 -
6.14 -\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
6.15 -
6.16 -\pagestyle{headings}
6.17 -\sloppy
6.18 -\binperiod %%%treat . like a binary operator
6.19 -
6.20 -\begin{document}
6.21 -\underscoreoff
6.22 -
6.23 -\index{definitions|see{rewriting, meta-level}}
6.24 -\index{rewriting!object-level|see{simplification}}
6.25 -\index{meta-rules|see{meta-rules}}
6.26 -
6.27 -\maketitle
6.28 -\emph{Note}: this document is part of the earlier Isabelle
6.29 -documentation and is mostly outdated. Fully obsolete parts of the
6.30 -original text have already been removed. The remaining material
6.31 -covers some aspects that did not make it into the newer manuals yet
6.32 -\cite{isabelle-isar-ref,isabelle-implementation}.
6.33 -
6.34 -\subsubsection*{Acknowledgements}
6.35 -Tobias Nipkow, of T. U. Munich, wrote most of
6.36 - Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification}.
6.37 - Markus Wenzel contributed to Chapter~\protect\ref{chap:syntax}.
6.38 - Jeremy Dawson, Sara Kalvala, Martin
6.39 - Simons and others suggested changes
6.40 - and corrections. The research has been funded by the EPSRC (grants
6.41 - GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
6.42 - (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
6.43 - Schwerpunktprogramm \emph{Deduktion}.
6.44 -
6.45 -\pagenumbering{roman} \tableofcontents \clearfirst
6.46 -
6.47 -%%seealso's must be last so that they appear last in the index entries
6.48 -\index{meta-rewriting|seealso{tactics, theorems}}
6.49 -
6.50 -\begingroup
6.51 - \bibliographystyle{plain} \small\raggedright\frenchspacing
6.52 - \bibliography{manual}
6.53 -\endgroup
6.54 -
6.55 -\end{document}
7.1 --- a/src/Doc/Ref/undocumented.tex Tue Jun 18 15:15:36 2013 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,268 +0,0 @@
7.4 -%%%%Currently UNDOCUMENTED low-level functions! from previous manual
7.5 -
7.6 -%%%%Low level information about terms and module Logic.
7.7 -%%%%Mainly used for implementation of Pure.
7.8 -
7.9 -%move to ML sources?
7.10 -
7.11 -\subsection{Basic declarations}
7.12 -The implication symbol is {\tt implies}.
7.13 -
7.14 -The term \verb|all T| is the universal quantifier for type {\tt T}\@.
7.15 -
7.16 -The term \verb|equals T| is the equality predicate for type {\tt T}\@.
7.17 -
7.18 -
7.19 -There are a number of basic functions on terms and types.
7.20 -
7.21 -\index{--->}
7.22 -\beginprog
7.23 -op ---> : typ list * typ -> typ
7.24 -\endprog
7.25 -Given types \([ \tau_1, \ldots, \tau_n]\) and \(\tau\), it
7.26 -forms the type \(\tau_1\to \cdots \to (\tau_n\to\tau)\).
7.27 -
7.28 -Calling {\prog{}type_of \${t}}\index{type_of} computes the type of the
7.29 -term~$t$. Raises exception {\tt TYPE} unless applications are well-typed.
7.30 -
7.31 -
7.32 -Calling \verb|subst_bounds|$([u_{n-1},\ldots,u_0],\,t)$\index{subst_bounds}
7.33 -substitutes the $u_i$ for loose bound variables in $t$. This achieves
7.34 -\(\beta\)-reduction of \(u_{n-1} \cdots u_0\) into $t$, replacing {\tt
7.35 -Bound~i} with $u_i$. For \((\lambda x y.t)(u,v)\), the bound variable
7.36 -indices in $t$ are $x:1$ and $y:0$. The appropriate call is
7.37 -\verb|subst_bounds([v,u],t)|. Loose bound variables $\geq n$ are reduced
7.38 -by $n$ to compensate for the disappearance of $n$ lambdas.
7.39 -
7.40 -\index{maxidx_of_term}
7.41 -\beginprog
7.42 -maxidx_of_term: term -> int
7.43 -\endprog
7.44 -Computes the maximum index of all the {\tt Var}s in a term.
7.45 -If there are no {\tt Var}s, the result is \(-1\).
7.46 -
7.47 -\index{term_match}
7.48 -\beginprog
7.49 -term_match: (term*term)list * term*term -> (term*term)list
7.50 -\endprog
7.51 -Calling \verb|term_match(vts,t,u)| instantiates {\tt Var}s in {\tt t} to
7.52 -match it with {\tt u}. The resulting list of variable/term pairs extends
7.53 -{\tt vts}, which is typically empty. First-order pattern matching is used
7.54 -to implement meta-level rewriting.
7.55 -
7.56 -
7.57 -\subsection{The representation of object-rules}
7.58 -The module {\tt Logic} contains operations concerned with inference ---
7.59 -especially, for constructing and destructing terms that represent
7.60 -object-rules.
7.61 -
7.62 -\index{occs}
7.63 -\beginprog
7.64 -op occs: term*term -> bool
7.65 -\endprog
7.66 -Does one term occur in the other?
7.67 -(This is a reflexive relation.)
7.68 -
7.69 -\index{add_term_vars}
7.70 -\beginprog
7.71 -add_term_vars: term*term list -> term list
7.72 -\endprog
7.73 -Accumulates the {\tt Var}s in the term, suppressing duplicates.
7.74 -The second argument should be the list of {\tt Var}s found so far.
7.75 -
7.76 -\index{add_term_frees}
7.77 -\beginprog
7.78 -add_term_frees: term*term list -> term list
7.79 -\endprog
7.80 -Accumulates the {\tt Free}s in the term, suppressing duplicates.
7.81 -The second argument should be the list of {\tt Free}s found so far.
7.82 -
7.83 -\index{mk_equals}
7.84 -\beginprog
7.85 -mk_equals: term*term -> term
7.86 -\endprog
7.87 -Given $t$ and $u$ makes the term $t\equiv u$.
7.88 -
7.89 -\index{dest_equals}
7.90 -\beginprog
7.91 -dest_equals: term -> term*term
7.92 -\endprog
7.93 -Given $t\equiv u$ returns the pair $(t,u)$.
7.94 -
7.95 -\index{list_implies:}
7.96 -\beginprog
7.97 -list_implies: term list * term -> term
7.98 -\endprog
7.99 -Given the pair $([\phi_1,\ldots, \phi_m], \phi)$
7.100 -makes the term \([\phi_1;\ldots; \phi_m] \Imp \phi\).
7.101 -
7.102 -\index{strip_imp_prems}
7.103 -\beginprog
7.104 -strip_imp_prems: term -> term list
7.105 -\endprog
7.106 -Given \([\phi_1;\ldots; \phi_m] \Imp \phi\)
7.107 -returns the list \([\phi_1,\ldots, \phi_m]\).
7.108 -
7.109 -\index{strip_imp_concl}
7.110 -\beginprog
7.111 -strip_imp_concl: term -> term
7.112 -\endprog
7.113 -Given \([\phi_1;\ldots; \phi_m] \Imp \phi\)
7.114 -returns the term \(\phi\).
7.115 -
7.116 -\index{list_equals}
7.117 -\beginprog
7.118 -list_equals: (term*term)list * term -> term
7.119 -\endprog
7.120 -For adding flex-flex constraints to an object-rule.
7.121 -Given $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$,
7.122 -makes the term \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\).
7.123 -
7.124 -\index{strip_equals}
7.125 -\beginprog
7.126 -strip_equals: term -> (term*term) list * term
7.127 -\endprog
7.128 -Given \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\),
7.129 -returns $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$.
7.130 -
7.131 -\index{rule_of}
7.132 -\beginprog
7.133 -rule_of: (term*term)list * term list * term -> term
7.134 -\endprog
7.135 -Makes an object-rule: given the triple
7.136 -\[ ([(t_1,u_1),\ldots, (t_k,u_k)], [\phi_1,\ldots, \phi_m], \phi) \]
7.137 -returns the term
7.138 -\([t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m]\Imp \phi\)
7.139 -
7.140 -\index{strip_horn}
7.141 -\beginprog
7.142 -strip_horn: term -> (term*term)list * term list * term
7.143 -\endprog
7.144 -Breaks an object-rule into its parts: given
7.145 -\[ [t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m] \Imp \phi \]
7.146 -returns the triple
7.147 -\(([(t_k,u_k),\ldots, (t_1,u_1)], [\phi_1,\ldots, \phi_m], \phi).\)
7.148 -
7.149 -\index{strip_assums}
7.150 -\beginprog
7.151 -strip_assums: term -> (term*int) list * (string*typ) list * term
7.152 -\endprog
7.153 -Strips premises of a rule allowing a more general form,
7.154 -where $\Forall$ and $\Imp$ may be intermixed.
7.155 -This is typical of assumptions of a subgoal in natural deduction.
7.156 -Returns additional information about the number, names,
7.157 -and types of quantified variables.
7.158 -
7.159 -
7.160 -\index{strip_prems}
7.161 -\beginprog
7.162 -strip_prems: int * term list * term -> term list * term
7.163 -\endprog
7.164 -For finding premise (or subgoal) $i$: given the triple
7.165 -\( (i, [], \phi_1;\ldots \phi_i\Imp \phi) \)
7.166 -it returns another triple,
7.167 -\((\phi_i, [\phi_{i-1},\ldots, \phi_1], \phi)\),
7.168 -where $\phi$ need not be atomic. Raises an exception if $i$ is out of
7.169 -range.
7.170 -
7.171 -
7.172 -\subsection{Environments}
7.173 -The module {\tt Envir} (which is normally closed)
7.174 -declares a type of environments.
7.175 -An environment holds variable assignments
7.176 -and the next index to use when generating a variable.
7.177 -\par\indent\vbox{\small \begin{verbatim}
7.178 - datatype env = Envir of {asol: term xolist, maxidx: int}
7.179 -\end{verbatim}}
7.180 -The operations of lookup, update, and generation of variables
7.181 -are used during unification.
7.182 -
7.183 -\beginprog
7.184 -empty: int->env
7.185 -\endprog
7.186 -Creates the environment with no assignments
7.187 -and the given index.
7.188 -
7.189 -\beginprog
7.190 -lookup: env * indexname -> term option
7.191 -\endprog
7.192 -Looks up a variable, specified by its indexname,
7.193 -and returns {\tt None} or {\tt Some} as appropriate.
7.194 -
7.195 -\beginprog
7.196 -update: (indexname * term) * env -> env
7.197 -\endprog
7.198 -Given a variable, term, and environment,
7.199 -produces {\em a new environment\/} where the variable has been updated.
7.200 -This has no side effect on the given environment.
7.201 -
7.202 -\beginprog
7.203 -genvar: env * typ -> env * term
7.204 -\endprog
7.205 -Generates a variable of the given type and returns it,
7.206 -paired with a new environment (with incremented {\tt maxidx} field).
7.207 -
7.208 -\beginprog
7.209 -alist_of: env -> (indexname * term) list
7.210 -\endprog
7.211 -Converts an environment into an association list
7.212 -containing the assignments.
7.213 -
7.214 -\beginprog
7.215 -norm_term: env -> term -> term
7.216 -\endprog
7.217 -
7.218 -Copies a term,
7.219 -following assignments in the environment,
7.220 -and performing all possible \(\beta\)-reductions.
7.221 -
7.222 -\beginprog
7.223 -rewrite: (env * (term*term)list) -> term -> term
7.224 -\endprog
7.225 -Rewrites a term using the given term pairs as rewrite rules. Assignments
7.226 -are ignored; the environment is used only with {\tt genvar}, to generate
7.227 -unique {\tt Var}s as placeholders for bound variables.
7.228 -
7.229 -
7.230 -\subsection{The unification functions}
7.231 -
7.232 -
7.233 -\beginprog
7.234 -unifiers: env * ((term*term)list) -> (env * (term*term)list) Seq.seq
7.235 -\endprog
7.236 -This is the main unification function.
7.237 -Given an environment and a list of disagreement pairs,
7.238 -it returns a sequence of outcomes.
7.239 -Each outcome consists of an updated environment and
7.240 -a list of flex-flex pairs (these are discussed below).
7.241 -
7.242 -\beginprog
7.243 -smash_unifiers: env * (term*term)list -> env Seq.seq
7.244 -\endprog
7.245 -This unification function maps an environment and a list of disagreement
7.246 -pairs to a sequence of updated environments. The function obliterates
7.247 -flex-flex pairs by choosing the obvious unifier. It may be used to tidy up
7.248 -any flex-flex pairs remaining at the end of a proof.
7.249 -
7.250 -
7.251 -\subsubsection{Multiple unifiers}
7.252 -The unification procedure performs Huet's {\sc match} operation
7.253 -\cite{huet75} in big steps.
7.254 -It solves \(\Var{f}(t_1,\ldots,t_p) \equiv u\) for \(\Var{f}\) by finding
7.255 -all ways of copying \(u\), first trying projection on the arguments
7.256 -\(t_i\). It never copies below any variable in \(u\); instead it returns a
7.257 -new variable, resulting in a flex-flex disagreement pair.
7.258 -
7.259 -
7.260 -\beginprog
7.261 -type_assign: cterm -> cterm
7.262 -\endprog
7.263 -Produces a cterm by updating the signature of its argument
7.264 -to include all variable/type assignments.
7.265 -Type inference under the resulting signature will assume the
7.266 -same type assignments as in the argument.
7.267 -This is used in the goal package to give persistence to type assignments
7.268 -within each proof.
7.269 -(Contrast with {\sc lcf}'s sticky types \cite[page 148]{paulson-book}.)
7.270 -
7.271 -