NEWS, CONTRIBUTORS, documentation for lift_bnf
authortraytel
Wed Aug 12 20:46:33 2015 +0200 (2015-08-12)
changeset 6092097c20589a0db
parent 60919 b0ba7799d05a
child 60921 487050067be9
NEWS, CONTRIBUTORS, documentation for lift_bnf
CONTRIBUTORS
NEWS
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/CONTRIBUTORS	Wed Aug 12 20:46:33 2015 +0200
     1.2 +++ b/CONTRIBUTORS	Wed Aug 12 20:46:33 2015 +0200
     1.3 @@ -21,6 +21,10 @@
     1.4  * Summer 2015: Florian Haftmann, TUM
     1.5    Fundamentals of abstract type class for factorial rings.
     1.6  
     1.7 +* Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich
     1.8 +  Command to lift a BNF structure on the raw type to the abstract type
     1.9 +  for typedefs.
    1.10 +
    1.11  
    1.12  Contributions to Isabelle2015
    1.13  -----------------------------
     2.1 --- a/NEWS	Wed Aug 12 20:46:33 2015 +0200
     2.2 +++ b/NEWS	Wed Aug 12 20:46:33 2015 +0200
     2.3 @@ -188,6 +188,9 @@
     2.4  * Nitpick:
     2.5    - Removed "check_potential" and "check_genuine" options.
     2.6  
     2.7 +* New command lift_bnf for lifting a BNF structure to a type defined
     2.8 +  using typedef
     2.9 +
    2.10  * Division on integers is bootstrapped directly from division on
    2.11  naturals and uses generic numeral algorithm for computations.
    2.12  Slight INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes
     3.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Aug 12 20:46:33 2015 +0200
     3.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Aug 12 20:46:33 2015 +0200
     3.3 @@ -2771,6 +2771,65 @@
     3.4  for further examples of BNF registration, some of which feature custom
     3.5  witnesses.
     3.6  
     3.7 +For many typedefs (in particular for type copies) lifting the BNF structure
     3.8 +from the raw type to the abstract type can be done uniformly. This is the task
     3.9 +of the @{command lift_bnf} command. Using @{command lift_bnf} the above
    3.10 +registration of @{typ "('d, 'a) fn"} as a BNF becomes much shorter.
    3.11 +*}
    3.12 +
    3.13 +    (*<*) context early begin (*>*)
    3.14 +    lift_bnf (*<*)(no_warn_wits)(*>*) ('d, 'a) fn by auto
    3.15 +    (*<*) end (*>*)
    3.16 +
    3.17 +text {*
    3.18 +Indeed, for type copies the proof obligations are so simple that they can be
    3.19 +discharged automatically, yielding another command @{command copy_bnf} which
    3.20 +does not issue proof obligations.
    3.21 +*}
    3.22 +
    3.23 +    (*<*) context late begin (*>*)
    3.24 +    copy_bnf ('d, 'a) fn
    3.25 +    (*<*) end (*>*)
    3.26 +
    3.27 +text {*
    3.28 +Since records (or rather record schemes) are particular type copies,
    3.29 +the @{command copy_bnf} can be used to register records as BNFs.
    3.30 +*}
    3.31 +
    3.32 +    record 'a point =
    3.33 +      xval :: 'a
    3.34 +      yval :: 'a
    3.35 +    
    3.36 +    copy_bnf ('a, 'z) point_ext
    3.37 +
    3.38 +text {*
    3.39 +The proof obligations handed over to the user by @{command lift_bnf} in
    3.40 +the general case are simpler than the acual BNF properties (in particular,
    3.41 +no cardinality reasoning is required). They are best illustrated on an
    3.42 +example. Suppose we define the type of nonempty lists.
    3.43 +*}
    3.44 +
    3.45 +    typedef 'a nonempty_list = "{xs :: 'a list. xs \<noteq> []}" by auto
    3.46 +
    3.47 +text {*
    3.48 +Then, @{command lift_bnf} requires us to prove that the set of nonempty lists
    3.49 +is closed under the map function and the zip function (where the latter only
    3.50 +occurs implicitly in the goal, in form of the variable
    3.51 +@{term "zs :: ('a \<times> 'b) list"}).
    3.52 +*}
    3.53 +
    3.54 +    lift_bnf (*<*)(no_warn_wits)(*>*) 'a nonempty_list
    3.55 +    proof -
    3.56 +      fix f and xs :: "'a list"
    3.57 +      assume "xs \<in> {xs. xs \<noteq> []}"
    3.58 +      then show "map f xs \<in> {xs. xs \<noteq> []}" by (cases xs(*<*)rule: list.exhaust(*>*)) auto
    3.59 +    next
    3.60 +      fix zs :: "('a \<times> 'b) list"
    3.61 +      assume "map fst zs \<in> {xs. xs \<noteq> []}" "map snd zs \<in> {xs. xs \<noteq> []}"
    3.62 +      then show "zs \<in> {xs. xs \<noteq> []}" by (cases zs(*<*)rule: list.exhaust(*>*)) auto
    3.63 +    qed
    3.64 +
    3.65 +text {*
    3.66  The next example declares a BNF axiomatically. This can be convenient for
    3.67  reasoning abstractly about an arbitrary BNF. The @{command bnf_axiomatization}
    3.68  command below introduces a type @{text "('a, 'b, 'c) F"}, three set constants,
    3.69 @@ -2825,6 +2884,48 @@
    3.70  %%% TODO: elaborate on proof obligations
    3.71  *}
    3.72  
    3.73 +subsubsection {* \keyw{lift_bnf} and \keyw{copy_bnf}
    3.74 +  \label{sssec:lift-bnf} *}
    3.75 +
    3.76 +text {*
    3.77 +\begin{matharray}{rcl}
    3.78 +  @{command_def "lift_bnf"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
    3.79 +  @{command_def "copy_bnf"} & : & @{text "local_theory \<rightarrow> local_theory"}
    3.80 +\end{matharray}
    3.81 +
    3.82 +@{rail \<open>
    3.83 +  @@{command lift_bnf} target? lb_options? \<newline>
    3.84 +    @{syntax tyargs} name wit_terms?  \<newline>
    3.85 +    ('via' @{syntax thmref})? @{syntax map_rel}?
    3.86 +  ;
    3.87 +  @{syntax_def lb_options}: '(' ((@{syntax plugins} | 'no_warn_wits') + ',') ')'
    3.88 +  ;
    3.89 +  @{syntax_def wit_terms}: '[' 'wits' ':' terms ']'
    3.90 +  ;
    3.91 +  @@{command copy_bnf} target? ('(' @{syntax plugins} ')')? \<newline>
    3.92 +    @{syntax tyargs} name ('via' @{syntax thmref})? @{syntax map_rel}?
    3.93 +\<close>}
    3.94 +\medskip
    3.95 +
    3.96 +\noindent
    3.97 +The @{command lift_bnf} command registers an existing type (abstract type),
    3.98 +defined as a subtype of a BNF (raw type) using the @{command typedef} command,
    3.99 +as a BNF. To do so, it lifts the BNF structure on the raw type to the abstract
   3.100 +type following a @{term type_definition} theorem (the theorem is usually inferred
   3.101 +from the type, but can also be explicitly supplied by the user using the
   3.102 +@{text via} slot). In addition, custom names for map, set functions, and the relator,
   3.103 +as well as nonemptiness witnesses can be specified; otherwise, default versions are used.
   3.104 +Nonemptiness witnesses are not lifted from the raw type's BNF (this would be
   3.105 +inherently incomplete), but must be given as terms (on the raw type) and proved
   3.106 +to be witnesses. The command warns aggresively about witness types that a present
   3.107 +in the raw type's BNF but not supplied by the user. The warning can be turned off
   3.108 +by passing the @{text no_warn_wits} option.
   3.109 +
   3.110 +The @{command copy_bnf} command, performes the same lifting for type copies
   3.111 +(@{command typedef}s with @{term UNIV} as the representing set) without bothering
   3.112 +the user with trivial proof obligations. (Here, all nonemptiness witnesses from the raw
   3.113 +type's BNF can also be lifted without problems.)
   3.114 +*}
   3.115  
   3.116  subsubsection {* \keyw{bnf_axiomatization}
   3.117    \label{sssec:bnf-axiomatization} *}