--- a/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 22:39:46 2013 +0200
@@ -153,12 +153,12 @@
mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
(map map_id0_of_bnf inners);
- fun map_comp_tac _ =
- mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
- (map map_comp_of_bnf inners);
+ fun map_comp0_tac _ =
+ mk_comp_map_comp0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer)
+ (map map_comp0_of_bnf inners);
fun mk_single_set_map_tac i _ =
- mk_comp_set_map_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
+ mk_comp_set_map_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer)
(collect_set_map_of_bnf outer)
(map ((fn thms => nth thms i) o set_map_of_bnf) inners);
@@ -233,7 +233,7 @@
rtac thm 1
end;
- val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -301,8 +301,8 @@
(Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
- fun map_comp_tac {context = ctxt, prems = _} =
- unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+ 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;
fun map_cong0_tac {context = ctxt, prems = _} =
mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
@@ -339,7 +339,7 @@
rtac thm 1
end;
- val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -391,8 +391,8 @@
val bd = mk_bd_of_bnf Ds As bnf;
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
- fun map_comp_tac {context = ctxt, prems = _} =
- unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+ 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;
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);
@@ -424,7 +424,7 @@
fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
- val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -475,7 +475,7 @@
val bd = mk_bd_of_bnf Ds As bnf;
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
- fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
+ fun map_comp0_tac _ = rtac (map_comp0_of_bnf bnf) 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_map_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf));
@@ -497,7 +497,7 @@
fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
- val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -630,7 +630,7 @@
(rtac (unfold_all thm) THEN'
SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
- val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
+ val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf))
(mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
(K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds)
(mk_tac (map_wpull_of_bnf bnf))
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -11,7 +11,7 @@
val mk_comp_bd_card_order_tac: thm list -> thm -> tactic
val mk_comp_bd_cinfinite_tac: thm -> thm -> tactic
val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
- val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic
+ val mk_comp_map_comp0_tac: thm -> thm -> thm list -> tactic
val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic
val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
@@ -62,17 +62,17 @@
EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1;
-fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps =
+fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s =
EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
- rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
- map (fn thm => rtac (thm RS sym RS fun_cong)) map_comps) 1;
+ rtac (Gmap_comp0 RS sym RS o_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_map_tac Gmap_comp Gmap_cong0 Gset_map set_maps =
+fun mk_comp_set_map_tac Gmap_comp0 Gmap_cong0 Gset_map set_maps =
EVERY' ([rtac ext] @
replicate 3 (rtac trans_o_apply) @
[rtac (arg_cong_Union RS trans),
rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
- rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans),
+ rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans),
rtac Gmap_cong0] @
map (fn thm => rtac (thm RS fun_cong)) set_maps @
[rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
--- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 22:39:46 2013 +0200
@@ -51,7 +51,7 @@
val in_mono_of_bnf: bnf -> thm
val in_rel_of_bnf: bnf -> thm
val map_comp'_of_bnf: bnf -> thm
- val map_comp_of_bnf: bnf -> thm
+ val map_comp0_of_bnf: bnf -> thm
val map_cong0_of_bnf: bnf -> thm
val map_cong_of_bnf: bnf -> thm
val map_def_of_bnf: bnf -> thm
@@ -114,7 +114,7 @@
type axioms = {
map_id0: thm,
- map_comp: thm,
+ map_comp0: thm,
map_cong0: thm,
set_map: thm list,
bd_card_order: thm,
@@ -125,7 +125,7 @@
};
fun mk_axioms' ((((((((id, comp), cong), nat), c_o), cinf), set_bd), wpull), rel) =
- {map_id0 = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
+ {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
bd_cinfinite = cinf, set_bd = set_bd, map_wpull = wpull, rel_OO_Grp = rel};
fun dest_cons [] = raise List.Empty
@@ -147,15 +147,15 @@
fun zip_axioms mid mcomp mcong snat bdco bdinf sbd wpull rel =
[mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [wpull, rel];
-fun dest_axioms {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun dest_axioms {map_id0, map_comp0, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
map_wpull, rel_OO_Grp} =
- zip_axioms map_id0 map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
+ zip_axioms map_id0 map_comp0 map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
rel_OO_Grp;
-fun map_axioms f {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun map_axioms f {map_id0, map_comp0, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
map_wpull, rel_OO_Grp} =
{map_id0 = f map_id0,
- map_comp = f map_comp,
+ map_comp0 = f map_comp0,
map_cong0 = f map_cong0,
set_map = map f set_map,
bd_card_order = f bd_card_order,
@@ -382,7 +382,7 @@
val map_def_of_bnf = #map_def o #defs o rep_bnf;
val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf;
val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf;
-val map_comp_of_bnf = #map_comp o #axioms o rep_bnf;
+val map_comp0_of_bnf = #map_comp0 o #axioms o rep_bnf;
val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
@@ -510,7 +510,7 @@
val in_relN = "in_rel";
val map_id0N = "map_id0";
val map_idN = "map_id";
-val map_compN = "map_comp";
+val map_comp0N = "map_comp0";
val map_comp'N = "map_comp'";
val map_cong0N = "map_cong0";
val map_congN = "map_cong";
@@ -558,7 +558,7 @@
(in_bdN, [Lazy.force (#in_bd facts)]),
(in_monoN, [Lazy.force (#in_mono facts)]),
(in_relN, [Lazy.force (#in_rel facts)]),
- (map_compN, [#map_comp axioms]),
+ (map_comp0N, [#map_comp0 axioms]),
(map_id0N, [#map_id0 axioms]),
(map_transferN, [Lazy.force (#map_transfer facts)]),
(map_wpullN, [#map_wpull axioms]),
@@ -850,7 +850,7 @@
mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA')
end;
- val map_comp_goal =
+ val map_comp0_goal =
let
val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs);
val comp_bnf_map_app = HOLogic.mk_comp
@@ -922,7 +922,7 @@
val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp));
- val goals = zip_axioms map_id0_goal map_comp_goal map_cong0_goal set_maps_goal
+ val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_maps_goal
card_order_bd_goal cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal;
fun mk_wit_goals (I, wit) =
@@ -1001,7 +1001,7 @@
val in_cong = Lazy.lazy mk_in_cong;
val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms));
- val map_comp' = Lazy.lazy (fn () => mk_map_comp' (#map_comp axioms));
+ val map_comp' = Lazy.lazy (fn () => mk_map_comp' (#map_comp0 axioms));
fun mk_map_cong () =
let
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -66,7 +66,7 @@
rtac set_map) set_maps) THEN'
rtac @{thm image_empty}) 1;
-fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp set_maps =
+fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp0 set_maps =
if null set_maps then
EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id0, rtac map_id0] 1
else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
@@ -76,13 +76,13 @@
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
set_maps,
- CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
- rtac (map_comp RS trans RS sym), rtac map_cong0,
+ CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp0 RS trans), rtac (map_comp0 RS trans),
+ rtac (map_comp0 RS trans RS sym), rtac map_cong0,
REPEAT_DETERM_N (length set_maps) o EVERY' [rtac (o_apply RS trans),
rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
-fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps
+fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp0 set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
@@ -95,7 +95,7 @@
EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I},
REPEAT_DETERM o
eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
- hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
+ hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac map_cong0,
REPEAT_DETERM_N n o EVERY' [rtac @{thm Collect_split_Grp_eqD}, etac @{thm set_mp}, atac],
rtac CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
@@ -105,7 +105,7 @@
hyp_subst_tac ctxt,
rtac @{thm relcomppI}, rtac @{thm conversepI},
EVERY' (map2 (fn convol => fn map_id0 =>
- EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id0]),
+ EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp0 RS sym, map_id0]),
REPEAT_DETERM_N n o rtac (convol RS fun_cong),
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac CollectI,
@@ -135,7 +135,7 @@
rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1
end;
-fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
+fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp0 set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
@@ -151,7 +151,7 @@
hyp_subst_tac ctxt, rtac @{thm conversepI}, rtac @{thm relcomppI}, rtac @{thm conversepI},
EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac sym, rtac trans,
rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
- rtac (map_comp RS sym), rtac CollectI,
+ rtac (map_comp0 RS sym), rtac CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
end;
@@ -161,7 +161,7 @@
rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono,
REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
-fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp set_maps
+fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp0 set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
@@ -180,20 +180,20 @@
eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
hyp_subst_tac ctxt,
rtac @{thm relcomppI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI},
- rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
+ rtac trans, rtac map_comp0, rtac sym, rtac map_cong0,
REPEAT_DETERM_N n o rtac @{thm fst_fstOp},
in_tac @{thm fstOp_in},
- rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
+ rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac map_cong0,
REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply,
rtac ballE, rtac subst,
rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE,
etac set_mp, atac],
in_tac @{thm fstOp_in},
rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI},
- rtac trans, rtac map_comp, rtac map_cong0,
+ rtac trans, rtac map_comp0, rtac map_cong0,
REPEAT_DETERM_N n o rtac o_apply,
in_tac @{thm sndOp_in},
- rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
+ rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac sym, rtac map_cong0,
REPEAT_DETERM_N n o rtac @{thm snd_sndOp},
in_tac @{thm sndOp_in},
rtac @{thm predicate2I},
@@ -206,7 +206,7 @@
rtac @{thm relcomppI}, rtac @{thm conversepI},
EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans,
rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
- rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
+ rtac (map_comp0 RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
end;
fun mk_in_rel_tac rel_OO_Gr {context = ctxt, prems = _} =
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 22:39:46 2013 +0200
@@ -214,8 +214,8 @@
val bd_Cinfinites = map bd_Cinfinite_of_bnf bnfs;
val bd_Cinfinite = hd bd_Cinfinites;
val in_monos = map in_mono_of_bnf bnfs;
- val map_comps = map map_comp_of_bnf bnfs;
- val sym_map_comps = map mk_sym map_comps;
+ val map_comp0s = map map_comp0_of_bnf bnfs;
+ val sym_map_comps = map mk_sym map_comp0s;
val map_comp's = map map_comp'_of_bnf bnfs;
val map_cong0s = map map_cong0_of_bnf bnfs;
val map_id0s = map map_id0_of_bnf bnfs;
@@ -237,7 +237,7 @@
(*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) =
map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
- fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp =
+ fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 =
let
val lhs = Term.list_comb (mapBsCs, all_gs) $
(Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
@@ -246,7 +246,7 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
- (K (mk_map_comp_id_tac map_comp))
+ (K (mk_map_comp_id_tac map_comp0))
|> Thm.close_derivation
end;
@@ -2193,7 +2193,7 @@
map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
end;
- val map_comp_thms =
+ val map_comp0_thms =
let
val goal = fold_rev Logic.all (fs @ gs)
(HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -2202,7 +2202,7 @@
fs_maps gs_maps fgs_maps)))
in
split_conj_thm (Goal.prove_sorry lthy [] [] goal
- (K (mk_map_comp_tac m n map_thms map_comps map_cong0s dtor_unfold_unique_thm))
+ (K (mk_map_comp0_tac m n map_thms map_comp0s map_cong0s dtor_unfold_unique_thm))
|> Thm.close_derivation)
end;
@@ -2459,7 +2459,7 @@
val map_id0_tacs =
map2 (K oo mk_map_id0_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms;
- val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms;
+ val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp0_thms;
val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
val set_nat_tacss =
map2 (map2 (K oo mk_set_map_tac)) hset_defss (transpose col_natural_thmss);
@@ -2476,7 +2476,7 @@
val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
- val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
+ val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss
bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs;
val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
@@ -2699,11 +2699,11 @@
(mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz')));
val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
in
- map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 =>
+ map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets
+ (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets
dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss))
|> Thm.close_derivation)
ks goals in_rels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -52,7 +52,7 @@
val mk_incl_lsbis_tac: int -> int -> thm -> tactic
val mk_length_Lev'_tac: thm -> tactic
val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
- val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
+ val mk_map_comp0_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
thm list list -> thm list list -> thm list list list -> tactic
val mk_map_id0_tac: thm list -> thm -> thm -> tactic
@@ -256,19 +256,19 @@
(rev ((1 upto n) ~~ (active_set_maps ~~ coalg_sets)))])
(rec_Sucs ~~ (morEs ~~ (map (chop m) set_mapss ~~ map (drop m) coalg_setss)))] 1;
-fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comps map_cong0s set_mapss =
+fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comp0s map_cong0s set_mapss =
let
val n = length rel_OO_Grps;
- val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ rel_OO_Grps);
+ val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_mapss ~~ rel_OO_Grps);
- fun mk_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) =
+ fun mk_if_tac ((((i, map_comp0), map_cong0), set_maps), rel_OO_Grp) =
EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
rtac (rel_OO_Grp RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
rtac @{thm relcomppI}, rtac @{thm conversepI},
EVERY' (map (fn thm =>
EVERY' [rtac @{thm GrpI},
- rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
+ 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 o eresolve_tac [CollectE, conjE], rtac CollectI,
CONJ_WRAP' (fn (i, thm) =>
@@ -281,17 +281,17 @@
(1 upto (m + n) ~~ set_maps)])
@{thms fst_diag_id snd_diag_id})];
- fun mk_only_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) =
+ fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_maps), rel_OO_Grp) =
EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
etac allE, etac allE, etac impE, atac,
dtac (rel_OO_Grp RS @{thm eq_refl} RS @{thm predicate2D}),
REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @
@{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}),
hyp_subst_tac ctxt,
- rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+ 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),
- atac, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+ 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),
rtac trans, rtac map_cong0,
@@ -1034,20 +1034,20 @@
EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps),
rtac unfold_dtor] 1;
-fun mk_map_comp_tac m n maps map_comps map_cong0s unfold_unique =
+fun mk_map_comp0_tac m n maps map_comp0s map_cong0s unfold_unique =
EVERY' [rtac unfold_unique,
- EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong0 =>
+ EVERY' (map3 (fn map_thm => fn map_comp0 => fn map_cong0 =>
EVERY' (map rtac
([@{thm o_assoc} RS trans,
- @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
+ @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans,
@{thm o_assoc} RS trans RS sym,
@{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 arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
+ @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans,
ext, o_apply RS trans, o_apply RS trans RS sym, map_cong0] @
replicate m (@{thm id_o} RS fun_cong) @
replicate n (@{thm o_id} RS fun_cong))))
- maps map_comps map_cong0s)] 1;
+ maps map_comp0s map_cong0s)] 1;
fun mk_mcong_tac ctxt m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
set_hset_hsetsss =
@@ -1177,38 +1177,38 @@
(drop m set_maps)])
(map_wpulls ~~ (pickWP_assms_tacs ~~ set_mapss)) 1;
-fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs
+fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comp0s pickWP_assms_tacs
{context = ctxt, prems = _: thm list} =
let
- val n = length map_comps;
+ val n = length map_comp0s;
in
unfold_thms_tac ctxt [mor_def] THEN
EVERY' [rtac conjI,
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
- CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
+ CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp0)) =>
EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
hyp_subst_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
- rtac (map_comp RS trans),
+ rtac (map_comp0 RS trans),
SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
pickWP_assms_tac])
- (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1
+ (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comp0s))] 1
end;
val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)};
val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
-fun mk_mor_thePull_pick_tac mor_def unfolds map_comps {context = ctxt, prems = _} =
+fun mk_mor_thePull_pick_tac mor_def unfolds map_comp0s {context = ctxt, prems = _} =
unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
- CONJ_WRAP' (fn (unfold, map_comp) =>
+ CONJ_WRAP' (fn (unfold, map_comp0) =>
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
hyp_subst_tac ctxt,
- SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
+ SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp0 :: @{thms comp_def id_def})),
rtac refl])
- (unfolds ~~ map_comps) 1;
+ (unfolds ~~ map_comp0s) 1;
fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_mapss map_wpulls pickWP_assms_tacs
{context = ctxt, prems = _} =
@@ -1287,7 +1287,7 @@
ALLGOALS (TRY o
FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
-fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets dtor_inject
+fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject
dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss =
let
val m = length dtor_set_incls;
@@ -1309,7 +1309,7 @@
rtac conjI, rtac refl, rtac refl])
(in_Jrels ~~ (active_set_maps ~~ dtor_set_set_inclss)),
CONJ_WRAP' (fn conv =>
- EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+ 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 n o EVERY' (map rtac [trans, o_apply, conv]),
rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
@@ -1339,7 +1339,7 @@
(dtor_sets ~~ passive_set_maps),
rtac conjI,
REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
- rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
+ 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]},
EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
dtac @{thm ssubst_mem[OF pair_collapse]},
@@ -1352,22 +1352,22 @@
EVERY' [rtac iffI, if_tac, only_if_tac] 1
end;
-fun mk_rel_coinduct_coind_tac m coinduct ks map_comps map_congs map_arg_congs set_mapss
+fun mk_rel_coinduct_coind_tac m coinduct ks map_comp0s map_congs map_arg_congs set_mapss
dtor_unfolds dtor_maps {context = ctxt, prems = _} =
let val n = length ks;
in
EVERY' [DETERM o rtac coinduct,
- EVERY' (map7 (fn i => fn map_comp => fn map_cong => fn map_arg_cong => fn set_maps =>
+ EVERY' (map7 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_maps =>
fn dtor_unfold => fn dtor_map =>
EVERY' [REPEAT_DETERM o eresolve_tac [exE, conjE],
select_prem_tac (length ks) (dtac @{thm spec2}) i, dtac mp, atac,
REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
rtac exI, rtac conjI, rtac conjI,
- rtac (map_comp RS trans), rtac (dtor_map RS trans RS sym),
- rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp, map_cong]),
+ 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 n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}),
- rtac (map_comp RS trans), rtac (map_cong RS trans),
+ 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 n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}),
etac (@{thm prod.cases} RS map_arg_cong RS trans),
@@ -1380,7 +1380,7 @@
hyp_subst_tac ctxt, rtac exI, rtac conjI, etac Collect_splitD_set_mp, atac,
rtac (o_apply RS trans), rtac (@{thm surjective_pairing} RS arg_cong)])
(drop m set_maps)])
- ks map_comps map_congs map_arg_congs set_mapss dtor_unfolds dtor_maps)] 1
+ ks map_comp0s map_congs map_arg_congs set_mapss dtor_unfolds dtor_maps)] 1
end;
val split_id_unfolds = @{thms prod.cases image_id id_apply};
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 22:39:46 2013 +0200
@@ -159,7 +159,7 @@
map (fn thm => ctrans OF [thm, bd0_Card_order RS @{thm ordLeq_csum1}]) set_bd0s)
set_bd0ss bd0_Card_orders;
val in_bds = map in_bd_of_bnf bnfs;
- val sym_map_comps = map (fn bnf => map_comp_of_bnf bnf RS sym) bnfs;
+ val sym_map_comps = map (fn bnf => map_comp0_of_bnf bnf RS sym) bnfs;
val map_comp's = map map_comp'_of_bnf bnfs;
val map_cong0s = map map_cong0_of_bnf bnfs;
val map_id0s = map map_id0_of_bnf bnfs;
@@ -194,7 +194,7 @@
(*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) =
map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
- fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp =
+ fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 =
let
val lhs = Term.list_comb (mapBsCs, all_gs) $
(Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
@@ -203,7 +203,7 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
- (K (mk_map_comp_id_tac map_comp))
+ (K (mk_map_comp_id_tac map_comp0))
|> Thm.close_derivation
end;
@@ -1692,8 +1692,8 @@
val timer = time (timer "helpers for BNF properties");
val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_map_unique_thms;
- val map_comp_tacs =
- map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks;
+ val map_comp0_tacs =
+ map2 (K oo mk_map_comp0_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks;
val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
val set_nat_tacss = map (map (K o mk_set_map_tac)) (transpose set_map_thmss);
val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
@@ -1703,7 +1703,7 @@
val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
- val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
+ val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss
bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs;
val ctor_witss =
@@ -1773,11 +1773,11 @@
(mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF));
val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
in
- map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 =>
+ map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets
+ (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets
ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss))
|> Thm.close_derivation)
ks goals in_rels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -39,7 +39,7 @@
val mk_least_min_alg_tac: thm -> thm -> tactic
val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list ->
thm list list -> thm list list list -> thm list -> tactic
- val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic
+ val mk_map_comp0_tac: thm list -> thm list -> thm -> int -> tactic
val mk_map_id0_tac: thm list -> thm -> tactic
val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic
@@ -710,11 +710,11 @@
EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id},
rtac (thm RS sym RS arg_cong)]) map_id0s)) 1;
-fun mk_map_comp_tac map_comps ctor_maps unique iplus1 =
+fun mk_map_comp0_tac map_comp0s ctor_maps unique iplus1 =
let
val i = iplus1 - 1;
val unique' = Thm.permute_prems 0 i unique;
- val map_comps' = drop i map_comps @ take i map_comps;
+ val map_comps' = drop i map_comp0s @ take i map_comp0s;
val ctor_maps' = drop i ctor_maps @ take i ctor_maps;
fun mk_comp comp simp =
EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac o_apply,
@@ -746,7 +746,7 @@
EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
REPEAT_DETERM_N n o etac UnE]))))] 1);
-fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets ctor_inject
+fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject
ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss =
let
val m = length ctor_set_incls;
@@ -773,7 +773,7 @@
rtac conjI, rtac refl, rtac refl])
(in_Irels ~~ (active_set_maps ~~ ctor_set_set_inclss)),
CONJ_WRAP' (fn conv =>
- EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+ 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 n o EVERY' (map rtac [trans, o_apply, conv]),
rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map,
@@ -802,7 +802,7 @@
(ctor_sets ~~ passive_set_maps),
rtac conjI,
REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
- rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+ rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
dtac @{thm ssubst_mem[OF pair_collapse]},
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -106,8 +106,8 @@
split_conv}) THEN
rtac refl 1;
-fun mk_map_comp_id_tac map_comp =
- (rtac trans THEN' rtac map_comp THEN' REPEAT_DETERM o stac @{thm o_id} THEN' 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;
fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
EVERY' [rtac mp, rtac map_cong0,