7897
|
1 |
|
|
2 |
\chapter{Isabelle/Isar Quick Reference}
|
|
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 \\
|
|
17 |
$\NOTE{a}{a@1~\dots~a@n}$ & reconsider facts \\
|
|
18 |
$\LET{p = t}$ & \text{abbreviate terms by matching} \\
|
|
19 |
\end{tabular}
|
|
20 |
|
|
21 |
\begin{matharray}{rcl}
|
|
22 |
theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\
|
|
23 |
& \Or & \LEMMA{name}{form}~proof \\
|
|
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^+} \\
|
|
31 |
& \Or & \ASSUME{name}{form^+}\\
|
|
32 |
& \Or & \THEN~goal{\dsh}stmt \\
|
|
33 |
& \Or & goal{\dsh}stmt \\
|
|
34 |
goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\
|
|
35 |
& \Or & \SHOW{name}{form}~proof \\
|
|
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} \\
|
|
44 |
\DOT & \equiv & \BY{assumption} \\
|
|
45 |
\HENCENAME & \equiv & \THEN~\HAVENAME \\
|
|
46 |
\THUSNAME & \equiv & \THEN~\SHOWNAME \\
|
|
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]
|
|
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}
|
|
70 |
\isarcmd{thm}~a@1~\dots~a@n & \text{print theorems} \\
|
|
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}
|
|
80 |
\multicolumn{2}{l}{\textbf{Single rules (forward-chaining facts)}} \\[0.5ex]
|
|
81 |
$assumption$ & apply assumption \\
|
|
82 |
$rule~a@1~\dots~a@n$ & apply some rule \\
|
|
83 |
$rule$ & apply standard rule (default for $\PROOFNAME$) \\
|
|
84 |
$induct~x$ & apply induction rule \\
|
|
85 |
$contradiction$ & apply $\neg{}$ elimination rule \\[2ex]
|
|
86 |
|
|
87 |
\multicolumn{2}{l}{\textbf{Multiple rules (inserting facts)}} \\[0.5ex]
|
|
88 |
$-$ & \text{no rules} \\
|
|
89 |
$intro~a@1~\dots~a@n$ & \text{introduction rules} \\
|
|
90 |
$elim~a@1~\dots~a@n$ & \text{elimination rules} \\[2ex]
|
|
91 |
|
|
92 |
\multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
|
|
93 |
$simp$ & Simplifier \\
|
|
94 |
$blast$, $fast$ & Classical reasoner \\
|
|
95 |
$force$, $auto$ & Simplifier + Classical reasoner \\
|
|
96 |
$arith$ & Arithmetic procedure \\
|
|
97 |
\end{tabular}
|
|
98 |
|
|
99 |
|
|
100 |
\section{Attributes}
|
|
101 |
|
|
102 |
\begin{tabular}{ll}
|
|
103 |
\multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]
|
|
104 |
$RS~b$ & resolve fact with rule \\
|
|
105 |
$OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\
|
|
106 |
$of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\
|
|
107 |
$standard$ & put into standard result form \\
|
|
108 |
$rulify$ & put into standard object-rule form \\
|
|
109 |
$elimify$ & put destruction rule into elimination form \\[1ex]
|
|
110 |
|
|
111 |
\multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
|
|
112 |
$simp$ & declare Simplifier rules \\
|
|
113 |
$intro$, $elim$, $dest$ & declare Classical reasoner rules (also ``$!$'' or ``$!!$'') \\
|
|
114 |
$iff$ & declare Simplifier + Classical reasoner rules \\
|
|
115 |
$trans$ & calculational rules (general transitivity) \\
|
|
116 |
\end{tabular}
|
|
117 |
|
7897
|
118 |
|
|
119 |
%%% Local Variables:
|
|
120 |
%%% mode: latex
|
|
121 |
%%% TeX-master: "isar-ref"
|
|
122 |
%%% End:
|