doc-src/IsarRef/refcard.tex
 author wenzelm Sat Feb 05 16:54:27 2000 +0100 (2000-02-05) changeset 8195 af2575a5c5ae parent 7987 d9aef93c0e32 child 8203 2fcc6017cb72 permissions -rw-r--r--
'.' == by this;
     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{x}$ & augment context by $\All x \Box$ \\

    10   $\ASSUME{a}{\phi}$ & augment context by $\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   $\isarcmd{next}$ & switch implicit blocks \\

    17   $\NOTE{a}{a@1\;\dots\;a@n}$ & 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 & \isarcmd{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{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\

    48   \WITH{a@1\;\dots\;a@n} & \equiv & \FROM{a@1\;\dots\;a@n~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} \\

    61   \PRESUME{a}{\phi} & \approx & \ASSUME{a}{\phi} \\

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

    63   \isarcmd{sorry} & \approx & \BY{cheating} \\

    64 \end{matharray}

    65

    66

    67 \subsection{Diagnostic commands}

    68

    69 \begin{matharray}{ll}

    70   \isarcmd{thm}~a@1\;\dots\;a@n & \text{print theorems} \\

    71   \isarcmd{term}~t & \text{print term} \\

    72   \isarcmd{prop}~\phi & \text{print meta-level proposition} \\

    73   \isarcmd{typ}~\tau & \text{print meta-level type} \\

    74 \end{matharray}

    75

    76

    77 \section{Proof methods}

    78

    79 \begin{tabular}{ll}

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

    81   $assumption$ & apply some assumption \\

    82   $this$ & apply current facts \\

    83   $rule~a@1\;\dots\;a@n$ & apply some rule  \\

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

    85   $induct~x$ & apply induction rule \\

    86   $contradiction$ & apply $\neg{}$ elimination rule (any order) \\[2ex]

    87

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

    89   $-$ & \text{no rules} \\

    90   $intro~a@1\;\dots\;a@n$ & \text{introduction rules} \\

    91   $elim~a@1\;\dots\;a@n$ & \text{elimination rules} \\

    92   $unfold~a@1\;\dots\;a@n$ & \text{definitions} \\[2ex]

    93

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

    95   $simp$ & Simplifier \\

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

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

    98   $arith$ & Arithmetic procedure \\

    99 \end{tabular}

   100

   101

   102 \section{Attributes}

   103

   104 \begin{tabular}{ll}

   105   \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]

   106   $OF~a@1\;\dots\;a@n$ & apply rule to facts (skipping $_$'') \\

   107   $of~t@1\;\dots\;t@n$ & apply rule to terms (skipping $_$'') \\

   108   $RS~b$ & resolve fact with rule \\

   109   $standard$ & put into standard result form \\

   110   $rulify$ & put into object-rule form \\

   111   $elimify$ & put destruction rule into elimination form \\[1ex]

   112

   113   \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]

   114   $simp$ & declare Simplifier rules \\

   115   $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also $!$'' or $!!$'') \\

   116   $iff$ & declare Simplifier + Classical Reasoner rules \\

   117   $trans$ & declare calculational rules (general transitivity) \\

   118 \end{tabular}

   119

   120 %%% Local Variables:

   121 %%% mode: latex

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

   123 %%% End: