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

  \MOREOVER & \approx & \NOTE{calculation}{calculation~this} \\

  \ULTIMATELY & \approx & \MOREOVER~\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{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~t$ & case analysis (provides cases) \\

  $induct~\vec 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{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{Methods}

\begin{tabular}{ll}

  $tactic~text$ & method from ML tactic \\

  $insert~\vec a$ & insert theorems (ignoring current facts) \\

  $res_inst_tac~insts$ & resolution with instantiation \\

  $eres_inst_tac~insts$ & elim-resolution with instantiation \\

  $dres_inst_tac~insts$ & destruct-resolution with instantiation \\

  $forw_inst_tac~insts$ & forward-resolution with instantiation \\

  $subgoal_tac~\phi$ & insert new claim \\

  $case_tac~t$ & exhaustion (datatypes) \\

  $induct_tac~\vec x$ & induction (datatypes) \\

\end{tabular}

%%% Local Variables: 

%%% mode: latex

%%% TeX-master: "isar-ref"

%%% End: