[isabelle-dev] NEWS: auxiliary contexts

[Lawrence Paulson]

I look forward to seeing some documentation on these increasingly mysterious constructs… :-)
Larry

On 16 Apr 2012, at 11:14, Brian Huffman wrote:

> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev