This repository contains the Isabelle proofs accompanying the paper 'ON CORRECTNESS OF DIGITWIZE ARITHMETIC'. To explore the proofs, download and install the 2019 version of Isabelle.
The CompArithDefs.thy file contains the basic definitions, like the digitwise addition/subtraction algorithm.
CompArith.thy contains the major results of the paper. The names of the proofs in this file follow ther naming convention of the paper.