7897
|
1 |
|
7981
|
2 |
\chapter{Isabelle/Isar Quick Reference}\label{ap:refcard}
|
7897
|
3 |
|
7974
|
4 |
\section{Proof commands}
|
|
5 |
|
|
6 |
\subsection{Primitives and basic syntax}
|
|
7 |
|
|
8 |
\begin{tabular}{ll}
|
|
9 |
$\FIX{x}$ & augment context by $\All x \Box$ \\
|
|
10 |
$\ASSUME{a}{\phi}$ & augment context by $\phi \Imp \Box$ \\
|
|
11 |
$\THEN$ & indicate forward chaining \\
|
|
12 |
$\HAVE{a}{\phi}$ & prove local result \\
|
|
13 |
$\SHOW{a}{\phi}$ & prove local result, establishing some goal \\
|
|
14 |
$\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\
|
|
15 |
$\BG~\dots~\EN$ & declare explicit blocks \\
|
|
16 |
$\isarcmd{next}$ & switch implicit blocks \\
|
7987
|
17 |
$\NOTE{a}{a@1\;\dots\;a@n}$ & reconsider facts \\
|
|
18 |
$\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\
|
7974
|
19 |
\end{tabular}
|
|
20 |
|
|
21 |
\begin{matharray}{rcl}
|
7987
|
22 |
theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\
|
|
23 |
& \Or & \LEMMA{name}{prop}~proof \\
|
7974
|
24 |
& \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex]
|
|
25 |
proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex]
|
|
26 |
stmt & = & \BG~stmt^*~\EN \\
|
|
27 |
& \Or & \isarcmd{next} \\
|
|
28 |
& \Or & \NOTE{name}{name^+} \\
|
|
29 |
& \Or & \LET{term = term} \\[0.5ex]
|
|
30 |
& \Or & \FIX{var^+} \\
|
7987
|
31 |
& \Or & \ASSUME{name}{prop^+}\\
|
7974
|
32 |
& \Or & \THEN~goal{\dsh}stmt \\
|
|
33 |
& \Or & goal{\dsh}stmt \\
|
7987
|
34 |
goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\
|
|
35 |
& \Or & \SHOW{name}{prop}~proof \\
|
7974
|
36 |
\end{matharray}
|
|
37 |
|
|
38 |
|
|
39 |
\subsection{Abbreviations and synonyms}
|
|
40 |
|
|
41 |
\begin{matharray}{rcl}
|
|
42 |
\BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\
|
|
43 |
\DDOT & \equiv & \BY{rule} \\
|
8195
|
44 |
\DOT & \equiv & \BY{this} \\
|
7974
|
45 |
\HENCENAME & \equiv & \THEN~\HAVENAME \\
|
|
46 |
\THUSNAME & \equiv & \THEN~\SHOWNAME \\
|
7987
|
47 |
\FROM{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\
|
|
48 |
\WITH{a@1\;\dots\;a@n} & \equiv & \FROM{a@1\;\dots\;a@n~this} \\[1ex]
|
7974
|
49 |
\FROM{this} & \equiv & \THEN \\
|
|
50 |
\FROM{this}~\HAVENAME & \equiv & \HENCENAME \\
|
|
51 |
\FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\
|
|
52 |
\end{matharray}
|
|
53 |
|
|
54 |
|
|
55 |
\subsection{Derived elements}
|
|
56 |
|
|
57 |
\begin{matharray}{rcl}
|
|
58 |
\ALSO@0 & \approx & \NOTE{calculation}{this} \\
|
|
59 |
\ALSO@{n+1} & \approx & \NOTE{calculation}{trans~[OF~calculation~this]} \\
|
|
60 |
\FINALLY & \approx & \ALSO~\FROM{calculation} \\
|
|
61 |
\PRESUME{a}{\phi} & \approx & \ASSUME{a}{\phi} \\
|
|
62 |
\DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\
|
|
63 |
\isarcmd{sorry} & \approx & \BY{cheating} \\
|
|
64 |
\end{matharray}
|
|
65 |
|
|
66 |
|
|
67 |
\subsection{Diagnostic commands}
|
|
68 |
|
|
69 |
\begin{matharray}{ll}
|
7987
|
70 |
\isarcmd{thm}~a@1\;\dots\;a@n & \text{print theorems} \\
|
7974
|
71 |
\isarcmd{term}~t & \text{print term} \\
|
|
72 |
\isarcmd{prop}~\phi & \text{print meta-level proposition} \\
|
|
73 |
\isarcmd{typ}~\tau & \text{print meta-level type} \\
|
|
74 |
\end{matharray}
|
|
75 |
|
|
76 |
|
|
77 |
\section{Proof methods}
|
|
78 |
|
|
79 |
\begin{tabular}{ll}
|
7976
|
80 |
\multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
|
7987
|
81 |
$assumption$ & apply some assumption \\
|
8195
|
82 |
$this$ & apply current facts \\
|
7987
|
83 |
$rule~a@1\;\dots\;a@n$ & apply some rule \\
|
7974
|
84 |
$rule$ & apply standard rule (default for $\PROOFNAME$) \\
|
|
85 |
$induct~x$ & apply induction rule \\
|
7987
|
86 |
$contradiction$ & apply $\neg{}$ elimination rule (any order) \\[2ex]
|
7974
|
87 |
|
7976
|
88 |
\multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
|
7974
|
89 |
$-$ & \text{no rules} \\
|
7987
|
90 |
$intro~a@1\;\dots\;a@n$ & \text{introduction rules} \\
|
|
91 |
$elim~a@1\;\dots\;a@n$ & \text{elimination rules} \\
|
|
92 |
$unfold~a@1\;\dots\;a@n$ & \text{definitions} \\[2ex]
|
7974
|
93 |
|
|
94 |
\multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
|
|
95 |
$simp$ & Simplifier \\
|
7987
|
96 |
$blast$, $fast$ & Classical Reasoner \\
|
|
97 |
$force$, $auto$ & Simplifier + Classical Reasoner \\
|
7974
|
98 |
$arith$ & Arithmetic procedure \\
|
|
99 |
\end{tabular}
|
|
100 |
|
|
101 |
|
|
102 |
\section{Attributes}
|
|
103 |
|
|
104 |
\begin{tabular}{ll}
|
|
105 |
\multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]
|
7987
|
106 |
$OF~a@1\;\dots\;a@n$ & apply rule to facts (skipping ``$_$'') \\
|
|
107 |
$of~t@1\;\dots\;t@n$ & apply rule to terms (skipping ``$_$'') \\
|
7976
|
108 |
$RS~b$ & resolve fact with rule \\
|
7974
|
109 |
$standard$ & put into standard result form \\
|
7976
|
110 |
$rulify$ & put into object-rule form \\
|
7974
|
111 |
$elimify$ & put destruction rule into elimination form \\[1ex]
|
|
112 |
|
|
113 |
\multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
|
|
114 |
$simp$ & declare Simplifier rules \\
|
7987
|
115 |
$intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``$!$'' or ``$!!$'') \\
|
|
116 |
$iff$ & declare Simplifier + Classical Reasoner rules \\
|
|
117 |
$trans$ & declare calculational rules (general transitivity) \\
|
7974
|
118 |
\end{tabular}
|
|
119 |
|
7897
|
120 |
%%% Local Variables:
|
|
121 |
%%% mode: latex
|
|
122 |
%%% TeX-master: "isar-ref"
|
|
123 |
%%% End:
|