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