[isabelle-dev] NEWS: auxiliary contexts
makarius at sketis.net
Mon Apr 16 13:12:54 CEST 2012
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:
> 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.
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
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.
More information about the isabelle-dev