src/HOL/Tools/BNF/bnf_lfp_size.ML
author desharna
Mon Oct 06 13:37:38 2014 +0200 (2014-10-06)
changeset 58578 9ff8ca957c02
parent 58461 75ee8d49c724
child 58634 9f10d82e8188
permissions -rw-r--r--
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
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@58315
     5
Generation of size functions for datatypes.
blanchet@56638
     6
*)
blanchet@56638
     7
blanchet@56642
     8
signature BNF_LFP_SIZE =
blanchet@56642
     9
sig
blanchet@58191
    10
  val size_plugin: string
blanchet@56651
    11
  val register_size: string -> string -> thm list -> thm list -> local_theory -> local_theory
blanchet@56651
    12
  val register_size_global: string -> string -> thm list -> thm list -> theory -> theory
blanchet@58179
    13
  val size_of: Proof.context -> string -> (string * (thm list * thm list)) option
blanchet@58179
    14
  val size_of_global: theory -> string -> (string * (thm list * thm list)) option
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@58179
    23
open BNF_FP_Def_Sugar
blanchet@56638
    24
blanchet@58337
    25
val size_plugin = "size";
blanchet@58186
    26
blanchet@58337
    27
val size_N = "size_";
blanchet@56638
    28
blanchet@58337
    29
val rec_o_mapN = "rec_o_map";
blanchet@58337
    30
val sizeN = "size";
blanchet@58337
    31
val size_o_mapN = "size_o_map";
blanchet@56638
    32
blanchet@56651
    33
val nitpicksimp_attrs = @{attributes [nitpick_simp]};
blanchet@56651
    34
val simp_attrs = @{attributes [simp]};
blanchet@56651
    35
blanchet@56651
    36
structure Data = Generic_Data
blanchet@56638
    37
(
blanchet@56638
    38
  type T = (string * (thm list * thm list)) Symtab.table;
blanchet@56638
    39
  val empty = Symtab.empty;
blanchet@56638
    40
  val extend = I
blanchet@56638
    41
  fun merge data = Symtab.merge (K true) data;
blanchet@56638
    42
);
blanchet@56638
    43
blanchet@56642
    44
fun register_size T_name size_name size_simps size_o_maps =
blanchet@56651
    45
  Context.proof_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps)))));
blanchet@56643
    46
blanchet@56651
    47
fun register_size_global T_name size_name size_simps size_o_maps =
blanchet@56651
    48
  Context.theory_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps)))));
blanchet@56651
    49
blanchet@58179
    50
val size_of = Symtab.lookup o Data.get o Context.Proof;
blanchet@58179
    51
val size_of_global = Symtab.lookup o Data.get o Context.Theory;
blanchet@56642
    52
blanchet@56638
    53
fun mk_plus_nat (t1, t2) = Const (@{const_name Groups.plus},
blanchet@56638
    54
  HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
blanchet@56638
    55
blanchet@56638
    56
fun mk_to_natT T = T --> HOLogic.natT;
blanchet@56638
    57
blanchet@58337
    58
fun mk_abs_zero_nat T = Term.absdummy T HOLogic.zero;
blanchet@56638
    59
blanchet@58355
    60
fun mk_pointfull ctxt th = unfold_thms ctxt [o_apply] (th RS fun_cong);
blanchet@56640
    61
blanchet@56640
    62
fun mk_unabs_def_unused_0 n =
blanchet@56640
    63
  funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong);
blanchet@56640
    64
blanchet@58180
    65
val rec_o_map_simps =
blanchet@58353
    66
  @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod id_bnf_def};
blanchet@56638
    67
blanchet@57399
    68
fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
blanchet@57399
    69
    ctor_rec_o_map =
blanchet@58377
    70
  HEADGOAL (subst_tac @{context} (SOME [1, 2]) [rec_def] THEN' rtac (ctor_rec_o_map RS trans) THEN'
traytel@57890
    71
    CONVERSION Thm.eta_long_conversion THEN'
traytel@57890
    72
    asm_simp_tac (ss_only (pre_map_defs @
blanchet@58180
    73
        distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simps)
blanchet@57993
    74
      ctxt));
blanchet@56638
    75
blanchet@58180
    76
val size_o_map_simps = @{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@58180
    81
    asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simps) ctxt)) THEN
