In a recent research paper, I formalised some of my theorems in the proof assistantÂ Isabelle, but left some of them as just proved 'by hand'. I found it helpful to use a different 'QED' symbol depending on which method I had used. Below is an enlarged version of the 'three cubes' symbol in the snippet… Continue reading The Isabelle logo as end-of-proof symbol

# Category: Mathematics

## A star operator for functions

If $latex f$ and $latex g$ are functions, what does $latex f*g$ mean? Definition 1. A separation algebra (citation) is a triple $latex (M, \circ, u)$, where $latex M$ is a set, $latex \circ$ has type $latex M \times M \rightharpoonup M$ and is commutative, associative and cancellative, and $latex u\in M$ is the unit… Continue reading A star operator for functions

## A comment on ‘Abstract Separation Logic’

Abstract Separation Logic (citation) is based on a partial composition operator, $latex \circ$, which has the following type: $latex \circ : \Sigma \times \Sigma \rightharpoonup \Sigma$ We shall concentrate henceforth on the simplest incarnation of this operator: disjoint union. Here are two useful theorems about disjoint union. Theorem 1. If $latex a\subseteq a'$ and $latex… Continue reading A comment on ‘Abstract Separation Logic’

## A little theorem about odd powers

Here's an interesting little theorem I came across in number theory. By instantiating $latex n$, one can generate an unlimited of exercises for maths students! Theorem. When two numbers are raised to the same odd power, the sum is divisible by the sum of the two numbers; that is: $latex a+b\mid a^{2n+1}+b^{2n+1}$ for any natural… Continue reading A little theorem about odd powers

## A proof environment for LaTeX

The johnproof style file provides an environment for typesetting proofs. Features include: It automatically handles page breaks, for those occasions when a long proof splits over multiple pages. It deals with assumptions and case splits. It assigns a label to each step in the proof, for referencing. It indicates the scope of each assumption using… Continue reading A proof environment for LaTeX

## A new notation for building sets?

We write $latex \forall x\in\mathbb{R}\ldotp x^2 \ge 0$ to express that the square of any real number is non-negative. We write $latex \exists x\in\mathbb{Z} \ldotp x \ge 0 \land x \le 0$ to express that there exists an integer that is both non-negative and non-positive. We write $latex \lambda x:\mathsf{int} \ldotp x+1$ to denote the… Continue reading A new notation for building sets?