1 |
1 |
2 \chapter{Isabelle/Isar Quick Reference} |
2 \chapter{Isabelle/Isar Quick Reference} |
|
3 |
|
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} |
3 |
117 |
4 |
118 |
5 %%% Local Variables: |
119 %%% Local Variables: |
6 %%% mode: latex |
120 %%% mode: latex |
7 %%% TeX-master: "isar-ref" |
121 %%% TeX-master: "isar-ref" |