author | wenzelm |
Sun, 24 Apr 2016 21:31:14 +0200 | |
changeset 63039 | 1a20fd9cf281 |
parent 62337 | d3996d5873dd |
child 63285 | e9c777bfd78c |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
2 |
||
26779 | 3 |
theory Quick_Reference |
42651 | 4 |
imports Base Main |
26779 | 5 |
begin |
6 |
||
58618 | 7 |
chapter \<open>Isabelle/Isar quick reference \label{ap:refcard}\<close> |
26779 | 8 |
|
58618 | 9 |
section \<open>Proof commands\<close> |
26779 | 10 |
|
62278 | 11 |
subsection \<open>Main grammar \label{ap:main-grammar}\<close> |
62270 | 12 |
|
13 |
text \<open> |
|
14 |
\begin{tabular}{rcl} |
|
15 |
\<open>main\<close> & = & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\ |
|
16 |
& \<open>|\<close> & \<^theory_text>\<open>theorem name: props "proof"\<close> \\ |
|
17 |
& \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\ |
|
18 |
& & \quad\<^theory_text>\<open>fixes "var\<^sup>+"\<close> \\ |
|
19 |
& & \quad\<^theory_text>\<open>assumes name: props\<close> \\ |
|
20 |
& & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\ |
|
21 |
\<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\ |
|
22 |
& \<open>|\<close> & \<^theory_text>\<open>"refinement\<^sup>*" done\<close> \\ |
|
23 |
\<open>refinement\<close> & = & \<^theory_text>\<open>apply method\<close> \\ |
|
24 |
& \<open>|\<close> & \<^theory_text>\<open>supply facts\<close> \\ |
|
25 |
& \<open>|\<close> & \<^theory_text>\<open>subgoal "proof"\<close> \\ |
|
26 |
& \<open>|\<close> & \<^theory_text>\<open>subgoal for "var\<^sup>+" "proof"\<close> \\ |
|
27 |
& \<open>|\<close> & \<^theory_text>\<open>using facts\<close> \\ |
|
28 |
& \<open>|\<close> & \<^theory_text>\<open>unfolding facts\<close> \\ |
|
29 |
\<open>statement\<close> & = & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close> \\ |
|
30 |
& \<open>|\<close> & \<^theory_text>\<open>next\<close> \\ |
|
31 |
& \<open>|\<close> & \<^theory_text>\<open>note name = facts\<close> \\ |
|
32 |
& \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\ |
|
33 |
& \<open>|\<close> & \<^theory_text>\<open>write name (mixfix)\<close> \\ |
|
34 |
& \<open>|\<close> & \<^theory_text>\<open>fix "var\<^sup>+"\<close> \\ |
|
35 |
& \<open>|\<close> & \<^theory_text>\<open>assume name: props\<close> \\ |
|
62337 | 36 |
& \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for "var\<^sup>+"\<close> \\ |
62270 | 37 |
& \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\ |
38 |
\<open>goal\<close> & = & \<^theory_text>\<open>have name: props "proof"\<close> \\ |
|
39 |
& \<open>|\<close> & \<^theory_text>\<open>have name: props if name: props for "var\<^sup>+" "proof"\<close> \\ |
|
40 |
& \<open>|\<close> & \<^theory_text>\<open>show name: props "proof"\<close> \\ |
|
41 |
& \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for "var\<^sup>+" "proof"\<close> \\ |
|
42 |
\end{tabular} |
|
43 |
\<close> |
|
44 |
||
45 |
||
46 |
subsection \<open>Primitives\<close> |
|
26779 | 47 |
|
58618 | 48 |
text \<open> |
26779 | 49 |
\begin{tabular}{ll} |
62270 | 50 |
\<^theory_text>\<open>fix x\<close> & augment context by \<open>\<And>x. \<box>\<close> \\ |
51 |
\<^theory_text>\<open>assume a: A\<close> & augment context by \<open>A \<Longrightarrow> \<box>\<close> \\ |
|
52 |
\<^theory_text>\<open>then\<close> & indicate forward chaining of facts \\ |
|
53 |
\<^theory_text>\<open>have a: A\<close> & prove local result \\ |
|
54 |
\<^theory_text>\<open>show a: A\<close> & prove local result, refining some goal \\ |
|
55 |
\<^theory_text>\<open>using a\<close> & indicate use of additional facts \\ |
|
56 |
\<^theory_text>\<open>unfolding a\<close> & unfold definitional equations \\ |
|
57 |
\<^theory_text>\<open>proof m\<^sub>1 \<dots> qed m\<^sub>2\<close> & indicate proof structure and refinements \\ |
|
58 |
\<^theory_text>\<open>{ \<dots> }\<close> & indicate explicit blocks \\ |
|
59 |
\<^theory_text>\<open>next\<close> & switch proof blocks \\ |
|
60 |
\<^theory_text>\<open>note a = b\<close> & reconsider and declare facts \\ |
|
61 |
\<^theory_text>\<open>let p = t\<close> & abbreviate terms by higher-order matching \\ |
|
62 |
\<^theory_text>\<open>write c (mx)\<close> & declare local mixfix syntax \\ |
|
26852 | 63 |
\end{tabular} |
58618 | 64 |
\<close> |
26779 | 65 |
|
66 |
||
58618 | 67 |
subsection \<open>Abbreviations and synonyms\<close> |
26779 | 68 |
|
58618 | 69 |
text \<open> |
26852 | 70 |
\begin{tabular}{rcl} |
62270 | 71 |
\<^theory_text>\<open>by m\<^sub>1 m\<^sub>2\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>proof m\<^sub>1 qed m\<^sub>2\<close> \\ |
72 |
\<^theory_text>\<open>..\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>by standard\<close> \\ |
|
73 |
\<^theory_text>\<open>.\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>by this\<close> \\ |
|
74 |
\<^theory_text>\<open>from a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>note a then\<close> \\ |
|
75 |
\<^theory_text>\<open>with a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>from a and this\<close> \\ |
|
76 |
\<^theory_text>\<open>from this\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>then\<close> \\ |
|
26852 | 77 |
\end{tabular} |
58618 | 78 |
\<close> |
26779 | 79 |
|
80 |
||
58618 | 81 |
subsection \<open>Derived elements\<close> |
26779 | 82 |
|
58618 | 83 |
text \<open> |
26852 | 84 |
\begin{tabular}{rcl} |
62270 | 85 |
\<^theory_text>\<open>also"\<^sub>0"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>note calculation = this\<close> \\ |
86 |
\<^theory_text>\<open>also"\<^sub>n\<^sub>+\<^sub>1"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>note calculation = trans [OF calculation this]\<close> \\ |
|
87 |
\<^theory_text>\<open>finally\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>also from calculation\<close> \\[0.5ex] |
|
88 |
\<^theory_text>\<open>moreover\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>note calculation = calculation this\<close> \\ |
|
89 |
\<^theory_text>\<open>ultimately\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>moreover from calculation\<close> \\[0.5ex] |
|
90 |
\<^theory_text>\<open>presume a: A\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>assume a: A\<close> \\ |
|
63039 | 91 |
\<^theory_text>\<open>define x where "x = t"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>fix x assume x_def: "x = t"\<close> \\ |
62270 | 92 |
\<^theory_text>\<open>consider x where A | \<dots>\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>have thesis\<close> \\ |
93 |
& & \quad \<^theory_text>\<open>if "\<And>x. A \<Longrightarrow> thesis" and \<dots> for thesis\<close> \\ |
|
94 |
\<^theory_text>\<open>obtain x where a: A \<proof>\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>consider x where A \<proof>\<close> \\ |
|
95 |
& & \<^theory_text>\<open>fix x assume a: A\<close> \\ |
|
96 |
\<^theory_text>\<open>case c\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>fix x assume c: A\<close> \\ |
|
97 |
\<^theory_text>\<open>sorry\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>by cheating\<close> \\ |
|
26852 | 98 |
\end{tabular} |
58618 | 99 |
\<close> |
26779 | 100 |
|
101 |
||
58618 | 102 |
subsection \<open>Diagnostic commands\<close> |
26779 | 103 |
|
58618 | 104 |
text \<open> |
26779 | 105 |
\begin{tabular}{ll} |
62270 | 106 |
\<^theory_text>\<open>typ \<tau>\<close> & print type \\ |
107 |
\<^theory_text>\<open>term t\<close> & print term \\ |
|
108 |
\<^theory_text>\<open>prop \<phi>\<close> & print proposition \\ |
|
109 |
\<^theory_text>\<open>thm a\<close> & print fact \\ |
|
110 |
\<^theory_text>\<open>print_statement a\<close> & print fact in long statement form \\ |
|
26779 | 111 |
\end{tabular} |
58618 | 112 |
\<close> |
26779 | 113 |
|
114 |
||
58618 | 115 |
section \<open>Proof methods\<close> |
26779 | 116 |
|
58618 | 117 |
text \<open> |
26779 | 118 |
\begin{tabular}{ll} |
61477 | 119 |
\multicolumn{2}{l}{\<^bold>\<open>Single steps (forward-chaining facts)\<close>} \\[0.5ex] |
62270 | 120 |
@{method assumption} & apply some goal assumption \\ |
26779 | 121 |
@{method this} & apply current facts \\ |
61493 | 122 |
@{method rule}~\<open>a\<close> & apply some rule \\ |
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
58618
diff
changeset
|
123 |
@{method standard} & apply standard rule (default for @{command "proof"}) \\ |
61493 | 124 |
@{method contradiction} & apply \<open>\<not>\<close> elimination rule (any order) \\ |
125 |
@{method cases}~\<open>t\<close> & case analysis (provides cases) \\ |
|
126 |
@{method induct}~\<open>x\<close> & proof by induction (provides cases) \\[2ex] |
|
26779 | 127 |
|
61477 | 128 |
\multicolumn{2}{l}{\<^bold>\<open>Repeated steps (inserting facts)\<close>} \\[0.5ex] |
26779 | 129 |
@{method "-"} & no rules \\ |
61493 | 130 |
@{method intro}~\<open>a\<close> & introduction rules \\ |
26779 | 131 |
@{method intro_classes} & class introduction rules \\ |
62270 | 132 |
@{method intro_locales} & locale introduction rules (without body) \\ |
133 |
@{method unfold_locales} & locale introduction rules (with body) \\ |
|
61493 | 134 |
@{method elim}~\<open>a\<close> & elimination rules \\ |
135 |
@{method unfold}~\<open>a\<close> & definitional rewrite rules \\[2ex] |
|
26779 | 136 |
|
61477 | 137 |
\multicolumn{2}{l}{\<^bold>\<open>Automated proof tools (inserting facts)\<close>} \\[0.5ex] |
26779 | 138 |
@{method iprover} & intuitionistic proof search \\ |
139 |
@{method blast}, @{method fast} & Classical Reasoner \\ |
|
140 |
@{method simp}, @{method simp_all} & Simplifier (+ Splitter) \\ |
|
141 |
@{method auto}, @{method force} & Simplifier + Classical Reasoner \\ |
|
142 |
@{method arith} & Arithmetic procedures \\ |
|
143 |
\end{tabular} |
|
58618 | 144 |
\<close> |
26779 | 145 |
|
146 |
||
58618 | 147 |
section \<open>Attributes\<close> |
26779 | 148 |
|
58618 | 149 |
text \<open> |
26779 | 150 |
\begin{tabular}{ll} |
61477 | 151 |
\multicolumn{2}{l}{\<^bold>\<open>Rules\<close>} \\[0.5ex] |
61493 | 152 |
@{attribute OF}~\<open>a\<close> & rule resolved with facts (skipping ``\<open>_\<close>'') \\ |
153 |
@{attribute of}~\<open>t\<close> & rule instantiated with terms (skipping ``\<open>_\<close>'') \\ |
|
154 |
@{attribute "where"}~\<open>x = t\<close> & rule instantiated with terms, by variable name \\ |
|
26779 | 155 |
@{attribute symmetric} & resolution with symmetry rule \\ |
61493 | 156 |
@{attribute THEN}~\<open>b\<close> & resolution with another rule \\ |
26779 | 157 |
@{attribute rule_format} & result put into standard rule format \\ |
158 |
@{attribute elim_format} & destruct rule turned into elimination rule format \\[1ex] |
|
159 |
||
61477 | 160 |
\multicolumn{2}{l}{\<^bold>\<open>Declarations\<close>} \\[0.5ex] |
26779 | 161 |
@{attribute simp} & Simplifier rule \\ |
162 |
@{attribute intro}, @{attribute elim}, @{attribute dest} & Pure or Classical Reasoner rule \\ |
|
163 |
@{attribute iff} & Simplifier + Classical Reasoner rule \\ |
|
164 |
@{attribute split} & case split rule \\ |
|
165 |
@{attribute trans} & transitivity rule \\ |
|
166 |
@{attribute sym} & symmetry rule \\ |
|
167 |
\end{tabular} |
|
58618 | 168 |
\<close> |
26779 | 169 |
|
170 |
||
58618 | 171 |
section \<open>Rule declarations and methods\<close> |
26779 | 172 |
|
58618 | 173 |
text \<open> |
26779 | 174 |
\begin{tabular}{l|lllll} |
175 |
& @{method rule} & @{method iprover} & @{method blast} & @{method simp} & @{method auto} \\ |
|
176 |
& & & @{method fast} & @{method simp_all} & @{method force} \\ |
|
177 |
\hline |
|
61493 | 178 |
@{attribute Pure.elim}\<open>!\<close> @{attribute Pure.intro}\<open>!\<close> |
179 |
& \<open>\<times>\<close> & \<open>\<times>\<close> \\ |
|
26779 | 180 |
@{attribute Pure.elim} @{attribute Pure.intro} |
61493 | 181 |
& \<open>\<times>\<close> & \<open>\<times>\<close> \\ |
182 |
@{attribute elim}\<open>!\<close> @{attribute intro}\<open>!\<close> |
|
183 |
& \<open>\<times>\<close> & & \<open>\<times>\<close> & & \<open>\<times>\<close> \\ |
|
26779 | 184 |
@{attribute elim} @{attribute intro} |
61493 | 185 |
& \<open>\<times>\<close> & & \<open>\<times>\<close> & & \<open>\<times>\<close> \\ |
26779 | 186 |
@{attribute iff} |
61493 | 187 |
& \<open>\<times>\<close> & & \<open>\<times>\<close> & \<open>\<times>\<close> & \<open>\<times>\<close> \\ |
188 |
@{attribute iff}\<open>?\<close> |
|
189 |
& \<open>\<times>\<close> \\ |
|
190 |
@{attribute elim}\<open>?\<close> @{attribute intro}\<open>?\<close> |
|
191 |
& \<open>\<times>\<close> \\ |
|
26779 | 192 |
@{attribute simp} |
61493 | 193 |
& & & & \<open>\<times>\<close> & \<open>\<times>\<close> \\ |
26779 | 194 |
@{attribute cong} |
61493 | 195 |
& & & & \<open>\<times>\<close> & \<open>\<times>\<close> \\ |
26779 | 196 |
@{attribute split} |
61493 | 197 |
& & & & \<open>\<times>\<close> & \<open>\<times>\<close> \\ |
26779 | 198 |
\end{tabular} |
58618 | 199 |
\<close> |
26779 | 200 |
|
201 |
||
62270 | 202 |
section \<open>Proof scripts\<close> |
26779 | 203 |
|
58618 | 204 |
subsection \<open>Commands\<close> |
26779 | 205 |
|
58618 | 206 |
text \<open> |
26779 | 207 |
\begin{tabular}{ll} |
62270 | 208 |
\<^theory_text>\<open>apply m\<close> & apply proof method during backwards refinement \\ |
209 |
\<^theory_text>\<open>apply_end m\<close> & apply proof method (as if in terminal position) \\ |
|
210 |
\<^theory_text>\<open>supply a\<close> & supply facts during backwards refinement \\ |
|
211 |
\<^theory_text>\<open>subgoal\<close> & nested proof during backwards refinement \\ |
|
212 |
\<^theory_text>\<open>defer n\<close> & move subgoal to end \\ |
|
213 |
\<^theory_text>\<open>prefer n\<close> & move subgoal to start \\ |
|
214 |
\<^theory_text>\<open>back\<close> & backtrack last command \\ |
|
215 |
\<^theory_text>\<open>done\<close> & complete proof \\ |
|
26779 | 216 |
\end{tabular} |
58618 | 217 |
\<close> |
26779 | 218 |
|
219 |
||
58618 | 220 |
subsection \<open>Methods\<close> |
26779 | 221 |
|
58618 | 222 |
text \<open> |
26779 | 223 |
\begin{tabular}{ll} |
61493 | 224 |
@{method rule_tac}~\<open>insts\<close> & resolution (with instantiation) \\ |
225 |
@{method erule_tac}~\<open>insts\<close> & elim-resolution (with instantiation) \\ |
|
226 |
@{method drule_tac}~\<open>insts\<close> & destruct-resolution (with instantiation) \\ |
|
227 |
@{method frule_tac}~\<open>insts\<close> & forward-resolution (with instantiation) \\ |
|
228 |
@{method cut_tac}~\<open>insts\<close> & insert facts (with instantiation) \\ |
|
229 |
@{method thin_tac}~\<open>\<phi>\<close> & delete assumptions \\ |
|
230 |
@{method subgoal_tac}~\<open>\<phi>\<close> & new claims \\ |
|
231 |
@{method rename_tac}~\<open>x\<close> & rename innermost goal parameters \\ |
|
232 |
@{method rotate_tac}~\<open>n\<close> & rotate assumptions of goal \\ |
|
233 |
@{method tactic}~\<open>text\<close> & arbitrary ML tactic \\ |
|
234 |
@{method case_tac}~\<open>t\<close> & exhaustion (datatypes) \\ |
|
235 |
@{method induct_tac}~\<open>x\<close> & induction (datatypes) \\ |
|
236 |
@{method ind_cases}~\<open>t\<close> & exhaustion + simplification (inductive predicates) \\ |
|
26779 | 237 |
\end{tabular} |
58618 | 238 |
\<close> |
26779 | 239 |
|
240 |
end |