# HG changeset patch # User traytel # Date 1455718686 -3600 # Node ID 7d0c92d5dd804bb80ca227bbc24cd5c62ab070fa # Parent 9f7fa08d23077469928561c98270ec8bdc1906ca document predicator in datatypes diff -r 9f7fa08d2307 -r 7d0c92d5dd80 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Feb 17 15:18:06 2016 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Feb 17 15:18:06 2016 +0100 @@ -342,7 +342,7 @@ text \ The @{command datatype} command introduces various constants in addition to the constructors. With each datatype are associated set functions, a map -function, a relator, discriminators, and selectors, all of which can be given +function,, a predicator, a relator, discriminators, and selectors, all of which can be given custom names. In the example below, the familiar names @{text null}, @{text hd}, @{text tl}, @{text set}, @{text map}, and @{text list_all2} override the default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2}, @@ -654,7 +654,7 @@ \noindent The discriminators and selectors are generated only if the @{text "discs_sels"} option is enabled or if names are specified for discriminators or selectors. -The set functions, map function, and relator are generated only if $m > 0$. +The set functions, map function, predicator, and relator are generated only if $m > 0$. In addition, some of the plugins introduce their own constants (Section~\ref{sec:selecting-plugins}). The case combinator, discriminators, @@ -858,7 +858,7 @@ one live type argument (e.g., @{typ "'a list"}). They are partitioned in two subgroups. The first subgroup consists of properties involving the constructors or the destructors and either a set function, the map function, -or the relator: +the predicator, or the relator: \begin{indentblock} \begin{description} @@ -944,7 +944,7 @@ (Section~\ref{ssec:code-generator}). The second subgroup consists of more abstract properties of the set functions, -the map function, and the relator: +the map function, the predicator, and the relator: \begin{indentblock} \begin{description} @@ -955,13 +955,8 @@ \item[@{text "t."}\hthm{inj_map_strong}\rm:] ~ \\ @{thm list.inj_map_strong[no_vars]} -\item[@{text "t."}\hthm{set_map}\rm:] ~ \\ -@{thm list.set_map[no_vars]} - -\item[@{text "t."}\hthm{set_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ -@{thm list.set_transfer[no_vars]} \\ -The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin -(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments. +\item[@{text "t."}\hthm{map_comp}\rm:] ~ \\ +@{thm list.map_comp[no_vars]} \item[@{text "t."}\hthm{map_cong0}\rm:] ~ \\ @{thm list.map_cong0[no_vars]} @@ -969,6 +964,9 @@ \item[@{text "t."}\hthm{map_cong} @{text "[fundef_cong]"}\rm:] ~ \\ @{thm list.map_cong[no_vars]} +\item[@{text "t."}\hthm{map_cong_pred}\rm:] ~ \\ +@{thm list.map_cong_pred[no_vars]} + \item[@{text "t."}\hthm{map_cong_simp}\rm:] ~ \\ @{thm list.map_cong_simp[no_vars]} @@ -986,6 +984,40 @@ The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin (Section~\ref{ssec:transfer}) for type constructors with no dead type arguments. +\item[@{text "t."}\hthm{pred_cong} @{text "[fundef_cong]"}\rm:] ~ \\ +@{thm list.pred_cong[no_vars]} + +\item[@{text "t."}\hthm{pred_cong_simp}\rm:] ~ \\ +@{thm list.pred_cong_simp[no_vars]} + +\item[@{text "t."}\hthm{pred_map}\rm:] ~ \\ +@{thm list.pred_map[no_vars]} + +\item[@{text "t."}\hthm{pred_mono_strong}\rm:] ~ \\ +@{thm list.pred_mono_strong[no_vars]} + +\item[@{text "t."}\hthm{pred_rel}\rm:] ~ \\ +@{thm list.pred_rel[no_vars]} + +\item[@{text "t."}\hthm{pred_set}\rm:] ~ \\ +@{thm list.pred_set[no_vars]} + +\item[@{text "t."}\hthm{pred_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ +@{thm list.pred_transfer[no_vars]} \\ +The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin +(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments. + +\item[@{text "t."}\hthm{pred_True}\rm:] ~ \\ +@{thm list.pred_True[no_vars]} + +\item[@{text "t."}\hthm{set_map}\rm:] ~ \\ +@{thm list.set_map[no_vars]} + +\item[@{text "t."}\hthm{set_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ +@{thm list.set_transfer[no_vars]} \\ +The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin +(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments. + \item[@{text "t."}\hthm{rel_compp} @{text "[relator_distr]"}\rm:] ~ \\ @{thm list.rel_compp[no_vars]} \\ The @{text "[relator_distr]"} attribute is set by the @{text lifting} plugin @@ -997,6 +1029,9 @@ \item[@{text "t."}\hthm{rel_eq}\rm:] ~ \\ @{thm list.rel_eq[no_vars]} +\item[@{text "t."}\hthm{rel_eq_onp}\rm:] ~ \\ +@{thm list.rel_eq_onp[no_vars]} + \item[@{text "t."}\hthm{rel_flip}\rm:] ~ \\ @{thm list.rel_flip[no_vars]} @@ -1750,6 +1785,7 @@ for map: lmap rel: llist_all2 + pred: llist_all where "ltl LNil = LNil" @@ -2711,7 +2747,12 @@ (functorial action), $n$ set functions (natural transformations), and an infinite cardinal bound that satisfy certain properties. For example, @{typ "'a llist"} is a unary BNF. -Its relator @{text "llist_all2 :: +Its predicator @{text "llist_all :: + ('a \ bool) \ + 'a llist \ bool"} +extends unary predicates over elements to unary predicates over +lazy lists. +Similarly, its relator @{text "llist_all2 :: ('a \ 'b \ bool) \ 'a llist \ 'b llist \ bool"} extends binary predicates over elements to binary predicates over parallel @@ -2738,7 +2779,7 @@ The type is simply a copy of the function space @{typ "'d \ 'a"}, where @{typ 'a} is live and @{typ 'd} is dead. We introduce it together with its map function, -set function, and relator. +set function, predicator, and relator. \ typedef ('d, 'a) fn = "UNIV :: ('d \ 'a) set" @@ -2756,6 +2797,11 @@ text \ \blankline \ lift_definition + pred_fn :: "('a \ bool) \ ('d, 'a) fn \ bool" + is + "pred_fun (\_. True)" . + + lift_definition rel_fn :: "('a \ 'b \ bool) \ ('d, 'a) fn \ ('d, 'b) fn \ bool" is "rel_fun (op =)" . @@ -2767,6 +2813,7 @@ sets: set_fn bd: "natLeq +c |UNIV :: 'd set|" rel: rel_fn + pred: pred_fn proof - show "map_fn id = id" by transfer auto @@ -2809,6 +2856,10 @@ show "rel_fn R = (\x y. \z. set_fn z \ {(x, y). R x y} \ map_fn fst z = x \ map_fn snd z = y)" unfolding fun_eq_iff relcompp.simps conversep.simps by transfer (force simp: rel_fun_def subset_iff) + next + fix P :: "'a \ bool" + show "pred_fn P = (\x. Ball (set_fn x) P)" + unfolding fun_eq_iff by transfer simp qed text \ \blankline \ @@ -2891,7 +2942,7 @@ lift_bnf (*<*)(no_warn_wits) (*>*)'a nonempty_list proof - - fix f(*<*):: "'a \ 'c"(*>*) and xs :: "'a list" + fix f (*<*):: "'a \ 'c"(*>*)and xs :: "'a list" assume "xs \ {xs. xs \ []}" then show "map f xs \ {xs. xs \ []}" by (cases xs(*<*) rule: list.exhaust(*>*)) auto @@ -2906,7 +2957,7 @@ The next example declares a BNF axiomatically. This can be convenient for reasoning abstractly about an arbitrary BNF. The @{command bnf_axiomatization} command below introduces a type @{text "('a, 'b, 'c) F"}, three set constants, -a map function, a relator, and a nonemptiness witness that depends only on +a map function, a predicator, a relator, and a nonemptiness witness that depends only on @{typ 'a}. The type @{text "'a \ ('a, 'b, 'c) F"} of the witness can be read as an implication: Given a witness for @{typ 'a}, we can construct a witness for @{text "('a, 'b, 'c) F"}. The BNF properties are postulated as axioms. @@ -2944,7 +2995,7 @@ \noindent The @{command bnf} command registers an existing type as a bounded natural functor (BNF). The type must be equipped with an appropriate map function -(functorial action). In addition, custom set functions, relators, and +(functorial action). In addition, custom set functions, predicators, relators, and nonemptiness witnesses can be specified; otherwise, default versions are used. The syntactic entity \synt{target} can be used to specify a local context, @@ -2983,7 +3034,7 @@ structure on the raw type to the abstract type following a @{term type_definition} theorem. The theorem is usually inferred from the type, but can also be explicitly supplied by means of the optional @{text via} clause. In -addition, custom names for the set functions, the map function, and the relator, +addition, custom names for the set functions, the map function, the predicator, and the relator, as well as nonemptiness witnesses can be specified. Nonemptiness witnesses are not lifted from the raw type's BNF, as this would be @@ -3034,7 +3085,7 @@ \noindent The @{command bnf_axiomatization} command declares a new type and associated constants -(map, set, relator, and cardinal bound) and asserts the BNF properties for +(map, set, predicator, relator, and cardinal bound) and asserts the BNF properties for these constants as axioms. The syntactic entity \synt{target} can be used to specify a local context, @@ -3359,9 +3410,6 @@ @{thm list.pred_inject(2)[no_vars]} \\ This property is generated only for (co)datatypes. -\item[@{text "t."}\hthm{rel_eq_onp}\rm:] ~ \\ -@{thm list.rel_eq_onp[no_vars]} - \item[@{text "t."}\hthm{left_total_rel} @{text "[transfer_rule]"}\rm:] ~ \\ @{thm list.left_total_rel[no_vars]} @@ -3424,9 +3472,9 @@ \end{indentblock} In addition, the plugin sets the @{text "[relator_eq]"} attribute on a -variant of the @{text t.rel_eq_onp} property generated by the @{text lifting} -plugin, the @{text "[relator_mono]"} attribute on @{text t.rel_mono}, and the -@{text "[relator_distr]"} attribute on @{text t.rel_compp}. +variant of the @{text t.rel_eq_onp} property, the @{text "[relator_mono]"} +attribute on @{text t.rel_mono}, and the @{text "[relator_distr]"} attribute +on @{text t.rel_compp}. \