src/Doc/IsarRef/HOL_Specific.thy

 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 *}
 
 text {* Isabelle/HOL is based on Higher-Order Logic, a polymorphic

   Thus, the specification consists of a single function described by a
   single recursive equation.
 
   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.
 
   The mandatory @{text mode} argument specifies the mode of operation

 
   Experienced users may define new modes by instantiating the locale
   @{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}
 
 *}

   injection from a quotient type to a raw type is called @{text
   rep_t}, its inverse @{text abs_t} unless explicit @{keyword (HOL)
   "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.
 
   \item @{command (HOL) "quotient_definition"} defines a constant on

     "descending_setup"} try to guess a raw statement that would lift
     to the current subgoal. Such statement is assumed as a new subgoal
     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
     theorem that would lift to the current subgoal, lifts it and
     leaves as a subgoal. This method can be used with partial

   properties using @{command (HOL) "specification"}, one can prove
   that the two constants are, in fact, equal.  If this might be a
   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 *}
 
 section {* Adhoc tuples *}
 

     generator. This allows @{command (HOL) "lift_definition"} to
     register (generated) code certificate theorems as abstract code
     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"}
     Defines a new function @{text f} with an abstract type @{text \<tau>}
     in terms of a corresponding operation @{text t} on a

     respectfulness theorem. For examples see @{file
     "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
     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.
 
   \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem
     from the Lifting infrastructure and thus de-register the corresponding quotient. 

 
   \item @{command (HOL) "quickcheck"} tests the current goal for
   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
   options are supported for @{command (HOL) "quickcheck"}, notably:
 

   of constants in the specified target language(s).  If no
   serialization instruction is given, only abstract code is generated
   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.
 
   For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
   refers to a single file; for \emph{Haskell}, it refers to a whole