--- 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 \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
--- 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 =
--- 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,
--- 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'
--- 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};
--- 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;
--- 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");
--- 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 =
--- 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}),
--- 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");
--- 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 =
--- 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
--- 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,