Companion to Concrete Semantics

Concrete Semantics (PDF download, hardcopy, mirrored PDF) is a book that teaches the Isabelle proof assistant by having the user implement a simple imperative language. Unfortunately, the disjoint code snippets set in fancy typography don't make it easy to turn it into running code. While the entire code for the book is included in the Isabelle installation, going back and forth between the book and the source can be a bit tedious. This post aims to make it all clearer.

Introduction
Copyright notice
Before you begin
1. Installation
2. Structure of the tutorial
Implementation
1. Arithmetic expressions

Copyright notice

The code is copied and rearranged from the Isabelle distribution, as such, it's covered by the following license:


ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.

Copyright (c) 1986-2024,
  University of Cambridge,
  Technische Universitaet Muenchen,
  and contributors.

  All rights reserved.

Redistribution and use in source and binary forms, with or without 
modification, are permitted provided that the following conditions are 
met:

* Redistributions of source code must retain the above copyright 
notice, this list of conditions and the following disclaimer.

* Redistributions in binary form must reproduce the above copyright 
notice, this list of conditions and the following disclaimer in the 
documentation and/or other materials provided with the distribution.

* Neither the name of the University of Cambridge or the Technische
Universitaet Muenchen nor the names of their contributors may be used
to endorse or promote products derived from this software without
specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS 
IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED 
TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A 
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT 
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT 
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, 
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY 
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE 
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Before you begin

Installation

To install Isabelle on a Linux-based system, first download the installation archive. Unpack it to a location such as $HOME/inst/ and then put in your shell config file (like .bashrc) the following:

export PATH=$HOME/inst/Isabelle2023/bin/:$PATH
export ISABELLE_HOME=$HOME/inst/Isabelle2023

Reload your shell, and you shall be able to run isabelle jedit to spawn the editor window.

Structure of the tutorial

I assume you're following along with the book, and have an editor open that can load and verify Isabelle. You can also take a look into the code from $ISABELLE_HOME/src/HOL/IMP, though this shouldn't be strictly necessary. Each section ends with a downloadable file containing a full theorem that can be loaded into Isabelle. The theorems are renamed, as Isabelle expects the theorem name to match the name of the file. Files in the main progression are named in ImpTutorial_$NUMBER.thy fashion, files that contain code that is not used in the final program have extra letters after the number. Snippets that do not contain a theorem definiton are expected to be appended to the previous theorem before the end, The code is presented both with pretty typesetting and using raw input values for special symbols. Tthe latter available by clicking the foldable section under formatted code, and can be copied into an editor as is. You might need to reload the editor after pasting the code, so the symbols are rendered properly. Colors are used to mark keywords, definitions, constructors, variables, and symbol inputs.

Insert symbols into your code by typing \symbol name. You might need to wait for a second while the editor searches for the symbol. All the symbols available for use in Isabelle code are listed in $ISABELLE_HOME/etc/symbols. Highlights:

\<Rightarrow> (⇒) for function definitions
\<^sub> for subscripts

Implementation

Arithmetic expressions

Definitions and basic evaluation

Page 28 in the book, chapter 3. Case Study: IMP Expressions. Code from $ISABELLE_HOME/src/HOL/IMP/AExp.thy

Listing 1: arithmetic expressions

theory ImpTutorial 
  imports Main
begin

type_synonym vname = string
type_synonym val = int
type_synonym state = "vname ⇒ val"

datatype aexp = 
  N int | 
  V vname | 
  Plus aexp aexp |

fun aval :: "aexp ⇒ state ⇒ val" where
  "aval (N n) s = n" |
  "aval (V x) s = s x" |
  "aval (Plus a₁ a₂) s = aval a₁ s + aval a₂ s"

end

Click to see unformatted code

theory ImpTutorial
  imports Main
begin
  
type_synonym vname = string
type_synonym val = int
type_synonym state = "vname \<Rightarrow> val"

datatype aexp = 
  N int | 
  V vname | 
  Plus aexp aexp |

fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
  "aval (N n) s = n" |
  "aval (V x) s = s x" |
  "aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"
   
end

Code at the end of this section: ImpTutorial_0.thy

First attempt at constant folding

Listing 2: constant folding function

fun asimp_const :: "aexp ⇒ aexp" where
  "asimp_const (N n) = N n" |
  "asimp_const (V x) = V x" |
  "asimp_const (Plus a₁ a₂) =
  (case (asimp_const a₁, asimp_const a₂) of
    (N n₁, N n₂) ⇒ N (n₁ + n₂) |
    (b₁, b₂) ⇒ Plus b₁ b₂)"

Click to see unformatted code

fun asimp_const :: "aexp \<Rightarrow> aexp" where
  "asimp_const (N n) = N n" |
  "asimp_const (V x) = V x" |
  "asimp_const (Plus a\<^sub>1 a\<^sub>2) =
  (case (asimp_const a\<^sub>1, asimp_const a\<^sub>2) of
    (N n\<^sub>1, N n\<^sub>2) \<Rightarrow> N (n\<^sub>1 + n\<^sub>2) |
    (b\<^sub>1, b\<^sub>2) \<Rightarrow> Plus b\<^sub>1 b\<^sub>2)"

