generate size instances for new-style datatypes
authorblanchet
Wed Apr 23 10:23:26 2014 +0200 (2014-04-23)
changeset 56638092a306bcc3d
parent 56637 d1d55f1bbc8a
child 56639 c9d6b581bd3b
generate size instances for new-style datatypes
src/HOL/BNF_LFP.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_util.ML
     1.1 --- a/src/HOL/BNF_LFP.thy	Wed Apr 23 10:23:26 2014 +0200
     1.2 +++ b/src/HOL/BNF_LFP.thy	Wed Apr 23 10:23:26 2014 +0200
     1.3 @@ -186,12 +186,78 @@
     1.4  lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
     1.5    by (rule ssubst)
     1.6  
     1.7 +lemma snd_o_convol: "(snd \<circ> (\<lambda>x. (f x, g x))) = g"
     1.8 +  by (rule ext) simp
     1.9 +
    1.10 +lemma inj_on_convol_id: "inj_on (\<lambda>x. (x, f x)) X"
    1.11 +  unfolding inj_on_def by simp
    1.12 +
    1.13  ML_file "Tools/BNF/bnf_lfp_util.ML"
    1.14  ML_file "Tools/BNF/bnf_lfp_tactics.ML"
    1.15  ML_file "Tools/BNF/bnf_lfp.ML"
    1.16  ML_file "Tools/BNF/bnf_lfp_compat.ML"
    1.17  ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
    1.18 +ML_file "Tools/BNF/bnf_lfp_size.ML"
    1.19  
    1.20  hide_fact (open) id_transfer
    1.21  
    1.22 +datatype_new x = X nat
    1.23 +thm x.size
    1.24 +
    1.25 +datatype_new 'a l = N | C 'a "'a l"
    1.26 +thm l.size
    1.27 +thm l.size_map
    1.28 +thm size_l_def size_l_overloaded_def
    1.29 +
    1.30 +datatype_new
    1.31 +  'a tl = TN | TC "'a mt" "'a tl" and
    1.32 +  'a mt = MT 'a "'a tl"
    1.33 +
    1.34 +thm size_tl_def size_tl_overloaded_def
    1.35 +thm size_mt_def size_mt_overloaded_def
    1.36 +
    1.37 +datatype_new 'a t = T 'a "'a t l"
    1.38 +thm t.size
    1.39 +
    1.40 +lemma size_l_cong: "(ALL x : set_l t. f x = g x) --> size_l f t = size_l g t"
    1.41 +  apply (induct_tac t)
    1.42 +  apply (simp only: l.size simp_thms)
    1.43 +  apply (simp add: l.set l.size simp_thms)
    1.44 +  done
    1.45 +
    1.46 +lemma t_size_map_t: "size_t g (map_t f t) = size_t (g \<circ> f) t"
    1.47 +  apply (rule t.induct)
    1.48 +  apply (simp_all only: t.map t.size comp_def l.size_map)
    1.49 +  apply (auto intro: size_l_cong)
    1.50 +  apply (subst size_l_cong[rule_format], assumption)
    1.51 +  apply (rule refl)
    1.52 +  done
    1.53 +
    1.54 +
    1.55 +thm t.size
    1.56 +
    1.57 +lemmas size_t_def' =
    1.58 +  size_t_def[THEN meta_eq_to_obj_eq, THEN fun_cong, THEN fun_cong]
    1.59 +
    1.60 +thm trans[OF size_t_def' t.rec(1), unfolded l.size_map snd_o_convol, folded size_t_def']
    1.61 +
    1.62 +lemma "size_t f (T x ts) = f x + size_l (size_t f) ts + Suc 0"
    1.63 +  unfolding size_t_def t.rec l.size_map snd_o_convol
    1.64 +  by rule
    1.65 +
    1.66 +
    1.67 +lemma "       (\<And>x2aa. x2aa \<in> set_l x2a \<Longrightarrow>
    1.68 +                size_t f1 (map_t g1 x2aa) = size_t (f1 \<circ> g1) x2aa) \<Longrightarrow>
    1.69 +       f1 (g1 x1a) +
    1.70 +       size_l snd (map_l (\<lambda>t. (t, size_t f1 t)) (map_l (map_t g1) x2a)) +
    1.71 +       Suc 0 =
    1.72 +       f1 (g1 x1a) + size_l snd (map_l (\<lambda>t. (t, size_t (\<lambda>x1. f1 (g1 x1)) t)) x2a) +
    1.73 +       Suc 0"
    1.74 +apply (simp only: l.size_map comp_def snd_conv t.size_map snd_o_convol)
    1.75 +
    1.76 +thm size_t_def size_t_overloaded_def
    1.77 +
    1.78 +xdatatype_new ('a, 'b, 'c) x = XN 'c | XC 'a "('a, 'b, 'c) x"
    1.79 +thm size_x_def size_x_overloaded_def
    1.80 +
    1.81  end
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Apr 23 10:23:26 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Apr 23 10:23:26 2014 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4  sig
     2.5    type fp_sugar =
     2.6      {T: typ,
     2.7 +     BT: typ,
     2.8       X: typ,
     2.9       fp: BNF_Util.fp_kind,
    2.10       fp_res_index: int,
    2.11 @@ -123,6 +124,7 @@
    2.12  
    2.13  type fp_sugar =
    2.14    {T: typ,
    2.15 +   BT: typ,
    2.16     X: typ,
    2.17     fp: fp_kind,
    2.18     fp_res_index: int,
    2.19 @@ -1086,6 +1088,7 @@
    2.20      val dtors = map (mk_dtor As) dtors0;
    2.21  
    2.22      val fpTs = map (domain_type o fastype_of) dtors;
    2.23 +    val fpBTs = map B_ify fpTs;
    2.24  
    2.25      fun massage_simple_notes base =
    2.26        filter_out (null o #2)
    2.27 @@ -1215,7 +1218,7 @@
    2.28                  end;
    2.29  
    2.30                val cxIns = map2 (mk_cIn ctor) ks xss;
    2.31 -              val cyIns = map2 (mk_cIn (map_types B_ify ctor)) ks yss;
    2.32 +              val cyIns = map2 (mk_cIn (Term.map_types B_ify ctor)) ks yss;
    2.33  
    2.34                fun mk_map_thm ctr_def' cxIn =
    2.35                  fold_thms lthy [ctr_def']
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 23 10:23:26 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 23 10:23:26 2014 +0200
     3.3 @@ -25,7 +25,7 @@
     3.4  open BNF_FP_N2M_Tactics
     3.5  
     3.6  fun force_typ ctxt T =
     3.7 -  map_types Type_Infer.paramify_vars
     3.8 +  Term.map_types Type_Infer.paramify_vars
     3.9    #> Type.constraint T
    3.10    #> Syntax.check_term ctxt
    3.11    #> singleton (Variable.polymorphic ctxt);
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Apr 23 10:23:26 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Apr 23 10:23:26 2014 +0200
     4.3 @@ -276,10 +276,11 @@
     4.4  
     4.5          fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec maps
     4.6              co_inducts co_rec_thms disc_corec_thms sel_corec_thmss rel_injects =
     4.7 -          {T = T, X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
     4.8 -           absT_info = absT_info, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs,
     4.9 -           ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
    4.10 -           maps = maps, common_co_inducts = common_co_inducts, co_inducts = co_inducts,
    4.11 +          {T = T, BT = Term.dummyT (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res,
    4.12 +           fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info, nested_bnfs = nested_bnfs,
    4.13 +           nesting_bnfs = nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs,
    4.14 +           ctr_sugar = ctr_sugar, co_rec = co_rec, maps = maps,
    4.15 +           common_co_inducts = common_co_inducts, co_inducts = co_inducts,
    4.16             co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
    4.17             sel_co_recss = sel_corec_thmss, rel_injects = rel_injects}
    4.18            |> morph_fp_sugar phi;
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Apr 23 10:23:26 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Apr 23 10:23:26 2014 +0200
     5.3 @@ -3,7 +3,7 @@
     5.4      Author:     Andrei Popescu, TU Muenchen
     5.5      Copyright   2012
     5.6  
     5.7 -Datatype construction.
     5.8 +New-style datatype construction.
     5.9  *)
    5.10  
    5.11  signature BNF_LFP =
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Apr 23 10:23:26 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Apr 23 10:23:26 2014 +0200
     6.3 @@ -3,7 +3,7 @@
     6.4      Author:     Jasmin Blanchette, TU Muenchen
     6.5      Copyright   2013
     6.6  
     6.7 -Recursor sugar ("primrec").
     6.8 +New-style recursor sugar ("primrec").
     6.9  *)
    6.10  
    6.11  signature BNF_LFP_REC_SUGAR =
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Wed Apr 23 10:23:26 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Wed Apr 23 10:23:26 2014 +0200
     7.3 @@ -3,7 +3,7 @@
     7.4      Author:     Jasmin Blanchette, TU Muenchen
     7.5      Copyright   2013
     7.6  
     7.7 -More recursor sugar.
     7.8 +More new-style recursor sugar.
     7.9  *)
    7.10  
    7.11  structure BNF_LFP_Rec_Sugar_More : sig end =
    7.12 @@ -141,14 +141,14 @@
    7.13          in
    7.14            if ctr_pos >= 0 then
    7.15              if d = SOME ~1 andalso length vs = ctr_pos then
    7.16 -              list_comb (permute_args ctr_pos (snd_const pT), vs)
    7.17 +              Term.list_comb (permute_args ctr_pos (snd_const pT), vs)
    7.18              else if length vs > ctr_pos andalso is_some d andalso
    7.19                  d = try (fn Bound n => n) (nth vs ctr_pos) then
    7.20 -              list_comb (snd_const pT $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs))
    7.21 +              Term.list_comb (snd_const pT $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs))
    7.22              else
    7.23                raise PRIMREC ("recursive call not directly applied to constructor argument", [t])
    7.24            else
    7.25 -            list_comb (u, map (subst (d |> d = SOME ~1 ? K NONE)) vs)
    7.26 +            Term.list_comb (u, map (subst (d |> d = SOME ~1 ? K NONE)) vs)
    7.27          end
    7.28    in
    7.29      subst (SOME ~1)
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Apr 23 10:23:26 2014 +0200
     8.3 @@ -0,0 +1,241 @@
     8.4 +(*  Title:      HOL/Tools/BNF/bnf_lfp_size.ML
     8.5 +    Author:     Jasmin Blanchette, TU Muenchen
     8.6 +    Copyright   2014
     8.7 +
     8.8 +Generation of size functions for new-style datatypes.
     8.9 +*)
    8.10 +
    8.11 +structure BNF_LFP_Size : sig end =
    8.12 +struct
    8.13 +
    8.14 +open BNF_Util
    8.15 +open BNF_Def
    8.16 +open BNF_FP_Def_Sugar
    8.17 +
    8.18 +val size_N = "size_"
    8.19 +
    8.20 +val sizeN = "size"
    8.21 +val size_mapN = "size_map"
    8.22 +
    8.23 +structure Data = Theory_Data
    8.24 +(
    8.25 +  type T = (string * (thm list * thm list)) Symtab.table;
    8.26 +  val empty = Symtab.empty;
    8.27 +  val extend = I
    8.28 +  fun merge data = Symtab.merge (K true) data;
    8.29 +);
    8.30 +
    8.31 +val zero_nat = @{const zero_class.zero (nat)};
    8.32 +
    8.33 +fun mk_plus_nat (t1, t2) = Const (@{const_name Groups.plus},
    8.34 +  HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
    8.35 +
    8.36 +fun mk_to_natT T = T --> HOLogic.natT;
    8.37 +
    8.38 +fun mk_abs_zero_nat T = Term.absdummy T zero_nat;
    8.39 +
    8.40 +fun generate_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs),
    8.41 +    fp_res = {bnfs = fp_bnfs, ...}, common_co_inducts = common_inducts, ...} : fp_sugar) :: _) thy =
    8.42 +  let
    8.43 +    val data = Data.get thy;
    8.44 +
    8.45 +    val Ts = map #T fp_sugars
    8.46 +    val T_names = map (fst o dest_Type) Ts;
    8.47 +    val nn = length Ts;
    8.48 +
    8.49 +    val B_ify = Term.typ_subst_atomic (As ~~ Bs);
    8.50 +
    8.51 +    val recs = map #co_rec fp_sugars;
    8.52 +    val rec_thmss = map #co_rec_thms fp_sugars;
    8.53 +    val rec_Ts = map fastype_of recs;
    8.54 +    val Cs = map body_type rec_Ts;
    8.55 +    val Cs_rho = map (rpair HOLogic.natT) Cs;
    8.56 +    val substCT = Term.subst_atomic_types Cs_rho;
    8.57 +
    8.58 +    val f_Ts = map mk_to_natT As;
    8.59 +    val f_TsB = map mk_to_natT Bs;
    8.60 +    val num_As = length As;
    8.61 +
    8.62 +    val f_names = map (prefix "f" o string_of_int) (1 upto num_As);
    8.63 +    val fs = map2 (curry Free) f_names f_Ts;
    8.64 +    val fsB = map2 (curry Free) f_names f_TsB;
    8.65 +    val As_fs = As ~~ fs;
    8.66 +
    8.67 +    val gen_size_names = map (Long_Name.map_base_name (prefix size_N)) T_names;
    8.68 +
    8.69 +    fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T'
    8.70 +      | is_pair_C _ _ = false;
    8.71 +
    8.72 +    fun mk_size_of_typ (T as TFree _) =
    8.73 +        pair (case AList.lookup (op =) As_fs T of
    8.74 +            SOME f => f
    8.75 +          | NONE => if member (op =) Cs T then Term.absdummy T (Bound 0) else mk_abs_zero_nat T)
    8.76 +      | mk_size_of_typ (T as Type (s, Ts)) =
    8.77 +        if is_pair_C s Ts then
    8.78 +          pair (snd_const T)
    8.79 +        else if exists (exists_subtype_in As) Ts then
    8.80 +          (case Symtab.lookup data s of
    8.81 +            SOME (gen_size_name, (_, gen_size_maps)) =>
    8.82 +            let
    8.83 +              val (args, gen_size_mapss') = split_list (map (fn T => mk_size_of_typ T []) Ts);
    8.84 +              val gen_size_const = Const (gen_size_name, map fastype_of args ---> mk_to_natT T);
    8.85 +            in
    8.86 +              fold (union Thm.eq_thm) (gen_size_maps :: gen_size_mapss')
    8.87 +              #> pair (Term.list_comb (gen_size_const, args))
    8.88 +            end
    8.89 +          | NONE => pair (mk_abs_zero_nat T))
    8.90 +        else
    8.91 +          pair (mk_abs_zero_nat T);
    8.92 +
    8.93 +    fun mk_size_of_arg t =
    8.94 +      mk_size_of_typ (fastype_of t) #>> (fn s => substCT (betapply (s, t)));
    8.95 +
    8.96 +    fun mk_gen_size_arg arg_T gen_size_maps =
    8.97 +      let
    8.98 +        val x_Ts = binder_types arg_T;
    8.99 +        val m = length x_Ts;
   8.100 +        val x_names = map (prefix "x" o string_of_int) (1 upto m);
   8.101 +        val xs = map2 (curry Free) x_names x_Ts;
   8.102 +        val (summands, gen_size_maps') =
   8.103 +          fold_map mk_size_of_arg xs gen_size_maps
   8.104 +          |>> remove (op =) zero_nat;
   8.105 +        val sum =
   8.106 +          if null summands then HOLogic.zero
   8.107 +          else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
   8.108 +      in
   8.109 +        (fold_rev Term.lambda (map substCT xs) sum, gen_size_maps')
   8.110 +      end;
   8.111 +
   8.112 +    fun mk_gen_size_rhs rec_T recx gen_size_maps =
   8.113 +      let
   8.114 +        val arg_Ts = binder_fun_types rec_T;
   8.115 +        val (args, gen_size_maps') = fold_map mk_gen_size_arg arg_Ts gen_size_maps;
   8.116 +      in
   8.117 +        (fold_rev Term.lambda fs (Term.list_comb (substCT recx, args)), gen_size_maps')
   8.118 +      end;
   8.119 +
   8.120 +    fun mk_def_binding f = Binding.conceal o Binding.name o Thm.def_name o f o Long_Name.base_name;
   8.121 +
   8.122 +    val (gen_size_rhss, nested_gen_size_maps) = fold_map2 mk_gen_size_rhs rec_Ts recs [];
   8.123 +    val gen_size_Ts = map fastype_of gen_size_rhss;
   8.124 +    val gen_size_consts = map2 (curry Const) gen_size_names gen_size_Ts;
   8.125 +    val gen_size_constsB = map (Term.map_types B_ify) gen_size_consts;
   8.126 +    val gen_size_def_bs = map (mk_def_binding I) gen_size_names;
   8.127 +
   8.128 +    val (gen_size_defs, thy2) =
   8.129 +      thy
   8.130 +      |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s), T, NoSyn))
   8.131 +        (gen_size_names ~~ gen_size_Ts))
   8.132 +      |> Global_Theory.add_defs false (map Thm.no_attributes (gen_size_def_bs ~~
   8.133 +        map Logic.mk_equals (gen_size_consts ~~ gen_size_rhss)));
   8.134 +
   8.135 +    val zeros = map mk_abs_zero_nat As;
   8.136 +
   8.137 +    val spec_size_rhss = map (fn c => Term.list_comb (c, zeros)) gen_size_consts;
   8.138 +    val spec_size_Ts = map fastype_of spec_size_rhss;
   8.139 +    val spec_size_consts = map (curry Const @{const_name size}) spec_size_Ts;
   8.140 +    val spec_size_def_bs = map (mk_def_binding (suffix "_overloaded")) gen_size_names;
   8.141 +
   8.142 +    fun define_spec_size def_b lhs0 rhs lthy =
   8.143 +      let
   8.144 +        val Free (c, _) = Syntax.check_term lthy lhs0;
   8.145 +        val (thm, lthy') = lthy
   8.146 +          |> Local_Theory.define ((Binding.name c, NoSyn), ((def_b, []), rhs))
   8.147 +          |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
   8.148 +        val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
   8.149 +        val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
   8.150 +      in (thm', lthy') end;
   8.151 +
   8.152 +    val (spec_size_defs, thy3) = thy2
   8.153 +      |> Class.instantiation (T_names, map dest_TFree As, [HOLogic.class_size])
   8.154 +      |> fold_map3 define_spec_size spec_size_def_bs spec_size_consts spec_size_rhss
   8.155 +      ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   8.156 +      ||> Local_Theory.exit_global;
   8.157 +
   8.158 +    val thy3_ctxt = Proof_Context.init_global thy3;
   8.159 +
   8.160 +    val gen_size_defs' =
   8.161 +      map (mk_unabs_def (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) gen_size_defs;
   8.162 +    val spec_size_defs' =
   8.163 +      map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) spec_size_defs;
   8.164 +
   8.165 +    fun derive_size_simp unfolds folds size_def' simp0 =
   8.166 +      fold_thms thy3_ctxt folds (unfold_thms thy3_ctxt unfolds (trans OF [size_def', simp0]));
   8.167 +    val derive_gen_size_simp =
   8.168 +      derive_size_simp (@{thm snd_o_convol} :: nested_gen_size_maps) gen_size_defs';
   8.169 +    val derive_spec_size_simp = derive_size_simp @{thms add_0_left add_0_right} spec_size_defs';
   8.170 +
   8.171 +    val gen_size_simpss = map2 (map o derive_gen_size_simp) gen_size_defs' rec_thmss;
   8.172 +    val gen_size_simps = flat gen_size_simpss;
   8.173 +    val spec_size_simpss = map2 (map o derive_spec_size_simp) spec_size_defs' gen_size_simpss;
   8.174 +
   8.175 +    val ABs = As ~~ Bs;
   8.176 +    val g_names = map (prefix "g" o string_of_int) (1 upto num_As);
   8.177 +    val gs = map2 (curry Free) g_names (map (op -->) ABs);
   8.178 +
   8.179 +    val liveness = map (op <>) ABs;
   8.180 +    val live_gs = AList.find (op =) (gs ~~ liveness) true;
   8.181 +    val live = length live_gs;
   8.182 +
   8.183 +    val u_names = map (prefix "u" o string_of_int) (1 upto nn);
   8.184 +    val us = map2 (curry Free) u_names Ts;
   8.185 +
   8.186 +    val maps0 = map map_of_bnf fp_bnfs;
   8.187 +    val map_thms = maps #maps fp_sugars;
   8.188 +
   8.189 +    fun mk_gen_size_map_tac ctxt =
   8.190 +      HEADGOAL (rtac (co_induct_of common_inducts)) THEN
   8.191 +      ALLGOALS (asm_simp_tac (ss_only (o_apply :: map_thms @ gen_size_simps) ctxt));
   8.192 +
   8.193 +    val gen_size_map_thmss =
   8.194 +      if live = 0 then
   8.195 +        replicate nn []
   8.196 +      else if null nested_gen_size_maps then
   8.197 +        let
   8.198 +          val xgmaps =
   8.199 +            map2 (fn map0 => fn u => Term.list_comb (mk_map live As Bs map0, live_gs) $ u) maps0 us;
   8.200 +          val fsizes =
   8.201 +            map (fn gen_size_constB => Term.list_comb (gen_size_constB, fsB)) gen_size_constsB;
   8.202 +          val lhss = map2 (curry (op $)) fsizes xgmaps;
   8.203 +
   8.204 +          val fgs = map2 (fn fB => fn g as Free (_, Type (_, [A, B])) =>
   8.205 +            if A = B then fB else HOLogic.mk_comp (fB, g)) fsB gs;
   8.206 +          val rhss = map2 (fn gen_size_const => fn u => Term.list_comb (gen_size_const, fgs) $ u)
   8.207 +            gen_size_consts us;
   8.208 +
   8.209 +          val goal = Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) lhss rhss)
   8.210 +            |> HOLogic.mk_Trueprop;
   8.211 +        in
   8.212 +          Goal.prove_global thy3 [] [] goal (mk_gen_size_map_tac o #context)
   8.213 +          |> Thm.close_derivation
   8.214 +          |> conj_dests nn
   8.215 +          |> map single
   8.216 +        end
   8.217 +      else
   8.218 +        (* TODO: implement general case, with nesting of datatypes that themselves nest other
   8.219 +           types *)
   8.220 +        replicate nn [];
   8.221 +
   8.222 +    val (_, thy4) = thy3
   8.223 +      |> fold_map3 (fn T_name => fn size_simps => fn gen_size_map_thms =>
   8.224 +          let val qualify = Binding.qualify true (Long_Name.base_name T_name) in
   8.225 +            Global_Theory.note_thmss ""
   8.226 +              ([((qualify (Binding.name sizeN),
   8.227 +                   [Simplifier.simp_add, Nitpick_Simps.add, Thm.declaration_attribute
   8.228 +                      (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
   8.229 +                 [(size_simps, [])]),
   8.230 +                ((qualify (Binding.name size_mapN), []), [(gen_size_map_thms, [])])]
   8.231 +               |> filter_out (forall (null o fst) o snd))
   8.232 +          end)
   8.233 +        T_names (map2 append gen_size_simpss spec_size_simpss) gen_size_map_thmss
   8.234 +      ||> Spec_Rules.add_global Spec_Rules.Equational (gen_size_consts, gen_size_simps);
   8.235 +  in
   8.236 +    thy4
   8.237 +    |> Data.map (fold2 (fn T_name => fn gen_size_name =>
   8.238 +        Symtab.update_new (T_name, (gen_size_name, (gen_size_simps, flat gen_size_map_thmss))))
   8.239 +      T_names gen_size_names)
   8.240 +  end;
   8.241 +
   8.242 +val _ = Theory.setup (fp_sugar_interpretation generate_size);
   8.243 +
   8.244 +end;
     9.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Apr 23 10:23:26 2014 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Apr 23 10:23:26 2014 +0200
     9.3 @@ -3,7 +3,7 @@
     9.4      Author:     Andrei Popescu, TU Muenchen
     9.5      Copyright   2012
     9.6  
     9.7 -Tactics for the datatype construction.
     9.8 +Tactics for the new-style datatype construction.
     9.9  *)
    9.10  
    9.11  signature BNF_LFP_TACTICS =
    10.1 --- a/src/HOL/Tools/BNF/bnf_lfp_util.ML	Wed Apr 23 10:23:26 2014 +0200
    10.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_util.ML	Wed Apr 23 10:23:26 2014 +0200
    10.3 @@ -3,7 +3,7 @@
    10.4      Author:     Jasmin Blanchette, TU Muenchen
    10.5      Copyright   2012
    10.6  
    10.7 -Library for the datatype construction.
    10.8 +Library for the new-style datatype construction.
    10.9  *)
   10.10  
   10.11  signature BNF_LFP_UTIL =