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;
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@7974
     9
  $\FIX{x}$ & augment context by $\All x \Box$ \\
wenzelm@7974
    10
  $\ASSUME{a}{\phi}$ & augment context by $\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@7974
    16
  $\isarcmd{next}$ & switch implicit blocks \\
wenzelm@7974
    17
  $\NOTE{a}{a@1~\dots~a@n}$ & reconsider facts \\
wenzelm@7974
    18
  $\LET{p = t}$ & \text{abbreviate terms by matching} \\
wenzelm@7974
    19
\end{tabular}
wenzelm@7974
    20
wenzelm@7974
    21
\begin{matharray}{rcl}
wenzelm@7974
    22
  theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\
wenzelm@7974
    23
  & \Or & \LEMMA{name}{form}~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@7974
    27
  & \Or & \isarcmd{next} \\
wenzelm@7974
    28
  & \Or & \NOTE{name}{name^+} \\
wenzelm@7974
    29
  & \Or & \LET{term = term} \\[0.5ex]
wenzelm@7974
    30
  & \Or & \FIX{var^+} \\
wenzelm@7974
    31
  & \Or & \ASSUME{name}{form^+}\\
wenzelm@7974
    32
  & \Or & \THEN~goal{\dsh}stmt \\
wenzelm@7974
    33
  & \Or & goal{\dsh}stmt \\
wenzelm@7974
    34
  goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\
wenzelm@7974
    35
  & \Or & \SHOW{name}{form}~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@7974
    44
  \DOT & \equiv & \BY{assumption} \\
wenzelm@7974
    45
  \HENCENAME & \equiv & \THEN~\HAVENAME \\
wenzelm@7974
    46
  \THUSNAME & \equiv & \THEN~\SHOWNAME \\
wenzelm@7974
    47
  \FROM{a@1~\dots~a@n} & \equiv & \NOTE{this}{a@1~\dots~a@n}~\THEN \\
wenzelm@7974
    48
  \WITH{a@1~\dots~a@n} & \equiv & \FROM{a@1~\dots~a@n~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@7974
    60
  \FINALLY & \approx & \ALSO~\FROM{calculation} \\
wenzelm@7974
    61
  \PRESUME{a}{\phi} & \approx & \ASSUME{a}{\phi} \\
wenzelm@7974
    62
  \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\
wenzelm@7974
    63
  \isarcmd{sorry} & \approx & \BY{cheating} \\
wenzelm@7974
    64
\end{matharray}
wenzelm@7974
    65
wenzelm@7974
    66
wenzelm@7974
    67
\subsection{Diagnostic commands}
wenzelm@7974
    68
wenzelm@7974
    69
\begin{matharray}{ll}
wenzelm@7974
    70
  \isarcmd{thm}~a@1~\dots~a@n & \text{print theorems} \\
wenzelm@7974
    71
  \isarcmd{term}~t & \text{print term} \\
wenzelm@7974
    72
  \isarcmd{prop}~\phi & \text{print meta-level proposition} \\
wenzelm@7974
    73
  \isarcmd{typ}~\tau & \text{print meta-level type} \\
wenzelm@7974
    74
\end{matharray}
wenzelm@7974
    75
wenzelm@7974
    76
wenzelm@7974
    77
\section{Proof methods}
wenzelm@7974
    78
wenzelm@7974
    79
\begin{tabular}{ll}
wenzelm@7976
    80
  \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
wenzelm@7974
    81
  $assumption$ & apply assumption \\
wenzelm@7974
    82
  $rule~a@1~\dots~a@n$ & apply some rule  \\
wenzelm@7974
    83
  $rule$ & apply standard rule (default for $\PROOFNAME$) \\
wenzelm@7974
    84
  $induct~x$ & apply induction rule \\
wenzelm@7974
    85
  $contradiction$ & apply $\neg{}$ elimination rule \\[2ex]
wenzelm@7974
    86
wenzelm@7976
    87
  \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
wenzelm@7974
    88
  $-$ & \text{no rules} \\
wenzelm@7974
    89
  $intro~a@1~\dots~a@n$ & \text{introduction rules} \\
wenzelm@7981
    90
  $elim~a@1~\dots~a@n$ & \text{elimination rules} \\
wenzelm@7981
    91
  $unfold~a@1~\dots~a@n$ & \text{definitions} \\[2ex]
wenzelm@7974
    92
wenzelm@7974
    93
  \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
wenzelm@7974
    94
  $simp$ & Simplifier \\
wenzelm@7974
    95
  $blast$, $fast$ & Classical reasoner \\
wenzelm@7974
    96
  $force$, $auto$ & Simplifier + Classical reasoner \\
wenzelm@7974
    97
  $arith$ & Arithmetic procedure \\
wenzelm@7974
    98
\end{tabular}
wenzelm@7974
    99
wenzelm@7974
   100
wenzelm@7974
   101
\section{Attributes}
wenzelm@7974
   102
wenzelm@7974
   103
\begin{tabular}{ll}
wenzelm@7974
   104
  \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]
wenzelm@7974
   105
  $OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\
wenzelm@7974
   106
  $of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\
wenzelm@7976
   107
  $RS~b$ & resolve fact with rule \\
wenzelm@7974
   108
  $standard$ & put into standard result form \\
wenzelm@7976
   109
  $rulify$ & put into object-rule form \\
wenzelm@7974
   110
  $elimify$ & put destruction rule into elimination form \\[1ex]
wenzelm@7974
   111
wenzelm@7974
   112
  \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
wenzelm@7974
   113
  $simp$ & declare Simplifier rules \\
wenzelm@7974
   114
  $intro$, $elim$, $dest$ & declare Classical reasoner rules (also ``$!$'' or ``$!!$'') \\
wenzelm@7974
   115
  $iff$ & declare Simplifier + Classical reasoner rules \\
wenzelm@7974
   116
  $trans$ & calculational rules (general transitivity) \\
wenzelm@7974
   117
\end{tabular}
wenzelm@7974
   118
wenzelm@7897
   119
wenzelm@7897
   120
%%% Local Variables: 
wenzelm@7897
   121
%%% mode: latex
wenzelm@7897
   122
%%% TeX-master: "isar-ref"
wenzelm@7897
   123
%%% End: