no need to make 'size' generation an interpretation -- overkill
authorblanchet
Wed Apr 23 10:23:27 2014 +0200 (2014-04-23)
changeset 566501f9ab71d43a5
parent 56649 16e1fa9d094f
child 56651 fc105315822a
no need to make 'size' generation an interpretation -- overkill
src/HOL/BNF_FP_Base.thy
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_fp_util.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Wed Apr 23 10:23:27 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Wed Apr 23 10:23:27 2014 +0200
     1.3 @@ -163,11 +163,58 @@
     1.4  lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1"
     1.5    unfolding fun_eq_iff vimage2p_def o_apply by simp
     1.6  
     1.7 +lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
     1.8 +  by (erule arg_cong)
     1.9 +
    1.10 +lemma snd_o_convol: "(snd \<circ> (\<lambda>x. (f x, g x))) = g"
    1.11 +  by (rule ext) simp
    1.12 +
    1.13 +lemma inj_on_convol_id: "inj_on (\<lambda>x. (x, f x)) X"
    1.14 +  unfolding inj_on_def by simp
    1.15 +
    1.16 +lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
    1.17 +  by (case_tac x) simp
    1.18 +
    1.19 +lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
    1.20 +  by (case_tac x) simp+
    1.21 +
    1.22 +lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
    1.23 +  by (case_tac x) simp+
    1.24 +
    1.25 +lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
    1.26 +  by (simp add: inj_on_def)
    1.27 +
    1.28 +
    1.29  ML_file "Tools/BNF/bnf_fp_util.ML"
    1.30  ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
    1.31 +ML_file "Tools/BNF/bnf_lfp_size.ML"
    1.32  ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
    1.33  ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
    1.34  ML_file "Tools/BNF/bnf_fp_n2m.ML"
    1.35  ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
    1.36  
    1.37 +ML_file "Tools/Function/size.ML"
    1.38 +setup Size.setup
    1.39 +
    1.40 +lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    1.41 +  by (cases b) auto
    1.42 +
    1.43 +lemma nat_size[simp, code]: "size (n\<Colon>nat) = n"
    1.44 +  by (induct n) simp_all
    1.45 +
    1.46 +declare prod.size[no_atp]
    1.47 +
    1.48 +lemma sum_size_o_map: "sum_size g1 g2 \<circ> map_sum f1 f2 = sum_size (g1 \<circ> f1) (g2 \<circ> f2)"
    1.49 +  by (rule ext) (case_tac x, auto)
    1.50 +
    1.51 +lemma prod_size_o_map: "prod_size g1 g2 \<circ> map_prod f1 f2 = prod_size (g1 \<circ> f1) (g2 \<circ> f2)"
    1.52 +  by (rule ext) auto
    1.53 +
    1.54 +setup {*
    1.55 +BNF_LFP_Size.register_size @{type_name sum} @{const_name sum_size} @{thms sum.size}
    1.56 +  @{thms sum_size_o_map}
    1.57 +#> BNF_LFP_Size.register_size @{type_name prod} @{const_name prod_size} @{thms prod.size}
    1.58 +  @{thms prod_size_o_map}
    1.59 +*}
    1.60 +
    1.61  end
     2.1 --- a/src/HOL/BNF_LFP.thy	Wed Apr 23 10:23:27 2014 +0200
     2.2 +++ b/src/HOL/BNF_LFP.thy	Wed Apr 23 10:23:27 2014 +0200
     2.3 @@ -186,61 +186,14 @@
     2.4  lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
     2.5    by (rule ssubst)
     2.6  
     2.7 -lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
     2.8 -  by (erule arg_cong)
     2.9 -
    2.10 -lemma snd_o_convol: "(snd \<circ> (\<lambda>x. (f x, g x))) = g"
    2.11 -  by (rule ext) simp
    2.12 -
    2.13 -lemma inj_on_convol_id: "inj_on (\<lambda>x. (x, f x)) X"
    2.14 -  unfolding inj_on_def by simp
    2.15 -
    2.16 -lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
    2.17 -  by (case_tac x) simp
    2.18 -
    2.19 -lemma case_sum_o_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
    2.20 -  by (case_tac x) simp+
    2.21 -
    2.22 -lemma case_prod_o_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
    2.23 -  by (case_tac x) simp+
    2.24 -
    2.25 -lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
    2.26 -  by (simp add: inj_on_def)
    2.27 -
    2.28  ML_file "Tools/BNF/bnf_lfp_util.ML"
    2.29  ML_file "Tools/BNF/bnf_lfp_tactics.ML"
    2.30  ML_file "Tools/BNF/bnf_lfp.ML"
    2.31  ML_file "Tools/BNF/bnf_lfp_compat.ML"
    2.32  ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
    2.33  
    2.34 -
    2.35 -subsection {* Size of a datatype value *}
    2.36 -
    2.37 -ML_file "Tools/BNF/bnf_lfp_size.ML"
    2.38 -ML_file "Tools/Function/size.ML"
    2.39 -setup Size.setup
    2.40 -
    2.41 -lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    2.42 -  by (cases b) auto
    2.43 -
    2.44 -lemma nat_size[simp, code]: "size (n\<Colon>nat) = n"
    2.45 -  by (induct n) simp_all
    2.46 -
    2.47 -declare prod.size[no_atp]
    2.48 -
    2.49 -lemma sum_size_o_map: "sum_size g1 g2 \<circ> map_sum f1 f2 = sum_size (g1 \<circ> f1) (g2 \<circ> f2)"
    2.50 -  by (rule ext) (case_tac x, auto)
    2.51 -
    2.52 -lemma prod_size_o_map: "prod_size g1 g2 \<circ> map_prod f1 f2 = prod_size (g1 \<circ> f1) (g2 \<circ> f2)"
    2.53 -  by (rule ext) auto
    2.54 -
    2.55 -setup {*
    2.56 -BNF_LFP_Size.register_size @{type_name sum} @{const_name sum_size} @{thms sum.size}
    2.57 -  @{thms sum_size_o_map}
    2.58 -#> BNF_LFP_Size.register_size @{type_name prod} @{const_name prod_size} @{thms prod.size}
    2.59 -  @{thms prod_size_o_map}
    2.60 -*}
    2.61 -
    2.62  hide_fact (open) id_transfer
    2.63  
    2.64 +datatype_new 'a x = X 'a
    2.65 +
    2.66  end
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Apr 23 10:23:27 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Apr 23 10:23:27 2014 +0200
     3.3 @@ -7,37 +7,10 @@
     3.4  
     3.5  signature BNF_FP_DEF_SUGAR =
     3.6  sig
     3.7 -  type fp_sugar =
     3.8 -    {T: typ,
     3.9 -     BT: typ,
    3.10 -     X: typ,
    3.11 -     fp: BNF_Util.fp_kind,
    3.12 -     fp_res_index: int,
    3.13 -     fp_res: BNF_FP_Util.fp_result,
    3.14 -     pre_bnf: BNF_Def.bnf,
    3.15 -     absT_info: BNF_Comp.absT_info,
    3.16 -     nested_bnfs: BNF_Def.bnf list,
    3.17 -     nesting_bnfs: BNF_Def.bnf list,
    3.18 -     ctrXs_Tss: typ list list,
    3.19 -     ctr_defs: thm list,
    3.20 -     ctr_sugar: Ctr_Sugar.ctr_sugar,
    3.21 -     co_rec: term,
    3.22 -     co_rec_def: thm,
    3.23 -     maps: thm list,
    3.24 -     common_co_inducts: thm list,
    3.25 -     co_inducts: thm list,
    3.26 -     co_rec_thms: thm list,
    3.27 -     disc_co_recs: thm list,
    3.28 -     sel_co_recss: thm list list,
    3.29 -     rel_injects: thm list,
    3.30 -     rel_distincts: thm list};
    3.31 -
    3.32 -  val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
    3.33 -  val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
    3.34 -  val fp_sugar_of: Proof.context -> string -> fp_sugar option
    3.35 -  val fp_sugars_of: Proof.context -> fp_sugar list
    3.36 -  val fp_sugar_interpretation: (fp_sugar list -> theory -> theory) -> theory -> theory
    3.37 -  val register_fp_sugars: fp_sugar list -> local_theory -> local_theory
    3.38 +  val fp_sugar_of: Proof.context -> string -> BNF_FP_Util.fp_sugar option
    3.39 +  val fp_sugars_of: Proof.context -> BNF_FP_Util.fp_sugar list
    3.40 +  val fp_sugar_interpretation: (BNF_FP_Util.fp_sugar list -> theory -> theory) -> theory -> theory
    3.41 +  val register_fp_sugars: BNF_FP_Util.fp_sugar list -> local_theory -> local_theory
    3.42  
    3.43    val co_induct_of: 'a list -> 'a
    3.44    val strong_co_induct_of: 'a list -> 'a
    3.45 @@ -121,63 +94,10 @@
    3.46  open BNF_Def
    3.47  open BNF_FP_Util
    3.48  open BNF_FP_Def_Sugar_Tactics
    3.49 +open BNF_LFP_Size
    3.50  
    3.51  val EqN = "Eq_";
    3.52  
    3.53 -type fp_sugar =
    3.54 -  {T: typ,
    3.55 -   BT: typ,
    3.56 -   X: typ,
    3.57 -   fp: fp_kind,
    3.58 -   fp_res_index: int,
    3.59 -   fp_res: fp_result,
    3.60 -   pre_bnf: bnf,
    3.61 -   absT_info: absT_info,
    3.62 -   nested_bnfs: bnf list,
    3.63 -   nesting_bnfs: bnf list,
    3.64 -   ctrXs_Tss: typ list list,
    3.65 -   ctr_defs: thm list,
    3.66 -   ctr_sugar: Ctr_Sugar.ctr_sugar,
    3.67 -   co_rec: term,
    3.68 -   co_rec_def: thm,
    3.69 -   maps: thm list,
    3.70 -   common_co_inducts: thm list,
    3.71 -   co_inducts: thm list,
    3.72 -   co_rec_thms: thm list,
    3.73 -   disc_co_recs: thm list,
    3.74 -   sel_co_recss: thm list list,
    3.75 -   rel_injects: thm list,
    3.76 -   rel_distincts: thm list};
    3.77 -
    3.78 -fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
    3.79 -    nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
    3.80 -    co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, rel_injects, rel_distincts} : fp_sugar) =
    3.81 -  {T = Morphism.typ phi T,
    3.82 -   BT = Morphism.typ phi BT,
    3.83 -   X = Morphism.typ phi X,
    3.84 -   fp = fp,
    3.85 -   fp_res = morph_fp_result phi fp_res,
    3.86 -   fp_res_index = fp_res_index,
    3.87 -   pre_bnf = morph_bnf phi pre_bnf,
    3.88 -   absT_info = morph_absT_info phi absT_info,
    3.89 -   nested_bnfs = map (morph_bnf phi) nested_bnfs,
    3.90 -   nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
    3.91 -   ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
    3.92 -   ctr_defs = map (Morphism.thm phi) ctr_defs,
    3.93 -   ctr_sugar = morph_ctr_sugar phi ctr_sugar,
    3.94 -   co_rec = Morphism.term phi co_rec,
    3.95 -   co_rec_def = Morphism.thm phi co_rec_def,
    3.96 -   maps = map (Morphism.thm phi) maps,
    3.97 -   common_co_inducts = map (Morphism.thm phi) common_co_inducts,
    3.98 -   co_inducts = map (Morphism.thm phi) co_inducts,
    3.99 -   co_rec_thms = map (Morphism.thm phi) co_rec_thms,
   3.100 -   disc_co_recs = map (Morphism.thm phi) disc_co_recs,
   3.101 -   sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss,
   3.102 -   rel_injects = map (Morphism.thm phi) rel_injects,
   3.103 -   rel_distincts = map (Morphism.thm phi) rel_distincts};
   3.104 -
   3.105 -val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
   3.106 -
   3.107  structure Data = Generic_Data
   3.108  (
   3.109    type T = fp_sugar Symtab.table;
   3.110 @@ -211,11 +131,12 @@
   3.111  
   3.112  val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
   3.113  
   3.114 -fun register_fp_sugars fp_sugars =
   3.115 +fun register_fp_sugars (fp_sugars as {fp, ...} :: _) =
   3.116    fold (fn fp_sugar as {T = Type (s, _), ...} =>
   3.117        Local_Theory.declaration {syntax = false, pervasive = true}
   3.118          (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
   3.119      fp_sugars
   3.120 +  #> Local_Theory.background_theory (generate_lfp_size fp_sugars)
   3.121    #> Local_Theory.background_theory (FP_Sugar_Interpretation.data fp_sugars);
   3.122  
   3.123  fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 23 10:23:27 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 23 10:23:27 2014 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  signature BNF_FP_N2M =
     4.5  sig
     4.6    val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
     4.7 -    BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list ->
     4.8 +    BNF_FP_Util.fp_sugar list -> binding list -> (string * sort) list ->
     4.9      typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
    4.10      BNF_FP_Util.fp_result * local_theory
    4.11  end;
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Apr 23 10:23:27 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Apr 23 10:23:27 2014 +0200
     5.3 @@ -11,13 +11,13 @@
     5.4    val dest_map: Proof.context -> string -> term -> term * term list
     5.5  
     5.6    val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
     5.7 -    term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory ->
     5.8 -    (BNF_FP_Def_Sugar.fp_sugar list
     5.9 +    term list list list list -> BNF_FP_Util.fp_sugar list -> local_theory ->
    5.10 +    (BNF_FP_Util.fp_sugar list
    5.11       * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
    5.12      * local_theory
    5.13    val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
    5.14      (term * term list list) list list -> local_theory ->
    5.15 -    (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
    5.16 +    (typ list * int list * BNF_FP_Util.fp_sugar list
    5.17       * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
    5.18      * local_theory
    5.19  end;
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Apr 23 10:23:27 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Apr 23 10:23:27 2014 +0200
     6.3 @@ -28,6 +28,34 @@
     6.4  
     6.5    val morph_fp_result: morphism -> fp_result -> fp_result
     6.6  
     6.7 +  type fp_sugar =
     6.8 +    {T: typ,
     6.9 +     BT: typ,
    6.10 +     X: typ,
    6.11 +     fp: BNF_Util.fp_kind,
    6.12 +     fp_res_index: int,
    6.13 +     fp_res: fp_result,
    6.14 +     pre_bnf: BNF_Def.bnf,
    6.15 +     absT_info: BNF_Comp.absT_info,
    6.16 +     nested_bnfs: BNF_Def.bnf list,
    6.17 +     nesting_bnfs: BNF_Def.bnf list,
    6.18 +     ctrXs_Tss: typ list list,
    6.19 +     ctr_defs: thm list,
    6.20 +     ctr_sugar: Ctr_Sugar.ctr_sugar,
    6.21 +     co_rec: term,
    6.22 +     co_rec_def: thm,
    6.23 +     maps: thm list,
    6.24 +     common_co_inducts: thm list,
    6.25 +     co_inducts: thm list,
    6.26 +     co_rec_thms: thm list,
    6.27 +     disc_co_recs: thm list,
    6.28 +     sel_co_recss: thm list list,
    6.29 +     rel_injects: thm list,
    6.30 +     rel_distincts: thm list};
    6.31 +
    6.32 +  val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
    6.33 +  val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
    6.34 +
    6.35    val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer
    6.36  
    6.37    val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
    6.38 @@ -184,6 +212,7 @@
    6.39  structure BNF_FP_Util : BNF_FP_UTIL =
    6.40  struct
    6.41  
    6.42 +open Ctr_Sugar
    6.43  open BNF_Comp
    6.44  open BNF_Def
    6.45  open BNF_Util
    6.46 @@ -226,6 +255,60 @@
    6.47     xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
    6.48     rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
    6.49  
    6.50 +type fp_sugar =
    6.51 +  {T: typ,
    6.52 +   BT: typ,
    6.53 +   X: typ,
    6.54 +   fp: fp_kind,
    6.55 +   fp_res_index: int,
    6.56 +   fp_res: fp_result,
    6.57 +   pre_bnf: bnf,
    6.58 +   absT_info: absT_info,
    6.59 +   nested_bnfs: bnf list,
    6.60 +   nesting_bnfs: bnf list,
    6.61 +   ctrXs_Tss: typ list list,
    6.62 +   ctr_defs: thm list,
    6.63 +   ctr_sugar: Ctr_Sugar.ctr_sugar,
    6.64 +   co_rec: term,
    6.65 +   co_rec_def: thm,
    6.66 +   maps: thm list,
    6.67 +   common_co_inducts: thm list,
    6.68 +   co_inducts: thm list,
    6.69 +   co_rec_thms: thm list,
    6.70 +   disc_co_recs: thm list,
    6.71 +   sel_co_recss: thm list list,
    6.72 +   rel_injects: thm list,
    6.73 +   rel_distincts: thm list};
    6.74 +
    6.75 +fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
    6.76 +    nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
    6.77 +    co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, rel_injects, rel_distincts} : fp_sugar) =
    6.78 +  {T = Morphism.typ phi T,
    6.79 +   BT = Morphism.typ phi BT,
    6.80 +   X = Morphism.typ phi X,
    6.81 +   fp = fp,
    6.82 +   fp_res = morph_fp_result phi fp_res,
    6.83 +   fp_res_index = fp_res_index,
    6.84 +   pre_bnf = morph_bnf phi pre_bnf,
    6.85 +   absT_info = morph_absT_info phi absT_info,
    6.86 +   nested_bnfs = map (morph_bnf phi) nested_bnfs,
    6.87 +   nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
    6.88 +   ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
    6.89 +   ctr_defs = map (Morphism.thm phi) ctr_defs,
    6.90 +   ctr_sugar = morph_ctr_sugar phi ctr_sugar,
    6.91 +   co_rec = Morphism.term phi co_rec,
    6.92 +   co_rec_def = Morphism.thm phi co_rec_def,
    6.93 +   maps = map (Morphism.thm phi) maps,
    6.94 +   common_co_inducts = map (Morphism.thm phi) common_co_inducts,
    6.95 +   co_inducts = map (Morphism.thm phi) co_inducts,
    6.96 +   co_rec_thms = map (Morphism.thm phi) co_rec_thms,
    6.97 +   disc_co_recs = map (Morphism.thm phi) disc_co_recs,
    6.98 +   sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss,
    6.99 +   rel_injects = map (Morphism.thm phi) rel_injects,
   6.100 +   rel_distincts = map (Morphism.thm phi) rel_distincts};
   6.101 +
   6.102 +val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
   6.103 +
   6.104  fun time ctxt timer msg = (if Config.get ctxt bnf_timing
   6.105    then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
   6.106      "ms")
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Apr 23 10:23:27 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Apr 23 10:23:27 2014 +0200
     7.3 @@ -9,6 +9,7 @@
     7.4  sig
     7.5    val register_size: string -> string -> thm list -> thm list -> theory -> theory
     7.6    val lookup_size: theory -> string -> (string * (thm list * thm list)) option
     7.7 +  val generate_lfp_size: BNF_FP_Util.fp_sugar list -> theory -> theory
     7.8  end;
     7.9  
    7.10  structure BNF_LFP_Size : BNF_LFP_SIZE =
    7.11 @@ -17,7 +18,7 @@
    7.12  open BNF_Util
    7.13  open BNF_Tactics
    7.14  open BNF_Def
    7.15 -open BNF_FP_Def_Sugar
    7.16 +open BNF_FP_Util
    7.17  
    7.18  val size_N = "size_"
    7.19  
    7.20 @@ -53,8 +54,7 @@
    7.21    funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong);
    7.22  
    7.23  val rec_o_map_simp_thms =
    7.24 -  @{thms o_def id_apply case_prod_app case_sum_o_map_sum case_prod_o_map_prod
    7.25 -      BNF_Comp.id_bnf_comp_def};
    7.26 +  @{thms o_def id_apply case_prod_app case_sum_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def};
    7.27  
    7.28  fun mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map =
    7.29    unfold_thms_tac ctxt [rec_def] THEN
    7.30 @@ -71,7 +71,7 @@
    7.31      asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simp_thms) ctxt)) THEN
    7.32    IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
    7.33  
    7.34 -fun generate_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
    7.35 +fun generate_lfp_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
    7.36        fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, nested_bnfs,
    7.37        nesting_bnfs, ...} : fp_sugar) :: _) thy =
    7.38      let
    7.39 @@ -335,8 +335,6 @@
    7.40            Symtab.update_new (T_name, (size_name, (size_simps, flat size_o_map_thmss))))
    7.41          T_names size_names)
    7.42      end
    7.43 -  | generate_size _ thy = thy;
    7.44 -
    7.45 -val _ = Theory.setup (fp_sugar_interpretation generate_size);
    7.46 +  | generate_lfp_size _ thy = thy;
    7.47  
    7.48  end;