--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Apr 27 15:24:37 2012 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Apr 27 17:06:36 2012 +0200
@@ -1254,14 +1254,99 @@
\end{description}
*}
+section {* Lifting package *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def (HOL) "setup_lifting"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
+ @{command_def (HOL) "lift_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
+ @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\
+ @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
+ @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
+ \end{matharray}
+
+ @{rail "
+ @@{command (HOL) setup_lifting} ('(' 'no_abs_code' ')')? \\
+ @{syntax thmref} @{syntax thmref}?;
+ "}
+
+ @{rail "
+ @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \\
+ 'is' @{syntax term};
+ "}
+
+ \begin{description}
+
+ \item @{command (HOL) "setup_lifting"} Sets up the Lifting package to work with
+ a user-defined type. The user must provide either a quotient
+ theorem @{text "Quotient R Abs Rep T"} or a type_definition theorem
+ @{text "type_definition Rep Abs A"}.
+ The package configures
+ transfer rules for equality and quantifiers on the type, and sets
+ up the @{command_def (HOL) "lift_definition"} command to work with the type.
+ In the case of a quotient theorem,
+ an optional theorem @{text "reflp R"} can be provided as a second argument.
+ This allows the package to generate stronger transfer rules.
+
+ @{command (HOL) "setup_lifting"} is called automatically if a quotient type
+ is defined by the command @{command (HOL) "quotient_type"} from the Quotient package.
+
+ If @{command (HOL) "setup_lifting"} is called with a type_definition theorem,
+ the abstract type implicitly defined by the theorem is declared as an abstract type in
+ the code 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_abs_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 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 representation type.
+ The term @{text t} doesn't have to be necessarily a constant but it can
+ be any term.
+
+ Users must discharge a respectfulness proof obligation when each
+ constant is defined. For a type copy, i.e. a typedef with @{text UNIV},
+ the proof is discharged automatically. The obligation is
+ presented in a user-friendly, readable form. A respectfulness
+ theorem in the standard format @{text f.rsp} and a transfer rule @{text f.tranfer}
+ for the Transfer package are generated by the package.
+
+ Integration with code_abstype: For typedefs (e.g. subtypes
+ corresponding to a datatype invariant, such as dlist),
+ @{command (HOL) "lift_definition"}
+ generates a code certificate theorem @{text f.rep_eq} and sets up
+ code generation for each constant.
+
+ \item @{command (HOL) "print_quotmaps"} prints stored quotient map
+ theorems.
+
+ \item @{command (HOL) "print_quotients"} prints stored quotient theorems.
+
+ \item @{attribute (HOL) quot_map} registers a quotient map theorem. For examples see
+ @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy files.
+
+ \item @{attribute (HOL) invariant_commute} registers a theorem which shows a relationship
+ between the constant @{text Lifting.invariant} (used for internal encoding of proper subtypes)
+ and a relator.
+ Such theorems allows the package to hide @{text Lifting.invariant} from a user
+ in a user-readable form of a respectfulness theorem. For examples see
+ @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy files.
+
+
+ \end{description}
+
+*}
+
section {* Quotient types *}
text {*
\begin{matharray}{rcl}
@{command_def (HOL) "quotient_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
@{command_def (HOL) "quotient_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
- @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\
- @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
+ @{command_def (HOL) "print_quotmapsQ3"} & : & @{text "context \<rightarrow>"}\\
+ @{command_def (HOL) "print_quotientsQ3"} & : & @{text "context \<rightarrow>"}\\
@{command_def (HOL) "print_quotconsts"} & : & @{text "context \<rightarrow>"}\\
@{method_def (HOL) "lifting"} & : & @{text method} \\
@{method_def (HOL) "lifting_setup"} & : & @{text method} \\
@@ -1323,10 +1408,10 @@
\item @{command (HOL) "quotient_definition"} defines a constant on
the quotient type.
- \item @{command (HOL) "print_quotmaps"} prints quotient map
+ \item @{command (HOL) "print_quotmapsQ3"} prints quotient map
functions.
- \item @{command (HOL) "print_quotients"} prints quotients.
+ \item @{command (HOL) "print_quotientsQ3"} prints quotients.
\item @{command (HOL) "print_quotconsts"} prints quotient constants.