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)" 
    by (simp add: fact_iter_def)
  also have "... = (Suc n * t) * fact n" 
    using hyp.
  also have "... = t * fact (Suc n)" 
    by (simp add: add_mult_distrib add_mult_distrib2)
  finally show ?case.
qed

Overall, I must say that this is the most readable proof I have seen in a system offering as much automation as Isabelle does. Also note that it is only slightly more verbose.