use the noted theorem whenever possible, also in 'BNF_Def'
authorblanchet
Thu Jul 24 00:24:00 2014 +0200 (2014-07-24)
changeset 57631959caab43a3d
parent 57630 04ab38720b50
child 57632 231e90cf2892
use the noted theorem whenever possible, also in 'BNF_Def'
src/HOL/Ctr_Sugar.thy
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
     1.1 --- a/src/HOL/Ctr_Sugar.thy	Thu Jul 24 00:24:00 2014 +0200
     1.2 +++ b/src/HOL/Ctr_Sugar.thy	Thu Jul 24 00:24:00 2014 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
     1.5    case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
     1.6    case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
     1.7 +
     1.8  declare [[coercion_args case_guard - + -]]
     1.9  declare [[coercion_args case_cons - -]]
    1.10  declare [[coercion_args case_abs -]]
     2.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Jul 24 00:24:00 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Jul 24 00:24:00 2014 +0200
     2.3 @@ -103,7 +103,7 @@
     2.4    val bnf_timing: bool Config.T
     2.5    val user_policy: fact_policy -> Proof.context -> fact_policy
     2.6    val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> Proof.context ->
     2.7 -    Proof.context
     2.8 +    bnf * Proof.context
     2.9  
    2.10    val print_bnfs: Proof.context -> unit
    2.11    val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> bool ->
    2.12 @@ -624,7 +624,7 @@
    2.13  
    2.14  val smart_max_inline_term_size = 25; (*FUDGE*)
    2.15  
    2.16 -fun note_bnf_thms fact_policy qualify0 bnf_b bnf =
    2.17 +fun note_bnf_thms fact_policy qualify0 bnf_b bnf lthy =
    2.18    let
    2.19      val axioms = axioms_of_bnf bnf;
    2.20      val facts = facts_of_bnf bnf;
    2.21 @@ -632,61 +632,63 @@
    2.22      val qualify =
    2.23        let val (_, qs, _) = Binding.dest bnf_b;
    2.24        in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify0 end;
    2.25 -  in
    2.26 -    (if fact_policy = Note_All then
    2.27 +
    2.28 +    fun note_if_note_all (noted0, lthy0) =
    2.29        let
    2.30          val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits);
    2.31          val notes =
    2.32            [(bd_card_orderN, [#bd_card_order axioms]),
    2.33 -            (bd_cinfiniteN, [#bd_cinfinite axioms]),
    2.34 -            (bd_Card_orderN, [#bd_Card_order facts]),
    2.35 -            (bd_CinfiniteN, [#bd_Cinfinite facts]),
    2.36 -            (bd_CnotzeroN, [#bd_Cnotzero facts]),
    2.37 -            (collect_set_mapN, [Lazy.force (#collect_set_map facts)]),
    2.38 -            (in_bdN, [Lazy.force (#in_bd facts)]),
    2.39 -            (in_monoN, [Lazy.force (#in_mono facts)]),
    2.40 -            (in_relN, [Lazy.force (#in_rel facts)]),
    2.41 -            (inj_mapN, [Lazy.force (#inj_map facts)]),
    2.42 -            (map_comp0N, [#map_comp0 axioms]),
    2.43 -            (map_transferN, [Lazy.force (#map_transfer facts)]),
    2.44 -            (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
    2.45 -            (set_map0N, #set_map0 axioms),
    2.46 -            (set_bdN, #set_bd axioms)] @
    2.47 -            (witNs ~~ wit_thmss_of_bnf bnf)
    2.48 -            |> map (fn (thmN, thms) =>
    2.49 -              ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), []),
    2.50 -              [(thms, [])]));
    2.51 -        in
    2.52 -          Local_Theory.notes notes #> snd
    2.53 -        end
    2.54 -      else
    2.55 -        I)
    2.56 -    #> (if fact_policy <> Dont_Note then
    2.57 -        let
    2.58 -          val notes =
    2.59 -            [(map_compN, [Lazy.force (#map_comp facts)], []),
    2.60 -            (map_cong0N, [#map_cong0 axioms], []),
    2.61 -            (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
    2.62 -            (map_idN, [Lazy.force (#map_id facts)], []),
    2.63 -            (map_id0N, [#map_id0 axioms], []),
    2.64 -            (map_identN, [Lazy.force (#map_ident facts)], []),
    2.65 -            (rel_comppN, [Lazy.force (#rel_OO facts)], []),
    2.66 -            (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
    2.67 -            (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
    2.68 -            (rel_eqN, [Lazy.force (#rel_eq facts)], []),
    2.69 -            (rel_flipN, [Lazy.force (#rel_flip facts)], []),
    2.70 -            (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
    2.71 -            (rel_monoN, [Lazy.force (#rel_mono facts)], []),
    2.72 -            (set_mapN, map Lazy.force (#set_map facts), [])]
    2.73 -            |> filter_out (null o #2)
    2.74 -            |> map (fn (thmN, thms, attrs) =>
    2.75 -              ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)),
    2.76 -                attrs), [(thms, [])]));
    2.77 -        in
    2.78 -          Local_Theory.notes notes #> snd
    2.79 -        end
    2.80 -      else
    2.81 -        I)
    2.82 +           (bd_cinfiniteN, [#bd_cinfinite axioms]),
    2.83 +           (bd_Card_orderN, [#bd_Card_order facts]),
    2.84 +           (bd_CinfiniteN, [#bd_Cinfinite facts]),
    2.85 +           (bd_CnotzeroN, [#bd_Cnotzero facts]),
    2.86 +           (collect_set_mapN, [Lazy.force (#collect_set_map facts)]),
    2.87 +           (in_bdN, [Lazy.force (#in_bd facts)]),
    2.88 +           (in_monoN, [Lazy.force (#in_mono facts)]),
    2.89 +           (in_relN, [Lazy.force (#in_rel facts)]),
    2.90 +           (inj_mapN, [Lazy.force (#inj_map facts)]),
    2.91 +           (map_comp0N, [#map_comp0 axioms]),
    2.92 +           (map_transferN, [Lazy.force (#map_transfer facts)]),
    2.93 +           (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
    2.94 +           (set_map0N, #set_map0 axioms),
    2.95 +           (set_bdN, #set_bd axioms)] @
    2.96 +          (witNs ~~ wit_thmss_of_bnf bnf)
    2.97 +          |> map (fn (thmN, thms) =>
    2.98 +            ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), []),
    2.99 +             [(thms, [])]));
   2.100 +      in
   2.101 +        Local_Theory.notes notes lthy0 |>> append noted0
   2.102 +      end
   2.103 +
   2.104 +    fun note_unless_dont_note (noted0, lthy0) =
   2.105 +      let
   2.106 +        val notes =
   2.107 +          [(map_compN, [Lazy.force (#map_comp facts)], []),
   2.108 +           (map_cong0N, [#map_cong0 axioms], []),
   2.109 +           (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
   2.110 +           (map_idN, [Lazy.force (#map_id facts)], []),
   2.111 +           (map_id0N, [#map_id0 axioms], []),
   2.112 +           (map_identN, [Lazy.force (#map_ident facts)], []),
   2.113 +           (rel_comppN, [Lazy.force (#rel_OO facts)], []),
   2.114 +           (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
   2.115 +           (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
   2.116 +           (rel_eqN, [Lazy.force (#rel_eq facts)], []),
   2.117 +           (rel_flipN, [Lazy.force (#rel_flip facts)], []),
   2.118 +           (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
   2.119 +           (rel_monoN, [Lazy.force (#rel_mono facts)], []),
   2.120 +           (set_mapN, map Lazy.force (#set_map facts), [])]
   2.121 +          |> filter_out (null o #2)
   2.122 +          |> map (fn (thmN, thms, attrs) =>
   2.123 +            ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), attrs),
   2.124 +             [(thms, [])]));
   2.125 +      in
   2.126 +        Local_Theory.notes notes lthy0 |>> append noted0
   2.127 +      end
   2.128 +  in
   2.129 +    ([], lthy)
   2.130 +    |> fact_policy = Note_All ? note_if_note_all
   2.131 +    |> fact_policy <> Dont_Note ? note_unless_dont_note
   2.132 +    |>> (fn [] => bnf | noted => morph_bnf (substitute_noted_thm noted) bnf)
   2.133    end;
   2.134  
   2.135  
   2.136 @@ -1339,7 +1341,7 @@
   2.137          val bnf = mk_bnf bnf_b Calpha live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms
   2.138            defs facts wits bnf_rel;
   2.139        in
   2.140 -        (bnf, lthy |> note_bnf_thms fact_policy qualify bnf_b bnf)
   2.141 +        note_bnf_thms fact_policy qualify bnf_b bnf lthy
   2.142        end;
   2.143  
   2.144      val one_step_defs =
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     3.3 @@ -150,7 +150,7 @@
     3.4  
     3.5  fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res
     3.6      ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss common_co_inducts co_inductss
     3.7 -    co_rec_thmss disc_co_recss sel_co_recsss rel_injectss rel_distinctss =
     3.8 +    co_rec_thmss disc_co_recss sel_co_recsss rel_injectss rel_distinctss noted =
     3.9    let
    3.10      val fp_sugars =
    3.11        map_index (fn (kk, T) =>
    3.12 @@ -162,7 +162,8 @@
    3.13           common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
    3.14           co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk,
    3.15           sel_co_recss = nth sel_co_recsss kk, rel_injects = nth rel_injectss kk,
    3.16 -         rel_distincts = nth rel_distinctss kk}) Ts
    3.17 +         rel_distincts = nth rel_distinctss kk}
    3.18 +        |> morph_fp_sugar (substitute_noted_thm noted)) Ts
    3.19    in
    3.20      register_fp_sugars fp_sugars
    3.21    end;
    3.22 @@ -1251,7 +1252,7 @@
    3.23            end;
    3.24  
    3.25          fun derive_maps_sets_rels (ctr_sugar as {case_cong, discs, selss, ctrs, exhaust, disc_thmss,
    3.26 -          sel_thmss, injects, distincts, ...} : ctr_sugar, lthy) =
    3.27 +            sel_thmss, injects, distincts, ...} : ctr_sugar, lthy) =
    3.28            if live = 0 then
    3.29              ((([], [], [], []), ctr_sugar), lthy)
    3.30            else
    3.31 @@ -1630,15 +1631,19 @@
    3.32                   (sel_setN, sel_set_thms, []),
    3.33                   (set_emptyN, set_empty_thms, [])]
    3.34                  |> massage_simple_notes fp_b_name;
    3.35 +
    3.36 +              val (noted, lthy') =
    3.37 +                lthy
    3.38 +                |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms)
    3.39 +                |> fp = Least_FP
    3.40 +                  ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms)
    3.41 +                |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set_thms)
    3.42 +                |> Local_Theory.notes (anonymous_notes @ notes);
    3.43 +
    3.44 +              val subst = Morphism.thm (substitute_noted_thm noted);
    3.45              in
    3.46 -              (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar),
    3.47 -               lthy
    3.48 -               |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms)
    3.49 -               |> fp = Least_FP
    3.50 -                 ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms)
    3.51 -               |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set_thms)
    3.52 -               |> Local_Theory.notes (anonymous_notes @ notes)
    3.53 -               |> snd)
    3.54 +              (((map subst map_thms, map subst rel_inject_thms, map subst rel_distinct_thms,
    3.55 +                 map (map subst) set_thmss), ctr_sugar), lthy')
    3.56              end;
    3.57  
    3.58          fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
    3.59 @@ -1709,8 +1714,8 @@
    3.60        in
    3.61          lthy
    3.62          |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
    3.63 -        |> Local_Theory.notes (common_notes @ notes) |> snd
    3.64 -        |> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs
    3.65 +        |> Local_Theory.notes (common_notes @ notes)
    3.66 +        |-> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs
    3.67            live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm]
    3.68            (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss
    3.69            rel_distinctss
    3.70 @@ -1791,11 +1796,10 @@
    3.71            |> massage_multi_notes;
    3.72        in
    3.73          lthy
    3.74 -        (* TODO: code theorems *)
    3.75          |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
    3.76            [flat sel_corec_thmss, flat corec_thmss]
    3.77 -        |> Local_Theory.notes (common_notes @ notes) |> snd
    3.78 -        |> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs
    3.79 +        |> Local_Theory.notes (common_notes @ notes)
    3.80 +        |-> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs
    3.81            live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
    3.82            [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms])
    3.83            corec_thmss disc_corec_thmss sel_corec_thmsss rel_injectss rel_distinctss
     4.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Jul 24 00:24:00 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Jul 24 00:24:00 2014 +0200
     4.3 @@ -2467,64 +2467,69 @@
     4.4            dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, lthy)
     4.5        end;
     4.6  
     4.7 -      val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m
     4.8 -        dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms)
     4.9 -        sym_map_comps map_cong0s;
    4.10 -      val dtor_corec_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m
    4.11 -        dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms)
    4.12 -        sym_map_comps map_cong0s;
    4.13 +    val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m
    4.14 +      dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms)
    4.15 +      sym_map_comps map_cong0s;
    4.16 +    val dtor_corec_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m
    4.17 +      dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms)
    4.18 +      sym_map_comps map_cong0s;
    4.19  
    4.20 -      val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
    4.21 +    val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
    4.22  
    4.23 -      val dtor_unfold_transfer_thms =
    4.24 -        mk_un_fold_transfer_thms Greatest_FP rels activephis
    4.25 -          (if m = 0 then map HOLogic.eq_const Ts
    4.26 -            else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis
    4.27 -          (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
    4.28 -          (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm
    4.29 -            (map map_transfer_of_bnf bnfs) dtor_unfold_thms)
    4.30 -          lthy;
    4.31 +    val dtor_unfold_transfer_thms =
    4.32 +      mk_un_fold_transfer_thms Greatest_FP rels activephis
    4.33 +        (if m = 0 then map HOLogic.eq_const Ts
    4.34 +          else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis
    4.35 +        (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
    4.36 +        (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm
    4.37 +          (map map_transfer_of_bnf bnfs) dtor_unfold_thms)
    4.38 +        lthy;
    4.39  
    4.40 -      val timer = time (timer "relator coinduction");
    4.41 +    val timer = time (timer "relator coinduction");
    4.42  
    4.43 -      val common_notes =
    4.44 -        [(dtor_coinductN, [dtor_coinduct_thm]),
    4.45 -        (dtor_rel_coinductN, [Jrel_coinduct_thm]),
    4.46 -        (dtor_unfold_transferN, dtor_unfold_transfer_thms)]
    4.47 -        |> map (fn (thmN, thms) =>
    4.48 -          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    4.49 +    val common_notes =
    4.50 +      [(dtor_coinductN, [dtor_coinduct_thm]),
    4.51 +      (dtor_rel_coinductN, [Jrel_coinduct_thm]),
    4.52 +      (dtor_unfold_transferN, dtor_unfold_transfer_thms)]
    4.53 +      |> map (fn (thmN, thms) =>
    4.54 +        ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    4.55  
    4.56 -      val notes =
    4.57 -        [(ctor_dtorN, ctor_dtor_thms),
    4.58 -        (ctor_exhaustN, ctor_exhaust_thms),
    4.59 -        (ctor_injectN, ctor_inject_thms),
    4.60 -        (dtor_corecN, dtor_corec_thms),
    4.61 -        (dtor_ctorN, dtor_ctor_thms),
    4.62 -        (dtor_exhaustN, dtor_exhaust_thms),
    4.63 -        (dtor_injectN, dtor_inject_thms),
    4.64 -        (dtor_unfoldN, dtor_unfold_thms),
    4.65 -        (dtor_unfold_uniqueN, dtor_unfold_unique_thms),
    4.66 -        (dtor_corec_uniqueN, dtor_corec_unique_thms),
    4.67 -        (dtor_unfold_o_mapN, dtor_unfold_o_Jmap_thms),
    4.68 -        (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms)]
    4.69 -        |> map (apsnd (map single))
    4.70 -        |> maps (fn (thmN, thmss) =>
    4.71 -          map2 (fn b => fn thms =>
    4.72 -            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    4.73 -          bs thmss);
    4.74 +    val notes =
    4.75 +      [(ctor_dtorN, ctor_dtor_thms),
    4.76 +      (ctor_exhaustN, ctor_exhaust_thms),
    4.77 +      (ctor_injectN, ctor_inject_thms),
    4.78 +      (dtor_corecN, dtor_corec_thms),
    4.79 +      (dtor_ctorN, dtor_ctor_thms),
    4.80 +      (dtor_exhaustN, dtor_exhaust_thms),
    4.81 +      (dtor_injectN, dtor_inject_thms),
    4.82 +      (dtor_unfoldN, dtor_unfold_thms),
    4.83 +      (dtor_unfold_uniqueN, dtor_unfold_unique_thms),
    4.84 +      (dtor_corec_uniqueN, dtor_corec_unique_thms),
    4.85 +      (dtor_unfold_o_mapN, dtor_unfold_o_Jmap_thms),
    4.86 +      (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms)]
    4.87 +      |> map (apsnd (map single))
    4.88 +      |> maps (fn (thmN, thmss) =>
    4.89 +        map2 (fn b => fn thms =>
    4.90 +          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    4.91 +        bs thmss);
    4.92  
    4.93      (*FIXME: once the package exports all the necessary high-level characteristic theorems,
    4.94         those should not only be concealed but rather not noted at all*)
    4.95      val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
    4.96 +
    4.97 +    val (noted, lthy') =
    4.98 +      lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes));
    4.99 +
   4.100 +    val fp_res =
   4.101 +      {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_recs = corecs,
   4.102 +       xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
   4.103 +       ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
   4.104 +       xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
   4.105 +       xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
   4.106 +       xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm}
   4.107 +      |> morph_fp_result (substitute_noted_thm noted);
   4.108    in
   4.109 -    timer;
   4.110 -    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_recs = corecs,
   4.111 -      xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
   4.112 -      ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
   4.113 -      xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
   4.114 -      xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
   4.115 -      xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm},
   4.116 -     lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes)) |> snd)
   4.117 +    timer; (fp_res, lthy')
   4.118    end;
   4.119  
   4.120  val _ =
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Jul 24 00:24:00 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Jul 24 00:24:00 2014 +0200
     5.3 @@ -1752,67 +1752,72 @@
     5.4            ctor_Irel_thms, Ibnf_common_notes @ Ibnf_notes, lthy)
     5.5        end;
     5.6  
     5.7 -      val ctor_fold_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm
     5.8 -        ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s;
     5.9 -      val ctor_rec_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm
    5.10 -        ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s;
    5.11 +    val ctor_fold_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm
    5.12 +      ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s;
    5.13 +    val ctor_rec_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm
    5.14 +      ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s;
    5.15  
    5.16 -      val Irels = if m = 0 then map HOLogic.eq_const Ts
    5.17 -        else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
    5.18 -      val Irel_induct_thm =
    5.19 -        mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
    5.20 -          (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
    5.21 -             ctor_Irel_thms rel_mono_strongs) lthy;
    5.22 +    val Irels = if m = 0 then map HOLogic.eq_const Ts
    5.23 +      else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
    5.24 +    val Irel_induct_thm =
    5.25 +      mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
    5.26 +        (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
    5.27 +           ctor_Irel_thms rel_mono_strongs) lthy;
    5.28  
    5.29 -      val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
    5.30 -      val ctor_fold_transfer_thms =
    5.31 -        mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis
    5.32 -          (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
    5.33 -          (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm
    5.34 -            (map map_transfer_of_bnf bnfs) ctor_fold_thms)
    5.35 -          lthy;
    5.36 +    val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
    5.37 +    val ctor_fold_transfer_thms =
    5.38 +      mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis
    5.39 +        (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
    5.40 +        (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm
    5.41 +          (map map_transfer_of_bnf bnfs) ctor_fold_thms)
    5.42 +        lthy;
    5.43  
    5.44 -      val timer = time (timer "relator induction");
    5.45 +    val timer = time (timer "relator induction");
    5.46  
    5.47 -      val common_notes =
    5.48 -        [(ctor_inductN, [ctor_induct_thm]),
    5.49 -        (ctor_induct2N, [ctor_induct2_thm]),
    5.50 -        (ctor_fold_transferN, ctor_fold_transfer_thms),
    5.51 -        (ctor_rel_inductN, [Irel_induct_thm])]
    5.52 -        |> map (fn (thmN, thms) =>
    5.53 -          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    5.54 +    val common_notes =
    5.55 +      [(ctor_inductN, [ctor_induct_thm]),
    5.56 +      (ctor_induct2N, [ctor_induct2_thm]),
    5.57 +      (ctor_fold_transferN, ctor_fold_transfer_thms),
    5.58 +      (ctor_rel_inductN, [Irel_induct_thm])]
    5.59 +      |> map (fn (thmN, thms) =>
    5.60 +        ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    5.61  
    5.62 -      val notes =
    5.63 -        [(ctor_dtorN, ctor_dtor_thms),
    5.64 -        (ctor_exhaustN, ctor_exhaust_thms),
    5.65 -        (ctor_foldN, ctor_fold_thms),
    5.66 -        (ctor_fold_uniqueN, ctor_fold_unique_thms),
    5.67 -        (ctor_rec_uniqueN, ctor_rec_unique_thms),
    5.68 -        (ctor_fold_o_mapN, ctor_fold_o_Imap_thms),
    5.69 -        (ctor_rec_o_mapN, ctor_rec_o_Imap_thms),
    5.70 -        (ctor_injectN, ctor_inject_thms),
    5.71 -        (ctor_recN, ctor_rec_thms),
    5.72 -        (dtor_ctorN, dtor_ctor_thms),
    5.73 -        (dtor_exhaustN, dtor_exhaust_thms),
    5.74 -        (dtor_injectN, dtor_inject_thms)]
    5.75 -        |> map (apsnd (map single))
    5.76 -        |> maps (fn (thmN, thmss) =>
    5.77 -          map2 (fn b => fn thms =>
    5.78 -            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    5.79 -          bs thmss);
    5.80 +    val notes =
    5.81 +      [(ctor_dtorN, ctor_dtor_thms),
    5.82 +      (ctor_exhaustN, ctor_exhaust_thms),
    5.83 +      (ctor_foldN, ctor_fold_thms),
    5.84 +      (ctor_fold_uniqueN, ctor_fold_unique_thms),
    5.85 +      (ctor_rec_uniqueN, ctor_rec_unique_thms),
    5.86 +      (ctor_fold_o_mapN, ctor_fold_o_Imap_thms),
    5.87 +      (ctor_rec_o_mapN, ctor_rec_o_Imap_thms),
    5.88 +      (ctor_injectN, ctor_inject_thms),
    5.89 +      (ctor_recN, ctor_rec_thms),
    5.90 +      (dtor_ctorN, dtor_ctor_thms),
    5.91 +      (dtor_exhaustN, dtor_exhaust_thms),
    5.92 +      (dtor_injectN, dtor_inject_thms)]
    5.93 +      |> map (apsnd (map single))
    5.94 +      |> maps (fn (thmN, thmss) =>
    5.95 +        map2 (fn b => fn thms =>
    5.96 +          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    5.97 +        bs thmss);
    5.98  
    5.99      (*FIXME: once the package exports all the necessary high-level characteristic theorems,
   5.100         those should not only be concealed but rather not noted at all*)
   5.101      val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
   5.102 +
   5.103 +    val (noted, lthy') =
   5.104 +      lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes));
   5.105 +
   5.106 +    val fp_res =
   5.107 +      {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_recs = recs,
   5.108 +       xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
   5.109 +       ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
   5.110 +       xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
   5.111 +       xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
   5.112 +       xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm}
   5.113 +      |> morph_fp_result (substitute_noted_thm noted);
   5.114    in
   5.115 -    timer;
   5.116 -    ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_recs = recs,
   5.117 -      xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
   5.118 -      ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
   5.119 -      xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
   5.120 -      xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
   5.121 -      xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm},
   5.122 -     lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes)) |> snd)
   5.123 +    timer; (fp_res, lthy')
   5.124    end;
   5.125  
   5.126  val _ =
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Jul 24 00:24:00 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Jul 24 00:24:00 2014 +0200
     6.3 @@ -354,14 +354,19 @@
     6.4         (sizeN, size_thmss, code_nitpicksimp_simp_attrs),
     6.5         (size_o_mapN, size_o_map_thmss, [])]
     6.6        |> massage_multi_notes;
     6.7 +
     6.8 +    val (noted, lthy3) =
     6.9 +      lthy2
    6.10 +      |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps)
    6.11 +      |> Local_Theory.notes notes;
    6.12 +
    6.13 +    val phi0 = substitute_noted_thm noted;
    6.14    in
    6.15 -    lthy2
    6.16 -    |> Local_Theory.notes notes |> snd
    6.17 -    |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps)
    6.18 +    lthy3
    6.19      |> Local_Theory.declaration {syntax = false, pervasive = true}
    6.20        (fn phi => Data.map (fold2 (fn T_name => fn Const (size_name, _) =>
    6.21             Symtab.update (T_name, (size_name,
    6.22 -             pairself (map (Morphism.thm phi)) (size_simps, flat size_o_map_thmss))))
    6.23 +             pairself (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_o_map_thmss))))
    6.24           T_names size_consts))
    6.25    end;
    6.26  
     7.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     7.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     7.3 @@ -1011,7 +1011,7 @@
     7.4                       (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
     7.5                       (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
     7.6                    I)
     7.7 -          |> Local_Theory.notes (anonymous_notes @ notes)
     7.8 +          |> Local_Theory.notes (anonymous_notes @ notes);
     7.9  
    7.10          val ctr_sugar =
    7.11            {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
     8.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Thu Jul 24 00:24:00 2014 +0200
     8.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Thu Jul 24 00:24:00 2014 +0200
     8.3 @@ -239,7 +239,7 @@
     8.4  fun substitute_noted_thm noted =
     8.5    let val tab = fold (fold (Termtab.default o `Thm.full_prop_of) o snd) noted Termtab.empty in
     8.6      Morphism.thm_morphism "Ctr_Sugar_Util.substitute_noted_thm"
     8.7 -      (perhaps (Termtab.lookup tab o Thm.full_prop_of))
     8.8 +      (perhaps (Termtab.lookup tab o Thm.full_prop_of) o Drule.zero_var_indexes)
     8.9    end
    8.10  
    8.11  (* The standard binding stands for a name generated following the canonical convention (e.g.,