24 } |
24 } |
25 \isamarkuptrue% |
25 \isamarkuptrue% |
26 % |
26 % |
27 \begin{isamarkuptext}% |
27 \begin{isamarkuptext}% |
28 Isar Proof methods closely resemble traditional tactics, when used |
28 Isar Proof methods closely resemble traditional tactics, when used |
29 in unstructured sequences of \mbox{\isa{\isacommand{apply}}} commands. |
29 in unstructured sequences of \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} commands. |
30 Isabelle/Isar provides emulations for all major ML tactics of |
30 Isabelle/Isar provides emulations for all major ML tactics of |
31 classic Isabelle --- mostly for the sake of easy porting of existing |
31 classic Isabelle --- mostly for the sake of easy porting of existing |
32 developments, as actual Isar proof texts would demand much less |
32 developments, as actual Isar proof texts would demand much less |
33 diversity of proof methods. |
33 diversity of proof methods. |
34 |
34 |
36 concrete syntax for additional arguments, options, modifiers etc. |
36 concrete syntax for additional arguments, options, modifiers etc. |
37 Thus a typical method text is usually more concise than the |
37 Thus a typical method text is usually more concise than the |
38 corresponding ML tactic. Furthermore, the Isar versions of classic |
38 corresponding ML tactic. Furthermore, the Isar versions of classic |
39 Isabelle tactics often cover several variant forms by a single |
39 Isabelle tactics often cover several variant forms by a single |
40 method with separate options to tune the behavior. For example, |
40 method with separate options to tune the behavior. For example, |
41 method \mbox{\isa{simp}} replaces all of \verb|simp_tac|~/ \verb|asm_simp_tac|~/ \verb|full_simp_tac|~/ \verb|asm_full_simp_tac|, there |
41 method \hyperlink{method.simp}{\mbox{\isa{simp}}} replaces all of \verb|simp_tac|~/ \verb|asm_simp_tac|~/ \verb|full_simp_tac|~/ \verb|asm_full_simp_tac|, there |
42 is also concrete syntax for augmenting the Simplifier context (the |
42 is also concrete syntax for augmenting the Simplifier context (the |
43 current ``simpset'') in a convenient way.% |
43 current ``simpset'') in a convenient way.% |
44 \end{isamarkuptext}% |
44 \end{isamarkuptext}% |
45 \isamarkuptrue% |
45 \isamarkuptrue% |
46 % |
46 % |
65 \item Abbreviations for singleton arguments (e.g.\ \verb|resolve_tac| |
65 \item Abbreviations for singleton arguments (e.g.\ \verb|resolve_tac| |
66 vs.\ \verb|rtac|). |
66 vs.\ \verb|rtac|). |
67 |
67 |
68 \end{enumerate} |
68 \end{enumerate} |
69 |
69 |
70 Basically, the set of Isar tactic emulations \mbox{\isa{rule{\isacharunderscore}tac}}, |
70 Basically, the set of Isar tactic emulations \hyperlink{method.rule_tac}{\mbox{\isa{rule{\isacharunderscore}tac}}}, |
71 \mbox{\isa{erule{\isacharunderscore}tac}}, \mbox{\isa{drule{\isacharunderscore}tac}}, \mbox{\isa{frule{\isacharunderscore}tac}} (see |
71 \hyperlink{method.erule_tac}{\mbox{\isa{erule{\isacharunderscore}tac}}}, \hyperlink{method.drule_tac}{\mbox{\isa{drule{\isacharunderscore}tac}}}, \hyperlink{method.frule_tac}{\mbox{\isa{frule{\isacharunderscore}tac}}} (see |
72 \secref{sec:tactics}) would be sufficient to cover the four modes, |
72 \secref{sec:tactics}) would be sufficient to cover the four modes, |
73 either with or without instantiation, and either with single or |
73 either with or without instantiation, and either with single or |
74 multiple arguments. Although it is more convenient in most cases to |
74 multiple arguments. Although it is more convenient in most cases to |
75 use the plain \mbox{\isa{rule}} method (see |
75 use the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method (see |
76 \secref{sec:pure-meth-att}), or any of its ``improper'' variants |
76 \secref{sec:pure-meth-att}), or any of its ``improper'' variants |
77 \mbox{\isa{erule}}, \mbox{\isa{drule}}, \mbox{\isa{frule}} (see |
77 \hyperlink{method.erule}{\mbox{\isa{erule}}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}, \hyperlink{method.frule}{\mbox{\isa{frule}}} (see |
78 \secref{sec:misc-meth-att}). Note that explicit goal addressing is |
78 \secref{sec:misc-meth-att}). Note that explicit goal addressing is |
79 only supported by the actual \mbox{\isa{rule{\isacharunderscore}tac}} version. |
79 only supported by the actual \hyperlink{method.rule_tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} version. |
80 |
80 |
81 With this in mind, plain resolution tactics correspond to Isar |
81 With this in mind, plain resolution tactics correspond to Isar |
82 methods as follows. |
82 methods as follows. |
83 |
83 |
84 \medskip |
84 \medskip |
93 \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\ |
93 \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\ |
94 \end{tabular} |
94 \end{tabular} |
95 \medskip |
95 \medskip |
96 |
96 |
97 Note that explicit goal addressing may be usually avoided by |
97 Note that explicit goal addressing may be usually avoided by |
98 changing the order of subgoals with \mbox{\isa{\isacommand{defer}}} or \mbox{\isa{\isacommand{prefer}}} (see \secref{sec:tactic-commands}).% |
98 changing the order of subgoals with \hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}} or \hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}} (see \secref{sec:tactic-commands}).% |
99 \end{isamarkuptext}% |
99 \end{isamarkuptext}% |
100 \isamarkuptrue% |
100 \isamarkuptrue% |
101 % |
101 % |
102 \isamarkupsection{Simplifier tactics% |
102 \isamarkupsection{Simplifier tactics% |
103 } |
103 } |
104 \isamarkuptrue% |
104 \isamarkuptrue% |
105 % |
105 % |
106 \begin{isamarkuptext}% |
106 \begin{isamarkuptext}% |
107 The main Simplifier tactics \verb|simp_tac| and variants (cf.\ |
107 The main Simplifier tactics \verb|simp_tac| and variants (cf.\ |
108 \cite{isabelle-ref}) are all covered by the \mbox{\isa{simp}} and |
108 \cite{isabelle-ref}) are all covered by the \hyperlink{method.simp}{\mbox{\isa{simp}}} and |
109 \mbox{\isa{simp{\isacharunderscore}all}} methods (see \secref{sec:simplifier}). Note that |
109 \hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}} methods (see \secref{sec:simplifier}). Note that |
110 there is no individual goal addressing available, simplification |
110 there is no individual goal addressing available, simplification |
111 acts either on the first goal (\mbox{\isa{simp}}) or all goals |
111 acts either on the first goal (\hyperlink{method.simp}{\mbox{\isa{simp}}}) or all goals |
112 (\mbox{\isa{simp{\isacharunderscore}all}}). |
112 (\hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}}). |
113 |
113 |
114 \medskip |
114 \medskip |
115 \begin{tabular}{lll} |
115 \begin{tabular}{lll} |
116 \verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \mbox{\isa{simp}} \\ |
116 \verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}} \\ |
117 \verb|ALLGOALS|~(\verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}{\isachardoublequote}}) & & \mbox{\isa{simp{\isacharunderscore}all}} \\[0.5ex] |
117 \verb|ALLGOALS|~(\verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}{\isachardoublequote}}) & & \hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}} \\[0.5ex] |
118 \verb|simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \mbox{\isa{simp}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}} \\ |
118 \verb|simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}} \\ |
119 \verb|asm_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \mbox{\isa{simp}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} \\ |
119 \verb|asm_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} \\ |
120 \verb|full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \mbox{\isa{simp}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}{\isachardoublequote}} \\ |
120 \verb|full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}{\isachardoublequote}} \\ |
121 \verb|asm_lr_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \mbox{\isa{simp}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharunderscore}lr{\isacharparenright}{\isachardoublequote}} \\ |
121 \verb|asm_lr_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharunderscore}lr{\isacharparenright}{\isachardoublequote}} \\ |
122 \end{tabular} |
122 \end{tabular} |
123 \medskip% |
123 \medskip% |
124 \end{isamarkuptext}% |
124 \end{isamarkuptext}% |
125 \isamarkuptrue% |
125 \isamarkuptrue% |
126 % |
126 % |
129 \isamarkuptrue% |
129 \isamarkuptrue% |
130 % |
130 % |
131 \begin{isamarkuptext}% |
131 \begin{isamarkuptext}% |
132 The Classical Reasoner provides a rather large number of variations |
132 The Classical Reasoner provides a rather large number of variations |
133 of automated tactics, such as \verb|blast_tac|, \verb|fast_tac|, \verb|clarify_tac| etc.\ (see \cite{isabelle-ref}). The corresponding |
133 of automated tactics, such as \verb|blast_tac|, \verb|fast_tac|, \verb|clarify_tac| etc.\ (see \cite{isabelle-ref}). The corresponding |
134 Isar methods usually share the same base name, such as \mbox{\isa{blast}}, \mbox{\isa{fast}}, \mbox{\isa{clarify}} etc.\ (see |
134 Isar methods usually share the same base name, such as \hyperlink{method.blast}{\mbox{\isa{blast}}}, \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.clarify}{\mbox{\isa{clarify}}} etc.\ (see |
135 \secref{sec:classical}).% |
135 \secref{sec:classical}).% |
136 \end{isamarkuptext}% |
136 \end{isamarkuptext}% |
137 \isamarkuptrue% |
137 \isamarkuptrue% |
138 % |
138 % |
139 \isamarkupsection{Miscellaneous tactics% |
139 \isamarkupsection{Miscellaneous tactics% |
165 Classic Isabelle provides a huge amount of tacticals for combination |
165 Classic Isabelle provides a huge amount of tacticals for combination |
166 and modification of existing tactics. This has been greatly reduced |
166 and modification of existing tactics. This has been greatly reduced |
167 in Isar, providing the bare minimum of combinators only: ``\isa{{\isachardoublequote}{\isacharcomma}{\isachardoublequote}}'' (sequential composition), ``\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}'' (alternative |
167 in Isar, providing the bare minimum of combinators only: ``\isa{{\isachardoublequote}{\isacharcomma}{\isachardoublequote}}'' (sequential composition), ``\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}'' (alternative |
168 choices), ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' (try), ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least |
168 choices), ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' (try), ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least |
169 once). These are usually sufficient in practice; if all fails, |
169 once). These are usually sufficient in practice; if all fails, |
170 arbitrary ML tactic code may be invoked via the \mbox{\isa{tactic}} |
170 arbitrary ML tactic code may be invoked via the \hyperlink{method.tactic}{\mbox{\isa{tactic}}} |
171 method (see \secref{sec:tactics}). |
171 method (see \secref{sec:tactics}). |
172 |
172 |
173 \medskip Common ML tacticals may be expressed directly in Isar as |
173 \medskip Common ML tacticals may be expressed directly in Isar as |
174 follows: |
174 follows: |
175 |
175 |
191 well. |
191 well. |
192 |
192 |
193 \medskip \verb|ALLGOALS|, \verb|SOMEGOAL| etc.\ (see |
193 \medskip \verb|ALLGOALS|, \verb|SOMEGOAL| etc.\ (see |
194 \cite{isabelle-ref}) are not available in Isar, since there is no |
194 \cite{isabelle-ref}) are not available in Isar, since there is no |
195 direct goal addressing. Nevertheless, some basic methods address |
195 direct goal addressing. Nevertheless, some basic methods address |
196 all goals internally, notably \mbox{\isa{simp{\isacharunderscore}all}} (see |
196 all goals internally, notably \hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}} (see |
197 \secref{sec:simplifier}). Also note that \verb|ALLGOALS| can be |
197 \secref{sec:simplifier}). Also note that \verb|ALLGOALS| can be |
198 often replaced by ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least once), although |
198 often replaced by ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least once), although |
199 this usually has a different operational behavior, such as solving |
199 this usually has a different operational behavior, such as solving |
200 goals in a different order. |
200 goals in a different order. |
201 |
201 |
202 \medskip Iterated resolution, such as \verb|REPEAT (FIRSTGOAL|\isasep\isanewline% |
202 \medskip Iterated resolution, such as \verb|REPEAT (FIRSTGOAL|\isasep\isanewline% |
203 \verb| (resolve_tac \<dots>))|, is usually better expressed using the \mbox{\isa{intro}} and \mbox{\isa{elim}} methods of Isar (see |
203 \verb| (resolve_tac \<dots>))|, is usually better expressed using the \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} methods of Isar (see |
204 \secref{sec:classical}).% |
204 \secref{sec:classical}).% |
205 \end{isamarkuptext}% |
205 \end{isamarkuptext}% |
206 \isamarkuptrue% |
206 \isamarkuptrue% |
207 % |
207 % |
208 \isadelimtheory |
208 \isadelimtheory |