src/Doc/Isar_Ref/Generic.thy

     @@{command print_options} ('!'?)
     ;
     @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?
   \<close>}
 
-  \begin{description}
-  
   \<^descr> @{command "print_options"} prints the available configuration
   options, with names, types, and current values; the ``@{text "!"}'' option
   indicates extra verbosity.
   
   \<^descr> @{text "name = value"} as an attribute expression modifies the
   named option, with the syntax of the value depending on the option's
   type.  For @{ML_type bool} the default value is @{text true}.  Any
   attempt to change a global option in a local context is ignored.
-
-  \end{description}
 \<close>
 
 
 section \<open>Basic proof tools\<close>
 

     (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
     ;
     @@{method sleep} @{syntax real}
   \<close>}
 
-  \begin{description}
-  
   \<^descr> @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text
   "a\<^sub>1 \<dots> a\<^sub>n"} expand (or fold back) the given definitions throughout
   all goals; any chained facts provided are inserted into the goal and
   subject to rewriting as well.
 

 
   \<^descr> @{method sleep}~@{text s} succeeds after a real-time delay of @{text
   s} seconds. This is occasionally useful for demonstration and testing
   purposes.
 
-  \end{description}
 
   \begin{matharray}{rcl}
     @{attribute_def tagged} & : & @{text attribute} \\
     @{attribute_def untagged} & : & @{text attribute} \\[0.5ex]
     @{attribute_def THEN} & : & @{text attribute} \\

     (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
     ;
     @@{attribute rotated} @{syntax int}?
   \<close>}
 
-  \begin{description}
-
   \<^descr> @{attribute tagged}~@{text "name value"} and @{attribute
   untagged}~@{text name} add and remove \emph{tags} of some theorem.
   Tags may be any list of string pairs that serve as formal comment.
   The first string is considered the tag name, the second its value.
   Note that @{attribute untagged} removes any tags of the same name.

   Note that the Classical Reasoner (\secref{sec:classical}) provides
   its own version of this operation.
 
   \<^descr> @{attribute no_vars} replaces schematic variables by free
   ones; this is mainly for tuning output of pretty printed theorems.
-
-  \end{description}
 \<close>
 
 
 subsection \<open>Low-level equational reasoning\<close>
 

   that are intended for specialized applications only.  Normally,
   single step calculations would be performed in a structured text
   (see also \secref{sec:calculation}), while the Simplifier methods
   provide the canonical way for automated normalization (see
   \secref{sec:simplifier}).
-
-  \begin{description}
 
   \<^descr> @{method subst}~@{text eq} performs a single substitution step
   using rule @{text eq}, which may be either a meta or object
   equality.
 

   structure of the rule.
   
   Note that the @{method simp} method already involves repeated
   application of split rules as declared in the current context, using
   @{attribute split}, for example.
-
-  \end{description}
 \<close>
 
 
 section \<open>The Simplifier \label{sec:simplifier}\<close>
 

     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
     ;
     @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') |
       'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
   \<close>}
-
-  \begin{description}
 
   \<^descr> @{method simp} invokes the Simplifier on the first subgoal,
   after inserting chained facts as additional goal premises; further
   rule declarations may be included via @{text "(simp add: facts)"}.
   The proof method fails if the subgoal remains unchanged after

   simplification.
 
   \<^descr> @{attribute simp_depth_limit} limits the number of recursive
   invocations of the Simplifier during conditional rewriting.
 
-  \end{description}
 
   By default the Simplifier methods above take local assumptions fully
   into account, using equational assumptions in the subsequent
   normalization process, or simplifying assumptions themselves.
   Further options allow to fine-tune the behavior of the Simplifier

       (() | 'add' | 'del')
     ;
     @@{command print_simpset} ('!'?)
   \<close>}
 
-  \begin{description}
-
   \<^descr> @{attribute simp} declares rewrite rules, by adding or
   deleting them from the simpset within the theory or proof context.
   Rewrite rules are theorems expressing some form of equality, for
   example:
 

   The Simplifier accepts the following formats for the @{text "lhs"}
   term:
 
   \begin{enumerate}
 
-  \<^enum> First-order patterns, considering the sublanguage of
-  application of constant operators to variable operands, without
-  @{text "\<lambda>"}-abstractions or functional variables.
-  For example:
-
-  @{text "(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)"} \\
-  @{text "f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)"}
-
-  \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}.
-  These are terms in @{text "\<beta>"}-normal form (this will always be the
-  case unless you have done something strange) where each occurrence
-  of an unknown is of the form @{text "?F x\<^sub>1 \<dots> x\<^sub>n"}, where the
-  @{text "x\<^sub>i"} are distinct bound variables.
-
-  For example, @{text "(\<forall>x. ?P x \<and> ?Q x) \<equiv> (\<forall>x. ?P x) \<and> (\<forall>x. ?Q x)"}
-  or its symmetric form, since the @{text "rhs"} is also a
-  higher-order pattern.
-
-  \<^enum> Physical first-order patterns over raw @{text "\<lambda>"}-term
-  structure without @{text "\<alpha>\<beta>\<eta>"}-equality; abstractions and bound
-  variables are treated like quasi-constant term material.
-
-  For example, the rule @{text "?f ?x \<in> range ?f = True"} rewrites the
-  term @{text "g a \<in> range g"} to @{text "True"}, but will fail to
-  match @{text "g (h b) \<in> range (\<lambda>x. g (h x))"}. However, offending
-  subterms (in our case @{text "?f ?x"}, which is not a pattern) can
-  be replaced by adding new variables and conditions like this: @{text
-  "?y = ?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is acceptable as a conditional
-  rewrite rule of the second category since conditions can be
-  arbitrary terms.
+    \item First-order patterns, considering the sublanguage of
+    application of constant operators to variable operands, without
+    @{text "\<lambda>"}-abstractions or functional variables.
+    For example:
+
+    @{text "(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)"} \\
+    @{text "f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)"}
+
+    \item Higher-order patterns in the sense of @{cite "nipkow-patterns"}.
+    These are terms in @{text "\<beta>"}-normal form (this will always be the
+    case unless you have done something strange) where each occurrence
+    of an unknown is of the form @{text "?F x\<^sub>1 \<dots> x\<^sub>n"}, where the
+    @{text "x\<^sub>i"} are distinct bound variables.
+
+    For example, @{text "(\<forall>x. ?P x \<and> ?Q x) \<equiv> (\<forall>x. ?P x) \<and> (\<forall>x. ?Q x)"}
+    or its symmetric form, since the @{text "rhs"} is also a
+    higher-order pattern.
+
+    \item Physical first-order patterns over raw @{text "\<lambda>"}-term
+    structure without @{text "\<alpha>\<beta>\<eta>"}-equality; abstractions and bound
+    variables are treated like quasi-constant term material.
+
+    For example, the rule @{text "?f ?x \<in> range ?f = True"} rewrites the
+    term @{text "g a \<in> range g"} to @{text "True"}, but will fail to
+    match @{text "g (h b) \<in> range (\<lambda>x. g (h x))"}. However, offending
+    subterms (in our case @{text "?f ?x"}, which is not a pattern) can
+    be replaced by adding new variables and conditions like this: @{text
+    "?y = ?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is acceptable as a conditional
+    rewrite rule of the second category since conditions can be
+    arbitrary terms.
 
   \end{enumerate}
 
   \<^descr> @{attribute split} declares case split rules.
 

   other tools that might get invoked internally (e.g.\ simplification
   procedures \secref{sec:simproc}).  A mismatch of the context of the
   simpset and the context of the problem being simplified may lead to
   unexpected results.
 
-  \end{description}
 
   The implicit simpset of the theory context is propagated
   monotonically through the theory hierarchy: forming a new theory,
   the union of the simpsets of its imports are taken as starting
   point.  Also note that definitional packages like @{command

 text \<open>Ordered rewriting is particularly effective in the case of
   associative-commutative operators.  (Associativity by itself is not
   permutative.)  When dealing with an AC-operator @{text "f"}, keep
   the following points in mind:
 
-  \begin{itemize}
-
   \<^item> The associative law must always be oriented from left to
   right, namely @{text "f (f x y) z = f x (f y z)"}.  The opposite
   orientation, if used with commutativity, leads to looping in
   conjunction with the standard term order.
 
   \<^item> To complete your set of rewrite rules, you must add not just
   associativity (A) and commutativity (C) but also a derived rule
   \emph{left-commutativity} (LC): @{text "f x (f y z) = f y (f x z)"}.
 
-  \end{itemize}
 
   Ordered rewriting with the combination of A, C, and LC sorts a term
   lexicographically --- the rewriting engine imitates bubble-sort.
 \<close>
 

   \<close>}
 
   These attributes and configurations options control various aspects of
   Simplifier tracing and debugging.
 
-  \begin{description}
-
   \<^descr> @{attribute simp_trace} makes the Simplifier output internal
   operations.  This includes rewrite steps, but also bookkeeping like
   modifications of the simpset.
 
   \<^descr> @{attribute simp_trace_depth_limit} limits the effect of

   \<^descr> @{attribute simp_break} declares term or theorem breakpoints for
   @{attribute simp_trace_new} as described above. Term breakpoints are
   patterns which are checked for matches on the redex of a rule application.
   Theorem breakpoints trigger when the corresponding theorem is applied in a
   rewrite step. For example:
-
-  \end{description}
 \<close>
 
 (*<*)experiment begin(*>*)
 declare conjI [simp_break]
 declare [[simp_break "?x \<and> ?y"]]

       @{syntax text} \<newline> (@'identifier' (@{syntax nameref}+))?
     ;
 
     @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
   \<close>}
-
-  \begin{description}
 
   \<^descr> @{command "simproc_setup"} defines a named simplification
   procedure that is invoked by the Simplifier whenever any of the
   given term patterns match the current redex.  The implementation,
   which is provided as ML source text, needs to be of type @{ML_type

 
   \<^descr> @{text "simproc add: name"} and @{text "simproc del: name"}
   add or delete named simprocs to the current Simplifier context.  The
   default is to add a simproc.  Note that @{command "simproc_setup"}
   already adds the new simproc to the subsequent context.
-
-  \end{description}
 \<close>
 
 
 subsubsection \<open>Example\<close>
 

   be simplification itself.  In rare situations, this strategy may
   need to be changed.  For example, if the premise of a conditional
   rule is an instance of its conclusion, as in @{text "Suc ?m < ?n \<Longrightarrow>
   ?m < ?n"}, the default strategy could loop.  % FIXME !??
 
-  \begin{description}
-
   \<^descr> @{ML Simplifier.set_subgoaler}~@{text "tac ctxt"} sets the
   subgoaler of the context to @{text "tac"}.  The tactic will
   be applied to the context of the running Simplifier instance.
 
   \<^descr> @{ML Simplifier.prems_of}~@{text "ctxt"} retrieves the current
   set of premises from the context.  This may be non-empty only if
   the Simplifier has been told to utilize local assumptions in the
   first place (cf.\ the options in \secref{sec:simp-meth}).
 
-  \end{description}
 
   As an example, consider the following alternative subgoaler:
 \<close>
 
 ML_val \<open>

   still apply the ordinary unsafe one in nested simplifications for
   conditional rules or congruences. Note that in this way the overall
   tactic is not totally safe: it may instantiate unknowns that appear
   also in other subgoals.
 
-  \begin{description}
-
   \<^descr> @{ML Simplifier.mk_solver}~@{text "name tac"} turns @{text
   "tac"} into a solver; the @{text "name"} is only attached as a
   comment and has no further significance.
 
   \<^descr> @{text "ctxt setSSolver solver"} installs @{text "solver"} as

 
   \<^descr> @{text "ctxt addSolver solver"} adds @{text "solver"} as an
   additional unsafe solver; it will be tried after the solvers which
   had already been present in @{text "ctxt"}.
 
-  \end{description}
 
   \<^medskip>
   The solver tactic is invoked with the context of the
   running Simplifier.  Further operations
   may be used to retrieve relevant information, such as the list of

 
   A typical looper is \emph{case splitting}: the expansion of a
   conditional.  Another possibility is to apply an elimination rule on
   the assumptions.  More adventurous loopers could start an induction.
 
-  \begin{description}
-
   \<^descr> @{text "ctxt setloop tac"} installs @{text "tac"} as the only
   looper tactic of @{text "ctxt"}.
 
   \<^descr> @{text "ctxt addloop (name, tac)"} adds @{text "tac"} as an
   additional looper tactic with name @{text "name"}, which is

 
   \<^descr> @{ML Splitter.del_split}~@{text "thm ctxt"} deletes the split
   tactic corresponding to @{text thm} from the looper tactics of
   @{text "ctxt"}.
 
-  \end{description}
 
   The splitter replaces applications of a given function; the
   right-hand side of the replacement can be anything.  For example,
   here is a splitting rule for conditional expressions:
 

     ;
 
     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
   \<close>}
 
-  \begin{description}
-  
   \<^descr> @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to
   be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,
   a\<^sub>n"}, or the implicit Simplifier context if no arguments are given.
   The result is fully simplified by default, including assumptions and
   conclusion; the options @{text no_asm} etc.\ tune the Simplifier in

   Note that forward simplification restricts the Simplifier to its
   most basic operation of term rewriting; solver and looper tactics
   (\secref{sec:simp-strategies}) are \emph{not} involved here.  The
   @{attribute simplified} attribute should be only rarely required
   under normal circumstances.
-
-  \end{description}
 \<close>
 
 
 section \<open>The Classical Reasoner \label{sec:classical}\<close>
 

     @@{attribute rule} 'del'
     ;
     @@{attribute iff} (((() | 'add') '?'?) | 'del')
   \<close>}
 
-  \begin{description}
-
   \<^descr> @{command "print_claset"} prints the collection of rules
   declared to the Classical Reasoner, i.e.\ the @{ML_type claset}
   within the context.
 
   \<^descr> @{attribute intro}, @{attribute elim}, and @{attribute dest}

   \<^descr> @{attribute swapped} turns an introduction rule into an
   elimination, by resolving with the classical swap principle @{text
   "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position.  This is mainly for
   illustrative purposes: the Classical Reasoner already swaps rules
   internally as explained above.
-
-  \end{description}
 \<close>
 
 
 subsection \<open>Structured methods\<close>
 

 
   @{rail \<open>
     @@{method rule} @{syntax thmrefs}?
   \<close>}
 
-  \begin{description}
-
   \<^descr> @{method rule} as offered by the Classical Reasoner is a
   refinement over the Pure one (see \secref{sec:pure-meth-att}).  Both
   versions work the same, but the classical version observes the
   classical rule context in addition to that of Isabelle/Pure.
 

 
   \<^descr> @{method contradiction} solves some goal by contradiction,
   deriving any result from both @{text "\<not> A"} and @{text A}.  Chained
   facts, which are guaranteed to participate, may appear in either
   order.
-
-  \end{description}
 \<close>
 
 
 subsection \<open>Fully automated methods\<close>
 

       ('cong' | 'split') (() | 'add' | 'del') |
       'iff' (((() | 'add') '?'?) | 'del') |
       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
   \<close>}
 
-  \begin{description}
-
   \<^descr> @{method blast} is a separate classical tableau prover that
   uses the same classical rule declarations as explained before.
 
   Proof search is coded directly in ML using special data structures.
   A successful proof is then reconstructed using regular Isabelle
   inferences.  It is faster and more powerful than the other classical
   reasoning tools, but has major limitations too.
 
   \begin{itemize}
 
-  \<^item> It does not use the classical wrapper tacticals, such as the
-  integration with the Simplifier of @{method fastforce}.
-
-  \<^item> It does not perform higher-order unification, as needed by the
-  rule @{thm [source=false] rangeI} in HOL.  There are often
-  alternatives to such rules, for example @{thm [source=false]
-  range_eqI}.
-
-  \<^item> Function variables may only be applied to parameters of the
-  subgoal.  (This restriction arises because the prover does not use
-  higher-order unification.)  If other function variables are present
-  then the prover will fail with the message
-  @{verbatim [display] \<open>Function unknown's argument not a bound variable\<close>}
-
-  \<^item> Its proof strategy is more general than @{method fast} but can
-  be slower.  If @{method blast} fails or seems to be running forever,
-  try @{method fast} and the other proof tools described below.
+    \item It does not use the classical wrapper tacticals, such as the
+    integration with the Simplifier of @{method fastforce}.
+
+    \item It does not perform higher-order unification, as needed by the
+    rule @{thm [source=false] rangeI} in HOL.  There are often
+    alternatives to such rules, for example @{thm [source=false]
+    range_eqI}.
+
+    \item Function variables may only be applied to parameters of the
+    subgoal.  (This restriction arises because the prover does not use
+    higher-order unification.)  If other function variables are present
+    then the prover will fail with the message
+    @{verbatim [display] \<open>Function unknown's argument not a bound variable\<close>}
+
+    \item Its proof strategy is more general than @{method fast} but can
+    be slower.  If @{method blast} fails or seems to be running forever,
+    try @{method fast} and the other proof tools described below.
 
   \end{itemize}
 
   The optional integer argument specifies a bound for the number of
   unsafe steps used in a proof.  By default, @{method blast} starts

   to preserve the formula they act on, so that it be used repeatedly.
   This method can prove more goals than @{method fast}, but is much
   slower, for example if the assumptions have many universal
   quantifiers.
 
-  \end{description}
 
   Any of the above methods support additional modifiers of the context
   of classical (and simplifier) rules, but the ones related to the
   Simplifier are explicitly prefixed by @{text simp} here.  The
   semantics of these ad-hoc rule declarations is analogous to the

     (@@{method safe} | @@{method clarify}) (@{syntax clamod} * )
     ;
     @@{method clarsimp} (@{syntax clasimpmod} * )
   \<close>}
 
-  \begin{description}
-
   \<^descr> @{method safe} repeatedly performs safe steps on all subgoals.
   It is deterministic, with at most one outcome.
 
   \<^descr> @{method clarify} performs a series of safe steps without
   splitting subgoals; see also @{method clarify_step}.
 
   \<^descr> @{method clarsimp} acts like @{method clarify}, but also does
   simplification.  Note that if the Simplifier context includes a
   splitter for the premises, the subgoal may still be split.
-
-  \end{description}
 \<close>
 
 
 subsection \<open>Single-step tactics\<close>
 

 
   These are the primitive tactics behind the automated proof methods
   of the Classical Reasoner.  By calling them yourself, you can
   execute these procedures one step at a time.
 
-  \begin{description}
-
   \<^descr> @{method safe_step} performs a safe step on the first subgoal.
   The safe wrapper tacticals are applied to a tactic that may include
   proof by assumption or Modus Ponens (taking care not to instantiate
   unknowns), or substitution.
 

   subgoal; no splitting step is applied.  For example, the subgoal
   @{text "A \<and> B"} is left as a conjunction.  Proof by assumption,
   Modus Ponens, etc., may be performed provided they do not
   instantiate unknowns.  Assumptions of the form @{text "x = t"} may
   be eliminated.  The safe wrapper tactical is applied.
-
-  \end{description}
 \<close>
 
 
 subsection \<open>Modifying the search step\<close>
 

   modification of the step tactics. Safe and unsafe wrappers are added
   to the context with the functions given below, supplying them with
   wrapper names.  These names may be used to selectively delete
   wrappers.
 
-  \begin{description}
-
   \<^descr> @{text "ctxt addSWrapper (name, wrapper)"} adds a new wrapper,
   which should yield a safe tactic, to modify the existing safe step
   tactic.
 
   \<^descr> @{text "ctxt addSbefore (name, tac)"} adds the given tactic as a

   rather safe way, after each safe step of the search.
 
   \<^descr> @{text "addss"} adds the simpset of the context to its
   classical set. The assumptions and goal will be simplified, before
   the each unsafe step of the search.
-
-  \end{description}
 \<close>
 
 
 section \<open>Object-logic setup \label{sec:object-logic}\<close>
 

     @@{attribute atomize} ('(' 'full' ')')?
     ;
     @@{attribute rule_format} ('(' 'noasm' ')')?
   \<close>}
 
-  \begin{description}
-  
   \<^descr> @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant
   @{text c} as the truth judgment of the current object-logic.  Its
   type @{text \<sigma>} should specify a coercion of the category of
   object-level propositions to @{text prop} of the Pure meta-logic;
   the mixfix annotation @{text "(mx)"} would typically just link the

 
   In common object-logics (HOL, FOL, ZF), the effect of @{attribute
   rule_format} is to replace (bounded) universal quantification
   (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding
   rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.
-
-  \end{description}
 \<close>
 
 
 section \<open>Tracing higher-order unification\<close>
 

 
   Higher-order unification works well in most practical situations,
   but sometimes needs extra care to identify problems.  These tracing
   options may help.
 
-  \begin{description}
-
   \<^descr> @{attribute unify_trace_simp} controls tracing of the
   simplification phase of higher-order unification.
 
   \<^descr> @{attribute unify_trace_types} controls warnings of
   incompleteness, when unification is not considering all possible

   unification cannot return an infinite sequence, though it can return
   an exponentially long one.  The search rarely approaches the default
   value in practice.  If the search is cut off, unification prints a
   warning ``Unification bound exceeded''.
 
-  \end{description}
 
   \begin{warn}
   Options for unification cannot be modified in a local context.  Only
   the global theory content is taken into account.
   \end{warn}