author wenzelm Tue, 20 Nov 2012 14:29:46 +0100 changeset 50130 8c6fde547cba parent 50129 e69db78b36d6 child 50131 921cc694057b
some documentation for "algebra" in HOL;
 src/Doc/IsarRef/HOL_Specific.thy file | annotate | diff | comparison | revisions src/Doc/IsarRef/document/root.tex file | annotate | diff | comparison | revisions src/Doc/manual.bib file | annotate | diff | comparison | revisions
--- a/src/Doc/IsarRef/HOL_Specific.thy	Tue Nov 20 13:27:24 2012 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Tue Nov 20 14:29:46 2012 +0100
@@ -1739,6 +1739,90 @@
*}

+section {* Algebraic reasoning via Gr\"obner bases *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{method_def (HOL) "algebra"} & : & @{text method} \\
+    @{attribute_def (HOL) algebra} & : & @{text attribute} \\
+  \end{matharray}
+
+  @{rail "
+    @@{method (HOL) algebra}
+      ('del' ':' @{syntax thmrefs})?
+    ;
+    @@{attribute (HOL) algebra} (() | 'add' | 'del')
+  "}
+
+  \begin{description}
+
+  \item @{method (HOL) algebra} performs algebraic reasoning via
+  \cite[\S3.2]{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}
+*}
+
+
+subsubsection {* Example *}
+
+text {* The subsequent example is from geometry: collinearity is
+  invariant by rotation.  *}
+
+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\<twosuperior> + s\<twosuperior> = 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)
+
+text {*
+*}
+
+
section {* Coherent Logic *}

text {*
--- a/src/Doc/IsarRef/document/root.tex	Tue Nov 20 13:27:24 2012 +0100
+++ b/src/Doc/IsarRef/document/root.tex	Tue Nov 20 14:29:46 2012 +0100
@@ -29,15 +29,16 @@
Jasmin Blanchette,
Timothy Bourke,
Lukas Bulwahn, \\
+  Amine Chaieb,
Lucas Dixon,
-  Florian Haftmann,
-  Brian Huffman, \\
+  Florian Haftmann, \\
+  Brian Huffman,
Gerwin Klein,
-  Alexander Krauss,
-  Ond\v{r}ej Kun\v{c}ar, \\
+  Alexander Krauss, \\
+  Ond\v{r}ej Kun\v{c}ar,
Tobias Nipkow,
-  Lars Noschinski,
-  David von Oheimb, \\
+  Lars Noschinski, \\
+  David von Oheimb,
Larry Paulson,
Sebastian Skalberg
}
--- a/src/Doc/manual.bib	Tue Nov 20 13:27:24 2012 +0100
+++ b/src/Doc/manual.bib	Tue Nov 20 14:29:46 2012 +0100
@@ -401,6 +401,13 @@

%C

+@PhdThesis{Chaieb-thesis,
+  author =       {Amine Chaieb},
+  title =        {Automated methods for formal proofs in simple arithmetics and algebra},
+  school =       {Technische Universit\"at M\"unchen},
+  year =         2008,
+  note =      {\url{http://www4.in.tum.de/~chaieb/pubs/pdf/diss.pdf}}}
+
@InProceedings{Chaieb-Wenzel:2007,
author = 	 {Amine Chaieb and Makarius Wenzel},
title = 	 {Context aware Calculation and Deduction ---