# HG changeset patch # User wenzelm # Date 1371562312 -7200 # Node ID d9fed6e99a57cc98505ebeabf72ea11e96c7c369 # Parent 8429123bc58ab3b3bb671f2b9ad7fb8af93d1721 eliminated old "ref" manual; diff -r 8429123bc58a -r d9fed6e99a57 NEWS --- a/NEWS Tue Jun 18 15:15:36 2013 +0200 +++ b/NEWS Tue Jun 18 15:31:52 2013 +0200 @@ -29,6 +29,9 @@ * Discontinued redundant 'use' command, which was superseded by 'ML_file' in Isabelle2013. Minor INCOMPATIBILITY. +* Updated and extended "isar-ref" and "implementation" manual, +eliminated old "ref" manual. + *** Prover IDE -- Isabelle/Scala/jEdit *** diff -r 8429123bc58a -r d9fed6e99a57 doc/Contents --- a/doc/Contents Tue Jun 18 15:15:36 2013 +0200 +++ b/doc/Contents Tue Jun 18 15:31:52 2013 +0200 @@ -17,7 +17,6 @@ Old Manuals (outdated) intro Old Introduction to Isabelle - ref Old Isabelle Reference Manual logics Isabelle's Logics: overview and misc logics logics-HOL Isabelle's Logics: HOL logics-ZF Isabelle's Logics: FOL and ZF diff -r 8429123bc58a -r d9fed6e99a57 src/Doc/ROOT --- a/src/Doc/ROOT Tue Jun 18 15:15:36 2013 +0200 +++ b/src/Doc/ROOT Tue Jun 18 15:31:52 2013 +0200 @@ -245,19 +245,6 @@ "document/root.tex" "document/svmono.cls" -session Ref (doc) in "Ref" = Pure + - options [document_variants = "ref"] - theories - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../ttbox.sty" - "../manual.bib" - "document/build" - "document/root.tex" - session Sledgehammer (doc) in "Sledgehammer" = Pure + options [document_variants = "sledgehammer"] theories diff -r 8429123bc58a -r d9fed6e99a57 src/Doc/Ref/abstract.txt --- a/src/Doc/Ref/abstract.txt Tue Jun 18 15:15:36 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -Isabelle Reference Manual. Report 283 - -This manual is a comprehensive description of Isabelle, including all -commands, functions and packages. Functions are organized according to the -task they perform. In each section, basic functions appear before advanced -ones. The Index provides an alphabetical listing. It is intended as a -reference, not for casual reading. The manual assumes familiarity with the -basic concepts explained in Report 280, Introduction to Isabelle. diff -r 8429123bc58a -r d9fed6e99a57 src/Doc/Ref/document/build --- a/src/Doc/Ref/document/build Tue Jun 18 15:15:36 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -#!/bin/bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_TOOL" logo - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - diff -r 8429123bc58a -r d9fed6e99a57 src/Doc/Ref/document/root.tex --- a/src/Doc/Ref/document/root.tex Tue Jun 18 15:15:36 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,52 +0,0 @@ -\documentclass[12pt,a4paper]{report} -\usepackage{graphicx,iman,extra,ttbox,pdfsetup} - -\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Isabelle Reference Manual} - -\author{{\em Lawrence C. Paulson}\\ - Computer Laboratory \\ University of Cambridge \\ - \texttt{lcp@cl.cam.ac.uk}\\[3ex] - With Contributions by Tobias Nipkow and Markus Wenzel} - -\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} - -\pagestyle{headings} -\sloppy -\binperiod %%%treat . like a binary operator - -\begin{document} -\underscoreoff - -\index{definitions|see{rewriting, meta-level}} -\index{rewriting!object-level|see{simplification}} -\index{meta-rules|see{meta-rules}} - -\maketitle -\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 -\cite{isabelle-isar-ref,isabelle-implementation}. - -\subsubsection*{Acknowledgements} -Tobias Nipkow, of T. U. Munich, wrote most of - Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification}. - Markus Wenzel contributed to Chapter~\protect\ref{chap:syntax}. - Jeremy Dawson, Sara Kalvala, Martin - Simons and others suggested changes - and corrections. The research has been funded by the EPSRC (grants - GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT - (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG - Schwerpunktprogramm \emph{Deduktion}. - -\pagenumbering{roman} \tableofcontents \clearfirst - -%%seealso's must be last so that they appear last in the index entries -\index{meta-rewriting|seealso{tactics, theorems}} - -\begingroup - \bibliographystyle{plain} \small\raggedright\frenchspacing - \bibliography{manual} -\endgroup - -\end{document} diff -r 8429123bc58a -r d9fed6e99a57 src/Doc/Ref/undocumented.tex --- a/src/Doc/Ref/undocumented.tex Tue Jun 18 15:15:36 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,268 +0,0 @@ -%%%%Currently UNDOCUMENTED low-level functions! from previous manual - -%%%%Low level information about terms and module Logic. -%%%%Mainly used for implementation of Pure. - -%move to ML sources? - -\subsection{Basic declarations} -The implication symbol is {\tt implies}. - -The term \verb|all T| is the universal quantifier for type {\tt T}\@. - -The term \verb|equals T| is the equality predicate for type {\tt T}\@. - - -There are a number of basic functions on terms and types. - -\index{--->} -\beginprog -op ---> : typ list * typ -> typ -\endprog -Given types \([ \tau_1, \ldots, \tau_n]\) and \(\tau\), it -forms the type \(\tau_1\to \cdots \to (\tau_n\to\tau)\). - -Calling {\prog{}type_of \${t}}\index{type_of} computes the type of the -term~$t$. Raises exception {\tt TYPE} unless applications are well-typed. - - -Calling \verb|subst_bounds|$([u_{n-1},\ldots,u_0],\,t)$\index{subst_bounds} -substitutes the $u_i$ for loose bound variables in $t$. This achieves -\(\beta\)-reduction of \(u_{n-1} \cdots u_0\) into $t$, replacing {\tt -Bound~i} with $u_i$. For \((\lambda x y.t)(u,v)\), the bound variable -indices in $t$ are $x:1$ and $y:0$. The appropriate call is -\verb|subst_bounds([v,u],t)|. Loose bound variables $\geq n$ are reduced -by $n$ to compensate for the disappearance of $n$ lambdas. - -\index{maxidx_of_term} -\beginprog -maxidx_of_term: term -> int -\endprog -Computes the maximum index of all the {\tt Var}s in a term. -If there are no {\tt Var}s, the result is \(-1\). - -\index{term_match} -\beginprog -term_match: (term*term)list * term*term -> (term*term)list -\endprog -Calling \verb|term_match(vts,t,u)| instantiates {\tt Var}s in {\tt t} to -match it with {\tt u}. The resulting list of variable/term pairs extends -{\tt vts}, which is typically empty. First-order pattern matching is used -to implement meta-level rewriting. - - -\subsection{The representation of object-rules} -The module {\tt Logic} contains operations concerned with inference --- -especially, for constructing and destructing terms that represent -object-rules. - -\index{occs} -\beginprog -op occs: term*term -> bool -\endprog -Does one term occur in the other? -(This is a reflexive relation.) - -\index{add_term_vars} -\beginprog -add_term_vars: term*term list -> term list -\endprog -Accumulates the {\tt Var}s in the term, suppressing duplicates. -The second argument should be the list of {\tt Var}s found so far. - -\index{add_term_frees} -\beginprog -add_term_frees: term*term list -> term list -\endprog -Accumulates the {\tt Free}s in the term, suppressing duplicates. -The second argument should be the list of {\tt Free}s found so far. - -\index{mk_equals} -\beginprog -mk_equals: term*term -> term -\endprog -Given $t$ and $u$ makes the term $t\equiv u$. - -\index{dest_equals} -\beginprog -dest_equals: term -> term*term -\endprog -Given $t\equiv u$ returns the pair $(t,u)$. - -\index{list_implies:} -\beginprog -list_implies: term list * term -> term -\endprog -Given the pair $([\phi_1,\ldots, \phi_m], \phi)$ -makes the term \([\phi_1;\ldots; \phi_m] \Imp \phi\). - -\index{strip_imp_prems} -\beginprog -strip_imp_prems: term -> term list -\endprog -Given \([\phi_1;\ldots; \phi_m] \Imp \phi\) -returns the list \([\phi_1,\ldots, \phi_m]\). - -\index{strip_imp_concl} -\beginprog -strip_imp_concl: term -> term -\endprog -Given \([\phi_1;\ldots; \phi_m] \Imp \phi\) -returns the term \(\phi\). - -\index{list_equals} -\beginprog -list_equals: (term*term)list * term -> term -\endprog -For adding flex-flex constraints to an object-rule. -Given $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$, -makes the term \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\). - -\index{strip_equals} -\beginprog -strip_equals: term -> (term*term) list * term -\endprog -Given \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\), -returns $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$. - -\index{rule_of} -\beginprog -rule_of: (term*term)list * term list * term -> term -\endprog -Makes an object-rule: given the triple -\[ ([(t_1,u_1),\ldots, (t_k,u_k)], [\phi_1,\ldots, \phi_m], \phi) \] -returns the term -\([t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m]\Imp \phi\) - -\index{strip_horn} -\beginprog -strip_horn: term -> (term*term)list * term list * term -\endprog -Breaks an object-rule into its parts: given -\[ [t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m] \Imp \phi \] -returns the triple -\(([(t_k,u_k),\ldots, (t_1,u_1)], [\phi_1,\ldots, \phi_m], \phi).\) - -\index{strip_assums} -\beginprog -strip_assums: term -> (term*int) list * (string*typ) list * term -\endprog -Strips premises of a rule allowing a more general form, -where $\Forall$ and $\Imp$ may be intermixed. -This is typical of assumptions of a subgoal in natural deduction. -Returns additional information about the number, names, -and types of quantified variables. - - -\index{strip_prems} -\beginprog -strip_prems: int * term list * term -> term list * term -\endprog -For finding premise (or subgoal) $i$: given the triple -\( (i, [], \phi_1;\ldots \phi_i\Imp \phi) \) -it returns another triple, -\((\phi_i, [\phi_{i-1},\ldots, \phi_1], \phi)\), -where $\phi$ need not be atomic. Raises an exception if $i$ is out of -range. - - -\subsection{Environments} -The module {\tt Envir} (which is normally closed) -declares a type of environments. -An environment holds variable assignments -and the next index to use when generating a variable. -\par\indent\vbox{\small \begin{verbatim} - datatype env = Envir of {asol: term xolist, maxidx: int} -\end{verbatim}} -The operations of lookup, update, and generation of variables -are used during unification. - -\beginprog -empty: int->env -\endprog -Creates the environment with no assignments -and the given index. - -\beginprog -lookup: env * indexname -> term option -\endprog -Looks up a variable, specified by its indexname, -and returns {\tt None} or {\tt Some} as appropriate. - -\beginprog -update: (indexname * term) * env -> env -\endprog -Given a variable, term, and environment, -produces {\em a new environment\/} where the variable has been updated. -This has no side effect on the given environment. - -\beginprog -genvar: env * typ -> env * term -\endprog -Generates a variable of the given type and returns it, -paired with a new environment (with incremented {\tt maxidx} field). - -\beginprog -alist_of: env -> (indexname * term) list -\endprog -Converts an environment into an association list -containing the assignments. - -\beginprog -norm_term: env -> term -> term -\endprog - -Copies a term, -following assignments in the environment, -and performing all possible \(\beta\)-reductions. - -\beginprog -rewrite: (env * (term*term)list) -> term -> term -\endprog -Rewrites a term using the given term pairs as rewrite rules. Assignments -are ignored; the environment is used only with {\tt genvar}, to generate -unique {\tt Var}s as placeholders for bound variables. - - -\subsection{The unification functions} - - -\beginprog -unifiers: env * ((term*term)list) -> (env * (term*term)list) Seq.seq -\endprog -This is the main unification function. -Given an environment and a list of disagreement pairs, -it returns a sequence of outcomes. -Each outcome consists of an updated environment and -a list of flex-flex pairs (these are discussed below). - -\beginprog -smash_unifiers: env * (term*term)list -> env Seq.seq -\endprog -This unification function maps an environment and a list of disagreement -pairs to a sequence of updated environments. The function obliterates -flex-flex pairs by choosing the obvious unifier. It may be used to tidy up -any flex-flex pairs remaining at the end of a proof. - - -\subsubsection{Multiple unifiers} -The unification procedure performs Huet's {\sc match} operation -\cite{huet75} in big steps. -It solves \(\Var{f}(t_1,\ldots,t_p) \equiv u\) for \(\Var{f}\) by finding -all ways of copying \(u\), first trying projection on the arguments -\(t_i\). It never copies below any variable in \(u\); instead it returns a -new variable, resulting in a flex-flex disagreement pair. - - -\beginprog -type_assign: cterm -> cterm -\endprog -Produces a cterm by updating the signature of its argument -to include all variable/type assignments. -Type inference under the resulting signature will assume the -same type assignments as in the argument. -This is used in the goal package to give persistence to type assignments -within each proof. -(Contrast with {\sc lcf}'s sticky types \cite[page 148]{paulson-book}.) - -