On 08/02/2013 12:04 AM, Makarius wrote:
On Wed, 17 Jul 2013, Christian Sternagel wrote:
in case anybody finds localized ad-hoc overloading useful.
Quite often it is just a matter to tell users about the existence of
such useful tools.
Do you feel like making an example theory, e.g.
src/HOL/ex/Adhoc_Overloading_Examples.thy or a short entry for the
isar-ref manual? E.g. somewhere here
http://isabelle.in.tum.de/repos/isabelle/annotate/122416054a9c/src/Doc/IsarRef/HOL_Specific.thy
I gave both a try. Please find the resulting changesets (via hg
export) attached (I also squeezed in some unrelated changes:
spell-checking, tuning of error messages. I hope that is okay).
cheers
chris
# HG changeset patch
# User Christian Sternagel
# Date 1375425767 -32400
# Fri Aug 02 15:42:47 2013 +0900
# Node ID a854ff7d191ae0735664632516e3274a1e7bd2f7
# Parent 5e53d4373e38de46b1f0358aeca06ecd8fbb4bdb
some documentation for adhoc overloading;
spell-checked;
diff -r 5e53d4373e38 -r a854ff7d191a src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy Fri Aug 02 15:42:01 2013 +0900
+++ b/src/Doc/IsarRef/HOL_Specific.thy Fri Aug 02 15:42:47 2013 +0900
@@ -1,5 +1,5 @@
theory HOL_Specific
-imports Base Main ~~/src/HOL/Library/Old_Recdef
+imports Base Main ~~/src/HOL/Library/Old_Recdef ~~/src/Tools/Adhoc_Overloading
begin
chapter {* Higher-Order Logic *}
@@ -588,7 +588,7 @@
There are no fixed syntactic restrictions on the body of the
function, but the induced functional must be provably monotonic
- wrt.\ the underlying order. The monotonicitity proof is performed
+ wrt.\ the underlying order. The monotonicity proof is performed
internally, and the definition is rejected when it fails. The proof
can be influenced by declaring hints using the
@{attribute (HOL) partial_function_mono} attribute.
@@ -622,7 +622,7 @@
@{const partial_function_definitions} appropriately.
\item @{attribute (HOL) partial_function_mono} declares rules for
- use in the internal monononicity proofs of partial function
+ use in the internal monotonicity proofs of partial function
definitions.
\end{description}
@@ -1288,7 +1288,7 @@
morphisms} specification provides alternative names. @{command
(HOL) quotient_type} requires the user to prove that the relation
is an equivalence relation (predicate @{text equivp}), unless the
- user specifies explicitely @{text partial} in which case the
+ user specifies explicitly @{text partial} in which case the
obligation is @{text part_equivp}. A quotient defined with @{text
partial} is weaker in the sense that less things can be proved
automatically.
@@ -1318,7 +1318,7 @@
and @{method (HOL) descending} continues in the same way as
@{method (HOL) lifting} does. @{method (HOL) descending} tries
to solve the arising regularization, injection and cleaning
-subgoals with the analoguous method @{method (HOL)
+subgoals with the analogous method @{method (HOL)
descending_setup} which leaves the four unsolved subgoals.
\item @{method (HOL) partiality_descending} finds the regularized
@@ -1416,6 +1416,46 @@
problem, one should use @{command (HOL) ax_specification}.
*}
+section {* Adhoc overloading of constants *}
+
+text {*
+ \begin{tabular}{rcll}
+ @{command_def adhoc_overloading} : @{text local_theory \rightarrow local_theory} \\
+ @{command_def no_adhoc_overloading} : @{text local_theory \rightarrow local_theory} \\
+ @{attribute_def show_variants} : @{text attribute} default @{text false} \\
+ \end{tabular}
+
+ \medskip
+
+ Adhoc overloading allows to overload a constant depending on
+ its type. Typically this involves the introduction of an
+ uninterpreted constant (used for input and output) and the addition
+ of some variants (used internally). For examples see
+ @{file ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy} and
+ @{file ~~/src/HOL/Library/Monad_Syntax.thy}.
+
+ @{rail
+(@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
+(@{syntax nameref} (@{syntax term} + ) + @'and')
+ }
+
+ \begin{description}
+
+ \item @{command adhoc_overloading}~@{text c v\^isub1 ... v\^isubn}
+ associates variants with an existing constant.
+
+ \item @{command no_adhoc_overloading} is similar to
+ @{command adhoc_overloading}, but removes the specified variants
+ from the present context.
+
+ \item @{attribute show_variants} controls printing of variants
+ of overloaded constants. If enabled, the internally used variants
+ are printed instead of their respective overloaded constants. This
+ is occasionally useful to check whether the system agrees with a
+ user's expectations about derived variants.
+
+ \end{description}
+*}
chapter {* Proof tools *}
@@ -1553,7 +1593,7 @@
equations in the code generator. The option @{text no_code}
of the command @{command (HOL) setup_lifting} can turn off that
behavior and causes that code
