--- a/src/Doc/Datatypes/Datatypes.thy Sat Mar 28 20:22:10 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Sat Mar 28 21:05:02 2015 +0100
@@ -865,25 +865,25 @@
\item[@{text "t."}\hthm{case_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
@{thm list.case_transfer[no_vars]} \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
\item[@{text "t."}\hthm{sel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
This property is missing for @{typ "'a list"} because there is no common
selector to all constructors. \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
\item[@{text "t."}\hthm{ctr_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
@{thm list.ctr_transfer(1)[no_vars]} \\
@{thm list.ctr_transfer(2)[no_vars]} \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
\item[@{text "t."}\hthm{disc_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
@{thm list.disc_transfer(1)[no_vars]} \\
@{thm list.disc_transfer(2)[no_vars]} \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
\item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.set(1)[no_vars]} \\
@@ -958,7 +958,7 @@
\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}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
\item[@{text "t."}\hthm{map_cong0}\rm:] ~ \\
@{thm list.map_cong0[no_vars]}
@@ -981,7 +981,7 @@
\item[@{text "t."}\hthm{map_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
@{thm list.map_transfer[no_vars]} \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(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]} \\
@@ -1012,7 +1012,7 @@
\item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
@{thm list.rel_transfer[no_vars]} \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
\end{description}
\end{indentblock}
@@ -1053,7 +1053,7 @@
\item[@{text "t."}\hthm{rec_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
@{thm list.rec_transfer[no_vars]} \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
\end{description}
\end{indentblock}
@@ -1928,7 +1928,7 @@
\item[@{text "t."}\hthm{corec_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
@{thm llist.corec_transfer[no_vars]} \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
\end{description}
\end{indentblock}
@@ -3066,7 +3066,8 @@
the \hthm{transfer} plugin generates a predicator @{text "t.pred_t"} and
properties that guide the Transfer tool.
-The plugin derives the following properties:
+For types with no dead type arguments (and at least one live type argument), the
+plugin derives the following properties:
\begin{indentblock}
\begin{description}
--- a/src/HOL/Tools/BNF/bnf_comp.ML Sat Mar 28 20:22:10 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Sat Mar 28 21:05:02 2015 +0100
@@ -791,7 +791,10 @@
val repTA = mk_T_of_bnf Ds As bnf;
val T_bind = qualify b;
- val TA_params = Term.add_tfreesT repTA (if has_live_phantoms then As' else []);
+ val all_TA_params_in_order = Term.add_tfreesT repTA As';
+ val TA_params =
+ (if has_live_phantoms then all_TA_params_in_order
+ else inter (op =) (Term.add_tfreesT repTA []) all_TA_params_in_order);
val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
maybe_typedef lthy has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
(fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
@@ -906,7 +909,9 @@
val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs)
|> map (fn (b, def) => ((b, []), [([def], [])]))
- val (noted, lthy'') = lthy' |> Local_Theory.notes notes
+ val (noted, lthy'') = lthy'
+ |> Local_Theory.notes notes
+ ||> (if repTA = TA then I else register_bnf_raw (fst (dest_Type TA)) bnf'')
in
((morph_bnf (substitute_noted_thm noted) bnf'', (all_deads, absT_info)), lthy'')
end;
--- a/src/HOL/Tools/BNF/bnf_def.ML Sat Mar 28 20:22:10 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Sat Mar 28 21:05:02 2015 +0100
@@ -1609,7 +1609,8 @@
[Pretty.block [Pretty.str (bdN ^ ":"), Pretty.brk 1,
Pretty.quote (Syntax.pretty_term ctxt bd)]]);
in
- Pretty.big_list "BNFs:" (map pretty_bnf (Symtab.dest (Data.get (Context.Proof ctxt))))
+ Pretty.big_list "Registered bounded natural functors:"
+ (map pretty_bnf (sort_wrt fst (Symtab.dest (Data.get (Context.Proof ctxt)))))
|> Pretty.writeln
end;
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Sat Mar 28 20:22:10 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Sat Mar 28 21:05:02 2015 +0100
@@ -93,7 +93,7 @@
in
[((Binding.empty, []), [([relator_eq_onp_thm], @{attributes [relator_eq_onp]})])]
end
- handle ERROR _ => [] (* the "lifting" plugin should work even if "quotient" is disabled *)
+ handle NO_PRED_DATA _ => [] (* the "lifting" plugin should work even if "quotient" is disabled *)
(* relator_mono *)
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Sat Mar 28 20:22:10 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Sat Mar 28 21:05:02 2015 +0100
@@ -6,6 +6,8 @@
signature TRANSFER_BNF =
sig
+ exception NO_PRED_DATA of unit
+
val transfer_plugin: string
val base_name_of_bnf: BNF_Def.bnf -> binding
val type_name_of_bnf: BNF_Def.bnf -> string
@@ -21,6 +23,8 @@
open BNF_FP_Util
open BNF_FP_Def_Sugar
+exception NO_PRED_DATA of unit
+
val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}
(* util functions *)
@@ -318,9 +322,9 @@
(* simplification rules for the predicator *)
fun lookup_defined_pred_data lthy name =
- case (Transfer.lookup_pred_data lthy name) of
+ case Transfer.lookup_pred_data lthy name of
SOME data => data
- | NONE => (error "lookup_pred_data: something went utterly wrong")
+ | NONE => raise NO_PRED_DATA ()
fun lives_of_fp (fp_sugar: fp_sugar) =
let
@@ -377,6 +381,7 @@
|> Variable.export lthy old_lthy
|> map Drule.zero_var_indexes
end
+ handle NO_PRED_DATA () => []
(* fp_sugar interpretation *)