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