blanchet@56645
    82
  IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
blanchet@56638
    83
blanchet@58179
    84
fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
desharna@58578
    85
      fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_maps = ctor_rec_o_maps, ...}, fp_nesting_bnfs,
blanchet@58179
    86
      live_nesting_bnfs, ...} : fp_sugar) :: _) lthy0 =
blanchet@58179
    87
    let
blanchet@58179
    88
      val data = Data.get (Context.Proof lthy0);
blanchet@56651
    89
blanchet@58179
    90
      val Ts = map #T fp_sugars
blanchet@58179
    91
      val T_names = map (fst o dest_Type) Ts;
blanchet@58179
    92
      val nn = length Ts;
blanchet@56640
    93
blanchet@58179
    94
      val B_ify = Term.typ_subst_atomic (As ~~ Bs);
blanchet@56651
    95
desharna@58461
    96
      val recs = map (#co_rec o #fp_co_induct_sugar) fp_sugars;
desharna@58459
    97
      val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars;
blanchet@58179
    98
      val rec_Ts as rec_T1 :: _ = map fastype_of recs;
blanchet@58179
    99
      val rec_arg_Ts = binder_fun_types rec_T1;
blanchet@58179
   100
      val Cs = map body_type rec_Ts;
blanchet@58179
   101
      val Cs_rho = map (rpair HOLogic.natT) Cs;
blanchet@58179
   102
      val substCnatT = Term.subst_atomic_types Cs_rho;
blanchet@56651
   103
blanchet@58179
   104
      val f_Ts = map mk_to_natT As;
blanchet@58179
   105
      val f_TsB = map mk_to_natT Bs;
blanchet@58179
   106
      val num_As = length As;
blanchet@56651
   107
blanchet@58179
   108
      fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0);
blanchet@56651
   109
blanchet@58179
   110
      val f_names = variant_names num_As "f";
blanchet@58179
   111
      val fs = map2 (curry Free) f_names f_Ts;
blanchet@58179
   112
      val fsB = map2 (curry Free) f_names f_TsB;
blanchet@58179
   113
      val As_fs = As ~~ fs;
blanchet@56638
   114
blanchet@58179
   115
      val size_bs =
blanchet@58179
   116
        map ((fn base => Binding.qualify false base (Binding.name (prefix size_N base))) o
blanchet@58179
   117
          Long_Name.base_name) T_names;
blanchet@56638
   118
