doc-src/IsarRef/refcard.tex
 author wenzelm Tue Sep 12 22:13:23 2000 +0200 (2000-09-12) changeset 9941 fe05af7ec816 parent 9905 14a71104a498 child 10223 31346d22bb54 permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
 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@9695  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@9695  64 % & & \Text{(permissive assumption)} \\  wenzelm@8619  65  \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\  wenzelm@9695  66 % & & \Text{(definitional assumption)} \\  wenzelm@8619  67  \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\  wenzelm@9695  68 % & & \Text{(generalized existence)} \\  wenzelm@8619  69  \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\  wenzelm@9695  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@9695  78  \isarkeyword{pr} & \Text{print current state} \\  wenzelm@9695  79  \isarkeyword{thm}~\vec a & \Text{print theorems} \\  wenzelm@9695  80  \isarkeyword{term}~t & \Text{print term} \\  wenzelm@9695  81  \isarkeyword{prop}~\phi & \Text{print meta-level proposition} \\  wenzelm@9695  82  \isarkeyword{typ}~\tau & \Text{print meta-level type} \\  wenzelm@7974  83 \end{matharray}  wenzelm@7974  84 wenzelm@7974  85 wenzelm@7974  86 \section{Proof methods}  wenzelm@7974  87 wenzelm@7974  88 \begin{tabular}{ll}  wenzelm@7976  89  \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]  wenzelm@7987  90  $assumption$ & apply some assumption \\  wenzelm@8195  91  $this$ & apply current facts \\  wenzelm@8513  92  $rule~\vec a$ & apply some rule \\  wenzelm@7974  93  $rule$ & apply standard rule (default for $\PROOFNAME$) \\  wenzelm@8447  94  $contradiction$ & apply $\neg{}$ elimination rule (any order) \\  wenzelm@8547  95  $cases~t$ & case analysis (provides cases) \\  wenzelm@8547  96  $induct~\vec x$ & proof by induction (provides cases) \\[2ex]  wenzelm@7974  97 wenzelm@7976  98  \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]  wenzelm@9695  99  $-$ & \Text{no rules} \\  wenzelm@9695  100  $intro~\vec a$ & \Text{introduction rules} \\  wenzelm@9695  101  $intro_classes$ & \Text{class introduction rules} \\  wenzelm@9695  102  $elim~\vec a$ & \Text{elimination rules} \\  wenzelm@9695  103  $unfold~\vec a$ & \Text{definitions} \\[2ex]  wenzelm@7974  104 wenzelm@7974  105  \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]  wenzelm@9603  106  $simp$, $simp_all$ & Simplifier (+ Splitter) \\  wenzelm@7987  107  $blast$, $fast$ & Classical Reasoner \\  wenzelm@9603  108  $auto$, $force$ & Simplifier + Classical Reasoner \\  wenzelm@7974  109  $arith$ & Arithmetic procedure \\  wenzelm@7974  110 \end{tabular}  wenzelm@7974  111 wenzelm@7974  112 wenzelm@7974  113 \section{Attributes}  wenzelm@7974  114 wenzelm@7974  115 \begin{tabular}{ll}  wenzelm@9905  116  \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]  wenzelm@9905  117  $OF~\vec a$ & rule applied to facts (skipping $_$'') \\  wenzelm@9905  118  $of~\vec t$ & rule applied to terms (skipping $_$'') \\  wenzelm@9905  119  $symmetric$ & resolution with symmetry of equality \\  wenzelm@9905  120  $THEN~b$ & resolution with other rule \\  wenzelm@9941  121  $rule_format$ & result put into standard rule format \\  wenzelm@9941  122  $elim_format$ & destruct rule turned into elimination rule format \\  wenzelm@9905  123  $standard$ & result put into standard form \\[1ex]  wenzelm@7974  124 wenzelm@9905  125  \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]  wenzelm@9905  126  $simp$ & Simplifier rule \\  wenzelm@9905  127  $intro$, $elim$, $dest$ & Classical Reasoner rule \\  wenzelm@9905  128  $iff$ & Simplifier + Classical Reasoner rule \\  wenzelm@9905  129  $split$ & case split rule \\  wenzelm@9905  130  $trans$ & transitivity rule \\  wenzelm@7974  131 \end{tabular}  wenzelm@7974  132 wenzelm@8511  133 wenzelm@8511  134 \section{Emulating tactic scripts}  wenzelm@8511  135 wenzelm@8547  136 \subsection{Commands}  wenzelm@8511  137 wenzelm@8511  138 \begin{tabular}{ll}  wenzelm@8547  139  $\isarkeyword{apply}~(m)$ & apply proof method at initial position \\  wenzelm@8547  140  $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\  wenzelm@9615  141  $\isarkeyword{done}$ & complete proof \\  wenzelm@8511  142  $\isarkeyword{defer}~n$ & move subgoal to end \\  wenzelm@8511  143  $\isarkeyword{prefer}~n$ & move subgoal to beginning \\  wenzelm@8511  144  $\isarkeyword{back}$ & backtrack last command \\  wenzelm@9615  145  $\isarkeyword{declare}$ & declare rules in current theory \\  wenzelm@8511  146 \end{tabular}  wenzelm@8511  147 wenzelm@8547  148 \subsection{Methods}  wenzelm@8511  149 wenzelm@8511  150 \begin{tabular}{ll}  wenzelm@9615  151  $rule_tac~insts$ & resolution (with instantiation) \\  wenzelm@9615  152  $erule_tac~insts$ & elim-resolution (with instantiation) \\  wenzelm@9615  153  $drule_tac~insts$ & destruct-resolution (with instantiation) \\  wenzelm@9615  154  $frule_tac~insts$ & forward-resolution (with instantiation) \\  wenzelm@9615  155  $cut_tac~insts$ & insert facts (with instantiation) \\  wenzelm@9615  156  $thin_tac~\phi$ & delete assumptions \\  wenzelm@9615  157  $subgoal_tac~\phi$ & new claims \\  wenzelm@9615  158  $rename_tac~\vec x$ & rename suffix of goal parameters \\  wenzelm@9615  159  $rotate_tac~n$ & rotate assumptions of goal \\  wenzelm@9615  160  $tactic~text$ & arbitrary ML tactic \\  wenzelm@8691  161  $case_tac~t$ & exhaustion (datatypes) \\  wenzelm@8691  162  $induct_tac~\vec x$ & induction (datatypes) \\  wenzelm@9615  163  $ind_cases~t$ & exhaustion + simplification (inductive sets) \\  wenzelm@8511  164 \end{tabular}  wenzelm@8511  165 wenzelm@8511  166 wenzelm@9615  167 %%% Local Variables:  wenzelm@7897  168 %%% mode: latex  wenzelm@7897  169 %%% TeX-master: "isar-ref"  wenzelm@9615  170 %%% End: