src/Doc/Isar_Ref/HOL_Specific.thy

 
   \end{description}
 \<close>
 
 
-section \<open>Quotient types\<close>
+section \<open>Quotient types with lifting and transfer\<close>
+
+text \<open>The quotient package defines a new quotient type given a raw type and
+  a partial equivalence relation (\secref{sec:quotient-type}). The package
+  also historically includes automation for transporting definitions and
+  theorems (\secref{sec:old-quotient}), but most of this automation was
+  superseded by the Lifting (\secref{sec:lifting}) and Transfer
+  (\secref{sec:transfer}) packages.\<close>
+
+
+subsection \<open>Quotient type definition \label{sec:quotient-type}\<close>
 
 text \<open>
   \begin{matharray}{rcl}
     @{command_def (HOL) "quotient_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
+  \end{matharray}
+
+  @{rail \<open>
+    @@{command (HOL) quotient_type} @{syntax typespec} @{syntax mixfix}? '='
+      quot_type \<newline> quot_morphisms? quot_parametric?
+    ;
+    quot_type: @{syntax type} '/' ('partial' ':')? @{syntax term}
+    ;
+    quot_morphisms: @'morphisms' @{syntax name} @{syntax name}
+    ;
+    quot_parametric: @'parametric' @{syntax thmref}
+  \<close>}
+
+  \begin{description}
+
+  \item @{command (HOL) "quotient_type"} defines a new quotient type @{text
+  \<tau>}. The injection from a quotient type to a raw type is called @{text
+  rep_\<tau>}, its inverse @{text abs_\<tau>} 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
+  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.
+
+  The command internally proves a Quotient theorem and sets up the Lifting
+  package by the command @{command (HOL) setup_lifting}. Thus the Lifting
+  and Transfer packages can be used also with quotient types defined by
+  @{command (HOL) "quotient_type"} without any extra set-up. The
+  parametricity theorem for the equivalence relation R can be provided as an
+  extra argument of the command and is passed to the corresponding internal
+  call of @{command (HOL) setup_lifting}. This theorem allows the Lifting
+  package to generate a stronger transfer rule for equality.
+
+  \end{description}
+\<close>
+
+
+subsection \<open>Lifting package \label{sec:lifting}\<close>
+
+text \<open>
+  The Lifting package allows users to lift terms of the raw type to the
+  abstract type, which is a necessary step in building a library for an
+  abstract type. Lifting defines a new constant by combining coercion
+  functions (@{term Abs} and @{term Rep}) with the raw term. It also proves
+  an appropriate transfer rule for the Transfer (\secref{sec:transfer})
+  package and, if possible, an equation for the code generator.
+
+  The Lifting package provides two main commands: @{command (HOL)
+  "setup_lifting"} for initializing the package to work with a new type, and
+  @{command (HOL) "lift_definition"} for lifting constants. The Lifting
+  package works with all four kinds of type abstraction: type copies,
+  subtypes, total quotients and partial quotients.
+
+  Theoretical background can be found in @{cite
+  "Huffman-Kuncar:2013:lifting_transfer"}.
+
+  \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) "lifting_forget"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
+    @{command_def (HOL) "lifting_update"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
+    @{command_def (HOL) "print_quot_maps"} & : & @{text "context \<rightarrow>"}\\
+    @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
+    @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "relator_eq_onp"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "lifting_restore"} & : & @{text attribute} \\
+  \end{matharray}
+
+  @{rail \<open>
+    @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \<newline>
+      (@'parametric' @{syntax thmref})?
+    ;
+    @@{command (HOL) lift_definition} ('(' 'code_dt' ')')? \<newline>
+      @{syntax name} '::' @{syntax type} @{syntax mixfix}? 'is' @{syntax term} \<newline>
+      (@'parametric' (@{syntax thmref}+))?
+    ;
+    @@{command (HOL) lifting_forget} @{syntax nameref}
+    ;
+    @@{command (HOL) lifting_update} @{syntax nameref}
+    ;
+    @@{attribute (HOL) lifting_restore}
+      @{syntax thmref} (@{syntax thmref} @{syntax thmref})?
+  \<close>}
+
+  \begin{description}
+
+  \item @{command (HOL) "setup_lifting"} Sets up the Lifting package to work
+  with a user-defined type. The command supports two modes. The first one is
+  a low-level mode when the user must provide as a first argument of
+  @{command (HOL) "setup_lifting"} a quotient theorem @{term "Quotient R Abs
+  Rep T"}. The package configures a transfer rule for equality, a domain
+  transfer rules and sets up the @{command_def (HOL) "lift_definition"}
+  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 @{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.
+
+  \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}.
+
+  \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 :: \<tau>"} @{keyword (HOL)
+  "is"} @{text 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. More formally, if @{text "t :: \<sigma>"}, then the command
+  builds a term @{text "F"} as a corresponding combination of abstraction
+  and representation functions such that @{text "F :: \<sigma> \<Rightarrow> \<tau>" } and defines
+  @{text "f \<equiv> 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
+  parametric transfer rules for @{text f}.
+
+  For each constant defined through trivial quotients (type copies or
+  subtypes) @{text f.rep_eq} is generated. The equation is a code
+  certificate that defines @{text f} using the representation function.
+
+  For each constant @{text f.abs_eq} is generated. The equation is
+  unconditional for total quotients. The equation defines @{text f} using
+  the abstraction function.
+
+  \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
+  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 "\<tau>"} meets the following inductive conditions:
+
+  \begin{description}
+
+  \item @{text "\<tau>"} is a type variable \item @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"},
+  where @{text "\<kappa>"} is an abstract type constructor and @{text "\<tau>\<^sub>1 \<dots> \<tau>\<^sub>n"}
+  do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed whereas
+  @{typ "int dlist dlist"} not)
+
+  \item @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"}, @{text "\<kappa>"} 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
+  equation.
+
+  \item @{command (HOL) lifting_forget} and @{command (HOL) lifting_update}
+  These two commands serve for storing and deleting the set-up of the
+  Lifting package and corresponding transfer rules defined by this package.
+  This is useful for hiding of type construction details of an abstract type
+  when the construction is finished but it still allows additions to this
+  construction when this is later necessary.
+
+  Whenever the Lifting package is set up with a new abstract type @{text
+  "\<tau>"} by @{command_def (HOL) "lift_definition"}, the package defines a new
+  bundle that is called @{text "\<tau>.lifting"}. This bundle already includes
+  set-up for the Lifting package. The new transfer rules introduced by
+  @{command (HOL) "lift_definition"} can be stored in the bundle by the
+  command @{command (HOL) "lifting_update"} @{text "\<tau>.lifting"}.
+
+  The command @{command (HOL) "lifting_forget"} @{text "\<tau>.lifting"} deletes
+  set-up of the Lifting package for @{text \<tau>} and deletes all the transfer
+  rules that were introduced by @{command (HOL) "lift_definition"} using
+  @{text \<tau>} as an abstract type.
+
+  The stored set-up in a bundle can be reintroduced by the Isar commands for
+  including a bundle (@{command "include"}, @{keyword "includes"} and
+  @{command "including"}).
+
+  \item @{command (HOL) "print_quot_maps"} prints stored quotient map
+  theorems.
+
+  \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.\
+  @{term "Quotient R Abs Rep T \<Longrightarrow> 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
+  if the involved type is BNF without dead variables.
+
+  \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
+  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
+  @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+  This property is proved automatically if the involved type is BNF without
+  dead variables.
+
+  \item @{attribute (HOL) "relator_mono"} registers a property describing a
+  monotonicity of a relator. E.g.\ @{prop "A \<le> B \<Longrightarrow> rel_set A \<le> 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
+  examples see @{file "~~/src/HOL/Lifting_Set.thy"} or @{file
+  "~~/src/HOL/Lifting.thy"}. This property is proved automatically if the
+  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
+  "rel_set R \<circ>\<circ> rel_set S = rel_set (R \<circ>\<circ> 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
+  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
+  (HOL) "relator_mono"}. For examples see @{file
+  "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This
+  property is proved automatically if the involved type is BNF without dead
+  variables.
+
+  \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem
+  from the Lifting infrastructure and thus de-register the corresponding
+  quotient. This effectively causes that @{command (HOL) lift_definition}
+  will not do any lifting for the corresponding type. This attribute is
+  rather used for low-level manipulation with set-up of the Lifting package
+  because @{command (HOL) lifting_forget} is preferred for normal usage.
+
+  \item @{attribute (HOL) lifting_restore} @{text "Quotient_thm pcr_def
+  pcr_cr_eq_thm"} registers the Quotient theorem @{text Quotient_thm} in the
+  Lifting infrastructure and thus sets up lifting for an abstract type
+  @{text \<tau>} (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 \<tau>}. E.g.\ for @{typ "'a
+  dlist"}, @{text pcr_def} is @{text "pcr_dlist A \<equiv> list_all2 A \<circ>\<circ>
+  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
+  the Lifting package because using of the bundle @{text \<tau>.lifting} together
+  with the commands @{command (HOL) lifting_forget} and @{command (HOL)
+  lifting_update} is preferred for normal usage.
+
+  \item Integration with the BNF package @{cite "isabelle-datatypes"}: As
+  already mentioned, the theorems that are registered by the following
+  attributes are proved and registered automatically if the involved type is
+  BNF without dead variables: @{attribute (HOL) quot_map}, @{attribute (HOL)
+  relator_eq_onp}, @{attribute (HOL) "relator_mono"}, @{attribute (HOL)
+  "relator_distr"}. Also the definition of a relator and predicator is
+  provided automatically. Moreover, if the BNF represents a datatype,
+  simplification rules for a predicator are again proved automatically.
+
+  \end{description}
+\<close>
+
+
+subsection \<open>Transfer package \label{sec:transfer}\<close>
+
+text \<open>
+  \begin{matharray}{rcl}
+    @{method_def (HOL) "transfer"} & : & @{text method} \\
+    @{method_def (HOL) "transfer'"} & : & @{text method} \\
+    @{method_def (HOL) "transfer_prover"} & : & @{text method} \\
+    @{attribute_def (HOL) "Transfer.transferred"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "untransferred"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "transfer_rule"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "transfer_domain_rule"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "relator_eq"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "relator_domain"} & : & @{text attribute} \\
+  \end{matharray}
+
+  \begin{description}
+
+  \item @{method (HOL) "transfer"} method replaces the current subgoal with
+  a logically equivalent one that uses different types and constants. The
+  replacement of types and constants is guided by the database of transfer
+  rules. Goals are generalized over all free variables by default; this is
+  necessary for variables whose types change, but can be overridden for
+  specific variables with e.g. @{text "transfer fixing: x y z"}.
+
+  \item @{method (HOL) "transfer'"} is a variant of @{method (HOL) transfer}
+  that allows replacing a subgoal with one that is logically stronger
+  (rather than equivalent). For example, a subgoal involving equality on a
+  quotient type could be replaced with a subgoal involving equality (instead
+  of the corresponding equivalence relation) on the underlying raw type.
+
+  \item @{method (HOL) "transfer_prover"} method assists with proving a
+  transfer rule for a new constant, provided the constant is defined in
+  terms of other constants that already have transfer rules. It should be
+  applied after unfolding the constant definitions.
+
+  \item @{attribute (HOL) "untransferred"} proves the same equivalent
+  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
+  relation @{text "ZN x n \<equiv> (x = int n)"}, corresponding transfer rules and
+  the theorem @{text "\<forall>x::int \<in> {0..}. x < x + 1"}, the attribute would
+  prove @{text "\<forall>n::nat. n < n + 1"}. The attribute is still in experimental
+  phase of development.
+
+  \item @{attribute (HOL) "transfer_rule"} attribute maintains a collection
+  of transfer rules, which relate constants at two different types. Typical
+  transfer rules may relate different type instances of the same polymorphic
+  constant, or they may relate an operation on a raw type to a corresponding
+  operation on an abstract type (quotient or subtype). For example:
+
+    @{text "((A ===> B) ===> list_all2 A ===> list_all2 B) map map"} \\
+    @{text "(cr_int ===> cr_int ===> cr_int) (\<lambda>(x,y) (u,v). (x+u, y+v)) plus"}
+
+  Lemmas involving predicates on relations can also be registered using the
+  same attribute. For example:
+
+    @{text "bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"} \\
+    @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)"}
+
+  Preservation of predicates on relations (@{text "bi_unique, bi_total,
+  right_unique, right_total, left_unique, left_total"}) with the respect to
+  a relator is proved automatically if the involved type is BNF @{cite
+  "isabelle-datatypes"} without dead variables.
+
+  \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 \<equiv> (x = int
+  n)"}, one can register the following transfer domain rule: @{text "Domainp
+  ZN = (\<lambda>x. x \<ge> 0)"}. The rules allow the package to produce more readable
+  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
+  =)"}. The @{method (HOL) transfer} method uses these lemmas to infer
+  transfer rules for non-polymorphic constants on the fly. For examples see
+  @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+  This property is proved automatically if the involved type is BNF without
+  dead variables.
+
+  \item @{attribute_def (HOL) "relator_domain"} attribute collects rules
+  describing domains of relators by predicators. E.g.\ @{term "Domainp
+  (rel_set T) = (\<lambda>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
+  property is proved automatically if the involved type is BNF without dead
+  variables.
+
+  \end{description}
+
+  Theoretical background can be found in @{cite
+  "Huffman-Kuncar:2013:lifting_transfer"}.
+\<close>
+
+
+subsection \<open>Old-style definitions for quotient types \label{sec:old-quotient}\<close>
+
+text \<open>
+  \begin{matharray}{rcl}
     @{command_def (HOL) "quotient_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
     @{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} \\

     @{attribute_def (HOL) "quot_lifted"} & : & @{text attribute} \\
     @{attribute_def (HOL) "quot_respect"} & : & @{text attribute} \\
     @{attribute_def (HOL) "quot_preserve"} & : & @{text attribute} \\
   \end{matharray}
 
-  The quotient package defines a new quotient type given a raw type and a
-  partial equivalence relation. The package also historically includes
-  automation for transporting definitions and theorems. But most of this
-  automation was superseded by the Lifting (\secref{sec:lifting}) and
-  Transfer (\secref{sec:transfer}) packages. The user should consider using
-  these two new packages for lifting definitions and transporting theorems.
-
   @{rail \<open>
-    @@{command (HOL) quotient_type} @{syntax typespec} @{syntax mixfix}? '='
-      quot_type \<newline> quot_morphisms? quot_parametric?
-    ;
-    quot_type: @{syntax type} '/' ('partial' ':')? @{syntax term}
-    ;
-    quot_morphisms: @'morphisms' @{syntax name} @{syntax name}
-    ;
-    quot_parametric: @'parametric' @{syntax thmref}
-    ;
     @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \<newline>
     @{syntax term} 'is' @{syntax term}
     ;
     constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
     ;
     @@{method (HOL) lifting} @{syntax thmrefs}?
     ;
     @@{method (HOL) lifting_setup} @{syntax thmrefs}?
   \<close>}
-
-  \begin{description}
-
-  \item @{command (HOL) "quotient_type"} defines a new quotient type @{text
-  \<tau>}. The injection from a quotient type to a raw type is called @{text
-  rep_\<tau>}, its inverse @{text abs_\<tau>} 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
-  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.
-
-  The command internally proves a Quotient theorem and sets up the Lifting
-  package by the command @{command (HOL) setup_lifting}. Thus the Lifting
-  and Transfer packages can be used also with quotient types defined by
-  @{command (HOL) "quotient_type"} without any extra set-up. The
-  parametricity theorem for the equivalence relation R can be provided as an
-  extra argument of the command and is passed to the corresponding internal
-  call of @{command (HOL) setup_lifting}. This theorem allows the Lifting
-  package to generate a stronger transfer rule for equality.
-
-  \end{description}
-
-  Most of the rest of the package was superseded by the Lifting
-  (\secref{sec:lifting}) and Transfer (\secref{sec:transfer}) packages.
 
   \begin{description}
 
   \item @{command (HOL) "quotient_definition"} defines a constant on the
   quotient type.

   \end{description}
 \<close>
 
 
 chapter \<open>Proof tools\<close>
-
-section \<open>Lifting package \label{sec:lifting}\<close>
-
-text \<open>
-  \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) "lifting_forget"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
-    @{command_def (HOL) "lifting_update"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
-    @{command_def (HOL) "print_quot_maps"} & : & @{text "context \<rightarrow>"}\\
-    @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
-    @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
-    @{attribute_def (HOL) "relator_eq_onp"} & : & @{text attribute} \\
-    @{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\
-    @{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\
-    @{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\
-    @{attribute_def (HOL) "lifting_restore"} & : & @{text attribute} \\
-  \end{matharray}
-
-  The Lifting package allows users to lift terms of the raw type to the
-  abstract type, which is a necessary step in building a library for an
-  abstract type. Lifting defines a new constant by combining coercion
-  functions (@{term Abs} and @{term Rep}) with the raw term. It also proves
-  an appropriate transfer rule for the Transfer (\secref{sec:transfer})
-  package and, if possible, an equation for the code generator.
-
-  The Lifting package provides two main commands: @{command (HOL)
-  "setup_lifting"} for initializing the package to work with a new type, and
-  @{command (HOL) "lift_definition"} for lifting constants. The Lifting
-  package works with all four kinds of type abstraction: type copies,
-  subtypes, total quotients and partial quotients.
-
-  Theoretical background can be found in @{cite
-  "Huffman-Kuncar:2013:lifting_transfer"}.
-
-  @{rail \<open>
-    @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \<newline>
-      (@'parametric' @{syntax thmref})?
-    ;
-    @@{command (HOL) lift_definition} ('(' 'code_dt' ')')? \<newline>
-      @{syntax name} '::' @{syntax type} @{syntax mixfix}? 'is' @{syntax term} \<newline>
-      (@'parametric' (@{syntax thmref}+))?
-    ;
-    @@{command (HOL) lifting_forget} @{syntax nameref}
-    ;
-    @@{command (HOL) lifting_update} @{syntax nameref}
-    ;
-    @@{attribute (HOL) lifting_restore}
-      @{syntax thmref} (@{syntax thmref} @{syntax thmref})?
-  \<close>}
-
-  \begin{description}
-
-  \item @{command (HOL) "setup_lifting"} Sets up the Lifting package to work
-  with a user-defined type. The command supports two modes. The first one is
-  a low-level mode when the user must provide as a first argument of
-  @{command (HOL) "setup_lifting"} a quotient theorem @{term "Quotient R Abs
-  Rep T"}. The package configures a transfer rule for equality, a domain
-  transfer rules and sets up the @{command_def (HOL) "lift_definition"}
-  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 @{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.
-
-  \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}.
-
-  \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 :: \<tau>"} @{keyword (HOL)
-  "is"} @{text 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. More formally, if @{text "t :: \<sigma>"}, then the command
-  builds a term @{text "F"} as a corresponding combination of abstraction
-  and representation functions such that @{text "F :: \<sigma> \<Rightarrow> \<tau>" } and defines
-  @{text "f \<equiv> 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
-  parametric transfer rules for @{text f}.
-
-  For each constant defined through trivial quotients (type copies or
-  subtypes) @{text f.rep_eq} is generated. The equation is a code
-  certificate that defines @{text f} using the representation function.
-
-  For each constant @{text f.abs_eq} is generated. The equation is
-  unconditional for total quotients. The equation defines @{text f} using
-  the abstraction function.
-
-  \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
-  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 "\<tau>"} meets the following inductive conditions:
-
-  \begin{description}
-
-  \item @{text "\<tau>"} is a type variable \item @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"},
-  where @{text "\<kappa>"} is an abstract type constructor and @{text "\<tau>\<^sub>1 \<dots> \<tau>\<^sub>n"}
-  do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed whereas
-  @{typ "int dlist dlist"} not)
-
-  \item @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"}, @{text "\<kappa>"} 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
-  equation.
-
-  \item @{command (HOL) lifting_forget} and @{command (HOL) lifting_update}
-  These two commands serve for storing and deleting the set-up of the
-  Lifting package and corresponding transfer rules defined by this package.
-  This is useful for hiding of type construction details of an abstract type
-  when the construction is finished but it still allows additions to this
-  construction when this is later necessary.
-
-  Whenever the Lifting package is set up with a new abstract type @{text
-  "\<tau>"} by @{command_def (HOL) "lift_definition"}, the package defines a new
-  bundle that is called @{text "\<tau>.lifting"}. This bundle already includes
-  set-up for the Lifting package. The new transfer rules introduced by
-  @{command (HOL) "lift_definition"} can be stored in the bundle by the
-  command @{command (HOL) "lifting_update"} @{text "\<tau>.lifting"}.
-
-  The command @{command (HOL) "lifting_forget"} @{text "\<tau>.lifting"} deletes
-  set-up of the Lifting package for @{text \<tau>} and deletes all the transfer
-  rules that were introduced by @{command (HOL) "lift_definition"} using
-  @{text \<tau>} as an abstract type.
-
-  The stored set-up in a bundle can be reintroduced by the Isar commands for
-  including a bundle (@{command "include"}, @{keyword "includes"} and
-  @{command "including"}).
-
-  \item @{command (HOL) "print_quot_maps"} prints stored quotient map
-  theorems.
-
-  \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.\
-  @{term "Quotient R Abs Rep T \<Longrightarrow> 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
-  if the involved type is BNF without dead variables.
-
-  \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
-  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
-  @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
-  This property is proved automatically if the involved type is BNF without
-  dead variables.
-
-  \item @{attribute (HOL) "relator_mono"} registers a property describing a
-  monotonicity of a relator. E.g.\ @{prop "A \<le> B \<Longrightarrow> rel_set A \<le> 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
-  examples see @{file "~~/src/HOL/Lifting_Set.thy"} or @{file
-  "~~/src/HOL/Lifting.thy"}. This property is proved automatically if the
-  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
-  "rel_set R \<circ>\<circ> rel_set S = rel_set (R \<circ>\<circ> 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
-  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
-  (HOL) "relator_mono"}. For examples see @{file
-  "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This
-  property is proved automatically if the involved type is BNF without dead
-  variables.
-
-  \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem
-  from the Lifting infrastructure and thus de-register the corresponding
-  quotient. This effectively causes that @{command (HOL) lift_definition}
-  will not do any lifting for the corresponding type. This attribute is
-  rather used for low-level manipulation with set-up of the Lifting package
-  because @{command (HOL) lifting_forget} is preferred for normal usage.
-
-  \item @{attribute (HOL) lifting_restore} @{text "Quotient_thm pcr_def
-  pcr_cr_eq_thm"} registers the Quotient theorem @{text Quotient_thm} in the
-  Lifting infrastructure and thus sets up lifting for an abstract type
-  @{text \<tau>} (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 \<tau>}. E.g.\ for @{typ "'a
-  dlist"}, @{text pcr_def} is @{text "pcr_dlist A \<equiv> list_all2 A \<circ>\<circ>
-  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
-  the Lifting package because using of the bundle @{text \<tau>.lifting} together
-  with the commands @{command (HOL) lifting_forget} and @{command (HOL)
-  lifting_update} is preferred for normal usage.
-
-  \item Integration with the BNF package @{cite "isabelle-datatypes"}: As
-  already mentioned, the theorems that are registered by the following
-  attributes are proved and registered automatically if the involved type is
-  BNF without dead variables: @{attribute (HOL) quot_map}, @{attribute (HOL)
-  relator_eq_onp}, @{attribute (HOL) "relator_mono"}, @{attribute (HOL)
-  "relator_distr"}. Also the definition of a relator and predicator is
-  provided automatically. Moreover, if the BNF represents a datatype,
-  simplification rules for a predicator are again proved automatically.
-
-  \end{description}
-\<close>
-
-
-section \<open>Transfer package \label{sec:transfer}\<close>
-
-text \<open>
-  \begin{matharray}{rcl}
-    @{method_def (HOL) "transfer"} & : & @{text method} \\
-    @{method_def (HOL) "transfer'"} & : & @{text method} \\
-    @{method_def (HOL) "transfer_prover"} & : & @{text method} \\
-    @{attribute_def (HOL) "Transfer.transferred"} & : & @{text attribute} \\
-    @{attribute_def (HOL) "untransferred"} & : & @{text attribute} \\
-    @{attribute_def (HOL) "transfer_rule"} & : & @{text attribute} \\
-    @{attribute_def (HOL) "transfer_domain_rule"} & : & @{text attribute} \\
-    @{attribute_def (HOL) "relator_eq"} & : & @{text attribute} \\
-    @{attribute_def (HOL) "relator_domain"} & : & @{text attribute} \\
-  \end{matharray}
-
-  \begin{description}
-
-  \item @{method (HOL) "transfer"} method replaces the current subgoal with
-  a logically equivalent one that uses different types and constants. The
-  replacement of types and constants is guided by the database of transfer
-  rules. Goals are generalized over all free variables by default; this is
-  necessary for variables whose types change, but can be overridden for
-  specific variables with e.g. @{text "transfer fixing: x y z"}.
-
-  \item @{method (HOL) "transfer'"} is a variant of @{method (HOL) transfer}
-  that allows replacing a subgoal with one that is logically stronger
-  (rather than equivalent). For example, a subgoal involving equality on a
-  quotient type could be replaced with a subgoal involving equality (instead
-  of the corresponding equivalence relation) on the underlying raw type.
-
-  \item @{method (HOL) "transfer_prover"} method assists with proving a
-  transfer rule for a new constant, provided the constant is defined in
-  terms of other constants that already have transfer rules. It should be
-  applied after unfolding the constant definitions.
-
-  \item @{attribute (HOL) "untransferred"} proves the same equivalent
-  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
-  relation @{text "ZN x n \<equiv> (x = int n)"}, corresponding transfer rules and
-  the theorem @{text "\<forall>x::int \<in> {0..}. x < x + 1"}, the attribute would
-  prove @{text "\<forall>n::nat. n < n + 1"}. The attribute is still in experimental
-  phase of development.
-
-  \item @{attribute (HOL) "transfer_rule"} attribute maintains a collection
-  of transfer rules, which relate constants at two different types. Typical
-  transfer rules may relate different type instances of the same polymorphic
-  constant, or they may relate an operation on a raw type to a corresponding
-  operation on an abstract type (quotient or subtype). For example:
-
-    @{text "((A ===> B) ===> list_all2 A ===> list_all2 B) map map"} \\
-    @{text "(cr_int ===> cr_int ===> cr_int) (\<lambda>(x,y) (u,v). (x+u, y+v)) plus"}
-
-  Lemmas involving predicates on relations can also be registered using the
-  same attribute. For example:
-
-    @{text "bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"} \\
-    @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)"}
-
-  Preservation of predicates on relations (@{text "bi_unique, bi_total,
-  right_unique, right_total, left_unique, left_total"}) with the respect to
-  a relator is proved automatically if the involved type is BNF @{cite
-  "isabelle-datatypes"} without dead variables.
-
-  \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 \<equiv> (x = int
-  n)"}, one can register the following transfer domain rule: @{text "Domainp
-  ZN = (\<lambda>x. x \<ge> 0)"}. The rules allow the package to produce more readable
-  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
-  =)"}. The @{method (HOL) transfer} method uses these lemmas to infer
-  transfer rules for non-polymorphic constants on the fly. For examples see
-  @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
-  This property is proved automatically if the involved type is BNF without
-  dead variables.
-
-  \item @{attribute_def (HOL) "relator_domain"} attribute collects rules
-  describing domains of relators by predicators. E.g.\ @{term "Domainp
-  (rel_set T) = (\<lambda>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
-  property is proved automatically if the involved type is BNF without dead
-  variables.
-
-  \end{description}
-
-  Theoretical background can be found in @{cite
-  "Huffman-Kuncar:2013:lifting_transfer"}.
-\<close>
-
 
 section \<open>Coercive subtyping\<close>
 
 text \<open>
   \begin{matharray}{rcl}