# HG changeset patch # User Christian Sternagel # Date 1375425767 -32400 # Node ID a806aa7a5370960c37d553bb2ce055ff72d41030 # Parent cebaf814ca6e3733d9f0437dd1c9092bdb17954e some documentation for adhoc overloading; spell-checked; diff -r cebaf814ca6e -r a806aa7a5370 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 \ local_theory"} \\ + @{command_def "no_adhoc_overloading"} & : & @{text "local_theory \ 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 :: \ 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.