---
orphan: true
---

### 8.3.2 First Example

For the first example, the goal will be to implement addition via a function called "add". The general form should be:

```isabelle
fun add :: "nat ⇒ nat ⇒ nat" where
    "base case"
    "recursive case"
```

where two natural numbers are added, and the result is a natural number that is the sum of the two input numbers. For example, `sum m n` should return the sum of m and n.

We first want to start off by defining the base case.
Basically, if we add some arbitrary number n by 0, then it should return n.

```isabelle
"add 0 n = n"
```

#### General Proof Structure for a Proof by Induction

Isabelle provides a general structure for how to approach and construct your proof. For this exercise, we will be using a proof by induction; first by proving a base case, and then by proving the sucessor case by using the induction hypothesis.

We start the proof by adding the command `proof(induction m)` after the `lemma` command. When we examine the output of this, we find that Isabelle actually provides us with the overall goal, subgoals (such as the base case and successor cases), and the general proof outline

For example, for the associative property lemma, we get this:
```isabelle
goal (2 subgoals):
 1. add (add 0 n) p = add 0 (add n p)
 2. ⋀m. add (add m n) p = add m (add n p) ⟹ add (add (Suc m) n) p = add (Suc m) (add n p) 
Proof outline with cases:
  case 0
  then show ?case sorry
next
  case (Suc m)
  then show ?case sorry
qed
```


### 8.3.3 First Exercise

For the first exercise, we will be proving the associative and commutative properties of a custom `add` function in Isabelle. This exercise comes from Exercise 2.2 of [Concrete Semantics Exercises](http://www.concrete-semantics.org/Exercises/exercises.pdf)
<!-- i need to change this to a footnote or something that links to references at the end -->

The custom add function is defined here:
```isabelle
fun add :: "nat ⇒ nat ⇒ nat" where
    "add 0 n = n" |
    "add (Suc m) n = Suc(add m n)"
```

We use 2 lemmas to prove each part of the exercise, namely:
```isabelle
lemma add_assoc: "add (add m n) p = add m (add n p)"
lemma add_comm: "add m n = add n m"
```

<!-- We first start off by proving the associative property: -->
(associative-property-proof)=
#### Associative Property Proof

We first start off by proving the associative property of addition, and we do this by declaring the lemma and its goal:
```isabelle
lemma add_assoc: "add (add m n) p = add m (add n p)"
```
We then add the type of proof, which in this case will be a simple induction proof via the `proof` command:
```isabelle
proof (induction m) 
```
We then set the base case with:
```isabelle
  case 0
```
which will set `m = 0` as the base case, and then will update the goal to:
`add (add 0 n) p = add 0 (add n p)`

We then use:
```isabelle
  show ?case by simp
```

in order to simplify that new goal to:
`add n p = add n p`

Next, we perform the inductive step in order to prove that if the associative property holds for m, it must also hold for it's successor of  `Suc m`

We introduce the inductive step:
```isabelle
next
  case (Suc m)
```

This creates 2 things:
  - A goal of: `add (add (Suc m) n) p = add (Suc m) (add n p)`
  -	An induction hypothesis (Suc.IH) that assumes the property holds for m:
    `add (add m n) p = add m (add n p)`

<!-- We then use the recursive definition of add to expand both sides of the equation, and apply the induction hypothesis to simplify the inner equality. This shows that the associative property also holds for the successor case: -->
```isabelle
  show ?case by (simp add: Suc.IH)
```

Here, simp first expands both sides of the equation using the recursive definition
`add (Suc m) n = Suc (add m n)`
This reduces the goal to
`Suc (add (add m n) p) = Suc (add m (add n p))`
The induction hypothesis (Suc.IH) is then applied to replace
`add (add m n) p` with `add m (add n p)`,
making both sides identical.
The expression simplifies to Suc (...) = Suc (...) and completes the inductive step.

The full lemma proof for associativity is here:
```isabelle
lemma add_assoc: "add (add m n) p = add m (add n p)"
proof (induction m) 
  case 0
  show ?case by simp
next
  case (Suc m)
  show ?case by (simp add: Suc.IH)
qed
```


(commutative-property-proof)=
#### Commutative Property Proof
Next, to prove the commutative property, we will first prove 2 helper lemmas:
```isabelle
lemma add_0_right: "add m 0 = m"
lemma add_Suc_right: "add m (Suc n) = Suc (add m n)"
```

These proofs follow the same general format for induction:
```isabelle
lemma add_0_right: "add m 0 = m"
proof (induction m)
  case 0
  show ?case by simp
next
  case (Suc m)
  show ?case by (simp add: Suc.IH)
qed

lemma add_Suc_right: "add m (Suc n) = Suc (add m n)"
proof (induction m)
  case 0
  show ?case by simp
next
  case (Suc m)
  show ?case by (simp add: Suc.IH)
qed
```

With the helper lemmas proven, we will use them to prove the commutative property

```isabelle
lemma add_comm: "add m n = add n m"
proof (induction m)
  case 0
  show ?case
    by (simp add: add_0_right)
next
  case (Suc m)
  show ?case
    by (simp add: Suc.IH add_Suc_right)
qed
```

where we use the add_0_right lemma in the base case and then the add_Suc_right lemma in the inductive step.

<!-- *This exercise was provided by Exercise 2.2 in {cite}`concreteSemanticsExercises`* -->