General Rules

Linting

  • Lines must not be longer than 100 symbols (as indicated by the blue line in jEdit).
  • Files should not be longer than 1500 lines. While this not a hard limit, exceeding this size limit should be seen as an opportunity to evaluate whether it can be sensibly split up.
  • Punctuation (e.g. , or .) is followed by a space. Use spaces around infix operators and between binders (quantifiers, lambdas). If a line has to be broken it is often sensible to put the linebreaks around operators. For a specific operator, it is up to you whether to put it at the end of the line or the beginning of the new line but you should apply your choice consistently.
  • Use two spaces to indent. You can use an extra indent when a long line forces a break to suggest the break is artificial rather than structural.
  • Use one blank line to separate top-level declarations such as theorems, definitions, datatype declarations, etc. You can group together several closely related top-level declarations by omitting the blank line. You may put two blank lines around contexts that are delimited by begin and end.

“Do Nots”

  • Do not use indexed access to dynamic fact collections, e.g. algebra_simps(8) or derivative_intros(3).
  • In procedural proofs, try to not apply tactics in the middle of a proof if they do not close a goal and do not give raise to a normal form.

Comments

For comments that are not considered part of the literal document, e.g. TODO notes, use ML-style comments (* ... *). Comment delimiters ― ‹...› are to be used for short inline comments, for example to clarify a proof step. For broader comments, like motiviations for definitions, use the text command. See also Theory Documentation.

Theorems and Definitions

The preferred method of stating assumptions is by using explicit assumes clauses; however, this is just a suggestion. You are free to state your assumptions using meta level implication if it reduces textual noise or simplifies the proof body.

If you use assumes, the theorem name must always be followed by a linebreak. Furthermore, the show must be on a separate line from the assumptions. You can put multiple short assumptions in one line at a time. Facts should be labelled with semantically meaningful names. If the fact is short enough, however, fact quoting should be preferred instead. Here is a valid example:

theorem C_if_complicated_B_if_A:
    assumes A and complicated_if_A: "A ⟹  complicated B"
    and c_if_complicated: "complicated B ⟹ C"
    shows C
      using ‹A› oops

If you prove involved existential statements or case distinctions you should write down the theorem using obtains, e.g:

theorem empty_or_infinite_if_card_eq_0:
  assumes "card A = 0"
  obtains (empty) "A = {}" | (infinite) B where "B ⊆ A" "¬ finite B"
    oops

Proofs

The proof, next, and qed commands are flushed to the left with respect to the current indentation block.

theorem nat_add_comm: "(n :: nat) + m = m + n"
proof (induction n)
  case 0
  then show ?case sorry
next
  case (Suc n)
  then show ?case sorry
qed

A from / have / using / unfolding / by combination can be put on the same line. If you need more than two lines, then from and have should be aligned while the using / unfolding / by commands are aligned to one extra indentation with respect to the have block. If you have to break within one of the blocks, add another extra indentation.

When arguments themselves are long enough to require line breaks, use an additional indent for the new lines.

Here is an example:

lemma pigeonhole_if_infinite_domain:
  assumes inf_domain: "infinite A"
  and finite_range: "finite (f`A)"
  shows "∃ a ∈ A. infinite {a' ∈ A. f a' = f a}"
using finite_range inf_domain
proof (induction "f`A" arbitrary: A rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert b F)
  ― ‹the pre-image of b›
  let ?Pb = "{a ∈ A. f a = b}"
  show ?case
  proof (cases "finite ?Pb")
    case True
    with ‹infinite A› have "infinite (A - ?Pb)"
      by simp
    moreover have "A - ?Pb = {a ∈ A. f a ≠ b}"
      by blast
    ultimately have "infinite {a ∈ A. f a ≠ b}"
      by simp
    from insert.IH[OF _ this] insert.hyps
    show ?thesis
      using rev_finite_subset
      by blast 
  next
    case False
    then have "?Pb ≠ {}" 
      by force
    with False show ?thesis
      by blast
  qed
qed

Facts that are crucial to the understanding of a step should be put in the from clause of a step. Auxiliary facts can be put in the trailing using block or passed as tactic arguments.

Calculations

Use calculation proofs when doing transitive reasoning. The transitive operator, = in the following example, must not be manually aligned:

lemma "((a::nat) + b) + c = c + (b + a)"
proof -
  have "(a + b) + c = (b + a) + c"  by simp
  also have "… = c + (b + a)" by simp
  finally show ?thesis by simp
qed

Datatype and function definitions

While each equation of a function definition must be on a separate line, a datatype declaration may be put on a single line if it is short enough. The separating | between several equations is either consistently put at the beginning of the line without indentation or at the end of the line. In case of the former, separate the constructor respectively equation by one space to obtain the usual indentation of two spaces. The where command for a definition should be on the same line as the declaration, or, if this is not possible, it goes onto the next line with an extra indentation. If the right-hand side of an equation has to be broken because it is too long, then it is shifted by one indentation plus one space (to account for the ") to the right. Linebreaks within the right-hand side recursively add one indentation.

Example:

datatype 'a list =
  Nil |
  Cons 'a "'a list"

function list_update :: "'a list ⇒ nat ⇒ 'a ⇒ 'a list" where
"list_update [] i v = []" |
"list_update (x # xs) i v = (
   case i of
     0 ⇒ v # xs |
     Suc j ⇒ x # list_update xs j v
   )"

or alternatively:

datatype 'a list =
  Nil
| Cons 'a "'a list"

function list_update :: "'a list ⇒ nat ⇒ 'a ⇒ 'a list" where
  "list_update [] i v = []"
| "list_update (x # xs) i v = (
     case i of
       0 ⇒ v # xs
     | Suc j ⇒ x # list_update xs j v
     )"

Locales

The imports of a locale go on the same line as the locale declaration, or, if the line has to be broken, they are indented by one level. Here, the +s that separate the imports always are at the end of the line. The fixes, defines, and assumes of a locale are indented by one level as well. The initial begin must always be followed by a blank line and end must be preceded by a blank line. Here are two examples:

locale ex1 = import1 + import2 +
  fixes a b :: 'a
  fixes A :: "'a rel"
  assumes "sym A"
  assumes "(a, b) ∈ A"
begin

lemma "(b, a) ∈ A"
  oops

end
 

locale ex2 =
  import1 +
  this_is_a_very_long_import +
  fixes a :: 'a
begin

lemma "a ∈ UNIV"
  oops

end