src/HOL/Tools/BNF/bnf_lfp_size.ML
author blanchet
Wed Apr 23 10:23:27 2014 +0200 (2014-04-23)
changeset 56654 54326fa7afe6
parent 56651 fc105315822a
child 56682 d39926ff0487
permissions -rw-r--r--
qualify name
blanchet@56638
     1
(*  Title:      HOL/Tools/BNF/bnf_lfp_size.ML
blanchet@56638
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@56638
     3
    Copyright   2014
blanchet@56638
     4
blanchet@56638
     5
Generation of size functions for new-style datatypes.
blanchet@56638
     6
*)
blanchet@56638
     7
blanchet@56642
     8
signature BNF_LFP_SIZE =
blanchet@56642
     9
sig
blanchet@56651
    10
  val register_size: string -> string -> thm list -> thm list -> local_theory -> local_theory
blanchet@56651
    11
  val register_size_global: string -> string -> thm list -> thm list -> theory -> theory
blanchet@56651
    12
  val lookup_size: Proof.context -> string -> (string * (thm list * thm list)) option
blanchet@56651
    13
  val lookup_size_global: theory -> string -> (string * (thm list * thm list)) option
blanchet@56651
    14
  val generate_lfp_size: BNF_FP_Util.fp_sugar list -> local_theory -> local_theory
blanchet@56642
    15
end;
blanchet@56642
    16
blanchet@56642
    17
structure BNF_LFP_Size : BNF_LFP_SIZE =
blanchet@56638
    18
struct
blanchet@56638
    19
blanchet@56638
    20
open BNF_Util
blanchet@56640
    21
open BNF_Tactics
blanchet@56638
    22
open BNF_Def
blanchet@56650
    23
open BNF_FP_Util
blanchet@56638
    24
blanchet@56638
    25
val size_N = "size_"
blanchet@56638
    26
blanchet@56640
    27
val rec_o_mapN = "rec_o_map"
blanchet@56638
    28
val sizeN = "size"
blanchet@56640
    29
val size_o_mapN = "size_o_map"
blanchet@56638
    30
blanchet@56651
    31
val nitpicksimp_attrs = @{attributes [nitpick_simp]};
blanchet@56651
    32
val simp_attrs = @{attributes [simp]};
blanchet@56651
    33
val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs;
blanchet@56651
    34
blanchet@56651
    35
structure Data = Generic_Data
blanchet@56638
    36
(
blanchet@56638
    37
  type T = (string * (thm list * thm list)) Symtab.table;
blanchet@56638
    38
  val empty = Symtab.empty;
blanchet@56638
    39
  val extend = I
blanchet@56638
    40
  fun merge data = Symtab.merge (K true) data;
blanchet@56638
    41
);
blanchet@56638
    42
blanchet@56642
    43
fun register_size T_name size_name size_simps size_o_maps =
blanchet@56651
    44
  Context.proof_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps)))));
blanchet@56643
    45
blanchet@56651
    46
fun register_size_global T_name size_name size_simps size_o_maps =
blanchet@56651
    47
  Context.theory_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps)))));
blanchet@56651
    48
blanchet@56651
    49
val lookup_size = Symtab.lookup o Data.get o Context.Proof;
blanchet@56651
    50
val lookup_size_global = Symtab.lookup o Data.get o Context.Theory;
blanchet@56642
    51
blanchet@56638
    52
val zero_nat = @{const zero_class.zero (nat)};
blanchet@56638
    53
blanchet@56638
    54
fun mk_plus_nat (t1, t2) = Const (@{const_name Groups.plus},
blanchet@56638
    55
  HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
blanchet@56638
    56
blanchet@56638
    57
fun mk_to_natT T = T --> HOLogic.natT;
blanchet@56638
    58
blanchet@56638
    59
fun mk_abs_zero_nat T = Term.absdummy T zero_nat;
blanchet@56638
    60
blanchet@56640
    61
fun pointfill ctxt th = unfold_thms ctxt [o_apply] (th RS fun_cong);
blanchet@56640
    62
blanchet@56640
    63
fun mk_unabs_def_unused_0 n =
blanchet@56640
    64
  funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong);
blanchet@56640
    65
blanchet@56640
    66
val rec_o_map_simp_thms =
blanchet@56651
    67
  @{thms o_def id_def case_prod_app case_sum_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def};
blanchet@56638
    68
blanchet@56640
    69
fun mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map =
blanchet@56640
    70
  unfold_thms_tac ctxt [rec_def] THEN
blanchet@56651
    71
  HEADGOAL (rtac (ctor_rec_o_map RS trans)) THEN
blanchet@56651
    72
  PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion) THEN
blanchet@56651
    73
  HEADGOAL (asm_simp_tac (ss_only (pre_map_defs @ distinct Thm.eq_thm_prop abs_inverses @
blanchet@56651
    74
    rec_o_map_simp_thms) ctxt));
blanchet@56638
    75
blanchet@56651
    76
val size_o_map_simp_thms = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
blanchet@56640
    77
blanchet@56640
    78
fun mk_size_o_map_tac ctxt size_def rec_o_map inj_maps size_maps =
blanchet@56640
    79
  unfold_thms_tac ctxt [size_def] THEN
blanchet@56640
    80
  HEADGOAL (rtac (rec_o_map RS trans) THEN'
blanchet@56642
    81
    asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simp_thms) ctxt)) THEN
blanchet@56645
    82
  IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
blanchet@56638
    83
blanchet@56651
    84
fun generate_lfp_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs),
blanchet@56651
    85
    fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, nested_bnfs,
blanchet@56651
    86
    nesting_bnfs, ...} : fp_sugar) :: _) lthy0 =
blanchet@56651
    87
  let
blanchet@56651
    88
    val data = Data.get (Context.Proof lthy0);
blanchet@56651
    89
blanchet@56651
    90
    val Ts = map #T fp_sugars
blanchet@56651
    91
    val T_names = map (fst o dest_Type) Ts;
blanchet@56651
    92
    val nn = length Ts;
blanchet@56651
    93
blanchet@56651
    94
    val B_ify = Term.typ_subst_atomic (As ~~ Bs);
blanchet@56651
    95
blanchet@56651
    96
    val recs = map #co_rec fp_sugars;
blanchet@56651
    97
    val rec_thmss = map #co_rec_thms fp_sugars;
blanchet@56651
    98
    val rec_Ts as rec_T1 :: _ = map fastype_of recs;
blanchet@56651
    99
    val rec_arg_Ts = binder_fun_types rec_T1;
blanchet@56651
   100
    val Cs = map body_type rec_Ts;
blanchet@56651
   101
    val Cs_rho = map (rpair HOLogic.natT) Cs;
blanchet@56651
   102
    val substCnatT = Term.subst_atomic_types Cs_rho;
blanchet@56651
   103
blanchet@56651
   104
    val f_Ts = map mk_to_natT As;
blanchet@56651
   105
    val f_TsB = map mk_to_natT Bs;
blanchet@56651
   106
    val num_As = length As;
blanchet@56651
   107
blanchet@56651
   108
    fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0);
blanchet@56640
   109
blanchet@56651
   110
    val f_names = variant_names num_As "f";
blanchet@56651
   111
    val fs = map2 (curry Free) f_names f_Ts;
blanchet@56651
   112
    val fsB = map2 (curry Free) f_names f_TsB;
blanchet@56651
   113
    val As_fs = As ~~ fs;
blanchet@56651
   114
blanchet@56654
   115
    val size_bs =
blanchet@56654
   116
      map ((fn base => Binding.qualify false base (Binding.name (prefix size_N base))) o
blanchet@56654
   117
        Long_Name.base_name) T_names;
blanchet@56651
   118
blanchet@56651
   119
    fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T'
blanchet@56651
   120
      | is_pair_C _ _ = false;
blanchet@56640
   121
blanchet@56651
   122
    fun mk_size_of_typ (T as TFree _) =
