# HG changeset patch # User blanchet # Date 1390238696 -3600 # Node ID a452de24a877d187c923814c91d50c766a4bd243 # Parent 4e5ddf3162ac2cc09337c0b131c057feddec2062 tuned names diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Main.thy --- a/src/HOL/Main.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Main.thy Mon Jan 20 18:24:56 2014 +0100 @@ -24,8 +24,7 @@ ordIso2 (infix "=o" 50) and csum (infixr "+c" 65) and cprod (infixr "*c" 80) and - cexp (infixr "^c" 90) and - convol ("<_ , _>") + cexp (infixr "^c" 90) no_syntax (xsymbols) "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Jan 20 18:24:56 2014 +0100 @@ -302,8 +302,8 @@ fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1; fun map_comp0_tac {context = ctxt, prems = _} = - unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN - rtac refl 1; + unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: + @{thms comp_assoc id_comp comp_id}) THEN rtac refl 1; fun map_cong0_tac {context = ctxt, prems = _} = mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf); val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_of_bnf bnf)); @@ -394,8 +394,8 @@ fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1; fun map_comp0_tac {context = ctxt, prems = _} = - unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN - rtac refl 1; + unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: + @{thms comp_assoc id_comp comp_id}) THEN rtac refl 1; fun map_cong0_tac {context = ctxt, prems = _} = rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); val set_map0_tacs = diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_comp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Mon Jan 20 18:24:56 2014 +0100 @@ -44,8 +44,8 @@ val Cnotzero_UNIV = @{thm Cnotzero_UNIV}; val arg_cong_Union = @{thm arg_cong[of _ _ Union]}; +val comp_eq_dest_lhs = @{thm comp_eq_dest_lhs}; val csum_Cnotzero1 = @{thm csum_Cnotzero1}; -val o_eq_dest_lhs = @{thm o_eq_dest_lhs}; val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]}; val trans_o_apply = @{thm trans[OF o_apply]}; @@ -54,7 +54,7 @@ (* Composition *) fun mk_comp_set_alt_tac ctxt collect_set_map = - unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN + unfold_thms_tac ctxt @{thms comp_assoc} THEN unfold_thms_tac ctxt [collect_set_map RS sym] THEN rtac refl 1; @@ -64,7 +64,7 @@ fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s = EVERY' ([rtac ext, rtac sym, rtac trans_o_apply, - rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @ + rtac (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans), rtac Gmap_cong0] @ map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1; fun mk_comp_set_map0_tac Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s = @@ -72,14 +72,14 @@ replicate 3 (rtac trans_o_apply) @ [rtac (arg_cong_Union RS trans), rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans), - rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), + rtac (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans), rtac Gmap_cong0] @ map (fn thm => rtac (thm RS fun_cong)) set_map0s @ - [rtac (Gset_map0 RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply, + [rtac (Gset_map0 RS comp_eq_dest_lhs), rtac sym, rtac trans_o_apply, rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply, - rtac (@{thm image_cong} OF [Gset_map0 RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), + rtac (@{thm image_cong} OF [Gset_map0 RS comp_eq_dest_lhs RS arg_cong_Union, refl] RS trans), rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union, - rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]}, + rtac @{thm trans[OF comp_eq_dest_lhs[OF image_o_collect[symmetric]]]}, rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @ [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac @{thm trans[OF image_insert]}, rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply, diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_def_tactics.ML --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Mon Jan 20 18:24:56 2014 +0100 @@ -47,7 +47,7 @@ val conversep_shift = @{thm conversep_le_swap} RS iffD1; fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply}; -fun mk_map_comp comp = @{thm o_eq_dest_lhs} OF [mk_sym comp]; +fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp]; fun mk_map_cong_tac ctxt cong0 = (hyp_subst_tac ctxt THEN' rtac cong0 THEN' REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1; @@ -61,7 +61,7 @@ (etac subset_trans THEN' atac) 1; fun mk_collect_set_map_tac set_map0s = - (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN' + (rtac (@{thm collect_comp} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN' EVERY' (map (fn set_map0 => rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN' rtac set_map0) set_map0s) THEN' diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Jan 20 18:24:56 2014 +0100 @@ -332,8 +332,8 @@ val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss; val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map; val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map; - val fold_thms = fp_case fp @{thm o_assoc[symmetric]} @{thm o_assoc} :: - @{thms id_apply o_apply o_id id_o map_pair.comp map_pair.id sum_map.comp sum_map.id}; + val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: @{thms id_apply + o_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id}; val rec_thms = fold_thms @ fp_case fp @{thms fst_convol map_pair_o_convol convol_o} @{thms sum_case_o_inj(1) sum_case_o_sum_map o_sum_case}; diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jan 20 18:24:56 2014 +0100 @@ -534,14 +534,14 @@ val n = length sym_map_comps; val rewrite_comp_comp2 = fp_case fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2}; val rewrite_comp_comp = fp_case fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp}; - val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_o} @{thm o_id} RS fun_cong); + val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong); val map_cong_active_args1 = replicate n (if is_rec then fp_case fp @{thm convol_o} @{thm o_sum_case} RS fun_cong else refl); - val map_cong_passive_args2 = replicate m (fp_case fp @{thm o_id} @{thm id_o} RS fun_cong); + val map_cong_passive_args2 = replicate m (fp_case fp @{thm comp_id} @{thm id_comp} RS fun_cong); val map_cong_active_args2 = replicate n (if is_rec then fp_case fp @{thm map_pair_o_convol_id} @{thm sum_case_o_sum_map_id} - else fp_case fp @{thm id_o} @{thm o_id} RS fun_cong); + else fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong); fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s; val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1; val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2; diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Jan 20 18:24:56 2014 +0100 @@ -1969,14 +1969,14 @@ val map_id0s_o_id = map (fn thm => - mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_o}) + mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_comp}) map_id0s; val (dtor_corec_unique_thms, dtor_corec_unique_thm) = `split_conj_thm (split_conj_prems n (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm) - |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @ - map_id0s_o_id @ sym_map_comps) + |> Local_Defs.unfold lthy (@{thms o_sum_case comp_id id_comp comp_assoc[symmetric] + sum_case_o_inj(1)} @ map_id0s_o_id @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); val timer = time (timer "corec definitions & thms"); diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Mon Jan 20 18:24:56 2014 +0100 @@ -137,7 +137,7 @@ Splitter.split_tac (split_if :: splits) ORELSE' eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' etac notE THEN' atac ORELSE' - (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def o_def split_def + (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def sum.cases} @ mapsx @ map_comps @ map_idents))))); fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Jan 20 18:24:56 2014 +0100 @@ -247,7 +247,7 @@ EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans, rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N m o rtac thm, - REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac, + REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong), atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, CONJ_WRAP' (fn (i, thm) => if i <= m @@ -267,11 +267,11 @@ @{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}), hyp_subst_tac ctxt, rtac bexI, rtac conjI, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, - REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong), - REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), + REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong), + REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong), atac, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, - REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong), - REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), + REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong), + REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong), rtac trans, rtac map_cong0, REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac], REPEAT_DETERM_N n o rtac refl, @@ -983,8 +983,8 @@ fun mk_map_tac m n cT unfold map_comp map_cong0 = EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym), rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS box_equals)), rtac map_cong0, - REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong), - REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), + REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong), + REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong), rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1; fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss = @@ -1010,9 +1010,10 @@ EVERY' [rtac map_unique, EVERY' (map2 (fn map_thm => fn map_comp0 => EVERY' (map rtac - [@{thm o_assoc} RS trans, + [@{thm comp_assoc[symmetric]} RS trans, @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans, - @{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans, + @{thm comp_assoc[symmetric]} RS sym RS trans, map_thm RS arg_cong RS trans, + @{thm comp_assoc[symmetric]} RS trans, @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl]])) maps map_comp0s)] 1; @@ -1053,7 +1054,7 @@ fun mk_dtor_map_unique_tac unfold_unique sym_map_comps ctxt = rtac unfold_unique 1 THEN - unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN + unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc[symmetric] id_comp comp_id}) THEN ALLGOALS (etac sym); fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_map0ss @@ -1157,7 +1158,7 @@ (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)), CONJ_WRAP' (fn conv => EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, - REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, + REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]}, REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]), rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac]) @{thms fst_conv snd_conv}]; @@ -1187,7 +1188,7 @@ rtac conjI, REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map, rtac box_equals, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans, - rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, + rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]}, EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac, dtac @{thm ssubst_mem[OF pair_collapse]}, REPEAT_DETERM o @@ -1212,10 +1213,11 @@ rtac exI, rtac conjI, rtac conjI, rtac (map_comp0 RS trans), rtac (dtor_map RS trans RS sym), rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp0, map_cong]), - REPEAT_DETERM_N m o rtac @{thm trans[OF fun_cong[OF o_id] sym[OF fun_cong[OF id_o]]]}, + REPEAT_DETERM_N m o + rtac @{thm trans[OF fun_cong[OF comp_id] sym[OF fun_cong[OF id_comp]]]}, REPEAT_DETERM_N n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}), rtac (map_comp0 RS trans), rtac (map_cong RS trans), - REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_o]}, + REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_comp]}, REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}), etac (@{thm prod.cases} RS map_arg_cong RS trans), SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.cases}), diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Jan 20 18:24:56 2014 +0100 @@ -1313,7 +1313,7 @@ val (ctor_rec_unique_thms, ctor_rec_unique_thm) = `split_conj_thm (split_conj_prems n (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm) - |> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @ + |> Local_Defs.unfold lthy (@{thms convol_o comp_id id_comp comp_assoc fst_convol} @ map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]}); val timer = time (timer "rec definitions & thms"); diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Jan 20 18:24:56 2014 +0100 @@ -461,7 +461,8 @@ fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx = unfold_thms_tac ctxt fun_defs THEN HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN - unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_idents) THEN + unfold_thms_tac ctxt (@{thms id_def split comp_def fst_conv snd_conv} @ map_comps @ + map_idents) THEN HEADGOAL (rtac refl); fun prepare_primrec fixes specs lthy = diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Jan 20 18:24:56 2014 +0100 @@ -404,7 +404,7 @@ EVERY' [rtac ord_eq_le_trans, resolve_tac set_map, rtac subset_trans, etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]]]; in - (rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm o_id}) THEN' + (rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm comp_id}) THEN' rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN' stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' rtac mor_incl_min_alg THEN' stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)) 1 @@ -585,7 +585,7 @@ fun mk_ctor_map_unique_tac fold_unique sym_map_comps ctxt = rtac fold_unique 1 THEN - unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc[symmetric] id_o o_id}) THEN + unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN ALLGOALS atac; fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply, @@ -675,7 +675,7 @@ fun mk_map_id0_tac map_id0s unique = (rtac sym THEN' rtac unique THEN' EVERY' (map (fn thm => - EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id}, + EVERY' [rtac trans, rtac @{thm id_comp}, rtac trans, rtac sym, rtac @{thm comp_id}, rtac (thm RS sym RS arg_cong)]) map_id0s)) 1; fun mk_map_comp0_tac map_comp0s ctor_maps unique iplus1 = @@ -737,7 +737,7 @@ (in_Irels ~~ (active_set_map0s ~~ ctor_set_set_inclss)), CONJ_WRAP' (fn conv => EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, - REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, + REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]}, REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]), rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map, etac eq_arg_cong_ctor_dtor]) @@ -766,7 +766,7 @@ rtac conjI, REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2), rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, - REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, + REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]}, EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac, dtac @{thm ssubst_mem[OF pair_collapse]}, REPEAT_DETERM o diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_tactics.ML --- a/src/HOL/Tools/BNF/bnf_tactics.ML Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML Mon Jan 20 18:24:56 2014 +0100 @@ -58,7 +58,7 @@ fun mk_Abs_inj_thm inj = inj OF (replicate 2 UNIV_I); fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac surj THEN' etac exI) 1) - (Abs_inj_thm RS @{thm bijI}); + (Abs_inj_thm RS @{thm bijI'}); @@ -95,7 +95,7 @@ rtac refl 1; fun mk_map_comp_id_tac map_comp0 = - (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1; + (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm comp_id} THEN' rtac refl) 1; fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} = EVERY' [rtac mp, rtac map_cong0,