# HG changeset patch # User wenzelm # Date 1210167151 -7200 # Node ID 2e6726015771a840c8afbcb328b692f4c2d6d073 # Parent d86eb226ecba00ac2172342e94da1df0a5ee743f removed obsolete conversion guide -- converted only section on tactics; diff -r d86eb226ecba -r 2e6726015771 doc-src/IsarRef/IsaMakefile --- a/doc-src/IsarRef/IsaMakefile Wed May 07 13:38:15 2008 +0200 +++ b/doc-src/IsarRef/IsaMakefile Wed May 07 15:32:31 2008 +0200 @@ -22,7 +22,8 @@ HOL-IsarRef: $(LOG)/HOL-IsarRef.gz $(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \ - Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/Quick_Reference.thy + Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/Quick_Reference.thy \ + Thy/ML_Tactic.thy @$(USEDIR) -s IsarRef HOL Thy diff -r d86eb226ecba -r 2e6726015771 doc-src/IsarRef/Makefile --- a/doc-src/IsarRef/Makefile Wed May 07 13:38:15 2008 +0200 +++ b/doc-src/IsarRef/Makefile Wed May 07 15:32:31 2008 +0200 @@ -13,11 +13,13 @@ NAME = isar-ref -FILES = isar-ref.tex Thy/document/intro.tex basics.tex Thy/document/syntax.tex \ - Thy/document/pure.tex Thy/document/Generic.tex logics.tex Thy/document/Quick_Reference.tex \ - conversion.tex \ - ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \ - ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib +FILES = isar-ref.tex basics.tex Thy/document/Generic.tex \ + Thy/document/HOLCF_Specific.tex Thy/document/HOL_Specific.tex \ + Thy/document/ML_Tactic.tex Thy/document/Quick_Reference.tex \ + Thy/document/ZF_Specific.tex Thy/document/intro.tex \ + Thy/document/pure.tex Thy/document/syntax.tex \ + logics.tex ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \ + ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib dvi: $(NAME).dvi diff -r d86eb226ecba -r 2e6726015771 doc-src/IsarRef/Thy/ML_Tactic.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/ML_Tactic.thy Wed May 07 15:32:31 2008 +0200 @@ -0,0 +1,186 @@ +(* $Id$ *) + +theory ML_Tactic +imports Main +begin + +chapter {* ML tactic expressions \label{sec:conv-tac} *} + +text {* + Isar Proof methods closely resemble traditional tactics, when used + in unstructured sequences of @{command "apply"} commands. + Isabelle/Isar provides emulations for all major ML tactics of + classic Isabelle --- mostly for the sake of easy porting of existing + developments, as actual Isar proof texts would demand much less + diversity of proof methods. + + Unlike tactic expressions in ML, Isar proof methods provide proper + concrete syntax for additional arguments, options, modifiers etc. + Thus a typical method text is usually more concise than the + corresponding ML tactic. Furthermore, the Isar versions of classic + Isabelle tactics often cover several variant forms by a single + method with separate options to tune the behavior. For example, + method @{method simp} replaces all of @{ML simp_tac}~/ @{ML + asm_simp_tac}~/ @{ML full_simp_tac}~/ @{ML asm_full_simp_tac}, there + is also concrete syntax for augmenting the Simplifier context (the + current ``simpset'') in a convenient way. +*} + + +section {* Resolution tactics *} + +text {* + Classic Isabelle provides several variant forms of tactics for + single-step rule applications (based on higher-order resolution). + The space of resolution tactics has the following main dimensions. + + \begin{enumerate} + + \item The ``mode'' of resolution: intro, elim, destruct, or forward + (e.g.\ @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac}, + @{ML forward_tac}). + + \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\ + @{ML res_inst_tac}). + + \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac} + vs.\ @{ML rtac}). + + \end{enumerate} + + Basically, the set of Isar tactic emulations @{method rule_tac}, + @{method erule_tac}, @{method drule_tac}, @{method frule_tac} (see + \secref{sec:tactics}) would be sufficient to cover the four modes, + either with or without instantiation, and either with single or + multiple arguments. Although it is more convenient in most cases to + use the plain @{method rule} method (see + \secref{sec:pure-meth-att}), or any of its ``improper'' variants + @{method erule}, @{method drule}, @{method frule} (see + \secref{sec:misc-meth-att}). Note that explicit goal addressing is + only supported by the actual @{method rule_tac} version. + + With this in mind, plain resolution tactics correspond to Isar + methods as follows. + + \medskip + \begin{tabular}{lll} + @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\ + @{ML resolve_tac}~@{text "[a\<^sub>1, \] 1"} & & @{text "rule a\<^sub>1 \"} \\ + @{ML res_inst_tac}~@{text "[(x\<^sub>1, t\<^sub>1), \] a 1"} & & + @{text "rule_tac x\<^sub>1 = t\<^sub>1 \ \ \ a"} \\[0.5ex] + @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\ + @{ML resolve_tac}~@{text "[a\<^sub>1, \] i"} & & @{text "rule_tac [i] a\<^sub>1 \"} \\ + @{ML res_inst_tac}~@{text "[(x\<^sub>1, t\<^sub>1), \] a i"} & & + @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \ \ \ a"} \\ + \end{tabular} + \medskip + + Note that explicit goal addressing may be usually avoided by + changing the order of subgoals with @{command "defer"} or @{command + "prefer"} (see \secref{sec:tactic-commands}). +*} + + +section {* Simplifier tactics *} + +text {* + The main Simplifier tactics @{ML simp_tac} and variants (cf.\ + \cite{isabelle-ref}) are all covered by the @{method simp} and + @{method simp_all} methods (see \secref{sec:simplifier}). Note that + there is no individual goal addressing available, simplification + acts either on the first goal (@{method simp}) or all goals + (@{method simp_all}). + + \medskip + \begin{tabular}{lll} + @{ML asm_full_simp_tac}~@{text "@{simpset} 1"} & & @{method simp} \\ + @{ML ALLGOALS}~(@{ML asm_full_simp_tac}~@{text "@{simpset}"}) & & @{method simp_all} \\[0.5ex] + @{ML simp_tac}~@{text "@{simpset} 1"} & & @{method simp}~@{text "(no_asm)"} \\ + @{ML asm_simp_tac}~@{text "@{simpset} 1"} & & @{method simp}~@{text "(no_asm_simp)"} \\ + @{ML full_simp_tac}~@{text "@{simpset} 1"} & & @{method simp}~@{text "(no_asm_use)"} \\ + @{ML asm_lr_simp_tac}~@{text "@{simpset} 1"} & & @{method simp}~@{text "(asm_lr)"} \\ + \end{tabular} + \medskip +*} + + +section {* Classical Reasoner tactics *} + +text {* + The Classical Reasoner provides a rather large number of variations + of automated tactics, such as @{ML blast_tac}, @{ML fast_tac}, @{ML + clarify_tac} etc.\ (see \cite{isabelle-ref}). The corresponding + Isar methods usually share the same base name, such as @{method + blast}, @{method fast}, @{method clarify} etc.\ (see + \secref{sec:classical}). +*} + + +section {* Miscellaneous tactics *} + +text {* + There are a few additional tactics defined in various theories of + Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. + The most common ones of these may be ported to Isar as follows. + + \medskip + \begin{tabular}{lll} + @{ML stac}~@{text "a 1"} & & @{text "subst a"} \\ + @{ML hyp_subst_tac}~@{text 1} & & @{text hypsubst} \\ + @{ML strip_tac}~@{text 1} & @{text "\"} & @{text "intro strip"} \\ + @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\ + & @{text "\"} & @{text "simp only: split_tupled_all"} \\ + & @{text "\"} & @{text "clarify"} \\ + \end{tabular} +*} + + +section {* Tacticals *} + +text {* + Classic Isabelle provides a huge amount of tacticals for combination + and modification of existing tactics. This has been greatly reduced + in Isar, providing the bare minimum of combinators only: ``@{text + ","}'' (sequential composition), ``@{text "|"}'' (alternative + choices), ``@{text "?"}'' (try), ``@{text "+"}'' (repeat at least + once). These are usually sufficient in practice; if all fails, + arbitrary ML tactic code may be invoked via the @{method tactic} + method (see \secref{sec:tactics}). + + \medskip Common ML tacticals may be expressed directly in Isar as + follows: + + \medskip + \begin{tabular}{lll} + @{text "tac\<^sub>1"}~@{ML_text THEN}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1, meth\<^sub>2"} \\ + @{text "tac\<^sub>1"}~@{ML_text ORELSE}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1 | meth\<^sub>2"} \\ + @{ML TRY}~@{text tac} & & @{text "meth?"} \\ + @{ML REPEAT1}~@{text tac} & & @{text "meth+"} \\ + @{ML REPEAT}~@{text tac} & & @{text "(meth+)?"} \\ + @{ML EVERY}~@{text "[tac\<^sub>1, \]"} & & @{text "meth\<^sub>1, \"} \\ + @{ML FIRST}~@{text "[tac\<^sub>1, \]"} & & @{text "meth\<^sub>1 | \"} \\ + \end{tabular} + \medskip + + \medskip @{ML CHANGED} (see \cite{isabelle-ref}) is usually not + required in Isar, since most basic proof methods already fail unless + there is an actual change in the goal state. Nevertheless, ``@{text + "?"}'' (try) may be used to accept \emph{unchanged} results as + well. + + \medskip @{ML ALLGOALS}, @{ML SOMEGOAL} etc.\ (see + \cite{isabelle-ref}) are not available in Isar, since there is no + direct goal addressing. Nevertheless, some basic methods address + all goals internally, notably @{method simp_all} (see + \secref{sec:simplifier}). Also note that @{ML ALLGOALS} can be + often replaced by ``@{text "+"}'' (repeat at least once), although + this usually has a different operational behavior, such as solving + goals in a different order. + + \medskip Iterated resolution, such as @{ML_text "REPEAT (FIRSTGOAL + (resolve_tac \))"}, is usually better expressed using the @{method + intro} and @{method elim} methods of Isar (see + \secref{sec:classical}). +*} + +end diff -r d86eb226ecba -r 2e6726015771 doc-src/IsarRef/Thy/ROOT.ML --- a/doc-src/IsarRef/Thy/ROOT.ML Wed May 07 13:38:15 2008 +0200 +++ b/doc-src/IsarRef/Thy/ROOT.ML Wed May 07 15:32:31 2008 +0200 @@ -10,3 +10,4 @@ use_thy "Generic"; use_thy "HOL_Specific"; use_thy "Quick_Reference"; +use_thy "ML_Tactic"; diff -r d86eb226ecba -r 2e6726015771 doc-src/IsarRef/Thy/document/ML_Tactic.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex Wed May 07 15:32:31 2008 +0200 @@ -0,0 +1,226 @@ +% +\begin{isabellebody}% +\def\isabellecontext{ML{\isacharunderscore}Tactic}% +% +\isadelimtheory +\isanewline +\isanewline +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ ML{\isacharunderscore}Tactic\isanewline +\isakeyword{imports}\ Main\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupchapter{ML tactic expressions \label{sec:conv-tac}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Isar Proof methods closely resemble traditional tactics, when used + in unstructured sequences of \mbox{\isa{\isacommand{apply}}} commands. + Isabelle/Isar provides emulations for all major ML tactics of + classic Isabelle --- mostly for the sake of easy porting of existing + developments, as actual Isar proof texts would demand much less + diversity of proof methods. + + Unlike tactic expressions in ML, Isar proof methods provide proper + concrete syntax for additional arguments, options, modifiers etc. + Thus a typical method text is usually more concise than the + corresponding ML tactic. Furthermore, the Isar versions of classic + Isabelle tactics often cover several variant forms by a single + method with separate options to tune the behavior. For example, + method \mbox{\isa{simp}} replaces all of \verb|simp_tac|~/ \verb|asm_simp_tac|~/ \verb|full_simp_tac|~/ \verb|asm_full_simp_tac|, there + is also concrete syntax for augmenting the Simplifier context (the + current ``simpset'') in a convenient way.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Resolution tactics% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Classic Isabelle provides several variant forms of tactics for + single-step rule applications (based on higher-order resolution). + The space of resolution tactics has the following main dimensions. + + \begin{enumerate} + + \item The ``mode'' of resolution: intro, elim, destruct, or forward + (e.g.\ \verb|resolve_tac|, \verb|eresolve_tac|, \verb|dresolve_tac|, + \verb|forward_tac|). + + \item Optional explicit instantiation (e.g.\ \verb|resolve_tac| vs.\ + \verb|res_inst_tac|). + + \item Abbreviations for singleton arguments (e.g.\ \verb|resolve_tac| + vs.\ \verb|rtac|). + + \end{enumerate} + + Basically, the set of Isar tactic emulations \mbox{\isa{rule{\isacharunderscore}tac}}, + \mbox{\isa{erule{\isacharunderscore}tac}}, \mbox{\isa{drule{\isacharunderscore}tac}}, \mbox{\isa{frule{\isacharunderscore}tac}} (see + \secref{sec:tactics}) would be sufficient to cover the four modes, + either with or without instantiation, and either with single or + multiple arguments. Although it is more convenient in most cases to + use the plain \mbox{\isa{rule}} method (see + \secref{sec:pure-meth-att}), or any of its ``improper'' variants + \mbox{\isa{erule}}, \mbox{\isa{drule}}, \mbox{\isa{frule}} (see + \secref{sec:misc-meth-att}). Note that explicit goal addressing is + only supported by the actual \mbox{\isa{rule{\isacharunderscore}tac}} version. + + With this in mind, plain resolution tactics correspond to Isar + methods as follows. + + \medskip + \begin{tabular}{lll} + \verb|rtac|~\isa{{\isachardoublequote}a\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}rule\ a{\isachardoublequote}} \\ + \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}} \\ + \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}} & & + \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\[0.5ex] + \verb|rtac|~\isa{{\isachardoublequote}a\ i{\isachardoublequote}} & & \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ a{\isachardoublequote}} \\ + \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}} \\ + \verb|res_inst_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ i{\isachardoublequote}} & & + \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\ + \end{tabular} + \medskip + + Note that explicit goal addressing may be usually avoided by + changing the order of subgoals with \mbox{\isa{\isacommand{defer}}} or \mbox{\isa{\isacommand{prefer}}} (see \secref{sec:tactic-commands}).% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Simplifier tactics% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The main Simplifier tactics \verb|simp_tac| and variants (cf.\ + \cite{isabelle-ref}) are all covered by the \mbox{\isa{simp}} and + \mbox{\isa{simp{\isacharunderscore}all}} methods (see \secref{sec:simplifier}). Note that + there is no individual goal addressing available, simplification + acts either on the first goal (\mbox{\isa{simp}}) or all goals + (\mbox{\isa{simp{\isacharunderscore}all}}). + + \medskip + \begin{tabular}{lll} + \verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \mbox{\isa{simp}} \\ + \verb|ALLGOALS|~(\verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}{\isachardoublequote}}) & & \mbox{\isa{simp{\isacharunderscore}all}} \\[0.5ex] + \verb|simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \mbox{\isa{simp}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}} \\ + \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}} \\ + \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}} \\ + \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}} \\ + \end{tabular} + \medskip% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Classical Reasoner tactics% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The Classical Reasoner provides a rather large number of variations + of automated tactics, such as \verb|blast_tac|, \verb|fast_tac|, \verb|clarify_tac| etc.\ (see \cite{isabelle-ref}). The corresponding + Isar methods usually share the same base name, such as \mbox{\isa{blast}}, \mbox{\isa{fast}}, \mbox{\isa{clarify}} etc.\ (see + \secref{sec:classical}).% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Miscellaneous tactics% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +There are a few additional tactics defined in various theories of + Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. + The most common ones of these may be ported to Isar as follows. + + \medskip + \begin{tabular}{lll} + \verb|stac|~\isa{{\isachardoublequote}a\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}subst\ a{\isachardoublequote}} \\ + \verb|hyp_subst_tac|~\isa{{\isadigit{1}}} & & \isa{hypsubst} \\ + \verb|strip_tac|~\isa{{\isadigit{1}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & \isa{{\isachardoublequote}intro\ strip{\isachardoublequote}} \\ + \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}} \\ + & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & \isa{{\isachardoublequote}simp\ only{\isacharcolon}\ split{\isacharunderscore}tupled{\isacharunderscore}all{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isasymlless}{\isachardoublequote}} & \isa{{\isachardoublequote}clarify{\isachardoublequote}} \\ + \end{tabular}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Tacticals% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Classic Isabelle provides a huge amount of tacticals for combination + and modification of existing tactics. This has been greatly reduced + in Isar, providing the bare minimum of combinators only: ``\isa{{\isachardoublequote}{\isacharcomma}{\isachardoublequote}}'' (sequential composition), ``\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}'' (alternative + choices), ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' (try), ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least + once). These are usually sufficient in practice; if all fails, + arbitrary ML tactic code may be invoked via the \mbox{\isa{tactic}} + method (see \secref{sec:tactics}). + + \medskip Common ML tacticals may be expressed directly in Isar as + follows: + + \medskip + \begin{tabular}{lll} + \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}} \\ + \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}} \\ + \verb|TRY|~\isa{tac} & & \isa{{\isachardoublequote}meth{\isacharquery}{\isachardoublequote}} \\ + \verb|REPEAT1|~\isa{tac} & & \isa{{\isachardoublequote}meth{\isacharplus}{\isachardoublequote}} \\ + \verb|REPEAT|~\isa{tac} & & \isa{{\isachardoublequote}{\isacharparenleft}meth{\isacharplus}{\isacharparenright}{\isacharquery}{\isachardoublequote}} \\ + \verb|EVERY|~\isa{{\isachardoublequote}{\isacharbrackleft}tac\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isachardoublequote}} \\ + \verb|FIRST|~\isa{{\isachardoublequote}{\isacharbrackleft}tac\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}\ {\isacharbar}\ {\isasymdots}{\isachardoublequote}} \\ + \end{tabular} + \medskip + + \medskip \verb|CHANGED| (see \cite{isabelle-ref}) is usually not + required in Isar, since most basic proof methods already fail unless + there is an actual change in the goal state. Nevertheless, ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' (try) may be used to accept \emph{unchanged} results as + well. + + \medskip \verb|ALLGOALS|, \verb|SOMEGOAL| etc.\ (see + \cite{isabelle-ref}) are not available in Isar, since there is no + direct goal addressing. Nevertheless, some basic methods address + all goals internally, notably \mbox{\isa{simp{\isacharunderscore}all}} (see + \secref{sec:simplifier}). Also note that \verb|ALLGOALS| can be + often replaced by ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least once), although + this usually has a different operational behavior, such as solving + goals in a different order. + + \medskip Iterated resolution, such as \verb|REPEAT (FIRSTGOAL|\isasep\isanewline% +\verb| (resolve_tac \))|, is usually better expressed using the \mbox{\isa{intro}} and \mbox{\isa{elim}} methods of Isar (see + \secref{sec:classical}).% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r d86eb226ecba -r 2e6726015771 doc-src/IsarRef/conversion.tex --- a/doc-src/IsarRef/conversion.tex Wed May 07 13:38:15 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,566 +0,0 @@ - -\chapter{Isabelle/Isar conversion guide}\label{ap:conv} - -Subsequently, we give a few practical hints on working in a mixed environment -of old Isabelle ML proof scripts and new Isabelle/Isar theories. There are -basically three ways to cope with this issue. -\begin{enumerate} -\item Do not convert old sources at all, but communicate directly at the level - of \emph{internal} theory and theorem values. -\item Port old-style theory files to new-style ones (very easy), and ML proof - scripts to Isar tactic-emulation scripts (quite easy). -\item Actually redo ML proof scripts as human-readable Isar proof texts - (probably hard, depending who wrote the original scripts). -\end{enumerate} - - -\section{No conversion} - -Internally, Isabelle is able to handle both old and new-style theories at the -same time; the theory loader automatically detects the input format. In any -case, the results are certain internal ML values of type \texttt{theory} and -\texttt{thm}. These may be accessed from either classic Isabelle or -Isabelle/Isar, provided that some minimal precautions are observed. - - -\subsection{Referring to theorem and theory values} - -\begin{ttbox} -thm : xstring -> thm -thms : xstring -> thm list -the_context : unit -> theory -theory : string -> theory -\end{ttbox} - -These functions provide general means to refer to logical objects from ML. -Old-style theories used to emit many ML bindings of theorems and theories, but -this is no longer done in new-style Isabelle/Isar theories. - -\begin{descr} -\item [$\mathtt{thm}~name$ and $\mathtt{thms}~name$] retrieve theorems stored - in the current theory context, including any ancestor node. - - The convention of old-style theories was to bind any theorem as an ML value - as well. New-style theories no longer do this, so ML code may require - \texttt{thm~"foo"} rather than just \texttt{foo}. - -\item [$\mathtt{the_context()}$] refers to the current theory context. - - Old-style theories often use the ML binding \texttt{thy}, which is - dynamically created by the ML code generated from old theory source. This - is no longer the recommended way in any case! Function \texttt{the_context} - should be used for old scripts as well. - -\item [$\mathtt{theory}~name$] retrieves the named theory from the global - theory-loader database. - - The ML code generated from old-style theories would include an ML binding - $name\mathtt{.thy}$ as part of an ML structure. -\end{descr} - - -\subsection{Storing theorem values} - -\begin{ttbox} -qed : string -> unit -bind_thm : string * thm -> unit -bind_thms : string * thm list -> unit -\end{ttbox} - -ML proof scripts have to be well-behaved by storing theorems properly within -the current theory context, in order to enable new-style theories to retrieve -these later. - -\begin{descr} - -\item [$\mathtt{qed}~name$] is the canonical way to conclude a proof script in - ML. This already manages entry in the theorem database of the current - theory context. - -\item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$] - store theorems that have been produced in ML in an ad-hoc manner. - -\end{descr} - -Note that the original ``LCF-system'' approach of binding theorem values on -the ML toplevel only has long been given up in Isabelle! Despite of this, old -legacy proof scripts occasionally contain code such as \texttt{val foo = - result();} which is ill-behaved in several respects. Apart from preventing -access from Isar theories, it also omits the result from the WWW presentation, -for example. - - -\subsection{ML declarations in Isar} - -\begin{matharray}{rcl} - \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\ - \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -Isabelle/Isar theories may contain ML declarations as well. For example, an -old-style theorem binding may be mimicked as follows. -\[ -\isarkeyword{ML}~\{*~\mbox{\texttt{val foo = thm "foo"}}~*\} -\] -Note that this command cannot be undone, so invalid theorem bindings in ML may -persist. Also note that the current theory may not be modified; use -$\isarkeyword{ML_setup}$ for declarations that act on the current context. - - -\section{Porting theories and proof scripts}\label{sec:port-scripts} - -Porting legacy theory and ML files to proper Isabelle/Isar theories has -several advantages. For example, the Proof~General user interface -\cite{proofgeneral} for Isabelle/Isar is more robust and more comfortable to -use than the version for classic Isabelle. This is due to the fact that the -generic ML toplevel has been replaced by a separate Isar interaction loop, -with full control over input synchronization and error conditions. - -Furthermore, the Isabelle document preparation system (see also -\cite{isabelle-sys}) only works properly with new-style theories. Output of -old-style sources is at the level of individual characters (and symbols), -without proper document markup as in Isabelle/Isar theories. - - -\subsection{Theories} - -Basically, the Isabelle/Isar theory syntax is a proper superset of the classic -one. Only a few quirks and legacy problems have been eliminated, resulting in -simpler rules and less special cases. The main changes of theory syntax are -as follows. - -\begin{itemize} -\item Quoted strings may contain arbitrary white space, and span several lines - without requiring \verb,\,\,\dots\verb,\, escapes. -\item Names may always be quoted. - - The old syntax would occasionally demand plain identifiers vs.\ quoted - strings to accommodate certain syntactic features. -\item Types and terms have to be \emph{atomic} as far as the theory syntax is - concerned; this typically requires quoting of input strings, e.g.\ ``$x + - y$''. - - The old theory syntax used to fake part of the syntax of types in order to - require less quoting in common cases; this was hard to predict, though. On - the other hand, Isar does not require quotes for simple terms, such as plain - identifiers $x$, numerals $1$, or symbols $\forall$ (input as - \verb,\,). -\item Theorem declarations require an explicit colon to separate the name from - the statement (the name is usually optional). Cf.\ the syntax of $\DEFS$ in - \S\ref{sec:consts}, or $\THEOREMNAME$ in \S\ref{sec:axms-thms}. -\end{itemize} - -Note that Isabelle/Isar error messages are usually quite explicit about the -problem at hand. So in cases of doubt, input syntax may be just as well tried -out interactively. - - -\subsection{Goal statements}\label{sec:conv-goal} - -\subsubsection{Simple goals} - -In ML the canonical a goal statement together with a complete proof script is -as follows: -\begin{ttbox} - Goal "\(\phi\)"; - by \(tac@1\); - \(\vdots\) - qed "\(name\)"; -\end{ttbox} -This form may be turned into an Isar tactic-emulation script like this: -\begin{matharray}{l} - \LEMMA{name}{\texttt"{\phi}\texttt"} \\ - \quad \APPLY{meth@1} \\ - \qquad \vdots \\ - \quad \DONE \\ -\end{matharray} -Note that the main statement may be $\THEOREMNAME$ or $\COROLLARYNAME$ as -well. See \S\ref{sec:conv-tac} for further details on how to convert actual -tactic expressions into proof methods. - -\medskip Classic Isabelle provides many variant forms of goal commands, see -also \cite{isabelle-ref} for further details. The second most common one is -\texttt{Goalw}, which expands definitions before commencing the actual proof -script. -\begin{ttbox} - Goalw [\(def@1\), \(\dots\)] "\(\phi\)"; -\end{ttbox} -This may be replaced by using the $unfold$ proof method explicitly. -\begin{matharray}{l} -\LEMMA{name}{\texttt"{\phi}\texttt"} \\ -\quad \APPLY{(unfold~def@1~\dots)} \\ -\end{matharray} - - -\subsubsection{Deriving rules} - -Deriving non-atomic meta-level propositions requires special precautions in -classic Isabelle: the primitive \texttt{goal} command decomposes a statement -into the atomic conclusion and a list of assumptions, which are exhibited as -ML values of type \texttt{thm}. After the proof is finished, these premises -are discharged again, resulting in the original rule statement. The ``long -format'' of Isabelle/Isar goal statements admits to emulate this technique -nicely. The general ML goal statement for derived rules looks like this: -\begin{ttbox} - val [\(prem@1\), \dots] = goal "\(\phi@1 \Imp \dots \Imp \psi\)"; - by \(tac@1\); - \(\vdots\) - qed "\(a\)" -\end{ttbox} -This form may be turned into a tactic-emulation script as follows: -\begin{matharray}{l} - \LEMMA{a}{} \\ - \quad \ASSUMES{prem@1}{\texttt"\phi@1\texttt"}~\AND~\dots \\ - \quad \SHOWS{}{\texttt"{\psi}\texttt"} \\ - \qquad \APPLY{meth@1} \\ - \qquad\quad \vdots \\ - \qquad \DONE \\ -\end{matharray} - -\medskip In practice, actual rules are often rather direct consequences of -corresponding atomic statements, typically stemming from the definition of a -new concept. In that case, the general scheme for deriving rules may be -greatly simplified, using one of the standard automated proof tools, such as -$simp$, $blast$, or $auto$. This could work as follows: -\begin{matharray}{l} - \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\ - \quad \BYY{(unfold~defs)}{blast} \\ -\end{matharray} -Note that classic Isabelle would support this form only in the special case -where $\phi@1$, \dots are atomic statements (when using the standard -\texttt{Goal} command). Otherwise the special treatment of rules would be -applied, disturbing this simple setup. - -\medskip Occasionally, derived rules would be established by first proving an -appropriate atomic statement (using $\forall$ and $\longrightarrow$ of the -object-logic), and putting the final result into ``rule format''. In classic -Isabelle this would usually proceed as follows: -\begin{ttbox} - Goal "\(\phi\)"; - by \(tac@1\); - \(\vdots\) - qed_spec_mp "\(name\)"; -\end{ttbox} -The operation performed by \texttt{qed_spec_mp} is also performed by the Isar -attribute ``$rule_format$'', see also \S\ref{sec:object-logic}. Thus the -corresponding Isar text may look like this: -\begin{matharray}{l} - \LEMMA{name~[rule_format]}{\texttt"{\phi}\texttt"} \\ - \quad \APPLY{meth@1} \\ - \qquad \vdots \\ - \quad \DONE \\ -\end{matharray} -Note plain ``$rule_format$'' actually performs a slightly different operation: -it fully replaces object-level implication and universal quantification -throughout the whole result statement. This is the right thing in most cases. -For historical reasons, \texttt{qed_spec_mp} would only operate on the -conclusion; one may get this exact behavior by using -``$rule_format~(no_asm)$'' instead. - -\medskip Actually ``$rule_format$'' is a bit unpleasant to work with, since -the final result statement is not shown in the text. An alternative is to -state the resulting rule in the intended form in the first place, and have the -initial refinement step turn it into internal object-logic form using the -$atomize$ method indicated below. The remaining script is unchanged. - -\begin{matharray}{l} - \LEMMA{name}{\texttt"{\All{\vec x}\vec\phi \Imp \psi}\texttt"} \\ - \quad \APPLY{(atomize~(full))} \\ - \quad \APPLY{meth@1} \\ - \qquad \vdots \\ - \quad \DONE \\ -\end{matharray} - -In many situations the $atomize$ step above is actually unnecessary, -especially if the subsequent script mainly consists of automated tools. - - -\subsection{Tactics}\label{sec:conv-tac} - -Isar Proof methods closely resemble traditional tactics, when used in -unstructured sequences of $\APPLYNAME$ commands (cf.\ \S\ref{sec:conv-goal}). -Isabelle/Isar provides emulations for all major ML tactics of classic Isabelle ---- mostly for the sake of easy porting of existing developments, as actual -Isar proof texts would demand much less diversity of proof methods. - -Unlike tactic expressions in ML, Isar proof methods provide proper concrete -syntax for additional arguments, options, modifiers etc. Thus a typical -method text is usually more concise than the corresponding ML tactic. -Furthermore, the Isar versions of classic Isabelle tactics often cover several -variant forms by a single method with separate options to tune the behavior. -For example, method $simp$ replaces all of \texttt{simp_tac}~/ -\texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac}, -there is also concrete syntax for augmenting the Simplifier context (the -current ``simpset'') in a convenient way. - - -\subsubsection{Resolution tactics} - -Classic Isabelle provides several variant forms of tactics for single-step -rule applications (based on higher-order resolution). The space of resolution -tactics has the following main dimensions. -\begin{enumerate} -\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\ - \texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac}, - \texttt{forward_tac}). -\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\ - \texttt{res_inst_tac}). -\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\ - \texttt{rtac}). -\end{enumerate} - -Basically, the set of Isar tactic emulations $rule_tac$, $erule_tac$, -$drule_tac$, $frule_tac$ (see \S\ref{sec:tactics}) would be sufficient to -cover the four modes, either with or without instantiation, and either with -single or multiple arguments. Although it is more convenient in most cases to -use the plain $rule$ method (see \S\ref{sec:pure-meth-att}), or any of its -``improper'' variants $erule$, $drule$, $frule$ (see -\S\ref{sec:misc-meth-att}). Note that explicit goal addressing is only -supported by the actual $rule_tac$ version. - -With this in mind, plain resolution tactics may be ported as follows. -\begin{matharray}{lll} - \texttt{rtac}~a~1 & & rule~a \\ - \texttt{resolve_tac}~[a@1, \dots]~1 & & rule~a@1~\dots \\ - \texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~1 & & - rule_tac~x@1 = t@1~and~\dots~in~a \\[0.5ex] - \texttt{rtac}~a~i & & rule_tac~[i]~a \\ - \texttt{resolve_tac}~[a@1, \dots]~i & & rule_tac~[i]~a@1~\dots \\ - \texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~i & & - rule_tac~[i]~x@1 = t@1~and~\dots~in~a \\ -\end{matharray} - -Note that explicit goal addressing may be usually avoided by changing the -order of subgoals with $\isarkeyword{defer}$ or $\isarkeyword{prefer}$ (see -\S\ref{sec:tactic-commands}). - -\medskip Some further (less frequently used) combinations of basic resolution -tactics may be expressed as follows. -\begin{matharray}{lll} - \texttt{ares_tac}~[a@1, \dots]~1 & & assumption~|~rule~a@1~\dots \\ - \texttt{eatac}~a~n~1 & & erule~(n)~a \\ - \texttt{datac}~a~n~1 & & drule~(n)~a \\ - \texttt{fatac}~a~n~1 & & frule~(n)~a \\ -\end{matharray} - - -\subsubsection{Simplifier tactics} - -The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants -(cf.\ \cite{isabelle-ref}) are all covered by the $simp$ and $simp_all$ -methods (see \S\ref{sec:simplifier}). Note that there is no individual goal -addressing available, simplification acts either on the first goal ($simp$) or -all goals ($simp_all$). - -\begin{matharray}{lll} - \texttt{Asm_full_simp_tac 1} & & simp \\ - \texttt{ALLGOALS Asm_full_simp_tac} & & simp_all \\[0.5ex] - \texttt{Simp_tac 1} & & simp~(no_asm) \\ - \texttt{Asm_simp_tac 1} & & simp~(no_asm_simp) \\ - \texttt{Full_simp_tac 1} & & simp~(no_asm_use) \\ - \texttt{Asm_lr_simp_tac 1} & & simp~(asm_lr) \\ -\end{matharray} - -Isar also provides separate method modifier syntax for augmenting the -Simplifier context (see \S\ref{sec:simplifier}), which is known as the -``simpset'' in ML. A typical ML expression with simpset changes looks like -this: -\begin{ttbox} -asm_full_simp_tac (simpset () addsimps [\(a@1\), \(\dots\)] delsimps [\(b@1\), \(\dots\)]) 1 -\end{ttbox} -The corresponding Isar text is as follows: -\[ -simp~add:~a@1~\dots~del:~b@1~\dots -\] -Global declarations of Simplifier rules (e.g.\ \texttt{Addsimps}) are covered -by application of attributes, see \S\ref{sec:conv-decls} for more information. - - -\subsubsection{Classical Reasoner tactics} - -The Classical Reasoner provides a rather large number of variations of -automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac}, -\texttt{Clarify_tac} etc.\ (see \cite{isabelle-ref}). The corresponding Isar -methods usually share the same base name, such as $blast$, $fast$, $clarify$ -etc.\ (see \S\ref{sec:classical}). - -Similar to the Simplifier, there is separate method modifier syntax for -augmenting the Classical Reasoner context, which is known as the ``claset'' in -ML. A typical ML expression with claset changes looks like this: -\begin{ttbox} -blast_tac (claset () addIs [\(a@1\), \(\dots\)] addSEs [\(b@1\), \(\dots\)]) 1 -\end{ttbox} -The corresponding Isar text is as follows: -\[ -blast~intro:~a@1~\dots~elim!:~b@1~\dots -\] -Global declarations of Classical Reasoner rules (e.g.\ \texttt{AddIs}) are -covered by application of attributes, see \S\ref{sec:conv-decls} for more -information. - - -\subsubsection{Miscellaneous tactics} - -There are a few additional tactics defined in various theories of -Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. The most -common ones of these may be ported to Isar as follows. - -\begin{matharray}{lll} - \texttt{stac}~a~1 & & subst~a \\ - \texttt{hyp_subst_tac}~1 & & hypsubst \\ - \texttt{strip_tac}~1 & \approx & intro~strip \\ - \texttt{split_all_tac}~1 & & simp~(no_asm_simp)~only:~split_tupled_all \\ - & \approx & simp~only:~split_tupled_all \\ - & \ll & clarify \\ -\end{matharray} - - -\subsubsection{Tacticals} - -Classic Isabelle provides a huge amount of tacticals for combination and -modification of existing tactics. This has been greatly reduced in Isar, -providing the bare minimum of combinators only: ``$,$'' (sequential -composition), ``$|$'' (alternative choices), ``$?$'' (try), ``$+$'' (repeat at -least once). These are usually sufficient in practice; if all fails, -arbitrary ML tactic code may be invoked via the $tactic$ method (see -\S\ref{sec:tactics}). - -\medskip Common ML tacticals may be expressed directly in Isar as follows: -\begin{matharray}{lll} -tac@1~\texttt{THEN}~tac@2 & & meth@1, meth@2 \\ -tac@1~\texttt{ORELSE}~tac@2 & & meth@1~|~meth@2 \\ -\texttt{TRY}~tac & & meth? \\ -\texttt{REPEAT1}~tac & & meth+ \\ -\texttt{REPEAT}~tac & & (meth+)? \\ -\texttt{EVERY}~[tac@1, \dots] & & meth@1, \dots \\ -\texttt{FIRST}~[tac@1, \dots] & & meth@1~|~\dots \\ -\end{matharray} - -\medskip \texttt{CHANGED} (see \cite{isabelle-ref}) is usually not required in -Isar, since most basic proof methods already fail unless there is an actual -change in the goal state. Nevertheless, ``$?$'' (try) may be used to accept -\emph{unchanged} results as well. - -\medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelle-ref}) -are not available in Isar, since there is no direct goal addressing. -Nevertheless, some basic methods address all goals internally, notably -$simp_all$ (see \S\ref{sec:simplifier}). Also note that \texttt{ALLGOALS} may -be often replaced by ``$+$'' (repeat at least once), although this usually has -a different operational behavior, such as solving goals in a different order. - -\medskip Iterated resolution, such as -\texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed -using the $intro$ and $elim$ methods of Isar (see \S\ref{sec:classical}). - - -\subsection{Declarations and ad-hoc operations}\label{sec:conv-decls} - -Apart from proof commands and tactic expressions, almost all of the remaining -ML code occurring in legacy proof scripts are either global context -declarations (such as \texttt{Addsimps}) or ad-hoc operations on theorems -(such as \texttt{RS}). In Isar both of these are covered by theorem -expressions with \emph{attributes}. - -\medskip Theorem operations may be attached as attributes in the very place -where theorems are referenced, say within a method argument. The subsequent -ML combinators may be expressed directly in Isar as follows. -\begin{matharray}{lll} - thm@1~\texttt{RS}~thm@2 & & thm@1~[THEN~thm@2] \\ - thm@1~\texttt{RSN}~(i, thm@2) & & thm@1~[THEN~[i]~thm@2] \\ - thm@1~\texttt{COMP}~thm@2 & & thm@1~[COMP~thm@2] \\ - \relax[thm@1, \dots]~\texttt{MRS}~thm & & thm~[OF~thm@1~\dots] \\ - \texttt{read_instantiate}~[(x@1, t@1), \dots]~thm & & thm~[where~x@1 = t@1~and~\dots] \\ - \texttt{make_elim}~thm & & thm~[elim_format] \\ - \texttt{standard}~thm & & thm~[standard] \\ -\end{matharray} - -Note that $OF$ is often more readable as $THEN$; likewise positional -instantiation with $of$ is often more appropriate than $where$. - -The special ML command \texttt{qed_spec_mp} of Isabelle/HOL and FOL may be -replaced by passing the result of a proof through $rule_format$. - -\medskip Global ML declarations may be expressed using the $\DECLARE$ command -(see \S\ref{sec:tactic-commands}) together with appropriate attributes. The -most common ones are as follows. -\begin{matharray}{lll} - \texttt{Addsimps}~[thm] & & \DECLARE~thm~[simp] \\ - \texttt{Delsimps}~[thm] & & \DECLARE~thm~[simp~del] \\ - \texttt{Addsplits}~[thm] & & \DECLARE~thm~[split] \\ - \texttt{Delsplits}~[thm] & & \DECLARE~thm~[split~del] \\[0.5ex] - \texttt{AddIs}~[thm] & & \DECLARE~thm~[intro] \\ - \texttt{AddEs}~[thm] & & \DECLARE~thm~[elim] \\ - \texttt{AddDs}~[thm] & & \DECLARE~thm~[dest] \\ - \texttt{AddSIs}~[thm] & & \DECLARE~thm~[intro!] \\ - \texttt{AddSEs}~[thm] & & \DECLARE~thm~[elim!] \\ - \texttt{AddSDs}~[thm] & & \DECLARE~thm~[dest!] \\[0.5ex] - \texttt{AddIffs}~[thm] & & \DECLARE~thm~[iff] \\ -\end{matharray} -Note that explicit $\DECLARE$ commands are rarely needed in practice; Isar -admits to declare theorems on-the-fly wherever they emerge. Consider the -following ML idiom: -\begin{ttbox} -Goal "\(\phi\)"; - \(\vdots\) -qed "name"; -Addsimps [name]; -\end{ttbox} -This may be expressed more succinctly in Isar like this: -\begin{matharray}{l} - \LEMMA{name~[simp]}{\phi} \\ - \quad\vdots -\end{matharray} -The $name$ may be even omitted, although this would make it difficult to -declare the theorem otherwise later (e.g.\ as $[simp~del]$). - - -\section{Writing actual Isar proof texts} - -Porting legacy ML proof scripts into Isar tactic emulation scripts (see -\S\ref{sec:port-scripts}) is mainly a technical issue, since the basic -representation of formal ``proof script'' is preserved. In contrast, -converting existing Isabelle developments into actual human-readably Isar -proof texts is more involved, due to the fundamental change of the underlying -paradigm. - -This issue is comparable to that of converting programs written in a low-level -programming languages (say Assembler) into higher-level ones (say Haskell). -In order to accomplish this, one needs a working knowledge of the target -language, as well an understanding of the \emph{original} idea of the piece of -code expressed in the low-level language. - -As far as Isar proofs are concerned, it is usually much easier to re-use only -definitions and the main statements, while following the arrangement of proof -scripts only very loosely. Ideally, one would also have some \emph{informal} -proof outlines available for guidance as well. In the worst case, obscure -proof scripts would have to be re-engineered by tracing forth and backwards, -and by educated guessing! - -\medskip This is a possible schedule to embark on actual conversion of legacy -proof scripts into Isar proof texts. - -\begin{enumerate} - -\item Port ML scripts to Isar tactic emulation scripts (see - \S\ref{sec:port-scripts}). - -\item Get sufficiently acquainted with Isabelle/Isar proof - development.\footnote{As there is still no Isar tutorial around, it is best - to look at existing Isar examples, see also \S\ref{sec:isar-howto}.} - -\item Recover the proof structure of a few important theorems. - -\item Rephrase the original intention of the course of reasoning in terms of - Isar proof language elements. - -\end{enumerate} - -Certainly, rewriting formal reasoning in Isar requires some additional effort. -On the other hand, one gains a human-readable representation of -machine-checked formal proof. Depending on the context of application, this -might be even indispensable to start with! - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "isar-ref" -%%% End: diff -r d86eb226ecba -r 2e6726015771 doc-src/IsarRef/isar-ref.tex --- a/doc-src/IsarRef/isar-ref.tex Wed May 07 13:38:15 2008 +0200 +++ b/doc-src/IsarRef/isar-ref.tex Wed May 07 15:32:31 2008 +0200 @@ -86,7 +86,7 @@ \appendix \input{Thy/document/Quick_Reference.tex} -\input{conversion.tex} +\input{Thy/document/ML_Tactic.tex} \begingroup \bibliographystyle{plain} \small\raggedright\frenchspacing