# HG changeset patch # User wenzelm # Date 1436174084 -7200 # Node ID aabae0331b2f1b864d8935d4df9ae42b060abe8e # Parent 98b64a1deff098665108f77907f31ada42ea51c0 removed outdated and mostly obsolete material; diff -r 98b64a1deff0 -r aabae0331b2f src/Doc/Isar_Ref/ML_Tactic.thy --- a/src/Doc/Isar_Ref/ML_Tactic.thy Mon Jul 06 10:56:14 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,177 +0,0 @@ -theory ML_Tactic -imports Base Main -begin - -chapter \ML tactic expressions\ - -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 Rule_Insts.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_ref (Pure) rule} method, or any of its - ``improper'' variants @{method erule}, @{method drule}, @{method - frule}. 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 "ctxt [a\<^sub>1, \] 1"} & & @{text "rule a\<^sub>1 \"} \\ - @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(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 "ctxt [a\<^sub>1, \] i"} & & @{text "rule_tac [i] a\<^sub>1 \"} \\ - @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(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 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 "@{context} 1"} & & @{method simp} \\ - @{ML ALLGOALS}~(@{ML asm_full_simp_tac}~@{text "@{context}"}) & & @{method simp_all} \\[0.5ex] - @{ML simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm)"} \\ - @{ML asm_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm_simp)"} \\ - @{ML full_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm_use)"} \\ - @{ML asm_lr_simp_tac}~@{text "@{context} 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. 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 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-implementation"}) 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-implementation"}) 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: subgoals are - solved 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 98b64a1deff0 -r aabae0331b2f src/Doc/Isar_Ref/document/root.tex --- a/src/Doc/Isar_Ref/document/root.tex Mon Jul 06 10:56:14 2015 +0200 +++ b/src/Doc/Isar_Ref/document/root.tex Mon Jul 06 11:14:44 2015 +0200 @@ -86,7 +86,6 @@ \input{Quick_Reference.tex} \let\int\intorig \input{Symbols.tex} -\input{ML_Tactic.tex} \begingroup \tocentry{\bibname} diff -r 98b64a1deff0 -r aabae0331b2f src/Doc/ROOT --- a/src/Doc/ROOT Mon Jul 06 10:56:14 2015 +0200 +++ b/src/Doc/ROOT Mon Jul 06 11:14:44 2015 +0200 @@ -171,7 +171,6 @@ HOL_Specific Quick_Reference Symbols - ML_Tactic document_files (in "..") "prepare_document" "pdfsetup.sty"