The Isabelle logo as end-of-proof symbol

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


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 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?