<commit_before>
\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 of facts \\
  $\HAVE{a}{\phi}$ & prove local result \\
  $\SHOW{a}{\phi}$ & prove local result, refining some goal \\
  $\USING{\vec a}$ & indicate use of additional facts \\
  $\UNFOLDING{\vec a}$ & unfold definitional equations \\
  $\PROOF{m@1}~\dots~\QED{m@2}$ & indicate proof structure and refinements \\
  $\BG~\dots~\EN$ & declare explicit blocks \\
  $\NEXT$ & switch 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 \isarkeyword{definition}~\dots \Or \dots \\[1ex]
  proof & = & prfx^*~\PROOF{method}~stmt^*~\QED{method} \\
  & \Or & prfx^*~\DONE \\[1ex]
  prfx & = & \APPLY{method} \\
  & \Or & \USING{name^+} \\
  & \Or & \UNFOLDING{name^+} \\
  stmt & = & \BG~stmt^*~\EN \\
  & \Or & \NEXT \\
  & \Or & \NOTE{name}{name^+} \\
  & \Or & \LET{term = term} \\
  & \Or & \FIX{var^+} \\
  & \Or & \ASSUME{name}{prop^+}\\
  & \Or & \THEN^?~goal \\
  goal & = & \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~\AND~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} \\
\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]
  $rules$ & \Text{intuitionistic proof search} \\
  $blast$, $fast$ & Classical Reasoner \\
  $simp$, $simp_all$ & Simplifier (+ Splitter) \\
  $auto$, $force$ & Simplifier + Classical Reasoner \\
  $arith$ & Arithmetic procedure \\
\end{tabular}


\section{Attributes}

\begin{tabular}{ll}
  \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
  $OF~\vec a$ & rule resolved with facts (skipping ``$_$'') \\
  $of~\vec t$ & rule instantiated with terms (skipping ``$_$'') \\
  $where~\vec x = \vec t$ & rule instantiated with terms, by variable name \\
  $symmetric$ & resolution with symmetry rule \\
  $THEN~b$ & resolution with another rule \\
  $rule_format$ & result put into standard rule format \\
  $elim_format$ & destruct rule turned into elimination rule format \\[1ex]

  \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
  $simp$ & Simplifier rule \\
  $intro$, $elim$, $dest$ & Pure or Classical Reasoner rule \\
  $iff$ & Simplifier + Classical Reasoner rule \\
  $split$ & case split rule \\
  $trans$ & transitivity rule \\
  $sym$ & symmetry rule \\
\end{tabular}


\section{Rule declarations and methods}

\begin{tabular}{l|lllll}
                          & $rule$   & $rules$  & $blast$ etc. & $simp$ etc. & $auto$ etc. \\
  \hline
  $elim!$ $intro!$ (Pure) & $\times$ & $\times$ \\
  $elim$ $intro$ (Pure)   & $\times$ & $\times$ \\
  $elim!$ $intro!$        & $\times$ &          & $\times$     &             & $\times$ \\
  $elim$ $intro$          & $\times$ &          & $\times$     &             & $\times$ \\
  $iff$                   & $\times$ &          & $\times$     & $\times$    & $\times$ \\
  $iff?$                  & $\times$ \\
  $elim?$ $intro?$        & $\times$ \\
  $simp$                  &          &          &              & $\times$    & $\times$ \\
  $cong$                  &          &          &              & $\times$    & $\times$ \\
  $split$                 &          &          &              & $\times$    & $\times$ \\
\end{tabular}


\section{Emulating tactic scripts}

\subsection{Commands}

\begin{tabular}{ll}
  $\APPLY{m}$ & apply proof method at initial position \\
  $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\
  $\isarkeyword{done}$ & complete proof \\
  $\isarkeyword{defer}~n$ & move subgoal to end \\
  $\isarkeyword{prefer}~n$ & move subgoal to beginning \\
  $\isarkeyword{back}$ & backtrack last command \\
  $\isarkeyword{declare}$ & declare rules in current theory \\
\end{tabular}

\subsection{Methods}

\begin{tabular}{ll}
  $rule_tac~insts$ & resolution (with instantiation) \\
  $erule_tac~insts$ & elim-resolution (with instantiation) \\
  $drule_tac~insts$ & destruct-resolution (with instantiation) \\
  $frule_tac~insts$ & forward-resolution (with instantiation) \\
  $cut_tac~insts$ & insert facts (with instantiation) \\
  $thin_tac~\phi$ & delete assumptions \\<commit_msg>removed 'declare' from tactic emulations;<commit_after>
