2 \chapter{Isabelle/Isar quick reference}\label{ap:refcard}
4 \section{Proof commands}
6 \subsection{Primitives and basic syntax}
9 $\FIX{\vec x}$ & augment context by $\All {\vec x} \Box$ \\
10 $\ASSUME{a}{\vec\phi}$ & augment context by $\vec\phi \Imp \Box$ \\
11 $\THEN$ & indicate forward chaining of facts \\
12 $\HAVE{a}{\phi}$ & prove local result \\
13 $\SHOW{a}{\phi}$ & prove local result, establishing some goal \\
14 $\USING{\vec a}$ & indicate use of additional facts \\
15 $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\
16 $\BG~\dots~\EN$ & declare explicit blocks \\
17 $\NEXT$ & switch implicit blocks \\
18 $\NOTE{a}{\vec b}$ & reconsider facts \\
19 $\LET{p = t}$ & \Text{abbreviate terms by higher-order matching} \\
22 \begin{matharray}{rcl}
23 theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\
24 & \Or & \LEMMA{name}{prop}~proof \\
25 & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex]
26 proof & = & prfx^*~\PROOF{method}~stmt^*~\QED{method} \\[1ex]
27 prfx & = & \APPLY{method} \\
28 & \Or & \USING{name^+} \\
29 stmt & = & \BG~stmt^*~\EN \\
31 & \Or & \NOTE{name}{name^+} \\
32 & \Or & \LET{term = term} \\[0.5ex]
33 & \Or & \FIX{var^+} \\
34 & \Or & \ASSUME{name}{prop^+}\\
35 & \Or & \THEN~goal{\dsh}stmt \\
37 goal & = & \HAVE{name}{prop}~proof \\
38 & \Or & \SHOW{name}{prop}~proof \\
42 \subsection{Abbreviations and synonyms}
44 \begin{matharray}{rcl}
45 \BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\
46 \DDOT & \equiv & \BY{rule} \\
47 \DOT & \equiv & \BY{this} \\
48 \HENCENAME & \equiv & \THEN~\HAVENAME \\
49 \THUSNAME & \equiv & \THEN~\SHOWNAME \\
50 \FROM{\vec a} & \equiv & \NOTE{this}{\vec a}~\THEN \\
51 \WITH{\vec a} & \equiv & \FROM{\vec a~\AND~this} \\[1ex]
52 \FROM{this} & \equiv & \THEN \\
53 \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\
54 \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\
58 \subsection{Derived elements}
60 \begin{matharray}{rcl}
61 \ALSO@0 & \approx & \NOTE{calculation}{this} \\
62 \ALSO@{n+1} & \approx & \NOTE{calculation}{trans~[OF~calculation~this]} \\
63 \FINALLY & \approx & \ALSO~\FROM{calculation} \\[0.5ex]
64 \MOREOVER & \approx & \NOTE{calculation}{calculation~this} \\
65 \ULTIMATELY & \approx & \MOREOVER~\FROM{calculation} \\[0.5ex]
66 \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi} \\
67 % & & \Text{(permissive assumption)} \\
68 \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\
69 % & & \Text{(definitional assumption)} \\
70 \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
71 % & & \Text{(generalized existence)} \\
72 \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\
73 % & & \Text{(named context)} \\[0.5ex]
74 \SORRY & \approx & \BY{cheating} \\
78 \subsection{Diagnostic commands}
81 \isarkeyword{pr} & \Text{print current state} \\
82 \isarkeyword{thm}~\vec a & \Text{print theorems} \\
83 \isarkeyword{term}~t & \Text{print term} \\
84 \isarkeyword{prop}~\phi & \Text{print meta-level proposition} \\
85 \isarkeyword{typ}~\tau & \Text{print meta-level type} \\
89 \section{Proof methods}
92 \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
93 $assumption$ & apply some assumption \\
94 $this$ & apply current facts \\
95 $rule~\vec a$ & apply some rule \\
96 $rule$ & apply standard rule (default for $\PROOFNAME$) \\
97 $contradiction$ & apply $\neg{}$ elimination rule (any order) \\
98 $cases~t$ & case analysis (provides cases) \\
99 $induct~\vec x$ & proof by induction (provides cases) \\[2ex]
101 \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
102 $-$ & \Text{no rules} \\
103 $intro~\vec a$ & \Text{introduction rules} \\
104 $intro_classes$ & \Text{class introduction rules} \\
105 $elim~\vec a$ & \Text{elimination rules} \\
106 $unfold~\vec a$ & \Text{definitions} \\[2ex]
108 \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
109 $rules$ & \Text{intuitionistic proof search} \\
110 $simp$, $simp_all$ & Simplifier (+ Splitter) \\
111 $blast$, $fast$ & Classical Reasoner \\
112 $auto$, $force$ & Simplifier + Classical Reasoner \\
113 $arith$ & Arithmetic procedure \\
120 \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
121 $OF~\vec a$ & rule applied to facts (skipping ``$_$'') \\
122 $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\
123 $symmetric$ & resolution with symmetry rule \\
124 $THEN~b$ & resolution with another rule \\
125 $rule_format$ & result put into standard rule format \\
126 $elim_format$ & destruct rule turned into elimination rule format \\[1ex]
128 \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
129 $simp$ & Simplifier rule \\
130 $intro$, $elim$, $dest$ & Pure or Classical Reasoner rule \\
131 $iff$ & Simplifier + Classical Reasoner rule \\
132 $split$ & case split rule \\
133 $trans$ & transitivity rule \\
134 $sym$ & symmetry rule \\
138 \section{Emulating tactic scripts}
140 \subsection{Commands}
143 $\APPLY{m}$ & apply proof method at initial position \\
144 $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\
145 $\isarkeyword{done}$ & complete proof \\
146 $\isarkeyword{defer}~n$ & move subgoal to end \\
147 $\isarkeyword{prefer}~n$ & move subgoal to beginning \\
148 $\isarkeyword{back}$ & backtrack last command \\
149 $\isarkeyword{declare}$ & declare rules in current theory \\
155 $rule_tac~insts$ & resolution (with instantiation) \\
156 $erule_tac~insts$ & elim-resolution (with instantiation) \\
157 $drule_tac~insts$ & destruct-resolution (with instantiation) \\
158 $frule_tac~insts$ & forward-resolution (with instantiation) \\
159 $cut_tac~insts$ & insert facts (with instantiation) \\
160 $thin_tac~\phi$ & delete assumptions \\
161 $subgoal_tac~\phi$ & new claims \\
162 $rename_tac~\vec x$ & rename suffix of goal parameters \\
163 $rotate_tac~n$ & rotate assumptions of goal \\
164 $tactic~text$ & arbitrary ML tactic \\
165 $case_tac~t$ & exhaustion (datatypes) \\
166 $induct_tac~\vec x$ & induction (datatypes) \\
167 $ind_cases~t$ & exhaustion + simplification (inductive sets) \\
173 %%% TeX-master: "isar-ref"