--- 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\<^isub>1 ... v\<^isub>n"}
+ 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 certificate theorems generated by
- @{command (HOL) "lift_definition"} are not registred as abstract
+ @{command (HOL) "lift_definition"} are not registered as abstract
code equations.
\item @{command (HOL) "lift_definition"} @{text "f :: \<tau> is t"}
@@ -1607,7 +1647,7 @@
files.
\item @{attribute (HOL) reflexivity_rule} registers a theorem that shows
- that a relator respects reflexivity and left-totality. For exampless
+ that a relator respects reflexivity and left-totality. For examples
see @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
The property is used in generation of abstraction function equations.
@@ -2009,7 +2049,7 @@
counterexamples using a series of assignments for its free
variables; by default the first subgoal is tested, an other can be
selected explicitly using an optional goal index. Assignments can
- be chosen exhausting the search space upto a given size, or using a
+ be chosen exhausting the search space up to a given size, or using a
fixed number of random assignments in the search space, or exploring
the search space symbolically using narrowing. By default,
quickcheck uses exhaustive testing. A number of configuration
@@ -2373,12 +2413,12 @@
internally.
Constants may be specified by giving them literally, referring to
- all executable contants within a certain theory by giving @{text
+ all executable constants within a certain theory by giving @{text
"name.*"}, or referring to \emph{all} executable constants currently
available by giving @{text "*"}.
By default, for each involved theory one corresponding name space
- module is generated. Alternativly, a module name may be specified
+ module is generated. Alternatively, a module name may be specified
after the @{keyword "module_name"} keyword; then \emph{all} code is
placed in this module.