# HG changeset patch # User wenzelm # Date 1015539679 -3600 # Node ID d8a345d9e067858b750d662f1e9a11a19fce54f6 # Parent 6faccf7d0f25c289eab6c5cdc8c2a7300d97a328 tuned; diff -r 6faccf7d0f25 -r d8a345d9e067 ANNOUNCE --- a/ANNOUNCE Thu Mar 07 22:52:07 2002 +0100 +++ b/ANNOUNCE Thu Mar 07 23:21:19 2002 +0100 @@ -18,7 +18,7 @@ Isabelle2002 is the official version to go along with that book (by Tobias Nipkow, Larry Paulson, Markus Wenzel). - * Pure: explicit proof terms for all internal inferences: + * Pure: explicit proof terms for all internal inferences; object-logics, proof tools etc. will benefit automatically (by Stefan Berghofer). @@ -27,28 +27,30 @@ operations, and type-inference for structured specifications (by Markus Wenzel). - * Pure/Isar: streamlined induction proof patterns + * Pure/Isar: streamlined cases/induction proof patterns (by Markus Wenzel). * Pure/HOL: infrastructure for generating functional and relational - code, using the ML run-time environment (by Stefan Berghofer). + code, using the ML run-time environment + (by Stefan Berghofer). - * HOL/library: numerals on all number types; several - improvements of tuple and record types; new definite description - operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories. + * HOL/library: numerals on all number types; several improvements of + tuple and record types; new definite description operator; keep + Hilbert's epsilon (Axiom of Choice) out of basic theories + (by Stefan Berghofer, Larry Paulson, Markus Wenzel). * HOL/Bali: large application concerning formal treatment of Java. (by David von Oheimb and Norbert Schirmer). * HOL/HoareParallel: large application concerning verification of parallel imperative programs (Owicki-Gries method, Rely-Guarantee - method, examples of garbage collection, mutual exclusion, etc.) + method, examples of garbage collection, mutual exclusion) (by Leonor Prensa Nieto). * HOL/GroupTheory: group theory examples including Sylow's theorem - (by Florian Kammüller). + (by Florian Kammueller). - * HOL/IMP: new proofs in Isar format + * HOL/IMP: several new proofs in Isar format (by Gerwin Klein). * HOL/MicroJava: exception handling on the bytecode level @@ -61,10 +63,8 @@ (by Markus Wenzel). * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting - larger heap size of applications. - - * System: support for MacOS X (for Poly/ML and SML/NJ). - + larger heap size of applications; support for MacOS X (Poly/ML and + SML/NJ). You may get Isabelle2002 from any of the following mirror sites: diff -r 6faccf7d0f25 -r d8a345d9e067 NEWS --- a/NEWS Thu Mar 07 22:52:07 2002 +0100 +++ b/NEWS Thu Mar 07 23:21:19 2002 +0100 @@ -210,7 +210,7 @@ - remove all special provisions on numerals in proofs; -* HOL: simp rules nat_number_of expand numerals on nat to Suc/0 +* HOL: simp rules nat_number expand numerals on nat to Suc/0 representation (depends on bin_arith_simps in the default context); * HOL: symbolic syntax for x^2 (numeral 2); diff -r 6faccf7d0f25 -r d8a345d9e067 doc-src/IsarRef/conversion.tex --- a/doc-src/IsarRef/conversion.tex Thu Mar 07 22:52:07 2002 +0100 +++ b/doc-src/IsarRef/conversion.tex Thu Mar 07 23:21:19 2002 +0100 @@ -188,7 +188,7 @@ This may be replaced by using the $unfold$ proof method explicitly. \begin{matharray}{l} \LEMMA{name}{\texttt"{\phi}\texttt"} \\ -\quad \APPLY{unfold~def@1~\dots} \\ +\quad \APPLY{(unfold~def@1~\dots)} \\ \end{matharray} @@ -224,7 +224,7 @@ $simp$, $blast$, or $auto$. This could work as follows: \begin{matharray}{l} \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\ - \quad \BYY{unfold~defs}{blast} \\ + \quad \BYY{(unfold~defs)}{blast} \\ \end{matharray} Note that classic Isabelle would support this form only in the special case where $\phi@1$, \dots are atomic statements (when using the standard @@ -265,7 +265,7 @@ \begin{matharray}{l} \LEMMA{name}{\texttt"{\All{\vec x}\vec\phi \Imp \psi}\texttt"} \\ - \quad \APPLY{atomize~(full)} \\ + \quad \APPLY{(atomize~(full))} \\ \quad \APPLY{meth@1} \\ \qquad \vdots \\ \quad \DONE \\ diff -r 6faccf7d0f25 -r d8a345d9e067 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Thu Mar 07 22:52:07 2002 +0100 +++ b/doc-src/IsarRef/generic.tex Thu Mar 07 23:21:19 2002 +0100 @@ -230,8 +230,8 @@ \quad \PROOF{succeed} \\ \qquad \FIX{thesis} \\ \qquad \ASSUME{that~[intro?]}{\All{\vec x} \vec\phi \Imp thesis} \\ - \qquad \SHOW{}{thesis} \\ - \quad\qquad \APPLY{insert~that} \\ + \qquad \THUS{}{thesis} \\ + \quad\qquad \APPLY{-} \\ \quad\qquad \USING{\vec b}~~\langle proof\rangle \\ \quad \QED{} \\ \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\ diff -r 6faccf7d0f25 -r d8a345d9e067 doc-src/IsarRef/logics.tex --- a/doc-src/IsarRef/logics.tex Thu Mar 07 22:52:07 2002 +0100 +++ b/doc-src/IsarRef/logics.tex Thu Mar 07 23:21:19 2002 +0100 @@ -228,18 +228,16 @@ \medskip In Isabelle/HOL record types have to be defined explicitly, fixing their field -names and types, and their (optional) parent record (see -{\S}\ref{sec:hol-record-def}). Afterwards, records may be formed using above -syntax, while obeying the canonical order of fields as given by their -declaration. The record package provides several standard operations like -selectors and updates (see {\S}\ref{sec:hol-record-ops}). The common setup -for various generic proof tools enable succinct reasoning patterns (see -{\S}\ref{sec:hol-record-thms}). See also the Isabelle/HOL tutorial -\cite{isabelle-hol-book} for further instructions on using records in +names and types, and their (optional) parent record. Afterwards, records may +be formed using above syntax, while obeying the canonical order of fields as +given by their declaration. The record package provides several standard +operations like selectors and updates. The common setup for various generic +proof tools enable succinct reasoning patterns. See also the Isabelle/HOL +tutorial \cite{isabelle-hol-book} for further instructions on using records in practice. -\subsubsection{Record specifications}\label{sec:hol-record-def} +\subsubsection{Record specifications} \indexisarcmdof{HOL}{record} \begin{matharray}{rcl} @@ -275,7 +273,7 @@ \end{descr} -\subsubsection{Record operations}\label{sec:hol-record-ops} +\subsubsection{Record operations} Any record definition of the form presented above produces certain standard operations. Selectors and updates are provided for any field, including the @@ -343,7 +341,7 @@ \noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ actually coincide for root records. -\subsubsection{Derived rules and proof tools}\label{sec:hol-record-thms} +\subsubsection{Derived rules and proof tools} The record package proves several results internally, declaring these facts to appropriate proof tools. This enables users to reason about record structures @@ -425,9 +423,8 @@ old-style theory syntax being used there! Apart from proper proof methods for case-analysis and induction, there are also emulations of ML tactics \texttt{case_tac} and \texttt{induct_tac} available, see -\S\ref{sec:hol-induct-tac} or \S\ref{sec:zf-induct-tac}; these admit to refer -directly to the internal structure of subgoals (including internally bound -parameters). +\S\ref{sec:hol-induct-tac}; these admit to refer directly to the internal +structure of subgoals (including internally bound parameters). \subsection{Recursive functions}\label{sec:recursion} @@ -858,7 +855,7 @@ \end{rail} -\subsubsection{Cases and induction: emulating tactic scripts}\label{sec:zf-induct-tac} +\subsubsection{Cases and induction: emulating tactic scripts} The following important tactical tools of Isabelle/ZF have been ported to Isar. These should be never used in proper proof texts! diff -r 6faccf7d0f25 -r d8a345d9e067 doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Thu Mar 07 22:52:07 2002 +0100 +++ b/doc-src/IsarRef/pure.tex Thu Mar 07 23:21:19 2002 +0100 @@ -1194,6 +1194,7 @@ \end{rail} \begin{descr} + \item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike $\PROOFNAME$ it retains ``$proof(prove)$'' mode. Thus consecutive method applications may be given just as in tactic scripts. @@ -1229,6 +1230,7 @@ $\isarkeyword{lemmas}$ (cf.\ \S\ref{sec:axms-thms}), so $\isarkeyword{declare}$ only has the effect of applying attributes as included in the theorem specification. + \end{descr} Any proper Isar proof method may be used with tactic script commands such as diff -r 6faccf7d0f25 -r d8a345d9e067 doc-src/isar.sty --- a/doc-src/isar.sty Thu Mar 07 22:52:07 2002 +0100 +++ b/doc-src/isar.sty Thu Mar 07 23:21:19 2002 +0100 @@ -30,7 +30,7 @@ \newcommand{\isaratt}{attribute} \newcommand{\I@optname}[1]{\ifthenelse{\equal{}{#1}}{}{~#1\colon}} -\newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~(#1)}} +\newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~#1}} \newcommand{\AND}{\isarkeyword{and}} \newcommand{\IN}{\isarkeyword{in}}