Email Gateway (Aug 18 2022 at 14:05): Email Gateway (Aug 18 2022 at 14:05):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
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.
Last updated: Apr 20 2024 at 08:16 UTC