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