doc-src/IsarRef/refcard.tex
 author wenzelm Sun Jul 23 12:01:05 2000 +0200 (2000-07-23) changeset 9408 d3d56e1d2ec1 parent 9233 8c8399b9ecaa child 9603 816917b6c2de permissions -rw-r--r--
classical atts now intro! / intro / intro?;
 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@8511 9 $\FIX{\vec x}$ & augment context by $\All {\vec x} \Box$ \\ wenzelm@8511 10 $\ASSUME{a}{\vec\phi}$ & augment context by $\vec\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@8447 16 $\NEXT$ & switch implicit blocks \\ wenzelm@8511 17 $\NOTE{a}{\vec b}$ & reconsider facts \\ wenzelm@7987 18 $\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\ wenzelm@7974 19 \end{tabular} wenzelm@7974 20 wenzelm@7974 21 \begin{matharray}{rcl} wenzelm@7987 22 theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\ wenzelm@7987 23 & \Or & \LEMMA{name}{prop}~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@8447 27 & \Or & \NEXT \\ wenzelm@7974 28 & \Or & \NOTE{name}{name^+} \\ wenzelm@7974 29 & \Or & \LET{term = term} \\[0.5ex] wenzelm@7974 30 & \Or & \FIX{var^+} \\ wenzelm@7987 31 & \Or & \ASSUME{name}{prop^+}\\ wenzelm@7974 32 & \Or & \THEN~goal{\dsh}stmt \\ wenzelm@7974 33 & \Or & goal{\dsh}stmt \\ wenzelm@7987 34 goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\ wenzelm@7987 35 & \Or & \SHOW{name}{prop}~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@8195 44 \DOT & \equiv & \BY{this} \\ wenzelm@7974 45 \HENCENAME & \equiv & \THEN~\HAVENAME \\ wenzelm@7974 46 \THUSNAME & \equiv & \THEN~\SHOWNAME \\ wenzelm@8511 47 \FROM{\vec a} & \equiv & \NOTE{this}{\vec a}~\THEN \\ wenzelm@8511 48 \WITH{\vec a} & \equiv & \FROM{\vec a~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@8511 60 \FINALLY & \approx & \ALSO~\FROM{calculation} \\[0.5ex] wenzelm@8619 61 \MOREOVER & \approx & \NOTE{calculation}{calculation~this} \\ wenzelm@8619 62 \ULTIMATELY & \approx & \MOREOVER~\FROM{calculation} \\[0.5ex] wenzelm@8619 63 \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi} \\ wenzelm@8619 64 % & & \text{(permissive assumption)} \\ wenzelm@8619 65 \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\ wenzelm@8619 66 % & & \text{(definitional assumption)} \\ wenzelm@8619 67 \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\ wenzelm@8619 68 % & & \text{(generalized existence)} \\ wenzelm@8619 69 \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\ wenzelm@8619 70 % & & \text{(named context)} \\[0.5ex] wenzelm@8511 71 \SORRY & \approx & \BY{cheating} \\ wenzelm@7974 72 \end{matharray} wenzelm@7974 73 wenzelm@7974 74 wenzelm@7974 75 \subsection{Diagnostic commands} wenzelm@7974 76 wenzelm@7974 77 \begin{matharray}{ll} wenzelm@8486 78 \isarkeyword{pr} & \text{print current state} \\ wenzelm@8513 79 \isarkeyword{thm}~\vec a & \text{print theorems} \\ wenzelm@8447 80 \isarkeyword{term}~t & \text{print term} \\ wenzelm@8447 81 \isarkeyword{prop}~\phi & \text{print meta-level proposition} \\ wenzelm@8447 82 \isarkeyword{typ}~\tau & \text{print meta-level type} \\ wenzelm@8447 83 \isarkeyword{print_facts} & \text{print named facts} \\ wenzelm@8447 84 \isarkeyword{print_binds} & \text{print term abbreviations} \\ wenzelm@8447 85 \isarkeyword{print_cases} & \text{print named cases} \\ wenzelm@7974 86 \end{matharray} wenzelm@7974 87 wenzelm@7974 88 wenzelm@7974 89 \section{Proof methods} wenzelm@7974 90 wenzelm@7974 91 \begin{tabular}{ll} wenzelm@7976 92 \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex] wenzelm@7987 93 $assumption$ & apply some assumption \\ wenzelm@8195 94 $this$ & apply current facts \\ wenzelm@8513 95 $rule~\vec a$ & apply some rule \\ wenzelm@7974 96 $rule$ & apply standard rule (default for $\PROOFNAME$) \\ wenzelm@8447 97 $contradiction$ & apply $\neg{}$ elimination rule (any order) \\ wenzelm@8547 98 $cases~t$ & case analysis (provides cases) \\ wenzelm@8547 99 $induct~\vec x$ & proof by induction (provides cases) \\[2ex] wenzelm@7974 100 wenzelm@7976 101 \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex] wenzelm@7974 102 $-$ & \text{no rules} \\ wenzelm@8513 103 $intro~\vec a$ & \text{introduction rules} \\ wenzelm@8513 104 $intro_classes$ & \text{class introduction rules} \\ wenzelm@8513 105 $elim~\vec a$ & \text{elimination rules} \\ wenzelm@8513 106 $unfold~\vec a$ & \text{definitions} \\[2ex] wenzelm@7974 107 wenzelm@7974 108 \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex] wenzelm@8486 109 $simp$ & Simplifier (+ Splitter) \\ wenzelm@7987 110 $blast$, $fast$ & Classical Reasoner \\ wenzelm@7987 111 $force$, $auto$ & Simplifier + Classical Reasoner \\ wenzelm@7974 112 $arith$ & Arithmetic procedure \\ wenzelm@7974 113 \end{tabular} wenzelm@7974 114 wenzelm@7974 115 wenzelm@7974 116 \section{Attributes} wenzelm@7974 117 wenzelm@7974 118 \begin{tabular}{ll} wenzelm@8511 119 \multicolumn{2}{l}{\textbf{Manipulate rules}} \\[0.5ex] wenzelm@8513 120 $OF~\vec a$ & apply rule to facts (skipping $_$'') \\ wenzelm@8513 121 $of~\vec t$ & apply rule to terms (skipping $_$'') \\ wenzelm@7976 122 $RS~b$ & resolve fact with rule \\ wenzelm@7974 123 $standard$ & put into standard result form \\ wenzelm@7976 124 $rulify$ & put into object-rule form \\ wenzelm@7974 125 $elimify$ & put destruction rule into elimination form \\[1ex] wenzelm@7974 126 wenzelm@8486 127 \multicolumn{2}{l}{\textbf{Declare rules}} \\[0.5ex] wenzelm@7974 128 $simp$ & declare Simplifier rules \\ wenzelm@8486 129 $split$ & declare Splitter rules \\ wenzelm@9408 130 $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also !'' or ?'') \\ wenzelm@7987 131 $iff$ & declare Simplifier + Classical Reasoner rules \\ wenzelm@7987 132 $trans$ & declare calculational rules (general transitivity) \\ wenzelm@7974 133 \end{tabular} wenzelm@7974 134 wenzelm@8511 135 wenzelm@8511 136 \section{Emulating tactic scripts} wenzelm@8511 137 wenzelm@8547 138 \subsection{Commands} wenzelm@8511 139 wenzelm@8511 140 \begin{tabular}{ll} wenzelm@8547 141 $\isarkeyword{apply}~(m)$ & apply proof method at initial position \\ wenzelm@8547 142 $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\ wenzelm@8511 143 $\isarkeyword{defer}~n$ & move subgoal to end \\ wenzelm@8511 144 $\isarkeyword{prefer}~n$ & move subgoal to beginning \\ wenzelm@8511 145 $\isarkeyword{back}$ & backtrack last command \\ wenzelm@8511 146 \end{tabular} wenzelm@8511 147 wenzelm@8547 148 \subsection{Methods} wenzelm@8511 149 wenzelm@8511 150 \begin{tabular}{ll} wenzelm@8511 151 $tactic~text$ & method from ML tactic \\ wenzelm@8691 152 $insert~\vec a$ & insert theorems (ignoring current facts) \\ wenzelm@8530 153 $res_inst_tac~insts$ & resolution with instantiation \\ wenzelm@8530 154 $eres_inst_tac~insts$ & elim-resolution with instantiation \\ wenzelm@8530 155 $dres_inst_tac~insts$ & destruct-resolution with instantiation \\ wenzelm@8530 156 $forw_inst_tac~insts$ & forward-resolution with instantiation \\ wenzelm@8530 157 $subgoal_tac~\phi$ & insert new claim \\ wenzelm@8691 158 $case_tac~t$ & exhaustion (datatypes) \\ wenzelm@8691 159 $induct_tac~\vec x$ & induction (datatypes) \\ wenzelm@8511 160 \end{tabular} wenzelm@8511 161 wenzelm@8511 162 wenzelm@7897 163 %%% Local Variables: wenzelm@7897 164 %%% mode: latex wenzelm@7897 165 %%% TeX-master: "isar-ref" wenzelm@7897 166 %%% End: