update isar-ref on Lifting
authorkuncar
Mon May 04 16:04:28 2015 +0200 (2015-05-04)
changeset 6025929f4e4366cb1
parent 60258 7364d4316a56
child 60260 2795bd5e502e
update isar-ref on Lifting
src/Doc/Isar_Ref/HOL_Specific.thy
     1.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon May 04 14:16:20 2015 +0200
     1.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon May 04 16:04:28 2015 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  theory HOL_Specific
     1.5  imports Base "~~/src/HOL/Library/Old_Datatype" "~~/src/HOL/Library/Old_Recdef"
     1.6 -  "~~/src/Tools/Adhoc_Overloading"
     1.7 +  "~~/src/Tools/Adhoc_Overloading" "~~/src/HOL/Library/Dlist"  "~~/src/HOL/Library/FSet"
     1.8  begin
     1.9  
    1.10  chapter \<open>Higher-Order Logic\<close>
    1.11 @@ -1616,8 +1616,8 @@
    1.12    \<close>}
    1.13  
    1.14    @{rail \<open>
    1.15 -    @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type}  @{syntax mixfix}? \<newline>
    1.16 -      'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?
    1.17 +    @@{command (HOL) lift_definition} ('(' 'code_dt' ')')? @{syntax name} '::' @{syntax type}  \<newline>  
    1.18 +      @{syntax mixfix}? 'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?
    1.19    \<close>}
    1.20  
    1.21    @{rail \<open>
    1.22 @@ -1695,9 +1695,24 @@
    1.23      the abstraction function.
    1.24  
    1.25      Integration with [@{attribute code} abstract]: For subtypes (e.g.,
    1.26 -    corresponding to a datatype invariant, such as dlist), @{command
    1.27 +    corresponding to a datatype invariant, such as @{typ "'a dlist"}), @{command
    1.28      (HOL) "lift_definition"} uses a code certificate theorem
    1.29 -    @{text f.rep_eq} as a code equation.
    1.30 +    @{text f.rep_eq} as a code equation. Because of the limitation of the code generator,
    1.31 +    @{text f.rep_eq} cannot be used as a code equation if the subtype occurs inside the result
    1.32 +    type rather than at the top level (e.g., function returning @{typ "'a dlist option"} vs. 
    1.33 +    @{typ "'a dlist"}). In this case, an extension of @{command
    1.34 +    (HOL) "lift_definition"} can be invoked by specifying the flag @{text "code_dt"}. This
    1.35 +    extension enables code execution through series of internal type and lifting definitions 
    1.36 +    if the return type @{text "\<tau>"} meets the following inductive conditions:
    1.37 +    \begin{description}
    1.38 +      \item  @{text "\<tau>"} is a type variable
    1.39 +      \item @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"}, where @{text "\<kappa>"} is an abstract type constructor 
    1.40 +        and @{text "\<tau>\<^sub>1 \<dots> \<tau>\<^sub>n"} do not contain abstract types (i.e., @{typ "int dlist"} is allowed 
    1.41 +        whereas @{typ "int dlist dlist"} not)
    1.42 +      \item @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"}, @{text "\<kappa>"} is a type constructor that was defined as a 
    1.43 +        (co)datatype whose constructor argument types do not contain either non-free datatypes 
    1.44 +        or the function type.
    1.45 +    \end{description}
    1.46  
    1.47      Integration with [@{attribute code} equation]: For total quotients, @{command
    1.48      (HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation.
    1.49 @@ -1780,7 +1795,7 @@
    1.50      and thus sets up lifting for an abstract type @{text \<tau>} (that is defined by @{text Quotient_thm}).
    1.51      Optional theorems @{text pcr_def} and @{text pcr_cr_eq_thm} can be specified to register 
    1.52      the parametrized
    1.53 -    correspondence relation for @{text \<tau>}. E.g., for @{text "'a dlist"}, @{text pcr_def} is
    1.54 +    correspondence relation for @{text \<tau>}. E.g., for @{typ "'a dlist"}, @{text pcr_def} is
    1.55      @{text "pcr_dlist A \<equiv> list_all2 A \<circ>\<circ> cr_dlist"} and @{text pcr_cr_eq_thm} is 
    1.56      @{text "pcr_dlist op= = op="}.
    1.57      This attribute is rather used for low-level