author | wenzelm |

Sun Oct 31 15:20:35 1999 +0100 (1999-10-31) | |

changeset 7987 | d9aef93c0e32 |

parent 7986 | 9d319a76dbeb |

child 7988 | feea893b47c7 |

tuned;

1.1 --- a/doc-src/IsarRef/generic.tex Sat Oct 30 20:41:30 1999 +0200 1.2 +++ b/doc-src/IsarRef/generic.tex Sun Oct 31 15:20:35 1999 +0100 1.3 @@ -37,9 +37,9 @@ 1.4 becomes a (generalized) \emph{elimination}. 1.5 1.6 Note that the classical reasoner introduces another version of $rule$ that 1.7 - is able to pick appropriate rules automatically, whenever explicit $thms$ 1.8 - are omitted (see \S\ref{sec:classical-basic}); that method is the default 1.9 - for $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates 1.10 + is able to pick appropriate rules automatically, whenever $thms$ are omitted 1.11 + (see \S\ref{sec:classical-basic}); that method is the default for 1.12 + $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates 1.13 $\BY{default}$. 1.14 \item [$erule~thms$] is similar to $rule$, but applies rules by 1.15 elim-resolution. This is an improper method, mainly for experimentation and 1.16 @@ -47,11 +47,11 @@ 1.17 $rule$ (single step, involving facts) or $elim$ (repeated steps, see 1.18 \S\ref{sec:classical-basic}). 1.19 \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given 1.20 - meta-level definitions throughout all goals; any facts provided are 1.21 - \emph{ignored}. 1.22 -\item [$succeed$] yields a single (unchanged) result; it is the identify of 1.23 + meta-level definitions throughout all goals; any facts provided are inserted 1.24 + into the goal and subject to rewriting as well. 1.25 +\item [$succeed$] yields a single (unchanged) result; it is the identity of 1.26 the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}). 1.27 -\item [$fail$] yields an empty result sequence; it is the identify of the 1.28 +\item [$fail$] yields an empty result sequence; it is the identity of the 1.29 ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}). 1.30 \end{descr} 1.31 1.32 @@ -98,12 +98,12 @@ 1.33 result). 1.34 \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules. $OF$ applies 1.35 $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note 1.36 - the reversed order). Note that premises may be skipped by including $\_$ 1.37 - (underscore) as argument. 1.38 + the reversed order). Note that premises may be skipped by including 1.39 + ``$\_$'' (underscore) as argument. 1.40 1.41 $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$ 1.42 - that does not include the automatic lifting process that is normally 1.43 - intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}). 1.44 + that skips the automatic lifting process that is normally intended (cf.\ 1.45 + \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}). 1.46 1.47 \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named 1.48 instantiation, respectively. The terms given in $of$ are substituted for 1.49 @@ -180,9 +180,10 @@ 1.50 \item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as 1.51 $\ALSO$, and concludes the current calculational thread. The final result 1.52 is exhibited as fact for forward chaining towards the next goal. Basically, 1.53 - $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Typical proof 1.54 - idioms are``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and 1.55 - ``$\FINALLY~\HAVE{}{\phi}~\DOT$''. 1.56 + $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that 1.57 + ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and 1.58 + ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding 1.59 + calculational proofs. 1.60 1.61 \item [$trans$] maintains the set of transitivity rules of the theory or proof 1.62 context, by adding or deleting theorems (the default is to add). 1.63 @@ -204,12 +205,12 @@ 1.64 intro_classes & : & \isarmeth \\ 1.65 \end{matharray} 1.66 1.67 -Axiomatic type classes are provided by Isabelle/Pure as a purely 1.68 -\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}). Thus 1.69 -any object logic may make use of this light-weight mechanism for abstract 1.70 -theories. See \cite{Wenzel:1997:TPHOL} for more information. There is also a 1.71 -tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of 1.72 -the standard Isabelle documentation. 1.73 +Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional} 1.74 +interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic 1.75 +may make use of this light-weight mechanism of abstract theories. See 1.76 +\cite{Wenzel:1997:TPHOL} for more information. There is also a tutorial on 1.77 +\emph{Using Axiomatic Type Classes in Isabelle} that is part of the standard 1.78 +Isabelle documentation. 1.79 %FIXME cite 1.80 1.81 \begin{rail} 1.82 @@ -225,21 +226,22 @@ 1.83 holding. Class axioms may not contain more than one type variable. The 1.84 class axioms (with implicit sort constraints added) are bound to the given 1.85 names. Furthermore a class introduction rule is generated, which is 1.86 - employed by method $intro_classes$ in support instantiation proofs of this 1.87 + employed by method $intro_classes$ to support instantiation proofs of this 1.88 class. 1.89 1.90 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t :: 1.91 (\vec s)c$] setup up a goal stating the class relation or type arity. The 1.92 - proof would usually proceed by the $intro_classes$ method, and then 1.93 - establish the characteristic theorems of the type classes involved. After 1.94 - finishing the proof the theory will be augmented by a type signature 1.95 - declaration corresponding to the resulting theorem. 1.96 -\item [$intro_classes$] repeatedly expands the class introduction rules of 1.97 + proof would usually proceed by $intro_classes$, and then establish the 1.98 + characteristic theorems of the type classes involved. After finishing the 1.99 + proof, the theory will be augmented by a type signature declaration 1.100 + corresponding to the resulting theorem. 1.101 +\item [$intro_classes$] repeatedly expands all class introduction rules of 1.102 this theory. 1.103 \end{descr} 1.104 1.105 -See theory \texttt{HOL/Isar_examples/Group} for a simple example of using 1.106 -axiomatic type classes, including instantiation proofs. 1.107 +%FIXME 1.108 +%See theory \texttt{HOL/Isar_examples/Group} for a simple example of using 1.109 +%axiomatic type classes, including instantiation proofs. 1.110 1.111 1.112 \section{The Simplifier} 1.113 @@ -345,7 +347,7 @@ 1.114 given ones may be applied. The latter form admits better control of what 1.115 actually happens, thus it is very appropriate as an initial method for 1.116 $\PROOFNAME$ that splits up certain connectives of the goal, before entering 1.117 - the actual proof. 1.118 + the actual sub-proof. 1.119 1.120 \item [$contradiction$] solves some goal by contradiction, deriving any result 1.121 from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may 1.122 @@ -388,7 +390,10 @@ 1.123 1.124 Any of above methods support additional modifiers of the context of classical 1.125 rules. There semantics is analogous to the attributes given in 1.126 -\S\ref{sec:classical-mod}. 1.127 +\S\ref{sec:classical-mod}. Facts provided by forward chaining are inserted 1.128 +into the goal before doing the search. The ``!''~argument causes the full 1.129 +context of assumptions to be included as well.\footnote{This is slightly less 1.130 + hazardous than for the Simplifier (see \S\ref{sec:simp}).} 1.131 1.132 1.133 \subsection{Combined automated methods} 1.134 @@ -403,7 +408,7 @@ 1.135 ('force' | 'auto') ('!' ?) (clasimpmod * ) 1.136 ; 1.137 1.138 - clasimpmod: ('simp' ('add' | 'del' | 'only') | other | 1.139 + clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' | 1.140 (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs 1.141 \end{rail} 1.142 1.143 @@ -414,8 +419,13 @@ 1.144 modifier arguments correspond to those given in \S\ref{sec:simp} and 1.145 \S\ref{sec:classical-auto}. Just note that the ones related to the 1.146 Simplifier are prefixed by \railtoken{simp} here. 1.147 + 1.148 + Facts provided by forward chaining are inserted into the goal before doing 1.149 + the search. The ``!''~argument causes the full context of assumptions to be 1.150 + included as well. 1.151 \end{descr} 1.152 1.153 + 1.154 \subsection{Modifying the context}\label{sec:classical-mod} 1.155 1.156 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}

2.1 --- a/doc-src/IsarRef/hol.tex Sat Oct 30 20:41:30 1999 +0200 2.2 +++ b/doc-src/IsarRef/hol.tex Sun Oct 31 15:20:35 1999 +0100 2.3 @@ -146,8 +146,8 @@ 2.4 \end{descr} 2.5 2.6 See \cite{isabelle-HOL} for more information. Note that 2.7 -$\isarkeyword{inductive_cases}$ corresponds to the ML function 2.8 -\texttt{mk_cases}. 2.9 +$\isarkeyword{inductive_cases}$ corresponds to the \texttt{mk_cases} ML 2.10 +function. 2.11 2.12 2.13 \section{Proof by induction}

3.1 --- a/doc-src/IsarRef/intro.tex Sat Oct 30 20:41:30 1999 +0200 3.2 +++ b/doc-src/IsarRef/intro.tex Sun Oct 31 15:20:35 1999 +0100 3.3 @@ -149,7 +149,7 @@ 3.4 \end{tabular} 3.5 \end{center} 3.6 3.7 -See \texttt{HOL/Isar_examples} for a collection of introductory examples. 3.8 +See \texttt{HOL/Isar_examples} for a collection of introductory examples, and 3.9 \texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from 3.10 browsable HTML sources, both sessions provide actual documents (in PDF). 3.11

4.1 --- a/doc-src/IsarRef/pure.tex Sat Oct 30 20:41:30 1999 +0200 4.2 +++ b/doc-src/IsarRef/pure.tex Sun Oct 31 15:20:35 1999 +0100 4.3 @@ -370,10 +370,9 @@ 4.4 afterwards. Thus $text$ may actually change the theory as a side effect. 4.5 4.6 \item [$\isarkeyword{setup}~text$] changes the current theory context by 4.7 - applying setup functions from $text$, which refers to an ML expression of 4.8 - type $(theory \to theory)~list$. The $\isarkeyword{setup}$ command is the 4.9 - canonical way to initialize object-logic specific tools and packages written 4.10 - in ML. 4.11 + applying $text$, which refers to an ML expression of type $(theory \to 4.12 + theory)~list$. The $\isarkeyword{setup}$ command is the canonical way to 4.13 + initialize object-logic specific tools and packages written in ML. 4.14 \end{descr} 4.15 4.16 4.17 @@ -424,7 +423,7 @@ 4.18 4.19 \section{Proof commands} 4.20 4.21 -Proof commands provide transitions of Isar/VM machine configurations, which 4.22 +Proof commands perform transitions of Isar/VM machine configurations, which 4.23 are block-structured, consisting of a stack of nodes with three main 4.24 components: logical proof context, current facts, and open goals. Isar/VM 4.25 transitions are \emph{typed} according to the following three three different 4.26 @@ -434,16 +433,18 @@ 4.27 to be \emph{proven}; the next command may refine it by some proof method 4.28 (read: tactic), and enter a sub-proof to establish the actual result. 4.29 \item [$proof(state)$] is like an internal theory mode: the context may be 4.30 - augmented by \emph{stating} additional assumptions, intermediate result etc. 4.31 + augmented by \emph{stating} additional assumptions, intermediate results 4.32 + etc. 4.33 \item [$proof(chain)$] is intermediate between $proof(state)$ and 4.34 - $proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just 4.35 - picked up in order to be used when refining the goal claimed next. 4.36 + $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$'' 4.37 + register) have been just picked up in order to be used when refining the 4.38 + goal claimed next. 4.39 \end{descr} 4.40 4.41 4.42 \subsection{Proof markup commands}\label{sec:markup-prf} 4.43 4.44 -\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect} 4.45 +\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect} 4.46 \indexisarcmd{txt}\indexisarcmd{txt-raw} 4.47 \begin{matharray}{rcl} 4.48 \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\ 4.49 @@ -480,10 +481,10 @@ 4.50 former closely correspond to Skolem constants, or meta-level universal 4.51 quantification as provided by the Isabelle/Pure logical framework. 4.52 Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in 4.53 -a local object that may be used in the subsequent proof as any other variable 4.54 +a local value that may be used in the subsequent proof as any other variable 4.55 or constant. Furthermore, any result $\edrv \phi[x]$ exported from the 4.56 -current context will be universally closed wrt.\ $x$ at the outermost level: 4.57 -$\edrv \All x \phi$; this is expressed using Isabelle's meta-variables. 4.58 +context will be universally closed wrt.\ $x$ at the outermost level: $\edrv 4.59 +\All x \phi$ (this is expressed using Isabelle's meta-variables). 4.60 4.61 Similarly, introducing some assumption $\chi$ has two effects. On the one 4.62 hand, a local theorem is created that may be used as a fact in subsequent 4.63 @@ -497,9 +498,9 @@ 4.64 user. 4.65 4.66 Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by 4.67 -combining $\FIX x$ with another kind of assumption that causes any 4.68 -hypothetical equation $x \equiv t$ to be eliminated by reflexivity. Thus, 4.69 -exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$. 4.70 +combining $\FIX x$ with another version of assumption that causes any 4.71 +hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule. 4.72 +Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$. 4.73 4.74 \begin{rail} 4.75 'fix' (vars + 'and') comment? 4.76 @@ -530,7 +531,7 @@ 4.77 these concatenated. 4.78 \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition. 4.79 In results exported from the context, $x$ is replaced by $t$. Basically, 4.80 - $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$, with the 4.81 + $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the 4.82 resulting hypothetical equation solved by reflexivity. 4.83 4.84 The default name for the definitional equation is $x_def$. 4.85 @@ -554,7 +555,7 @@ 4.86 Any fact will usually be involved in further proofs, either as explicit 4.87 arguments of proof methods or when forward chaining towards the next goal via 4.88 $\THEN$ (and variants). Note that the special theorem name 4.89 -$this$.\indexisarthm{this} refers to the most recently established facts. 4.90 +$this$\indexisarthm{this} refers to the most recently established facts. 4.91 \begin{rail} 4.92 'note' thmdef? thmrefs comment? 4.93 ; 4.94 @@ -596,8 +597,8 @@ 4.95 \begin{matharray}{rcl} 4.96 \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\ 4.97 \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\ 4.98 - \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\ 4.99 - \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\ 4.100 + \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ 4.101 + \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ 4.102 \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ 4.103 \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ 4.104 \end{matharray} 4.105 @@ -605,7 +606,7 @@ 4.106 Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$ 4.107 and $\LEMMANAME$. New local goals may be claimed within proof mode as well. 4.108 Four variants are available, indicating whether the result is meant to solve 4.109 -some pending goal and whether forward chaining is employed. 4.110 +some pending goal or whether forward chaining is employed. 4.111 4.112 \begin{rail} 4.113 ('theorem' | 'lemma') goal 4.114 @@ -620,7 +621,7 @@ 4.115 \begin{descr} 4.116 \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal, 4.117 eventually resulting in some theorem $\turn \phi$ put back into the theory. 4.118 -\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as 4.119 +\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as 4.120 ``lemma''. 4.121 \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a 4.122 theorem with the current assumption context as hypotheses. 4.123 @@ -655,8 +656,8 @@ 4.124 goal to a number of sub-goals that are to be solved later. Facts are passed 4.125 to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode. 4.126 4.127 -\item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining goals 4.128 - completely. No facts are passed to $m@2$. 4.129 +\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve 4.130 + remaining goals. No facts are passed to $m@2$. 4.131 \end{enumerate} 4.132 4.133 The only other proper way to affect pending goals is by $\SHOWNAME$ (or 4.134 @@ -668,17 +669,19 @@ 4.135 or constitute some well-understood reduction to new sub-goals. Arbitrary 4.136 automatic proof tools that are prone leave a large number of badly structured 4.137 sub-goals are no help in continuing the proof document in any intelligible 4.138 -way. A much better technique would be to $\SHOWNAME$ some non-trivial 4.139 -reduction as an explicit rule, which is solved completely by some automated 4.140 -method, and then applied to some pending goal. 4.141 +way. 4.142 +%FIXME 4.143 +%A more appropriate technique would be to $\SHOWNAME$ some non-trivial 4.144 +%reduction as an explicit rule, which is solved completely by some automated 4.145 +%method, and then applied to some pending goal. 4.146 4.147 \medskip 4.148 4.149 Unless given explicitly by the user, the default initial method is 4.150 ``$default$'', which is usually set up to apply a single standard elimination 4.151 or introduction rule according to the topmost symbol involved. There is no 4.152 -separate default terminal method; in any case the final step is to solve all 4.153 -remaining goals by assumption, though. 4.154 +separate default terminal method. In any case, any goals left after that are 4.155 +solved by assumption as the very last step. 4.156 4.157 \begin{rail} 4.158 'proof' interest? meth? comment? 4.159 @@ -708,8 +711,8 @@ 4.160 $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing 4.161 some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$. 4.162 \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it 4.163 - abbreviates $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both 4.164 - methods. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done 4.165 + abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods, 4.166 + though. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done 4.167 by expanding its definition; in many cases $\PROOF{m@1}$ is already 4.168 sufficient to see what is going wrong. 4.169 \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it 4.170 @@ -717,12 +720,12 @@ 4.171 \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it 4.172 abbreviates $\BY{assumption}$. 4.173 \item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake}; 4.174 - provided that \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ 4.175 - pretends to solve the goal without further ado. Of course, the result is a 4.176 - fake theorem only, involving some oracle in its internal derivation object 4.177 - (this is indicated as ``$[!]$'' in the printed result). The main 4.178 - application of $\isarkeyword{sorry}$ is to support experimentation and 4.179 - top-down proof development. 4.180 + provided that the \texttt{quick_and_dirty} flag is enabled, 4.181 + $\isarkeyword{sorry}$ pretends to solve the goal without further ado. Of 4.182 + course, the result is a fake theorem only, involving some oracle in its 4.183 + internal derivation object (this is indicated as ``$[!]$'' in the printed 4.184 + result). The main application of $\isarkeyword{sorry}$ is to support 4.185 + experimentation and top-down proof development. 4.186 \end{descr} 4.187 4.188 4.189 @@ -772,13 +775,13 @@ 4.190 \end{matharray} 4.191 4.192 Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements, 4.193 -or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$ 4.194 -etc.) with a list of patterns $\ISS{p@1 \dots}{p@n}$. In both cases, 4.195 -higher-order matching is invoked to bind extra-logical term variables, which 4.196 -may be either named schematic variables of the form $\Var{x}$, or nameless 4.197 -dummies ``\texttt{_}'' (underscore).\indexisarvar{_@\texttt{_}} Note that in 4.198 -the $\LETNAME$ form the patterns occur on the left-hand side, while the 4.199 -$\ISNAME$ patterns are in postfix position. 4.200 +or by annotating assumptions or goal statements with a list of patterns 4.201 +$\ISS{p@1\;\dots}{p@n}$. In both cases, higher-order matching is invoked to 4.202 +bind extra-logical term variables, which may be either named schematic 4.203 +variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}'' 4.204 +(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the 4.205 +patterns occur on the left-hand side, while the $\ISNAME$ patterns are in 4.206 +postfix position. 4.207 4.208 Term abbreviations are quite different from actual local definitions as 4.209 introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are 4.210 @@ -807,7 +810,7 @@ 4.211 (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its 4.212 (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its 4.213 object-logical statement. The latter two abstract over any meta-level 4.214 -parameters bound by $\Forall$. 4.215 +parameters. 4.216 4.217 Fact statements resulting from assumptions or finished goals are bound as 4.218 $\Var{this_prop}$\indexisarvar{this-prop}, 4.219 @@ -816,7 +819,7 @@ 4.220 $\Var{this}$ refers to an object-logic statement that is an application 4.221 $f(t)$, then $t$ is bound to the special text variable 4.222 ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of 4.223 -this feature are calculational proofs (see \S\ref{sec:calculation}). 4.224 +the latter are calculational proofs (see \S\ref{sec:calculation}). 4.225 4.226 4.227 \subsection{Block structure} 4.228 @@ -834,8 +837,8 @@ 4.229 again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of 4.230 different context within a sub-proof may be switched via $\isarkeyword{next}$, 4.231 which is just a single block-close followed by block-open again. Thus the 4.232 -effect of $\isarkeyword{next}$ is a local reset the proof 4.233 -context.\footnote{There is no goal focus involved here!} 4.234 +effect of $\isarkeyword{next}$ to reset the local proof context. There is no 4.235 +goal focus involved here! 4.236 4.237 For slightly more advanced applications, there are explicit block parentheses 4.238 as well. These typically achieve a stronger forward style of reasoning. 4.239 @@ -887,8 +890,8 @@ 4.240 specifications are applied to a temporary context derived from the current 4.241 theory or proof; the result is discarded, i.e.\ attributes involved in 4.242 $thms$ do not have any permanent effect. 4.243 -\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-checks 4.244 - and print terms or propositions according to the current theory or proof 4.245 +\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-check and 4.246 + print terms or propositions according to the current theory or proof 4.247 context; the inferred type of $t$ is output as well. Note that these 4.248 commands are also useful in inspecting the current environment of term 4.249 abbreviations. 4.250 @@ -915,17 +918,16 @@ 4.251 process. 4.252 \item [$\isarkeyword{pwd}~$] prints the current working directory. 4.253 \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$, 4.254 - $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some 4.255 + $\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some 4.256 theory given as $name$ argument. These commands are basically the same as 4.257 - the corresponding ML functions\footnote{For historic reasons, the original 4.258 - ML versions also change the theory context to that of the theory loaded.} 4.259 - (see also \cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar 4.260 - versions may load new- and old-style theories alike. 4.261 + the corresponding ML functions\footnote{The ML versions also change the 4.262 + implicit theory context to that of the theory loaded.} (see also 4.263 + \cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar versions may 4.264 + load new- and old-style theories alike. 4.265 \end{descr} 4.266 4.267 -Note that these system commands are scarcely used when working with the 4.268 -Proof~General interface, since loading of theories is done fully 4.269 -transparently. 4.270 +These system commands are scarcely used when working with the Proof~General 4.271 +interface, since loading of theories is done fully transparently. 4.272 4.273 %%% Local Variables: 4.274 %%% mode: latex

5.1 --- a/doc-src/IsarRef/refcard.tex Sat Oct 30 20:41:30 1999 +0200 5.2 +++ b/doc-src/IsarRef/refcard.tex Sun Oct 31 15:20:35 1999 +0100 5.3 @@ -14,13 +14,13 @@ 5.4 $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\ 5.5 $\BG~\dots~\EN$ & declare explicit blocks \\ 5.6 $\isarcmd{next}$ & switch implicit blocks \\ 5.7 - $\NOTE{a}{a@1~\dots~a@n}$ & reconsider facts \\ 5.8 - $\LET{p = t}$ & \text{abbreviate terms by matching} \\ 5.9 + $\NOTE{a}{a@1\;\dots\;a@n}$ & reconsider facts \\ 5.10 + $\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\ 5.11 \end{tabular} 5.12 5.13 \begin{matharray}{rcl} 5.14 - theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\ 5.15 - & \Or & \LEMMA{name}{form}~proof \\ 5.16 + theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\ 5.17 + & \Or & \LEMMA{name}{prop}~proof \\ 5.18 & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex] 5.19 proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex] 5.20 stmt & = & \BG~stmt^*~\EN \\ 5.21 @@ -28,11 +28,11 @@ 5.22 & \Or & \NOTE{name}{name^+} \\ 5.23 & \Or & \LET{term = term} \\[0.5ex] 5.24 & \Or & \FIX{var^+} \\ 5.25 - & \Or & \ASSUME{name}{form^+}\\ 5.26 + & \Or & \ASSUME{name}{prop^+}\\ 5.27 & \Or & \THEN~goal{\dsh}stmt \\ 5.28 & \Or & goal{\dsh}stmt \\ 5.29 - goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\ 5.30 - & \Or & \SHOW{name}{form}~proof \\ 5.31 + goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\ 5.32 + & \Or & \SHOW{name}{prop}~proof \\ 5.33 \end{matharray} 5.34 5.35 5.36 @@ -44,8 +44,8 @@ 5.37 \DOT & \equiv & \BY{assumption} \\ 5.38 \HENCENAME & \equiv & \THEN~\HAVENAME \\ 5.39 \THUSNAME & \equiv & \THEN~\SHOWNAME \\ 5.40 - \FROM{a@1~\dots~a@n} & \equiv & \NOTE{this}{a@1~\dots~a@n}~\THEN \\ 5.41 - \WITH{a@1~\dots~a@n} & \equiv & \FROM{a@1~\dots~a@n~this} \\[1ex] 5.42 + \FROM{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\ 5.43 + \WITH{a@1\;\dots\;a@n} & \equiv & \FROM{a@1\;\dots\;a@n~this} \\[1ex] 5.44 \FROM{this} & \equiv & \THEN \\ 5.45 \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\ 5.46 \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\ 5.47 @@ -67,7 +67,7 @@ 5.48 \subsection{Diagnostic commands} 5.49 5.50 \begin{matharray}{ll} 5.51 - \isarcmd{thm}~a@1~\dots~a@n & \text{print theorems} \\ 5.52 + \isarcmd{thm}~a@1\;\dots\;a@n & \text{print theorems} \\ 5.53 \isarcmd{term}~t & \text{print term} \\ 5.54 \isarcmd{prop}~\phi & \text{print meta-level proposition} \\ 5.55 \isarcmd{typ}~\tau & \text{print meta-level type} \\ 5.56 @@ -78,22 +78,22 @@ 5.57 5.58 \begin{tabular}{ll} 5.59 \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex] 5.60 - $assumption$ & apply assumption \\ 5.61 - $rule~a@1~\dots~a@n$ & apply some rule \\ 5.62 + $assumption$ & apply some assumption \\ 5.63 + $rule~a@1\;\dots\;a@n$ & apply some rule \\ 5.64 $rule$ & apply standard rule (default for $\PROOFNAME$) \\ 5.65 $induct~x$ & apply induction rule \\ 5.66 - $contradiction$ & apply $\neg{}$ elimination rule \\[2ex] 5.67 + $contradiction$ & apply $\neg{}$ elimination rule (any order) \\[2ex] 5.68 5.69 \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex] 5.70 $-$ & \text{no rules} \\ 5.71 - $intro~a@1~\dots~a@n$ & \text{introduction rules} \\ 5.72 - $elim~a@1~\dots~a@n$ & \text{elimination rules} \\ 5.73 - $unfold~a@1~\dots~a@n$ & \text{definitions} \\[2ex] 5.74 + $intro~a@1\;\dots\;a@n$ & \text{introduction rules} \\ 5.75 + $elim~a@1\;\dots\;a@n$ & \text{elimination rules} \\ 5.76 + $unfold~a@1\;\dots\;a@n$ & \text{definitions} \\[2ex] 5.77 5.78 \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex] 5.79 $simp$ & Simplifier \\ 5.80 - $blast$, $fast$ & Classical reasoner \\ 5.81 - $force$, $auto$ & Simplifier + Classical reasoner \\ 5.82 + $blast$, $fast$ & Classical Reasoner \\ 5.83 + $force$, $auto$ & Simplifier + Classical Reasoner \\ 5.84 $arith$ & Arithmetic procedure \\ 5.85 \end{tabular} 5.86 5.87 @@ -102,8 +102,8 @@ 5.88 5.89 \begin{tabular}{ll} 5.90 \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex] 5.91 - $OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\ 5.92 - $of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\ 5.93 + $OF~a@1\;\dots\;a@n$ & apply rule to facts (skipping ``$_$'') \\ 5.94 + $of~t@1\;\dots\;t@n$ & apply rule to terms (skipping ``$_$'') \\ 5.95 $RS~b$ & resolve fact with rule \\ 5.96 $standard$ & put into standard result form \\ 5.97 $rulify$ & put into object-rule form \\ 5.98 @@ -111,12 +111,11 @@ 5.99 5.100 \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex] 5.101 $simp$ & declare Simplifier rules \\ 5.102 - $intro$, $elim$, $dest$ & declare Classical reasoner rules (also ``$!$'' or ``$!!$'') \\ 5.103 - $iff$ & declare Simplifier + Classical reasoner rules \\ 5.104 - $trans$ & calculational rules (general transitivity) \\ 5.105 + $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``$!$'' or ``$!!$'') \\ 5.106 + $iff$ & declare Simplifier + Classical Reasoner rules \\ 5.107 + $trans$ & declare calculational rules (general transitivity) \\ 5.108 \end{tabular} 5.109 5.110 - 5.111 %%% Local Variables: 5.112 %%% mode: latex 5.113 %%% TeX-master: "isar-ref"