63 \item Abbreviations for singleton arguments (e.g.\ \verb|resolve_tac| |
63 \item Abbreviations for singleton arguments (e.g.\ \verb|resolve_tac| |
64 vs.\ \verb|rtac|). |
64 vs.\ \verb|rtac|). |
65 |
65 |
66 \end{enumerate} |
66 \end{enumerate} |
67 |
67 |
68 Basically, the set of Isar tactic emulations \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}}, |
68 Basically, the set of Isar tactic emulations \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}}, |
69 \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 |
69 \hyperlink{method.erule-tac}{\mbox{\isa{erule{\isaliteral{5F}{\isacharunderscore}}tac}}}, \hyperlink{method.drule-tac}{\mbox{\isa{drule{\isaliteral{5F}{\isacharunderscore}}tac}}}, \hyperlink{method.frule-tac}{\mbox{\isa{frule{\isaliteral{5F}{\isacharunderscore}}tac}}} (see |
70 \secref{sec:tactics}) would be sufficient to cover the four modes, |
70 \secref{sec:tactics}) would be sufficient to cover the four modes, |
71 either with or without instantiation, and either with single or |
71 either with or without instantiation, and either with single or |
72 multiple arguments. Although it is more convenient in most cases to |
72 multiple arguments. Although it is more convenient in most cases to |
73 use the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method (see |
73 use the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method (see |
74 \secref{sec:pure-meth-att}), or any of its ``improper'' variants |
74 \secref{sec:pure-meth-att}), or any of its ``improper'' variants |
75 \hyperlink{method.erule}{\mbox{\isa{erule}}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}, \hyperlink{method.frule}{\mbox{\isa{frule}}} (see |
75 \hyperlink{method.erule}{\mbox{\isa{erule}}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}, \hyperlink{method.frule}{\mbox{\isa{frule}}} (see |
76 \secref{sec:misc-meth-att}). Note that explicit goal addressing is |
76 \secref{sec:misc-meth-att}). Note that explicit goal addressing is |
77 only supported by the actual \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} version. |
77 only supported by the actual \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}} version. |
78 |
78 |
79 With this in mind, plain resolution tactics correspond to Isar |
79 With this in mind, plain resolution tactics correspond to Isar |
80 methods as follows. |
80 methods as follows. |
81 |
81 |
82 \medskip |
82 \medskip |
83 \begin{tabular}{lll} |
83 \begin{tabular}{lll} |
84 \verb|rtac|~\isa{{\isachardoublequote}a\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}rule\ a{\isachardoublequote}} \\ |
84 \verb|rtac|~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}rule\ a{\isaliteral{22}{\isachardoublequote}}} \\ |
85 \verb|resolve_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}rule\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}{\isachardoublequote}} \\ |
85 \verb|resolve_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}rule\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\ |
86 \verb|res_inst_tac|~\isa{{\isachardoublequote}ctxt\ {\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ {\isadigit{1}}{\isachardoublequote}} & & |
86 \verb|res_inst_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}\ a\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & |
87 \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\[0.5ex] |
87 \isa{{\isaliteral{22}{\isachardoublequote}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C494E3E}{\isasymIN}}\ a{\isaliteral{22}{\isachardoublequote}}} \\[0.5ex] |
88 \verb|rtac|~\isa{{\isachardoublequote}a\ i{\isachardoublequote}} & & \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ a{\isachardoublequote}} \\ |
88 \verb|rtac|~\isa{{\isaliteral{22}{\isachardoublequote}}a\ i{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{5B}{\isacharbrackleft}}i{\isaliteral{5D}{\isacharbrackright}}\ a{\isaliteral{22}{\isachardoublequote}}} \\ |
89 \verb|resolve_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ i{\isachardoublequote}} & & \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}{\isachardoublequote}} \\ |
89 \verb|resolve_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}\ i{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{5B}{\isacharbrackleft}}i{\isaliteral{5D}{\isacharbrackright}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\ |
90 \verb|res_inst_tac|~\isa{{\isachardoublequote}ctxt\ {\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ i{\isachardoublequote}} & & |
90 \verb|res_inst_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}\ a\ i{\isaliteral{22}{\isachardoublequote}}} & & |
91 \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\ |
91 \isa{{\isaliteral{22}{\isachardoublequote}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{5B}{\isacharbrackleft}}i{\isaliteral{5D}{\isacharbrackright}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C494E3E}{\isasymIN}}\ a{\isaliteral{22}{\isachardoublequote}}} \\ |
92 \end{tabular} |
92 \end{tabular} |
93 \medskip |
93 \medskip |
94 |
94 |
95 Note that explicit goal addressing may be usually avoided by |
95 Note that explicit goal addressing may be usually avoided by |
96 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}).% |
96 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}).% |
102 \isamarkuptrue% |
102 \isamarkuptrue% |
103 % |
103 % |
104 \begin{isamarkuptext}% |
104 \begin{isamarkuptext}% |
105 The main Simplifier tactics \verb|simp_tac| and variants (cf.\ |
105 The main Simplifier tactics \verb|simp_tac| and variants (cf.\ |
106 \cite{isabelle-ref}) are all covered by the \hyperlink{method.simp}{\mbox{\isa{simp}}} and |
106 \cite{isabelle-ref}) are all covered by the \hyperlink{method.simp}{\mbox{\isa{simp}}} and |
107 \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} methods (see \secref{sec:simplifier}). Note that |
107 \hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}} methods (see \secref{sec:simplifier}). Note that |
108 there is no individual goal addressing available, simplification |
108 there is no individual goal addressing available, simplification |
109 acts either on the first goal (\hyperlink{method.simp}{\mbox{\isa{simp}}}) or all goals |
109 acts either on the first goal (\hyperlink{method.simp}{\mbox{\isa{simp}}}) or all goals |
110 (\hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}}). |
110 (\hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}}). |
111 |
111 |
112 \medskip |
112 \medskip |
113 \begin{tabular}{lll} |
113 \begin{tabular}{lll} |
114 \verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}} \\ |
114 \verb|asm_full_simp_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}simpset{\isaliteral{7D}{\isacharbraceright}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}} \\ |
115 \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] |
115 \verb|ALLGOALS|~(\verb|asm_full_simp_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}simpset{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}) & & \hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}} \\[0.5ex] |
116 \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}} \\ |
116 \verb|simp_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}simpset{\isaliteral{7D}{\isacharbraceright}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ |
117 \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}} \\ |
117 \verb|asm_simp_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}simpset{\isaliteral{7D}{\isacharbraceright}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ |
118 \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}} \\ |
118 \verb|full_simp_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}simpset{\isaliteral{7D}{\isacharbraceright}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}use{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ |
119 \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}} \\ |
119 \verb|asm_lr_simp_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}simpset{\isaliteral{7D}{\isacharbraceright}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{5F}{\isacharunderscore}}lr{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ |
120 \end{tabular} |
120 \end{tabular} |
121 \medskip% |
121 \medskip% |
122 \end{isamarkuptext}% |
122 \end{isamarkuptext}% |
123 \isamarkuptrue% |
123 \isamarkuptrue% |
124 % |
124 % |
143 Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. |
143 Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. |
144 The most common ones of these may be ported to Isar as follows. |
144 The most common ones of these may be ported to Isar as follows. |
145 |
145 |
146 \medskip |
146 \medskip |
147 \begin{tabular}{lll} |
147 \begin{tabular}{lll} |
148 \verb|stac|~\isa{{\isachardoublequote}a\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}subst\ a{\isachardoublequote}} \\ |
148 \verb|stac|~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}subst\ a{\isaliteral{22}{\isachardoublequote}}} \\ |
149 \verb|hyp_subst_tac|~\isa{{\isadigit{1}}} & & \isa{hypsubst} \\ |
149 \verb|hyp_subst_tac|~\isa{{\isadigit{1}}} & & \isa{hypsubst} \\ |
150 \verb|strip_tac|~\isa{{\isadigit{1}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & \isa{{\isachardoublequote}intro\ strip{\isachardoublequote}} \\ |
150 \verb|strip_tac|~\isa{{\isadigit{1}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C617070726F783E}{\isasymapprox}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}intro\ strip{\isaliteral{22}{\isachardoublequote}}} \\ |
151 \verb|split_all_tac|~\isa{{\isadigit{1}}} & & \isa{{\isachardoublequote}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}\ only{\isacharcolon}\ split{\isacharunderscore}tupled{\isacharunderscore}all{\isachardoublequote}} \\ |
151 \verb|split_all_tac|~\isa{{\isadigit{1}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}simp\ {\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}\ only{\isaliteral{3A}{\isacharcolon}}\ split{\isaliteral{5F}{\isacharunderscore}}tupled{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{22}{\isachardoublequote}}} \\ |
152 & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & \isa{{\isachardoublequote}simp\ only{\isacharcolon}\ split{\isacharunderscore}tupled{\isacharunderscore}all{\isachardoublequote}} \\ |
152 & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C617070726F783E}{\isasymapprox}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}simp\ only{\isaliteral{3A}{\isacharcolon}}\ split{\isaliteral{5F}{\isacharunderscore}}tupled{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{22}{\isachardoublequote}}} \\ |
153 & \isa{{\isachardoublequote}{\isasymlless}{\isachardoublequote}} & \isa{{\isachardoublequote}clarify{\isachardoublequote}} \\ |
153 & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C6C6573733E}{\isasymlless}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}clarify{\isaliteral{22}{\isachardoublequote}}} \\ |
154 \end{tabular}% |
154 \end{tabular}% |
155 \end{isamarkuptext}% |
155 \end{isamarkuptext}% |
156 \isamarkuptrue% |
156 \isamarkuptrue% |
157 % |
157 % |
158 \isamarkupsection{Tacticals% |
158 \isamarkupsection{Tacticals% |
160 \isamarkuptrue% |
160 \isamarkuptrue% |
161 % |
161 % |
162 \begin{isamarkuptext}% |
162 \begin{isamarkuptext}% |
163 Classic Isabelle provides a huge amount of tacticals for combination |
163 Classic Isabelle provides a huge amount of tacticals for combination |
164 and modification of existing tactics. This has been greatly reduced |
164 and modification of existing tactics. This has been greatly reduced |
165 in Isar, providing the bare minimum of combinators only: ``\isa{{\isachardoublequote}{\isacharcomma}{\isachardoublequote}}'' (sequential composition), ``\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}'' (alternative |
165 in Isar, providing the bare minimum of combinators only: ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}}'' (sequential composition), ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}'' (alternative |
166 choices), ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' (try), ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least |
166 choices), ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' (try), ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequote}}}'' (repeat at least |
167 once). These are usually sufficient in practice; if all fails, |
167 once). These are usually sufficient in practice; if all fails, |
168 arbitrary ML tactic code may be invoked via the \hyperlink{method.tactic}{\mbox{\isa{tactic}}} |
168 arbitrary ML tactic code may be invoked via the \hyperlink{method.tactic}{\mbox{\isa{tactic}}} |
169 method (see \secref{sec:tactics}). |
169 method (see \secref{sec:tactics}). |
170 |
170 |
171 \medskip Common ML tacticals may be expressed directly in Isar as |
171 \medskip Common ML tacticals may be expressed directly in Isar as |
172 follows: |
172 follows: |
173 |
173 |
174 \medskip |
174 \medskip |
175 \begin{tabular}{lll} |
175 \begin{tabular}{lll} |
176 \isa{{\isachardoublequote}tac\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\verb|THEN|~\isa{{\isachardoublequote}tac\isactrlsub {\isadigit{2}}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}{\isacharcomma}\ meth\isactrlsub {\isadigit{2}}{\isachardoublequote}} \\ |
176 \isa{{\isaliteral{22}{\isachardoublequote}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}~\verb|THEN|~\isa{{\isaliteral{22}{\isachardoublequote}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}meth\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ meth\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} \\ |
177 \isa{{\isachardoublequote}tac\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\verb|ORELSE|~\isa{{\isachardoublequote}tac\isactrlsub {\isadigit{2}}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}\ {\isacharbar}\ meth\isactrlsub {\isadigit{2}}{\isachardoublequote}} \\ |
177 \isa{{\isaliteral{22}{\isachardoublequote}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}~\verb|ORELSE|~\isa{{\isaliteral{22}{\isachardoublequote}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}meth\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}\ meth\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} \\ |
178 \verb|TRY|~\isa{tac} & & \isa{{\isachardoublequote}meth{\isacharquery}{\isachardoublequote}} \\ |
178 \verb|TRY|~\isa{tac} & & \isa{{\isaliteral{22}{\isachardoublequote}}meth{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}} \\ |
179 \verb|REPEAT1|~\isa{tac} & & \isa{{\isachardoublequote}meth{\isacharplus}{\isachardoublequote}} \\ |
179 \verb|REPEAT1|~\isa{tac} & & \isa{{\isaliteral{22}{\isachardoublequote}}meth{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequote}}} \\ |
180 \verb|REPEAT|~\isa{tac} & & \isa{{\isachardoublequote}{\isacharparenleft}meth{\isacharplus}{\isacharparenright}{\isacharquery}{\isachardoublequote}} \\ |
180 \verb|REPEAT|~\isa{tac} & & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}meth{\isaliteral{2B}{\isacharplus}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}} \\ |
181 \verb|EVERY|~\isa{{\isachardoublequote}{\isacharbrackleft}tac\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isachardoublequote}} \\ |
181 \verb|EVERY|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}meth\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\ |
182 \verb|FIRST|~\isa{{\isachardoublequote}{\isacharbrackleft}tac\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}\ {\isacharbar}\ {\isasymdots}{\isachardoublequote}} \\ |
182 \verb|FIRST|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}meth\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\ |
183 \end{tabular} |
183 \end{tabular} |
184 \medskip |
184 \medskip |
185 |
185 |
186 \medskip \verb|CHANGED| (see \cite{isabelle-ref}) is usually not |
186 \medskip \verb|CHANGED| (see \cite{isabelle-ref}) is usually not |
187 required in Isar, since most basic proof methods already fail unless |
187 required in Isar, since most basic proof methods already fail unless |
188 there is an actual change in the goal state. Nevertheless, ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' (try) may be used to accept \emph{unchanged} results as |
188 there is an actual change in the goal state. Nevertheless, ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' (try) may be used to accept \emph{unchanged} results as |
189 well. |
189 well. |
190 |
190 |
191 \medskip \verb|ALLGOALS|, \verb|SOMEGOAL| etc.\ (see |
191 \medskip \verb|ALLGOALS|, \verb|SOMEGOAL| etc.\ (see |
192 \cite{isabelle-ref}) are not available in Isar, since there is no |
192 \cite{isabelle-ref}) are not available in Isar, since there is no |
193 direct goal addressing. Nevertheless, some basic methods address |
193 direct goal addressing. Nevertheless, some basic methods address |
194 all goals internally, notably \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} (see |
194 all goals internally, notably \hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}} (see |
195 \secref{sec:simplifier}). Also note that \verb|ALLGOALS| can be |
195 \secref{sec:simplifier}). Also note that \verb|ALLGOALS| can be |
196 often replaced by ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least once), although |
196 often replaced by ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequote}}}'' (repeat at least once), although |
197 this usually has a different operational behavior, such as solving |
197 this usually has a different operational behavior, such as solving |
198 goals in a different order. |
198 goals in a different order. |
199 |
199 |
200 \medskip Iterated resolution, such as \verb|REPEAT (FIRSTGOAL|\isasep\isanewline% |
200 \medskip Iterated resolution, such as \verb|REPEAT (FIRSTGOAL|\isasep\isanewline% |
201 \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 |
201 \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 |