doc-src/IsarRef/refcard.tex
 author haftmann Fri Dec 29 12:11:04 2006 +0100 (2006-12-29) changeset 21927 9677abe5d374 parent 19990 837f1b10722c child 24176 9620a57a5a57 permissions -rw-r--r--
added handling for explicit classrel witnesses
 wenzelm@7897  1 wenzelm@13048  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@13017  11  $\THEN$ & indicate forward chaining of facts \\  wenzelm@7974  12  $\HAVE{a}{\phi}$ & prove local result \\  wenzelm@19990  13  $\SHOW{a}{\phi}$ & prove local result, refining some goal \\  wenzelm@13017  14  $\USING{\vec a}$ & indicate use of additional facts \\  wenzelm@19990  15  $\UNFOLDING{\vec a}$ & unfold definitional equations \\  wenzelm@19990  16  $\PROOF{m@1}~\dots~\QED{m@2}$ & indicate proof structure and refinements \\  wenzelm@7974  17  $\BG~\dots~\EN$ & declare explicit blocks \\  wenzelm@19990  18  $\NEXT$ & switch blocks \\  wenzelm@8511  19  $\NOTE{a}{\vec b}$ & reconsider facts \\  wenzelm@9695  20  $\LET{p = t}$ & \Text{abbreviate terms by higher-order matching} \\  wenzelm@7974  21 \end{tabular}  wenzelm@7974  22 wenzelm@7974  23 \begin{matharray}{rcl}  wenzelm@19990  24  theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \Or \isarkeyword{definition}~\dots \Or \dots \\[1ex]  wenzelm@19990  25  proof & = & prfx^*~\PROOF{method}~stmt^*~\QED{method} \\  wenzelm@19990  26  & \Or & prfx^*~\DONE \\[1ex]  wenzelm@13024  27  prfx & = & \APPLY{method} \\  wenzelm@13024  28  & \Or & \USING{name^+} \\  wenzelm@19990  29  & \Or & \UNFOLDING{name^+} \\  wenzelm@7974  30  stmt & = & \BG~stmt^*~\EN \\  wenzelm@8447  31  & \Or & \NEXT \\  wenzelm@7974  32  & \Or & \NOTE{name}{name^+} \\  wenzelm@19990  33  & \Or & \LET{term = term} \\  wenzelm@7974  34  & \Or & \FIX{var^+} \\  wenzelm@7987  35  & \Or & \ASSUME{name}{prop^+}\\  wenzelm@19990  36  & \Or & \THEN^?~goal \\  wenzelm@13024  37  goal & = & \HAVE{name}{prop}~proof \\  wenzelm@7987  38  & \Or & \SHOW{name}{prop}~proof \\  wenzelm@7974  39 \end{matharray}  wenzelm@7974  40 wenzelm@7974  41 wenzelm@7974  42 \subsection{Abbreviations and synonyms}  wenzelm@7974  43 wenzelm@7974  44 \begin{matharray}{rcl}  wenzelm@7974  45  \BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\  wenzelm@7974  46  \DDOT & \equiv & \BY{rule} \\  wenzelm@8195  47  \DOT & \equiv & \BY{this} \\  wenzelm@7974  48  \HENCENAME & \equiv & \THEN~\HAVENAME \\  wenzelm@7974  49  \THUSNAME & \equiv & \THEN~\SHOWNAME \\  wenzelm@8511  50  \FROM{\vec a} & \equiv & \NOTE{this}{\vec a}~\THEN \\  wenzelm@13041  51  \WITH{\vec a} & \equiv & \FROM{\vec a~\AND~this} \\[1ex]  wenzelm@7974  52  \FROM{this} & \equiv & \THEN \\  wenzelm@7974  53  \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\  wenzelm@7974  54  \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\  wenzelm@7974  55 \end{matharray}  wenzelm@7974  56 wenzelm@7974  57 wenzelm@7974  58 \subsection{Derived elements}  wenzelm@7974  59 wenzelm@7974  60 \begin{matharray}{rcl}  wenzelm@7974  61  \ALSO@0 & \approx & \NOTE{calculation}{this} \\  wenzelm@7974  62  \ALSO@{n+1} & \approx & \NOTE{calculation}{trans~[OF~calculation~this]} \\  wenzelm@8511  63  \FINALLY & \approx & \ALSO~\FROM{calculation} \\[0.5ex]  wenzelm@8619  64  \MOREOVER & \approx & \NOTE{calculation}{calculation~this} \\  wenzelm@8619  65  \ULTIMATELY & \approx & \MOREOVER~\FROM{calculation} \\[0.5ex]  wenzelm@8619  66  \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi} \\  wenzelm@9695  67 % & & \Text{(permissive assumption)} \\  wenzelm@8619  68  \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\  wenzelm@9695  69 % & & \Text{(definitional assumption)} \\  wenzelm@8619  70  \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\  wenzelm@9695  71 % & & \Text{(generalized existence)} \\  wenzelm@8619  72  \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\  wenzelm@9695  73 % & & \Text{(named context)} \\[0.5ex]  wenzelm@8511  74  \SORRY & \approx & \BY{cheating} \\  wenzelm@7974  75 \end{matharray}  wenzelm@7974  76 wenzelm@7974  77 wenzelm@7974  78 \subsection{Diagnostic commands}  wenzelm@7974  79 wenzelm@7974  80 \begin{matharray}{ll}  wenzelm@9695  81  \isarkeyword{pr} & \Text{print current state} \\  wenzelm@9695  82  \isarkeyword{thm}~\vec a & \Text{print theorems} \\  wenzelm@9695  83  \isarkeyword{term}~t & \Text{print term} \\  wenzelm@9695  84  \isarkeyword{prop}~\phi & \Text{print meta-level proposition} \\  wenzelm@9695  85  \isarkeyword{typ}~\tau & \Text{print meta-level type} \\  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@9695  102  $-$ & \Text{no rules} \\  wenzelm@9695  103  $intro~\vec a$ & \Text{introduction rules} \\  wenzelm@9695  104  $intro_classes$ & \Text{class introduction rules} \\  wenzelm@9695  105  $elim~\vec a$ & \Text{elimination rules} \\  wenzelm@9695  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@13024  109  $rules$ & \Text{intuitionistic proof search} \\  wenzelm@13472  110  $blast$, $fast$ & Classical Reasoner \\  wenzelm@9603  111  $simp$, $simp_all$ & Simplifier (+ Splitter) \\  wenzelm@9603  112  $auto$, $force$ & Simplifier + Classical Reasoner \\  wenzelm@7974  113  $arith$ & Arithmetic procedure \\  wenzelm@7974  114 \end{tabular}  wenzelm@7974  115 wenzelm@7974  116 wenzelm@7974  117 \section{Attributes}  wenzelm@7974  118 wenzelm@7974  119 \begin{tabular}{ll}  wenzelm@9905  120  \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]  ballarin@14175  121  $OF~\vec a$ & rule resolved with facts (skipping $_$'') \\  ballarin@14175  122  $of~\vec t$ & rule instantiated with terms (skipping $_$'') \\  ballarin@14175  123  $where~\vec x = \vec t$ & rule instantiated with terms, by variable name \\  wenzelm@13041  124  $symmetric$ & resolution with symmetry rule \\  wenzelm@13041  125  $THEN~b$ & resolution with another rule \\  wenzelm@9941  126  $rule_format$ & result put into standard rule format \\  wenzelm@13041  127  $elim_format$ & destruct rule turned into elimination rule format \\[1ex]  wenzelm@7974  128 wenzelm@9905  129  \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]  wenzelm@9905  130  $simp$ & Simplifier rule \\  wenzelm@13041  131  $intro$, $elim$, $dest$ & Pure or Classical Reasoner rule \\  wenzelm@9905  132  $iff$ & Simplifier + Classical Reasoner rule \\  wenzelm@9905  133  $split$ & case split rule \\  wenzelm@9905  134  $trans$ & transitivity rule \\  wenzelm@13041  135  $sym$ & symmetry rule \\  wenzelm@7974  136 \end{tabular}  wenzelm@7974  137 wenzelm@8511  138 wenzelm@13472  139 \section{Rule declarations and methods}  wenzelm@13472  140 wenzelm@13472  141 \begin{tabular}{l|lllll}  wenzelm@13472  142  & $rule$ & $rules$ & $blast$ etc. & $simp$ etc. & $auto$ etc. \\  wenzelm@13472  143  \hline  wenzelm@13472  144  $elim!$ $intro!$ (Pure) & $\times$ & $\times$ \\  wenzelm@13472  145  $elim$ $intro$ (Pure) & $\times$ & $\times$ \\  wenzelm@13472  146  $elim!$ $intro!$ & $\times$ & & $\times$ & & $\times$ \\  wenzelm@13472  147  $elim$ $intro$ & $\times$ & & $\times$ & & $\times$ \\  wenzelm@13472  148  $iff$ & $\times$ & & $\times$ & $\times$ & $\times$ \\  wenzelm@13472  149  $iff?$ & $\times$ \\  wenzelm@13472  150  $elim?$ $intro?$ & $\times$ \\  wenzelm@13472  151  $simp$ & & & & $\times$ & $\times$ \\  wenzelm@13472  152  $cong$ & & & & $\times$ & $\times$ \\  wenzelm@13472  153  $split$ & & & & $\times$ & $\times$ \\  wenzelm@13472  154 \end{tabular}  wenzelm@13472  155 wenzelm@13472  156 wenzelm@8511  157 \section{Emulating tactic scripts}  wenzelm@8511  158 wenzelm@8547  159 \subsection{Commands}  wenzelm@8511  160 wenzelm@8511  161 \begin{tabular}{ll}  wenzelm@10223  162  $\APPLY{m}$ & apply proof method at initial position \\  wenzelm@8547  163  $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\  wenzelm@9615  164  $\isarkeyword{done}$ & complete proof \\  wenzelm@8511  165  $\isarkeyword{defer}~n$ & move subgoal to end \\  wenzelm@8511  166  $\isarkeyword{prefer}~n$ & move subgoal to beginning \\  wenzelm@8511  167  $\isarkeyword{back}$ & backtrack last command \\  wenzelm@9615  168  $\isarkeyword{declare}$ & declare rules in current theory \\  wenzelm@8511  169 \end{tabular}  wenzelm@8511  170 wenzelm@8547  171 \subsection{Methods}  wenzelm@8511  172 wenzelm@8511  173 \begin{tabular}{ll}  wenzelm@9615  174  $rule_tac~insts$ & resolution (with instantiation) \\  wenzelm@9615  175  $erule_tac~insts$ & elim-resolution (with instantiation) \\  wenzelm@9615  176  $drule_tac~insts$ & destruct-resolution (with instantiation) \\  wenzelm@9615  177  $frule_tac~insts$ & forward-resolution (with instantiation) \\  wenzelm@9615  178  $cut_tac~insts$ & insert facts (with instantiation) \\  wenzelm@9615  179  $thin_tac~\phi$ & delete assumptions \\  wenzelm@9615  180  $subgoal_tac~\phi$ & new claims \\  wenzelm@9615  181  $rename_tac~\vec x$ & rename suffix of goal parameters \\  wenzelm@9615  182  $rotate_tac~n$ & rotate assumptions of goal \\  wenzelm@9615  183  $tactic~text$ & arbitrary ML tactic \\  wenzelm@8691  184  $case_tac~t$ & exhaustion (datatypes) \\  wenzelm@8691  185  $induct_tac~\vec x$ & induction (datatypes) \\  wenzelm@9615  186  $ind_cases~t$ & exhaustion + simplification (inductive sets) \\  wenzelm@8511  187 \end{tabular}  wenzelm@8511  188 wenzelm@8511  189 wenzelm@9615  190 %%% Local Variables:  wenzelm@7897  191 %%% mode: latex  wenzelm@7897  192 %%% TeX-master: "isar-ref"  wenzelm@9615  193 %%% End: