# Theory Documentation

Documentation is key for the long-term value of a development. Without documentation, once a project loses its original maintainer(s), the project virtually dies due to inaccessibility. In general, all comments must be written using Isabelle markdown (see Isabelle reference manual).

## References

Every project comes with a `.bib`

containing the references that were used when developing the theories.
This file should be placed in the folder `document`

.
Those references are then inserted at the appropriate places when documenting the theories (using the antiquation `@cite`

).

## Header Documentation

Every file starts with:

- a comment declaring the author(s) of the file if there is more than one person working on the project
- the list of imports
- a file comment containing the general documentation
in this order.
Original authors should mark themselves with the
`✐‹creator ...›`

tag. Additional (later) contributors should use the`✐‹contributor ...›`

tag.

The file comment consists of the following sections:

- the title of the file followed by a summary of the content of the file
- main definitions (optional; can be covered in the summary)
- main theorems (optional; can be covered in the summary)
- notations (if notation is introduced)
- fact collections and bundles (if relevant fact collections or bundles are introduced)
- implementation notes (optional; description of important design decisions or interface features, including use of type classes and simp canonical form for new definitions)
- references (references to textbooks, papers, or Wikipedia pages)
- tags (a list of keywords that could be useful for search)

The following is an example of a file header:

```
✐‹creator "Kevin Kappelmann"›
✐‹contributor "Simon Wimmer"›
chapter ‹Continued Fractions›
theory Scratch
imports HOL.Archimedean_Field "HOL-Library.Stream"
begin
paragraph ‹Summary›
text ‹We define generalised, simple, and regular continued fractions and
functions to evaluate their convergents. We follow the naming conventions from
@{cite wikicontinuedfractions} and @{cite wall2018analytic}.›
paragraph ‹Main Definitions›
text ‹
▪ Generalised continued fractions (gcfs)
▪ Simple continued fractions (scfs)
▪ (Regular) continued fractions ((r)cfs)
▪ Computation of convergents using the recurrence relation in
@{const convergents}.
▪ Computation of convergents by directly evaluating the fraction described by
the gcf in @{const convergents'}.
›
paragraph ‹Notations›
text ‹
▪ @{term "⌊x⌋"} is the floor for any ‹x› of an integral domain.
›
paragraph ‹Fact Collections›
text ‹
▪ ‹gcf_simps› contains simplification rules for gcfs
›
paragraph ‹Implementation Notes›
text ‹
▪ The most commonly used kind of continued fractions in the literature are
regular continued fractions. We hence just call them @{const continued_fractions}
in the library.
▪ We use streams from @{theory "HOL-Library.Stream"} to encode infinite sequences.
›
paragraph ‹Tags›
text ‹numerics, number theory, approximations, fractions›
```

## Theory-Body Documentation and Sectioning

Every theory should result in a human-readable file. For this, we document and section theories. Regarding the former, all definitions and major theorems are accompanied by a text block (or comment).

- For definitions, the block should convey the mathematical meaning and motivation. For clarity, minor technicalities need not be mentioned (e.g. divisions by zero)
- For major theorems, the block should address the importance and re-usability of the theorem.
- When referring to constants (
`@const`

), terms (`@term`

), types (`@typ`

), theorems (`@thm`

) etc., antiquotations must be used. In particular, for constants,`@const`

must be preferred over`@term`

.

Moreover, the theory should be sectioned using the `chapter`

, `section`

, `subsection`

, `paragraph`

, etc. commands.
If a new section starts at the start of a theory, the corresponding sectioning command should go before the theory header.
Explanatory text that motivates and guides the user through the theory development should be added.

Example:

```
paragraph ‹Generalised Continued Fractions›
text ‹
A ∗‹generalised continued fraction› (gcf) is a potentially infinite expression
of the form
\begin{equation*}
h+\cfrac{a_0}
{b_0+\cfrac{a_1}
{b_1+\cfrac{a_2}
{b_2+\cfrac{a_3}
{b_3+\dotsb}}}}
\end{equation*}
›
(* Above code produces:
a₀
h + ---------------------------
a₁
b₀ + --------------------
a₂
b₁ + --------------
a₃
b₂ + --------
b₃ + ...
*)
text ‹where ‹h› is called the ∗‹head term› or ∗‹integer part›, the ‹a⇘is⇙› are
called the ∗‹partial numerators› and the ‹b⇘is⇙› the ∗‹partial denominators› of the
gcf. We store the sequence of partial numerators and denominators in a sequence
of @{term generalized_continued_fraction_pairs} ‹s›.
For convenience, one often writes ‹[h; (a⇩0, b⇩0), (a⇩1, b⇩1), (a⇩2, b⇩2), …]›.
›
definition "generalised_continued_fraction ≡ ..."
```