refactor fp_sugar move theorems
authordesharna
Fri Sep 26 14:41:54 2014 +0200 (2014-09-26)
changeset 58460a88eb33058f7
parent 58459 f70bffabd7cf
child 58461 75ee8d49c724
refactor fp_sugar move theorems
src/HOL/Library/bnf_lfp_countable.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
src/HOL/Tools/SMT/smt_datatypes.ML
     1.1 --- a/src/HOL/Library/bnf_lfp_countable.ML	Fri Sep 26 14:41:15 2014 +0200
     1.2 +++ b/src/HOL/Library/bnf_lfp_countable.ML	Fri Sep 26 14:41:54 2014 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4  
     1.5        val fp_sugars as {fp_nesting_bnfs, common_co_inducts = induct :: _, ...} :: _ =
     1.6          map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
     1.7 -      val ctr_sugars = map #ctr_sugar fp_sugars;
     1.8 +      val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
     1.9  
    1.10        val ctrss0 = map #ctrs ctr_sugars;
    1.11        val ns = map length ctrss0;
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 26 14:41:15 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 26 14:41:54 2014 +0200
     2.3 @@ -8,7 +8,10 @@
     2.4  
     2.5  signature BNF_FP_DEF_SUGAR =
     2.6  sig
     2.7 -  type fp_ctr_sugar = {}
     2.8 +  type fp_ctr_sugar =
     2.9 +    {ctrXs_Tss: typ list list,
    2.10 +     ctr_defs: thm list,
    2.11 +     ctr_sugar: Ctr_Sugar.ctr_sugar}
    2.12  
    2.13    type fp_bnf_sugar =
    2.14      {rel_injects: thm list,
    2.15 @@ -31,9 +34,6 @@
    2.16       absT_info: BNF_Comp.absT_info,
    2.17       fp_nesting_bnfs: BNF_Def.bnf list,
    2.18       live_nesting_bnfs: BNF_Def.bnf list,
    2.19 -     ctrXs_Tss: typ list list,
    2.20 -     ctr_defs: thm list,
    2.21 -     ctr_sugar: Ctr_Sugar.ctr_sugar,
    2.22       co_rec: term,
    2.23       co_rec_def: thm,
    2.24       maps: thm list,
    2.25 @@ -160,7 +160,10 @@
    2.26  val set_inductN = "set_induct";
    2.27  val set_selN = "set_sel";
    2.28  
    2.29 -type fp_ctr_sugar = {}
    2.30 +type fp_ctr_sugar =
    2.31 +  {ctrXs_Tss: typ list list,
    2.32 +   ctr_defs: thm list,
    2.33 +   ctr_sugar: Ctr_Sugar.ctr_sugar}
    2.34  
    2.35  type fp_bnf_sugar =
    2.36    {rel_injects: thm list,
    2.37 @@ -183,9 +186,6 @@
    2.38     absT_info: absT_info,
    2.39     fp_nesting_bnfs: bnf list,
    2.40     live_nesting_bnfs: bnf list,
    2.41 -   ctrXs_Tss: typ list list,
    2.42 -   ctr_defs: thm list,
    2.43 -   ctr_sugar: Ctr_Sugar.ctr_sugar,
    2.44     co_rec: term,
    2.45     co_rec_def: thm,
    2.46     maps: thm list,
    2.47 @@ -205,9 +205,14 @@
    2.48     co_rec_discs = map (Morphism.thm phi) co_rec_discs,
    2.49     co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss}
    2.50  
    2.51 +fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar} : fp_ctr_sugar) =
    2.52 +  {ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
    2.53 +   ctr_defs = map (Morphism.thm phi) ctr_defs,
    2.54 +   ctr_sugar = morph_ctr_sugar phi ctr_sugar}
    2.55 +
    2.56  fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
    2.57 -    live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
    2.58 -    fp_ctr_sugar, fp_bnf_sugar, fp_co_induct_sugar} : fp_sugar) =
    2.59 +    live_nesting_bnfs, co_rec, co_rec_def, maps, common_co_inducts, fp_ctr_sugar, fp_bnf_sugar,
    2.60 +    fp_co_induct_sugar} : fp_sugar) =
    2.61    {T = Morphism.typ phi T,
    2.62     BT = Morphism.typ phi BT,
    2.63     X = Morphism.typ phi X,
    2.64 @@ -218,14 +223,11 @@
    2.65     absT_info = morph_absT_info phi absT_info,
    2.66     fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs,
    2.67     live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs,
    2.68 -   ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
    2.69 -   ctr_defs = map (Morphism.thm phi) ctr_defs,
    2.70 -   ctr_sugar = morph_ctr_sugar phi ctr_sugar,
    2.71     co_rec = Morphism.term phi co_rec,
    2.72     co_rec_def = Morphism.thm phi co_rec_def,
    2.73     maps = map (Morphism.thm phi) maps,
    2.74     common_co_inducts = map (Morphism.thm phi) common_co_inducts,
    2.75 -   fp_ctr_sugar = fp_ctr_sugar,
    2.76 +   fp_ctr_sugar = morph_fp_ctr_sugar phi fp_ctr_sugar,
    2.77     fp_bnf_sugar = morph_fp_bnf_sugar phi fp_bnf_sugar,
    2.78     fp_co_induct_sugar = morph_fp_co_induct_sugar phi fp_co_induct_sugar};
    2.79  
    2.80 @@ -286,10 +288,12 @@
    2.81          {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
    2.82           pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk,
    2.83           fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
    2.84 -         ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk,
    2.85           co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk, maps = nth mapss kk,
    2.86           common_co_inducts = common_co_inducts,
    2.87 -         fp_ctr_sugar = {},
    2.88 +         fp_ctr_sugar =
    2.89 +           {ctrXs_Tss = nth ctrXs_Tsss kk,
    2.90 +            ctr_defs = nth ctr_defss kk,
    2.91 +            ctr_sugar = nth ctr_sugars kk},
    2.92           fp_bnf_sugar =
    2.93             {rel_injects = nth rel_injectss kk,
    2.94              rel_distincts = nth rel_distinctss kk},
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Sep 26 14:41:15 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Sep 26 14:41:54 2014 +0200
     3.3 @@ -136,7 +136,7 @@
     3.4      val nn = length fpTs;
     3.5      val kks = 0 upto nn - 1;
     3.6  
     3.7 -    fun target_ctr_sugar_of_fp_sugar fpT ({T, ctr_sugar, ...} : fp_sugar) =
     3.8 +    fun target_ctr_sugar_of_fp_sugar fpT ({T, fp_ctr_sugar = {ctr_sugar, ...}, ...} : fp_sugar) =
     3.9        let
    3.10          val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
    3.11          val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho);
    3.12 @@ -144,7 +144,7 @@
    3.13          morph_ctr_sugar phi ctr_sugar
    3.14        end;
    3.15  
    3.16 -    val ctr_defss = map #ctr_defs fp_sugars0;
    3.17 +    val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0;
    3.18      val mapss = map #maps fp_sugars0;
    3.19      val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
    3.20  
    3.21 @@ -296,10 +296,12 @@
    3.22              ({fp_bnf_sugar = {rel_injects, rel_distincts, ...}, ...} : fp_sugar) =
    3.23            {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
    3.24             pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs,
    3.25 -           live_nesting_bnfs = live_nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs,
    3.26 -           ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
    3.27 +           live_nesting_bnfs = live_nesting_bnfs, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
    3.28             common_co_inducts = common_co_inducts,
    3.29 -           fp_ctr_sugar = {},
    3.30 +           fp_ctr_sugar =
    3.31 +             {ctrXs_Tss = ctrXs_Tss,
    3.32 +              ctr_defs = ctr_defs,
    3.33 +              ctr_sugar = ctr_sugar},
    3.34             fp_bnf_sugar =
    3.35               {rel_injects = rel_injects,
    3.36                rel_distincts = rel_distincts},
    3.37 @@ -457,7 +459,8 @@
    3.38      val perm_callssss0 = permute callssss0;
    3.39      val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
    3.40  
    3.41 -    val perm_callssss = map2 (indexify_callsss o #ctrs o #ctr_sugar) perm_fp_sugars0 perm_callssss0;
    3.42 +    val perm_callssss =
    3.43 +      map2 (indexify_callsss o #ctrs o #ctr_sugar o #fp_ctr_sugar) perm_fp_sugars0 perm_callssss0;
    3.44  
    3.45      val ((perm_fp_sugars, fp_sugar_thms), lthy) =
    3.46        if length perm_Tss = 1 then
     4.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 26 14:41:15 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 26 14:41:54 2014 +0200
     4.3 @@ -420,7 +420,8 @@
     4.4      val perm_indices = map #fp_res_index perm_fp_sugars;
     4.5  
     4.6      val perm_fpTs = map #T perm_fp_sugars;
     4.7 -    val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars;
     4.8 +    val perm_ctrXs_Tsss' =
     4.9 +      map (repair_nullary_single_ctr o #ctrXs_Tss o #fp_ctr_sugar) perm_fp_sugars;
    4.10  
    4.11      val nn0 = length res_Ts;
    4.12      val nn = length perm_fpTs;
    4.13 @@ -495,7 +496,7 @@
    4.14            distinct_discsss collapses corec_thms corec_discs corec_selss
    4.15        end;
    4.16  
    4.17 -    fun mk_spec ({T, ctr_sugar as {exhaust_discs, sel_defs, ...}, co_rec = corec,
    4.18 +    fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...}, co_rec = corec,
    4.19          fp_co_induct_sugar = {co_rec_thms = corec_thms, co_rec_discs = corec_discs,
    4.20          co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
    4.21        {corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, exhaust_discs = exhaust_discs,
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Fri Sep 26 14:41:15 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Fri Sep 26 14:41:54 2014 +0200
     5.3 @@ -76,14 +76,14 @@
     5.4       absT_info = trivial_absT_info_of fpT,
     5.5       fp_nesting_bnfs = [],
     5.6       live_nesting_bnfs = [],
     5.7 -     ctrXs_Tss = ctr_Tss,
     5.8 -     ctr_defs = @{thms Inl_def_alt Inr_def_alt},
     5.9 -     ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
    5.10       co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
    5.11       co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]},
    5.12       maps = @{thms map_sum.simps},
    5.13       common_co_inducts = @{thms sum.induct},
    5.14 -     fp_ctr_sugar = {},
    5.15 +     fp_ctr_sugar =
    5.16 +       {ctrXs_Tss = ctr_Tss,
    5.17 +        ctr_defs = @{thms Inl_def_alt Inr_def_alt},
    5.18 +        ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
    5.19       fp_bnf_sugar =
    5.20         {rel_injects = @{thms rel_sum_simps(1,4)},
    5.21          rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}},
    5.22 @@ -120,14 +120,14 @@
    5.23       absT_info = trivial_absT_info_of fpT,
    5.24       fp_nesting_bnfs = [],
    5.25       live_nesting_bnfs = [],
    5.26 -     ctrXs_Tss = [ctr_Ts],
    5.27 -     ctr_defs = @{thms Pair_def_alt},
    5.28 -     ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
    5.29       co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
    5.30       co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
    5.31       maps = @{thms map_prod_simp},
    5.32       common_co_inducts = @{thms prod.induct},
    5.33 -     fp_ctr_sugar = {},
    5.34 +     fp_ctr_sugar =
    5.35 +       {ctrXs_Tss = [ctr_Ts],
    5.36 +        ctr_defs = @{thms Pair_def_alt},
    5.37 +        ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
    5.38       fp_bnf_sugar =
    5.39         {rel_injects = @{thms rel_prod_apply},
    5.40          rel_distincts = []},
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Sep 26 14:41:15 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Sep 26 14:41:54 2014 +0200
     6.3 @@ -236,7 +236,7 @@
     6.4      fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
     6.5        (index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs));
     6.6  
     6.7 -    val fp_ctr_sugars = map (#ctr_sugar o checked_fp_sugar_of) fpT_names;
     6.8 +    val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar o checked_fp_sugar_of) fpT_names;
     6.9      val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
    6.10      val all_infos = Old_Datatype_Data.get_all thy;
    6.11      val (orig_descr' :: nested_descrs) =
    6.12 @@ -290,11 +290,12 @@
    6.13        else
    6.14          ((fp_sugars, (NONE, NONE)), lthy);
    6.15  
    6.16 -    fun mk_ctr_of ({ctr_sugar = {ctrs, ...}, ...} : fp_sugar) (Type (_, Ts)) = map (mk_ctr Ts) ctrs;
    6.17 +    fun mk_ctr_of ({fp_ctr_sugar = {ctr_sugar = {ctrs, ...}, ...}, ...} : fp_sugar) (Type (_, Ts)) =
    6.18 +      map (mk_ctr Ts) ctrs;
    6.19      val substAT = Term.typ_subst_atomic (var_As ~~ As);
    6.20  
    6.21      val Xs' = map #X fp_sugars';
    6.22 -    val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss) fp_sugars';
    6.23 +    val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss o #fp_ctr_sugar) fp_sugars';
    6.24      val ctrss' = map2 mk_ctr_of fp_sugars' fpTs';
    6.25      val {common_co_inducts = induct :: _, ...} :: _ = fp_sugars';
    6.26      val inducts = map (hd o #co_inducts o #fp_co_induct_sugar) fp_sugars';
    6.27 @@ -317,8 +318,9 @@
    6.28      val rec'_names = map (fst o dest_Const) recs';
    6.29      val rec'_thms = flat rec'_thmss;
    6.30  
    6.31 -    fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
    6.32 -        distincts, case_thms, case_cong, case_cong_weak, split, split_asm, ...}, ...} : fp_sugar) =
    6.33 +    fun mk_info (kk, {T = Type (T_name0, _), fp_ctr_sugar = {ctr_sugar = {casex, exhaust, nchotomy,
    6.34 +        injects, distincts, case_thms, case_cong, case_cong_weak, split,
    6.35 +        split_asm, ...}, ...}, ...} : fp_sugar) =
    6.36        (T_name0,
    6.37         {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct',
    6.38          inducts = inducts', exhaust = exhaust, nchotomy = nchotomy, rec_names = rec'_names,
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Sep 26 14:41:15 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Sep 26 14:41:54 2014 +0200
     7.3 @@ -24,7 +24,7 @@
     7.4    | is_new_datatype ctxt s =
     7.5      (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
     7.6  
     7.7 -fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_sugar, co_rec = recx,
     7.8 +fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, fp_ctr_sugar = {ctr_sugar, ...}, co_rec = recx,
     7.9      fp_co_induct_sugar = {co_rec_thms = rec_thms, ...}, ...} : fp_sugar) =
    7.10    {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
    7.11     recx = recx, rec_thms = rec_thms};
    7.12 @@ -51,7 +51,7 @@
    7.13              SOME (T, C) => [T, C]
    7.14            | NONE => [U]);
    7.15  
    7.16 -      val ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
    7.17 +      val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) fp_sugars;
    7.18        val fun_arg_Tssss = map (map (map zip_XrecT)) ctrXs_Tsss;
    7.19  
    7.20        val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
     8.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Fri Sep 26 14:41:15 2014 +0200
     8.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Fri Sep 26 14:41:54 2014 +0200
     8.3 @@ -71,13 +71,13 @@
     8.4        | info :: _ => (map (pair (hd fps)) (get_typedef_decl info T Ts), ctxt))
     8.5    in
     8.6      (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
     8.7 -      SOME {fp, fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} =>
     8.8 +      SOME {fp, fp_res = {Ts = fp_Ts, ...}, fp_ctr_sugar = {ctr_sugar, ...}, ...} =>
     8.9        if member (op =) fps fp then
    8.10          let
    8.11            val ns = map (fst o dest_Type) fp_Ts
    8.12            val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns
    8.13            val Xs = map #X mutual_fp_sugars
    8.14 -          val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars
    8.15 +          val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) mutual_fp_sugars
    8.16  
    8.17            (* Datatypes nested through datatypes and codatatypes nested through codatatypes are
    8.18               allowed. So are mutually (co)recursive (co)datatypes. *)