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;
     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 \\

    12   $\HAVE{a}{\phi}$ & prove local result \\

    13   $\SHOW{a}{\phi}$ & prove local result, establishing some goal \\

    14   $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\

    15   $\BG~\dots~\EN$ & declare explicit blocks \\

    16   $\NEXT$ & switch implicit blocks \\

    17   $\NOTE{a}{\vec b}$ & reconsider facts \\

    18   $\LET{p = t}$ & \Text{abbreviate terms by higher-order matching} \\

    19 \end{tabular}

    20

    21 \begin{matharray}{rcl}

    22   theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\

    23   & \Or & \LEMMA{name}{prop}~proof \\

    24   & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex]

    25   proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex]

    26   stmt & = & \BG~stmt^*~\EN \\

    27   & \Or & \NEXT \\

    28   & \Or & \NOTE{name}{name^+} \\

    29   & \Or & \LET{term = term} \\[0.5ex]

    30   & \Or & \FIX{var^+} \\

    31   & \Or & \ASSUME{name}{prop^+}\\

    32   & \Or & \THEN~goal{\dsh}stmt \\

    33   & \Or & goal{\dsh}stmt \\

    34   goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\

    35   & \Or & \SHOW{name}{prop}~proof \\

    36 \end{matharray}

    37

    38

    39 \subsection{Abbreviations and synonyms}

    40

    41 \begin{matharray}{rcl}

    42   \BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\

    43   \DDOT & \equiv & \BY{rule} \\

    44   \DOT & \equiv & \BY{this} \\

    45   \HENCENAME & \equiv & \THEN~\HAVENAME \\

    46   \THUSNAME & \equiv & \THEN~\SHOWNAME \\

    47   \FROM{\vec a} & \equiv & \NOTE{this}{\vec a}~\THEN \\

    48   \WITH{\vec a} & \equiv & \FROM{\vec a~this} \\[1ex]

    49   \FROM{this} & \equiv & \THEN \\

    50   \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\

    51   \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\

    52 \end{matharray}

    53

    54

    55 \subsection{Derived elements}

    56

    57 \begin{matharray}{rcl}

    58   \ALSO@0 & \approx & \NOTE{calculation}{this} \\

    59   \ALSO@{n+1} & \approx & \NOTE{calculation}{trans~[OF~calculation~this]} \\

    60   \FINALLY & \approx & \ALSO~\FROM{calculation} \\[0.5ex]

    61   \MOREOVER & \approx & \NOTE{calculation}{calculation~this} \\

    62   \ULTIMATELY & \approx & \MOREOVER~\FROM{calculation} \\[0.5ex]

    63   \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi} \\

    64 %  & & \Text{(permissive assumption)} \\

    65   \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\

    66 %  & & \Text{(definitional assumption)} \\

    67   \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\

    68 %  & & \Text{(generalized existence)} \\

    69   \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\

    70 %  & & \Text{(named context)} \\[0.5ex]

    71   \SORRY & \approx & \BY{cheating} \\

    72 \end{matharray}

    73

    74

    75 \subsection{Diagnostic commands}

    76

    77 \begin{matharray}{ll}

    78   \isarkeyword{pr} & \Text{print current state} \\

    79   \isarkeyword{thm}~\vec a & \Text{print theorems} \\

    80   \isarkeyword{term}~t & \Text{print term} \\

    81   \isarkeyword{prop}~\phi & \Text{print meta-level proposition} \\

    82   \isarkeyword{typ}~\tau & \Text{print meta-level type} \\

    83 \end{matharray}

    84

    85

    86 \section{Proof methods}

    87

    88 \begin{tabular}{ll}

    89   \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]

    90   $assumption$ & apply some assumption \\

    91   $this$ & apply current facts \\

    92   $rule~\vec a$ & apply some rule  \\

    93   $rule$ & apply standard rule (default for $\PROOFNAME$) \\

    94   $contradiction$ & apply $\neg{}$ elimination rule (any order) \\

    95   $cases~t$ & case analysis (provides cases) \\

    96   $induct~\vec x$ & proof by induction (provides cases) \\[2ex]

    97

    98   \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]

    99   $-$ & \Text{no rules} \\

   100   $intro~\vec a$ & \Text{introduction rules} \\

   101   $intro_classes$ & \Text{class introduction rules} \\

   102   $elim~\vec a$ & \Text{elimination rules} \\

   103   $unfold~\vec a$ & \Text{definitions} \\[2ex]

   104

   105   \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]

   106   $simp$, $simp_all$ & Simplifier (+ Splitter) \\

   107   $blast$, $fast$ & Classical Reasoner \\

   108   $auto$, $force$ & Simplifier + Classical Reasoner \\

   109   $arith$ & Arithmetic procedure \\

   110 \end{tabular}

   111

   112

   113 \section{Attributes}

   114

   115 \begin{tabular}{ll}

   116   \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]

   117   $OF~\vec a$ & rule applied to facts (skipping $_$'') \\

   118   $of~\vec t$ & rule applied to terms (skipping $_$'') \\

   119   $symmetric$ & resolution with symmetry of equality \\

   120   $THEN~b$ & resolution with other rule \\

   121   $rule_format$ & result put into standard rule format \\

   122   $elim_format$ & destruct rule turned into elimination rule format \\

   123   $standard$ & result put into standard form \\[1ex]

   124

   125   \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]

   126   $simp$ & Simplifier rule \\

   127   $intro$, $elim$, $dest$ & Classical Reasoner rule \\

   128   $iff$ & Simplifier + Classical Reasoner rule \\

   129   $split$ & case split rule \\

   130   $trans$ & transitivity rule \\

   131 \end{tabular}

   132

   133

   134 \section{Emulating tactic scripts}

   135

   136 \subsection{Commands}

   137

   138 \begin{tabular}{ll}

   139   $\isarkeyword{apply}~(m)$ & apply proof method at initial position \\

   140   $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\

   141   $\isarkeyword{done}$ & complete proof \\

   142   $\isarkeyword{defer}~n$ & move subgoal to end \\

   143   $\isarkeyword{prefer}~n$ & move subgoal to beginning \\

   144   $\isarkeyword{back}$ & backtrack last command \\

   145   $\isarkeyword{declare}$ & declare rules in current theory \\

   146 \end{tabular}

   147

   148 \subsection{Methods}

   149

   150 \begin{tabular}{ll}

   151   $rule_tac~insts$ & resolution (with instantiation) \\

   152   $erule_tac~insts$ & elim-resolution (with instantiation) \\

   153   $drule_tac~insts$ & destruct-resolution (with instantiation) \\

   154   $frule_tac~insts$ & forward-resolution (with instantiation) \\

   155   $cut_tac~insts$ & insert facts (with instantiation) \\

   156   $thin_tac~\phi$ & delete assumptions \\

   157   $subgoal_tac~\phi$ & new claims \\

   158   $rename_tac~\vec x$ & rename suffix of goal parameters \\

   159   $rotate_tac~n$ & rotate assumptions of goal \\

   160   $tactic~text$ & arbitrary ML tactic \\

   161   $case_tac~t$ & exhaustion (datatypes) \\

   162   $induct_tac~\vec x$ & induction (datatypes) \\

   163   $ind_cases~t$ & exhaustion + simplification (inductive sets) \\

   164 \end{tabular}

   165

   166

   167 %%% Local Variables:

   168 %%% mode: latex

   169 %%% TeX-master: "isar-ref"

   170 %%% End: