tuning

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Dec 19 14:06:13 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jan 05 06:56:15 2015 +0100
@@ -64,6 +64,9 @@
      fp_bnf_sugar: fp_bnf_sugar,
      fp_co_induct_sugar: fp_co_induct_sugar};
 
+  val co_induct_of: 'a list -> 'a
+  val strong_co_induct_of: 'a list -> 'a
+
   val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
   val transfer_fp_sugar: theory -> fp_sugar -> fp_sugar
   val fp_sugar_of: Proof.context -> string -> fp_sugar option
@@ -76,8 +79,7 @@
   val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
   val register_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
 
-  val co_induct_of: 'a list -> 'a
-  val strong_co_induct_of: 'a list -> 'a
+  val mk_parametricity_goal: Proof.context -> term list -> term -> term -> term
 
   val flat_corec_preds_predsss_gettersss: 'a list -> 'a list list list -> 'a list list list ->
     'a list
@@ -154,8 +156,6 @@
       BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
       BNF_FP_Util.fp_result * local_theory) ->
     (local_theory -> local_theory) parser
-
-  val mk_parametricity_goal: Proof.context -> term list -> term -> term -> term
 end;
 
 structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR =
@@ -243,6 +243,9 @@
    fp_bnf_sugar: fp_bnf_sugar,
    fp_co_induct_sugar: fp_co_induct_sugar};
 
+fun co_induct_of (i :: _) = i;
+fun strong_co_induct_of [_, s] = s;
+
 fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_selss, rel_injects, rel_distincts,
     rel_sels, rel_intros, rel_cases, set_thms, set_selssss, set_introssss,
     set_cases} : fp_bnf_sugar) =
@@ -328,9 +331,6 @@
 val fp_sugars_of = fp_sugars_of_generic o Context.Proof;
 val fp_sugars_of_global = fp_sugars_of_generic o Context.Theory;
 
-fun co_induct_of (i :: _) = i;
-fun strong_co_induct_of [_, s] = s;
-
 structure FP_Sugar_Plugin = Plugin(type T = fp_sugar list);
 
 fun fp_sugars_interpretation name f =

--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Fri Dec 19 14:06:13 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Mon Jan 05 06:56:15 2015 +0100
@@ -5,65 +5,54 @@
 Parametricity of primitively (co)recursive functions.
 *)
 
-(* DO NOT FORGET TO DOCUMENT THIS NEW PLUGIN!!! *)
-
 signature BNF_FP_REC_SUGAR_TRANSFER =
 sig
-
-val primrec_transfer_pluginN : string
-val primcorec_transfer_pluginN : string
-
-val primrec_transfer_interpretation:
-  BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context -> Proof.context
-val primcorec_transfer_interpretation:
-  BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context -> Proof.context
-
+  val primrec_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context ->
+    Proof.context
+  val primcorec_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context ->
+    Proof.context
 end;
 
 structure BNF_FP_Rec_Sugar_Transfer : BNF_FP_REC_SUGAR_TRANSFER =
 struct
 
+open Ctr_Sugar_Util
+open Ctr_Sugar_Tactics
 open BNF_Def
+open BNF_FP_Util
 open BNF_FP_Def_Sugar
 open BNF_FP_Rec_Sugar_Util
-open BNF_FP_Util
-open Ctr_Sugar_Tactics
-open Ctr_Sugar_Util
 
-val primrec_transfer_pluginN = Plugin_Name.declare_setup @{binding primrec_transfer};
-val primcorec_transfer_pluginN = Plugin_Name.declare_setup @{binding primcorec_transfer};
+val transferN = "transfer";
 
 fun mk_primrec_transfer_tac ctxt def =
   Ctr_Sugar_Tactics.unfold_thms_tac ctxt [def] THEN
   HEADGOAL (Transfer.transfer_prover_tac ctxt);
 
 fun mk_primcorec_transfer_tac apply_transfer ctxt f_def corec_def type_definitions
-  dtor_corec_transfers rel_pre_defs disc_eq_cases cases case_distribs case_congs =
+    dtor_corec_transfers rel_pre_defs disc_eq_cases cases case_distribs case_congs =
   let
     fun instantiate_with_lambda thm =
       let
         val prop = Thm.prop_of thm;
-        val @{const Trueprop} $
-          (Const (@{const_name HOL.eq}, _) $
-            (Var (_, fT) $ _) $ _) = prop;
+        val @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, fT) $ _) $ _) = prop;
         val T = range_type fT;
-        val idx = Term.maxidx_of_term prop + 1;
-        val bool_expr = Var (("x", idx), HOLogic.boolT);
-        val then_expr = Var (("t", idx), T);
-        val else_expr = Var (("e", idx), T);
-        val lambda = Term.lambda bool_expr (mk_If bool_expr then_expr else_expr);
+        val j = Term.maxidx_of_term prop + 1;
+        val cond = Var (("x", j), HOLogic.boolT);
+        val then_branch = Var (("t", j), T);
+        val else_branch = Var (("e", j), T);
+        val lambda = Term.lambda cond (mk_If cond then_branch else_branch);
       in
         cterm_instantiate_pos [SOME (certify ctxt lambda)] thm
       end;
 
     val transfer_rules =
-      @{thm Abs_transfer[OF
-        BNF_Composition.type_definition_id_bnf_UNIV
+      @{thm Abs_transfer[OF BNF_Composition.type_definition_id_bnf_UNIV
         BNF_Composition.type_definition_id_bnf_UNIV]} ::
       map (fn thm => @{thm Abs_transfer} OF [thm, thm]) type_definitions @
       map (Local_Defs.unfold ctxt rel_pre_defs) dtor_corec_transfers;
-    val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add
-    val ctxt' = Context.proof_map (fold add_transfer_rule transfer_rules) ctxt
+    val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add;
+    val ctxt' = Context.proof_map (fold add_transfer_rule transfer_rules) ctxt;
 
     val case_distribs = map instantiate_with_lambda case_distribs;
     val simps = case_distribs @ disc_eq_cases @ cases @ @{thms if_True if_False};
@@ -82,71 +71,63 @@
 
 fun fp_sugar_of_bnf ctxt = fp_sugar_of ctxt o (fn Type (s, _) => s) o T_of_bnf;
 
-val cat_somes = map the o filter is_some
-fun maybe_apply z = the_default z oo Option.map
-
 fun bnf_depth_first_traverse ctxt f T z =
-  case T of
+  (case T of
     Type (s, innerTs) =>
     (case bnf_of ctxt s of
       NONE => z
     | SOME bnf => let val z' = f bnf z in
         fold (bnf_depth_first_traverse ctxt f) innerTs z'
       end)
-  | _ => z
+  | _ => z)
 
 fun if_all_bnfs ctxt Ts f g =
-  let
-    val bnfs = cat_somes (map (fn T =>
-      case T of Type (s, _) => BNF_Def.bnf_of ctxt s | _ => NONE) Ts);
-  in
+  let val bnfs = map_filter (fn Type (s, _) => BNF_Def.bnf_of ctxt s | _ => NONE) Ts in
     if length bnfs = length Ts then f bnfs else g
   end;
 
 fun mk_goal lthy f =
   let
-    val skematicTs = Term.add_tvarsT (fastype_of f) [];
+    val skematic_Ts = Term.add_tvarsT (fastype_of f) [];
 
     val ((As, Bs), names_lthy) = lthy
-      |> Ctr_Sugar_Util.mk_TFrees' (map snd skematicTs)
-      ||>> Ctr_Sugar_Util.mk_TFrees' (map snd skematicTs);
+      |> Ctr_Sugar_Util.mk_TFrees' (map snd skematic_Ts)
+      ||>> Ctr_Sugar_Util.mk_TFrees' (map snd skematic_Ts);
 
     val (Rs, names_lthy) =
       Ctr_Sugar_Util.mk_Frees "R" (map2 BNF_Util.mk_pred2T As Bs) names_lthy;
 
-    val fA = Term.subst_TVars (map fst skematicTs ~~ As) f;
-    val fB = Term.subst_TVars (map fst skematicTs ~~ Bs) f;
+    val fA = Term.subst_TVars (map fst skematic_Ts ~~ As) f;
+    val fB = Term.subst_TVars (map fst skematic_Ts ~~ Bs) f;
   in
     (BNF_FP_Def_Sugar.mk_parametricity_goal lthy Rs fA fB, names_lthy)
   end;
 
 fun prove_parametricity_if_bnf prove {transfers, fun_names, funs, fun_defs, fpTs} lthy =
   fold_index (fn (n, (((transfer, f_names), f), def)) => fn lthy =>
-      if not transfer then lthy
+      if not transfer then
+        lthy
       else
         if_all_bnfs lthy fpTs
           (fn bnfs => fn () => prove n bnfs f_names f def lthy)
-          (fn () => let val _ = error "Function is not parametric." in lthy end) ())
+          (fn () => error "Function is not parametric" (*FIXME: wording*)) ())
     (transfers ~~ fun_names ~~ funs ~~ fun_defs) lthy;
 
 fun prim_co_rec_transfer_interpretation prove =
   prove_parametricity_if_bnf (fn n => fn bnfs => fn f_name => fn f => fn def => fn lthy =>
-    case try (prove n bnfs f def) lthy of
-      NONE => error "Failed to prove parametricity."
+    (case try (prove n bnfs f def) lthy of
+      NONE => error "Failed to prove parametricity"
     | SOME thm =>
       let
-        val notes =
-          [("transfer", [thm], K @{attributes [transfer_rule]})]
+        val notes = [(transferN, [thm], K @{attributes [transfer_rule]})]
           |> massage_simple_notes f_name;
       in
         snd (Local_Theory.notes notes lthy)
-      end);
+      end));
 
 val primrec_transfer_interpretation = prim_co_rec_transfer_interpretation
-  (fn n => fn bnfs => fn f => fn def => fn lthy =>
-     let
-       val (goal, names_lthy) = mk_goal lthy f;
-     in
+  (fn _ => fn _ => fn f => fn def => fn lthy =>
+     let val (goal, names_lthy) = mk_goal lthy f in
        Goal.prove lthy [] [] goal (fn {context = ctxt, prems = _} =>
          mk_primrec_transfer_tac ctxt def)
        |> singleton (Proof_Context.export names_lthy lthy)
@@ -159,33 +140,32 @@
        val fp_sugars = map (the o fp_sugar_of_bnf lthy) bnfs;
        val (goal, names_lthy) = mk_goal lthy f;
        val (disc_eq_cases, case_thms, case_distribs, case_congs) =
-         bnf_depth_first_traverse lthy (fn bnf => fn xs =>
+         bnf_depth_first_traverse lthy (fn bnf => fn quad =>
            let
-             fun add_thms (xs, ys, zs, ws) (fp_sugar : fp_sugar) =
-               let
-                 val ctr_sugar = #ctr_sugar (#fp_ctr_sugar fp_sugar);
-                 val xs' = #disc_eq_cases ctr_sugar;
-                 val ys' = #case_thms ctr_sugar;
-                 val zs' = #case_distribs ctr_sugar;
-                 val w = #case_cong ctr_sugar;
-                 val union' = union Thm.eq_thm;
-                 val insert' = insert Thm.eq_thm;
-               in
-                 (union' xs' xs, union' ys' ys, union' zs' zs, insert' w ws)
-               end;
+             fun add_thms (disc_eq_cases0, case_thms0, case_distribs0, case_congs0)
+                {fp_ctr_sugar = {ctr_sugar = {disc_eq_cases, case_thms, case_distribs, case_cong,
+                   ...}, ...}, ...} =
+               (union Thm.eq_thm disc_eq_cases disc_eq_cases0,
+                union Thm.eq_thm case_thms case_thms0,
+                union Thm.eq_thm case_distribs case_distribs0,
+                insert Thm.eq_thm case_cong case_congs0);
            in
-             maybe_apply xs (add_thms xs) (fp_sugar_of_bnf lthy bnf)
+             Option.map (add_thms quad) (fp_sugar_of_bnf lthy bnf)
+             |> the_default quad
            end) (fastype_of f) ([], [], [], []);
      in
        Goal.prove lthy [] [] goal (fn {context = ctxt, prems = _} =>
          mk_primcorec_transfer_tac true ctxt def
          (#co_rec_def (#fp_co_induct_sugar (nth fp_sugars n)))
          (map (#type_definition o #absT_info) fp_sugars)
-         (flat (map (#xtor_co_rec_transfers o #fp_res) fp_sugars))
+         (maps (#xtor_co_rec_transfers o #fp_res) fp_sugars)
          (map (rel_def_of_bnf o #pre_bnf) fp_sugars)
          disc_eq_cases case_thms case_distribs case_congs)
        |> singleton (Proof_Context.export names_lthy lthy)
        |> Thm.close_derivation
      end);
 
-end
+val _ = Theory.setup (BNF_LFP_Rec_Sugar.primrec_interpretation Transfer_BNF.transfer_plugin
+  primrec_transfer_interpretation);
+
+end;

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Dec 19 14:06:13 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jan 05 06:56:15 2015 +0100
@@ -68,6 +68,7 @@
 open BNF_FP_Def_Sugar
 open BNF_FP_N2M_Sugar
 open BNF_FP_Rec_Sugar_Util
+open BNF_FP_Rec_Sugar_Transfer
 open BNF_GFP_Rec_Sugar_Tactics
 
 val codeN = "code";
@@ -951,7 +952,7 @@
         val prems = maps (s_not_conj o #prems) disc_eqns;
         val ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE;
         val code_rhs_opt = Option.map #code_rhs_opt sel_eqn_opt |> the_default NONE;
-        val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000 (* FIXME *);
+        val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000; (* FIXME *)
 
         val extra_disc_eqn =
           {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = n,
@@ -1504,8 +1505,7 @@
       Parse.!!! (Parse.list1 primcorec_option_parser) --| @{keyword ")"}) []) --
     (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd);
 
-val _ = Theory.setup (primcorec_interpretation
-  BNF_FP_Rec_Sugar_Transfer.primcorec_transfer_pluginN
-  BNF_FP_Rec_Sugar_Transfer.primcorec_transfer_interpretation)
+val _ = Theory.setup (primcorec_interpretation Transfer_BNF.transfer_plugin
+  primcorec_transfer_interpretation);
 
 end;

--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Dec 19 14:06:13 2014 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Jan 05 06:56:15 2015 +0100
@@ -6,6 +6,7 @@
 
 signature TRANSFER_BNF =
 sig
+  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
@@ -20,6 +21,8 @@
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 
+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))
@@ -293,8 +296,6 @@
 
 (* BNF interpretation *)
 
-val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}
-
 fun transfer_bnf_interpretation bnf lthy =
   let
     val dead = dead_of_bnf bnf

--- a/src/HOL/Transfer.thy	Fri Dec 19 14:06:13 2014 +0100
+++ b/src/HOL/Transfer.thy	Mon Jan 05 06:56:15 2015 +0100
@@ -371,12 +371,6 @@
 ML_file "Tools/Transfer/transfer_bnf.ML"
 ML_file "Tools/BNF/bnf_fp_rec_sugar_transfer.ML"
 
-ML {*
-val _ = Theory.setup (BNF_LFP_Rec_Sugar.primrec_interpretation
-  BNF_FP_Rec_Sugar_Transfer.primrec_transfer_pluginN
-  BNF_FP_Rec_Sugar_Transfer.primrec_transfer_interpretation)
-*}
-
 declare pred_fun_def [simp]
 declare rel_fun_eq [relator_eq]