[isabelle-dev] NEWS: auxiliary contexts

[Brian Huffman]

On Sun, Apr 15, 2012 at 2:54 PM, Makarius <makarius at sketis.net> wrote:
> * Auxiliary contexts indicate block structure for specifications with
> additional parameters and assumptions.  Such unnamed contexts may be
> nested within other targets, like 'theory', 'locale', 'class',
> 'instantiation' etc.  Results from the local context are generalized
> accordingly and applied to the enclosing target context.

> The most basic application is to factor-out context elements of
> several fixes/assumes/shows theorem statements

This is very nice! Finally we have a mechanism similar to "Section" in
Coq, a more lightweight alternative to locales. I already replaced a
one-off locale with this new local context (changeset 4d49f3ffe97e),
and I expect I'll come across a few more places where I can make
similar changes.

> Any other local theory specification element works within the "context
> ... begin ... end" block as well.

Another good use case is recursive functions with many parameters that
don't change in recursive calls. For example, here's a recursion
combinator for binary integers:

context
  fixes z0 z1 :: "'a"
  fixes f0 f1 :: "'a => 'a"
begin

function bin_rec :: "int => 'a" where
  "bin_rec x =
    (if x = 0 then z0 else if x = -1 then z1 else
      (if x mod 2 = 0 then f0 else f1) (bin_rec (x div 2)))"
by pat_completeness auto

Fixing z0, z1, f0, and f1 in the context makes the function definition
more legible, it makes termination proof simpler, and it also yields a
simpler induction rule, similar to what you get with "for" in an
inductive predicate definition. In fact, it seems like these context
blocks could totally subsume the "for" option.

Another application might be to fix a few type variables of specific
sorts, which would be useful in files with lots of sort annotations.
This would take care of the need for a defaulting mechanism for type
variables.

context
  fixes dummy :: "'t::long_class_name_that_I_don't_want_to_type_again"
begin
...
end

Good work, and many thanks for implementing this!

- Brian