[isabelle-dev] NEWS: auxiliary contexts
lp15 at cam.ac.uk
Tue Apr 17 09:01:45 CEST 2012
I look forward to seeing some documentation on these increasingly mysterious constructs… :-)
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:
> fixes z0 z1 :: "'a"
> fixes f0 f1 :: "'a => 'a"
> 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
> fixes dummy :: "'t::long_class_name_that_I_don't_want_to_type_again"
> Good work, and many thanks for implementing this!
> - Brian
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev