tuned names
authorblanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55067a452de24a877
parent 55066 4e5ddf3162ac
child 55068 526671cca4a7
tuned names
src/HOL/Main.thy
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_comp_tactics.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/BNF/bnf_tactics.ML
     1.1 --- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -24,8 +24,7 @@
     1.4    ordIso2 (infix "=o" 50) and
     1.5    csum (infixr "+c" 65) and
     1.6    cprod (infixr "*c" 80) and
     1.7 -  cexp (infixr "^c" 90) and
     1.8 -  convol ("<_ , _>")
     1.9 +  cexp (infixr "^c" 90)
    1.10  
    1.11  no_syntax (xsymbols)
    1.12    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
     2.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Jan 20 18:24:56 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Jan 20 18:24:56 2014 +0100
     2.3 @@ -302,8 +302,8 @@
     2.4  
     2.5      fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
     2.6      fun map_comp0_tac {context = ctxt, prems = _} =
     2.7 -      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
     2.8 -      rtac refl 1;
     2.9 +      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
    2.10 +        @{thms comp_assoc id_comp comp_id}) THEN rtac refl 1;
    2.11      fun map_cong0_tac {context = ctxt, prems = _} =
    2.12        mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
    2.13      val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_of_bnf bnf));
    2.14 @@ -394,8 +394,8 @@
    2.15  
    2.16      fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
    2.17      fun map_comp0_tac {context = ctxt, prems = _} =
    2.18 -      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
    2.19 -      rtac refl 1;
    2.20 +      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
    2.21 +        @{thms comp_assoc id_comp comp_id}) THEN rtac refl 1;
    2.22      fun map_cong0_tac {context = ctxt, prems = _} =
    2.23        rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    2.24      val set_map0_tacs =
     3.1 --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     3.3 @@ -44,8 +44,8 @@
     3.4  
     3.5  val Cnotzero_UNIV = @{thm Cnotzero_UNIV};
     3.6  val arg_cong_Union = @{thm arg_cong[of _ _ Union]};
     3.7 +val comp_eq_dest_lhs = @{thm comp_eq_dest_lhs};
     3.8  val csum_Cnotzero1 = @{thm csum_Cnotzero1};
     3.9 -val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
    3.10  val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
    3.11  val trans_o_apply = @{thm trans[OF o_apply]};
    3.12  
    3.13 @@ -54,7 +54,7 @@
    3.14  (* Composition *)
    3.15  
    3.16  fun mk_comp_set_alt_tac ctxt collect_set_map =
    3.17 -  unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN
    3.18 +  unfold_thms_tac ctxt @{thms comp_assoc} THEN
    3.19    unfold_thms_tac ctxt [collect_set_map RS sym] THEN
    3.20    rtac refl 1;
    3.21  
    3.22 @@ -64,7 +64,7 @@
    3.23  
    3.24  fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s =
    3.25    EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
    3.26 -    rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
    3.27 +    rtac (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans), rtac Gmap_cong0] @
    3.28      map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1;
    3.29  
    3.30  fun mk_comp_set_map0_tac Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s =
    3.31 @@ -72,14 +72,14 @@
    3.32      replicate 3 (rtac trans_o_apply) @
    3.33      [rtac (arg_cong_Union RS trans),
    3.34       rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
    3.35 -     rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans),
    3.36 +     rtac (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans),
    3.37       rtac Gmap_cong0] @
    3.38       map (fn thm => rtac (thm RS fun_cong)) set_map0s @
    3.39 -     [rtac (Gset_map0 RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
    3.40 +     [rtac (Gset_map0 RS comp_eq_dest_lhs), rtac sym, rtac trans_o_apply,
    3.41       rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
    3.42 -     rtac (@{thm image_cong} OF [Gset_map0 RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
    3.43 +     rtac (@{thm image_cong} OF [Gset_map0 RS comp_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
    3.44       rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union,
    3.45 -     rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]},
    3.46 +     rtac @{thm trans[OF comp_eq_dest_lhs[OF image_o_collect[symmetric]]]},
    3.47       rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
    3.48       [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac @{thm trans[OF image_insert]},
    3.49          rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply,
     4.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     4.3 @@ -47,7 +47,7 @@
     4.4  val conversep_shift = @{thm conversep_le_swap} RS iffD1;
     4.5  
     4.6  fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply};
     4.7 -fun mk_map_comp comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
     4.8 +fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp];
     4.9  fun mk_map_cong_tac ctxt cong0 =
    4.10    (hyp_subst_tac ctxt THEN' rtac cong0 THEN'
    4.11     REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
    4.12 @@ -61,7 +61,7 @@
    4.13    (etac subset_trans THEN' atac) 1;
    4.14  
    4.15  fun mk_collect_set_map_tac set_map0s =
    4.16 -  (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
    4.17 +  (rtac (@{thm collect_comp} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
    4.18    EVERY' (map (fn set_map0 =>
    4.19      rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN'
    4.20      rtac set_map0) set_map0s) THEN'
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jan 20 18:24:56 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jan 20 18:24:56 2014 +0100
     5.3 @@ -332,8 +332,8 @@
     5.4          val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss;
     5.5          val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
     5.6          val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
     5.7 -        val fold_thms = fp_case fp @{thm o_assoc[symmetric]} @{thm o_assoc} ::
     5.8 -          @{thms id_apply o_apply o_id id_o map_pair.comp map_pair.id sum_map.comp sum_map.id};
     5.9 +        val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: @{thms id_apply
    5.10 +          o_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
    5.11          val rec_thms = fold_thms @ fp_case fp
    5.12            @{thms fst_convol map_pair_o_convol convol_o}
    5.13            @{thms sum_case_o_inj(1) sum_case_o_sum_map o_sum_case};
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jan 20 18:24:56 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jan 20 18:24:56 2014 +0100
     6.3 @@ -534,14 +534,14 @@
     6.4      val n = length sym_map_comps;
     6.5      val rewrite_comp_comp2 = fp_case fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2};
     6.6      val rewrite_comp_comp = fp_case fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp};
     6.7 -    val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_o} @{thm o_id} RS fun_cong);
     6.8 +    val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
     6.9      val map_cong_active_args1 = replicate n (if is_rec
    6.10        then fp_case fp @{thm convol_o} @{thm o_sum_case} RS fun_cong
    6.11        else refl);
    6.12 -    val map_cong_passive_args2 = replicate m (fp_case fp @{thm o_id} @{thm id_o} RS fun_cong);
    6.13 +    val map_cong_passive_args2 = replicate m (fp_case fp @{thm comp_id} @{thm id_comp} RS fun_cong);
    6.14      val map_cong_active_args2 = replicate n (if is_rec
    6.15        then fp_case fp @{thm map_pair_o_convol_id} @{thm sum_case_o_sum_map_id}
    6.16 -      else fp_case fp @{thm id_o} @{thm o_id} RS fun_cong);
    6.17 +      else fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
    6.18      fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
    6.19      val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
    6.20      val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2;
     7.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jan 20 18:24:56 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jan 20 18:24:56 2014 +0100
     7.3 @@ -1969,14 +1969,14 @@
     7.4  
     7.5      val map_id0s_o_id =
     7.6        map (fn thm =>
     7.7 -        mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_o})
     7.8 +        mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_comp})
     7.9        map_id0s;
    7.10  
    7.11      val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
    7.12        `split_conj_thm (split_conj_prems n
    7.13          (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
    7.14 -        |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @
    7.15 -           map_id0s_o_id @ sym_map_comps)
    7.16 +        |> Local_Defs.unfold lthy (@{thms o_sum_case comp_id id_comp comp_assoc[symmetric]
    7.17 +           sum_case_o_inj(1)} @ map_id0s_o_id @ sym_map_comps)
    7.18          OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
    7.19  
    7.20      val timer = time (timer "corec definitions & thms");
     8.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     8.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     8.3 @@ -137,7 +137,7 @@
     8.4      Splitter.split_tac (split_if :: splits) ORELSE'
     8.5      eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
     8.6      etac notE THEN' atac ORELSE'
     8.7 -    (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def o_def split_def
     8.8 +    (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
     8.9         sum.cases} @ mapsx @ map_comps @ map_idents)))));
    8.10  
    8.11  fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
     9.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     9.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     9.3 @@ -247,7 +247,7 @@
     9.4          EVERY' (map (fn thm =>
     9.5            EVERY' [rtac @{thm GrpI},
     9.6              rtac trans, rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
     9.7 -            REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac,
     9.8 +            REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong), atac,
     9.9              REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
    9.10              CONJ_WRAP' (fn (i, thm) =>
    9.11                if i <= m
    9.12 @@ -267,11 +267,11 @@
    9.13            @{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}),
    9.14          hyp_subst_tac ctxt,
    9.15          rtac bexI, rtac conjI, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
    9.16 -        REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
    9.17 -        REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
    9.18 +        REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
    9.19 +        REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
    9.20          atac, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
    9.21 -        REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
    9.22 -        REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
    9.23 +        REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
    9.24 +        REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
    9.25          rtac trans, rtac map_cong0,
    9.26          REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
    9.27          REPEAT_DETERM_N n o rtac refl,
    9.28 @@ -983,8 +983,8 @@
    9.29  fun mk_map_tac m n cT unfold map_comp map_cong0 =
    9.30    EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
    9.31      rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS box_equals)), rtac map_cong0,
    9.32 -    REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
    9.33 -    REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
    9.34 +    REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
    9.35 +    REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
    9.36      rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
    9.37  
    9.38  fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss =
    9.39 @@ -1010,9 +1010,10 @@
    9.40    EVERY' [rtac map_unique,
    9.41      EVERY' (map2 (fn map_thm => fn map_comp0 =>
    9.42        EVERY' (map rtac
    9.43 -        [@{thm o_assoc} RS trans,
    9.44 +        [@{thm comp_assoc[symmetric]} RS trans,
    9.45          @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans,
    9.46 -        @{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans,
    9.47 +        @{thm comp_assoc[symmetric]} RS sym RS trans, map_thm RS arg_cong RS trans,
    9.48 +        @{thm comp_assoc[symmetric]} RS trans,
    9.49          @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl]]))
    9.50      maps map_comp0s)] 1;
    9.51  
    9.52 @@ -1053,7 +1054,7 @@
    9.53  
    9.54  fun mk_dtor_map_unique_tac unfold_unique sym_map_comps ctxt =
    9.55    rtac unfold_unique 1 THEN
    9.56 -  unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN
    9.57 +  unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc[symmetric] id_comp comp_id}) THEN
    9.58    ALLGOALS (etac sym);
    9.59  
    9.60  fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_map0ss
    9.61 @@ -1157,7 +1158,7 @@
    9.62          (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
    9.63          CONJ_WRAP' (fn conv =>
    9.64            EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
    9.65 -          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
    9.66 +          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
    9.67            REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
    9.68            rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
    9.69          @{thms fst_conv snd_conv}];
    9.70 @@ -1187,7 +1188,7 @@
    9.71          rtac conjI,
    9.72          REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
    9.73            rtac box_equals, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
    9.74 -          rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
    9.75 +          rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
    9.76            EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
    9.77              dtac @{thm ssubst_mem[OF pair_collapse]},
    9.78              REPEAT_DETERM o
    9.79 @@ -1212,10 +1213,11 @@
    9.80            rtac exI, rtac conjI, rtac conjI,
    9.81            rtac (map_comp0 RS trans), rtac (dtor_map RS trans RS sym),
    9.82            rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp0, map_cong]),
    9.83 -          REPEAT_DETERM_N m o rtac @{thm trans[OF fun_cong[OF o_id] sym[OF fun_cong[OF id_o]]]},
    9.84 +          REPEAT_DETERM_N m o
    9.85 +            rtac @{thm trans[OF fun_cong[OF comp_id] sym[OF fun_cong[OF id_comp]]]},
    9.86            REPEAT_DETERM_N n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}),
    9.87            rtac (map_comp0 RS trans), rtac (map_cong RS trans),
    9.88 -          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_o]},
    9.89 +          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_comp]},
    9.90            REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}),
    9.91            etac (@{thm prod.cases} RS map_arg_cong RS trans),
    9.92            SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.cases}), 
    10.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Jan 20 18:24:56 2014 +0100
    10.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Jan 20 18:24:56 2014 +0100
    10.3 @@ -1313,7 +1313,7 @@
    10.4      val (ctor_rec_unique_thms, ctor_rec_unique_thm) =
    10.5        `split_conj_thm (split_conj_prems n
    10.6          (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm)
    10.7 -        |> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @
    10.8 +        |> Local_Defs.unfold lthy (@{thms convol_o comp_id id_comp comp_assoc fst_convol} @
    10.9             map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
   10.10  
   10.11      val timer = time (timer "rec definitions & thms");
    11.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jan 20 18:24:56 2014 +0100
    11.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jan 20 18:24:56 2014 +0100
    11.3 @@ -461,7 +461,8 @@
    11.4  fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx =
    11.5    unfold_thms_tac ctxt fun_defs THEN
    11.6    HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
    11.7 -  unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_idents) THEN
    11.8 +  unfold_thms_tac ctxt (@{thms id_def split comp_def fst_conv snd_conv} @ map_comps @
    11.9 +    map_idents) THEN
   11.10    HEADGOAL (rtac refl);
   11.11  
   11.12  fun prepare_primrec fixes specs lthy =
    12.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
    12.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
    12.3 @@ -404,7 +404,7 @@
    12.4            EVERY' [rtac ord_eq_le_trans, resolve_tac set_map, rtac subset_trans,
    12.5              etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]]];
    12.6    in
    12.7 -    (rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm o_id}) THEN'
    12.8 +    (rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm comp_id}) THEN'
    12.9      rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN'
   12.10      stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' rtac mor_incl_min_alg THEN'
   12.11      stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)) 1
   12.12 @@ -585,7 +585,7 @@
   12.13  
   12.14  fun mk_ctor_map_unique_tac fold_unique sym_map_comps ctxt =
   12.15    rtac fold_unique 1 THEN
   12.16 -  unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc[symmetric] id_o o_id}) THEN
   12.17 +  unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
   12.18    ALLGOALS atac;
   12.19  
   12.20  fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
   12.21 @@ -675,7 +675,7 @@
   12.22  fun mk_map_id0_tac map_id0s unique =
   12.23    (rtac sym THEN' rtac unique THEN'
   12.24    EVERY' (map (fn thm =>
   12.25 -    EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id},
   12.26 +    EVERY' [rtac trans, rtac @{thm id_comp}, rtac trans, rtac sym, rtac @{thm comp_id},
   12.27        rtac (thm RS sym RS arg_cong)]) map_id0s)) 1;
   12.28  
   12.29  fun mk_map_comp0_tac map_comp0s ctor_maps unique iplus1 =
   12.30 @@ -737,7 +737,7 @@
   12.31          (in_Irels ~~ (active_set_map0s ~~ ctor_set_set_inclss)),
   12.32          CONJ_WRAP' (fn conv =>
   12.33            EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
   12.34 -          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   12.35 +          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
   12.36            REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
   12.37            rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map,
   12.38            etac eq_arg_cong_ctor_dtor])
   12.39 @@ -766,7 +766,7 @@
   12.40          rtac conjI,
   12.41          REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
   12.42            rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
   12.43 -          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   12.44 +          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
   12.45            EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
   12.46              dtac @{thm ssubst_mem[OF pair_collapse]},
   12.47              REPEAT_DETERM o
    13.1 --- a/src/HOL/Tools/BNF/bnf_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
    13.2 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
    13.3 @@ -58,7 +58,7 @@
    13.4  
    13.5  fun mk_Abs_inj_thm inj = inj OF (replicate 2 UNIV_I);
    13.6  fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac surj THEN' etac exI) 1)
    13.7 -  (Abs_inj_thm RS @{thm bijI});
    13.8 +  (Abs_inj_thm RS @{thm bijI'});
    13.9  
   13.10  
   13.11  
   13.12 @@ -95,7 +95,7 @@
   13.13    rtac refl 1;
   13.14  
   13.15  fun mk_map_comp_id_tac map_comp0 =
   13.16 -  (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
   13.17 +  (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm comp_id} THEN' rtac refl) 1;
   13.18  
   13.19  fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
   13.20    EVERY' [rtac mp, rtac map_cong0,