doc-src/IsarRef/generic.tex
changeset 7315 76a39a3784b5
parent 7175 8263d0b50e12
child 7319 3907d597cae6
     1.1 --- a/doc-src/IsarRef/generic.tex	Sun Aug 22 18:21:36 1999 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sun Aug 22 21:13:20 1999 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  
     1.5  \chapter{Generic Tools and Packages}\label{ch:gen-tools}
     1.6  
     1.7 -\section{Basic proof methods and attributes}\label{sec:pure-meth}
     1.8 +\section{Basic proof methods}\label{sec:pure-meth}
     1.9  
    1.10  \indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
    1.11  \indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
    1.12 @@ -33,6 +33,9 @@
    1.13  %FIXME thmref (single)
    1.14  %FIXME var vs. term
    1.15  
    1.16 +
    1.17 +\section{Miscellaneous attributes}
    1.18 +
    1.19  \indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
    1.20  \indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
    1.21  \indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
    1.22 @@ -78,6 +81,73 @@
    1.23  
    1.24  FIXME
    1.25  
    1.26 +
    1.27 +\section{Calculational proof}\label{sec:calculation}
    1.28 +
    1.29 +\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}
    1.30 +\begin{matharray}{rcl}
    1.31 +  \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
    1.32 +  \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
    1.33 +  trans & : & \isaratt \\
    1.34 +\end{matharray}
    1.35 +
    1.36 +Calculational proof is forward reasoning with implicit application of
    1.37 +transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
    1.38 +an auxiliary register $calculation$\indexisarreg{calculation} for accumulating
    1.39 +results obtained by transitivity obtained together with the current facts.
    1.40 +Command $\ALSO$ updates $calculation$ from the most recent result, while
    1.41 +$\FINALLY$ exhibits the final result by forward chaining towards the next goal
    1.42 +statement.  Both commands require valid current facts, i.e.\ may occur only
    1.43 +after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or
    1.44 +some finished $\HAVENAME$ or $\SHOWNAME$.
    1.45 +
    1.46 +Also note that the automatic term abbreviation ``$\dots$'' has its canonical
    1.47 +application with calculational proofs.  It automatically refers to the
    1.48 +argument\footnote{The argument of a curried infix expression is its right-hand
    1.49 +  side.} of the preceding statement.
    1.50 +
    1.51 +Isabelle/Isar calculations are implicitly subject to block structure in the
    1.52 +sense that new threads of calculational reasoning are commenced for any new
    1.53 +block (as opened by a local goal, for example).  This means that, apart from
    1.54 +being able to nest calculations, there is no separate \emph{begin-calculation}
    1.55 +command required.
    1.56 +
    1.57 +\begin{rail}
    1.58 +  ('also' | 'finally') transrules? comment?
    1.59 +  ;
    1.60 +  'trans' (() | 'add' ':' | 'del' ':') thmrefs
    1.61 +  ;
    1.62 +
    1.63 +  transrules: '(' thmrefs ')' interest?
    1.64 +  ;
    1.65 +\end{rail}
    1.66 +
    1.67 +\begin{descr}
    1.68 +\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
    1.69 +  follows.  The first occurrence of $\ALSO$ in some calculational thread
    1.70 +  initialises $calculation$ by $facts$. Any subsequent $\ALSO$ on the
    1.71 +  \emph{same} level of block-structure updates $calculation$ by some
    1.72 +  transitivity rule applied to $calculation$ and $facts$ (in that order).
    1.73 +  Transitivity rules are picked from the current context plus those given as
    1.74 +  $thms$ (the latter have precedence).
    1.75 +  
    1.76 +\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
    1.77 +  $\ALSO$, and concludes the current calculational thread.  The final result
    1.78 +  is exhibited as fact for forward chaining towards the next goal. Basically,
    1.79 +  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  A typical proof
    1.80 +  idiom is $\FINALLY~\SHOW~\VVar{thesis}~\DOT$.
    1.81 +  
    1.82 +\item [Attribute $trans$] maintains the set of transitivity rules of the
    1.83 +  theory or proof context, by adding or deleting the theorems provided as
    1.84 +  arguments.  The default is adding of rules.
    1.85 +\end{descr}
    1.86 +
    1.87 +See theory \texttt{HOL/Isar_examples/Group} for a simple applications of
    1.88 +calculations for basic equational reasoning.
    1.89 +\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
    1.90 +calculational steps in combination with natural deduction.
    1.91 +
    1.92 +
    1.93  \section{Axiomatic Type Classes}\label{sec:axclass}
    1.94  
    1.95  \indexisarcmd{axclass}\indexisarcmd{instance}
    1.96 @@ -114,8 +184,48 @@
    1.97  
    1.98  \section{The Simplifier}
    1.99  
   1.100 +\subsection{Simplification methods}
   1.101 +
   1.102 +\indexisarmeth{simp}\indexisarmeth{asm_simp}\indexisaratt{simp}
   1.103 +\begin{matharray}{rcl}
   1.104 +  simp & : & \isarmeth \\
   1.105 +  asm_simp & : & \isarmeth \\
   1.106 +  simp & : & \isaratt \\
   1.107 +\end{matharray}
   1.108 +
   1.109 +\begin{rail}
   1.110 +  'simp' (simpmod+)?
   1.111 +  ;
   1.112 +
   1.113 +  simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
   1.114 +  ;
   1.115 +\end{rail}
   1.116 +
   1.117 +
   1.118 +\subsection{Forward simplification}
   1.119 +
   1.120 +\indexisaratt{simplify}\indexisaratt{asm_simplify}\indexisaratt{full_simplify}\indexisaratt{asm_full_simplify}
   1.121 +\begin{matharray}{rcl}
   1.122 +  simplify & : & \isaratt \\
   1.123 +  asm_simplify & : & \isaratt \\
   1.124 +  full_simplify & : & \isaratt \\
   1.125 +  asm_full_simplify & : & \isaratt \\
   1.126 +\end{matharray}
   1.127 +
   1.128 +FIXME
   1.129 +
   1.130 +
   1.131  \section{The Classical Reasoner}
   1.132  
   1.133 +\subsection{Single step methods}
   1.134 +
   1.135 +\subsection{Automatic methods}
   1.136 +
   1.137 +\subsection{Combined automatic methods}
   1.138 +
   1.139 +\subsection{Modifying the context}
   1.140 +
   1.141 +
   1.142  
   1.143  %\indexisarcmd{}
   1.144  %\begin{matharray}{rcl}