doc-src/IsarRef/refcard.tex
author wenzelm
Sat Oct 30 20:13:16 1999 +0200 (1999-10-30)
changeset 7981 5120a2a15d06
parent 7976 8005c92a85d7
child 7987 d9aef93c0e32
permissions -rw-r--r--
tuned;
     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 matching} \\
    19 \end{tabular}
    20 
    21 \begin{matharray}{rcl}
    22   theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\
    23   & \Or & \LEMMA{name}{form}~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}{form^+}\\
    32   & \Or & \THEN~goal{\dsh}stmt \\
    33   & \Or & goal{\dsh}stmt \\
    34   goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\
    35   & \Or & \SHOW{name}{form}~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{assumption} \\
    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 assumption \\
    82   $rule~a@1~\dots~a@n$ & apply some rule  \\
    83   $rule$ & apply standard rule (default for $\PROOFNAME$) \\
    84   $induct~x$ & apply induction rule \\
    85   $contradiction$ & apply $\neg{}$ elimination rule \\[2ex]
    86 
    87   \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
    88   $-$ & \text{no rules} \\
    89   $intro~a@1~\dots~a@n$ & \text{introduction rules} \\
    90   $elim~a@1~\dots~a@n$ & \text{elimination rules} \\
    91   $unfold~a@1~\dots~a@n$ & \text{definitions} \\[2ex]
    92 
    93   \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
    94   $simp$ & Simplifier \\
    95   $blast$, $fast$ & Classical reasoner \\
    96   $force$, $auto$ & Simplifier + Classical reasoner \\
    97   $arith$ & Arithmetic procedure \\
    98 \end{tabular}
    99 
   100 
   101 \section{Attributes}
   102 
   103 \begin{tabular}{ll}
   104   \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]
   105   $OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\
   106   $of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\
   107   $RS~b$ & resolve fact with rule \\
   108   $standard$ & put into standard result form \\
   109   $rulify$ & put into object-rule form \\
   110   $elimify$ & put destruction rule into elimination form \\[1ex]
   111 
   112   \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
   113   $simp$ & declare Simplifier rules \\
   114   $intro$, $elim$, $dest$ & declare Classical reasoner rules (also ``$!$'' or ``$!!$'') \\
   115   $iff$ & declare Simplifier + Classical reasoner rules \\
   116   $trans$ & calculational rules (general transitivity) \\
   117 \end{tabular}
   118 
   119 
   120 %%% Local Variables: 
   121 %%% mode: latex
   122 %%% TeX-master: "isar-ref"
   123 %%% End: