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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
