[isabelle] A finished project and an interesting unification bug



I was sitting down to write an email about a unification bug, and it
occurred to me that Isabelle users might also be interested in the
status of our project.

I've been working on the L4.verified project at NICTA (see
http://ertos.nicta.com.au/research/l4.verified/). Our objective was to
use Isabelle as an analysis tool in proving that an operating system
kernel satisfied certain conditions. I'm pleased to report that Isabelle
has served us well and our project was completed successfully. You can
read the story in various places, including slashdot (see
http://tech.slashdot.org/story/09/08/13/0827231/Worlds-First-Formally).

With our project done, one of my follow-up jobs was to push our patch to the record package back upstream. The repository record package was effectively unusable for records with more than 150 fields, a limit we increase to around 1000. I'm hoping the change will make it into the next Isabelle release.

While cleaning up the mechanism by which certain facts about record updators were proven, I came across a charming unification bug.

Suppose one were to define a predicate and some rules about it like so:

constdefs
  somepredicate :: "(('b => 'b) => ('a => 'a))
                              => 'a => 'b => bool"
 "somepredicate upd v x == True"

lemma somepredicate_idI:
  "somepredicate id (f v) v"
  by (simp add: somepredicate_def)

lemma somepredicate_triv:
  "somepredicate upd v x ==> somepredicate upd v x"
  by assumption

We can resolve the two rules against each other:

lemmas somepredicate_triv [OF somepredicate_idI]

However, if we first instantiate 'a with a function type, we get a TERM
exception out of the bowels of the unifier:

lemmas somepredicate_triv[where v="f :: nat => bool", OF somepredicate_idI]

*** exception TERM raised: fastype: expected function type
*** At command "lemmas".

I've confirmed this issue exists in multiple versions of Isabelle
including a recent snapshot. Severity is medium, it being easy to work
around the issue once isolated but difficult to track down when it first
appeared (the first time I attempted to define a record with a
functional field type). Likelihood of anyone else tripping on this in the near future is low.

Yours,
    Thomas.







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.