blanchet@56651
   123
        pair (case AList.lookup (op =) As_fs T of
blanchet@56651
   124
            SOME f => f
blanchet@56651
   125
          | NONE => if member (op =) Cs T then Term.absdummy T (Bound 0) else mk_abs_zero_nat T)
blanchet@56651
   126
      | mk_size_of_typ (T as Type (s, Ts)) =
blanchet@56651
   127
        if is_pair_C s Ts then
blanchet@56651
   128
          pair (snd_const T)
blanchet@56651
   129
        else if exists (exists_subtype_in As) Ts then
blanchet@56651
   130
          (case Symtab.lookup data s of
blanchet@56651
   131
            SOME (size_name, (_, size_o_maps as _ :: _)) =>
blanchet@56651
   132
            let
blanchet@56651
   133
              val (args, size_o_mapss') = split_list (map (fn T => mk_size_of_typ T []) Ts);
blanchet@56651
   134
              val size_const = Const (size_name, map fastype_of args ---> mk_to_natT T);
blanchet@56651
   135
            in
blanchet@56651
   136
              fold (union Thm.eq_thm) (size_o_maps :: size_o_mapss')
blanchet@56651
   137
              #> pair (Term.list_comb (size_const, args))
blanchet@56651
   138
            end
blanchet@56651
   139
          | _ => pair (mk_abs_zero_nat T))
blanchet@56651
   140
        else
blanchet@56651
   141
          pair (mk_abs_zero_nat T);
blanchet@56638
   142
blanchet@56651
   143
    fun mk_size_of_arg t =
blanchet@56651
   144
      mk_size_of_typ (fastype_of t) #>> (fn s => substCnatT (betapply (s, t)));
blanchet@56651
   145
blanchet@56651
   146
    fun mk_size_arg rec_arg_T size_o_maps =
blanchet@56651
   147
      let
blanchet@56651
   148
        val x_Ts = binder_types rec_arg_T;
blanchet@56651
   149
        val m = length x_Ts;
blanchet@56651
   150
        val x_names = variant_names m "x";
blanchet@56651
   151
        val xs = map2 (curry Free) x_names x_Ts;
blanchet@56651
   152
        val (summands, size_o_maps') =
blanchet@56651
   153
          fold_map mk_size_of_arg xs size_o_maps
blanchet@56651
   154
          |>> remove (op =) zero_nat;
blanchet@56651
   155
        val sum =
blanchet@56651
   156
          if null summands then HOLogic.zero
blanchet@56651
   157
          else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
blanchet@56651
   158
      in
blanchet@56651
   159
        (fold_rev Term.lambda (map substCnatT xs) sum, size_o_maps')
blanchet@56651
   160
      end;
blanchet@56651
   161
blanchet@56651
   162
    fun mk_size_rhs recx size_o_maps =
blanchet@56651
   163
      let val (args, size_o_maps') = fold_map mk_size_arg rec_arg_Ts size_o_maps in
blanchet@56651
   164
        (fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args)), size_o_maps')
blanchet@56651
   165
      end;
blanchet@56651
   166
blanchet@56651
   167
    val maybe_conceal_def_binding = Thm.def_binding
blanchet@56651
   168
      #> Config.get lthy0 bnf_note_all = false ? Binding.conceal;
blanchet@56651
   169
blanchet@56651
   170
    val (size_rhss, nested_size_o_maps) = fold_map mk_size_rhs recs [];
blanchet@56651
   171
    val size_Ts = map fastype_of size_rhss;
blanchet@56638
   172
blanchet@56651
   173
    val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0
blanchet@56651
   174
      |> apfst split_list o fold_map2 (fn b => fn rhs =>
blanchet@56651
   175
          Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd)
blanchet@56651
   176
        size_bs size_rhss
blanchet@56651
   177
      ||> `Local_Theory.restore;
blanchet@56651
   178
blanchet@56651
   179
    val phi = Proof_Context.export_morphism lthy1 lthy1';
blanchet@56651
   180
blanchet@56651
   181
    val size_defs = map (Morphism.thm phi) raw_size_defs;
blanchet@56651
   182
blanchet@56651
   183
    val size_consts0 = map (Morphism.term phi) raw_size_consts;
blanchet@56651
   184
    val size_consts = map2 retype_const_or_free size_Ts size_consts0;
blanchet@56651
   185
    val size_constsB = map (Term.map_types B_ify) size_consts;
blanchet@56651
   186
blanchet@56651
   187
    val zeros = map mk_abs_zero_nat As;
blanchet@56638
   188
blanchet@56651
   189
    val overloaded_size_rhss = map (fn c => Term.list_comb (c, zeros)) size_consts;
blanchet@56651
   190
    val overloaded_size_Ts = map fastype_of overloaded_size_rhss;
blanchet@56651
   191
    val overloaded_size_consts = map (curry Const @{const_name size}) overloaded_size_Ts;
blanchet@56651
   192
    val overloaded_size_def_bs =
blanchet@56651
   193
      map (maybe_conceal_def_binding o Binding.suffix_name "_overloaded") size_bs;
blanchet@56638
   194
blanchet@56651
   195
    fun define_overloaded_size def_b lhs0 rhs lthy =
blanchet@56651
   196
      let
blanchet@56651
   197
        val Free (c, _) = Syntax.check_term lthy lhs0;
blanchet@56651
   198
        val (thm, lthy') = lthy
blanchet@56651
   199
          |> Local_Theory.define ((Binding.name c, NoSyn), ((def_b, []), rhs))
blanchet@56651
   200
          |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
blanchet@56651
   201
        val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
blanchet@56651
   202
        val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
blanchet@56651
   203
      in (thm', lthy') end;
blanchet@56638
   204
blanchet@56651
   205
    val (overloaded_size_defs, lthy2) = lthy1
blanchet@56651
   206
      |> Local_Theory.background_theory_result
blanchet@56651
   207
        (Class.instantiation (T_names, map dest_TFree As, [HOLogic.class_size])
blanchet@56651
   208
         #> fold_map3 define_overloaded_size overloaded_size_def_bs overloaded_size_consts
blanchet@56651
   209
           overloaded_size_rhss
blanchet@56651
   210
         ##> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
blanchet@56651
   211
         ##> Local_Theory.exit_global);
blanchet@56651
   212
blanchet@56651
   213
    val size_defs' =
blanchet@56651
   214
      map (mk_unabs_def (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs;
blanchet@56651
   215
    val size_defs_unused_0 =
blanchet@56651
   216
      map (mk_unabs_def_unused_0 (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs;
blanchet@56651
   217
    val overloaded_size_defs' =
blanchet@56651
   218
      map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) overloaded_size_defs;
blanchet@56651
   219
blanchet@56651
   220
    val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps;
blanchet@56651
   221
    val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs);
blanchet@56651
   222
blanchet@56651
   223
    fun derive_size_simp size_def' simp0 =
blanchet@56651
   224
      (trans OF [size_def', simp0])
blanchet@56651
   225
      |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_id snd_o_convol} @
blanchet@56651
   226
        all_inj_maps @ nested_size_maps) lthy2)
blanchet@56651
   227
      |> fold_thms lthy2 size_defs_unused_0;
blanchet@56651
   228
    fun derive_overloaded_size_simp size_def' simp0 =
blanchet@56651
   229
      (trans OF [size_def', simp0])
blanchet@56651
   230
      |> unfold_thms lthy2 @{thms add_0_left add_0_right}
blanchet@56651
   231
      |> fold_thms lthy2 overloaded_size_defs';
blanchet@56651
   232
blanchet@56651
   233
    val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss;
blanchet@56651
   234
    val size_simps = flat size_simpss;
blanchet@56651
   235
    val overloaded_size_simpss =
blanchet@56651
   236
      map2 (map o derive_overloaded_size_simp) overloaded_size_defs' size_simpss;
blanchet@56651
   237
    val size_thmss = map2 append size_simpss overloaded_size_simpss;
blanchet@56651
   238
blanchet@56651
   239
    val ABs = As ~~ Bs;
blanchet@56651
   240
    val g_names = variant_names num_As "g";
blanchet@56651
   241
    val gs = map2 (curry Free) g_names (map (op -->) ABs);
blanchet@56651
   242
blanchet@56651
   243
    val liveness = map (op <>) ABs;
blanchet@56651
   244
    val live_gs = AList.find (op =) (gs ~~ liveness) true;
blanchet@56651
   245
    val live = length live_gs;
blanchet@56651
   246
blanchet@56651
   247
    val maps0 = map map_of_bnf fp_bnfs;
blanchet@56651
   248
blanchet@56651
   249
    val (rec_o_map_thmss, size_o_map_thmss) =
blanchet@56651
   250
      if live = 0 then
blanchet@56651
   251
        `I (replicate nn [])
blanchet@56651
   252
      else
blanchet@56651
   253
        let
blanchet@56651
   254
          val pre_bnfs = map #pre_bnf fp_sugars;
blanchet@56651
   255
          val pre_map_defs = map map_def_of_bnf pre_bnfs;
blanchet@56651
   256
          val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
blanchet@56651
   257
          val rec_defs = map #co_rec_def fp_sugars;
blanchet@56651
   258
blanchet@56651
   259
          val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
blanchet@56651
   260
blanchet@56651
   261
          val num_rec_args = length rec_arg_Ts;
blanchet@56651
   262
          val h_Ts = map B_ify rec_arg_Ts;
blanchet@56651
   263
          val h_names = variant_names num_rec_args "h";
blanchet@56651
   264
          val hs = map2 (curry Free) h_names h_Ts;
blanchet@56651
   265
          val hrecs = map (fn recx => Term.list_comb (Term.map_types B_ify recx, hs)) recs;
blanchet@56638
   266
blanchet@56651
   267
          val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) hrecs gmaps;
blanchet@56651
   268
blanchet@56651
   269
          val ABgs = ABs ~~ gs;
blanchet@56651
   270
blanchet@56651
   271
          fun mk_rec_arg_arg (x as Free (_, T)) =
blanchet@56651
   272
            let val U = B_ify T in
blanchet@56651
   273
              if T = U then x else build_map lthy2 (the o AList.lookup (op =) ABgs) (T, U) $ x
blanchet@56651
   274
            end;
blanchet@56651
   275
blanchet@56651
   276
          fun mk_rec_o_map_arg rec_arg_T h =
blanchet@56651
   277
            let
blanchet@56651
   278
              val x_Ts = binder_types rec_arg_T;
blanchet@56651
   279
              val m = length x_Ts;
blanchet@56651
   280
              val x_names = variant_names m "x";
blanchet@56651
   281
              val xs = map2 (curry Free) x_names x_Ts;
blanchet@56651
   282
              val xs' = map mk_rec_arg_arg xs;
blanchet@56651
   283
            in
blanchet@56651
   284
              fold_rev Term.lambda xs (Term.list_comb (h, xs'))
blanchet@56651
   285
            end;
blanchet@56651
   286
blanchet@56651
   287
          fun mk_rec_o_map_rhs recx =
blanchet@56651
   288
            let val args = map2 mk_rec_o_map_arg rec_arg_Ts hs in
blanchet@56651
   289
              Term.list_comb (recx, args)
blanchet@56651
   290
            end;
blanchet@56651
   291
blanchet@56651
   292
          val rec_o_map_rhss = map mk_rec_o_map_rhs recs;
blanchet@56638
   293
blanchet@56651
   294
          val rec_o_map_goals =
blanchet@56651
   295
            map2 (fold_rev (fold_rev Logic.all) [gs, hs] o HOLogic.mk_Trueprop oo
blanchet@56651
   296
              curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss;
blanchet@56651
   297
          val rec_o_map_thms =
blanchet@56651
   298
            map3 (fn goal => fn rec_def => fn ctor_rec_o_map =>
blanchet@56651
   299
                Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} =>
blanchet@56651
   300
                  mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map)
blanchet@56651
   301
                |> Thm.close_derivation)
blanchet@56651
   302
              rec_o_map_goals rec_defs ctor_rec_o_maps;
blanchet@56651
   303
blanchet@56651
   304
          val size_o_map_conds =
blanchet@56651
   305
            if exists (can Logic.dest_implies o Thm.prop_of) nested_size_o_maps then
blanchet@56651
   306
              map (HOLogic.mk_Trueprop o mk_inj) live_gs
blanchet@56651
   307
            else
blanchet@56651
   308
              [];
blanchet@56651
   309
blanchet@56651
   310
          val fsizes = map (fn size_constB => Term.list_comb (size_constB, fsB)) size_constsB;
blanchet@56651
   311
          val size_o_map_lhss = map2 (curry HOLogic.mk_comp) fsizes gmaps;
blanchet@56651
   312
blanchet@56651
   313
          val fgs = map2 (fn fB => fn g as Free (_, Type (_, [A, B])) =>
blanchet@56651
   314
            if A = B then fB else HOLogic.mk_comp (fB, g)) fsB gs;
blanchet@56651
   315
          val size_o_map_rhss = map (fn c => Term.list_comb (c, fgs)) size_consts;
blanchet@56651
   316
blanchet@56651
   317
          val size_o_map_goals =
blanchet@56651
   318
            map2 (fold_rev (fold_rev Logic.all) [fsB, gs] o
blanchet@56651
   319
              curry Logic.list_implies size_o_map_conds o HOLogic.mk_Trueprop oo
blanchet@56651
   320
              curry HOLogic.mk_eq) size_o_map_lhss size_o_map_rhss;
blanchet@56651
   321
          val size_o_map_thms =
blanchet@56651
   322
            map3 (fn goal => fn size_def => fn rec_o_map =>
blanchet@56651
   323
                Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} =>
blanchet@56651
   324
                  mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
blanchet@56651
   325
                |> Thm.close_derivation)
blanchet@56651
   326
              size_o_map_goals size_defs rec_o_map_thms;
blanchet@56640
   327
        in
blanchet@56651
   328
          pairself (map single) (rec_o_map_thms, size_o_map_thms)
blanchet@56640
   329
        end;
blanchet@56640
   330
blanchet@56651
   331
    val massage_multi_notes =
blanchet@56651
   332
      maps (fn (thmN, thmss, attrs) =>
blanchet@56651
   333
        map2 (fn T_name => fn thms =>
blanchet@56651
   334
            ((Binding.qualify true (Long_Name.base_name T_name) (Binding.name thmN), attrs),
blanchet@56651
   335
             [(thms, [])]))
blanchet@56651
   336
          T_names thmss)
blanchet@56651
   337
      #> filter_out (null o fst o hd o snd);
blanchet@56638
   338
blanchet@56651
   339
    val notes =
blanchet@56651
   340
      [(rec_o_mapN, rec_o_map_thmss, []),
blanchet@56651
   341
       (sizeN, size_thmss, code_nitpicksimp_simp_attrs),
blanchet@56651
   342
       (size_o_mapN, size_o_map_thmss, [])]
blanchet@56651
   343
      |> massage_multi_notes;
blanchet@56651
   344
  in
blanchet@56651
   345
    lthy2
blanchet@56651
   346
    |> Local_Theory.notes notes |> snd
blanchet@56651
   347
    |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps)
blanchet@56651
   348
    |> Local_Theory.declaration {syntax = false, pervasive = true}
blanchet@56651
   349
      (fn phi => Data.map (fold2 (fn T_name => fn Const (size_name, _) =>
blanchet@56651
   350
           Symtab.update (T_name, (size_name,
blanchet@56651
   351
             pairself (map (Morphism.thm phi)) (size_simps, flat size_o_map_thmss))))
blanchet@56651
   352
         T_names size_consts))
blanchet@56651
   353
  end;
blanchet@56638
   354
blanchet@56638
   355
end;