[isabelle-dev] NEWS: auxiliary contexts

[Makarius]

On Mon, 16 Apr 2012, Brian Huffman wrote:

> 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.

Good observation.

Back then when 'function' and 'inductive' were localized, there was a 
discussion with Alex Krauss and Stefan Berghofer about the precise meaning 
the the small auxiliary context introduced via 'for' around the package. 
There were reasons for the current (slightly different) arrangement for 
the two packages, but the above form of having the context really 
factored-out was not covered by either one.  Now it can be used with any 
other package as well, that lacks additional treatment of local 
parameters.

In any case, the 'for' notation is a legitimate add-on to certain tools 
and packages that have a need for some private context extension in one 
way or the other.  Over time its use is expected to increase a little, 
without becoming too prominent.  It is a useful add-on solution in the 
backhand of package implementors.


 	Makarius