--- 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 \\
--- 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}
--- 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}
--- 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