removed outdated and mostly obsolete material;
authorwenzelm
Mon Jul 06 11:14:44 2015 +0200 (2015-07-06)
changeset 60656aabae0331b2f
parent 60655 98b64a1deff0
child 60657 3509a2ce2e8f
removed outdated and mostly obsolete material;
src/Doc/Isar_Ref/ML_Tactic.thy
src/Doc/Isar_Ref/document/root.tex
src/Doc/ROOT
     1.1 --- a/src/Doc/Isar_Ref/ML_Tactic.thy	Mon Jul 06 10:56:14 2015 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,177 +0,0 @@
     1.4 -theory ML_Tactic
     1.5 -imports Base Main
     1.6 -begin
     1.7 -
     1.8 -chapter \<open>ML tactic expressions\<close>
     1.9 -
    1.10 -text \<open>
    1.11 -  Isar Proof methods closely resemble traditional tactics, when used
    1.12 -  in unstructured sequences of @{command "apply"} commands.
    1.13 -  Isabelle/Isar provides emulations for all major ML tactics of
    1.14 -  classic Isabelle --- mostly for the sake of easy porting of existing
    1.15 -  developments, as actual Isar proof texts would demand much less
    1.16 -  diversity of proof methods.
    1.17 -
    1.18 -  Unlike tactic expressions in ML, Isar proof methods provide proper
    1.19 -  concrete syntax for additional arguments, options, modifiers etc.
    1.20 -  Thus a typical method text is usually more concise than the
    1.21 -  corresponding ML tactic.  Furthermore, the Isar versions of classic
    1.22 -  Isabelle tactics often cover several variant forms by a single
    1.23 -  method with separate options to tune the behavior.  For example,
    1.24 -  method @{method simp} replaces all of @{ML simp_tac}~/ @{ML
    1.25 -  asm_simp_tac}~/ @{ML full_simp_tac}~/ @{ML asm_full_simp_tac}, there
    1.26 -  is also concrete syntax for augmenting the Simplifier context (the
    1.27 -  current ``simpset'') in a convenient way.
    1.28 -\<close>
    1.29 -
    1.30 -
    1.31 -section \<open>Resolution tactics\<close>
    1.32 -
    1.33 -text \<open>
    1.34 -  Classic Isabelle provides several variant forms of tactics for
    1.35 -  single-step rule applications (based on higher-order resolution).
    1.36 -  The space of resolution tactics has the following main dimensions.
    1.37 -
    1.38 -  \begin{enumerate}
    1.39 -
    1.40 -  \item The ``mode'' of resolution: intro, elim, destruct, or forward
    1.41 -  (e.g.\ @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac},
    1.42 -  @{ML forward_tac}).
    1.43 -
    1.44 -  \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\
    1.45 -  @{ML Rule_Insts.res_inst_tac}).
    1.46 -
    1.47 -  \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac}
    1.48 -  vs.\ @{ML rtac}).
    1.49 -
    1.50 -  \end{enumerate}
    1.51 -
    1.52 -  Basically, the set of Isar tactic emulations @{method rule_tac},
    1.53 -  @{method erule_tac}, @{method drule_tac}, @{method frule_tac} (see
    1.54 -  \secref{sec:tactics}) would be sufficient to cover the four modes,
    1.55 -  either with or without instantiation, and either with single or
    1.56 -  multiple arguments.  Although it is more convenient in most cases to
    1.57 -  use the plain @{method_ref (Pure) rule} method, or any of its
    1.58 -  ``improper'' variants @{method erule}, @{method drule}, @{method
    1.59 -  frule}.  Note that explicit goal addressing is only supported by the
    1.60 -  actual @{method rule_tac} version.
    1.61 -
    1.62 -  With this in mind, plain resolution tactics correspond to Isar
    1.63 -  methods as follows.
    1.64 -
    1.65 -  \medskip
    1.66 -  \begin{tabular}{lll}
    1.67 -    @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\
    1.68 -    @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
    1.69 -    @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
    1.70 -    @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
    1.71 -    @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
    1.72 -    @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
    1.73 -    @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
    1.74 -    @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
    1.75 -  \end{tabular}
    1.76 -  \medskip
    1.77 -
    1.78 -  Note that explicit goal addressing may be usually avoided by
    1.79 -  changing the order of subgoals with @{command "defer"} or @{command
    1.80 -  "prefer"} (see \secref{sec:tactic-commands}).
    1.81 -\<close>
    1.82 -
    1.83 -
    1.84 -section \<open>Simplifier tactics\<close>
    1.85 -
    1.86 -text \<open>The main Simplifier tactics @{ML simp_tac} and variants are
    1.87 -  all covered by the @{method simp} and @{method simp_all} methods
    1.88 -  (see \secref{sec:simplifier}).  Note that there is no individual
    1.89 -  goal addressing available, simplification acts either on the first
    1.90 -  goal (@{method simp}) or all goals (@{method simp_all}).
    1.91 -
    1.92 -  \medskip
    1.93 -  \begin{tabular}{lll}
    1.94 -    @{ML asm_full_simp_tac}~@{text "@{context} 1"} & & @{method simp} \\
    1.95 -    @{ML ALLGOALS}~(@{ML asm_full_simp_tac}~@{text "@{context}"}) & & @{method simp_all} \\[0.5ex]
    1.96 -    @{ML simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm)"} \\
    1.97 -    @{ML asm_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm_simp)"} \\
    1.98 -    @{ML full_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm_use)"} \\
    1.99 -    @{ML asm_lr_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(asm_lr)"} \\
   1.100 -  \end{tabular}
   1.101 -  \medskip
   1.102 -\<close>
   1.103 -
   1.104 -
   1.105 -section \<open>Classical Reasoner tactics\<close>
   1.106 -
   1.107 -text \<open>The Classical Reasoner provides a rather large number of
   1.108 -  variations of automated tactics, such as @{ML blast_tac}, @{ML
   1.109 -  fast_tac}, @{ML clarify_tac} etc.  The corresponding Isar methods
   1.110 -  usually share the same base name, such as @{method blast}, @{method
   1.111 -  fast}, @{method clarify} etc.\ (see \secref{sec:classical}).\<close>
   1.112 -
   1.113 -
   1.114 -section \<open>Miscellaneous tactics\<close>
   1.115 -
   1.116 -text \<open>
   1.117 -  There are a few additional tactics defined in various theories of
   1.118 -  Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF.
   1.119 -  The most common ones of these may be ported to Isar as follows.
   1.120 -
   1.121 -  \medskip
   1.122 -  \begin{tabular}{lll}
   1.123 -    @{ML stac}~@{text "a 1"} & & @{text "subst a"} \\
   1.124 -    @{ML hyp_subst_tac}~@{text 1} & & @{text hypsubst} \\
   1.125 -    @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\
   1.126 -      & @{text "\<approx>"} & @{text "simp only: split_tupled_all"} \\
   1.127 -      & @{text "\<lless>"} & @{text "clarify"} \\
   1.128 -  \end{tabular}
   1.129 -\<close>
   1.130 -
   1.131 -
   1.132 -section \<open>Tacticals\<close>
   1.133 -
   1.134 -text \<open>
   1.135 -  Classic Isabelle provides a huge amount of tacticals for combination
   1.136 -  and modification of existing tactics.  This has been greatly reduced
   1.137 -  in Isar, providing the bare minimum of combinators only: ``@{text
   1.138 -  ","}'' (sequential composition), ``@{text "|"}'' (alternative
   1.139 -  choices), ``@{text "?"}'' (try), ``@{text "+"}'' (repeat at least
   1.140 -  once).  These are usually sufficient in practice; if all fails,
   1.141 -  arbitrary ML tactic code may be invoked via the @{method tactic}
   1.142 -  method (see \secref{sec:tactics}).
   1.143 -
   1.144 -  \medskip Common ML tacticals may be expressed directly in Isar as
   1.145 -  follows:
   1.146 -
   1.147 -  \medskip
   1.148 -  \begin{tabular}{lll}
   1.149 -    @{text "tac\<^sub>1"}~@{ML_text THEN}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1, meth\<^sub>2"} \\
   1.150 -    @{text "tac\<^sub>1"}~@{ML_text ORELSE}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1 | meth\<^sub>2"} \\
   1.151 -    @{ML TRY}~@{text tac} & & @{text "meth?"} \\
   1.152 -    @{ML REPEAT1}~@{text tac} & & @{text "meth+"} \\
   1.153 -    @{ML REPEAT}~@{text tac} & & @{text "(meth+)?"} \\
   1.154 -    @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>]"} & & @{text "meth\<^sub>1, \<dots>"} \\
   1.155 -    @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>]"} & & @{text "meth\<^sub>1 | \<dots>"} \\
   1.156 -  \end{tabular}
   1.157 -  \medskip
   1.158 -
   1.159 -  \medskip @{ML CHANGED} (see @{cite "isabelle-implementation"}) is
   1.160 -  usually not required in Isar, since most basic proof methods already
   1.161 -  fail unless there is an actual change in the goal state.
   1.162 -  Nevertheless, ``@{text "?"}''  (try) may be used to accept
   1.163 -  \emph{unchanged} results as well.
   1.164 -
   1.165 -  \medskip @{ML ALLGOALS}, @{ML SOMEGOAL} etc.\ (see
   1.166 -  @{cite "isabelle-implementation"}) are not available in Isar, since
   1.167 -  there is no direct goal addressing.  Nevertheless, some basic
   1.168 -  methods address all goals internally, notably @{method simp_all}
   1.169 -  (see \secref{sec:simplifier}).  Also note that @{ML ALLGOALS} can be
   1.170 -  often replaced by ``@{text "+"}'' (repeat at least once), although
   1.171 -  this usually has a different operational behavior: subgoals are
   1.172 -  solved in a different order.
   1.173 -
   1.174 -  \medskip Iterated resolution, such as
   1.175 -  @{ML_text "REPEAT (FIRSTGOAL (resolve_tac ...))"}, is usually better
   1.176 -  expressed using the @{method intro} and @{method elim} methods of
   1.177 -  Isar (see \secref{sec:classical}).
   1.178 -\<close>
   1.179 -
   1.180 -end
     2.1 --- a/src/Doc/Isar_Ref/document/root.tex	Mon Jul 06 10:56:14 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/document/root.tex	Mon Jul 06 11:14:44 2015 +0200
     2.3 @@ -86,7 +86,6 @@
     2.4  \input{Quick_Reference.tex}
     2.5  \let\int\intorig
     2.6  \input{Symbols.tex}
     2.7 -\input{ML_Tactic.tex}
     2.8  
     2.9  \begingroup
    2.10    \tocentry{\bibname}
     3.1 --- a/src/Doc/ROOT	Mon Jul 06 10:56:14 2015 +0200
     3.2 +++ b/src/Doc/ROOT	Mon Jul 06 11:14:44 2015 +0200
     3.3 @@ -171,7 +171,6 @@
     3.4      HOL_Specific
     3.5      Quick_Reference
     3.6      Symbols
     3.7 -    ML_Tactic
     3.8    document_files (in "..")
     3.9      "prepare_document"
    3.10      "pdfsetup.sty"