\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 of facts \\
  $\HAVE{a}{\phi}$ & prove local result \\
  $\SHOW{a}{\phi}$ & prove local result, refining some goal \\
  $\USING{\vec a}$ & indicate use of additional facts \\
  $\UNFOLDING{\vec a}$ & unfold definitional equations \\
  $\PROOF{m@1}~\dots~\QED{m@2}$ & indicate proof structure and refinements \\
  $\BG~\dots~\EN$ & declare explicit blocks \\
  $\NEXT$ & switch 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 \isarkeyword{definition}~\dots \Or \dots \\[1ex]
  proof & = & prfx^*~\PROOF{method}~stmt^*~\QED{method} \\
  & \Or & prfx^*~\DONE \\[1ex]
  prfx & = & \APPLY{method} \\
  & \Or & \USING{name^+} \\
  & \Or & \UNFOLDING{name^+} \\
  stmt & = & \BG~stmt^*~\EN \\
  & \Or & \NEXT \\
  & \Or & \NOTE{name}{name^+} \\
  & \Or & \LET{term = term} \\
  & \Or & \FIX{var^+} \\
  & \Or & \ASSUME{name}{prop^+}\\
  & \Or & \THEN^?~goal \\
  goal & = & \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~\AND~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} \\
\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]
  $rules$ & \Text{intuitionistic proof search} \\
  $blast$, $fast$ & Classical Reasoner \\
  $simp$, $simp_all$ & Simplifier (+ Splitter) \\
  $auto$, $force$ & Simplifier + Classical Reasoner \\
  $arith$ & Arithmetic procedure \\
\end{tabular}


\section{Attributes}

\begin{tabular}{ll}
  \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
  $OF~\vec a$ & rule resolved with facts (skipping ``$_$'') \\
  $of~\vec t$ & rule instantiated with terms (skipping ``$_$'') \\
  $where~\vec x = \vec t$ & rule instantiated with terms, by variable name \\
  $symmetric$ & resolution with symmetry rule \\
  $THEN~b$ & resolution with another rule \\
  $rule_format$ & result put into standard rule format \\
  $elim_format$ & destruct rule turned into elimination rule format \\[1ex]

  \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
  $simp$ & Simplifier rule \\
  $intro$, $elim$, $dest$ & Pure or Classical Reasoner rule \\
  $iff$ & Simplifier + Classical Reasoner rule \\
  $split$ & case split rule \\
  $trans$ & transitivity rule \\
  $sym$ & symmetry rule \\
\end{tabular}


\section{Rule declarations and methods}

\begin{tabular}{l|lllll}
                          & $rule$   & $rules$  & $blast$ etc. & $simp$ etc. & $auto$ etc. \\
  \hline
  $elim!$ $intro!$ (Pure) & $\times$ & $\times$ \\
  $elim$ $intro$ (Pure)   & $\times$ & $\times$ \\
  $elim!$ $intro!$        & $\times$ &          & $\times$     &             & $\times$ \\
  $elim$ $intro$          & $\times$ &          & $\times$     &             & $\times$ \\
  $iff$                   & $\times$ &          & $\times$     & $\times$    & $\times$ \\
  $iff?$                  & $\times$ \\
  $elim?$ $intro?$        & $\times$ \\
  $simp$                  &          &          &              & $\times$    & $\times$ \\
  $cong$                  &          &          &              & $\times$    & $\times$ \\
  $split$                 &          &          &              & $\times$    & $\times$ \\
\end{tabular}


\section{Emulating tactic scripts}

\subsection{Commands}

\begin{tabular}{ll}
  $\APPLY{m}$ & apply proof method at initial position \\
  $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\
  $\isarkeyword{done}$ & complete proof \\
  $\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}
  $rule_tac~insts$ & resolution (with instantiation) \\
  $erule_tac~insts$ & elim-resolution (with instantiation) \\
  $drule_tac~insts$ & destruct-resolution (with instantiation) \\
  $frule_tac~insts$ & forward-resolution (with instantiation) \\
  $cut_tac~insts$ & insert facts (with instantiation) \\
  $thin_tac~\phi$ & delete assumptions \\
{'fraction_non_alphanumeric': 0.20809040524004896, 'fraction_numerical': 0.00503850860145397, 'mean_word_length': 2.6276762402088774, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3486839', 'n_tokens_mistral': 5204, 'n_tokens_neox': 5030, 'n_words': 1086}