# HG changeset patch # User wenzelm # Date 1436204974 -7200 # Node ID eca624a8f6605833fd4f6c946792933b1857125b # Parent 0e745bd11c5523b362a5449b9108480e22f529ef tuned; diff -r 0e745bd11c55 -r eca624a8f660 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Mon Jul 06 19:33:30 2015 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon Jul 06 19:49:34 2015 +0200 @@ -1427,7 +1427,6 @@ chapter \Proof tools\ - section \Lifting package \label{sec:lifting}\ text \ @@ -1474,7 +1473,8 @@ ; @@{command (HOL) lifting_update} @{syntax nameref} ; - @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})? + @@{attribute (HOL) lifting_restore} + @{syntax thmref} (@{syntax thmref} @{syntax thmref})? \} \begin{description} @@ -1488,28 +1488,28 @@ command to work with the abstract type. An optional theorem @{term "reflp R"}, which certifies that the equivalence relation R is total, can be provided as a second argument. This allows the package to generate - stronger transfer rules. And finally, the parametricity theorem for R can - be provided as a third argument. This allows the package to generate a - stronger transfer rule for equality. + stronger transfer rules. And finally, the parametricity theorem for @{term + R} can be provided as a third argument. This allows the package to + generate a stronger transfer rule for equality. Users generally will not prove the @{text Quotient} theorem manually for new types, as special commands exist to automate the process. - When a new subtype is defined by @{command (HOL) typedef}, @{command (HOL) - "lift_definition"} can be used in its second mode, where only the - type_definition theorem @{text "type_definition Rep Abs A"} is used as an - argument of the command. The command internally proves the corresponding - Quotient theorem and registers it with @{command (HOL) setup_lifting} - using its first mode. + \medskip When a new subtype is defined by @{command (HOL) typedef}, + @{command (HOL) "lift_definition"} can be used in its second mode, where + only the @{term type_definition} theorem @{term "type_definition Rep Abs + A"} is used as an argument of the command. The command internally proves + the corresponding @{term Quotient} theorem and registers it with @{command + (HOL) setup_lifting} using its first mode. For quotients, the command @{command (HOL) quotient_type} can be used. The command defines a new quotient type and similarly to the previous case, the corresponding Quotient theorem is proved and registered by @{command (HOL) setup_lifting}. - The command @{command (HOL) "setup_lifting"} also sets up the code - generator for the new type. Later on, when a new constant is defined by - @{command (HOL) "lift_definition"}, the Lifting package proves and + \medskip The command @{command (HOL) "setup_lifting"} also sets up the + code generator for the new type. Later on, when a new constant is defined + by @{command (HOL) "lift_definition"}, the Lifting package proves and registers a code equation (if there is one) for the new constant. \item @{command (HOL) "lift_definition"} @{text "f :: \"} @{keyword (HOL) @@ -1518,15 +1518,15 @@ representation type. More formally, if @{text "t :: \"}, then the command builds a term @{text "F"} as a corresponding combination of abstraction and representation functions such that @{text "F :: \ \ \" } and defines - @{text f} is as @{text "f \ F t"}. The term @{text t} does not have to be - necessarily a constant but it can be any term. - - The command opens a proof environment and the user must discharge a - respectfulness proof obligation. For a type copy, i.e., a typedef with - @{text UNIV}, the obligation is discharged automatically. The proof goal - is presented in a user-friendly, readable form. A respectfulness theorem - in the standard format @{text f.rsp} and a transfer rule @{text - f.transfer} for the Transfer package are generated by the package. + @{text "f \ F t"}. The term @{text t} does not have to be necessarily a + constant but it can be any term. + + The command opens a proof and the user must discharge a respectfulness + proof obligation. For a type copy, i.e.\ a typedef with @{text UNIV}, the + obligation is discharged automatically. The proof goal is presented in a + user-friendly, readable form. A respectfulness theorem in the standard + format @{text f.rsp} and a transfer rule @{text f.transfer} for the + Transfer package are generated by the package. The user can specify a parametricity theorems for @{text t} after the keyword @{keyword "parametric"}, which allows the command to generate @@ -1540,24 +1540,31 @@ unconditional for total quotients. The equation defines @{text f} using the abstraction function. - Integration with [@{attribute code} abstract]: For subtypes (e.g., - corresponding to a datatype invariant, such as @{typ "'a dlist"}), + \medskip Integration with [@{attribute code} abstract]: For subtypes + (e.g.\ corresponding to a datatype invariant, such as @{typ "'a dlist"}), @{command (HOL) "lift_definition"} uses a code certificate theorem @{text f.rep_eq} as a code equation. Because of the limitation of the code generator, @{text f.rep_eq} cannot be used as a code equation if the - subtype occurs inside the result type rather than at the top level (e.g., - function returning @{typ "'a dlist option"} vs. @{typ "'a dlist"}). In - this case, an extension of @{command (HOL) "lift_definition"} can be + subtype occurs inside the result type rather than at the top level (e.g.\ + function returning @{typ "'a dlist option"} vs. @{typ "'a dlist"}). + + In this case, an extension of @{command (HOL) "lift_definition"} can be invoked by specifying the flag @{text "code_dt"}. This extension enables code execution through series of internal type and lifting definitions if the return type @{text "\"} meets the following inductive conditions: - \begin{description} \item @{text "\"} is a type variable \item @{text "\ = - \\<^sub>1 \ \\<^sub>n \"}, where @{text "\"} is an abstract type constructor and - @{text "\\<^sub>1 \ \\<^sub>n"} do not contain abstract types (i.e., @{typ "int - dlist"} is allowed whereas @{typ "int dlist dlist"} not) \item @{text "\ = - \\<^sub>1 \ \\<^sub>n \"}, @{text "\"} is a type constructor that was defined as a - (co)datatype whose constructor argument types do not contain either - non-free datatypes or the function type. \end{description} + + \begin{description} + + \item @{text "\"} is a type variable \item @{text "\ = \\<^sub>1 \ \\<^sub>n \"}, + where @{text "\"} is an abstract type constructor and @{text "\\<^sub>1 \ \\<^sub>n"} + do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed whereas + @{typ "int dlist dlist"} not) + + \item @{text "\ = \\<^sub>1 \ \\<^sub>n \"}, @{text "\"} is a type constructor that + was defined as a (co)datatype whose constructor argument types do not + contain either non-free datatypes or the function type. + + \end{description} Integration with [@{attribute code} equation]: For total quotients, @{command (HOL) "lift_definition"} uses @{text f.abs_eq} as a code @@ -1592,7 +1599,7 @@ \item @{command (HOL) "print_quotients"} prints stored quotient theorems. \item @{attribute (HOL) quot_map} registers a quotient map theorem, a - theorem showing how to "lift" quotients over type constructors. E.g., + theorem showing how to "lift" quotients over type constructors. E.g.\ @{term "Quotient R Abs Rep T \ Quotient (rel_set R) (image Abs) (image Rep) (rel_set T)"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically @@ -1600,7 +1607,7 @@ \item @{attribute (HOL) relator_eq_onp} registers a theorem that shows that a relator applied to an equality restricted by a predicate @{term P} - (i.e., @{term "eq_onp P"}) is equal to a predicator applied to the @{term + (i.e.\ @{term "eq_onp P"}) is equal to a predicator applied to the @{term P}. The combinator @{const eq_onp} is used for internal encoding of proper subtypes. Such theorems allows the package to hide @{text eq_onp} from a user in a user-readable form of a respectfulness theorem. For examples see @@ -1609,7 +1616,7 @@ dead variables. \item @{attribute (HOL) "relator_mono"} registers a property describing a - monotonicity of a relator. E.g., @{term "A \ B \ rel_set A \ rel_set B"}. + monotonicity of a relator. E.g.\ @{prop "A \ B \ rel_set A \ rel_set B"}. This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"} when a parametricity theorem for the raw term is specified and also for the reflexivity prover. For @@ -1618,11 +1625,11 @@ involved type is BNF without dead variables. \item @{attribute (HOL) "relator_distr"} registers a property describing a - distributivity of the relation composition and a relator. E.g., @{text + distributivity of the relation composition and a relator. E.g.\ @{text "rel_set R \\ rel_set S = rel_set (R \\ S)"}. This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"} when a parametricity theorem for the raw term is specified. When this - equality does not hold unconditionally (e.g., for the function type), the + equality does not hold unconditionally (e.g.\ for the function type), the user can specified each direction separately and also register multiple theorems with different set of assumptions. This attribute can be used only after the monotonicity property was already registered by @{attribute @@ -1643,7 +1650,7 @@ Lifting infrastructure and thus sets up lifting for an abstract type @{text \} (that is defined by @{text Quotient_thm}). Optional theorems @{text pcr_def} and @{text pcr_cr_eq_thm} can be specified to register the - parametrized correspondence relation for @{text \}. E.g., for @{typ "'a + parametrized correspondence relation for @{text \}. E.g.\ for @{typ "'a dlist"}, @{text pcr_def} is @{text "pcr_dlist A \ list_all2 A \\ cr_dlist"} and @{text pcr_cr_eq_thm} is @{text "pcr_dlist op= = op="}. This attribute is rather used for low-level manipulation with set-up of @@ -1703,7 +1710,7 @@ theorem as @{method (HOL) "transfer"} internally does. \item @{attribute (HOL) Transfer.transferred} works in the opposite - direction than @{method (HOL) "transfer'"}. E.g., given the transfer + direction than @{method (HOL) "transfer'"}. E.g.\ given the transfer relation @{text "ZN x n \ (x = int n)"}, corresponding transfer rules and the theorem @{text "\x::int \ {0..}. x < x + 1"}, the attribute would prove @{text "\n::nat. n < n + 1"}. The attribute is still in experimental @@ -1731,10 +1738,10 @@ \item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection of rules, which specify a domain of a transfer relation by a - predicate. E.g., given the transfer relation @{text "ZN x n \ (x = int + predicate. E.g.\ given the transfer relation @{text "ZN x n \ (x = int n)"}, one can register the following transfer domain rule: @{text "Domainp ZN = (\x. x \ 0)"}. The rules allow the package to produce more readable - transferred goals, e.g., when quantifiers are transferred. + transferred goals, e.g.\ when quantifiers are transferred. \item @{attribute (HOL) relator_eq} attribute collects identity laws for relators of various type constructors, e.g. @{term "rel_set (op =) = (op @@ -1745,7 +1752,7 @@ dead variables. \item @{attribute_def (HOL) "relator_domain"} attribute collects rules - describing domains of relators by predicators. E.g., @{term "Domainp + describing domains of relators by predicators. E.g.\ @{term "Domainp (rel_set T) = (\A. Ball A (Domainp T))"}. This allows the package to lift transfer domain rules through type constructors. For examples see @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This @@ -2153,7 +2160,7 @@ an argument to tester, making @{text "tester ="} optional. When multiple testers are given, these are applied in parallel. If no tester is specified, quickcheck uses the testers that are set - active, i.e., configurations @{attribute + active, i.e.\ configurations @{attribute quickcheck_exhaustive_active}, @{attribute quickcheck_random_active}, @{attribute quickcheck_narrowing_active} are set to true. @@ -2183,7 +2190,7 @@ structured proofs should be ignored. \item[@{text locale}] specifies how to process conjectures in - a locale context, i.e., they can be interpreted or expanded. + a locale context, i.e.\ they can be interpreted or expanded. The option is a whitespace-separated list of the two words @{text interpret} and @{text expand}. The list determines the order they are employed. The default setting is to first use