1.1 --- a/doc-src/IsarRef/IsaMakefile Wed May 07 13:38:15 2008 +0200
1.2 +++ b/doc-src/IsarRef/IsaMakefile Wed May 07 15:32:31 2008 +0200
1.3 @@ -22,7 +22,8 @@
1.4 HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
1.5
1.6 $(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \
1.7 - Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/Quick_Reference.thy
1.8 + Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/Quick_Reference.thy \
1.9 + Thy/ML_Tactic.thy
1.10 @$(USEDIR) -s IsarRef HOL Thy
1.11
1.12
2.1 --- a/doc-src/IsarRef/Makefile Wed May 07 13:38:15 2008 +0200
2.2 +++ b/doc-src/IsarRef/Makefile Wed May 07 15:32:31 2008 +0200
2.3 @@ -13,11 +13,13 @@
2.4
2.5 NAME = isar-ref
2.6
2.7 -FILES = isar-ref.tex Thy/document/intro.tex basics.tex Thy/document/syntax.tex \
2.8 - Thy/document/pure.tex Thy/document/Generic.tex logics.tex Thy/document/Quick_Reference.tex \
2.9 - conversion.tex \
2.10 - ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \
2.11 - ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
2.12 +FILES = isar-ref.tex basics.tex Thy/document/Generic.tex \
2.13 + Thy/document/HOLCF_Specific.tex Thy/document/HOL_Specific.tex \
2.14 + Thy/document/ML_Tactic.tex Thy/document/Quick_Reference.tex \
2.15 + Thy/document/ZF_Specific.tex Thy/document/intro.tex \
2.16 + Thy/document/pure.tex Thy/document/syntax.tex \
2.17 + logics.tex ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \
2.18 + ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
2.19
2.20 dvi: $(NAME).dvi
2.21
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/IsarRef/Thy/ML_Tactic.thy Wed May 07 15:32:31 2008 +0200
3.3 @@ -0,0 +1,186 @@
3.4 +(* $Id$ *)
3.5 +
3.6 +theory ML_Tactic
3.7 +imports Main
3.8 +begin
3.9 +
3.10 +chapter {* ML tactic expressions \label{sec:conv-tac} *}
3.11 +
3.12 +text {*
3.13 + Isar Proof methods closely resemble traditional tactics, when used
3.14 + in unstructured sequences of @{command "apply"} commands.
3.15 + Isabelle/Isar provides emulations for all major ML tactics of
3.16 + classic Isabelle --- mostly for the sake of easy porting of existing
3.17 + developments, as actual Isar proof texts would demand much less
3.18 + diversity of proof methods.
3.19 +
3.20 + Unlike tactic expressions in ML, Isar proof methods provide proper
3.21 + concrete syntax for additional arguments, options, modifiers etc.
3.22 + Thus a typical method text is usually more concise than the
3.23 + corresponding ML tactic. Furthermore, the Isar versions of classic
3.24 + Isabelle tactics often cover several variant forms by a single
3.25 + method with separate options to tune the behavior. For example,
3.26 + method @{method simp} replaces all of @{ML simp_tac}~/ @{ML
3.27 + asm_simp_tac}~/ @{ML full_simp_tac}~/ @{ML asm_full_simp_tac}, there
3.28 + is also concrete syntax for augmenting the Simplifier context (the
3.29 + current ``simpset'') in a convenient way.
3.30 +*}
3.31 +
3.32 +
3.33 +section {* Resolution tactics *}
3.34 +
3.35 +text {*
3.36 + Classic Isabelle provides several variant forms of tactics for
3.37 + single-step rule applications (based on higher-order resolution).
3.38 + The space of resolution tactics has the following main dimensions.
3.39 +
3.40 + \begin{enumerate}
3.41 +
3.42 + \item The ``mode'' of resolution: intro, elim, destruct, or forward
3.43 + (e.g.\ @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac},
3.44 + @{ML forward_tac}).
3.45 +
3.46 + \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\
3.47 + @{ML res_inst_tac}).
3.48 +
3.49 + \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac}
3.50 + vs.\ @{ML rtac}).
3.51 +
3.52 + \end{enumerate}
3.53 +
3.54 + Basically, the set of Isar tactic emulations @{method rule_tac},
3.55 + @{method erule_tac}, @{method drule_tac}, @{method frule_tac} (see
3.56 + \secref{sec:tactics}) would be sufficient to cover the four modes,
3.57 + either with or without instantiation, and either with single or
3.58 + multiple arguments. Although it is more convenient in most cases to
3.59 + use the plain @{method rule} method (see
3.60 + \secref{sec:pure-meth-att}), or any of its ``improper'' variants
3.61 + @{method erule}, @{method drule}, @{method frule} (see
3.62 + \secref{sec:misc-meth-att}). Note that explicit goal addressing is
3.63 + only supported by the actual @{method rule_tac} version.
3.64 +
3.65 + With this in mind, plain resolution tactics correspond to Isar
3.66 + methods as follows.
3.67 +
3.68 + \medskip
3.69 + \begin{tabular}{lll}
3.70 + @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\
3.71 + @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
3.72 + @{ML res_inst_tac}~@{text "[(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
3.73 + @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
3.74 + @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
3.75 + @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
3.76 + @{ML res_inst_tac}~@{text "[(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
3.77 + @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
3.78 + \end{tabular}
3.79 + \medskip
3.80 +
3.81 + Note that explicit goal addressing may be usually avoided by
3.82 + changing the order of subgoals with @{command "defer"} or @{command
3.83 + "prefer"} (see \secref{sec:tactic-commands}).
3.84 +*}
3.85 +
3.86 +
3.87 +section {* Simplifier tactics *}
3.88 +
3.89 +text {*
3.90 + The main Simplifier tactics @{ML simp_tac} and variants (cf.\
3.91 + \cite{isabelle-ref}) are all covered by the @{method simp} and
3.92 + @{method simp_all} methods (see \secref{sec:simplifier}). Note that
3.93 + there is no individual goal addressing available, simplification
3.94 + acts either on the first goal (@{method simp}) or all goals
3.95 + (@{method simp_all}).
3.96 +
3.97 + \medskip
3.98 + \begin{tabular}{lll}
3.99 + @{ML asm_full_simp_tac}~@{text "@{simpset} 1"} & & @{method simp} \\
3.100 + @{ML ALLGOALS}~(@{ML asm_full_simp_tac}~@{text "@{simpset}"}) & & @{method simp_all} \\[0.5ex]
3.101 + @{ML simp_tac}~@{text "@{simpset} 1"} & & @{method simp}~@{text "(no_asm)"} \\
3.102 + @{ML asm_simp_tac}~@{text "@{simpset} 1"} & & @{method simp}~@{text "(no_asm_simp)"} \\
3.103 + @{ML full_simp_tac}~@{text "@{simpset} 1"} & & @{method simp}~@{text "(no_asm_use)"} \\
3.104 + @{ML asm_lr_simp_tac}~@{text "@{simpset} 1"} & & @{method simp}~@{text "(asm_lr)"} \\
3.105 + \end{tabular}
3.106 + \medskip
3.107 +*}
3.108 +
3.109 +
3.110 +section {* Classical Reasoner tactics *}
3.111 +
3.112 +text {*
3.113 + The Classical Reasoner provides a rather large number of variations
3.114 + of automated tactics, such as @{ML blast_tac}, @{ML fast_tac}, @{ML
3.115 + clarify_tac} etc.\ (see \cite{isabelle-ref}). The corresponding
3.116 + Isar methods usually share the same base name, such as @{method
3.117 + blast}, @{method fast}, @{method clarify} etc.\ (see
3.118 + \secref{sec:classical}).
3.119 +*}
3.120 +
3.121 +
3.122 +section {* Miscellaneous tactics *}
3.123 +
3.124 +text {*
3.125 + There are a few additional tactics defined in various theories of
3.126 + Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF.
3.127 + The most common ones of these may be ported to Isar as follows.
3.128 +
3.129 + \medskip
3.130 + \begin{tabular}{lll}
3.131 + @{ML stac}~@{text "a 1"} & & @{text "subst a"} \\
3.132 + @{ML hyp_subst_tac}~@{text 1} & & @{text hypsubst} \\
3.133 + @{ML strip_tac}~@{text 1} & @{text "\<approx>"} & @{text "intro strip"} \\
3.134 + @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\
3.135 + & @{text "\<approx>"} & @{text "simp only: split_tupled_all"} \\
3.136 + & @{text "\<lless>"} & @{text "clarify"} \\
3.137 + \end{tabular}
3.138 +*}
3.139 +
3.140 +
3.141 +section {* Tacticals *}
3.142 +
3.143 +text {*
3.144 + Classic Isabelle provides a huge amount of tacticals for combination
3.145 + and modification of existing tactics. This has been greatly reduced
3.146 + in Isar, providing the bare minimum of combinators only: ``@{text
3.147 + ","}'' (sequential composition), ``@{text "|"}'' (alternative
3.148 + choices), ``@{text "?"}'' (try), ``@{text "+"}'' (repeat at least
3.149 + once). These are usually sufficient in practice; if all fails,
3.150 + arbitrary ML tactic code may be invoked via the @{method tactic}
3.151 + method (see \secref{sec:tactics}).
3.152 +
3.153 + \medskip Common ML tacticals may be expressed directly in Isar as
3.154 + follows:
3.155 +
3.156 + \medskip
3.157 + \begin{tabular}{lll}
3.158 + @{text "tac\<^sub>1"}~@{ML_text THEN}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1, meth\<^sub>2"} \\
3.159 + @{text "tac\<^sub>1"}~@{ML_text ORELSE}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1 | meth\<^sub>2"} \\
3.160 + @{ML TRY}~@{text tac} & & @{text "meth?"} \\
3.161 + @{ML REPEAT1}~@{text tac} & & @{text "meth+"} \\
3.162 + @{ML REPEAT}~@{text tac} & & @{text "(meth+)?"} \\
3.163 + @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>]"} & & @{text "meth\<^sub>1, \<dots>"} \\
3.164 + @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>]"} & & @{text "meth\<^sub>1 | \<dots>"} \\
3.165 + \end{tabular}
3.166 + \medskip
3.167 +
3.168 + \medskip @{ML CHANGED} (see \cite{isabelle-ref}) is usually not
3.169 + required in Isar, since most basic proof methods already fail unless
3.170 + there is an actual change in the goal state. Nevertheless, ``@{text
3.171 + "?"}'' (try) may be used to accept \emph{unchanged} results as
3.172 + well.
3.173 +
3.174 + \medskip @{ML ALLGOALS}, @{ML SOMEGOAL} etc.\ (see
3.175 + \cite{isabelle-ref}) are not available in Isar, since there is no
3.176 + direct goal addressing. Nevertheless, some basic methods address
3.177 + all goals internally, notably @{method simp_all} (see
3.178 + \secref{sec:simplifier}). Also note that @{ML ALLGOALS} can be
3.179 + often replaced by ``@{text "+"}'' (repeat at least once), although
3.180 + this usually has a different operational behavior, such as solving
3.181 + goals in a different order.
3.182 +
3.183 + \medskip Iterated resolution, such as @{ML_text "REPEAT (FIRSTGOAL
3.184 + (resolve_tac \<dots>))"}, is usually better expressed using the @{method
3.185 + intro} and @{method elim} methods of Isar (see
3.186 + \secref{sec:classical}).
3.187 +*}
3.188 +
3.189 +end
4.1 --- a/doc-src/IsarRef/Thy/ROOT.ML Wed May 07 13:38:15 2008 +0200
4.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML Wed May 07 15:32:31 2008 +0200
4.3 @@ -10,3 +10,4 @@
4.4 use_thy "Generic";
4.5 use_thy "HOL_Specific";
4.6 use_thy "Quick_Reference";
4.7 +use_thy "ML_Tactic";
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex Wed May 07 15:32:31 2008 +0200
5.3 @@ -0,0 +1,226 @@
5.4 +%
5.5 +\begin{isabellebody}%
5.6 +\def\isabellecontext{ML{\isacharunderscore}Tactic}%
5.7 +%
5.8 +\isadelimtheory
5.9 +\isanewline
5.10 +\isanewline
5.11 +%
5.12 +\endisadelimtheory
5.13 +%
5.14 +\isatagtheory
5.15 +\isacommand{theory}\isamarkupfalse%
5.16 +\ ML{\isacharunderscore}Tactic\isanewline
5.17 +\isakeyword{imports}\ Main\isanewline
5.18 +\isakeyword{begin}%
5.19 +\endisatagtheory
5.20 +{\isafoldtheory}%
5.21 +%
5.22 +\isadelimtheory
5.23 +%
5.24 +\endisadelimtheory
5.25 +%
5.26 +\isamarkupchapter{ML tactic expressions \label{sec:conv-tac}%
5.27 +}
5.28 +\isamarkuptrue%
5.29 +%
5.30 +\begin{isamarkuptext}%
5.31 +Isar Proof methods closely resemble traditional tactics, when used
5.32 + in unstructured sequences of \mbox{\isa{\isacommand{apply}}} commands.
5.33 + Isabelle/Isar provides emulations for all major ML tactics of
5.34 + classic Isabelle --- mostly for the sake of easy porting of existing
5.35 + developments, as actual Isar proof texts would demand much less
5.36 + diversity of proof methods.
5.37 +
5.38 + Unlike tactic expressions in ML, Isar proof methods provide proper
5.39 + concrete syntax for additional arguments, options, modifiers etc.
5.40 + Thus a typical method text is usually more concise than the
5.41 + corresponding ML tactic. Furthermore, the Isar versions of classic
5.42 + Isabelle tactics often cover several variant forms by a single
5.43 + method with separate options to tune the behavior. For example,
5.44 + method \mbox{\isa{simp}} replaces all of \verb|simp_tac|~/ \verb|asm_simp_tac|~/ \verb|full_simp_tac|~/ \verb|asm_full_simp_tac|, there
5.45 + is also concrete syntax for augmenting the Simplifier context (the
5.46 + current ``simpset'') in a convenient way.%
5.47 +\end{isamarkuptext}%
5.48 +\isamarkuptrue%
5.49 +%
5.50 +\isamarkupsection{Resolution tactics%
5.51 +}
5.52 +\isamarkuptrue%
5.53 +%
5.54 +\begin{isamarkuptext}%
5.55 +Classic Isabelle provides several variant forms of tactics for
5.56 + single-step rule applications (based on higher-order resolution).
5.57 + The space of resolution tactics has the following main dimensions.
5.58 +
5.59 + \begin{enumerate}
5.60 +
5.61 + \item The ``mode'' of resolution: intro, elim, destruct, or forward
5.62 + (e.g.\ \verb|resolve_tac|, \verb|eresolve_tac|, \verb|dresolve_tac|,
5.63 + \verb|forward_tac|).
5.64 +
5.65 + \item Optional explicit instantiation (e.g.\ \verb|resolve_tac| vs.\
5.66 + \verb|res_inst_tac|).
5.67 +
5.68 + \item Abbreviations for singleton arguments (e.g.\ \verb|resolve_tac|
5.69 + vs.\ \verb|rtac|).
5.70 +
5.71 + \end{enumerate}
5.72 +
5.73 + Basically, the set of Isar tactic emulations \mbox{\isa{rule{\isacharunderscore}tac}},
5.74 + \mbox{\isa{erule{\isacharunderscore}tac}}, \mbox{\isa{drule{\isacharunderscore}tac}}, \mbox{\isa{frule{\isacharunderscore}tac}} (see
5.75 + \secref{sec:tactics}) would be sufficient to cover the four modes,
5.76 + either with or without instantiation, and either with single or
5.77 + multiple arguments. Although it is more convenient in most cases to
5.78 + use the plain \mbox{\isa{rule}} method (see
5.79 + \secref{sec:pure-meth-att}), or any of its ``improper'' variants
5.80 + \mbox{\isa{erule}}, \mbox{\isa{drule}}, \mbox{\isa{frule}} (see
5.81 + \secref{sec:misc-meth-att}). Note that explicit goal addressing is
5.82 + only supported by the actual \mbox{\isa{rule{\isacharunderscore}tac}} version.
5.83 +
5.84 + With this in mind, plain resolution tactics correspond to Isar
5.85 + methods as follows.
5.86 +
5.87 + \medskip
5.88 + \begin{tabular}{lll}
5.89 + \verb|rtac|~\isa{{\isachardoublequote}a\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}rule\ a{\isachardoublequote}} \\
5.90 + \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}} \\
5.91 + \verb|res_inst_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ {\isadigit{1}}{\isachardoublequote}} & &
5.92 + \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\[0.5ex]
5.93 + \verb|rtac|~\isa{{\isachardoublequote}a\ i{\isachardoublequote}} & & \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ a{\isachardoublequote}} \\
5.94 + \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}} \\
5.95 + \verb|res_inst_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ i{\isachardoublequote}} & &
5.96 + \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\
5.97 + \end{tabular}
5.98 + \medskip
5.99 +
5.100 + Note that explicit goal addressing may be usually avoided by
5.101 + changing the order of subgoals with \mbox{\isa{\isacommand{defer}}} or \mbox{\isa{\isacommand{prefer}}} (see \secref{sec:tactic-commands}).%
5.102 +\end{isamarkuptext}%
5.103 +\isamarkuptrue%
5.104 +%
5.105 +\isamarkupsection{Simplifier tactics%
5.106 +}
5.107 +\isamarkuptrue%
5.108 +%
5.109 +\begin{isamarkuptext}%
5.110 +The main Simplifier tactics \verb|simp_tac| and variants (cf.\
5.111 + \cite{isabelle-ref}) are all covered by the \mbox{\isa{simp}} and
5.112 + \mbox{\isa{simp{\isacharunderscore}all}} methods (see \secref{sec:simplifier}). Note that
5.113 + there is no individual goal addressing available, simplification
5.114 + acts either on the first goal (\mbox{\isa{simp}}) or all goals
5.115 + (\mbox{\isa{simp{\isacharunderscore}all}}).
5.116 +
5.117 + \medskip
5.118 + \begin{tabular}{lll}
5.119 + \verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \mbox{\isa{simp}} \\
5.120 + \verb|ALLGOALS|~(\verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}{\isachardoublequote}}) & & \mbox{\isa{simp{\isacharunderscore}all}} \\[0.5ex]
5.121 + \verb|simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \mbox{\isa{simp}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}} \\
5.122 + \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}} \\
5.123 + \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}} \\
5.124 + \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}} \\
5.125 + \end{tabular}
5.126 + \medskip%
5.127 +\end{isamarkuptext}%
5.128 +\isamarkuptrue%
5.129 +%
5.130 +\isamarkupsection{Classical Reasoner tactics%
5.131 +}
5.132 +\isamarkuptrue%
5.133 +%
5.134 +\begin{isamarkuptext}%
5.135 +The Classical Reasoner provides a rather large number of variations
5.136 + of automated tactics, such as \verb|blast_tac|, \verb|fast_tac|, \verb|clarify_tac| etc.\ (see \cite{isabelle-ref}). The corresponding
5.137 + Isar methods usually share the same base name, such as \mbox{\isa{blast}}, \mbox{\isa{fast}}, \mbox{\isa{clarify}} etc.\ (see
5.138 + \secref{sec:classical}).%
5.139 +\end{isamarkuptext}%
5.140 +\isamarkuptrue%
5.141 +%
5.142 +\isamarkupsection{Miscellaneous tactics%
5.143 +}
5.144 +\isamarkuptrue%
5.145 +%
5.146 +\begin{isamarkuptext}%
5.147 +There are a few additional tactics defined in various theories of
5.148 + Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF.
5.149 + The most common ones of these may be ported to Isar as follows.
5.150 +
5.151 + \medskip
5.152 + \begin{tabular}{lll}
5.153 + \verb|stac|~\isa{{\isachardoublequote}a\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}subst\ a{\isachardoublequote}} \\
5.154 + \verb|hyp_subst_tac|~\isa{{\isadigit{1}}} & & \isa{hypsubst} \\
5.155 + \verb|strip_tac|~\isa{{\isadigit{1}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & \isa{{\isachardoublequote}intro\ strip{\isachardoublequote}} \\
5.156 + \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}} \\
5.157 + & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & \isa{{\isachardoublequote}simp\ only{\isacharcolon}\ split{\isacharunderscore}tupled{\isacharunderscore}all{\isachardoublequote}} \\
5.158 + & \isa{{\isachardoublequote}{\isasymlless}{\isachardoublequote}} & \isa{{\isachardoublequote}clarify{\isachardoublequote}} \\
5.159 + \end{tabular}%
5.160 +\end{isamarkuptext}%
5.161 +\isamarkuptrue%
5.162 +%
5.163 +\isamarkupsection{Tacticals%
5.164 +}
5.165 +\isamarkuptrue%
5.166 +%
5.167 +\begin{isamarkuptext}%
5.168 +Classic Isabelle provides a huge amount of tacticals for combination
5.169 + and modification of existing tactics. This has been greatly reduced
5.170 + in Isar, providing the bare minimum of combinators only: ``\isa{{\isachardoublequote}{\isacharcomma}{\isachardoublequote}}'' (sequential composition), ``\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}'' (alternative
5.171 + choices), ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' (try), ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least
5.172 + once). These are usually sufficient in practice; if all fails,
5.173 + arbitrary ML tactic code may be invoked via the \mbox{\isa{tactic}}
5.174 + method (see \secref{sec:tactics}).
5.175 +
5.176 + \medskip Common ML tacticals may be expressed directly in Isar as
5.177 + follows:
5.178 +
5.179 + \medskip
5.180 + \begin{tabular}{lll}
5.181 + \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}} \\
5.182 + \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}} \\
5.183 + \verb|TRY|~\isa{tac} & & \isa{{\isachardoublequote}meth{\isacharquery}{\isachardoublequote}} \\
5.184 + \verb|REPEAT1|~\isa{tac} & & \isa{{\isachardoublequote}meth{\isacharplus}{\isachardoublequote}} \\
5.185 + \verb|REPEAT|~\isa{tac} & & \isa{{\isachardoublequote}{\isacharparenleft}meth{\isacharplus}{\isacharparenright}{\isacharquery}{\isachardoublequote}} \\
5.186 + \verb|EVERY|~\isa{{\isachardoublequote}{\isacharbrackleft}tac\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isachardoublequote}} \\
5.187 + \verb|FIRST|~\isa{{\isachardoublequote}{\isacharbrackleft}tac\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}\ {\isacharbar}\ {\isasymdots}{\isachardoublequote}} \\
5.188 + \end{tabular}
5.189 + \medskip
5.190 +
5.191 + \medskip \verb|CHANGED| (see \cite{isabelle-ref}) is usually not
5.192 + required in Isar, since most basic proof methods already fail unless
5.193 + there is an actual change in the goal state. Nevertheless, ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' (try) may be used to accept \emph{unchanged} results as
5.194 + well.
5.195 +
5.196 + \medskip \verb|ALLGOALS|, \verb|SOMEGOAL| etc.\ (see
5.197 + \cite{isabelle-ref}) are not available in Isar, since there is no
5.198 + direct goal addressing. Nevertheless, some basic methods address
5.199 + all goals internally, notably \mbox{\isa{simp{\isacharunderscore}all}} (see
5.200 + \secref{sec:simplifier}). Also note that \verb|ALLGOALS| can be
5.201 + often replaced by ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least once), although
5.202 + this usually has a different operational behavior, such as solving
5.203 + goals in a different order.
5.204 +
5.205 + \medskip Iterated resolution, such as \verb|REPEAT (FIRSTGOAL|\isasep\isanewline%
5.206 +\verb| (resolve_tac \<dots>))|, is usually better expressed using the \mbox{\isa{intro}} and \mbox{\isa{elim}} methods of Isar (see
5.207 + \secref{sec:classical}).%
5.208 +\end{isamarkuptext}%
5.209 +\isamarkuptrue%
5.210 +%
5.211 +\isadelimtheory
5.212 +%
5.213 +\endisadelimtheory
5.214 +%
5.215 +\isatagtheory
5.216 +\isacommand{end}\isamarkupfalse%
5.217 +%
5.218 +\endisatagtheory
5.219 +{\isafoldtheory}%
5.220 +%
5.221 +\isadelimtheory
5.222 +%
5.223 +\endisadelimtheory
5.224 +\isanewline
5.225 +\end{isabellebody}%
5.226 +%%% Local Variables:
5.227 +%%% mode: latex
5.228 +%%% TeX-master: "root"
5.229 +%%% End:
6.1 --- a/doc-src/IsarRef/conversion.tex Wed May 07 13:38:15 2008 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,566 +0,0 @@
6.4 -
6.5 -\chapter{Isabelle/Isar conversion guide}\label{ap:conv}
6.6 -
6.7 -Subsequently, we give a few practical hints on working in a mixed environment
6.8 -of old Isabelle ML proof scripts and new Isabelle/Isar theories. There are
6.9 -basically three ways to cope with this issue.
6.10 -\begin{enumerate}
6.11 -\item Do not convert old sources at all, but communicate directly at the level
6.12 - of \emph{internal} theory and theorem values.
6.13 -\item Port old-style theory files to new-style ones (very easy), and ML proof
6.14 - scripts to Isar tactic-emulation scripts (quite easy).
6.15 -\item Actually redo ML proof scripts as human-readable Isar proof texts
6.16 - (probably hard, depending who wrote the original scripts).
6.17 -\end{enumerate}
6.18 -
6.19 -
6.20 -\section{No conversion}
6.21 -
6.22 -Internally, Isabelle is able to handle both old and new-style theories at the
6.23 -same time; the theory loader automatically detects the input format. In any
6.24 -case, the results are certain internal ML values of type \texttt{theory} and
6.25 -\texttt{thm}. These may be accessed from either classic Isabelle or
6.26 -Isabelle/Isar, provided that some minimal precautions are observed.
6.27 -
6.28 -
6.29 -\subsection{Referring to theorem and theory values}
6.30 -
6.31 -\begin{ttbox}
6.32 -thm : xstring -> thm
6.33 -thms : xstring -> thm list
6.34 -the_context : unit -> theory
6.35 -theory : string -> theory
6.36 -\end{ttbox}
6.37 -
6.38 -These functions provide general means to refer to logical objects from ML.
6.39 -Old-style theories used to emit many ML bindings of theorems and theories, but
6.40 -this is no longer done in new-style Isabelle/Isar theories.
6.41 -
6.42 -\begin{descr}
6.43 -\item [$\mathtt{thm}~name$ and $\mathtt{thms}~name$] retrieve theorems stored
6.44 - in the current theory context, including any ancestor node.
6.45 -
6.46 - The convention of old-style theories was to bind any theorem as an ML value
6.47 - as well. New-style theories no longer do this, so ML code may require
6.48 - \texttt{thm~"foo"} rather than just \texttt{foo}.
6.49 -
6.50 -\item [$\mathtt{the_context()}$] refers to the current theory context.
6.51 -
6.52 - Old-style theories often use the ML binding \texttt{thy}, which is
6.53 - dynamically created by the ML code generated from old theory source. This
6.54 - is no longer the recommended way in any case! Function \texttt{the_context}
6.55 - should be used for old scripts as well.
6.56 -
6.57 -\item [$\mathtt{theory}~name$] retrieves the named theory from the global
6.58 - theory-loader database.
6.59 -
6.60 - The ML code generated from old-style theories would include an ML binding
6.61 - $name\mathtt{.thy}$ as part of an ML structure.
6.62 -\end{descr}
6.63 -
6.64 -
6.65 -\subsection{Storing theorem values}
6.66 -
6.67 -\begin{ttbox}
6.68 -qed : string -> unit
6.69 -bind_thm : string * thm -> unit
6.70 -bind_thms : string * thm list -> unit
6.71 -\end{ttbox}
6.72 -
6.73 -ML proof scripts have to be well-behaved by storing theorems properly within
6.74 -the current theory context, in order to enable new-style theories to retrieve
6.75 -these later.
6.76 -
6.77 -\begin{descr}
6.78 -
6.79 -\item [$\mathtt{qed}~name$] is the canonical way to conclude a proof script in
6.80 - ML. This already manages entry in the theorem database of the current
6.81 - theory context.
6.82 -
6.83 -\item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$]
6.84 - store theorems that have been produced in ML in an ad-hoc manner.
6.85 -
6.86 -\end{descr}
6.87 -
6.88 -Note that the original ``LCF-system'' approach of binding theorem values on
6.89 -the ML toplevel only has long been given up in Isabelle! Despite of this, old
6.90 -legacy proof scripts occasionally contain code such as \texttt{val foo =
6.91 - result();} which is ill-behaved in several respects. Apart from preventing
6.92 -access from Isar theories, it also omits the result from the WWW presentation,
6.93 -for example.
6.94 -
6.95 -
6.96 -\subsection{ML declarations in Isar}
6.97 -
6.98 -\begin{matharray}{rcl}
6.99 - \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
6.100 - \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
6.101 -\end{matharray}
6.102 -
6.103 -Isabelle/Isar theories may contain ML declarations as well. For example, an
6.104 -old-style theorem binding may be mimicked as follows.
6.105 -\[
6.106 -\isarkeyword{ML}~\{*~\mbox{\texttt{val foo = thm "foo"}}~*\}
6.107 -\]
6.108 -Note that this command cannot be undone, so invalid theorem bindings in ML may
6.109 -persist. Also note that the current theory may not be modified; use
6.110 -$\isarkeyword{ML_setup}$ for declarations that act on the current context.
6.111 -
6.112 -
6.113 -\section{Porting theories and proof scripts}\label{sec:port-scripts}
6.114 -
6.115 -Porting legacy theory and ML files to proper Isabelle/Isar theories has
6.116 -several advantages. For example, the Proof~General user interface
6.117 -\cite{proofgeneral} for Isabelle/Isar is more robust and more comfortable to
6.118 -use than the version for classic Isabelle. This is due to the fact that the
6.119 -generic ML toplevel has been replaced by a separate Isar interaction loop,
6.120 -with full control over input synchronization and error conditions.
6.121 -
6.122 -Furthermore, the Isabelle document preparation system (see also
6.123 -\cite{isabelle-sys}) only works properly with new-style theories. Output of
6.124 -old-style sources is at the level of individual characters (and symbols),
6.125 -without proper document markup as in Isabelle/Isar theories.
6.126 -
6.127 -
6.128 -\subsection{Theories}
6.129 -
6.130 -Basically, the Isabelle/Isar theory syntax is a proper superset of the classic
6.131 -one. Only a few quirks and legacy problems have been eliminated, resulting in
6.132 -simpler rules and less special cases. The main changes of theory syntax are
6.133 -as follows.
6.134 -
6.135 -\begin{itemize}
6.136 -\item Quoted strings may contain arbitrary white space, and span several lines
6.137 - without requiring \verb,\,\,\dots\verb,\, escapes.
6.138 -\item Names may always be quoted.
6.139 -
6.140 - The old syntax would occasionally demand plain identifiers vs.\ quoted
6.141 - strings to accommodate certain syntactic features.
6.142 -\item Types and terms have to be \emph{atomic} as far as the theory syntax is
6.143 - concerned; this typically requires quoting of input strings, e.g.\ ``$x +
6.144 - y$''.
6.145 -
6.146 - The old theory syntax used to fake part of the syntax of types in order to
6.147 - require less quoting in common cases; this was hard to predict, though. On
6.148 - the other hand, Isar does not require quotes for simple terms, such as plain
6.149 - identifiers $x$, numerals $1$, or symbols $\forall$ (input as
6.150 - \verb,\<forall>,).
6.151 -\item Theorem declarations require an explicit colon to separate the name from
6.152 - the statement (the name is usually optional). Cf.\ the syntax of $\DEFS$ in
6.153 - \S\ref{sec:consts}, or $\THEOREMNAME$ in \S\ref{sec:axms-thms}.
6.154 -\end{itemize}
6.155 -
6.156 -Note that Isabelle/Isar error messages are usually quite explicit about the
6.157 -problem at hand. So in cases of doubt, input syntax may be just as well tried
6.158 -out interactively.
6.159 -
6.160 -
6.161 -\subsection{Goal statements}\label{sec:conv-goal}
6.162 -
6.163 -\subsubsection{Simple goals}
6.164 -
6.165 -In ML the canonical a goal statement together with a complete proof script is
6.166 -as follows:
6.167 -\begin{ttbox}
6.168 - Goal "\(\phi\)";
6.169 - by \(tac@1\);
6.170 - \(\vdots\)
6.171 - qed "\(name\)";
6.172 -\end{ttbox}
6.173 -This form may be turned into an Isar tactic-emulation script like this:
6.174 -\begin{matharray}{l}
6.175 - \LEMMA{name}{\texttt"{\phi}\texttt"} \\
6.176 - \quad \APPLY{meth@1} \\
6.177 - \qquad \vdots \\
6.178 - \quad \DONE \\
6.179 -\end{matharray}
6.180 -Note that the main statement may be $\THEOREMNAME$ or $\COROLLARYNAME$ as
6.181 -well. See \S\ref{sec:conv-tac} for further details on how to convert actual
6.182 -tactic expressions into proof methods.
6.183 -
6.184 -\medskip Classic Isabelle provides many variant forms of goal commands, see
6.185 -also \cite{isabelle-ref} for further details. The second most common one is
6.186 -\texttt{Goalw}, which expands definitions before commencing the actual proof
6.187 -script.
6.188 -\begin{ttbox}
6.189 - Goalw [\(def@1\), \(\dots\)] "\(\phi\)";
6.190 -\end{ttbox}
6.191 -This may be replaced by using the $unfold$ proof method explicitly.
6.192 -\begin{matharray}{l}
6.193 -\LEMMA{name}{\texttt"{\phi}\texttt"} \\
6.194 -\quad \APPLY{(unfold~def@1~\dots)} \\
6.195 -\end{matharray}
6.196 -
6.197 -
6.198 -\subsubsection{Deriving rules}
6.199 -
6.200 -Deriving non-atomic meta-level propositions requires special precautions in
6.201 -classic Isabelle: the primitive \texttt{goal} command decomposes a statement
6.202 -into the atomic conclusion and a list of assumptions, which are exhibited as
6.203 -ML values of type \texttt{thm}. After the proof is finished, these premises
6.204 -are discharged again, resulting in the original rule statement. The ``long
6.205 -format'' of Isabelle/Isar goal statements admits to emulate this technique
6.206 -nicely. The general ML goal statement for derived rules looks like this:
6.207 -\begin{ttbox}
6.208 - val [\(prem@1\), \dots] = goal "\(\phi@1 \Imp \dots \Imp \psi\)";
6.209 - by \(tac@1\);
6.210 - \(\vdots\)
6.211 - qed "\(a\)"
6.212 -\end{ttbox}
6.213 -This form may be turned into a tactic-emulation script as follows:
6.214 -\begin{matharray}{l}
6.215 - \LEMMA{a}{} \\
6.216 - \quad \ASSUMES{prem@1}{\texttt"\phi@1\texttt"}~\AND~\dots \\
6.217 - \quad \SHOWS{}{\texttt"{\psi}\texttt"} \\
6.218 - \qquad \APPLY{meth@1} \\
6.219 - \qquad\quad \vdots \\
6.220 - \qquad \DONE \\
6.221 -\end{matharray}
6.222 -
6.223 -\medskip In practice, actual rules are often rather direct consequences of
6.224 -corresponding atomic statements, typically stemming from the definition of a
6.225 -new concept. In that case, the general scheme for deriving rules may be
6.226 -greatly simplified, using one of the standard automated proof tools, such as
6.227 -$simp$, $blast$, or $auto$. This could work as follows:
6.228 -\begin{matharray}{l}
6.229 - \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\
6.230 - \quad \BYY{(unfold~defs)}{blast} \\
6.231 -\end{matharray}
6.232 -Note that classic Isabelle would support this form only in the special case
6.233 -where $\phi@1$, \dots are atomic statements (when using the standard
6.234 -\texttt{Goal} command). Otherwise the special treatment of rules would be
6.235 -applied, disturbing this simple setup.
6.236 -
6.237 -\medskip Occasionally, derived rules would be established by first proving an
6.238 -appropriate atomic statement (using $\forall$ and $\longrightarrow$ of the
6.239 -object-logic), and putting the final result into ``rule format''. In classic
6.240 -Isabelle this would usually proceed as follows:
6.241 -\begin{ttbox}
6.242 - Goal "\(\phi\)";
6.243 - by \(tac@1\);
6.244 - \(\vdots\)
6.245 - qed_spec_mp "\(name\)";
6.246 -\end{ttbox}
6.247 -The operation performed by \texttt{qed_spec_mp} is also performed by the Isar
6.248 -attribute ``$rule_format$'', see also \S\ref{sec:object-logic}. Thus the
6.249 -corresponding Isar text may look like this:
6.250 -\begin{matharray}{l}
6.251 - \LEMMA{name~[rule_format]}{\texttt"{\phi}\texttt"} \\
6.252 - \quad \APPLY{meth@1} \\
6.253 - \qquad \vdots \\
6.254 - \quad \DONE \\
6.255 -\end{matharray}
6.256 -Note plain ``$rule_format$'' actually performs a slightly different operation:
6.257 -it fully replaces object-level implication and universal quantification
6.258 -throughout the whole result statement. This is the right thing in most cases.
6.259 -For historical reasons, \texttt{qed_spec_mp} would only operate on the
6.260 -conclusion; one may get this exact behavior by using
6.261 -``$rule_format~(no_asm)$'' instead.
6.262 -
6.263 -\medskip Actually ``$rule_format$'' is a bit unpleasant to work with, since
6.264 -the final result statement is not shown in the text. An alternative is to
6.265 -state the resulting rule in the intended form in the first place, and have the
6.266 -initial refinement step turn it into internal object-logic form using the
6.267 -$atomize$ method indicated below. The remaining script is unchanged.
6.268 -
6.269 -\begin{matharray}{l}
6.270 - \LEMMA{name}{\texttt"{\All{\vec x}\vec\phi \Imp \psi}\texttt"} \\
6.271 - \quad \APPLY{(atomize~(full))} \\
6.272 - \quad \APPLY{meth@1} \\
6.273 - \qquad \vdots \\
6.274 - \quad \DONE \\
6.275 -\end{matharray}
6.276 -
6.277 -In many situations the $atomize$ step above is actually unnecessary,
6.278 -especially if the subsequent script mainly consists of automated tools.
6.279 -
6.280 -
6.281 -\subsection{Tactics}\label{sec:conv-tac}
6.282 -
6.283 -Isar Proof methods closely resemble traditional tactics, when used in
6.284 -unstructured sequences of $\APPLYNAME$ commands (cf.\ \S\ref{sec:conv-goal}).
6.285 -Isabelle/Isar provides emulations for all major ML tactics of classic Isabelle
6.286 ---- mostly for the sake of easy porting of existing developments, as actual
6.287 -Isar proof texts would demand much less diversity of proof methods.
6.288 -
6.289 -Unlike tactic expressions in ML, Isar proof methods provide proper concrete
6.290 -syntax for additional arguments, options, modifiers etc. Thus a typical
6.291 -method text is usually more concise than the corresponding ML tactic.
6.292 -Furthermore, the Isar versions of classic Isabelle tactics often cover several
6.293 -variant forms by a single method with separate options to tune the behavior.
6.294 -For example, method $simp$ replaces all of \texttt{simp_tac}~/
6.295 -\texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac},
6.296 -there is also concrete syntax for augmenting the Simplifier context (the
6.297 -current ``simpset'') in a convenient way.
6.298 -
6.299 -
6.300 -\subsubsection{Resolution tactics}
6.301 -
6.302 -Classic Isabelle provides several variant forms of tactics for single-step
6.303 -rule applications (based on higher-order resolution). The space of resolution
6.304 -tactics has the following main dimensions.
6.305 -\begin{enumerate}
6.306 -\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\
6.307 - \texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac},
6.308 - \texttt{forward_tac}).
6.309 -\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\
6.310 - \texttt{res_inst_tac}).
6.311 -\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\
6.312 - \texttt{rtac}).
6.313 -\end{enumerate}
6.314 -
6.315 -Basically, the set of Isar tactic emulations $rule_tac$, $erule_tac$,
6.316 -$drule_tac$, $frule_tac$ (see \S\ref{sec:tactics}) would be sufficient to
6.317 -cover the four modes, either with or without instantiation, and either with
6.318 -single or multiple arguments. Although it is more convenient in most cases to
6.319 -use the plain $rule$ method (see \S\ref{sec:pure-meth-att}), or any of its
6.320 -``improper'' variants $erule$, $drule$, $frule$ (see
6.321 -\S\ref{sec:misc-meth-att}). Note that explicit goal addressing is only
6.322 -supported by the actual $rule_tac$ version.
6.323 -
6.324 -With this in mind, plain resolution tactics may be ported as follows.
6.325 -\begin{matharray}{lll}
6.326 - \texttt{rtac}~a~1 & & rule~a \\
6.327 - \texttt{resolve_tac}~[a@1, \dots]~1 & & rule~a@1~\dots \\
6.328 - \texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~1 & &
6.329 - rule_tac~x@1 = t@1~and~\dots~in~a \\[0.5ex]
6.330 - \texttt{rtac}~a~i & & rule_tac~[i]~a \\
6.331 - \texttt{resolve_tac}~[a@1, \dots]~i & & rule_tac~[i]~a@1~\dots \\
6.332 - \texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~i & &
6.333 - rule_tac~[i]~x@1 = t@1~and~\dots~in~a \\
6.334 -\end{matharray}
6.335 -
6.336 -Note that explicit goal addressing may be usually avoided by changing the
6.337 -order of subgoals with $\isarkeyword{defer}$ or $\isarkeyword{prefer}$ (see
6.338 -\S\ref{sec:tactic-commands}).
6.339 -
6.340 -\medskip Some further (less frequently used) combinations of basic resolution
6.341 -tactics may be expressed as follows.
6.342 -\begin{matharray}{lll}
6.343 - \texttt{ares_tac}~[a@1, \dots]~1 & & assumption~|~rule~a@1~\dots \\
6.344 - \texttt{eatac}~a~n~1 & & erule~(n)~a \\
6.345 - \texttt{datac}~a~n~1 & & drule~(n)~a \\
6.346 - \texttt{fatac}~a~n~1 & & frule~(n)~a \\
6.347 -\end{matharray}
6.348 -
6.349 -
6.350 -\subsubsection{Simplifier tactics}
6.351 -
6.352 -The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants
6.353 -(cf.\ \cite{isabelle-ref}) are all covered by the $simp$ and $simp_all$
6.354 -methods (see \S\ref{sec:simplifier}). Note that there is no individual goal
6.355 -addressing available, simplification acts either on the first goal ($simp$) or
6.356 -all goals ($simp_all$).
6.357 -
6.358 -\begin{matharray}{lll}
6.359 - \texttt{Asm_full_simp_tac 1} & & simp \\
6.360 - \texttt{ALLGOALS Asm_full_simp_tac} & & simp_all \\[0.5ex]
6.361 - \texttt{Simp_tac 1} & & simp~(no_asm) \\
6.362 - \texttt{Asm_simp_tac 1} & & simp~(no_asm_simp) \\
6.363 - \texttt{Full_simp_tac 1} & & simp~(no_asm_use) \\
6.364 - \texttt{Asm_lr_simp_tac 1} & & simp~(asm_lr) \\
6.365 -\end{matharray}
6.366 -
6.367 -Isar also provides separate method modifier syntax for augmenting the
6.368 -Simplifier context (see \S\ref{sec:simplifier}), which is known as the
6.369 -``simpset'' in ML. A typical ML expression with simpset changes looks like
6.370 -this:
6.371 -\begin{ttbox}
6.372 -asm_full_simp_tac (simpset () addsimps [\(a@1\), \(\dots\)] delsimps [\(b@1\), \(\dots\)]) 1
6.373 -\end{ttbox}
6.374 -The corresponding Isar text is as follows:
6.375 -\[
6.376 -simp~add:~a@1~\dots~del:~b@1~\dots
6.377 -\]
6.378 -Global declarations of Simplifier rules (e.g.\ \texttt{Addsimps}) are covered
6.379 -by application of attributes, see \S\ref{sec:conv-decls} for more information.
6.380 -
6.381 -
6.382 -\subsubsection{Classical Reasoner tactics}
6.383 -
6.384 -The Classical Reasoner provides a rather large number of variations of
6.385 -automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac},
6.386 -\texttt{Clarify_tac} etc.\ (see \cite{isabelle-ref}). The corresponding Isar
6.387 -methods usually share the same base name, such as $blast$, $fast$, $clarify$
6.388 -etc.\ (see \S\ref{sec:classical}).
6.389 -
6.390 -Similar to the Simplifier, there is separate method modifier syntax for
6.391 -augmenting the Classical Reasoner context, which is known as the ``claset'' in
6.392 -ML. A typical ML expression with claset changes looks like this:
6.393 -\begin{ttbox}
6.394 -blast_tac (claset () addIs [\(a@1\), \(\dots\)] addSEs [\(b@1\), \(\dots\)]) 1
6.395 -\end{ttbox}
6.396 -The corresponding Isar text is as follows:
6.397 -\[
6.398 -blast~intro:~a@1~\dots~elim!:~b@1~\dots
6.399 -\]
6.400 -Global declarations of Classical Reasoner rules (e.g.\ \texttt{AddIs}) are
6.401 -covered by application of attributes, see \S\ref{sec:conv-decls} for more
6.402 -information.
6.403 -
6.404 -
6.405 -\subsubsection{Miscellaneous tactics}
6.406 -
6.407 -There are a few additional tactics defined in various theories of
6.408 -Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. The most
6.409 -common ones of these may be ported to Isar as follows.
6.410 -
6.411 -\begin{matharray}{lll}
6.412 - \texttt{stac}~a~1 & & subst~a \\
6.413 - \texttt{hyp_subst_tac}~1 & & hypsubst \\
6.414 - \texttt{strip_tac}~1 & \approx & intro~strip \\
6.415 - \texttt{split_all_tac}~1 & & simp~(no_asm_simp)~only:~split_tupled_all \\
6.416 - & \approx & simp~only:~split_tupled_all \\
6.417 - & \ll & clarify \\
6.418 -\end{matharray}
6.419 -
6.420 -
6.421 -\subsubsection{Tacticals}
6.422 -
6.423 -Classic Isabelle provides a huge amount of tacticals for combination and
6.424 -modification of existing tactics. This has been greatly reduced in Isar,
6.425 -providing the bare minimum of combinators only: ``$,$'' (sequential
6.426 -composition), ``$|$'' (alternative choices), ``$?$'' (try), ``$+$'' (repeat at
6.427 -least once). These are usually sufficient in practice; if all fails,
6.428 -arbitrary ML tactic code may be invoked via the $tactic$ method (see
6.429 -\S\ref{sec:tactics}).
6.430 -
6.431 -\medskip Common ML tacticals may be expressed directly in Isar as follows:
6.432 -\begin{matharray}{lll}
6.433 -tac@1~\texttt{THEN}~tac@2 & & meth@1, meth@2 \\
6.434 -tac@1~\texttt{ORELSE}~tac@2 & & meth@1~|~meth@2 \\
6.435 -\texttt{TRY}~tac & & meth? \\
6.436 -\texttt{REPEAT1}~tac & & meth+ \\
6.437 -\texttt{REPEAT}~tac & & (meth+)? \\
6.438 -\texttt{EVERY}~[tac@1, \dots] & & meth@1, \dots \\
6.439 -\texttt{FIRST}~[tac@1, \dots] & & meth@1~|~\dots \\
6.440 -\end{matharray}
6.441 -
6.442 -\medskip \texttt{CHANGED} (see \cite{isabelle-ref}) is usually not required in
6.443 -Isar, since most basic proof methods already fail unless there is an actual
6.444 -change in the goal state. Nevertheless, ``$?$'' (try) may be used to accept
6.445 -\emph{unchanged} results as well.
6.446 -
6.447 -\medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelle-ref})
6.448 -are not available in Isar, since there is no direct goal addressing.
6.449 -Nevertheless, some basic methods address all goals internally, notably
6.450 -$simp_all$ (see \S\ref{sec:simplifier}). Also note that \texttt{ALLGOALS} may
6.451 -be often replaced by ``$+$'' (repeat at least once), although this usually has
6.452 -a different operational behavior, such as solving goals in a different order.
6.453 -
6.454 -\medskip Iterated resolution, such as
6.455 -\texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed
6.456 -using the $intro$ and $elim$ methods of Isar (see \S\ref{sec:classical}).
6.457 -
6.458 -
6.459 -\subsection{Declarations and ad-hoc operations}\label{sec:conv-decls}
6.460 -
6.461 -Apart from proof commands and tactic expressions, almost all of the remaining
6.462 -ML code occurring in legacy proof scripts are either global context
6.463 -declarations (such as \texttt{Addsimps}) or ad-hoc operations on theorems
6.464 -(such as \texttt{RS}). In Isar both of these are covered by theorem
6.465 -expressions with \emph{attributes}.
6.466 -
6.467 -\medskip Theorem operations may be attached as attributes in the very place
6.468 -where theorems are referenced, say within a method argument. The subsequent
6.469 -ML combinators may be expressed directly in Isar as follows.
6.470 -\begin{matharray}{lll}
6.471 - thm@1~\texttt{RS}~thm@2 & & thm@1~[THEN~thm@2] \\
6.472 - thm@1~\texttt{RSN}~(i, thm@2) & & thm@1~[THEN~[i]~thm@2] \\
6.473 - thm@1~\texttt{COMP}~thm@2 & & thm@1~[COMP~thm@2] \\
6.474 - \relax[thm@1, \dots]~\texttt{MRS}~thm & & thm~[OF~thm@1~\dots] \\
6.475 - \texttt{read_instantiate}~[(x@1, t@1), \dots]~thm & & thm~[where~x@1 = t@1~and~\dots] \\
6.476 - \texttt{make_elim}~thm & & thm~[elim_format] \\
6.477 - \texttt{standard}~thm & & thm~[standard] \\
6.478 -\end{matharray}
6.479 -
6.480 -Note that $OF$ is often more readable as $THEN$; likewise positional
6.481 -instantiation with $of$ is often more appropriate than $where$.
6.482 -
6.483 -The special ML command \texttt{qed_spec_mp} of Isabelle/HOL and FOL may be
6.484 -replaced by passing the result of a proof through $rule_format$.
6.485 -
6.486 -\medskip Global ML declarations may be expressed using the $\DECLARE$ command
6.487 -(see \S\ref{sec:tactic-commands}) together with appropriate attributes. The
6.488 -most common ones are as follows.
6.489 -\begin{matharray}{lll}
6.490 - \texttt{Addsimps}~[thm] & & \DECLARE~thm~[simp] \\
6.491 - \texttt{Delsimps}~[thm] & & \DECLARE~thm~[simp~del] \\
6.492 - \texttt{Addsplits}~[thm] & & \DECLARE~thm~[split] \\
6.493 - \texttt{Delsplits}~[thm] & & \DECLARE~thm~[split~del] \\[0.5ex]
6.494 - \texttt{AddIs}~[thm] & & \DECLARE~thm~[intro] \\
6.495 - \texttt{AddEs}~[thm] & & \DECLARE~thm~[elim] \\
6.496 - \texttt{AddDs}~[thm] & & \DECLARE~thm~[dest] \\
6.497 - \texttt{AddSIs}~[thm] & & \DECLARE~thm~[intro!] \\
6.498 - \texttt{AddSEs}~[thm] & & \DECLARE~thm~[elim!] \\
6.499 - \texttt{AddSDs}~[thm] & & \DECLARE~thm~[dest!] \\[0.5ex]
6.500 - \texttt{AddIffs}~[thm] & & \DECLARE~thm~[iff] \\
6.501 -\end{matharray}
6.502 -Note that explicit $\DECLARE$ commands are rarely needed in practice; Isar
6.503 -admits to declare theorems on-the-fly wherever they emerge. Consider the
6.504 -following ML idiom:
6.505 -\begin{ttbox}
6.506 -Goal "\(\phi\)";
6.507 - \(\vdots\)
6.508 -qed "name";
6.509 -Addsimps [name];
6.510 -\end{ttbox}
6.511 -This may be expressed more succinctly in Isar like this:
6.512 -\begin{matharray}{l}
6.513 - \LEMMA{name~[simp]}{\phi} \\
6.514 - \quad\vdots
6.515 -\end{matharray}
6.516 -The $name$ may be even omitted, although this would make it difficult to
6.517 -declare the theorem otherwise later (e.g.\ as $[simp~del]$).
6.518 -
6.519 -
6.520 -\section{Writing actual Isar proof texts}
6.521 -
6.522 -Porting legacy ML proof scripts into Isar tactic emulation scripts (see
6.523 -\S\ref{sec:port-scripts}) is mainly a technical issue, since the basic
6.524 -representation of formal ``proof script'' is preserved. In contrast,
6.525 -converting existing Isabelle developments into actual human-readably Isar
6.526 -proof texts is more involved, due to the fundamental change of the underlying
6.527 -paradigm.
6.528 -
6.529 -This issue is comparable to that of converting programs written in a low-level
6.530 -programming languages (say Assembler) into higher-level ones (say Haskell).
6.531 -In order to accomplish this, one needs a working knowledge of the target
6.532 -language, as well an understanding of the \emph{original} idea of the piece of
6.533 -code expressed in the low-level language.
6.534 -
6.535 -As far as Isar proofs are concerned, it is usually much easier to re-use only
6.536 -definitions and the main statements, while following the arrangement of proof
6.537 -scripts only very loosely. Ideally, one would also have some \emph{informal}
6.538 -proof outlines available for guidance as well. In the worst case, obscure
6.539 -proof scripts would have to be re-engineered by tracing forth and backwards,
6.540 -and by educated guessing!
6.541 -
6.542 -\medskip This is a possible schedule to embark on actual conversion of legacy
6.543 -proof scripts into Isar proof texts.
6.544 -
6.545 -\begin{enumerate}
6.546 -
6.547 -\item Port ML scripts to Isar tactic emulation scripts (see
6.548 - \S\ref{sec:port-scripts}).
6.549 -
6.550 -\item Get sufficiently acquainted with Isabelle/Isar proof
6.551 - development.\footnote{As there is still no Isar tutorial around, it is best
6.552 - to look at existing Isar examples, see also \S\ref{sec:isar-howto}.}
6.553 -
6.554 -\item Recover the proof structure of a few important theorems.
6.555 -
6.556 -\item Rephrase the original intention of the course of reasoning in terms of
6.557 - Isar proof language elements.
6.558 -
6.559 -\end{enumerate}
6.560 -
6.561 -Certainly, rewriting formal reasoning in Isar requires some additional effort.
6.562 -On the other hand, one gains a human-readable representation of
6.563 -machine-checked formal proof. Depending on the context of application, this
6.564 -might be even indispensable to start with!
6.565 -
6.566 -%%% Local Variables:
6.567 -%%% mode: latex
6.568 -%%% TeX-master: "isar-ref"
6.569 -%%% End:
7.1 --- a/doc-src/IsarRef/isar-ref.tex Wed May 07 13:38:15 2008 +0200
7.2 +++ b/doc-src/IsarRef/isar-ref.tex Wed May 07 15:32:31 2008 +0200
7.3 @@ -86,7 +86,7 @@
7.4
7.5 \appendix
7.6 \input{Thy/document/Quick_Reference.tex}
7.7 -\input{conversion.tex}
7.8 +\input{Thy/document/ML_Tactic.tex}
7.9
7.10 \begingroup
7.11 \bibliographystyle{plain} \small\raggedright\frenchspacing