Numbers (N) and unevaluated variables (V) cannot be simplified. Addition (Plus) can only be simplified if both arguments evaluate to numbers, in which case it evaluates to a number that is the sum of the arguments.

A correct constant folding function doesn't change the meaning of the program. We need to prove that any given arithmetic expression evaluated to the same value under the same state, whether or not constant folding has been applied. This statement is written like this in Isabelle (I'm using this notation for consitency and it's not meant to be copied into an editor, so I'm not providing unformatted versions):

lemma "aval (asimp_const a) s = aval a s"

This alone will not work, as it's missing the proof.

Manual proof by induction

If we were to prove this manually, we'd start from considering each case. For a = N n the statement becomes:

aval (asimp_const (N n)) s = aval (N n) s

From listing 2, line 2 know that

asimp_const (N n) = N n

Thus the statment we want to prove becomes

aval (N n) s = aval (N n) s

which is obviously true, no need to dig deeper into the definition of aval. Since asimp_const is defined in the same way for the variable constructor V v, the proof goes the same way.

What's left to prove is the case a = Plus a₁ a₂ and thus

aval (asimp_const (Plus a₁ a₂)) s = aval (Plus a₁ a₂) s

We'll prove it by induction on asimp_const. Assume

aval (asimp_const a₁) s = aval a₁ s

and

aval (asimp_const a₂) s = aval a₂ s

There are now two options. Either both asimp_const a₁ = N n₁ and asimp_const a₂ = N n₂, or at least one doesn't. In the first case, the induction assumptions become

aval (N n₁) s = aval a₁ s

and

aval (N n₂) s = aval a₂ s

From the definition of asimp_const (listing 2, lines 4-5)

asimp_const (Plus (N n₁) (N n₂)) = N (n₁ + n₂)

thus the formula to prove becomes

aval (N (n₁ + n₂)) s = aval (Plus a₁ a₂) s

From the definition of aval (listing 1, line 15) we see that the left hand side evaluates to just n₁ + n₂.

n₁ + n₂ = aval (Plus a₁ a₂) s

Again from the definition of aval (listing 1, line 17), we can expand the right hand side

n₁ + n₂ = aval a₁ s + aval a₂ s

Using the assumptions we have

n₁ + n₂ = aval (N n₁) s + aval (N n₂) s

which is true for any n₁ and n₂.

Now for the case where asimp_const a₁ ≠ N n₁ and/or asimp_const a₂ ≠ N n₂,

asimp_const (Plus a₁ a₂) = Plus (asimp_const a₁) (asimp_const a₂)

lemma "aval (asimp_const a) s = aval a s"
  apply(induction a)
  apply (auto split: aexp.split)
done

Code at the end of this section: ImpTutorial_0a.thy

After exercises.

theory ImpTutorial
    imports Main
  begin
  
  type_synonym vname = string
  type_synonym val = int
  type_synonym state = "vname \<Rightarrow> val"

  datatype aexp = 
    N int | 
    V vname | 
    Plus aexp aexp |
    Times aexp aexp

  fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
    "aval (N n) s = n" |
    "aval (V x) s = s x" |
    "aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"
    "aval (Times a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s * aval a\<^sub>2 s"
   
end

Code at the end of this section: ImpTutorial_1.thy

Evaluation


  fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
    "plus (N i\<^sub>1) (N i\<^sub>2) = N (i\<^sub>1 + i\<^sub>2)" |
    "plus (N i) a = (if i=0 then a else Plus (N i) a)" |
    "plus a (N i) = (if i=0 then a else Plus a (N i))" |
    "plus a\<^sub>1 a\<^sub>2 = Plus a\<^sub>1 a\<^sub>2"
  
  fun asimp :: "aexp \ aexp" where
    "asimp (N n) = N n" |
    "asimp (V x) = V x" |
    "asimp (Plus a\<^sub>1 a\<^sub>2) = plus (asimp a\<^sub>1) (asimp a\<^sub>2)"
  
  lemma aval_plus[simp]:
    "aval (plus a1 a2) s = aval a1 s + aval a2 s"
  apply(induction a1 a2 rule: plus.induct)
  apply simp_all (* just for a change from auto *)
  done
  
  theorem aval_asimp[simp]:
    "aval (asimp a) s = aval a s"
  apply(induction a)
  apply simp_all
    done
  end

fun asimp_const :: "aexp \<Rightarrow> aexp" where
    "asimp_const (N n) = N n" |
    "asimp_const (V x) = V x" |
    "asimp_const (Plus a\<^sub>1 a\<^sub>2) = 
      (case (asimp_const a\<^sub>1, asimp_const a\<^sub>2) of
        (N n\<^sub>1, N n\<^sub>2) \<Rightarrow> N (n\<^sub>1 + n\<^sub>2) |
        (b\<^sub>1, b\<^sub>2) \<Rightarrow> Plus b\<^sub>1 b\<^sub>2)"