# HG changeset patch # User wenzelm # Date 1514571472 -3600 # Node ID ba52a058942f89e7182db243bdc89d08e639367a # Parent fee3ed06a281cc16b2b9bb2ab00e84570afb6b1e prefer formal citations; more accurate bibtex entries; diff -r fee3ed06a281 -r ba52a058942f src/Doc/Codegen/Computations.thy --- a/src/Doc/Codegen/Computations.thy Fri Dec 29 18:09:38 2017 +0100 +++ b/src/Doc/Codegen/Computations.thy Fri Dec 29 19:17:52 2017 +0100 @@ -263,7 +263,7 @@ text \ Computations are a device to implement fast proof procedures. Then results of a computation are often assumed to be trustable - and thus wrapped in oracles (see \cite{isabelle-isar-ref}), + and thus wrapped in oracles (see @{cite "isabelle-isar-ref"}), as in the following example:\footnote{ The technical details how numerals are dealt with are given later in \secref{sec:literal_input}.} @@ -294,7 +294,7 @@ text \ \<^item> Antiquotation @{ML_antiquotation computation_conv} basically yields a conversion of type @{ML_type "Proof.context -> cterm -> thm"} - (see further \cite{isabelle-implementation}). + (see further @{cite "isabelle-implementation"}). \<^item> The antiquotation expects one functional argument to bridge the \qt{untrusted gap}; this can be done e.g.~using an oracle. Since that oracle diff -r fee3ed06a281 -r ba52a058942f src/Doc/Prog_Prove/Isar.thy --- a/src/Doc/Prog_Prove/Isar.thy Fri Dec 29 18:09:38 2017 +0100 +++ b/src/Doc/Prog_Prove/Isar.thy Fri Dec 29 19:17:52 2017 +0100 @@ -505,7 +505,7 @@ Therefore the \isakeyword{also} hidden in \isakeyword{finally} sets \calculation\ to \t\<^sub>1 < t\<^sub>4\ and the final ``\texttt{.}'' succeeds. -For more information on this style of proof see \cite{BauerW-TPHOLs01}. +For more information on this style of proof see @{cite "BauerW-TPHOLs01"}. \fi \section{Streamlining Proofs} diff -r fee3ed06a281 -r ba52a058942f src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy --- a/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Fri Dec 29 18:09:38 2017 +0100 +++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Fri Dec 29 19:17:52 2017 +0100 @@ -28,8 +28,8 @@ instantiating type-classes, adding relationships between locales (@{command sublocale}) and type-classes (@{command subclass}). Handy introductions are the - respective tutorials \cite{isabelle-locale} - \cite{isabelle-classes}. + respective tutorials @{cite "isabelle-locale"} + @{cite "isabelle-classes"}. \ subsection \Strengths and restrictions of type classes\ @@ -48,7 +48,7 @@ to the numerical type on the right hand side. How to accomplish this given the quite restrictive type system - of {Isabelle/HOL}? Paulson \cite{paulson-numerical} explains + of {Isabelle/HOL}? Paulson @{cite "paulson-numerical"} explains that each numerical type has some characteristic properties which define an characteristic algebraic structure; @{text \} then corresponds to specialization of the corresponding @@ -122,7 +122,7 @@ optionally showing the logical content for each class also. Optional parameters restrict the graph to a particular segment which is useful to get a graspable view. See - the Isar reference manual \cite{isabelle-isar-ref} for details. + the Isar reference manual @{cite "isabelle-isar-ref"} for details. \ @@ -144,7 +144,7 @@ \<^item> @{command class} @{class one} with @{term [source] "1::'a::one"} \noindent Before the introduction of the @{command class} statement in - Isabelle \cite{Haftmann-Wenzel:2006:classes} it was impossible + Isabelle @{cite "Haftmann-Wenzel:2006:classes"} it was impossible to define operations with associated axioms in the same class, hence there were always pairs of syntactic and logical type classes. This restriction is lifted nowadays, but there are diff -r fee3ed06a281 -r ba52a058942f src/HOL/Algebra/Multiplicative_Group.thy --- a/src/HOL/Algebra/Multiplicative_Group.thy Fri Dec 29 18:09:38 2017 +0100 +++ b/src/HOL/Algebra/Multiplicative_Group.thy Fri Dec 29 19:17:52 2017 +0100 @@ -724,7 +724,7 @@ text \ In this section we show that the multiplicative group of a finite field is generated by a single element, i.e. it is cyclic. The proof is inspired - by the first proof given in the survey~\cite{conrad-cyclicity}. + by the first proof given in the survey~@{cite "conrad-cyclicity"}. \ lemma (in group) pow_order_eq_1: diff -r fee3ed06a281 -r ba52a058942f src/HOL/Algebra/document/root.bib --- a/src/HOL/Algebra/document/root.bib Fri Dec 29 18:09:38 2017 +0100 +++ b/src/HOL/Algebra/document/root.bib Fri Dec 29 19:17:52 2017 +0100 @@ -7,6 +7,13 @@ note = {Also Computer Laboratory Technical Report number 473.} } +@Misc{conrad-cyclicity, + author = {Keith Conrad}, + title = {CYCLICITY OF {$(Z/(p))^x$}}, + howpublished = {Expository paper from the author's website}, + note = {\url{http://www.math.uconn.edu/~kconrad/blurbs/grouptheory/cyclicFp.pdf}}, +} + @Book{Jacobson:1985, author = {Nathan Jacobson}, title = {Basic Algebra I}, @@ -20,6 +27,6 @@ Abstract Algebra with {Isabelle HOL}}, journal = {J. Automated Reasoning}, year = 1999, - number = 23, + volume = 23, pages = {235--264} } diff -r fee3ed06a281 -r ba52a058942f src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Fri Dec 29 18:09:38 2017 +0100 +++ b/src/HOL/Binomial.thy Fri Dec 29 19:17:52 2017 +0100 @@ -708,7 +708,7 @@ using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric]) -text \The absorption identity (equation 5.5 \cite[p.~157]{GKP}): +text \The absorption identity (equation 5.5 @{cite \p.~157\ GKP_CM}): \[ {r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0. \]\ @@ -718,7 +718,7 @@ text \The absorption identity is written in the following form to avoid division by $k$ (the lower index) and therefore remove the $k \neq 0$ -restriction\cite[p.~157]{GKP}: +restriction @{cite \p.~157\ GKP_CM}: \[ k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k. \]\ @@ -730,7 +730,7 @@ by (cases n) (simp_all add: binomial_eq_0 Suc_times_binomial del: binomial_Suc_Suc mult_Suc) text \The absorption companion identity for natural number coefficients, - following the proof by GKP \cite[p.~157]{GKP}:\ + following the proof by GKP @{cite \p.~157\ GKP_CM}:\ lemma binomial_absorb_comp: "(n - k) * (n choose k) = n * ((n - 1) choose k)" (is "?lhs = ?rhs") proof (cases "n \ k") @@ -761,7 +761,7 @@ by (subst choose_reduce_nat) simp_all text \ - Equation 5.9 of the reference material \cite[p.~159]{GKP} is a useful + Equation 5.9 of the reference material @{cite \p.~159\ GKP_CM} is a useful summation formula, operating on both indices: \[ \sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n}, @@ -783,7 +783,7 @@ subsubsection \Summation on the upper index\ text \ - Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP}, + Another summation formula is equation 5.10 of the reference material @{cite \p.~160\ GKP_CM}, aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} = {n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\] \ diff -r fee3ed06a281 -r ba52a058942f src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Dec 29 18:09:38 2017 +0100 +++ b/src/HOL/HOL.thy Fri Dec 29 19:17:52 2017 +0100 @@ -56,7 +56,7 @@ subsection \Primitive logic\ text \ -The definition of the logic is based on Mike Gordon's technical report \cite{Gordon-TR68} that +The definition of the logic is based on Mike Gordon's technical report @{cite "Gordon-TR68"} that describes the first implementation of HOL. However, there are a number of differences. In particular, we start with the definite description operator and introduce Hilbert's \\\ operator only much later. Moreover, axiom \(P \ Q) \ (Q \ P) \ (P = Q)\ is derived from the other diff -r fee3ed06a281 -r ba52a058942f src/HOL/document/root.bib --- a/src/HOL/document/root.bib Fri Dec 29 18:09:38 2017 +0100 +++ b/src/HOL/document/root.bib Fri Dec 29 19:17:52 2017 +0100 @@ -12,6 +12,16 @@ year = 1992 } +@book{GKP_CM, + author = {Graham, Ronald L. and Knuth, Donald E. and Patashnik, Oren}, + title = {Concrete Mathematics: A Foundation for Computer Science}, + year = {1994}, + isbn = {0201558025}, + edition = {2nd}, + publisher = {Addison--Wesley}, + address = {Boston, MA, USA}, +} + @techreport{Gordon-TR68, author = "Mike Gordon", title = "{HOL}: {A} Machine Oriented Formulation of Higher-Order Logic",