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