tuned variable names
authorblanchet
Fri Jun 27 10:11:44 2014 +0200 (2014-06-27)
changeset 573975004aca20821
parent 57396 42eede5610a9
child 57398 882091eb1e9a
tuned variable names
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_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.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
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Jun 27 10:11:44 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Jun 27 10:11:44 2014 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5    val flat_corec_preds_predsss_gettersss: 'a list -> 'a list list list -> 'a list list list ->
     1.6      'a list
     1.7 -  val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
     1.8 +  val nesting_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
     1.9  
    1.10    type lfp_sugar_thms =
    1.11      (thm list * thm * Args.src list) * (thm list list * Args.src list)
    1.12 @@ -142,20 +142,21 @@
    1.13    #> fp = Least_FP ? generate_lfp_size fp_sugars
    1.14    #> Local_Theory.background_theory (FP_Sugar_Interpretation.data fp_sugars);
    1.15  
    1.16 -fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
    1.17 +fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res
    1.18      ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss common_co_inducts co_inductss
    1.19      co_rec_thmss disc_co_recss sel_co_recsss rel_injectss rel_distinctss =
    1.20    let
    1.21      val fp_sugars =
    1.22        map_index (fn (kk, T) =>
    1.23          {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
    1.24 -         pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, nested_bnfs = nested_bnfs,
    1.25 -         nesting_bnfs = nesting_bnfs, ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk,
    1.26 -         ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk,
    1.27 -         maps = nth mapss kk, common_co_inducts = common_co_inducts,
    1.28 -         co_inducts = nth co_inductss kk, co_rec_thms = nth co_rec_thmss kk,
    1.29 -         disc_co_recs = nth disc_co_recss kk, sel_co_recss = nth sel_co_recsss kk,
    1.30 -         rel_injects = nth rel_injectss kk, rel_distincts = nth rel_distinctss kk}) Ts
    1.31 +         pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk,
    1.32 +         fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
    1.33 +         ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk,
    1.34 +         co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk, maps = nth mapss kk,
    1.35 +         common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
    1.36 +         co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk,
    1.37 +         sel_co_recss = nth sel_co_recsss kk, rel_injects = nth rel_injectss kk,
    1.38 +         rel_distincts = nth rel_distinctss kk}) Ts
    1.39    in
    1.40      register_fp_sugars fp_sugars
    1.41    end;
    1.42 @@ -254,7 +255,7 @@
    1.43  fun rel_binding_of_spec ((_, (_, b)), _) = b;
    1.44  fun sel_default_eqs_of_spec (_, ts) = ts;
    1.45  
    1.46 -fun add_nesty_bnf_names Us =
    1.47 +fun add_nesting_bnf_names Us =
    1.48    let
    1.49      fun add (Type (s, Ts)) ss =
    1.50          let val (needs, ss') = fold_map add Ts ss in
    1.51 @@ -263,8 +264,8 @@
    1.52        | add T ss = (member (op =) Us T, ss);
    1.53    in snd oo add end;
    1.54  
    1.55 -fun nesty_bnfs ctxt ctr_Tsss Us =
    1.56 -  map_filter (bnf_of ctxt) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_Tsss []);
    1.57 +fun nesting_bnfs ctxt ctr_Tsss Us =
    1.58 +  map_filter (bnf_of ctxt) (fold (fold (fold (add_nesting_bnf_names Us))) ctr_Tsss []);
    1.59  
    1.60  fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
    1.61  
    1.62 @@ -444,8 +445,8 @@
    1.63    end;
    1.64  
    1.65  fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
    1.66 -    nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses
    1.67 -    ctrss ctr_defss recs rec_defs lthy =
    1.68 +    live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions
    1.69 +    abs_inverses ctrss ctr_defss recs rec_defs lthy =
    1.70    let
    1.71      val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
    1.72  
    1.73 @@ -455,9 +456,10 @@
    1.74  
    1.75      val pre_map_defs = map map_def_of_bnf pre_bnfs;
    1.76      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
    1.77 -    val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
    1.78 -    val nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
    1.79 -    val nested_set_maps = maps set_map_of_bnf nested_bnfs;
    1.80 +    val live_nesting_map_idents =
    1.81 +      map (unfold_thms lthy [id_def] o map_id0_of_bnf) live_nesting_bnfs;
    1.82 +    val fp_nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) fp_nesting_bnfs;
    1.83 +    val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs;
    1.84  
    1.85      val fp_b_names = map base_name_of_typ fpTs;
    1.86  
    1.87 @@ -482,7 +484,7 @@
    1.88          (T_name, map mk_set Us)
    1.89        end;
    1.90  
    1.91 -    val setss_nested = map mk_sets_nested nested_bnfs;
    1.92 +    val setss_nested = map mk_sets_nested fp_nesting_bnfs;
    1.93  
    1.94      val (induct_thms, induct_thm) =
    1.95        let
    1.96 @@ -541,7 +543,7 @@
    1.97          val thm =
    1.98            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    1.99              mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' fp_abs_inverses
   1.100 -              abs_inverses nested_set_maps pre_set_defss)
   1.101 +              abs_inverses fp_nesting_set_maps pre_set_defss)
   1.102            |> singleton (Proof_Context.export names_lthy lthy)
   1.103            (* for "datatype_realizer.ML": *)
   1.104            |> Thm.name_derivation (fst (dest_Type (hd fpTs)) ^ Long_Name.separator ^
   1.105 @@ -580,8 +582,8 @@
   1.106          val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
   1.107          val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss;
   1.108  
   1.109 -        val tacss =
   1.110 -          map4 (map ooo mk_rec_tac pre_map_defs (nested_map_idents @ nesting_map_idents) rec_defs)
   1.111 +        val tacss = map4 (map ooo
   1.112 +              mk_rec_tac pre_map_defs (fp_nesting_map_idents @ live_nesting_map_idents) rec_defs)
   1.113              ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss;
   1.114  
   1.115          fun prove goal tac =
   1.116 @@ -721,8 +723,8 @@
   1.117    end;
   1.118  
   1.119  fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
   1.120 -    dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
   1.121 -    mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
   1.122 +    dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
   1.123 +    kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
   1.124      corecs corec_defs export_args lthy =
   1.125    let
   1.126      fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec =
   1.127 @@ -734,8 +736,9 @@
   1.128  
   1.129      val pre_map_defs = map map_def_of_bnf pre_bnfs;
   1.130      val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
   1.131 -    val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
   1.132 -    val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
   1.133 +    val live_nesting_map_idents =
   1.134 +      map (unfold_thms lthy [id_def] o map_id0_of_bnf) live_nesting_bnfs;
   1.135 +    val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs;
   1.136  
   1.137      val fp_b_names = map base_name_of_typ fpTs;
   1.138  
   1.139 @@ -806,8 +809,8 @@
   1.140  
   1.141          fun prove dtor_coinduct' goal =
   1.142            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   1.143 -            mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses
   1.144 -              abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss)
   1.145 +            mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs
   1.146 +              fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss)
   1.147            |> singleton (Proof_Context.export names_lthy lthy)
   1.148            |> Thm.close_derivation;
   1.149  
   1.150 @@ -852,7 +855,7 @@
   1.151          val goalss = map8 (map4 oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss';
   1.152  
   1.153          val tacss =
   1.154 -          map4 (map ooo mk_corec_tac corec_defs nesting_map_idents)
   1.155 +          map4 (map ooo mk_corec_tac corec_defs live_nesting_map_idents)
   1.156              ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss;
   1.157  
   1.158          fun prove goal tac =
   1.159 @@ -1073,14 +1076,14 @@
   1.160      val time = time lthy;
   1.161      val timer = time (Timer.startRealTimer ());
   1.162  
   1.163 -    val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
   1.164 -    val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
   1.165 +    val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
   1.166 +    val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
   1.167  
   1.168      val pre_map_defs = map map_def_of_bnf pre_bnfs;
   1.169      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
   1.170      val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
   1.171 -    val nesting_set_maps = maps set_map_of_bnf nesting_bnfs;
   1.172 -    val nested_set_maps = maps set_map_of_bnf nested_bnfs;
   1.173 +    val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs;
   1.174 +    val live_nesting_set_maps = maps set_map_of_bnf live_nesting_bnfs;
   1.175  
   1.176      val live = live_of_bnf any_fp_bnf;
   1.177      val _ =
   1.178 @@ -1245,7 +1248,7 @@
   1.179  
   1.180                fun mk_set_thm fp_set_thm ctr_def' cxIn =
   1.181                  fold_thms lthy [ctr_def']
   1.182 -                  (unfold_thms lthy (pre_set_defs @ nested_set_maps @ nesting_set_maps @
   1.183 +                  (unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @
   1.184                         (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_set @
   1.185                         abs_inverses)
   1.186                       (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
   1.187 @@ -1357,8 +1360,7 @@
   1.188                                      let
   1.189                                        val X = HOLogic.dest_setT (range_type (fastype_of set));
   1.190                                        val (x, ctxt') = yield_singleton (mk_Frees "x") X ctxt;
   1.191 -                                      val assm = HOLogic.mk_Trueprop
   1.192 -                                        (HOLogic.mk_mem (x, set $ a));
   1.193 +                                      val assm = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ a));
   1.194                                      in
   1.195                                        travese_nested_types x ctxt'
   1.196                                        |>> map (Logic.mk_implies o pair assm)
   1.197 @@ -1527,7 +1529,7 @@
   1.198        let
   1.199          val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
   1.200            derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct xtor_co_rec_thms
   1.201 -            nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses type_definitions
   1.202 +            live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses type_definitions
   1.203              abs_inverses ctrss ctr_defss recs rec_defs lthy;
   1.204  
   1.205          val induct_type_attr = Attrib.internal o K o Induct.induct_type;
   1.206 @@ -1548,8 +1550,8 @@
   1.207          lthy
   1.208          |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
   1.209          |> Local_Theory.notes (common_notes @ notes) |> snd
   1.210 -        |> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs
   1.211 -          fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm]
   1.212 +        |> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs
   1.213 +          live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm]
   1.214            (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss
   1.215            rel_distinctss
   1.216        end;
   1.217 @@ -1563,8 +1565,8 @@
   1.218               (corec_thmss, corec_attrs), (disc_corec_thmss, disc_corec_attrs),
   1.219               (disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
   1.220            derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
   1.221 -            dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
   1.222 -            abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
   1.223 +            dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
   1.224 +            ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
   1.225              (Proof_Context.export lthy' no_defs_lthy) lthy;
   1.226  
   1.227          val ((rel_coinduct_thms, rel_coinduct_thm),
   1.228 @@ -1611,8 +1613,8 @@
   1.229          |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
   1.230            [flat sel_corec_thmss, flat corec_thmss]
   1.231          |> Local_Theory.notes (common_notes @ notes) |> snd
   1.232 -        |> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos nested_bnfs
   1.233 -          nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
   1.234 +        |> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs
   1.235 +          live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
   1.236            [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms])
   1.237            corec_thmss disc_corec_thmss sel_corec_thmsss rel_injectss rel_distinctss
   1.238        end;
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Jun 27 10:11:44 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Jun 27 10:11:44 2014 +0200
     2.3 @@ -71,9 +71,10 @@
     2.4      val fp_absT_infos = map #absT_info fp_sugars;
     2.5      val fp_bnfs = of_fp_res #bnfs;
     2.6      val pre_bnfs = map #pre_bnf fp_sugars;
     2.7 -    val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
     2.8 -    val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
     2.9 -    val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
    2.10 +    val nesting_bnfss =
    2.11 +      map (fn sugar => #fp_nesting_bnfs sugar @ #live_nesting_bnfs sugar) fp_sugars;
    2.12 +    val fp_or_nesting_bnfss = fp_bnfs :: nesting_bnfss;
    2.13 +    val fp_or_nesting_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_or_nesting_bnfss);
    2.14  
    2.15      val fp_absTs = map #absT fp_absT_infos;
    2.16      val fp_repTs = map #repT fp_absT_infos;
    2.17 @@ -137,7 +138,7 @@
    2.18  
    2.19      val rels =
    2.20        let
    2.21 -        fun find_rel T As Bs = fp_nesty_bnfss
    2.22 +        fun find_rel T As Bs = fp_or_nesting_bnfss
    2.23            |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
    2.24            |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
    2.25            |> Option.map (fn bnf =>
    2.26 @@ -186,7 +187,7 @@
    2.27          xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs rel_monos)
    2.28          lthy;
    2.29  
    2.30 -    val rel_eqs = no_refl (map rel_eq_of_bnf fp_nesty_bnfs);
    2.31 +    val rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
    2.32      val map_id0s = no_refl (map map_id0_of_bnf bnfs);
    2.33  
    2.34      val xtor_co_induct_thm =
    2.35 @@ -419,7 +420,8 @@
    2.36  
    2.37          val map_thms = no_refl (maps (fn bnf =>
    2.38             let val map_comp0 = map_comp0_of_bnf bnf RS sym
    2.39 -           in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) fp_nesty_bnfs) @
    2.40 +           in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end)
    2.41 +          fp_or_nesting_bnfs) @
    2.42            remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
    2.43            (map2 (fn thm => fn bnf =>
    2.44              @{thm type_copy_map_comp0_undo} OF
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Jun 27 10:11:44 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Jun 27 10:11:44 2014 +0200
     3.3 @@ -237,8 +237,8 @@
     3.4          val repTs = map #repT absT_infos;
     3.5          val abs_inverses = map #abs_inverse absT_infos;
     3.6  
     3.7 -        val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
     3.8 -        val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
     3.9 +        val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
    3.10 +        val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
    3.11  
    3.12          val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
    3.13            mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
    3.14 @@ -256,15 +256,16 @@
    3.15               fp_sugar_thms) =
    3.16            if fp = Least_FP then
    3.17              derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
    3.18 -              xtor_co_rec_thms nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
    3.19 -              fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs lthy
    3.20 +              xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
    3.21 +              fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs
    3.22 +              lthy
    3.23              |> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
    3.24                ([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
    3.25              ||> (fn info => (SOME info, NONE))
    3.26            else
    3.27              derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
    3.28 -              dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
    3.29 -              fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
    3.30 +              dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
    3.31 +              mss ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
    3.32                ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy
    3.33              |> `(fn ((coinduct_thms_pairs, _), (corec_thmss, _), (disc_corec_thmss, _), _,
    3.34                       (sel_corec_thmsss, _)) =>
    3.35 @@ -278,11 +279,11 @@
    3.36              co_rec_def maps co_inducts co_rec_thms disc_corec_thms sel_corec_thmss
    3.37              ({rel_injects, rel_distincts, ...} : fp_sugar) =
    3.38            {T = T, BT = Term.dummyT (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res,
    3.39 -           fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info, nested_bnfs = nested_bnfs,
    3.40 -           nesting_bnfs = nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs,
    3.41 -           ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
    3.42 -           common_co_inducts = common_co_inducts, co_inducts = co_inducts,
    3.43 -           co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
    3.44 +           fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info,
    3.45 +           fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
    3.46 +           ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
    3.47 +           co_rec_def = co_rec_def, maps = maps, common_co_inducts = common_co_inducts,
    3.48 +           co_inducts = co_inducts, co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
    3.49             sel_co_recss = sel_corec_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
    3.50            |> morph_fp_sugar phi;
    3.51  
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Jun 27 10:11:44 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Jun 27 10:11:44 2014 +0200
     4.3 @@ -37,8 +37,8 @@
     4.4       fp_res: fp_result,
     4.5       pre_bnf: BNF_Def.bnf,
     4.6       absT_info: BNF_Comp.absT_info,
     4.7 -     nested_bnfs: BNF_Def.bnf list,
     4.8 -     nesting_bnfs: BNF_Def.bnf list,
     4.9 +     fp_nesting_bnfs: BNF_Def.bnf list,
    4.10 +     live_nesting_bnfs: BNF_Def.bnf list,
    4.11       ctrXs_Tss: typ list list,
    4.12       ctr_defs: thm list,
    4.13       ctr_sugar: Ctr_Sugar.ctr_sugar,
    4.14 @@ -264,8 +264,8 @@
    4.15     fp_res: fp_result,
    4.16     pre_bnf: bnf,
    4.17     absT_info: absT_info,
    4.18 -   nested_bnfs: bnf list,
    4.19 -   nesting_bnfs: bnf list,
    4.20 +   fp_nesting_bnfs: bnf list,
    4.21 +   live_nesting_bnfs: bnf list,
    4.22     ctrXs_Tss: typ list list,
    4.23     ctr_defs: thm list,
    4.24     ctr_sugar: Ctr_Sugar.ctr_sugar,
    4.25 @@ -280,8 +280,8 @@
    4.26     rel_injects: thm list,
    4.27     rel_distincts: thm list};
    4.28  
    4.29 -fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
    4.30 -    nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
    4.31 +fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
    4.32 +    live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
    4.33      co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, rel_injects, rel_distincts} : fp_sugar) =
    4.34    {T = Morphism.typ phi T,
    4.35     BT = Morphism.typ phi BT,
    4.36 @@ -291,8 +291,8 @@
    4.37     fp_res_index = fp_res_index,
    4.38     pre_bnf = morph_bnf phi pre_bnf,
    4.39     absT_info = morph_absT_info phi absT_info,
    4.40 -   nested_bnfs = map (morph_bnf phi) nested_bnfs,
    4.41 -   nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
    4.42 +   fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs,
    4.43 +   live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs,
    4.44     ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
    4.45     ctr_defs = map (Morphism.thm phi) ctr_defs,
    4.46     ctr_sugar = morph_ctr_sugar phi ctr_sugar,
     5.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Jun 27 10:11:44 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Jun 27 10:11:44 2014 +0200
     5.3 @@ -79,9 +79,9 @@
     5.4    {corec: term,
     5.5     disc_exhausts: thm list,
     5.6     sel_defs: thm list,
     5.7 -   nested_maps: thm list,
     5.8 -   nested_map_idents: thm list,
     5.9 -   nested_map_comps: thm list,
    5.10 +   fp_nesting_maps: thm list,
    5.11 +   fp_nesting_map_idents: thm list,
    5.12 +   fp_nesting_map_comps: thm list,
    5.13     ctr_specs: corec_ctr_spec list};
    5.14  
    5.15  exception NOT_A_MAP of term;
    5.16 @@ -375,7 +375,7 @@
    5.17    let
    5.18      val thy = Proof_Context.theory_of lthy0;
    5.19  
    5.20 -    val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs,
    5.21 +    val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
    5.22            common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
    5.23        nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
    5.24  
    5.25 @@ -464,9 +464,11 @@
    5.26          co_rec_thms = corec_thms, disc_co_recs = disc_corecs,
    5.27          sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
    5.28        {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, disc_exhausts = disc_exhausts,
    5.29 -       sel_defs = sel_defs, nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
    5.30 -       nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
    5.31 -       nested_map_comps = map map_comp_of_bnf nested_bnfs,
    5.32 +       sel_defs = sel_defs,
    5.33 +       fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,
    5.34 +       fp_nesting_map_idents =
    5.35 +         map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) fp_nesting_bnfs,
    5.36 +       fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs,
    5.37         ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs
    5.38           sel_corecss};
    5.39    in
    5.40 @@ -1173,8 +1175,8 @@
    5.41                  |> single
    5.42              end;
    5.43  
    5.44 -        fun prove_sel ({sel_defs, nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...}
    5.45 -              : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss
    5.46 +        fun prove_sel ({sel_defs, fp_nesting_maps, fp_nesting_map_idents, fp_nesting_map_comps,
    5.47 +              ctr_specs, ...} : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss
    5.48              ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, code_rhs_opt, eqn_pos, ...}
    5.49               : coeqn_data_sel) =
    5.50            let
    5.51 @@ -1195,8 +1197,8 @@
    5.52                |> curry Logic.list_all (map dest_Free fun_args);
    5.53              val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy rhs_term;
    5.54            in
    5.55 -            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
    5.56 -              nested_map_idents nested_map_comps sel_corec k m excludesss
    5.57 +            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms fp_nesting_maps
    5.58 +              fp_nesting_map_idents fp_nesting_map_comps sel_corec k m excludesss
    5.59              |> K |> Goal.prove_sorry lthy [] [] goal
    5.60              |> Thm.close_derivation
    5.61              |> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Jun 27 10:11:44 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Jun 27 10:11:44 2014 +0200
     6.3 @@ -79,8 +79,8 @@
     6.4  
     6.5  type rec_spec =
     6.6    {recx: term,
     6.7 -   nested_map_idents: thm list,
     6.8 -   nested_map_comps: thm list,
     6.9 +   fp_nesting_map_idents: thm list,
    6.10 +   fp_nesting_map_comps: thm list,
    6.11     ctr_specs: rec_ctr_spec list};
    6.12  
    6.13  type basic_lfp_sugar =
    6.14 @@ -135,7 +135,7 @@
    6.15    let
    6.16      val thy = Proof_Context.theory_of lthy0;
    6.17  
    6.18 -    val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, nested_map_idents, nested_map_comps,
    6.19 +    val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_idents, fp_nesting_map_comps,
    6.20           common_induct, n2m, lthy) =
    6.21        get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0;
    6.22  
    6.23 @@ -195,7 +195,7 @@
    6.24      fun mk_spec ctr_offset
    6.25          ({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) =
    6.26        {recx = mk_co_rec thy Least_FP (substAT T) perm_Cs' recx,
    6.27 -       nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
    6.28 +       fp_nesting_map_idents = fp_nesting_map_idents, fp_nesting_map_comps = fp_nesting_map_comps,
    6.29         ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
    6.30    in
    6.31      ((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, common_induct, inducts), lthy)
    6.32 @@ -464,8 +464,8 @@
    6.33  
    6.34      val defs = build_defs lthy nonexhaustive bs mxs funs_data rec_specs has_call;
    6.35  
    6.36 -    fun prove lthy' def_thms' ({ctr_specs, nested_map_idents, nested_map_comps, ...} : rec_spec)
    6.37 -        (fun_data : eqn_data list) =
    6.38 +    fun prove lthy' def_thms' ({ctr_specs, fp_nesting_map_idents, fp_nesting_map_comps, ...}
    6.39 +        : rec_spec) (fun_data : eqn_data list) =
    6.40        let
    6.41          val js =
    6.42            find_indices (op = o pairself (fn {fun_name, ctr, ...} => (fun_name, ctr)))
    6.43 @@ -477,8 +477,8 @@
    6.44            |> map_filter (try (fn (x, [y]) =>
    6.45              (#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
    6.46            |> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) =>
    6.47 -              mk_primrec_tac lthy' num_extra_args nested_map_idents nested_map_comps def_thms
    6.48 -                rec_thm
    6.49 +              mk_primrec_tac lthy' num_extra_args fp_nesting_map_idents fp_nesting_map_comps
    6.50 +                def_thms rec_thm
    6.51                |> K |> Goal.prove_sorry lthy' [] [] user_eqn
    6.52                (* for code extraction from proof terms: *)
    6.53                |> singleton (Proof_Context.export lthy' lthy)
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Jun 27 10:11:44 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Jun 27 10:11:44 2014 +0200
     7.3 @@ -29,7 +29,7 @@
     7.4  fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
     7.5    let
     7.6      val ((missing_arg_Ts, perm0_kks,
     7.7 -          fp_sugars as {nested_bnfs, common_co_inducts = [common_induct], ...} :: _,
     7.8 +          fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
     7.9            (lfp_sugar_thms, _)), lthy) =
    7.10        nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0;
    7.11  
    7.12 @@ -47,11 +47,12 @@
    7.13      val ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
    7.14      val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_Tsss;
    7.15  
    7.16 -    val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs;
    7.17 -    val nested_map_comps = map map_comp_of_bnf nested_bnfs;
    7.18 +    val fp_nesting_map_idents =
    7.19 +      map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) fp_nesting_bnfs;
    7.20 +    val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs;
    7.21    in
    7.22      (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
    7.23 -     nested_map_idents, nested_map_comps, common_induct, is_some lfp_sugar_thms, lthy)
    7.24 +     fp_nesting_map_idents, fp_nesting_map_comps, common_induct, is_some lfp_sugar_thms, lthy)
    7.25    end;
    7.26  
    7.27  exception NOT_A_MAP of term;
     8.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Jun 27 10:11:44 2014 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Jun 27 10:11:44 2014 +0200
     8.3 @@ -66,12 +66,12 @@
     8.4  val rec_o_map_simp_thms =
     8.5    @{thms o_def id_def case_prod_app case_sum_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def};
     8.6  
     8.7 -fun mk_rec_o_map_tac ctxt rec_def pre_map_defs nesting_map_idents abs_inverses ctor_rec_o_map =
     8.8 +fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_idents abs_inverses ctor_rec_o_map =
     8.9    unfold_thms_tac ctxt [rec_def] THEN
    8.10    HEADGOAL (rtac (ctor_rec_o_map RS trans)) THEN
    8.11    PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion) THEN
    8.12    HEADGOAL (asm_simp_tac (ss_only (pre_map_defs @
    8.13 -    distinct Thm.eq_thm_prop (nesting_map_idents @ abs_inverses) @ rec_o_map_simp_thms) ctxt));
    8.14 +    distinct Thm.eq_thm_prop (live_nesting_map_idents @ abs_inverses) @ rec_o_map_simp_thms) ctxt));
    8.15  
    8.16  val size_o_map_simp_thms = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
    8.17  
    8.18 @@ -82,8 +82,8 @@
    8.19    IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
    8.20  
    8.21  fun generate_lfp_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs),
    8.22 -    fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, nested_bnfs,
    8.23 -    nesting_bnfs, ...} : fp_sugar) :: _) lthy0 =
    8.24 +    fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, fp_nesting_bnfs,
    8.25 +    live_nesting_bnfs, ...} : fp_sugar) :: _) lthy0 =
    8.26    let
    8.27      val data = Data.get (Context.Proof lthy0);
    8.28  
    8.29 @@ -221,7 +221,7 @@
    8.30         |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm)));
    8.31  
    8.32      val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps;
    8.33 -    val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs)
    8.34 +    val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs)
    8.35        |> distinct Thm.eq_thm_prop;
    8.36  
    8.37      fun derive_size_simp size_def' simp0 =
    8.38 @@ -258,7 +258,7 @@
    8.39          let
    8.40            val pre_bnfs = map #pre_bnf fp_sugars;
    8.41            val pre_map_defs = map map_def_of_bnf pre_bnfs;
    8.42 -          val nesting_map_idents = map map_ident_of_bnf nesting_bnfs;
    8.43 +          val live_nesting_map_idents = map map_ident_of_bnf live_nesting_bnfs;
    8.44            val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
    8.45            val rec_defs = map #co_rec_def fp_sugars;
    8.46  
    8.47 @@ -303,7 +303,7 @@
    8.48            val rec_o_map_thms =
    8.49              map3 (fn goal => fn rec_def => fn ctor_rec_o_map =>
    8.50                  Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} =>
    8.51 -                  mk_rec_o_map_tac ctxt rec_def pre_map_defs nesting_map_idents abs_inverses
    8.52 +                  mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_idents abs_inverses
    8.53                      ctor_rec_o_map)
    8.54                  |> Thm.close_derivation)
    8.55                rec_o_map_goals rec_defs ctor_rec_o_maps;