blanchet@58208
   119
      fun is_prod_C @{type_name prod} [_, T'] = member (op =) Cs T'
blanchet@58208
   120
        | is_prod_C _ _ = false;
blanchet@56651
   121
blanchet@58179
   122
      fun mk_size_of_typ (T as TFree _) =
blanchet@58179
   123
          pair (case AList.lookup (op =) As_fs T of
blanchet@58179
   124
              SOME f => f
blanchet@58179
   125
            | NONE => if member (op =) Cs T then Term.absdummy T (Bound 0) else mk_abs_zero_nat T)
blanchet@58179
   126
        | mk_size_of_typ (T as Type (s, Ts)) =
blanchet@58208
   127
          if is_prod_C s Ts then
blanchet@58179
   128
            pair (snd_const T)
blanchet@58179
   129
          else if exists (exists_subtype_in (As @ Cs)) Ts then
blanchet@58179
   130
            (case Symtab.lookup data s of
blanchet@58179
   131
              SOME (size_name, (_, size_o_maps)) =>
blanchet@58179
   132
              let
blanchet@58355
   133
                val (args, size_o_mapss') = fold_map mk_size_of_typ Ts [];
blanchet@58179
   134
                val size_const = Const (size_name, map fastype_of args ---> mk_to_natT T);
blanchet@58179
   135
              in
blanchet@58355
   136
                append (size_o_maps :: size_o_mapss')
blanchet@58179
   137
                #> pair (Term.list_comb (size_const, args))
blanchet@58179
   138
              end
blanchet@58179
   139
            | _ => pair (mk_abs_zero_nat T))
blanchet@58179
   140
          else
blanchet@58179
   141
            pair (mk_abs_zero_nat T);
blanchet@56651
   142
blanchet@58179
   143
      fun mk_size_of_arg t =
blanchet@58179
   144
        mk_size_of_typ (fastype_of t) #>> (fn s => substCnatT (betapply (s, t)));
blanchet@56638
   145
blanchet@58338
   146
      fun is_recursive_or_plain_case Ts =
blanchet@58338
   147
        exists (exists_subtype_in Cs) Ts orelse forall (not o exists_subtype_in As) Ts;
blanchet@58338
   148
blanchet@58338
   149
      (* We want the size function to enjoy the following properties:
blanchet@58338
   150
blanchet@58355
   151
          1. The size of a list should coincide with its length.
blanchet@58355
   152
          2. All the nonrecursive constructors of a type should have the same size.
blanchet@58355
   153
          3. Each constructor through which nested recursion takes place should count as at least
blanchet@58355
   154
             one in the generic size function.
blanchet@58355
   155
          4. The "size" function should be definable as "size_t (%_. 0) ... (%_. 0)", where "size_t"
blanchet@58355
   156
             is the generic function.
blanchet@58338
   157
blanchet@58355
   158
         This explains the somewhat convoluted logic ahead. *)
blanchet@58338
   159
blanchet@58338
   160
      val base_case =
blanchet@58338
   161
        if forall (is_recursive_or_plain_case o binder_types) rec_arg_Ts then HOLogic.zero
blanchet@58338
   162
        else HOLogic.Suc_zero;
blanchet@58338
   163
blanchet@58355
   164
      fun mk_size_arg rec_arg_T =
blanchet@58179
   165
        let
blanchet@58179
   166
          val x_Ts = binder_types rec_arg_T;
blanchet@58179
   167
          val m = length x_Ts;
blanchet@58179
   168
          val x_names = variant_names m "x";
blanchet@58179
   169
          val xs = map2 (curry Free) x_names x_Ts;
blanchet@58355
   170
          val (summands, size_o_mapss) =
blanchet@58355
   171
            fold_map mk_size_of_arg xs []
blanchet@58337
   172
            |>> remove (op =) HOLogic.zero;
blanchet@58179
   173
          val sum =
blanchet@58338
   174
            if null summands then base_case
blanchet@58179
   175
            else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
blanchet@56640
   176
        in
blanchet@58355
   177
          append size_o_mapss
blanchet@58355
   178
          #> pair (fold_rev Term.lambda (map substCnatT xs) sum)
blanchet@56640
   179
        end;
blanchet@56640
   180
blanchet@58355
   181
      fun mk_size_rhs recx =
blanchet@58355
   182
        fold_map mk_size_arg rec_arg_Ts
blanchet@58355
   183
        #>> (fn args => fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args)));
blanchet@58179
   184
blanchet@58179
   185
      val maybe_conceal_def_binding = Thm.def_binding
blanchet@58208
   186
        #> not (Config.get lthy0 bnf_note_all) ? Binding.conceal;
blanchet@58179
   187
blanchet@58355
   188
      val (size_rhss, nested_size_o_mapss) = fold_map mk_size_rhs recs [];
blanchet@58179
   189
      val size_Ts = map fastype_of size_rhss;
blanchet@58179
   190
blanchet@58355
   191
      val nested_size_o_maps_complete = forall (not o null) nested_size_o_mapss;
blanchet@58355
   192
      val nested_size_o_maps = fold (union Thm.eq_thm_prop) nested_size_o_mapss [];
blanchet@58355
   193
blanchet@58179
   194
      val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0
blanchet@58179
   195
        |> apfst split_list o fold_map2 (fn b => fn rhs =>
blanchet@58179
   196
            Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
blanchet@58179
   197
            #>> apsnd snd)
blanchet@58179
   198
          size_bs size_rhss
blanchet@58179
   199
        ||> `Local_Theory.restore;
blanchet@58179
   200
blanchet@58179
   201
      val phi = Proof_Context.export_morphism lthy1 lthy1';
blanchet@58179
   202
blanchet@58179
   203
      val size_defs = map (Morphism.thm phi) raw_size_defs;
blanchet@58179
   204
blanchet@58179
   205
      val size_consts0 = map (Morphism.term phi) raw_size_consts;
blanchet@58179
   206
      val size_consts = map2 retype_const_or_free size_Ts size_consts0;
blanchet@58179
   207
      val size_constsB = map (Term.map_types B_ify) size_consts;
blanchet@58179
   208
blanchet@58179
   209
      val zeros = map mk_abs_zero_nat As;
blanchet@58179
   210
blanchet@58179
   211
      val overloaded_size_rhss = map (fn c => Term.list_comb (c, zeros)) size_consts;
blanchet@58179
   212
      val overloaded_size_Ts = map fastype_of overloaded_size_rhss;
blanchet@58179
   213
      val overloaded_size_consts = map (curry Const @{const_name size}) overloaded_size_Ts;
blanchet@58179
   214
      val overloaded_size_def_bs =
blanchet@58179
   215
        map (maybe_conceal_def_binding o Binding.suffix_name "_overloaded") size_bs;
blanchet@58179
   216
blanchet@58179
   217
      fun define_overloaded_size def_b lhs0 rhs lthy =
blanchet@58179
   218
        let
blanchet@58179
   219
          val Free (c, _) = Syntax.check_term lthy lhs0;
blanchet@58179
   220
          val (thm, lthy') = lthy
blanchet@58179
   221
            |> Local_Theory.define ((Binding.name c, NoSyn), ((def_b, []), rhs))
blanchet@58179
   222
            |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
blanchet@58179
   223
          val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
blanchet@58179
   224
          val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
blanchet@58179
   225
        in (thm', lthy') end;
blanchet@58179
   226
blanchet@58179
   227
      val (overloaded_size_defs, lthy2) = lthy1
blanchet@58179
   228
        |> Local_Theory.background_theory_result
blanchet@58179
   229
          (Class.instantiation (T_names, map dest_TFree As, [HOLogic.class_size])
blanchet@58179
   230
           #> fold_map3 define_overloaded_size overloaded_size_def_bs overloaded_size_consts
blanchet@58179
   231
             overloaded_size_rhss
blanchet@58179
   232
           ##> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
blanchet@58179
   233
           ##> Local_Theory.exit_global);
blanchet@56638
   234
blanchet@58179
   235
      val size_defs' =
blanchet@58179
   236
        map (mk_unabs_def (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs;
blanchet@58179
   237
      val size_defs_unused_0 =
blanchet@58179
   238
        map (mk_unabs_def_unused_0 (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs;
blanchet@58179
   239
      val overloaded_size_defs' =
blanchet@58179
   240
        map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) overloaded_size_defs;
blanchet@58179
   241
blanchet@58179
   242
      val all_overloaded_size_defs = overloaded_size_defs @
blanchet@58179
   243
        (Spec_Rules.retrieve lthy0 @{const size ('a)}
blanchet@58179
   244
         |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm)));
blanchet@58179
   245
blanchet@58355
   246
      val nested_size_maps = map (mk_pointfull lthy2) nested_size_o_maps @ nested_size_o_maps;
blanchet@58179
   247
      val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs)
blanchet@58179
   248
        |> distinct Thm.eq_thm_prop;
blanchet@58179
   249
blanchet@58179
   250
      fun derive_size_simp size_def' simp0 =
blanchet@58179
   251
        (trans OF [size_def', simp0])
blanchet@58179
   252
        |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_ident id_def o_def
blanchet@58179
   253
          snd_conv} @ all_inj_maps @ nested_size_maps) lthy2)
blanchet@58179
   254
        |> fold_thms lthy2 size_defs_unused_0;
blanchet@58179
   255
blanchet@58179
   256
      fun derive_overloaded_size_simp overloaded_size_def' simp0 =
blanchet@58179
   257
        (trans OF [overloaded_size_def', simp0])
blanchet@58179
   258
        |> unfold_thms lthy2 @{thms add_0_left add_0_right}
blanchet@58179
   259
        |> fold_thms lthy2 all_overloaded_size_defs;
blanchet@58179
   260
blanchet@58179
   261
      val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss;
blanchet@58179
   262
      val size_simps = flat size_simpss;
blanchet@58179
   263
      val overloaded_size_simpss =
blanchet@58179
   264
        map2 (map o derive_overloaded_size_simp) overloaded_size_defs' size_simpss;
blanchet@58179
   265
      val size_thmss = map2 append size_simpss overloaded_size_simpss;
blanchet@58179
   266
blanchet@58179
   267
      val ABs = As ~~ Bs;
blanchet@58179
   268
      val g_names = variant_names num_As "g";
blanchet@58179
   269
      val gs = map2 (curry Free) g_names (map (op -->) ABs);
blanchet@58179
   270
blanchet@58179
   271
      val liveness = map (op <>) ABs;
blanchet@58179
   272
      val live_gs = AList.find (op =) (gs ~~ liveness) true;
blanchet@58179
   273
      val live = length live_gs;
blanchet@58179
   274
blanchet@58179
   275
      val maps0 = map map_of_bnf fp_bnfs;
blanchet@58179
   276
blanchet@58179
   277
      val (rec_o_map_thmss, size_o_map_thmss) =
blanchet@58179
   278
        if live = 0 then
blanchet@58179
   279
          `I (replicate nn [])
blanchet@58179
   280
        else
blanchet@58179
   281
          let
blanchet@58179
   282
            val pre_bnfs = map #pre_bnf fp_sugars;
blanchet@58179
   283
            val pre_map_defs = map map_def_of_bnf pre_bnfs;
blanchet@58179
   284
            val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
blanchet@58179
   285
            val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
desharna@58461
   286
            val rec_defs = map (#co_rec_def o #fp_co_induct_sugar) fp_sugars;
blanchet@58179
   287
blanchet@58179
   288
            val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
blanchet@57631
   289
blanchet@58179
   290
            val num_rec_args = length rec_arg_Ts;
blanchet@58179
   291
            val h_Ts = map B_ify rec_arg_Ts;
blanchet@58179
   292
            val h_names = variant_names num_rec_args "h";
blanchet@58179
   293
            val hs = map2 (curry Free) h_names h_Ts;
blanchet@58179
   294
            val hrecs = map (fn recx => Term.list_comb (Term.map_types B_ify recx, hs)) recs;
blanchet@58179
   295
blanchet@58179
   296
            val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) hrecs gmaps;
blanchet@58179
   297
blanchet@58179
   298
            val ABgs = ABs ~~ gs;
blanchet@58179
   299
blanchet@58179
   300
            fun mk_rec_arg_arg (x as Free (_, T)) =
blanchet@58179
   301
              let val U = B_ify T in
blanchet@58179
   302
                if T = U then x else build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U) $ x
blanchet@58179
   303
              end;
blanchet@58179
   304
blanchet@58179
   305
            fun mk_rec_o_map_arg rec_arg_T h =
blanchet@58179
   306
              let
blanchet@58179
   307
                val x_Ts = binder_types rec_arg_T;
blanchet@58179
   308
                val m = length x_Ts;
blanchet@58179
   309
                val x_names = variant_names m "x";
blanchet@58179
   310
                val xs = map2 (curry Free) x_names x_Ts;
blanchet@58179
   311
                val xs' = map mk_rec_arg_arg xs;
blanchet@58179
   312
              in
blanchet@58179
   313
                fold_rev Term.lambda xs (Term.list_comb (h, xs'))
blanchet@58179
   314
              end;
blanchet@58179
   315
blanchet@58179
   316
            fun mk_rec_o_map_rhs recx =
blanchet@58179
   317
              let val args = map2 mk_rec_o_map_arg rec_arg_Ts hs in
blanchet@58179
   318
                Term.list_comb (recx, args)
blanchet@58179
   319
              end;
blanchet@58179
   320
blanchet@58179
   321
            val rec_o_map_rhss = map mk_rec_o_map_rhs recs;
blanchet@58179
   322
blanchet@58179
   323
            val rec_o_map_goals =
blanchet@58179
   324
              map2 (fold_rev (fold_rev Logic.all) [gs, hs] o HOLogic.mk_Trueprop oo
blanchet@58179
   325
                curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss;
blanchet@58179
   326
            val rec_o_map_thms =
blanchet@58179
   327
              map3 (fn goal => fn rec_def => fn ctor_rec_o_map =>
blanchet@58179
   328
                  Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
blanchet@58179
   329
                    mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
blanchet@58179
   330
                      ctor_rec_o_map)
blanchet@58179
   331
                  |> Thm.close_derivation)
blanchet@58179
   332
                rec_o_map_goals rec_defs ctor_rec_o_maps;
blanchet@58179
   333
blanchet@58179
   334
            val size_o_map_conds =
blanchet@58179
   335
              if exists (can Logic.dest_implies o Thm.prop_of) nested_size_o_maps then
blanchet@58179
   336
                map (HOLogic.mk_Trueprop o mk_inj) live_gs
blanchet@58179
   337
              else
blanchet@58179
   338
                [];
blanchet@58179
   339
blanchet@58179
   340
            val fsizes = map (fn size_constB => Term.list_comb (size_constB, fsB)) size_constsB;
blanchet@58179
   341
            val size_o_map_lhss = map2 (curry HOLogic.mk_comp) fsizes gmaps;
blanchet@57631
   342
blanchet@58179
   343
            val fgs = map2 (fn fB => fn g as Free (_, Type (_, [A, B])) =>
blanchet@58179
   344
              if A = B then fB else HOLogic.mk_comp (fB, g)) fsB gs;
blanchet@58179
   345
            val size_o_map_rhss = map (fn c => Term.list_comb (c, fgs)) size_consts;
blanchet@58179
   346
blanchet@58179
   347
            val size_o_map_goals =
blanchet@58179
   348
              map2 (fold_rev (fold_rev Logic.all) [fsB, gs] o
blanchet@58179
   349
                curry Logic.list_implies size_o_map_conds o HOLogic.mk_Trueprop oo
blanchet@58179
   350
                curry HOLogic.mk_eq) size_o_map_lhss size_o_map_rhss;
blanchet@58179
   351
blanchet@58179
   352
            val size_o_map_thmss =
blanchet@58355
   353
              if nested_size_o_maps_complete then
blanchet@58355
   354
                map3 (fn goal => fn size_def => fn rec_o_map =>
blanchet@58355
   355
                    Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
blanchet@58355
   356
                      mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
blanchet@58355
   357
                    |> Thm.close_derivation
blanchet@58355
   358
                    |> single)
blanchet@58355
   359
                  size_o_map_goals size_defs rec_o_map_thms
blanchet@58355
   360
              else
blanchet@58355
   361
                replicate nn [];
blanchet@58179
   362
          in
blanchet@58179
   363
            (map single rec_o_map_thms, size_o_map_thmss)
blanchet@58179
   364
          end;
blanchet@58179
   365
blanchet@58335
   366
      (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *)
blanchet@58335
   367
      val code_attrs = Code.add_default_eqn_attrib;
blanchet@58335
   368
blanchet@58179
   369
      val massage_multi_notes =
blanchet@58179
   370
        maps (fn (thmN, thmss, attrs) =>
blanchet@58179
   371
          map2 (fn T_name => fn thms =>
blanchet@58179
   372
              ((Binding.qualify true (Long_Name.base_name T_name) (Binding.name thmN), attrs),
blanchet@58179
   373
               [(thms, [])]))
blanchet@58179
   374
            T_names thmss)
blanchet@58179
   375
        #> filter_out (null o fst o hd o snd);
blanchet@58179
   376
blanchet@58179
   377
      val notes =
blanchet@58179
   378
        [(rec_o_mapN, rec_o_map_thmss, []),
blanchet@58335
   379
         (sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs),
blanchet@58179
   380
         (size_o_mapN, size_o_map_thmss, [])]
blanchet@58179
   381
        |> massage_multi_notes;
blanchet@58179
   382
blanchet@58179
   383
      val (noted, lthy3) =
blanchet@58179
   384
        lthy2
blanchet@58179
   385
        |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps)
blanchet@58179
   386
        |> Local_Theory.notes notes;
blanchet@58179
   387
blanchet@58179
   388
      val phi0 = substitute_noted_thm noted;
blanchet@58179
   389
    in
blanchet@58179
   390
      lthy3
blanchet@58179
   391
      |> Local_Theory.declaration {syntax = false, pervasive = true}
blanchet@58179
   392
        (fn phi => Data.map (fold2 (fn T_name => fn Const (size_name, _) =>
blanchet@58179
   393
             Symtab.update (T_name, (size_name,
blanchet@58179
   394
               pairself (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_o_map_thmss))))
blanchet@58179
   395
           T_names size_consts))
blanchet@58179
   396
    end
blanchet@58179
   397
  | generate_datatype_size _ lthy = lthy;
blanchet@58179
   398
blanchet@58191
   399
val _ = Theory.setup (fp_sugars_interpretation size_plugin
blanchet@58186
   400
  (map_local_theory o generate_datatype_size) generate_datatype_size);
blanchet@56638
   401
blanchet@56638
   402
end;