disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
--- a/src/HOL/String.thy Tue Oct 06 21:04:44 2015 +0200
+++ b/src/HOL/String.thy Wed Oct 07 10:02:43 2015 +0200
@@ -8,7 +8,7 @@
subsection \<open>Characters and strings\<close>
-datatype nibble =
+datatype (plugins del: transfer) nibble =
Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
| Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 06 21:04:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Oct 07 10:02:43 2015 +0200
@@ -64,6 +64,8 @@
fp_bnf_sugar: fp_bnf_sugar,
fp_co_induct_sugar: fp_co_induct_sugar}
+ val transfer_plugin: string
+
val co_induct_of: 'a list -> 'a
val strong_co_induct_of: 'a list -> 'a
@@ -254,6 +256,8 @@
fp_bnf_sugar: fp_bnf_sugar,
fp_co_induct_sugar: fp_co_induct_sugar};
+val transfer_plugin = Plugin_Name.declare_setup @{binding transfer};
+
fun co_induct_of (i :: _) = i;
fun strong_co_induct_of [_, s] = s;
@@ -636,24 +640,27 @@
end;
in
if live = 0 then
- let
- val relAsBs = HOLogic.eq_const fpT;
- val rel_cases_thm = derive_rel_cases relAsBs [] [];
-
- val case_transfer_thm = derive_case_transfer rel_cases_thm;
-
- val notes =
- [(case_transferN, [case_transfer_thm], K [])]
- |> massage_simple_notes fp_b_name;
-
- val (noted, lthy') = lthy
- |> Local_Theory.notes notes;
-
- val subst = Morphism.thm (substitute_noted_thm noted);
- in
- (([], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [], []),
- lthy')
- end
+ if plugins transfer_plugin then
+ let
+ val relAsBs = HOLogic.eq_const fpT;
+ val rel_cases_thm = derive_rel_cases relAsBs [] [];
+
+ val case_transfer_thm = derive_case_transfer rel_cases_thm;
+
+ val notes =
+ [(case_transferN, [case_transfer_thm], K [])]
+ |> massage_simple_notes fp_b_name;
+
+ val (noted, lthy') = lthy
+ |> Local_Theory.notes notes;
+
+ val subst = Morphism.thm (substitute_noted_thm noted);
+ in
+ (([], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [], []),
+ lthy')
+ end
+ else
+ (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy)
else
let
val mapx = mk_map live As Bs (map_of_bnf fp_bnf);
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Tue Oct 06 21:04:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Wed Oct 07 10:02:43 2015 +0200
@@ -154,7 +154,7 @@
|> Thm.close_derivation
end);
-val _ = Theory.setup (lfp_rec_sugar_interpretation Transfer_BNF.transfer_plugin
+val _ = Theory.setup (lfp_rec_sugar_interpretation transfer_plugin
lfp_rec_sugar_transfer_interpretation);
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Oct 06 21:04:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Oct 07 10:02:43 2015 +0200
@@ -1604,7 +1604,7 @@
--| @{keyword ")"}) []) --
(Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorec_cmd);
-val _ = Theory.setup (gfp_rec_sugar_interpretation Transfer_BNF.transfer_plugin
+val _ = Theory.setup (gfp_rec_sugar_interpretation transfer_plugin
gfp_rec_sugar_transfer_interpretation);
end;
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Tue Oct 06 21:04:44 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Oct 07 10:02:43 2015 +0200
@@ -8,7 +8,6 @@
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
val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data
@@ -25,8 +24,6 @@
exception NO_PRED_DATA of unit
-val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}
-
(* util functions *)
fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))