# HG changeset patch # User blanchet # Date 1377808786 -7200 # Node ID 271b34513bfbbde3d744ae029079b9f1b5561fb2 # Parent 7422380afe235e26dda85c9f16862ef563d629d3 renamed BNF axiom diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_comp.ML --- 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)) diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_comp_tactics.ML --- 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, diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_def.ML --- 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 diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_def_tactics.ML --- 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 = _} = diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_gfp.ML --- 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' diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- 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}; diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_lfp.ML --- 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' diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- 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]}, diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_tactics.ML --- 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,