doc-src/IsarRef/refcard.tex

added 'case' command;
added 'print_facts', 'print_binds', 'print_cases' commands;
added 'cases' method;
tuned;

\chapter{Isabelle/Isar Quick Reference}\label{ap:refcard}

\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 \\
  $\NEXT$ & switch implicit blocks \\
  $\NOTE{a}{a@1\;\dots\;a@n}$ & 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{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} \\
  \CASE{c} & & \text{invoke named context} \\
  \SORRY &  & \text{fake proof} \\
\end{matharray}


\subsection{Diagnostic commands}

\begin{matharray}{ll}
  \isarkeyword{thm}~a@1\;\dots\;a@n & \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~a@1\;\dots\;a@n$ & apply some rule  \\
  $rule$ & apply standard rule (default for $\PROOFNAME$) \\
  $contradiction$ & apply $\neg{}$ elimination rule (any order) \\
  $cases~x$ & case analysis (emits named cases) \\
  $induct~x$ & proof by induction (emits named cases) \\[2ex]

  \multicolumn{2}{l}{\textbf{Repeated steps (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} \\
  $unfold~a@1\;\dots\;a@n$ & \text{definitions} \\[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]
  $OF~a@1\;\dots\;a@n$ & apply rule to facts (skipping ``$_$'') \\
  $of~t@1\;\dots\;t@n$ & 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{Modify context}} \\[0.5ex]
  $simp$ & declare Simplifier rules \\
  $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``?'' or ``??'') \\
  $iff$ & declare Simplifier + Classical Reasoner rules \\
  $trans$ & declare calculational rules (general transitivity) \\
\end{tabular}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "isar-ref"
%%% End: