# HG changeset patch
# User wenzelm
# Date 1436206061 -7200
# Node ID 91d36d6a6a88c05ed97e4f0fb33a0747554acd49
# Parent  ac02ff182f46822c75cd28d6c0e6a432bd27a535
clarified sections;

diff -r ac02ff182f46 -r 91d36d6a6a88 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 06 20:05:17 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 06 20:07:41 2015 +0200
@@ -1776,256 +1776,6 @@
 
 chapter \<open>Proof tools\<close>
 
-section \<open>Coercive subtyping\<close>
-
-text \<open>
-  \begin{matharray}{rcl}
-    @{attribute_def (HOL) coercion} & : & @{text attribute} \\
-    @{attribute_def (HOL) coercion_enabled} & : & @{text attribute} \\
-    @{attribute_def (HOL) coercion_map} & : & @{text attribute} \\
-  \end{matharray}
-
-  Coercive subtyping allows the user to omit explicit type
-  conversions, also called \emph{coercions}.  Type inference will add
-  them as necessary when parsing a term. See
-  @{cite "traytel-berghofer-nipkow-2011"} for details.
-
-  @{rail \<open>
-    @@{attribute (HOL) coercion} (@{syntax term})?
-    ;
-    @@{attribute (HOL) coercion_map} (@{syntax term})?
-  \<close>}
-
-  \begin{description}
-
-  \item @{attribute (HOL) "coercion"}~@{text "f"} registers a new
-  coercion function @{text "f :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2"} where @{text "\<sigma>\<^sub>1"} and
-  @{text "\<sigma>\<^sub>2"} are type constructors without arguments.  Coercions are
-  composed by the inference algorithm if needed.  Note that the type
-  inference algorithm is complete only if the registered coercions
-  form a lattice.
-
-  \item @{attribute (HOL) "coercion_map"}~@{text "map"} registers a
-  new map function to lift coercions through type constructors. The
-  function @{text "map"} must conform to the following type pattern
-
-  \begin{matharray}{lll}
-    @{text "map"} & @{text "::"} &
-      @{text "f\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> f\<^sub>n \<Rightarrow> (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Rightarrow> (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t"} \\
-  \end{matharray}
-
-  where @{text "t"} is a type constructor and @{text "f\<^sub>i"} is of type
-  @{text "\<alpha>\<^sub>i \<Rightarrow> \<beta>\<^sub>i"} or @{text "\<beta>\<^sub>i \<Rightarrow> \<alpha>\<^sub>i"}.  Registering a map function
-  overwrites any existing map function for this particular type
-  constructor.
-
-  \item @{attribute (HOL) "coercion_enabled"} enables the coercion
-  inference algorithm.
-
-  \end{description}
-\<close>
-
-
-section \<open>Arithmetic proof support\<close>
-
-text \<open>
-  \begin{matharray}{rcl}
-    @{method_def (HOL) arith} & : & @{text method} \\
-    @{attribute_def (HOL) arith} & : & @{text attribute} \\
-    @{attribute_def (HOL) arith_split} & : & @{text attribute} \\
-  \end{matharray}
-
-  \begin{description}
-
-  \item @{method (HOL) arith} decides linear arithmetic problems (on
-  types @{text nat}, @{text int}, @{text real}).  Any current facts
-  are inserted into the goal before running the procedure.
-
-  \item @{attribute (HOL) arith} declares facts that are supplied to
-  the arithmetic provers implicitly.
-
-  \item @{attribute (HOL) arith_split} attribute declares case split
-  rules to be expanded before @{method (HOL) arith} is invoked.
-
-  \end{description}
-
-  Note that a simpler (but faster) arithmetic prover is already
-  invoked by the Simplifier.
-\<close>
-
-
-section \<open>Intuitionistic proof search\<close>
-
-text \<open>
-  \begin{matharray}{rcl}
-    @{method_def (HOL) iprover} & : & @{text method} \\
-  \end{matharray}
-
-  @{rail \<open>
-    @@{method (HOL) iprover} (@{syntax rulemod} *)
-  \<close>}
-
-  \begin{description}
-
-  \item @{method (HOL) iprover} performs intuitionistic proof search,
-  depending on specifically declared rules from the context, or given
-  as explicit arguments.  Chained facts are inserted into the goal
-  before commencing proof search.
-
-  Rules need to be classified as @{attribute (Pure) intro},
-  @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
-  ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
-  applied aggressively (without considering back-tracking later).
-  Rules declared with ``@{text "?"}'' are ignored in proof search (the
-  single-step @{method (Pure) rule} method still observes these).  An
-  explicit weight annotation may be given as well; otherwise the
-  number of rule premises will be taken into account here.
-
-  \end{description}
-\<close>
-
-
-section \<open>Model Elimination and Resolution\<close>
-
-text \<open>
-  \begin{matharray}{rcl}
-    @{method_def (HOL) "meson"} & : & @{text method} \\
-    @{method_def (HOL) "metis"} & : & @{text method} \\
-  \end{matharray}
-
-  @{rail \<open>
-    @@{method (HOL) meson} @{syntax thmrefs}?
-    ;
-    @@{method (HOL) metis}
-      ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?
-      @{syntax thmrefs}?
-  \<close>}
-
-  \begin{description}
-
-  \item @{method (HOL) meson} implements Loveland's model elimination
-  procedure @{cite "loveland-78"}.  See @{file
-  "~~/src/HOL/ex/Meson_Test.thy"} for examples.
-
-  \item @{method (HOL) metis} combines ordered resolution and ordered
-  paramodulation to find first-order (or mildly higher-order) proofs.
-  The first optional argument specifies a type encoding; see the
-  Sledgehammer manual @{cite "isabelle-sledgehammer"} for details.  The
-  directory @{file "~~/src/HOL/Metis_Examples"} contains several small
-  theories developed to a large extent using @{method (HOL) metis}.
-
-  \end{description}
-\<close>
-
-
-section \<open>Algebraic reasoning via Gr\"obner bases\<close>
-
-text \<open>
-  \begin{matharray}{rcl}
-    @{method_def (HOL) "algebra"} & : & @{text method} \\
-    @{attribute_def (HOL) algebra} & : & @{text attribute} \\
-  \end{matharray}
-
-  @{rail \<open>
-    @@{method (HOL) algebra}
-      ('add' ':' @{syntax thmrefs})?
-      ('del' ':' @{syntax thmrefs})?
-    ;
-    @@{attribute (HOL) algebra} (() | 'add' | 'del')
-  \<close>}
-
-  \begin{description}
-
-  \item @{method (HOL) algebra} performs algebraic reasoning via
-  Gr\"obner bases, see also @{cite "Chaieb-Wenzel:2007"} and
-  @{cite \<open>\S3.2\<close> "Chaieb-thesis"}. The method handles deals with two main
-  classes of problems:
-
-  \begin{enumerate}
-
-  \item Universal problems over multivariate polynomials in a
-  (semi)-ring/field/idom; the capabilities of the method are augmented
-  according to properties of these structures. For this problem class
-  the method is only complete for algebraically closed fields, since
-  the underlying method is based on Hilbert's Nullstellensatz, where
-  the equivalence only holds for algebraically closed fields.
-
-  The problems can contain equations @{text "p = 0"} or inequations
-  @{text "q \<noteq> 0"} anywhere within a universal problem statement.
-
-  \item All-exists problems of the following restricted (but useful)
-  form:
-
-  @{text [display] "\<forall>x\<^sub>1 \<dots> x\<^sub>n.
-    e\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<and> \<dots> \<and> e\<^sub>m(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<longrightarrow>
-    (\<exists>y\<^sub>1 \<dots> y\<^sub>k.
-      p\<^sub>1\<^sub>1(x\<^sub>1, \<dots> ,x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>1\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0 \<and>
-      \<dots> \<and>
-      p\<^sub>t\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>t\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0)"}
-
-  Here @{text "e\<^sub>1, \<dots>, e\<^sub>n"} and the @{text "p\<^sub>i\<^sub>j"} are multivariate
-  polynomials only in the variables mentioned as arguments.
-
-  \end{enumerate}
-
-  The proof method is preceded by a simplification step, which may be
-  modified by using the form @{text "(algebra add: ths\<^sub>1 del: ths\<^sub>2)"}.
-  This acts like declarations for the Simplifier
-  (\secref{sec:simplifier}) on a private simpset for this tool.
-
-  \item @{attribute algebra} (as attribute) manages the default
-  collection of pre-simplification rules of the above proof method.
-
-  \end{description}
-\<close>
-
-
-subsubsection \<open>Example\<close>
-
-text \<open>The subsequent example is from geometry: collinearity is
-  invariant by rotation.\<close>
-
-(*<*)experiment begin(*>*)
-type_synonym point = "int \<times> int"
-
-fun collinear :: "point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
-  "collinear (Ax, Ay) (Bx, By) (Cx, Cy) \<longleftrightarrow>
-    (Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx)"
-
-lemma collinear_inv_rotation:
-  assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1"
-  shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
-    (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
-  using assms by (algebra add: collinear.simps)
-(*<*)end(*>*)
-
-text \<open>
- See also @{file "~~/src/HOL/ex/Groebner_Examples.thy"}.
-\<close>
-
-
-section \<open>Coherent Logic\<close>
-
-text \<open>
-  \begin{matharray}{rcl}
-    @{method_def (HOL) "coherent"} & : & @{text method} \\
-  \end{matharray}
-
-  @{rail \<open>
-    @@{method (HOL) coherent} @{syntax thmrefs}?
-  \<close>}
-
-  \begin{description}
-
-  \item @{method (HOL) coherent} solves problems of \emph{Coherent
-  Logic} @{cite "Bezem-Coquand:2005"}, which covers applications in
-  confluence theory, lattice theory and projective geometry.  See
-  @{file "~~/src/HOL/ex/Coherent.thy"} for some examples.
-
-  \end{description}
-\<close>
-
-
 section \<open>Proving propositions\<close>
 
 text \<open>
@@ -2318,6 +2068,256 @@
 \<close>
 
 
+section \<open>Coercive subtyping\<close>
+
+text \<open>
+  \begin{matharray}{rcl}
+    @{attribute_def (HOL) coercion} & : & @{text attribute} \\
+    @{attribute_def (HOL) coercion_enabled} & : & @{text attribute} \\
+    @{attribute_def (HOL) coercion_map} & : & @{text attribute} \\
+  \end{matharray}
+
+  Coercive subtyping allows the user to omit explicit type
+  conversions, also called \emph{coercions}.  Type inference will add
+  them as necessary when parsing a term. See
+  @{cite "traytel-berghofer-nipkow-2011"} for details.
+
+  @{rail \<open>
+    @@{attribute (HOL) coercion} (@{syntax term})?
+    ;
+    @@{attribute (HOL) coercion_map} (@{syntax term})?
+  \<close>}
+
+  \begin{description}
+
+  \item @{attribute (HOL) "coercion"}~@{text "f"} registers a new
+  coercion function @{text "f :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2"} where @{text "\<sigma>\<^sub>1"} and
+  @{text "\<sigma>\<^sub>2"} are type constructors without arguments.  Coercions are
+  composed by the inference algorithm if needed.  Note that the type
+  inference algorithm is complete only if the registered coercions
+  form a lattice.
+
+  \item @{attribute (HOL) "coercion_map"}~@{text "map"} registers a
+  new map function to lift coercions through type constructors. The
+  function @{text "map"} must conform to the following type pattern
+
+  \begin{matharray}{lll}
+    @{text "map"} & @{text "::"} &
+      @{text "f\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> f\<^sub>n \<Rightarrow> (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Rightarrow> (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t"} \\
+  \end{matharray}
+
+  where @{text "t"} is a type constructor and @{text "f\<^sub>i"} is of type
+  @{text "\<alpha>\<^sub>i \<Rightarrow> \<beta>\<^sub>i"} or @{text "\<beta>\<^sub>i \<Rightarrow> \<alpha>\<^sub>i"}.  Registering a map function
+  overwrites any existing map function for this particular type
+  constructor.
+
+  \item @{attribute (HOL) "coercion_enabled"} enables the coercion
+  inference algorithm.
+
+  \end{description}
+\<close>
+
+
+section \<open>Arithmetic proof support\<close>
+
+text \<open>
+  \begin{matharray}{rcl}
+    @{method_def (HOL) arith} & : & @{text method} \\
+    @{attribute_def (HOL) arith} & : & @{text attribute} \\
+    @{attribute_def (HOL) arith_split} & : & @{text attribute} \\
+  \end{matharray}
+
+  \begin{description}
+
+  \item @{method (HOL) arith} decides linear arithmetic problems (on
+  types @{text nat}, @{text int}, @{text real}).  Any current facts
+  are inserted into the goal before running the procedure.
+
+  \item @{attribute (HOL) arith} declares facts that are supplied to
+  the arithmetic provers implicitly.
+
+  \item @{attribute (HOL) arith_split} attribute declares case split
+  rules to be expanded before @{method (HOL) arith} is invoked.
+
+  \end{description}
+
+  Note that a simpler (but faster) arithmetic prover is already
+  invoked by the Simplifier.
+\<close>
+
+
+section \<open>Intuitionistic proof search\<close>
+
+text \<open>
+  \begin{matharray}{rcl}
+    @{method_def (HOL) iprover} & : & @{text method} \\
+  \end{matharray}
+
+  @{rail \<open>
+    @@{method (HOL) iprover} (@{syntax rulemod} *)
+  \<close>}
+
+  \begin{description}
+
+  \item @{method (HOL) iprover} performs intuitionistic proof search,
+  depending on specifically declared rules from the context, or given
+  as explicit arguments.  Chained facts are inserted into the goal
+  before commencing proof search.
+
+  Rules need to be classified as @{attribute (Pure) intro},
+  @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
+  ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
+  applied aggressively (without considering back-tracking later).
+  Rules declared with ``@{text "?"}'' are ignored in proof search (the
+  single-step @{method (Pure) rule} method still observes these).  An
+  explicit weight annotation may be given as well; otherwise the
+  number of rule premises will be taken into account here.
+
+  \end{description}
+\<close>
+
+
+section \<open>Model Elimination and Resolution\<close>
+
+text \<open>
+  \begin{matharray}{rcl}
+    @{method_def (HOL) "meson"} & : & @{text method} \\
+    @{method_def (HOL) "metis"} & : & @{text method} \\
+  \end{matharray}
+
+  @{rail \<open>
+    @@{method (HOL) meson} @{syntax thmrefs}?
+    ;
+    @@{method (HOL) metis}
+      ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?
+      @{syntax thmrefs}?
+  \<close>}
+
+  \begin{description}
+
+  \item @{method (HOL) meson} implements Loveland's model elimination
+  procedure @{cite "loveland-78"}.  See @{file
+  "~~/src/HOL/ex/Meson_Test.thy"} for examples.
+
+  \item @{method (HOL) metis} combines ordered resolution and ordered
+  paramodulation to find first-order (or mildly higher-order) proofs.
+  The first optional argument specifies a type encoding; see the
+  Sledgehammer manual @{cite "isabelle-sledgehammer"} for details.  The
+  directory @{file "~~/src/HOL/Metis_Examples"} contains several small
+  theories developed to a large extent using @{method (HOL) metis}.
+
+  \end{description}
+\<close>
+
+
+section \<open>Algebraic reasoning via Gr\"obner bases\<close>
+
+text \<open>
+  \begin{matharray}{rcl}
+    @{method_def (HOL) "algebra"} & : & @{text method} \\
+    @{attribute_def (HOL) algebra} & : & @{text attribute} \\
+  \end{matharray}
+
+  @{rail \<open>
+    @@{method (HOL) algebra}
+      ('add' ':' @{syntax thmrefs})?
+      ('del' ':' @{syntax thmrefs})?
+    ;
+    @@{attribute (HOL) algebra} (() | 'add' | 'del')
+  \<close>}
+
+  \begin{description}
+
+  \item @{method (HOL) algebra} performs algebraic reasoning via
+  Gr\"obner bases, see also @{cite "Chaieb-Wenzel:2007"} and
+  @{cite \<open>\S3.2\<close> "Chaieb-thesis"}. The method handles deals with two main
+  classes of problems:
+
+  \begin{enumerate}
+
+  \item Universal problems over multivariate polynomials in a
+  (semi)-ring/field/idom; the capabilities of the method are augmented
+  according to properties of these structures. For this problem class
+  the method is only complete for algebraically closed fields, since
+  the underlying method is based on Hilbert's Nullstellensatz, where
+  the equivalence only holds for algebraically closed fields.
+
+  The problems can contain equations @{text "p = 0"} or inequations
+  @{text "q \<noteq> 0"} anywhere within a universal problem statement.
+
+  \item All-exists problems of the following restricted (but useful)
+  form:
+
+  @{text [display] "\<forall>x\<^sub>1 \<dots> x\<^sub>n.
+    e\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<and> \<dots> \<and> e\<^sub>m(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<longrightarrow>
+    (\<exists>y\<^sub>1 \<dots> y\<^sub>k.
+      p\<^sub>1\<^sub>1(x\<^sub>1, \<dots> ,x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>1\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0 \<and>
+      \<dots> \<and>
+      p\<^sub>t\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>t\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0)"}
+
+  Here @{text "e\<^sub>1, \<dots>, e\<^sub>n"} and the @{text "p\<^sub>i\<^sub>j"} are multivariate
+  polynomials only in the variables mentioned as arguments.
+
+  \end{enumerate}
+
+  The proof method is preceded by a simplification step, which may be
+  modified by using the form @{text "(algebra add: ths\<^sub>1 del: ths\<^sub>2)"}.
+  This acts like declarations for the Simplifier
+  (\secref{sec:simplifier}) on a private simpset for this tool.
+
+  \item @{attribute algebra} (as attribute) manages the default
+  collection of pre-simplification rules of the above proof method.
+
+  \end{description}
+\<close>
+
+
+subsubsection \<open>Example\<close>
+
+text \<open>The subsequent example is from geometry: collinearity is
+  invariant by rotation.\<close>
+
+(*<*)experiment begin(*>*)
+type_synonym point = "int \<times> int"
+
+fun collinear :: "point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
+  "collinear (Ax, Ay) (Bx, By) (Cx, Cy) \<longleftrightarrow>
+    (Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx)"
+
+lemma collinear_inv_rotation:
+  assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1"
+  shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
+    (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
+  using assms by (algebra add: collinear.simps)
+(*<*)end(*>*)
+
+text \<open>
+ See also @{file "~~/src/HOL/ex/Groebner_Examples.thy"}.
+\<close>
+
+
+section \<open>Coherent Logic\<close>
+
+text \<open>
+  \begin{matharray}{rcl}
+    @{method_def (HOL) "coherent"} & : & @{text method} \\
+  \end{matharray}
+
+  @{rail \<open>
+    @@{method (HOL) coherent} @{syntax thmrefs}?
+  \<close>}
+
+  \begin{description}
+
+  \item @{method (HOL) coherent} solves problems of \emph{Coherent
+  Logic} @{cite "Bezem-Coquand:2005"}, which covers applications in
+  confluence theory, lattice theory and projective geometry.  See
+  @{file "~~/src/HOL/ex/Coherent.thy"} for some examples.
+
+  \end{description}
+\<close>
+
+
 section \<open>Unstructured case analysis and induction \label{sec:hol-induct-tac}\<close>
 
 text \<open>