renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
authorblanchet
Wed Apr 24 14:15:01 2013 +0200 (2013-04-24)
changeset 517614c9f08836d87
parent 51760 e5ce85418346
child 51762 219a3063ed29
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_comp_tactics.ML
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_def_tactics.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_gfp_tactics.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_lfp_tactics.ML
src/HOL/BNF/Tools/bnf_tactics.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 14:14:36 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 14:15:01 2013 +0200
     1.3 @@ -150,15 +150,15 @@
     1.4      val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
     1.5  
     1.6      fun map_id_tac _ =
     1.7 -      mk_comp_map_id_tac (map_id_of_bnf outer) (map_cong_of_bnf outer)
     1.8 +      mk_comp_map_id_tac (map_id_of_bnf outer) (map_cong0_of_bnf outer)
     1.9          (map map_id_of_bnf inners);
    1.10  
    1.11      fun map_comp_tac _ =
    1.12 -      mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
    1.13 +      mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
    1.14          (map map_comp_of_bnf inners);
    1.15  
    1.16      fun mk_single_set_natural_tac i _ =
    1.17 -      mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
    1.18 +      mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
    1.19          (collect_set_natural_of_bnf outer)
    1.20          (map ((fn thms => nth thms i) o set_natural_of_bnf) inners);
    1.21  
    1.22 @@ -181,8 +181,8 @@
    1.23            |> Thm.close_derivation)
    1.24          (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
    1.25  
    1.26 -    fun map_cong_tac _ =
    1.27 -      mk_comp_map_cong_tac set_alt_thms (map_cong_of_bnf outer) (map map_cong_of_bnf inners);
    1.28 +    fun map_cong0_tac _ =
    1.29 +      mk_comp_map_cong0_tac set_alt_thms (map_cong0_of_bnf outer) (map map_cong0_of_bnf inners);
    1.30  
    1.31      val set_bd_tacs =
    1.32        if ! quick_and_dirty then
    1.33 @@ -238,7 +238,7 @@
    1.34          unfold_thms_tac lthy basic_thms THEN rtac thm 1
    1.35        end;
    1.36  
    1.37 -    val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
    1.38 +    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
    1.39        bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
    1.40  
    1.41      val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
    1.42 @@ -309,8 +309,8 @@
    1.43      fun map_comp_tac {context = ctxt, prems = _} =
    1.44        unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
    1.45        rtac refl 1;
    1.46 -    fun map_cong_tac {context = ctxt, prems = _} =
    1.47 -      mk_kill_map_cong_tac ctxt n (live - n) (map_cong_of_bnf bnf);
    1.48 +    fun map_cong0_tac {context = ctxt, prems = _} =
    1.49 +      mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
    1.50      val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
    1.51      fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
    1.52      fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
    1.53 @@ -348,7 +348,7 @@
    1.54          rtac thm 1
    1.55        end;
    1.56  
    1.57 -    val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
    1.58 +    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
    1.59        bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
    1.60  
    1.61      val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
    1.62 @@ -403,8 +403,8 @@
    1.63      fun map_comp_tac {context = ctxt, prems = _} =
    1.64        unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
    1.65        rtac refl 1;
    1.66 -    fun map_cong_tac {context = ctxt, prems = _} =
    1.67 -      rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    1.68 +    fun map_cong0_tac {context = ctxt, prems = _} =
    1.69 +      rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    1.70      val set_natural_tacs =
    1.71        if ! quick_and_dirty then
    1.72          replicate (n + live) (K all_tac)
    1.73 @@ -435,7 +435,7 @@
    1.74      fun srel_O_Gr_tac _ =
    1.75        mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
    1.76  
    1.77 -    val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
    1.78 +    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
    1.79        bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
    1.80  
    1.81      val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
    1.82 @@ -488,8 +488,8 @@
    1.83  
    1.84      fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
    1.85      fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
    1.86 -    fun map_cong_tac {context = ctxt, prems = _} =
    1.87 -      rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    1.88 +    fun map_cong0_tac {context = ctxt, prems = _} =
    1.89 +      rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    1.90      val set_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf));
    1.91      fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
    1.92      fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
    1.93 @@ -512,7 +512,7 @@
    1.94      fun srel_O_Gr_tac _ =
    1.95        mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
    1.96  
    1.97 -    val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
    1.98 +    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
    1.99        bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
   1.100  
   1.101      val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   1.102 @@ -653,7 +653,7 @@
   1.103        SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
   1.104  
   1.105      val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
   1.106 -      (mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
   1.107 +      (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
   1.108        (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
   1.109        (mk_tac (map_wpull_of_bnf bnf))
   1.110        (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf)));
     2.1 --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Wed Apr 24 14:14:36 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Wed Apr 24 14:15:01 2013 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4    val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
     2.5    val mk_comp_in_bd_tac: thm -> thm list -> thm -> thm list -> thm -> tactic
     2.6    val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic
     2.7 -  val mk_comp_map_cong_tac: thm list -> thm -> thm list -> tactic
     2.8 +  val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
     2.9    val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic
    2.10    val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
    2.11    val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
    2.12 @@ -24,7 +24,7 @@
    2.13    val mk_kill_bd_cinfinite_tac: thm -> tactic
    2.14    val kill_in_alt_tac: tactic
    2.15    val mk_kill_in_bd_tac: int -> bool -> thm -> thm -> thm -> thm -> thm -> tactic
    2.16 -  val mk_kill_map_cong_tac: Proof.context -> int -> int -> thm -> tactic
    2.17 +  val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic
    2.18    val mk_kill_set_bd_tac: thm -> thm -> tactic
    2.19  
    2.20    val empty_natural_tac: tactic
    2.21 @@ -69,22 +69,22 @@
    2.22    unfold_thms_tac ctxt [collect_set_natural RS sym] THEN
    2.23    rtac refl 1;
    2.24  
    2.25 -fun mk_comp_map_id_tac Gmap_id Gmap_cong map_ids =
    2.26 -  EVERY' ([rtac ext, rtac (Gmap_cong RS trans)] @
    2.27 +fun mk_comp_map_id_tac Gmap_id Gmap_cong0 map_ids =
    2.28 +  EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
    2.29      map (fn thm => rtac (thm RS fun_cong)) map_ids @ [rtac (Gmap_id RS fun_cong)]) 1;
    2.30  
    2.31 -fun mk_comp_map_comp_tac Gmap_comp Gmap_cong map_comps =
    2.32 +fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps =
    2.33    EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
    2.34 -    rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong] @
    2.35 +    rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
    2.36      map (fn thm => rtac (thm RS sym RS fun_cong)) map_comps) 1;
    2.37  
    2.38 -fun mk_comp_set_natural_tac Gmap_comp Gmap_cong Gset_natural set_naturals =
    2.39 +fun mk_comp_set_natural_tac Gmap_comp Gmap_cong0 Gset_natural set_naturals =
    2.40    EVERY' ([rtac ext] @
    2.41      replicate 3 (rtac trans_o_apply) @
    2.42      [rtac (arg_cong_Union RS trans),
    2.43       rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
    2.44       rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans),
    2.45 -     rtac Gmap_cong] @
    2.46 +     rtac Gmap_cong0] @
    2.47       map (fn thm => rtac (thm RS fun_cong)) set_naturals @
    2.48       [rtac (Gset_natural RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
    2.49       rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
    2.50 @@ -98,14 +98,14 @@
    2.51          rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],
    2.52       rtac @{thm image_empty}]) 1;
    2.53  
    2.54 -fun mk_comp_map_cong_tac comp_set_alts map_cong map_congs =
    2.55 +fun mk_comp_map_cong0_tac comp_set_alts map_cong0 map_cong0s =
    2.56    let
    2.57       val n = length comp_set_alts;
    2.58    in
    2.59      (if n = 0 then rtac refl 1
    2.60 -    else rtac map_cong 1 THEN
    2.61 -      EVERY' (map_index (fn (i, map_cong) =>
    2.62 -        rtac map_cong THEN' EVERY' (map_index (fn (k, set_alt) =>
    2.63 +    else rtac map_cong0 1 THEN
    2.64 +      EVERY' (map_index (fn (i, map_cong0) =>
    2.65 +        rtac map_cong0 THEN' EVERY' (map_index (fn (k, set_alt) =>
    2.66            EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac meta_mp,
    2.67              rtac (equalityD2 RS set_mp), rtac (set_alt RS fun_cong RS trans),
    2.68              rtac trans_o_apply, rtac (@{thm collect_def} RS arg_cong_Union),
    2.69 @@ -113,7 +113,7 @@
    2.70              rtac @{thm insertI1}, rtac (o_apply RS equalityD2 RS set_mp),
    2.71              etac @{thm imageI}, atac])
    2.72            comp_set_alts))
    2.73 -      map_congs) 1)
    2.74 +      map_cong0s) 1)
    2.75    end;
    2.76  
    2.77  fun mk_comp_bd_card_order_tac Fbd_card_orders Gbd_card_order =
    2.78 @@ -233,8 +233,8 @@
    2.79  
    2.80  (* Kill operation *)
    2.81  
    2.82 -fun mk_kill_map_cong_tac ctxt n m map_cong =
    2.83 -  (rtac map_cong THEN' EVERY' (replicate n (rtac refl)) THEN'
    2.84 +fun mk_kill_map_cong0_tac ctxt n m map_cong0 =
    2.85 +  (rtac map_cong0 THEN' EVERY' (replicate n (rtac refl)) THEN'
    2.86      EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1;
    2.87  
    2.88  fun mk_kill_bd_card_order_tac n bd_card_order =
     3.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 14:14:36 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 14:15:01 2013 +0200
     3.3 @@ -52,7 +52,7 @@
     3.4    val in_srel_of_bnf: BNF -> thm
     3.5    val map_comp'_of_bnf: BNF -> thm
     3.6    val map_comp_of_bnf: BNF -> thm
     3.7 -  val map_cong_of_bnf: BNF -> thm
     3.8 +  val map_cong0_of_bnf: BNF -> thm
     3.9    val map_def_of_bnf: BNF -> thm
    3.10    val map_id'_of_bnf: BNF -> thm
    3.11    val map_id_of_bnf: BNF -> thm
    3.12 @@ -107,7 +107,7 @@
    3.13  type axioms = {
    3.14    map_id: thm,
    3.15    map_comp: thm,
    3.16 -  map_cong: thm,
    3.17 +  map_cong0: thm,
    3.18    set_natural: thm list,
    3.19    bd_card_order: thm,
    3.20    bd_cinfinite: thm,
    3.21 @@ -118,7 +118,7 @@
    3.22  };
    3.23  
    3.24  fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), srel) =
    3.25 -  {map_id = id, map_comp = comp, map_cong = cong, set_natural = nat, bd_card_order = c_o,
    3.26 +  {map_id = id, map_comp = comp, map_cong0 = cong, set_natural = nat, bd_card_order = c_o,
    3.27     bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, srel_O_Gr = srel};
    3.28  
    3.29  fun dest_cons [] = raise Empty
    3.30 @@ -141,16 +141,16 @@
    3.31  fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull srel =
    3.32    [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, srel];
    3.33  
    3.34 -fun dest_axioms {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
    3.35 +fun dest_axioms {map_id, map_comp, map_cong0, set_natural, bd_card_order, bd_cinfinite, set_bd,
    3.36    in_bd, map_wpull, srel_O_Gr} =
    3.37 -  zip_axioms map_id map_comp map_cong set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull
    3.38 +  zip_axioms map_id map_comp map_cong0 set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull
    3.39      srel_O_Gr;
    3.40  
    3.41 -fun map_axioms f {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
    3.42 +fun map_axioms f {map_id, map_comp, map_cong0, set_natural, bd_card_order, bd_cinfinite, set_bd,
    3.43    in_bd, map_wpull, srel_O_Gr} =
    3.44    {map_id = f map_id,
    3.45      map_comp = f map_comp,
    3.46 -    map_cong = f map_cong,
    3.47 +    map_cong0 = f map_cong0,
    3.48      set_natural = map f set_natural,
    3.49      bd_card_order = f bd_card_order,
    3.50      bd_cinfinite = f bd_cinfinite,
    3.51 @@ -371,7 +371,7 @@
    3.52  val map_id'_of_bnf = Lazy.force o #map_id' o #facts o rep_bnf;
    3.53  val map_comp_of_bnf = #map_comp o #axioms o rep_bnf;
    3.54  val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
    3.55 -val map_cong_of_bnf = #map_cong o #axioms o rep_bnf;
    3.56 +val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
    3.57  val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
    3.58  val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
    3.59  val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
    3.60 @@ -507,7 +507,7 @@
    3.61  val map_id'N = "map_id'";
    3.62  val map_compN = "map_comp";
    3.63  val map_comp'N = "map_comp'";
    3.64 -val map_congN = "map_cong";
    3.65 +val map_cong0N = "map_cong0";
    3.66  val map_wpullN = "map_wpull";
    3.67  val rel_eqN = "rel_eq";
    3.68  val rel_flipN = "rel_flip";
    3.69 @@ -814,7 +814,7 @@
    3.70          fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
    3.71        end;
    3.72  
    3.73 -    val map_cong_goal =
    3.74 +    val map_cong0_goal =
    3.75        let
    3.76          fun mk_prem z set f f_copy =
    3.77            Logic.all z (Logic.mk_implies
    3.78 @@ -890,7 +890,7 @@
    3.79  
    3.80      val srel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (srel, Rs), O_Gr));
    3.81  
    3.82 -    val goals = zip_axioms map_id_goal map_comp_goal map_cong_goal set_naturals_goal
    3.83 +    val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_naturals_goal
    3.84        card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal srel_O_Gr_goal;
    3.85  
    3.86      fun mk_wit_goals (I, wit) =
    3.87 @@ -1004,7 +1004,7 @@
    3.88                  (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))
    3.89            in
    3.90              Goal.prove_sorry lthy [] [] goal
    3.91 -              (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong axioms)
    3.92 +              (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong0 axioms)
    3.93                  (#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_natural'))
    3.94              |> Thm.close_derivation
    3.95            end;
    3.96 @@ -1020,7 +1020,7 @@
    3.97              val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
    3.98            in
    3.99              Goal.prove_sorry lthy [] [] goal
   3.100 -              (mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong axioms) (Lazy.force map_id')
   3.101 +              (mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id')
   3.102                  (Lazy.force map_comp') (map Lazy.force set_natural'))
   3.103              |> Thm.close_derivation
   3.104            end;
   3.105 @@ -1074,7 +1074,7 @@
   3.106              val rhs = mk_converse (Term.list_comb (srel, Rs));
   3.107              val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_subset lhs rhs));
   3.108              val le_thm = Goal.prove_sorry lthy [] [] le_goal
   3.109 -              (mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong axioms)
   3.110 +              (mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms)
   3.111                  (Lazy.force map_comp') (map Lazy.force set_natural'))
   3.112                |> Thm.close_derivation
   3.113              val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
   3.114 @@ -1094,7 +1094,7 @@
   3.115              val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
   3.116            in
   3.117              Goal.prove_sorry lthy [] [] goal
   3.118 -              (mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong axioms)
   3.119 +              (mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms)
   3.120                  (Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_natural'))
   3.121              |> Thm.close_derivation
   3.122            end;
   3.123 @@ -1201,7 +1201,7 @@
   3.124                  let
   3.125                    val notes =
   3.126                      [(map_comp'N, [Lazy.force (#map_comp' facts)]),
   3.127 -                    (map_congN, [#map_cong axioms]),
   3.128 +                    (map_cong0N, [#map_cong0 axioms]),
   3.129                      (map_id'N, [Lazy.force (#map_id' facts)]),
   3.130                      (rel_eqN, [Lazy.force (#rel_eq facts)]),
   3.131                      (rel_flipN, [Lazy.force (#rel_flip facts)]),
     4.1 --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Apr 24 14:14:36 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Apr 24 14:15:01 2013 +0200
     4.3 @@ -51,7 +51,7 @@
     4.4      rtac set_natural) set_naturals) THEN'
     4.5    rtac @{thm image_empty}) 1;
     4.6  
     4.7 -fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals =
     4.8 +fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_naturals =
     4.9    if null set_naturals then
    4.10      EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1
    4.11    else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
    4.12 @@ -62,12 +62,12 @@
    4.13        rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
    4.14        set_naturals,
    4.15      CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
    4.16 -      rtac (map_comp RS trans RS sym), rtac map_cong,
    4.17 +      rtac (map_comp RS trans RS sym), rtac map_cong0,
    4.18        REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans),
    4.19          rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
    4.20          rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
    4.21  
    4.22 -fun mk_srel_Gr_tac srel_O_Grs map_id map_cong map_id' map_comp set_naturals
    4.23 +fun mk_srel_Gr_tac srel_O_Grs map_id map_cong0 map_id' map_comp set_naturals
    4.24    {context = ctxt, prems = _} =
    4.25    let
    4.26      val n = length set_naturals;
    4.27 @@ -80,7 +80,7 @@
    4.28          REPEAT_DETERM o dtac Pair_eqD,
    4.29          REPEAT_DETERM o etac conjE, hyp_subst_tac,
    4.30          rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
    4.31 -        rtac sym, rtac trans, rtac map_comp, rtac map_cong,
    4.32 +        rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
    4.33          REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
    4.34            REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
    4.35            rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
    4.36 @@ -97,7 +97,7 @@
    4.37          EVERY' (map2 (fn convol => fn map_id =>
    4.38            EVERY' [rtac CollectI, rtac exI, rtac conjI,
    4.39              rtac Pair_eqI, rtac conjI, rtac refl, rtac sym,
    4.40 -            rtac (box_equals OF [map_cong, map_comp RS sym, map_id]),
    4.41 +            rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]),
    4.42              REPEAT_DETERM_N n o rtac (convol RS fun_cong),
    4.43              REPEAT_DETERM o eresolve_tac [CollectE, conjE],
    4.44              rtac CollectI,
    4.45 @@ -121,7 +121,7 @@
    4.46        rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
    4.47        rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
    4.48  
    4.49 -fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong map_comp set_naturals
    4.50 +fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong0 map_comp set_naturals
    4.51    {context = ctxt, prems = _} =
    4.52    let
    4.53      val n = length set_naturals;
    4.54 @@ -136,7 +136,7 @@
    4.55          rtac @{thm relcompI}, rtac @{thm converseI},
    4.56          EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
    4.57            rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans,
    4.58 -          rtac map_cong, REPEAT_DETERM_N n o rtac thm,
    4.59 +          rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
    4.60            rtac (map_comp RS sym), rtac CollectI,
    4.61            CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
    4.62              etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
    4.63 @@ -146,7 +146,7 @@
    4.64    EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
    4.65      rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
    4.66  
    4.67 -fun mk_srel_O_tac srel_O_Grs srel_Id map_cong map_wppull map_comp set_naturals
    4.68 +fun mk_srel_O_tac srel_O_Grs srel_Id map_cong0 map_wppull map_comp set_naturals
    4.69    {context = ctxt, prems = _} =
    4.70    let
    4.71      val n = length set_naturals;
    4.72 @@ -162,22 +162,22 @@
    4.73          REPEAT_DETERM o etac conjE, hyp_subst_tac,
    4.74          rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
    4.75          rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
    4.76 -        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
    4.77 +        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
    4.78          REPEAT_DETERM_N n o rtac @{thm fst_fstO},
    4.79          in_tac @{thm fstO_in},
    4.80          rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
    4.81 -        rtac sym, rtac trans, rtac map_comp, rtac map_cong,
    4.82 +        rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
    4.83          REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst,
    4.84            rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE,
    4.85            etac set_mp, atac],
    4.86          in_tac @{thm fstO_in},
    4.87          rtac @{thm relcompI}, rtac @{thm converseI},
    4.88          rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
    4.89 -        rtac sym, rtac trans, rtac map_comp, rtac map_cong,
    4.90 +        rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
    4.91          REPEAT_DETERM_N n o rtac o_apply,
    4.92          in_tac @{thm sndO_in},
    4.93          rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
    4.94 -        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
    4.95 +        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
    4.96          REPEAT_DETERM_N n o rtac @{thm snd_sndO},
    4.97          in_tac @{thm sndO_in},
    4.98          rtac @{thm subrelI},
    4.99 @@ -192,7 +192,7 @@
   4.100          rtac @{thm relcompI}, rtac @{thm converseI},
   4.101          EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
   4.102            rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans,
   4.103 -          rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm,
   4.104 +          rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
   4.105            rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
   4.106    end;
   4.107  
     5.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 14:14:36 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 14:15:01 2013 +0200
     5.3 @@ -222,7 +222,7 @@
     5.4      val map_comps = map map_comp_of_bnf bnfs;
     5.5      val sym_map_comps = map (fn thm => thm RS sym) map_comps;
     5.6      val map_comp's = map map_comp'_of_bnf bnfs;
     5.7 -    val map_congs = map map_cong_of_bnf bnfs;
     5.8 +    val map_cong0s = map map_cong0_of_bnf bnfs;
     5.9      val map_ids = map map_id_of_bnf bnfs;
    5.10      val map_id's = map map_id'_of_bnf bnfs;
    5.11      val map_wpulls = map map_wpull_of_bnf bnfs;
    5.12 @@ -260,7 +260,7 @@
    5.13  
    5.14      (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
    5.15        map id ... id f(m+1) ... f(m+n) x = x*)
    5.16 -    fun mk_map_congL x mapAsAs sets map_cong map_id' =
    5.17 +    fun mk_map_cong0L x mapAsAs sets map_cong0 map_id' =
    5.18        let
    5.19          fun mk_prem set f z z' =
    5.20            HOLogic.mk_Trueprop
    5.21 @@ -270,11 +270,11 @@
    5.22        in
    5.23          Goal.prove_sorry lthy [] []
    5.24            (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
    5.25 -          (K (mk_map_congL_tac m map_cong map_id'))
    5.26 +          (K (mk_map_cong0L_tac m map_cong0 map_id'))
    5.27          |> Thm.close_derivation
    5.28        end;
    5.29  
    5.30 -    val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
    5.31 +    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_id's;
    5.32      val in_mono'_thms = map (fn thm =>
    5.33        (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos;
    5.34  
    5.35 @@ -866,7 +866,7 @@
    5.36          Goal.prove_sorry lthy [] []
    5.37            (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
    5.38              (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
    5.39 -          (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_congs set_natural'ss))
    5.40 +          (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_cong0s set_natural'ss))
    5.41          |> Thm.close_derivation
    5.42        end;
    5.43  
    5.44 @@ -1770,7 +1770,7 @@
    5.45            to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
    5.46            length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
    5.47            set_rv_Lev_thmsss set_Lev_thmsss set_image_Lev_thmsss
    5.48 -          set_natural'ss coalg_set_thmss map_comp_id_thms map_congs map_arg_cong_thms)
    5.49 +          set_natural'ss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms)
    5.50        |> Thm.close_derivation;
    5.51  
    5.52      val timer = time (timer "Behavioral morphism");
    5.53 @@ -1799,11 +1799,11 @@
    5.54  
    5.55          val goals = map3 mk_goal (map (mk_LSBIS As) ks) final_maps strTAs;
    5.56        in
    5.57 -        map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong =>
    5.58 +        map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
    5.59            Goal.prove_sorry lthy [] [] goal
    5.60 -            (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBIS_thms))
    5.61 +            (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBIS_thms))
    5.62            |> Thm.close_derivation)
    5.63 -        goals lsbisE_thms map_comp_id_thms map_congs
    5.64 +        goals lsbisE_thms map_comp_id_thms map_cong0s
    5.65        end;
    5.66  
    5.67      val coalg_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
    5.68 @@ -1919,7 +1919,7 @@
    5.69            Goal.prove_sorry lthy [] []
    5.70              (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
    5.71              (mk_mor_Rep_tac m (mor_def :: dtor_defs) Reps Abs_inverses coalg_final_set_thmss
    5.72 -              map_comp_id_thms map_congL_thms)
    5.73 +              map_comp_id_thms map_cong0L_thms)
    5.74            |> Thm.close_derivation;
    5.75  
    5.76          val mor_Abs =
    5.77 @@ -1974,7 +1974,7 @@
    5.78            (fold_rev Logic.all ss
    5.79              (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks))))
    5.80            (K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs'
    5.81 -            map_comp_id_thms map_congs))
    5.82 +            map_comp_id_thms map_cong0s))
    5.83          |> Thm.close_derivation
    5.84        end;
    5.85      val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
    5.86 @@ -2084,11 +2084,11 @@
    5.87           mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
    5.88          val goals = map3 mk_goal dtors ctors FTs;
    5.89        in
    5.90 -        map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_congL =>
    5.91 +        map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
    5.92            Goal.prove_sorry lthy [] [] goal
    5.93 -            (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtor_thms)
    5.94 +            (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtor_thms)
    5.95            |> Thm.close_derivation)
    5.96 -          goals ctor_defs dtor_unfold_thms map_comp_id_thms map_congL_thms
    5.97 +          goals ctor_defs dtor_unfold_thms map_comp_id_thms map_cong0L_thms
    5.98        end;
    5.99  
   5.100      val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
   5.101 @@ -2175,11 +2175,11 @@
   5.102            end;
   5.103          val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs;
   5.104        in
   5.105 -        map3 (fn goal => fn unfold => fn map_cong =>
   5.106 +        map3 (fn goal => fn unfold => fn map_cong0 =>
   5.107            Goal.prove_sorry lthy [] [] goal
   5.108 -            (mk_corec_tac m corec_defs unfold map_cong corec_Inl_sum_thms)
   5.109 +            (mk_corec_tac m corec_defs unfold map_cong0 corec_Inl_sum_thms)
   5.110            |> Thm.close_derivation)
   5.111 -        goals dtor_unfold_thms map_congs
   5.112 +        goals dtor_unfold_thms map_cong0s
   5.113        end;
   5.114  
   5.115      val corec_unique_mor_thm =
   5.116 @@ -2409,11 +2409,11 @@
   5.117              val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's;
   5.118              val cTs = map (SOME o certifyT lthy) FTs';
   5.119              val maps =
   5.120 -              map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong =>
   5.121 +              map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong0 =>
   5.122                  Goal.prove_sorry lthy [] [] goal
   5.123 -                  (K (mk_map_tac m n cT unfold map_comp' map_cong))
   5.124 +                  (K (mk_map_tac m n cT unfold map_comp' map_cong0))
   5.125                  |> Thm.close_derivation)
   5.126 -              goals cTs dtor_unfold_thms map_comp's map_congs;
   5.127 +              goals cTs dtor_unfold_thms map_comp's map_cong0s;
   5.128            in
   5.129              map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
   5.130            end;
   5.131 @@ -2427,7 +2427,7 @@
   5.132                  fs_maps gs_maps fgs_maps)))
   5.133            in
   5.134              split_conj_thm (Goal.prove_sorry lthy [] [] goal
   5.135 -              (K (mk_map_comp_tac m n map_thms map_comps map_congs dtor_unfold_unique_thm))
   5.136 +              (K (mk_map_comp_tac m n map_thms map_comps map_cong0s dtor_unfold_unique_thm))
   5.137                |> Thm.close_derivation)
   5.138            end;
   5.139  
   5.140 @@ -2548,7 +2548,7 @@
   5.141              map (split_conj_thm o mk_specN n) thms
   5.142            end;
   5.143  
   5.144 -        val map_cong_thms =
   5.145 +        val map_cong0_thms =
   5.146            let
   5.147              val cTs = map (SOME o certifyT lthy o
   5.148                Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params;
   5.149 @@ -2559,7 +2559,7 @@
   5.150              fun mk_prems sets z =
   5.151                Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys')
   5.152  
   5.153 -            fun mk_map_cong sets z fmap gmap =
   5.154 +            fun mk_map_cong0 sets z fmap gmap =
   5.155                HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z));
   5.156  
   5.157              fun mk_coind_body sets (x, T) z fmap gmap y y_copy =
   5.158 @@ -2581,11 +2581,11 @@
   5.159  
   5.160              val goal =
   5.161                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   5.162 -                (map4 mk_map_cong setss_by_bnf Jzs fs_maps fs_copy_maps));
   5.163 +                (map4 mk_map_cong0 setss_by_bnf Jzs fs_maps fs_copy_maps));
   5.164  
   5.165              val thm = singleton (Proof_Context.export names_lthy lthy)
   5.166                (Goal.prove_sorry lthy [] [] goal
   5.167 -              (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_congs set_natural'ss
   5.168 +              (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_natural'ss
   5.169                set_hset_thmss set_hset_hset_thmsss)))
   5.170                |> Thm.close_derivation
   5.171            in
   5.172 @@ -2685,7 +2685,7 @@
   5.173          val map_id_tacs =
   5.174            map2 (K oo mk_map_id_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms;
   5.175          val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms;
   5.176 -        val map_cong_tacs = map (mk_map_cong_tac m) map_cong_thms;
   5.177 +        val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
   5.178          val set_nat_tacss =
   5.179            map2 (map2 (K oo mk_set_natural_tac)) hset_defss (transpose col_natural_thmss);
   5.180  
   5.181 @@ -2709,7 +2709,7 @@
   5.182  
   5.183          val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
   5.184  
   5.185 -        val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
   5.186 +        val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
   5.187            bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
   5.188  
   5.189          val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
   5.190 @@ -2941,14 +2941,14 @@
   5.191                    HOLogic.mk_mem (HOLogic.mk_prod (dtor $ Jz, dtor' $ Jz'), srelR)));
   5.192              val goals = map6 mk_goal Jzs Jz's dtors dtor's JsrelRs srelRs;
   5.193            in
   5.194 -            map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
   5.195 +            map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
   5.196                fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
   5.197                fn set_naturals => fn dtor_set_incls => fn dtor_set_set_inclss =>
   5.198                Goal.prove_sorry lthy [] [] goal
   5.199 -                (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets
   5.200 +                (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets
   5.201                    dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss))
   5.202                |> Thm.close_derivation)
   5.203 -            ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_dtor_set_thmss'
   5.204 +            ks goals in_srels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
   5.205                dtor_inject_thms dtor_ctor_thms set_natural'ss dtor_set_incl_thmss
   5.206                dtor_set_set_incl_thmsss
   5.207            end;
     6.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Apr 24 14:14:36 2013 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Apr 24 14:15:01 2013 +0200
     6.3 @@ -256,12 +256,12 @@
     6.4    EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
     6.5      atac, atac, rtac (hset_def RS sym)] 1
     6.6  
     6.7 -fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_congs set_naturalss =
     6.8 +fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_naturalss =
     6.9    let
    6.10      val n = length srel_O_Grs;
    6.11 -    val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ srel_O_Grs);
    6.12 +    val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_naturalss ~~ srel_O_Grs);
    6.13  
    6.14 -    fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =
    6.15 +    fun mk_if_tac ((((i, map_comp), map_cong0), set_naturals), srel_O_Gr) =
    6.16        EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
    6.17          etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
    6.18          rtac (srel_O_Gr RS equalityD2 RS set_mp),
    6.19 @@ -276,11 +276,11 @@
    6.20                else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
    6.21                  rtac trans_fun_cong_image_id_id_apply, atac])
    6.22              (1 upto (m + n) ~~ set_naturals),
    6.23 -            rtac trans, rtac trans, rtac map_comp, rtac map_cong, REPEAT_DETERM_N m o rtac thm,
    6.24 +            rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
    6.25              REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
    6.26            @{thms fst_diag_id snd_diag_id})];
    6.27  
    6.28 -    fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =
    6.29 +    fun mk_only_if_tac ((((i, map_comp), map_cong0), set_naturals), srel_O_Gr) =
    6.30        EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
    6.31          etac allE, etac allE, etac impE, atac,
    6.32          dtac (srel_O_Gr RS equalityD1 RS set_mp),
    6.33 @@ -290,13 +290,13 @@
    6.34          REPEAT_DETERM o etac conjE,
    6.35          hyp_subst_tac,
    6.36          REPEAT_DETERM o eresolve_tac [CollectE, conjE],
    6.37 -        rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong,
    6.38 +        rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
    6.39          REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
    6.40          REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
    6.41 -        etac sym, rtac trans, rtac map_comp, rtac trans, rtac map_cong,
    6.42 +        etac sym, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
    6.43          REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
    6.44          REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
    6.45 -        rtac trans, rtac map_cong,
    6.46 +        rtac trans, rtac map_cong0,
    6.47          REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
    6.48          REPEAT_DETERM_N n o rtac refl,
    6.49          etac sym, rtac CollectI,
    6.50 @@ -841,7 +841,7 @@
    6.51  fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
    6.52    to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
    6.53    prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_naturalss coalg_setss
    6.54 -  map_comp_ids map_congs map_arg_congs {context = ctxt, prems = _} =
    6.55 +  map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} =
    6.56    let
    6.57      val n = length beh_defs;
    6.58      val ks = 1 upto n;
    6.59 @@ -939,7 +939,7 @@
    6.60            (drop m set_naturals ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
    6.61  
    6.62      fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),
    6.63 -      ((map_comp_id, (map_cong, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
    6.64 +      ((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
    6.65        EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
    6.66          rtac (@{thm if_P} RS
    6.67            (if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans),
    6.68 @@ -950,7 +950,7 @@
    6.69          if n = 1 then K all_tac
    6.70          else (rtac (sum_case_weak_cong RS trans) THEN'
    6.71            rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
    6.72 -        rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl),
    6.73 +        rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
    6.74          EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
    6.75            DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
    6.76              rtac trans, rtac @{thm Shift_def},
    6.77 @@ -1001,15 +1001,15 @@
    6.78              (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
    6.79      CONJ_WRAP' mor_tac
    6.80        (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
    6.81 -        ((map_comp_ids ~~ (map_congs ~~ map_arg_congs)) ~~
    6.82 +        ((map_comp_ids ~~ (map_cong0s ~~ map_arg_congs)) ~~
    6.83            (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1
    6.84    end;
    6.85  
    6.86 -fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBISs =
    6.87 +fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBISs =
    6.88    EVERY' [rtac @{thm congruentI}, dtac lsbisE,
    6.89      REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], rtac (o_apply RS trans),
    6.90      etac (sym RS arg_cong RS trans), rtac (map_comp_id RS trans),
    6.91 -    rtac (map_cong RS trans), REPEAT_DETERM_N m o rtac refl,
    6.92 +    rtac (map_cong0 RS trans), REPEAT_DETERM_N m o rtac refl,
    6.93      EVERY' (map (fn equiv_LSBIS =>
    6.94        EVERY' [rtac @{thm equiv_proj}, rtac equiv_LSBIS, etac set_mp, atac])
    6.95      equiv_LSBISs), rtac sym, rtac (o_apply RS trans),
    6.96 @@ -1042,18 +1042,18 @@
    6.97          rtac congruent_str_final, atac, rtac o_apply])
    6.98      (equiv_LSBISs ~~ congruent_str_finals)] 1;
    6.99  
   6.100 -fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_congLs
   6.101 +fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls
   6.102    {context = ctxt, prems = _} =
   6.103    unfold_thms_tac ctxt defs THEN
   6.104    EVERY' [rtac conjI,
   6.105      CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
   6.106 -    CONJ_WRAP' (fn (Rep, ((map_comp_id, map_congL), coalg_final_sets)) =>
   6.107 -      EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_congL,
   6.108 +    CONJ_WRAP' (fn (Rep, ((map_comp_id, map_cong0L), coalg_final_sets)) =>
   6.109 +      EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_cong0L,
   6.110          EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
   6.111            EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse,
   6.112              etac set_rev_mp, rtac coalg_final_set, rtac Rep])
   6.113          Abs_inverses (drop m coalg_final_sets))])
   6.114 -    (Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1;
   6.115 +    (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
   6.116  
   6.117  fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
   6.118    unfold_thms_tac ctxt defs THEN
   6.119 @@ -1061,16 +1061,16 @@
   6.120      CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
   6.121      CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
   6.122  
   6.123 -fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_congs =
   6.124 +fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
   6.125    EVERY' [rtac iffD2, rtac mor_UNIV,
   6.126 -    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong))) =>
   6.127 +    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) =>
   6.128        EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
   6.129          rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
   6.130          rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
   6.131 -        rtac (o_apply RS trans RS sym), rtac map_cong,
   6.132 +        rtac (o_apply RS trans RS sym), rtac map_cong0,
   6.133          REPEAT_DETERM_N m o rtac refl,
   6.134          EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) unfold_defs)])
   6.135 -    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
   6.136 +    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_cong0s)))] 1;
   6.137  
   6.138  fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
   6.139    sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
   6.140 @@ -1109,17 +1109,17 @@
   6.141        rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
   6.142        rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
   6.143  
   6.144 -fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtors
   6.145 +fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtors
   6.146    {context = ctxt, prems = _} =
   6.147    unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
   6.148 -    rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
   6.149 +    rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
   6.150      EVERY' (map (fn thm =>
   6.151        rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
   6.152      rtac sym, rtac id_apply] 1;
   6.153  
   6.154 -fun mk_corec_tac m corec_defs unfold map_cong corec_Inls {context = ctxt, prems = _} =
   6.155 +fun mk_corec_tac m corec_defs unfold map_cong0 corec_Inls {context = ctxt, prems = _} =
   6.156    unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
   6.157 -    rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
   6.158 +    rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
   6.159      REPEAT_DETERM_N m o rtac refl,
   6.160      EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
   6.161  
   6.162 @@ -1184,9 +1184,9 @@
   6.163      rtac impI, REPEAT_DETERM o etac conjE,
   6.164      CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
   6.165  
   6.166 -fun mk_map_tac m n cT unfold map_comp' map_cong =
   6.167 +fun mk_map_tac m n cT unfold map_comp' map_cong0 =
   6.168    EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
   6.169 -    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
   6.170 +    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong0,
   6.171      REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
   6.172      REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
   6.173      rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
   6.174 @@ -1210,9 +1210,9 @@
   6.175    EVERY' [rtac (unfold_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
   6.176      rtac unfold_dtor] 1;
   6.177  
   6.178 -fun mk_map_comp_tac m n maps map_comps map_congs unfold_unique =
   6.179 +fun mk_map_comp_tac m n maps map_comps map_cong0s unfold_unique =
   6.180    EVERY' [rtac unfold_unique,
   6.181 -    EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong =>
   6.182 +    EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong0 =>
   6.183        EVERY' (map rtac
   6.184          ([@{thm o_assoc} RS trans,
   6.185          @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
   6.186 @@ -1220,12 +1220,12 @@
   6.187          @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans,
   6.188          @{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans,
   6.189          @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
   6.190 -        ext, o_apply RS trans,  o_apply RS trans RS sym, map_cong] @
   6.191 +        ext, o_apply RS trans,  o_apply RS trans RS sym, map_cong0] @
   6.192          replicate m (@{thm id_o} RS fun_cong) @
   6.193          replicate n (@{thm o_id} RS fun_cong))))
   6.194 -    maps map_comps map_congs)] 1;
   6.195 +    maps map_comps map_cong0s)] 1;
   6.196  
   6.197 -fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_congs set_naturalss set_hsetss
   6.198 +fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_naturalss set_hsetss
   6.199    set_hset_hsetsss =
   6.200    let
   6.201      val n = length map_comp's;
   6.202 @@ -1233,13 +1233,13 @@
   6.203    in
   6.204      EVERY' ([rtac rev_mp,
   6.205        coinduct_tac] @
   6.206 -      maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong), set_naturals), set_hsets),
   6.207 +      maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_naturals), set_hsets),
   6.208          set_hset_hsetss) =>
   6.209          [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
   6.210 -         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
   6.211 +         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
   6.212           REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply),
   6.213           REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
   6.214 -         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
   6.215 +         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
   6.216           EVERY' (maps (fn set_hset =>
   6.217             [rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE,
   6.218             REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
   6.219 @@ -1253,7 +1253,7 @@
   6.220                 EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
   6.221             (drop m set_naturals ~~ set_hset_hsetss)])
   6.222          (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~
   6.223 -          map_congs ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @
   6.224 +          map_cong0s ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @
   6.225        [rtac impI,
   6.226         CONJ_WRAP' (fn k =>
   6.227           EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,
   6.228 @@ -1499,7 +1499,7 @@
   6.229    ALLGOALS (TRY o
   6.230      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
   6.231  
   6.232 -fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets dtor_inject dtor_ctor
   6.233 +fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor
   6.234    set_naturals dtor_set_incls dtor_set_set_inclss =
   6.235    let
   6.236      val m = length dtor_set_incls;
   6.237 @@ -1521,7 +1521,7 @@
   6.238              rtac conjI, rtac refl, rtac refl])
   6.239          (in_Jsrels ~~ (active_set_naturals ~~ dtor_set_set_inclss)),
   6.240          CONJ_WRAP' (fn conv =>
   6.241 -          EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
   6.242 +          EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
   6.243            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   6.244            REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
   6.245            rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
   6.246 @@ -1547,7 +1547,7 @@
   6.247          rtac conjI,
   6.248          REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
   6.249            rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
   6.250 -          rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   6.251 +          rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   6.252            EVERY' (map (fn in_Jsrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
   6.253              dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
   6.254              dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jsrels),
     7.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 14:14:36 2013 +0200
     7.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 14:15:01 2013 +0200
     7.3 @@ -144,7 +144,7 @@
     7.4      val in_bds = map in_bd_of_bnf bnfs;
     7.5      val sym_map_comps = map (fn bnf => map_comp_of_bnf bnf RS sym) bnfs;
     7.6      val map_comp's = map map_comp'_of_bnf bnfs;
     7.7 -    val map_congs = map map_cong_of_bnf bnfs;
     7.8 +    val map_cong0s = map map_cong0_of_bnf bnfs;
     7.9      val map_ids = map map_id_of_bnf bnfs;
    7.10      val map_id's = map map_id'_of_bnf bnfs;
    7.11      val map_wpulls = map map_wpull_of_bnf bnfs;
    7.12 @@ -195,7 +195,7 @@
    7.13  
    7.14      (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
    7.15        map id ... id f(m+1) ... f(m+n) x = x*)
    7.16 -    fun mk_map_congL x mapAsAs sets map_cong map_id' =
    7.17 +    fun mk_map_cong0L x mapAsAs sets map_cong0 map_id' =
    7.18        let
    7.19          fun mk_prem set f z z' = HOLogic.mk_Trueprop
    7.20            (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
    7.21 @@ -204,11 +204,11 @@
    7.22        in
    7.23          Goal.prove_sorry lthy [] []
    7.24            (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
    7.25 -          (K (mk_map_congL_tac m map_cong map_id'))
    7.26 +          (K (mk_map_cong0L_tac m map_cong0 map_id'))
    7.27          |> Thm.close_derivation
    7.28        end;
    7.29  
    7.30 -    val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
    7.31 +    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_id's;
    7.32      val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs;
    7.33      val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;
    7.34  
    7.35 @@ -407,7 +407,7 @@
    7.36            (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ inv_fs)
    7.37              (Logic.list_implies (prems, concl)))
    7.38            (K (mk_mor_inv_tac alg_def mor_def
    7.39 -            set_natural'ss morE_thms map_comp_id_thms map_congL_thms))
    7.40 +            set_natural'ss morE_thms map_comp_id_thms map_cong0L_thms))
    7.41          |> Thm.close_derivation
    7.42        end;
    7.43  
    7.44 @@ -897,7 +897,7 @@
    7.45            (fold_rev Logic.all (init_xs @ Bs @ ss @ init_fs @ init_fs_copy)
    7.46              (Logic.list_implies (prems @ mor_prems, unique)))
    7.47            (K (mk_init_unique_mor_tac m alg_def alg_init_thm least_min_alg_thms
    7.48 -            in_mono'_thms alg_set_thms morE_thms map_congs))
    7.49 +            in_mono'_thms alg_set_thms morE_thms map_cong0s))
    7.50            |> Thm.close_derivation;
    7.51        in
    7.52          (ex_mor, split_conj_thm unique_mor)
    7.53 @@ -1180,11 +1180,11 @@
    7.54            mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
    7.55          val goals = map3 mk_goal dtors ctors FTs;
    7.56        in
    7.57 -        map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_congL =>
    7.58 +        map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L =>
    7.59            Goal.prove_sorry lthy [] [] goal
    7.60 -            (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_fold_thms))
    7.61 +            (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_fold_thms))
    7.62            |> Thm.close_derivation)
    7.63 -        goals dtor_defs ctor_fold_thms map_comp_id_thms map_congL_thms
    7.64 +        goals dtor_defs ctor_fold_thms map_comp_id_thms map_cong0L_thms
    7.65        end;
    7.66  
    7.67      val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
    7.68 @@ -1431,10 +1431,10 @@
    7.69                  HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_maps))));
    7.70              val goals = map4 mk_goal fs_maps map_FTFT's ctors ctor's;
    7.71              val maps =
    7.72 -              map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong =>
    7.73 -                Goal.prove_sorry lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong))
    7.74 +              map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
    7.75 +                Goal.prove_sorry lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong0))
    7.76                  |> Thm.close_derivation)
    7.77 -              goals ctor_fold_thms map_comp_id_thms map_congs;
    7.78 +              goals ctor_fold_thms map_comp_id_thms map_cong0s;
    7.79            in
    7.80              map (fn thm => thm RS @{thm pointfreeE}) maps
    7.81            end;
    7.82 @@ -1450,7 +1450,7 @@
    7.83                  (map2 (curry HOLogic.mk_eq) us fs_maps));
    7.84              val unique = Goal.prove_sorry lthy [] []
    7.85                (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
    7.86 -              (K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_congs))
    7.87 +              (K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_cong0s))
    7.88                |> Thm.close_derivation;
    7.89            in
    7.90              `split_conj_thm unique
    7.91 @@ -1588,18 +1588,18 @@
    7.92              map split_conj_thm thms
    7.93            end;
    7.94  
    7.95 -        val map_cong_thms =
    7.96 +        val map_cong0_thms =
    7.97            let
    7.98              fun mk_prem z set f g y y' =
    7.99                mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y)));
   7.100  
   7.101 -            fun mk_map_cong sets z fmap gmap =
   7.102 +            fun mk_map_cong0 sets z fmap gmap =
   7.103                HOLogic.mk_imp
   7.104                  (Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys'),
   7.105                  HOLogic.mk_eq (fmap $ z, gmap $ z));
   7.106  
   7.107              fun mk_cphi sets z fmap gmap =
   7.108 -              certify lthy (Term.absfree (dest_Free z) (mk_map_cong sets z fmap gmap));
   7.109 +              certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
   7.110  
   7.111              val cphis = map4 mk_cphi setss_by_bnf Izs fs_maps fs_copy_maps;
   7.112  
   7.113 @@ -1607,11 +1607,11 @@
   7.114  
   7.115              val goal =
   7.116                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   7.117 -                (map4 mk_map_cong setss_by_bnf Izs fs_maps fs_copy_maps));
   7.118 +                (map4 mk_map_cong0 setss_by_bnf Izs fs_maps fs_copy_maps));
   7.119  
   7.120              val thm = singleton (Proof_Context.export names_lthy lthy)
   7.121                (Goal.prove_sorry lthy [] [] goal
   7.122 -              (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs ctor_map_thms))
   7.123 +              (mk_mcong_tac (rtac induct) Fset_set_thmsss map_cong0s ctor_map_thms))
   7.124                |> Thm.close_derivation;
   7.125            in
   7.126              split_conj_thm thm
   7.127 @@ -1692,7 +1692,7 @@
   7.128          val map_id_tacs = map (K o mk_map_id_tac map_ids) ctor_map_unique_thms;
   7.129          val map_comp_tacs =
   7.130            map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks;
   7.131 -        val map_cong_tacs = map (mk_map_cong_tac m) map_cong_thms;
   7.132 +        val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
   7.133          val set_nat_tacss = map (map (K o mk_set_natural_tac)) (transpose set_natural_thmss);
   7.134          val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
   7.135          val bd_cinf_tacs = replicate n (K (rtac (bd_Cinfinite RS conjunct1) 1));
   7.136 @@ -1703,7 +1703,7 @@
   7.137  
   7.138          val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
   7.139  
   7.140 -        val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
   7.141 +        val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
   7.142            bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
   7.143  
   7.144          val ctor_witss =
   7.145 @@ -1778,14 +1778,14 @@
   7.146                    HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), srelR)));
   7.147              val goals = map6 mk_goal xFs yFs ctors ctor's IsrelRs srelRs;
   7.148            in
   7.149 -            map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
   7.150 +            map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
   7.151                fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
   7.152                fn set_naturals => fn ctor_set_incls => fn ctor_set_set_inclss =>
   7.153                Goal.prove_sorry lthy [] [] goal
   7.154 -               (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets
   7.155 +               (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
   7.156                   ctor_inject ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss))
   7.157                |> Thm.close_derivation)
   7.158 -            ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_ctor_set_thmss'
   7.159 +            ks goals in_srels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
   7.160                ctor_inject_thms ctor_dtor_thms set_natural'ss ctor_set_incl_thmss
   7.161                ctor_set_set_incl_thmsss
   7.162            end;
     8.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Wed Apr 24 14:14:36 2013 +0200
     8.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Wed Apr 24 14:15:01 2013 +0200
     8.3 @@ -139,7 +139,7 @@
     8.4      CONJ_WRAP' mor_tac (set_natural's ~~ map_comp_ids)) 1
     8.5    end;
     8.6  
     8.7 -fun mk_mor_inv_tac alg_def mor_def set_natural's morEs map_comp_ids map_congLs =
     8.8 +fun mk_mor_inv_tac alg_def mor_def set_natural's morEs map_comp_ids map_cong0Ls =
     8.9    let
    8.10      val fbetw_tac = EVERY' [rtac ballI, etac set_mp, etac imageI];
    8.11      fun Collect_tac set_natural' =
    8.12 @@ -147,12 +147,12 @@
    8.13          FIRST' [rtac subset_UNIV,
    8.14            (EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
    8.15              etac @{thm image_mono}, atac])]) set_natural';
    8.16 -    fun mor_tac (set_natural', ((morE, map_comp_id), map_congL)) =
    8.17 +    fun mor_tac (set_natural', ((morE, map_comp_id), map_cong0L)) =
    8.18        EVERY' [rtac ballI, ftac @{thm rev_bspec}, atac,
    8.19           REPEAT o eresolve_tac [CollectE, conjE], rtac sym, rtac trans, rtac sym,
    8.20           etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_natural',
    8.21           rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_natural',
    8.22 -         rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_congL RS arg_cong),
    8.23 +         rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_cong0L RS arg_cong),
    8.24           REPEAT_DETERM_N (length morEs) o
    8.25             (EVERY' [rtac subst, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])];
    8.26    in
    8.27 @@ -162,7 +162,7 @@
    8.28      REPEAT o etac conjE THEN'
    8.29      rtac conjI THEN'
    8.30      CONJ_WRAP' (K fbetw_tac) set_natural's THEN'
    8.31 -    CONJ_WRAP' mor_tac (set_natural's ~~ (morEs ~~ map_comp_ids ~~ map_congLs))) 1
    8.32 +    CONJ_WRAP' mor_tac (set_natural's ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1
    8.33    end;
    8.34  
    8.35  fun mk_mor_str_tac ks mor_def =
    8.36 @@ -436,7 +436,7 @@
    8.37    end;
    8.38  
    8.39  fun mk_init_unique_mor_tac m
    8.40 -    alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_congs =
    8.41 +    alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_cong0s =
    8.42    let
    8.43      val n = length least_min_algs;
    8.44      val ks = (1 upto n);
    8.45 @@ -444,22 +444,22 @@
    8.46      fun mor_tac morE in_mono = EVERY' [etac morE, rtac set_mp, rtac in_mono,
    8.47        REPEAT_DETERM_N n o rtac @{thm Collect_restrict}, rtac CollectI,
    8.48        REPEAT_DETERM_N (m + n) o (TRY o rtac conjI THEN' atac)];
    8.49 -    fun cong_tac map_cong = EVERY' [rtac (map_cong RS arg_cong),
    8.50 +    fun cong_tac map_cong0 = EVERY' [rtac (map_cong0 RS arg_cong),
    8.51        REPEAT_DETERM_N m o rtac refl,
    8.52        REPEAT_DETERM_N n o (etac @{thm prop_restrict} THEN' atac)];
    8.53  
    8.54 -    fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong))) = EVERY' [rtac ballI, rtac CollectI,
    8.55 +    fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong0))) = EVERY' [rtac ballI, rtac CollectI,
    8.56        REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
    8.57        REPEAT_DETERM_N m o rtac subset_UNIV,
    8.58        REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
    8.59        rtac trans, mor_tac morE in_mono,
    8.60 -      rtac trans, cong_tac map_cong,
    8.61 +      rtac trans, cong_tac map_cong0,
    8.62        rtac sym, mor_tac morE in_mono];
    8.63  
    8.64      fun mk_unique_tac (k, least_min_alg) =
    8.65        select_prem_tac n (etac @{thm prop_restrict}) k THEN' rtac least_min_alg THEN'
    8.66        stac alg_def THEN'
    8.67 -      CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_congs)));
    8.68 +      CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s)));
    8.69    in
    8.70      CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1
    8.71    end;
    8.72 @@ -514,9 +514,9 @@
    8.73      CONJ_WRAP' mk_unique type_defs 1
    8.74    end;
    8.75  
    8.76 -fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_folds =
    8.77 +fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_folds =
    8.78    EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx,
    8.79 -    rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
    8.80 +    rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
    8.81      EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
    8.82        ctor_o_folds),
    8.83      rtac sym, rtac id_apply] 1;
    8.84 @@ -575,16 +575,16 @@
    8.85        CONJ_WRAP' (K atac) ks] 1
    8.86    end;
    8.87  
    8.88 -fun mk_map_tac m n foldx map_comp_id map_cong =
    8.89 +fun mk_map_tac m n foldx map_comp_id map_cong0 =
    8.90    EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans, rtac o_apply,
    8.91 -    rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong RS arg_cong),
    8.92 +    rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong0 RS arg_cong),
    8.93      REPEAT_DETERM_N m o rtac refl,
    8.94      REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
    8.95      rtac sym, rtac o_apply] 1;
    8.96  
    8.97 -fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_congs =
    8.98 +fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_cong0s =
    8.99    let
   8.100 -    val n = length map_congs;
   8.101 +    val n = length map_cong0s;
   8.102      fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm pointfreeE},
   8.103        rtac sym, rtac trans, rtac o_apply, rtac trans, rtac (comp_id RS arg_cong),
   8.104        rtac (cong RS arg_cong),
   8.105 @@ -592,8 +592,8 @@
   8.106        REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply]))];
   8.107    in
   8.108      EVERY' [rtac fold_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
   8.109 -      CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_congs,
   8.110 -      CONJ_WRAP' mk_mor (map_comp_ids ~~ map_congs)] 1
   8.111 +      CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_cong0s,
   8.112 +      CONJ_WRAP' mk_mor (map_comp_ids ~~ map_cong0s)] 1
   8.113    end;
   8.114  
   8.115  fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
   8.116 @@ -647,7 +647,7 @@
   8.117      (induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1
   8.118    end;
   8.119  
   8.120 -fun mk_mcong_tac induct_tac set_setsss map_congs ctor_maps {context = ctxt, prems = _} =
   8.121 +fun mk_mcong_tac induct_tac set_setsss map_cong0s ctor_maps {context = ctxt, prems = _} =
   8.122    let
   8.123      fun use_asm thm = EVERY' [etac bspec, etac set_rev_mp, rtac thm];
   8.124  
   8.125 @@ -655,14 +655,14 @@
   8.126        CONJ_WRAP' (fn thm =>
   8.127          EVERY' [rtac ballI, etac bspec, etac set_rev_mp, etac thm]) set_sets];
   8.128  
   8.129 -    fun mk_map_cong ctor_map map_cong set_setss =
   8.130 +    fun mk_map_cong0 ctor_map map_cong0 set_setss =
   8.131        EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
   8.132 -        rtac trans, rtac ctor_map, rtac trans, rtac (map_cong RS arg_cong),
   8.133 +        rtac trans, rtac ctor_map, rtac trans, rtac (map_cong0 RS arg_cong),
   8.134          EVERY' (map use_asm (map hd set_setss)),
   8.135          EVERY' (map useIH (transpose (map tl set_setss))),
   8.136          rtac sym, rtac ctor_map];
   8.137    in
   8.138 -    (induct_tac THEN' EVERY' (map3 mk_map_cong ctor_maps map_congs set_setsss)) 1
   8.139 +    (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
   8.140    end;
   8.141  
   8.142  fun mk_incl_min_alg_tac induct_tac set_setsss alg_sets alg_min_alg {context = ctxt, prems = _} =
   8.143 @@ -775,7 +775,7 @@
   8.144            EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
   8.145              REPEAT_DETERM_N n o etac UnE]))))] 1);
   8.146  
   8.147 -fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets ctor_inject
   8.148 +fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject
   8.149    ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss =
   8.150    let
   8.151      val m = length ctor_set_incls;
   8.152 @@ -802,7 +802,7 @@
   8.153              rtac conjI, rtac refl, rtac refl])
   8.154          (in_Isrels ~~ (active_set_naturals ~~ ctor_set_set_inclss)),
   8.155          CONJ_WRAP' (fn conv =>
   8.156 -          EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
   8.157 +          EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
   8.158            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   8.159            REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
   8.160            rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map,
   8.161 @@ -827,7 +827,7 @@
   8.162          (ctor_sets ~~ passive_set_naturals),
   8.163          rtac conjI,
   8.164          REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
   8.165 -          rtac trans, rtac map_comp, rtac trans, rtac map_cong,
   8.166 +          rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
   8.167            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   8.168            EVERY' (map (fn in_Isrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
   8.169              dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
     9.1 --- a/src/HOL/BNF/Tools/bnf_tactics.ML	Wed Apr 24 14:14:36 2013 +0200
     9.2 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Wed Apr 24 14:15:01 2013 +0200
     9.3 @@ -27,8 +27,8 @@
     9.4      thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
     9.5  
     9.6    val mk_map_comp_id_tac: thm -> tactic
     9.7 -  val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
     9.8 -  val mk_map_congL_tac: int -> thm -> thm -> tactic
     9.9 +  val mk_map_cong0_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
    9.10 +  val mk_map_cong0L_tac: int -> thm -> thm -> tactic
    9.11  end;
    9.12  
    9.13  structure BNF_Tactics : BNF_TACTICS =
    9.14 @@ -101,12 +101,12 @@
    9.15  fun mk_map_comp_id_tac map_comp =
    9.16    (rtac trans THEN' rtac map_comp THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
    9.17  
    9.18 -fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} =
    9.19 -  EVERY' [rtac mp, rtac map_cong,
    9.20 +fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
    9.21 +  EVERY' [rtac mp, rtac map_cong0,
    9.22      CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
    9.23  
    9.24 -fun mk_map_congL_tac passive map_cong map_id' =
    9.25 -  (rtac trans THEN' rtac map_cong THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
    9.26 +fun mk_map_cong0L_tac passive map_cong0 map_id' =
    9.27 +  (rtac trans THEN' rtac map_cong0 THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
    9.28    REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN
    9.29    rtac map_id' 1;
    9.30