From eb412dc1fdb43b270ff87f926d0cf8b390084ff1 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sun, 10 Jan 2016 14:00:15 0500
Subject: [PATCH] books/bookvol13 theorem and example from Judson
Goal: Proving Axiom Correct
Theorems related to Euclid's algorithm and reference.

books/bookvol13.pamphlet  104 +++++++++++++++++++++++++++++++++++++++
books/bookvolbib.pamphlet  102 ++++++++++++++++++++++
changelog  3 +
patch  6 +
src/axiomwebsite/patches.html  2 +
5 files changed, 168 insertions(+), 49 deletions()
diff git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index ae81603..a110c03 100644
 a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ 276,7 +276,7 @@ natural language statements may require Coq lemmas.
From WikiProof \cite{Wiki14a} we quote:
Let \[a, b \in \Z\] and $a \ne 0 or b \ne 0$.
+Let \[a, b \in \Z\] and $a \ne 0$ or $b \ne 0$.
The steps of the algorithm are:
\begin{enumerate}
@@ 312,6 +312,108 @@ We quote the {\bf Division Theorem} proof \cite{Wiki14b}:
For every pair of integers $a$, $b$ where $b \ne 0$, there exist unique
integers $q,r$ such that $a = qb + r$ and $0 \le r \le \abs{b}$.
+\section{The Division Algorithm}
+From Judson \cite{Juds15},
+
+An Application of the Principle of WellOrdering that we will use
+often is the division algorithm.
+
+{\bf Theorem 2.9 Division Algorithm} Let $a$ and $b$ be integers, with
+$b > 0$. Then there exists unique integers $q$ and $r$ such that
+\[a=bq+r\]
+where $0 \le r < b$.
+
+{\bf Proof}
+
+Let $a$ and $b$ be integers. If $b = ak$ for some integer $k$, we write
+$a \vert b$. An integer $d$ is called a {\sl common divisor} of $a$ and
+\index{common divisor}
+$b$ if $d \vert a$ and $d \vert b$. The {\sl greatest common divisor}
+\index{greatest common divisor}
+of integers $a$ and $b$ is a positive integer $d$ such that $d$ is
+a common divisor of $a$ and $b$ and if $d^{'}$ is any other common
+divisor of $a$ and $b$, then $d^{'} \vert d$. We write $d=gcd(a,b)$;
+for example, $gcd(24,36)=12$ and $gcd(120,102)=6$. We say that two
+integers $a$ and $b$ are {\sl relatively prime} if $gcd(a,b)=1$.
+\index{relatively prime}
+
+{\bf Theorem 2.10} Let $a$ and $b$ be nonzero integers. Then there
+exist integers $r$ and $s$ such that
+\[gcd(a,b)=ar+bs\]
+Furthermore, the greatest common divisor of $a$ and $b$ is unique.
+
+{\bf Proof}
+
+{\bf Collary 2.11} Let $a$ and $b$ be two integers that are relatively
+prime. Then there exist integers $r$ and $s$ such that
+\[ar+bs=1\]
+
+{\bf The Euclidean Algorithm}
+\index{The Euclidean Algorithm}
+
+Among other things, Theorem 2.10 allows us to compute the greatest
+common divisor of two integers.
+
+{\bf Example 2.1.2} Let us compute the greatest common divisor of 945 and
+2415. First observe that
+\[
+\begin{array}{rcl}
+2415 & = & 945 \cdot 2 + 525\\
+945 & = & 525 \cdot 1 + 420\\
+525 & = & 420 \cdot 1 + 105\\
+420 & = & 105 \cdot 4 + 0\\
+\end{array}
+\]
+
+Reversing our steps, 105 divides 420, 105 divides 525, 105 divides 945,
+and 105 divides 2415. Hence, 105 divides both 945 and 2415. If $d$ were
+another common divisor of 945 and 2415, then $d$ would also have to
+divide 105. Therefore, $gcd(945,2415)=105$.
+
+If we work backward through the above sequence of equations, we can also
+obtain numbers $r$ and $s$ such that
+\[945r + 2415s = 105\]
+
+\[
+\begin{array}{rcl}
+105 & = & 525 + (1)\cdot 420\\
+105 & = & 525 + (1)\cdot [945+(1)\cdot 525]\\
+105 & = & 2\cdot 525+(1)\cdot 945\\
+105 & = & 2\cdot[2415+(2)\cdot 945]+(1)\cdot 945\\
+105 & = & 2*2415+(5)\cdot 945
+\end{array}
+\]
+So $r=5$ and $s2$. Notice the $r$ and $s$ are not unique, since
+$r=41$ and $s=16$ would also work.
+
+To compute $gcd(a,b)=d$, we are using repeated divisions to obtain
+a decreasing sequence of positive integers
+$r_1 > r_2 > \ldots > r_n = d$; that is
+
+\[
+\begin{array}{rcl}
+b & = & aq_1+r_1\\
+a & = & r_1q_2+r_2\\
+r_1 & = & r_2q_3+r_3\\
+\vdots\\
+r_{n2} & = & r_{n1}q_n+r_n\\
+r_{n1} & = & r_nq_{n+1}
+\end{array}
+\]
+
+To find $r$ and $s$ such that $ar+bs=d$, we begin with the last equation
+and substitute results obtained from the previous equations:
+
+\[
+\begin{array}{rcl}
+d & = & r_n\\
+d & = & r_{n2}  r_{n1}q_n\\
+d & = & r_{n2}  q_n(r_{n3}q_{n1}r_{n2}\\
+d & = & q_nr_{n3}+(1+q_nq_{n1})r_{n2}\\
+\vdots\\
+d & = & ra+sb
+\end{array}
+\]
\chapter{Software Details}
\section{Installed Software}
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 32be553..5f5beee 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 22,32 +22,27 @@ paragraph for those unfamiliar with the terms.
\section{Algebra Documentation References}
\index{Sims, Charles}
\begin{chunk}{axiom.bib}
@article{Sims71,
 author = "Sims, Charles",
 title = "Determining the Conjugacy Classes of a Permutation Group",
 journal = "Computers in Algebra and Number Theory, SIAMAMS Proc.",
 volume = "4",
 publisher = "American Math. Soc.",
 year = "1991",
 pages = "191195",
 comment = "documentation for PermutationGroup"

}

\end{chunk}

\index{W\"orzBusekros, A.}
+\index{Gonshor, H.}
\begin{chunk}{axiom.bib}
@article{Worz80,
 author = {W\"orzBusekros, A.},
 title = "Algebra in Genetics",
 publisher = "SpringerVerlag",
 journal = "Lecture Notes in Biomathematics",
 volume = "36",
 year = "1980",
 comment = "documentation for AlgebraGivenByStructuralConstants"
+@article{Gons71,
+ author = "Gonshor, H.",
+ title = "Contributions to Genetic Algebras",
+ journal = "Proc. Edinburgh Mathmatical Society (Series 2)",
+ volume = "17",
+ number = "4",
+ month = "December",
+ year = "1971",
+ issn = "14643839",
+ pages = "289298",
+ doi = "10.1017/S0013091500009548",
+ url = "http://journals.cambridge.org/article_S0013091500009548",
+ comment = "documentation for AlgebraGivenByStructuralConstants",
+ abstract =
+ "Etherington introduced certain algebraic methods into the study of
+ population genetics. It was noted that algebras arising in genetic
+ systems tend to have certain abstract properties and that these can be
+ used to give elegant proofs of some classical stability theorems in
+ population genetics."
}
\end{chunk}
@@ 90,27 +85,32 @@ paragraph for those unfamiliar with the terms.
\end{chunk}
\index{Gonshor, H.}
+\index{Sims, Charles}
\begin{chunk}{axiom.bib}
@article{Gons71,
 author = "Gonshor, H.",
 title = "Contributions to Genetic Algebras",
 journal = "Proc. Edinburgh Mathmatical Society (Series 2)",
 volume = "17",
 number = "4",
 month = "December",
 year = "1971",
 issn = "14643839",
 pages = "289298",
 doi = "10.1017/S0013091500009548",
 url = "http://journals.cambridge.org/article_S0013091500009548",
 comment = "documentation for AlgebraGivenByStructuralConstants",
 abstract =
 "Etherington introduced certain algebraic methods into the study of
 population genetics. It was noted that algebras arising in genetic
 systems tend to have certain abstract properties and that these can be
 used to give elegant proofs of some classical stability theorems in
 population genetics."
+@article{Sims71,
+ author = "Sims, Charles",
+ title = "Determining the Conjugacy Classes of a Permutation Group",
+ journal = "Computers in Algebra and Number Theory, SIAMAMS Proc.",
+ volume = "4",
+ publisher = "American Math. Soc.",
+ year = "1991",
+ pages = "191195",
+ comment = "documentation for PermutationGroup"
+
+}
+
+\end{chunk}
+
+\index{W\"orzBusekros, A.}
+\begin{chunk}{axiom.bib}
+@article{Worz80,
+ author = {W\"orzBusekros, A.},
+ title = "Algebra in Genetics",
+ publisher = "SpringerVerlag",
+ journal = "Lecture Notes in Biomathematics",
+ volume = "36",
+ year = "1980",
+ comment = "documentation for AlgebraGivenByStructuralConstants"
}
\end{chunk}
@@ 7896,6 +7896,18 @@ rational righthand sides etc."
\section{To Be Classified} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Judson, Thomas W.}
+\begin{chunk}{axiom.bib}
+@book{Juds15,
+ author = "Judson, Thomas W.",
+ title = "Abstract Algebra: Theory and Applications",
+ year = "2015",
+ url = "http://abstract.ups.edu/aata/colophon1.html",
+ publisher = "Website"
+}
+
+\end{chunk}
+
\index{Kaltofen, Erich}
\begin{chunk}{axiom.bib}
@InProceedings{Kalt83,
diff git a/changelog b/changelog
index 6be419e..62cb492 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,6 @@
+20160110 tpd src/axiomwebsite/patches.html 20160110.01.tpd.patch
+20160110 tpd books/bookvol13 theorem and example from Judson
+20160110 tpd books/bookvolbib add Juds15
20151230 tpd src/axiomwebsite/patches.html 20151230.01.tpd.patch
20151230 tpd src/interp/functor.lisp merge and rewrite code
20151230 tpd src/interp/gerror.lisp merge and rewrite code
diff git a/patch b/patch
index 6bcd20d..9cb5735 100644
 a/patch
+++ b/patch
@@ 1,5 +1,5 @@
books/bookvol9 merge code, rewrite into common lisp
+books/bookvol13 theorem and example from Judson
Goal: literate interpreter
+Goal: Proving Axiom Correct
Move the lisp support code support sections of the interpreter.
+Theorems related to Euclid's algorithm and reference.
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 180680e..3bc7aa5 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5180,6 +5180,8 @@ books/bookvol5 move more functions from gutil.lisp
src/interp/gutil.lisp merge with bookvol5, bookvol9
20151230.01.tpd.patch
books/bookvol9 merge code, rewrite into common lisp
+20160110.01.tpd.patch
+books/bookvol13 theorem and example from Judson

1.7.5.4