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