doc-src/IsarRef/refcard.tex
author wenzelm
Sun Jul 23 12:01:05 2000 +0200 (2000-07-23)
changeset 9408 d3d56e1d2ec1
parent 9233 8c8399b9ecaa
child 9603 816917b6c2de
permissions -rw-r--r--
classical atts now intro! / intro / intro?;
     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   \isarkeyword{print_facts} & \text{print named facts} \\
    84   \isarkeyword{print_binds} & \text{print term abbreviations} \\
    85   \isarkeyword{print_cases} & \text{print named cases} \\
    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   $simp$ & Simplifier (+ Splitter) \\
   110   $blast$, $fast$ & Classical Reasoner \\
   111   $force$, $auto$ & Simplifier + Classical Reasoner \\
   112   $arith$ & Arithmetic procedure \\
   113 \end{tabular}
   114 
   115 
   116 \section{Attributes}
   117 
   118 \begin{tabular}{ll}
   119   \multicolumn{2}{l}{\textbf{Manipulate rules}} \\[0.5ex]
   120   $OF~\vec a$ & apply rule to facts (skipping ``$_$'') \\
   121   $of~\vec t$ & apply rule to terms (skipping ``$_$'') \\
   122   $RS~b$ & resolve fact with rule \\
   123   $standard$ & put into standard result form \\
   124   $rulify$ & put into object-rule form \\
   125   $elimify$ & put destruction rule into elimination form \\[1ex]
   126 
   127   \multicolumn{2}{l}{\textbf{Declare rules}} \\[0.5ex]
   128   $simp$ & declare Simplifier rules \\
   129   $split$ & declare Splitter rules \\
   130   $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``!'' or ``?'') \\
   131   $iff$ & declare Simplifier + Classical Reasoner rules \\
   132   $trans$ & declare calculational rules (general transitivity) \\
   133 \end{tabular}
   134 
   135 
   136 \section{Emulating tactic scripts}
   137 
   138 \subsection{Commands}
   139 
   140 \begin{tabular}{ll}
   141   $\isarkeyword{apply}~(m)$ & apply proof method at initial position \\
   142   $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\
   143   $\isarkeyword{defer}~n$ & move subgoal to end \\
   144   $\isarkeyword{prefer}~n$ & move subgoal to beginning \\
   145   $\isarkeyword{back}$ & backtrack last command \\
   146 \end{tabular}
   147 
   148 \subsection{Methods}
   149 
   150 \begin{tabular}{ll}
   151   $tactic~text$ & method from ML tactic \\
   152   $insert~\vec a$ & insert theorems (ignoring current facts) \\
   153   $res_inst_tac~insts$ & resolution with instantiation \\
   154   $eres_inst_tac~insts$ & elim-resolution with instantiation \\
   155   $dres_inst_tac~insts$ & destruct-resolution with instantiation \\
   156   $forw_inst_tac~insts$ & forward-resolution with instantiation \\
   157   $subgoal_tac~\phi$ & insert new claim \\
   158   $case_tac~t$ & exhaustion (datatypes) \\
   159   $induct_tac~\vec x$ & induction (datatypes) \\
   160 \end{tabular}
   161 
   162 
   163 %%% Local Variables: 
   164 %%% mode: latex
   165 %%% TeX-master: "isar-ref"
   166 %%% End: