doc-src/IsarRef/refcard.tex
author haftmann
Fri Dec 29 12:11:04 2006 +0100 (2006-12-29)
changeset 21927 9677abe5d374
parent 19990 837f1b10722c
child 24176 9620a57a5a57
permissions -rw-r--r--
added handling for explicit classrel witnesses
wenzelm@7897
     1
wenzelm@13048
     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@13017
    11
  $\THEN$ & indicate forward chaining of facts \\
wenzelm@7974
    12
  $\HAVE{a}{\phi}$ & prove local result \\
wenzelm@19990
    13
  $\SHOW{a}{\phi}$ & prove local result, refining some goal \\
wenzelm@13017
    14
  $\USING{\vec a}$ & indicate use of additional facts \\
wenzelm@19990
    15
  $\UNFOLDING{\vec a}$ & unfold definitional equations \\
wenzelm@19990
    16
  $\PROOF{m@1}~\dots~\QED{m@2}$ & indicate proof structure and refinements \\
wenzelm@7974
    17
  $\BG~\dots~\EN$ & declare explicit blocks \\
wenzelm@19990
    18
  $\NEXT$ & switch blocks \\
wenzelm@8511
    19
  $\NOTE{a}{\vec b}$ & reconsider facts \\
wenzelm@9695
    20
  $\LET{p = t}$ & \Text{abbreviate terms by higher-order matching} \\
wenzelm@7974
    21
\end{tabular}
wenzelm@7974
    22
wenzelm@7974
    23
\begin{matharray}{rcl}
wenzelm@19990
    24
  theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \Or \isarkeyword{definition}~\dots \Or \dots \\[1ex]
wenzelm@19990
    25
  proof & = & prfx^*~\PROOF{method}~stmt^*~\QED{method} \\
wenzelm@19990
    26
  & \Or & prfx^*~\DONE \\[1ex]
wenzelm@13024
    27
  prfx & = & \APPLY{method} \\
wenzelm@13024
    28
  & \Or & \USING{name^+} \\
wenzelm@19990
    29
  & \Or & \UNFOLDING{name^+} \\
wenzelm@7974
    30
  stmt & = & \BG~stmt^*~\EN \\
wenzelm@8447
    31
  & \Or & \NEXT \\
wenzelm@7974
    32
  & \Or & \NOTE{name}{name^+} \\
wenzelm@19990
    33
  & \Or & \LET{term = term} \\
wenzelm@7974
    34
  & \Or & \FIX{var^+} \\
wenzelm@7987
    35
  & \Or & \ASSUME{name}{prop^+}\\
wenzelm@19990
    36
  & \Or & \THEN^?~goal \\
wenzelm@13024
    37
  goal & = & \HAVE{name}{prop}~proof \\
wenzelm@7987
    38
  & \Or & \SHOW{name}{prop}~proof \\
wenzelm@7974
    39
\end{matharray}
wenzelm@7974
    40
wenzelm@7974
    41
wenzelm@7974
    42
\subsection{Abbreviations and synonyms}
wenzelm@7974
    43
wenzelm@7974
    44
\begin{matharray}{rcl}
wenzelm@7974
    45
  \BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\
wenzelm@7974
    46
  \DDOT & \equiv & \BY{rule} \\
wenzelm@8195
    47
  \DOT & \equiv & \BY{this} \\
wenzelm@7974
    48
  \HENCENAME & \equiv & \THEN~\HAVENAME \\
wenzelm@7974
    49
  \THUSNAME & \equiv & \THEN~\SHOWNAME \\
wenzelm@8511
    50
  \FROM{\vec a} & \equiv & \NOTE{this}{\vec a}~\THEN \\
wenzelm@13041
    51
  \WITH{\vec a} & \equiv & \FROM{\vec a~\AND~this} \\[1ex]
wenzelm@7974
    52
  \FROM{this} & \equiv & \THEN \\
wenzelm@7974
    53
  \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\
wenzelm@7974
    54
  \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\
wenzelm@7974
    55
\end{matharray}
wenzelm@7974
    56
wenzelm@7974
    57
wenzelm@7974
    58
\subsection{Derived elements}
wenzelm@7974
    59
wenzelm@7974
    60
\begin{matharray}{rcl}
wenzelm@7974
    61
  \ALSO@0 & \approx & \NOTE{calculation}{this} \\
wenzelm@7974
    62
  \ALSO@{n+1} & \approx & \NOTE{calculation}{trans~[OF~calculation~this]} \\
wenzelm@8511
    63
  \FINALLY & \approx & \ALSO~\FROM{calculation} \\[0.5ex]
wenzelm@8619
    64
  \MOREOVER & \approx & \NOTE{calculation}{calculation~this} \\
wenzelm@8619
    65
  \ULTIMATELY & \approx & \MOREOVER~\FROM{calculation} \\[0.5ex]
wenzelm@8619
    66
  \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi} \\
wenzelm@9695
    67
%  & & \Text{(permissive assumption)} \\
wenzelm@8619
    68
  \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\
wenzelm@9695
    69
%  & & \Text{(definitional assumption)} \\
wenzelm@8619
    70
  \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
wenzelm@9695
    71
%  & & \Text{(generalized existence)} \\
wenzelm@8619
    72
  \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\
wenzelm@9695
    73
%  & & \Text{(named context)} \\[0.5ex]
wenzelm@8511
    74
  \SORRY & \approx & \BY{cheating} \\
wenzelm@7974
    75
\end{matharray}
wenzelm@7974
    76
wenzelm@7974
    77
wenzelm@7974
    78
\subsection{Diagnostic commands}
wenzelm@7974
    79
wenzelm@7974
    80
\begin{matharray}{ll}
wenzelm@9695
    81
  \isarkeyword{pr} & \Text{print current state} \\
wenzelm@9695
    82
  \isarkeyword{thm}~\vec a & \Text{print theorems} \\
wenzelm@9695
    83
  \isarkeyword{term}~t & \Text{print term} \\
wenzelm@9695
    84
  \isarkeyword{prop}~\phi & \Text{print meta-level proposition} \\
wenzelm@9695
    85
  \isarkeyword{typ}~\tau & \Text{print meta-level type} \\
wenzelm@7974
    86
\end{matharray}
wenzelm@7974
    87
wenzelm@7974
    88
wenzelm@7974
    89
\section{Proof methods}
wenzelm@7974
    90
wenzelm@7974
    91
\begin{tabular}{ll}
wenzelm@7976
    92
  \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
wenzelm@7987
    93
  $assumption$ & apply some assumption \\
wenzelm@8195
    94
  $this$ & apply current facts \\
wenzelm@8513
    95
  $rule~\vec a$ & apply some rule  \\
wenzelm@7974
    96
  $rule$ & apply standard rule (default for $\PROOFNAME$) \\
wenzelm@8447
    97
  $contradiction$ & apply $\neg{}$ elimination rule (any order) \\
wenzelm@8547
    98
  $cases~t$ & case analysis (provides cases) \\
wenzelm@8547
    99
  $induct~\vec x$ & proof by induction (provides cases) \\[2ex]
wenzelm@7974
   100
wenzelm@7976
   101
  \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
wenzelm@9695
   102
  $-$ & \Text{no rules} \\
wenzelm@9695
   103
  $intro~\vec a$ & \Text{introduction rules} \\
wenzelm@9695
   104
  $intro_classes$ & \Text{class introduction rules} \\
wenzelm@9695
   105
  $elim~\vec a$ & \Text{elimination rules} \\
wenzelm@9695
   106
  $unfold~\vec a$ & \Text{definitions} \\[2ex]
wenzelm@7974
   107
wenzelm@7974
   108
  \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
wenzelm@13024
   109
  $rules$ & \Text{intuitionistic proof search} \\
wenzelm@13472
   110
  $blast$, $fast$ & Classical Reasoner \\
wenzelm@9603
   111
  $simp$, $simp_all$ & Simplifier (+ Splitter) \\
wenzelm@9603
   112
  $auto$, $force$ & Simplifier + Classical Reasoner \\
wenzelm@7974
   113
  $arith$ & Arithmetic procedure \\
wenzelm@7974
   114
\end{tabular}
wenzelm@7974
   115
wenzelm@7974
   116
wenzelm@7974
   117
\section{Attributes}
wenzelm@7974
   118
wenzelm@7974
   119
\begin{tabular}{ll}
wenzelm@9905
   120
  \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
ballarin@14175
   121
  $OF~\vec a$ & rule resolved with facts (skipping ``$_$'') \\
ballarin@14175
   122
  $of~\vec t$ & rule instantiated with terms (skipping ``$_$'') \\
ballarin@14175
   123
  $where~\vec x = \vec t$ & rule instantiated with terms, by variable name \\
wenzelm@13041
   124
  $symmetric$ & resolution with symmetry rule \\
wenzelm@13041
   125
  $THEN~b$ & resolution with another rule \\
wenzelm@9941
   126
  $rule_format$ & result put into standard rule format \\
wenzelm@13041
   127
  $elim_format$ & destruct rule turned into elimination rule format \\[1ex]
wenzelm@7974
   128
wenzelm@9905
   129
  \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
wenzelm@9905
   130
  $simp$ & Simplifier rule \\
wenzelm@13041
   131
  $intro$, $elim$, $dest$ & Pure or Classical Reasoner rule \\
wenzelm@9905
   132
  $iff$ & Simplifier + Classical Reasoner rule \\
wenzelm@9905
   133
  $split$ & case split rule \\
wenzelm@9905
   134
  $trans$ & transitivity rule \\
wenzelm@13041
   135
  $sym$ & symmetry rule \\
wenzelm@7974
   136
\end{tabular}
wenzelm@7974
   137
wenzelm@8511
   138
wenzelm@13472
   139
\section{Rule declarations and methods}
wenzelm@13472
   140
wenzelm@13472
   141
\begin{tabular}{l|lllll}
wenzelm@13472
   142
                          & $rule$   & $rules$  & $blast$ etc. & $simp$ etc. & $auto$ etc. \\
wenzelm@13472
   143
  \hline
wenzelm@13472
   144
  $elim!$ $intro!$ (Pure) & $\times$ & $\times$ \\
wenzelm@13472
   145
  $elim$ $intro$ (Pure)   & $\times$ & $\times$ \\
wenzelm@13472
   146
  $elim!$ $intro!$        & $\times$ &          & $\times$     &             & $\times$ \\
wenzelm@13472
   147
  $elim$ $intro$          & $\times$ &          & $\times$     &             & $\times$ \\
wenzelm@13472
   148
  $iff$                   & $\times$ &          & $\times$     & $\times$    & $\times$ \\
wenzelm@13472
   149
  $iff?$                  & $\times$ \\
wenzelm@13472
   150
  $elim?$ $intro?$        & $\times$ \\
wenzelm@13472
   151
  $simp$                  &          &          &              & $\times$    & $\times$ \\
wenzelm@13472
   152
  $cong$                  &          &          &              & $\times$    & $\times$ \\
wenzelm@13472
   153
  $split$                 &          &          &              & $\times$    & $\times$ \\
wenzelm@13472
   154
\end{tabular}
wenzelm@13472
   155
wenzelm@13472
   156
wenzelm@8511
   157
\section{Emulating tactic scripts}
wenzelm@8511
   158
wenzelm@8547
   159
\subsection{Commands}
wenzelm@8511
   160
wenzelm@8511
   161
\begin{tabular}{ll}
wenzelm@10223
   162
  $\APPLY{m}$ & apply proof method at initial position \\
wenzelm@8547
   163
  $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\
wenzelm@9615
   164
  $\isarkeyword{done}$ & complete proof \\
wenzelm@8511
   165
  $\isarkeyword{defer}~n$ & move subgoal to end \\
wenzelm@8511
   166
  $\isarkeyword{prefer}~n$ & move subgoal to beginning \\
wenzelm@8511
   167
  $\isarkeyword{back}$ & backtrack last command \\
wenzelm@9615
   168
  $\isarkeyword{declare}$ & declare rules in current theory \\
wenzelm@8511
   169
\end{tabular}
wenzelm@8511
   170
wenzelm@8547
   171
\subsection{Methods}
wenzelm@8511
   172
wenzelm@8511
   173
\begin{tabular}{ll}
wenzelm@9615
   174
  $rule_tac~insts$ & resolution (with instantiation) \\
wenzelm@9615
   175
  $erule_tac~insts$ & elim-resolution (with instantiation) \\
wenzelm@9615
   176
  $drule_tac~insts$ & destruct-resolution (with instantiation) \\
wenzelm@9615
   177
  $frule_tac~insts$ & forward-resolution (with instantiation) \\
wenzelm@9615
   178
  $cut_tac~insts$ & insert facts (with instantiation) \\
wenzelm@9615
   179
  $thin_tac~\phi$ & delete assumptions \\
wenzelm@9615
   180
  $subgoal_tac~\phi$ & new claims \\
wenzelm@9615
   181
  $rename_tac~\vec x$ & rename suffix of goal parameters \\
wenzelm@9615
   182
  $rotate_tac~n$ & rotate assumptions of goal \\
wenzelm@9615
   183
  $tactic~text$ & arbitrary ML tactic \\
wenzelm@8691
   184
  $case_tac~t$ & exhaustion (datatypes) \\
wenzelm@8691
   185
  $induct_tac~\vec x$ & induction (datatypes) \\
wenzelm@9615
   186
  $ind_cases~t$ & exhaustion + simplification (inductive sets) \\
wenzelm@8511
   187
\end{tabular}
wenzelm@8511
   188
wenzelm@8511
   189
wenzelm@9615
   190
%%% Local Variables:
wenzelm@7897
   191
%%% mode: latex
wenzelm@7897
   192
%%% TeX-master: "isar-ref"
wenzelm@9615
   193
%%% End: