\chapter{Isabelle/Isar Quick Reference}\label{ap:refcard}
\section{Proof commands}
\subsection{Primitives and basic syntax}
\begin{tabular}{ll}
$\FIX{\vec x}$ & augment context by $\All {\vec x} \Box$ \\
$\ASSUME{a}{\vec\phi}$ & augment context by $\vec\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 \\
$\NEXT$ & switch implicit blocks \\
$\NOTE{a}{\vec b}$ & reconsider facts \\
$\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\
\end{tabular}
\begin{matharray}{rcl}
theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\
& \Or & \LEMMA{name}{prop}~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 & \NEXT \\
& \Or & \NOTE{name}{name^+} \\
& \Or & \LET{term = term} \\[0.5ex]
& \Or & \FIX{var^+} \\
& \Or & \ASSUME{name}{prop^+}\\
& \Or & \THEN~goal{\dsh}stmt \\
& \Or & goal{\dsh}stmt \\
goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\
& \Or & \SHOW{name}{prop}~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{this} \\
\HENCENAME & \equiv & \THEN~\HAVENAME \\
\THUSNAME & \equiv & \THEN~\SHOWNAME \\
\FROM{\vec a} & \equiv & \NOTE{this}{\vec a}~\THEN \\
\WITH{\vec a} & \equiv & \FROM{\vec a~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} \\[0.5ex]
\PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi}~~\text{(permissive assumption)} \\
\DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t}~~\text{(definitional assumption)} \\
\OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi}~~\text{(generalized existence)} \\
\CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi}~~\text{(named context)} \\[0.5ex]
\SORRY & \approx & \BY{cheating} \\
\end{matharray}
\subsection{Diagnostic commands}
\begin{matharray}{ll}
\isarkeyword{help} & \text{print help on Isar language elements} \\
\isarkeyword{pr} & \text{print current state} \\
\isarkeyword{thm}~\vec a & \text{print theorems} \\
\isarkeyword{term}~t & \text{print term} \\
\isarkeyword{prop}~\phi & \text{print meta-level proposition} \\
\isarkeyword{typ}~\tau & \text{print meta-level type} \\
\isarkeyword{print_facts} & \text{print named facts} \\
\isarkeyword{print_binds} & \text{print term abbreviations} \\
\isarkeyword{print_cases} & \text{print named cases} \\
\end{matharray}
\section{Proof methods}
\begin{tabular}{ll}
\multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
$assumption$ & apply some assumption \\
$this$ & apply current facts \\
$rule~\vec a$ & apply some rule \\
$rule$ & apply standard rule (default for $\PROOFNAME$) \\
$contradiction$ & apply $\neg{}$ elimination rule (any order) \\
$cases~x$ & case analysis (provides cases) \\
$induct~x$ & proof by induction (provides cases) \\[2ex]
\multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
$-$ & \text{no rules} \\
$intro~\vec a$ & \text{introduction rules} \\
$intro_classes$ & \text{class introduction rules} \\
$elim~\vec a$ & \text{elimination rules} \\
$unfold~\vec a$ & \text{definitions} \\[2ex]
\multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
$simp$ & Simplifier (+ Splitter) \\
$blast$, $fast$ & Classical Reasoner \\
$force$, $auto$ & Simplifier + Classical Reasoner \\
$arith$ & Arithmetic procedure \\
\end{tabular}
\section{Attributes}
\begin{tabular}{ll}
\multicolumn{2}{l}{\textbf{Manipulate rules}} \\[0.5ex]
$OF~\vec a$ & apply rule to facts (skipping ``$_$'') \\
$of~\vec t$ & apply rule to terms (skipping ``$_$'') \\
$RS~b$ & resolve fact with rule \\
$standard$ & put into standard result form \\
$rulify$ & put into object-rule form \\
$elimify$ & put destruction rule into elimination form \\[1ex]
\multicolumn{2}{l}{\textbf{Declare rules}} \\[0.5ex]
$simp$ & declare Simplifier rules \\
$split$ & declare Splitter rules \\
$intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``?'' or ``??'') \\
$iff$ & declare Simplifier + Classical Reasoner rules \\
$trans$ & declare calculational rules (general transitivity) \\
\end{tabular}
\section{Emulating tactic scripts}
\subsection{Proof commands}
\begin{tabular}{ll}
$\isarkeyword{apply}~(m)$ & apply proof method (at initial position) \\
$\isarkeyword{apply_end}~(m)$ & apply proof method (near terminal position) \\
$\isarkeyword{defer}~n$ & move subgoal to end \\
$\isarkeyword{prefer}~n$ & move subgoal to beginning \\
$\isarkeyword{back}$ & backtrack last command \\
\end{tabular}
\subsection{Proof methods}
\begin{tabular}{ll}
$tactic~text$ & method from ML tactic \\
\end{tabular}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"
%%% End: