eliminated old "ref" manual;
authorwenzelm
Tue Jun 18 15:31:52 2013 +0200 (2013-06-18)
changeset 52415d9fed6e99a57
parent 52414 8429123bc58a
child 52416 383ffec6a548
eliminated old "ref" manual;
NEWS
doc/Contents
src/Doc/ROOT
src/Doc/Ref/abstract.txt
src/Doc/Ref/document/build
src/Doc/Ref/document/root.tex
src/Doc/Ref/undocumented.tex
src/HOL/Tools/reflection.ML
     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 -