# HG changeset patch # User wenzelm # Date 941208535 -7200 # Node ID 34245feb6e82ff4533457fafbdc88c9547d950e4 # Parent 0d801c6e4dc0caaa4fe7c9c1d2972e1238838fd2 improved; diff -r 0d801c6e4dc0 -r 34245feb6e82 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Fri Oct 29 12:49:50 1999 +0200 +++ b/doc-src/IsarRef/generic.tex Fri Oct 29 16:48:55 1999 +0200 @@ -317,7 +317,8 @@ \subsection{Basic methods}\label{sec:classical-basic} -\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction} +\indexisarmeth{rule}\indexisarmeth{intro} +\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} \begin{matharray}{rcl} rule & : & \isarmeth \\ intro & : & \isarmeth \\ diff -r 0d801c6e4dc0 -r 34245feb6e82 doc-src/IsarRef/isar-ref.tex --- a/doc-src/IsarRef/isar-ref.tex Fri Oct 29 12:49:50 1999 +0200 +++ b/doc-src/IsarRef/isar-ref.tex Fri Oct 29 16:48:55 1999 +0200 @@ -2,7 +2,7 @@ %% $Id$ \documentclass[12pt,a4paper,fleqn]{report} -\usepackage{graphicx,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup} +\usepackage{latexsym,graphicx,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup} \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual} \author{\emph{Markus Wenzel} \\ TU M\"unchen} @@ -22,6 +22,7 @@ \newcommand{\drv}{\mathrel{\vdash}} \newcommand{\edrv}{\mathop{\drv}\nolimits} +\newcommand{\Or}{\mathrel{\;|\;}} \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} @@ -32,7 +33,7 @@ \renewcommand{\phi}{\varphi} -%\includeonly{pure} +%\includeonly{refcard} diff -r 0d801c6e4dc0 -r 34245feb6e82 doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Fri Oct 29 12:49:50 1999 +0200 +++ b/doc-src/IsarRef/pure.tex Fri Oct 29 16:48:55 1999 +0200 @@ -823,8 +823,8 @@ \indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}} \begin{matharray}{rcl} \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\ + \BG & : & \isartrans{proof(state)}{proof(state)} \\ + \EN & : & \isartrans{proof(state)}{proof(state)} \\ \end{matharray} While Isar is inherently block-structured, opening and closing blocks is @@ -857,12 +857,12 @@ \subsection{Diagnostics} -\indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm} +\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ} \begin{matharray}{rcl} - \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\ + \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\ \isarcmd{term} & : & \isarkeep{theory~|~proof} \\ \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\ - \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\ + \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\ \end{matharray} These commands are not part of the actual Isabelle/Isar syntax, but assist @@ -870,29 +870,29 @@ theory or proof configuration is not changed. \begin{rail} - 'typ' type + 'thm' thmrefs ; 'term' term ; 'prop' prop ; - 'thm' thmrefs + 'typ' type ; \end{rail} \begin{descr} -\item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic - according to the current theory or proof context. +\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current + theory or proof context. Note that any attributes included in the theorem + specifications are applied to a temporary context derived from the current + theory or proof; the result is discarded, i.e.\ attributes involved in + $thms$ do not have any permanent effect. \item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-checks and print terms or propositions according to the current theory or proof context; the inferred type of $t$ is output as well. Note that these commands are also useful in inspecting the current environment of term abbreviations. -\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current - theory or proof context. Note that any attributes included in the theorem - specifications are applied to a temporary context derived from the current - theory or proof; the result is discarded, i.e.\ attributes involved in - $thms$ do not have any permanent effect. +\item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic + according to the current theory or proof context. \end{descr} diff -r 0d801c6e4dc0 -r 34245feb6e82 doc-src/IsarRef/refcard.tex --- a/doc-src/IsarRef/refcard.tex Fri Oct 29 12:49:50 1999 +0200 +++ b/doc-src/IsarRef/refcard.tex Fri Oct 29 16:48:55 1999 +0200 @@ -1,6 +1,120 @@ \chapter{Isabelle/Isar Quick Reference} +\section{Proof commands} + +\subsection{Primitives and basic syntax} + +\begin{tabular}{ll} + $\FIX{x}$ & augment context by $\All x \Box$ \\ + $\ASSUME{a}{\phi}$ & augment context by $\phi \Imp \Box$ \\ + $\THEN$ & indicate forward chaining \\ + $\HAVE{a}{\phi}$ & prove local result \\ + $\SHOW{a}{\phi}$ & prove local result, establishing some goal \\ + $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\ + $\BG~\dots~\EN$ & declare explicit blocks \\ + $\isarcmd{next}$ & switch implicit blocks \\ + $\NOTE{a}{a@1~\dots~a@n}$ & reconsider facts \\ + $\LET{p = t}$ & \text{abbreviate terms by matching} \\ +\end{tabular} + +\begin{matharray}{rcl} + theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\ + & \Or & \LEMMA{name}{form}~proof \\ + & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex] + proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex] + stmt & = & \BG~stmt^*~\EN \\ + & \Or & \isarcmd{next} \\ + & \Or & \NOTE{name}{name^+} \\ + & \Or & \LET{term = term} \\[0.5ex] + & \Or & \FIX{var^+} \\ + & \Or & \ASSUME{name}{form^+}\\ + & \Or & \THEN~goal{\dsh}stmt \\ + & \Or & goal{\dsh}stmt \\ + goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\ + & \Or & \SHOW{name}{form}~proof \\ +\end{matharray} + + +\subsection{Abbreviations and synonyms} + +\begin{matharray}{rcl} + \BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\ + \DDOT & \equiv & \BY{rule} \\ + \DOT & \equiv & \BY{assumption} \\ + \HENCENAME & \equiv & \THEN~\HAVENAME \\ + \THUSNAME & \equiv & \THEN~\SHOWNAME \\ + \FROM{a@1~\dots~a@n} & \equiv & \NOTE{this}{a@1~\dots~a@n}~\THEN \\ + \WITH{a@1~\dots~a@n} & \equiv & \FROM{a@1~\dots~a@n~this} \\[1ex] + \FROM{this} & \equiv & \THEN \\ + \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\ + \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\ +\end{matharray} + + +\subsection{Derived elements} + +\begin{matharray}{rcl} + \ALSO@0 & \approx & \NOTE{calculation}{this} \\ + \ALSO@{n+1} & \approx & \NOTE{calculation}{trans~[OF~calculation~this]} \\ + \FINALLY & \approx & \ALSO~\FROM{calculation} \\ + \PRESUME{a}{\phi} & \approx & \ASSUME{a}{\phi} \\ + \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\ + \isarcmd{sorry} & \approx & \BY{cheating} \\ +\end{matharray} + + +\subsection{Diagnostic commands} + +\begin{matharray}{ll} + \isarcmd{thm}~a@1~\dots~a@n & \text{print theorems} \\ + \isarcmd{term}~t & \text{print term} \\ + \isarcmd{prop}~\phi & \text{print meta-level proposition} \\ + \isarcmd{typ}~\tau & \text{print meta-level type} \\ +\end{matharray} + + +\section{Proof methods} + +\begin{tabular}{ll} + \multicolumn{2}{l}{\textbf{Single rules (forward-chaining facts)}} \\[0.5ex] + $assumption$ & apply assumption \\ + $rule~a@1~\dots~a@n$ & apply some rule \\ + $rule$ & apply standard rule (default for $\PROOFNAME$) \\ + $induct~x$ & apply induction rule \\ + $contradiction$ & apply $\neg{}$ elimination rule \\[2ex] + + \multicolumn{2}{l}{\textbf{Multiple rules (inserting facts)}} \\[0.5ex] + $-$ & \text{no rules} \\ + $intro~a@1~\dots~a@n$ & \text{introduction rules} \\ + $elim~a@1~\dots~a@n$ & \text{elimination rules} \\[2ex] + + \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex] + $simp$ & Simplifier \\ + $blast$, $fast$ & Classical reasoner \\ + $force$, $auto$ & Simplifier + Classical reasoner \\ + $arith$ & Arithmetic procedure \\ +\end{tabular} + + +\section{Attributes} + +\begin{tabular}{ll} + \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex] + $RS~b$ & resolve fact with rule \\ + $OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\ + $of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\ + $standard$ & put into standard result form \\ + $rulify$ & put into standard object-rule form \\ + $elimify$ & put destruction rule into elimination form \\[1ex] + + \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex] + $simp$ & declare Simplifier rules \\ + $intro$, $elim$, $dest$ & declare Classical reasoner rules (also ``$!$'' or ``$!!$'') \\ + $iff$ & declare Simplifier + Classical reasoner rules \\ + $trans$ & calculational rules (general transitivity) \\ +\end{tabular} + %%% Local Variables: %%% mode: latex