# Playing with Isar

Handwritten versions: Pg. 1, Pg. 2, Pg. 3.

Lately I have been playing with the Isabelle proof assistant, and I really like what I have been seeing. Isabelle has a lot of automation, and that is sort of one of my basic prerequisites when investigating proof systems. Isabelle has impressed me, though, because of how it has both automation and pretty great tools for creating well documented, readable theories.

In this essay I want to highlight one of these features: the Isar proof language. This really nice language allows a programmer to create clean, readable proofs, even elegant proof some of the time. In short, Isabelle's Isar language lets you write machine checkable proofs that read like paper proofs.

Lets consider a classic example of proving an iterative version of factorial is correct. The normal definitions and hand approach might look something like this:

```f(n)    = 1          when n = 0
n * f(n-1) otherwise

f'(n,t) = t           when n = 0
f'(n-1,n*t) otherwise```

Here we assume that the domains are over the natural numbers. Here is a simple proof by induction:

1. Assume `n = 0`, then `f'(0,t) = t*f(0)` by definition.
2. Assume `f'(n,t) = t*f(n)`, then
``` f'(n+1,t) = f'(n,(n+1)*t) by definition
= (n+1)*t*f(n)  by induction hypothesis
= t*f(n+1)      by definition and arithmetic```

This proves `f'(n,t)=t*f(n)`.

The above is about as simple an example as I can think of. Now, observe what this might look like when we do the same in an Isabelle theory; pay attention to the similarities and differences in the corresponding proofs.

```primrec fact :: "nat => nat"
where "fact 0 = 1" | "fact (Suc n) = (Suc n) * fact n"

primrec fact_iter :: "nat => nat => nat"
where
"fact_iter 0 t = t" |
"fact_iter (Suc n) t = fact_iter n (Suc n * t)"

theorem fact_iter_correct: "fact_iter n t = t * fact n"
proof (induct n arbitrary: t)
case 0 thus ?case by (simp add: fact_iter_def fact_def)
next
case (Suc n) note hyp = this
have "fact_iter (Suc n) t = fact_iter n (Suc n * t)"