--- a/src/HOL/BNF/Tools/bnf_comp.ML Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Apr 24 14:15:01 2013 +0200
@@ -150,15 +150,15 @@
val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
fun map_id_tac _ =
- mk_comp_map_id_tac (map_id_of_bnf outer) (map_cong_of_bnf outer)
+ mk_comp_map_id_tac (map_id_of_bnf outer) (map_cong0_of_bnf outer)
(map map_id_of_bnf inners);
fun map_comp_tac _ =
- mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
+ mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
(map map_comp_of_bnf inners);
fun mk_single_set_natural_tac i _ =
- mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
+ mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
(collect_set_natural_of_bnf outer)
(map ((fn thms => nth thms i) o set_natural_of_bnf) inners);
@@ -181,8 +181,8 @@
|> Thm.close_derivation)
(map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
- fun map_cong_tac _ =
- mk_comp_map_cong_tac set_alt_thms (map_cong_of_bnf outer) (map map_cong_of_bnf inners);
+ fun map_cong0_tac _ =
+ mk_comp_map_cong0_tac set_alt_thms (map_cong0_of_bnf outer) (map map_cong0_of_bnf inners);
val set_bd_tacs =
if ! quick_and_dirty then
@@ -238,7 +238,7 @@
unfold_thms_tac lthy basic_thms THEN rtac thm 1
end;
- val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -309,8 +309,8 @@
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
rtac refl 1;
- fun map_cong_tac {context = ctxt, prems = _} =
- mk_kill_map_cong_tac ctxt n (live - n) (map_cong_of_bnf bnf);
+ fun map_cong0_tac {context = ctxt, prems = _} =
+ mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
@@ -348,7 +348,7 @@
rtac thm 1
end;
- val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -403,8 +403,8 @@
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
rtac refl 1;
- fun map_cong_tac {context = ctxt, prems = _} =
- rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 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_natural_tacs =
if ! quick_and_dirty then
replicate (n + live) (K all_tac)
@@ -435,7 +435,7 @@
fun srel_O_Gr_tac _ =
mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
- val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -488,8 +488,8 @@
fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
- fun map_cong_tac {context = ctxt, prems = _} =
- rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 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_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf));
fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
@@ -512,7 +512,7 @@
fun srel_O_Gr_tac _ =
mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
- val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -653,7 +653,7 @@
SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
- (mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
+ (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
(K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
(mk_tac (map_wpull_of_bnf bnf))
(mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf)));
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Wed Apr 24 14:15:01 2013 +0200
@@ -13,7 +13,7 @@
val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
val mk_comp_in_bd_tac: thm -> thm list -> thm -> thm list -> thm -> tactic
val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic
- val mk_comp_map_cong_tac: thm list -> thm -> thm list -> tactic
+ val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic
val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
@@ -24,7 +24,7 @@
val mk_kill_bd_cinfinite_tac: thm -> tactic
val kill_in_alt_tac: tactic
val mk_kill_in_bd_tac: int -> bool -> thm -> thm -> thm -> thm -> thm -> tactic
- val mk_kill_map_cong_tac: Proof.context -> int -> int -> thm -> tactic
+ val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic
val mk_kill_set_bd_tac: thm -> thm -> tactic
val empty_natural_tac: tactic
@@ -69,22 +69,22 @@
unfold_thms_tac ctxt [collect_set_natural RS sym] THEN
rtac refl 1;
-fun mk_comp_map_id_tac Gmap_id Gmap_cong map_ids =
- EVERY' ([rtac ext, rtac (Gmap_cong RS trans)] @
+fun mk_comp_map_id_tac Gmap_id Gmap_cong0 map_ids =
+ EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
map (fn thm => rtac (thm RS fun_cong)) map_ids @ [rtac (Gmap_id RS fun_cong)]) 1;
-fun mk_comp_map_comp_tac Gmap_comp Gmap_cong map_comps =
+fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps =
EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
- rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong] @
+ 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;
-fun mk_comp_set_natural_tac Gmap_comp Gmap_cong Gset_natural set_naturals =
+fun mk_comp_set_natural_tac Gmap_comp Gmap_cong0 Gset_natural set_naturals =
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_cong] @
+ rtac Gmap_cong0] @
map (fn thm => rtac (thm RS fun_cong)) set_naturals @
[rtac (Gset_natural RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
@@ -98,14 +98,14 @@
rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],
rtac @{thm image_empty}]) 1;
-fun mk_comp_map_cong_tac comp_set_alts map_cong map_congs =
+fun mk_comp_map_cong0_tac comp_set_alts map_cong0 map_cong0s =
let
val n = length comp_set_alts;
in
(if n = 0 then rtac refl 1
- else rtac map_cong 1 THEN
- EVERY' (map_index (fn (i, map_cong) =>
- rtac map_cong THEN' EVERY' (map_index (fn (k, set_alt) =>
+ else rtac map_cong0 1 THEN
+ EVERY' (map_index (fn (i, map_cong0) =>
+ rtac map_cong0 THEN' EVERY' (map_index (fn (k, set_alt) =>
EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac meta_mp,
rtac (equalityD2 RS set_mp), rtac (set_alt RS fun_cong RS trans),
rtac trans_o_apply, rtac (@{thm collect_def} RS arg_cong_Union),
@@ -113,7 +113,7 @@
rtac @{thm insertI1}, rtac (o_apply RS equalityD2 RS set_mp),
etac @{thm imageI}, atac])
comp_set_alts))
- map_congs) 1)
+ map_cong0s) 1)
end;
fun mk_comp_bd_card_order_tac Fbd_card_orders Gbd_card_order =
@@ -233,8 +233,8 @@
(* Kill operation *)
-fun mk_kill_map_cong_tac ctxt n m map_cong =
- (rtac map_cong THEN' EVERY' (replicate n (rtac refl)) THEN'
+fun mk_kill_map_cong0_tac ctxt n m map_cong0 =
+ (rtac map_cong0 THEN' EVERY' (replicate n (rtac refl)) THEN'
EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1;
fun mk_kill_bd_card_order_tac n bd_card_order =
--- a/src/HOL/BNF/Tools/bnf_def.ML Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Apr 24 14:15:01 2013 +0200
@@ -52,7 +52,7 @@
val in_srel_of_bnf: BNF -> thm
val map_comp'_of_bnf: BNF -> thm
val map_comp_of_bnf: BNF -> thm
- val map_cong_of_bnf: BNF -> thm
+ val map_cong0_of_bnf: BNF -> thm
val map_def_of_bnf: BNF -> thm
val map_id'_of_bnf: BNF -> thm
val map_id_of_bnf: BNF -> thm
@@ -107,7 +107,7 @@
type axioms = {
map_id: thm,
map_comp: thm,
- map_cong: thm,
+ map_cong0: thm,
set_natural: thm list,
bd_card_order: thm,
bd_cinfinite: thm,
@@ -118,7 +118,7 @@
};
fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), srel) =
- {map_id = id, map_comp = comp, map_cong = cong, set_natural = nat, bd_card_order = c_o,
+ {map_id = id, map_comp = comp, map_cong0 = cong, set_natural = nat, bd_card_order = c_o,
bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, srel_O_Gr = srel};
fun dest_cons [] = raise Empty
@@ -141,16 +141,16 @@
fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull srel =
[mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, srel];
-fun dest_axioms {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
+fun dest_axioms {map_id, map_comp, map_cong0, set_natural, bd_card_order, bd_cinfinite, set_bd,
in_bd, map_wpull, srel_O_Gr} =
- zip_axioms map_id map_comp map_cong set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull
+ zip_axioms map_id map_comp map_cong0 set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull
srel_O_Gr;
-fun map_axioms f {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
+fun map_axioms f {map_id, map_comp, map_cong0, set_natural, bd_card_order, bd_cinfinite, set_bd,
in_bd, map_wpull, srel_O_Gr} =
{map_id = f map_id,
map_comp = f map_comp,
- map_cong = f map_cong,
+ map_cong0 = f map_cong0,
set_natural = map f set_natural,
bd_card_order = f bd_card_order,
bd_cinfinite = f bd_cinfinite,
@@ -371,7 +371,7 @@
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_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
-val map_cong_of_bnf = #map_cong o #axioms o rep_bnf;
+val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
@@ -507,7 +507,7 @@
val map_id'N = "map_id'";
val map_compN = "map_comp";
val map_comp'N = "map_comp'";
-val map_congN = "map_cong";
+val map_cong0N = "map_cong0";
val map_wpullN = "map_wpull";
val rel_eqN = "rel_eq";
val rel_flipN = "rel_flip";
@@ -814,7 +814,7 @@
fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
end;
- val map_cong_goal =
+ val map_cong0_goal =
let
fun mk_prem z set f f_copy =
Logic.all z (Logic.mk_implies
@@ -890,7 +890,7 @@
val srel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (srel, Rs), O_Gr));
- val goals = zip_axioms map_id_goal map_comp_goal map_cong_goal set_naturals_goal
+ val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_naturals_goal
card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal srel_O_Gr_goal;
fun mk_wit_goals (I, wit) =
@@ -1004,7 +1004,7 @@
(Logic.list_implies (prems, HOLogic.mk_Trueprop concl))
in
Goal.prove_sorry lthy [] [] goal
- (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong axioms)
+ (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong0 axioms)
(#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
end;
@@ -1020,7 +1020,7 @@
val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
in
Goal.prove_sorry lthy [] [] goal
- (mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong axioms) (Lazy.force map_id')
+ (mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id')
(Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
end;
@@ -1074,7 +1074,7 @@
val rhs = mk_converse (Term.list_comb (srel, Rs));
val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_subset lhs rhs));
val le_thm = Goal.prove_sorry lthy [] [] le_goal
- (mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong axioms)
+ (mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms)
(Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
@@ -1094,7 +1094,7 @@
val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
in
Goal.prove_sorry lthy [] [] goal
- (mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong axioms)
+ (mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms)
(Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
end;
@@ -1201,7 +1201,7 @@
let
val notes =
[(map_comp'N, [Lazy.force (#map_comp' facts)]),
- (map_congN, [#map_cong axioms]),
+ (map_cong0N, [#map_cong0 axioms]),
(map_id'N, [Lazy.force (#map_id' facts)]),
(rel_eqN, [Lazy.force (#rel_eq facts)]),
(rel_flipN, [Lazy.force (#rel_flip facts)]),
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Wed Apr 24 14:15:01 2013 +0200
@@ -51,7 +51,7 @@
rtac set_natural) set_naturals) THEN'
rtac @{thm image_empty}) 1;
-fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals =
+fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_naturals =
if null set_naturals then
EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1
else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
@@ -62,12 +62,12 @@
rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
set_naturals,
CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
- rtac (map_comp RS trans RS sym), rtac map_cong,
+ rtac (map_comp RS trans RS sym), rtac map_cong0,
REPEAT_DETERM_N (length set_naturals) 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_srel_Gr_tac srel_O_Grs map_id map_cong map_id' map_comp set_naturals
+fun mk_srel_Gr_tac srel_O_Grs map_id map_cong0 map_id' map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
@@ -80,7 +80,7 @@
REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE, hyp_subst_tac,
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac map_cong,
+ rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
@@ -97,7 +97,7 @@
EVERY' (map2 (fn convol => fn map_id =>
EVERY' [rtac CollectI, rtac exI, rtac conjI,
rtac Pair_eqI, rtac conjI, rtac refl, rtac sym,
- rtac (box_equals OF [map_cong, map_comp RS sym, map_id]),
+ rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]),
REPEAT_DETERM_N n o rtac (convol RS fun_cong),
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac CollectI,
@@ -121,7 +121,7 @@
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
-fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong map_comp set_naturals
+fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong0 map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
@@ -136,7 +136,7 @@
rtac @{thm relcompI}, rtac @{thm converseI},
EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans,
- rtac map_cong, REPEAT_DETERM_N n o rtac thm,
+ rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
rtac (map_comp RS sym), rtac CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
@@ -146,7 +146,7 @@
EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
-fun mk_srel_O_tac srel_O_Grs srel_Id map_cong map_wppull map_comp set_naturals
+fun mk_srel_O_tac srel_O_Grs srel_Id map_cong0 map_wppull map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
@@ -162,22 +162,22 @@
REPEAT_DETERM o etac conjE, hyp_subst_tac,
rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
+ rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
REPEAT_DETERM_N n o rtac @{thm fst_fstO},
in_tac @{thm fstO_in},
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac map_cong,
+ rtac sym, rtac trans, rtac map_comp, 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_fstO_sndO}, atac, etac notE,
etac set_mp, atac],
in_tac @{thm fstO_in},
rtac @{thm relcompI}, rtac @{thm converseI},
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac map_cong,
+ rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
REPEAT_DETERM_N n o rtac o_apply,
in_tac @{thm sndO_in},
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
+ rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
REPEAT_DETERM_N n o rtac @{thm snd_sndO},
in_tac @{thm sndO_in},
rtac @{thm subrelI},
@@ -192,7 +192,7 @@
rtac @{thm relcompI}, rtac @{thm converseI},
EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans,
- rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm,
+ rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
end;
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Apr 24 14:15:01 2013 +0200
@@ -222,7 +222,7 @@
val map_comps = map map_comp_of_bnf bnfs;
val sym_map_comps = map (fn thm => thm RS sym) map_comps;
val map_comp's = map map_comp'_of_bnf bnfs;
- val map_congs = map map_cong_of_bnf bnfs;
+ val map_cong0s = map map_cong0_of_bnf bnfs;
val map_ids = map map_id_of_bnf bnfs;
val map_id's = map map_id'_of_bnf bnfs;
val map_wpulls = map map_wpull_of_bnf bnfs;
@@ -260,7 +260,7 @@
(*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
map id ... id f(m+1) ... f(m+n) x = x*)
- fun mk_map_congL x mapAsAs sets map_cong map_id' =
+ fun mk_map_cong0L x mapAsAs sets map_cong0 map_id' =
let
fun mk_prem set f z z' =
HOLogic.mk_Trueprop
@@ -270,11 +270,11 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
- (K (mk_map_congL_tac m map_cong map_id'))
+ (K (mk_map_cong0L_tac m map_cong0 map_id'))
|> Thm.close_derivation
end;
- val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
+ val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_id's;
val in_mono'_thms = map (fn thm =>
(thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos;
@@ -866,7 +866,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
(mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
- (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_congs set_natural'ss))
+ (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_cong0s set_natural'ss))
|> Thm.close_derivation
end;
@@ -1770,7 +1770,7 @@
to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
set_rv_Lev_thmsss set_Lev_thmsss set_image_Lev_thmsss
- set_natural'ss coalg_set_thmss map_comp_id_thms map_congs map_arg_cong_thms)
+ set_natural'ss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms)
|> Thm.close_derivation;
val timer = time (timer "Behavioral morphism");
@@ -1799,11 +1799,11 @@
val goals = map3 mk_goal (map (mk_LSBIS As) ks) final_maps strTAs;
in
- map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong =>
+ map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBIS_thms))
+ (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBIS_thms))
|> Thm.close_derivation)
- goals lsbisE_thms map_comp_id_thms map_congs
+ goals lsbisE_thms map_comp_id_thms map_cong0s
end;
val coalg_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
@@ -1919,7 +1919,7 @@
Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
(mk_mor_Rep_tac m (mor_def :: dtor_defs) Reps Abs_inverses coalg_final_set_thmss
- map_comp_id_thms map_congL_thms)
+ map_comp_id_thms map_cong0L_thms)
|> Thm.close_derivation;
val mor_Abs =
@@ -1974,7 +1974,7 @@
(fold_rev Logic.all ss
(HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks))))
(K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs'
- map_comp_id_thms map_congs))
+ map_comp_id_thms map_cong0s))
|> Thm.close_derivation
end;
val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
@@ -2084,11 +2084,11 @@
mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
val goals = map3 mk_goal dtors ctors FTs;
in
- map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_congL =>
+ map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
Goal.prove_sorry lthy [] [] goal
- (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtor_thms)
+ (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtor_thms)
|> Thm.close_derivation)
- goals ctor_defs dtor_unfold_thms map_comp_id_thms map_congL_thms
+ goals ctor_defs dtor_unfold_thms map_comp_id_thms map_cong0L_thms
end;
val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
@@ -2175,11 +2175,11 @@
end;
val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs;
in
- map3 (fn goal => fn unfold => fn map_cong =>
+ map3 (fn goal => fn unfold => fn map_cong0 =>
Goal.prove_sorry lthy [] [] goal
- (mk_corec_tac m corec_defs unfold map_cong corec_Inl_sum_thms)
+ (mk_corec_tac m corec_defs unfold map_cong0 corec_Inl_sum_thms)
|> Thm.close_derivation)
- goals dtor_unfold_thms map_congs
+ goals dtor_unfold_thms map_cong0s
end;
val corec_unique_mor_thm =
@@ -2409,11 +2409,11 @@
val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's;
val cTs = map (SOME o certifyT lthy) FTs';
val maps =
- map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong =>
+ map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong0 =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_map_tac m n cT unfold map_comp' map_cong))
+ (K (mk_map_tac m n cT unfold map_comp' map_cong0))
|> Thm.close_derivation)
- goals cTs dtor_unfold_thms map_comp's map_congs;
+ goals cTs dtor_unfold_thms map_comp's map_cong0s;
in
map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
end;
@@ -2427,7 +2427,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_congs dtor_unfold_unique_thm))
+ (K (mk_map_comp_tac m n map_thms map_comps map_cong0s dtor_unfold_unique_thm))
|> Thm.close_derivation)
end;
@@ -2548,7 +2548,7 @@
map (split_conj_thm o mk_specN n) thms
end;
- val map_cong_thms =
+ val map_cong0_thms =
let
val cTs = map (SOME o certifyT lthy o
Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params;
@@ -2559,7 +2559,7 @@
fun mk_prems sets z =
Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys')
- fun mk_map_cong sets z fmap gmap =
+ fun mk_map_cong0 sets z fmap gmap =
HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z));
fun mk_coind_body sets (x, T) z fmap gmap y y_copy =
@@ -2581,11 +2581,11 @@
val goal =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map4 mk_map_cong setss_by_bnf Jzs fs_maps fs_copy_maps));
+ (map4 mk_map_cong0 setss_by_bnf Jzs fs_maps fs_copy_maps));
val thm = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] goal
- (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_congs set_natural'ss
+ (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_natural'ss
set_hset_thmss set_hset_hset_thmsss)))
|> Thm.close_derivation
in
@@ -2685,7 +2685,7 @@
val map_id_tacs =
map2 (K oo mk_map_id_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_cong_tacs = map (mk_map_cong_tac m) map_cong_thms;
+ val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
val set_nat_tacss =
map2 (map2 (K oo mk_set_natural_tac)) hset_defss (transpose col_natural_thmss);
@@ -2709,7 +2709,7 @@
val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
- val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
+ val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
@@ -2941,14 +2941,14 @@
HOLogic.mk_mem (HOLogic.mk_prod (dtor $ Jz, dtor' $ Jz'), srelR)));
val goals = map6 mk_goal Jzs Jz's dtors dtor's JsrelRs srelRs;
in
- map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
+ map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
fn set_naturals => fn dtor_set_incls => fn dtor_set_set_inclss =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets
+ (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets
dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss))
|> Thm.close_derivation)
- ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_dtor_set_thmss'
+ ks goals in_srels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
dtor_inject_thms dtor_ctor_thms set_natural'ss dtor_set_incl_thmss
dtor_set_set_incl_thmsss
end;
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed Apr 24 14:15:01 2013 +0200
@@ -256,12 +256,12 @@
EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
atac, atac, rtac (hset_def RS sym)] 1
-fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_congs set_naturalss =
+fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_naturalss =
let
val n = length srel_O_Grs;
- val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ srel_O_Grs);
+ val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_naturalss ~~ srel_O_Grs);
- fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =
+ fun mk_if_tac ((((i, map_comp), map_cong0), set_naturals), srel_O_Gr) =
EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
rtac (srel_O_Gr RS equalityD2 RS set_mp),
@@ -276,11 +276,11 @@
else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
rtac trans_fun_cong_image_id_id_apply, atac])
(1 upto (m + n) ~~ set_naturals),
- rtac trans, rtac trans, rtac map_comp, rtac map_cong, REPEAT_DETERM_N m o rtac thm,
+ rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
@{thms fst_diag_id snd_diag_id})];
- fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =
+ fun mk_only_if_tac ((((i, map_comp), map_cong0), set_naturals), srel_O_Gr) =
EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
etac allE, etac allE, etac impE, atac,
dtac (srel_O_Gr RS equalityD1 RS set_mp),
@@ -290,13 +290,13 @@
REPEAT_DETERM o etac conjE,
hyp_subst_tac,
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
- rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong,
+ rtac bexI, rtac conjI, rtac trans, rtac map_comp, 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),
- etac sym, rtac trans, rtac map_comp, rtac trans, rtac map_cong,
+ etac sym, rtac trans, rtac map_comp, 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_cong,
+ rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
REPEAT_DETERM_N n o rtac refl,
etac sym, rtac CollectI,
@@ -841,7 +841,7 @@
fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_naturalss coalg_setss
- map_comp_ids map_congs map_arg_congs {context = ctxt, prems = _} =
+ map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} =
let
val n = length beh_defs;
val ks = 1 upto n;
@@ -939,7 +939,7 @@
(drop m set_naturals ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),
- ((map_comp_id, (map_cong, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
+ ((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
rtac (@{thm if_P} RS
(if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans),
@@ -950,7 +950,7 @@
if n = 1 then K all_tac
else (rtac (sum_case_weak_cong RS trans) THEN'
rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
- rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl),
+ rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
rtac trans, rtac @{thm Shift_def},
@@ -1001,15 +1001,15 @@
(set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
CONJ_WRAP' mor_tac
(ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
- ((map_comp_ids ~~ (map_congs ~~ map_arg_congs)) ~~
+ ((map_comp_ids ~~ (map_cong0s ~~ map_arg_congs)) ~~
(length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1
end;
-fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBISs =
+fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBISs =
EVERY' [rtac @{thm congruentI}, dtac lsbisE,
REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], rtac (o_apply RS trans),
etac (sym RS arg_cong RS trans), rtac (map_comp_id RS trans),
- rtac (map_cong RS trans), REPEAT_DETERM_N m o rtac refl,
+ rtac (map_cong0 RS trans), REPEAT_DETERM_N m o rtac refl,
EVERY' (map (fn equiv_LSBIS =>
EVERY' [rtac @{thm equiv_proj}, rtac equiv_LSBIS, etac set_mp, atac])
equiv_LSBISs), rtac sym, rtac (o_apply RS trans),
@@ -1042,18 +1042,18 @@
rtac congruent_str_final, atac, rtac o_apply])
(equiv_LSBISs ~~ congruent_str_finals)] 1;
-fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_congLs
+fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls
{context = ctxt, prems = _} =
unfold_thms_tac ctxt defs THEN
EVERY' [rtac conjI,
CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
- CONJ_WRAP' (fn (Rep, ((map_comp_id, map_congL), coalg_final_sets)) =>
- EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_congL,
+ CONJ_WRAP' (fn (Rep, ((map_comp_id, map_cong0L), coalg_final_sets)) =>
+ EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_cong0L,
EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse,
etac set_rev_mp, rtac coalg_final_set, rtac Rep])
Abs_inverses (drop m coalg_final_sets))])
- (Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1;
+ (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
unfold_thms_tac ctxt defs THEN
@@ -1061,16 +1061,16 @@
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
-fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_congs =
+fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
EVERY' [rtac iffD2, rtac mor_UNIV,
- CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong))) =>
+ CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) =>
EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
- rtac (o_apply RS trans RS sym), rtac map_cong,
+ rtac (o_apply RS trans RS sym), rtac map_cong0,
REPEAT_DETERM_N m o rtac refl,
EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) unfold_defs)])
- ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
+ ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_cong0s)))] 1;
fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
@@ -1109,17 +1109,17 @@
rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
-fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtors
+fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtors
{context = ctxt, prems = _} =
unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
- rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
+ rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
EVERY' (map (fn thm =>
rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
rtac sym, rtac id_apply] 1;
-fun mk_corec_tac m corec_defs unfold map_cong corec_Inls {context = ctxt, prems = _} =
+fun mk_corec_tac m corec_defs unfold map_cong0 corec_Inls {context = ctxt, prems = _} =
unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
- rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
+ rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
REPEAT_DETERM_N m o rtac refl,
EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
@@ -1184,9 +1184,9 @@
rtac impI, REPEAT_DETERM o etac conjE,
CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
-fun mk_map_tac m n cT unfold map_comp' map_cong =
+fun mk_map_tac m n cT unfold map_comp' map_cong0 =
EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
- rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
+ rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong0,
REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
@@ -1210,9 +1210,9 @@
EVERY' [rtac (unfold_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
rtac unfold_dtor] 1;
-fun mk_map_comp_tac m n maps map_comps map_congs unfold_unique =
+fun mk_map_comp_tac m n maps map_comps map_cong0s unfold_unique =
EVERY' [rtac unfold_unique,
- EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong =>
+ EVERY' (map3 (fn map_thm => fn map_comp => 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,
@@ -1220,12 +1220,12 @@
@{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,
- ext, o_apply RS trans, o_apply RS trans RS sym, map_cong] @
+ 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_congs)] 1;
+ maps map_comps map_cong0s)] 1;
-fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_congs set_naturalss set_hsetss
+fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_naturalss set_hsetss
set_hset_hsetsss =
let
val n = length map_comp's;
@@ -1233,13 +1233,13 @@
in
EVERY' ([rtac rev_mp,
coinduct_tac] @
- maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong), set_naturals), set_hsets),
+ maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_naturals), set_hsets),
set_hset_hsetss) =>
[REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
- rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
+ rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply),
REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
- rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
+ rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
EVERY' (maps (fn set_hset =>
[rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE,
REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
@@ -1253,7 +1253,7 @@
EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
(drop m set_naturals ~~ set_hset_hsetss)])
(map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~
- map_congs ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @
+ map_cong0s ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @
[rtac impI,
CONJ_WRAP' (fn k =>
EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,
@@ -1499,7 +1499,7 @@
ALLGOALS (TRY o
FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
-fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets dtor_inject dtor_ctor
+fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor
set_naturals dtor_set_incls dtor_set_set_inclss =
let
val m = length dtor_set_incls;
@@ -1521,7 +1521,7 @@
rtac conjI, rtac refl, rtac refl])
(in_Jsrels ~~ (active_set_naturals ~~ dtor_set_set_inclss)),
CONJ_WRAP' (fn conv =>
- EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
+ EVERY' [rtac trans, rtac map_comp, 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])
@@ -1547,7 +1547,7 @@
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 map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
+ rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
EVERY' (map (fn in_Jsrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jsrels),
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Wed Apr 24 14:15:01 2013 +0200
@@ -144,7 +144,7 @@
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 map_comp's = map map_comp'_of_bnf bnfs;
- val map_congs = map map_cong_of_bnf bnfs;
+ val map_cong0s = map map_cong0_of_bnf bnfs;
val map_ids = map map_id_of_bnf bnfs;
val map_id's = map map_id'_of_bnf bnfs;
val map_wpulls = map map_wpull_of_bnf bnfs;
@@ -195,7 +195,7 @@
(*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
map id ... id f(m+1) ... f(m+n) x = x*)
- fun mk_map_congL x mapAsAs sets map_cong map_id' =
+ fun mk_map_cong0L x mapAsAs sets map_cong0 map_id' =
let
fun mk_prem set f z z' = HOLogic.mk_Trueprop
(mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
@@ -204,11 +204,11 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
- (K (mk_map_congL_tac m map_cong map_id'))
+ (K (mk_map_cong0L_tac m map_cong0 map_id'))
|> Thm.close_derivation
end;
- val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
+ val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_id's;
val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs;
val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;
@@ -407,7 +407,7 @@
(fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ inv_fs)
(Logic.list_implies (prems, concl)))
(K (mk_mor_inv_tac alg_def mor_def
- set_natural'ss morE_thms map_comp_id_thms map_congL_thms))
+ set_natural'ss morE_thms map_comp_id_thms map_cong0L_thms))
|> Thm.close_derivation
end;
@@ -897,7 +897,7 @@
(fold_rev Logic.all (init_xs @ Bs @ ss @ init_fs @ init_fs_copy)
(Logic.list_implies (prems @ mor_prems, unique)))
(K (mk_init_unique_mor_tac m alg_def alg_init_thm least_min_alg_thms
- in_mono'_thms alg_set_thms morE_thms map_congs))
+ in_mono'_thms alg_set_thms morE_thms map_cong0s))
|> Thm.close_derivation;
in
(ex_mor, split_conj_thm unique_mor)
@@ -1180,11 +1180,11 @@
mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
val goals = map3 mk_goal dtors ctors FTs;
in
- map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_congL =>
+ map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_fold_thms))
+ (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_fold_thms))
|> Thm.close_derivation)
- goals dtor_defs ctor_fold_thms map_comp_id_thms map_congL_thms
+ goals dtor_defs ctor_fold_thms map_comp_id_thms map_cong0L_thms
end;
val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
@@ -1431,10 +1431,10 @@
HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_maps))));
val goals = map4 mk_goal fs_maps map_FTFT's ctors ctor's;
val maps =
- map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong =>
- Goal.prove_sorry lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong))
+ map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
+ Goal.prove_sorry lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong0))
|> Thm.close_derivation)
- goals ctor_fold_thms map_comp_id_thms map_congs;
+ goals ctor_fold_thms map_comp_id_thms map_cong0s;
in
map (fn thm => thm RS @{thm pointfreeE}) maps
end;
@@ -1450,7 +1450,7 @@
(map2 (curry HOLogic.mk_eq) us fs_maps));
val unique = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_congs))
+ (K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_cong0s))
|> Thm.close_derivation;
in
`split_conj_thm unique
@@ -1588,18 +1588,18 @@
map split_conj_thm thms
end;
- val map_cong_thms =
+ val map_cong0_thms =
let
fun mk_prem z set f g y y' =
mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y)));
- fun mk_map_cong sets z fmap gmap =
+ fun mk_map_cong0 sets z fmap gmap =
HOLogic.mk_imp
(Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys'),
HOLogic.mk_eq (fmap $ z, gmap $ z));
fun mk_cphi sets z fmap gmap =
- certify lthy (Term.absfree (dest_Free z) (mk_map_cong sets z fmap gmap));
+ certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
val cphis = map4 mk_cphi setss_by_bnf Izs fs_maps fs_copy_maps;
@@ -1607,11 +1607,11 @@
val goal =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map4 mk_map_cong setss_by_bnf Izs fs_maps fs_copy_maps));
+ (map4 mk_map_cong0 setss_by_bnf Izs fs_maps fs_copy_maps));
val thm = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] goal
- (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs ctor_map_thms))
+ (mk_mcong_tac (rtac induct) Fset_set_thmsss map_cong0s ctor_map_thms))
|> Thm.close_derivation;
in
split_conj_thm thm
@@ -1692,7 +1692,7 @@
val map_id_tacs = map (K o mk_map_id_tac map_ids) 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_cong_tacs = map (mk_map_cong_tac m) map_cong_thms;
+ val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
val set_nat_tacss = map (map (K o mk_set_natural_tac)) (transpose set_natural_thmss);
val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
val bd_cinf_tacs = replicate n (K (rtac (bd_Cinfinite RS conjunct1) 1));
@@ -1703,7 +1703,7 @@
val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
- val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
+ val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
val ctor_witss =
@@ -1778,14 +1778,14 @@
HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), srelR)));
val goals = map6 mk_goal xFs yFs ctors ctor's IsrelRs srelRs;
in
- map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
+ map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
fn set_naturals => fn ctor_set_incls => fn ctor_set_set_inclss =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets
+ (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
ctor_inject ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss))
|> Thm.close_derivation)
- ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_ctor_set_thmss'
+ ks goals in_srels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
ctor_inject_thms ctor_dtor_thms set_natural'ss ctor_set_incl_thmss
ctor_set_set_incl_thmsss
end;
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Apr 24 14:15:01 2013 +0200
@@ -139,7 +139,7 @@
CONJ_WRAP' mor_tac (set_natural's ~~ map_comp_ids)) 1
end;
-fun mk_mor_inv_tac alg_def mor_def set_natural's morEs map_comp_ids map_congLs =
+fun mk_mor_inv_tac alg_def mor_def set_natural's morEs map_comp_ids map_cong0Ls =
let
val fbetw_tac = EVERY' [rtac ballI, etac set_mp, etac imageI];
fun Collect_tac set_natural' =
@@ -147,12 +147,12 @@
FIRST' [rtac subset_UNIV,
(EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
etac @{thm image_mono}, atac])]) set_natural';
- fun mor_tac (set_natural', ((morE, map_comp_id), map_congL)) =
+ fun mor_tac (set_natural', ((morE, map_comp_id), map_cong0L)) =
EVERY' [rtac ballI, ftac @{thm rev_bspec}, atac,
REPEAT o eresolve_tac [CollectE, conjE], rtac sym, rtac trans, rtac sym,
etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_natural',
rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_natural',
- rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_congL RS arg_cong),
+ rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_cong0L RS arg_cong),
REPEAT_DETERM_N (length morEs) o
(EVERY' [rtac subst, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])];
in
@@ -162,7 +162,7 @@
REPEAT o etac conjE THEN'
rtac conjI THEN'
CONJ_WRAP' (K fbetw_tac) set_natural's THEN'
- CONJ_WRAP' mor_tac (set_natural's ~~ (morEs ~~ map_comp_ids ~~ map_congLs))) 1
+ CONJ_WRAP' mor_tac (set_natural's ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1
end;
fun mk_mor_str_tac ks mor_def =
@@ -436,7 +436,7 @@
end;
fun mk_init_unique_mor_tac m
- alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_congs =
+ alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_cong0s =
let
val n = length least_min_algs;
val ks = (1 upto n);
@@ -444,22 +444,22 @@
fun mor_tac morE in_mono = EVERY' [etac morE, rtac set_mp, rtac in_mono,
REPEAT_DETERM_N n o rtac @{thm Collect_restrict}, rtac CollectI,
REPEAT_DETERM_N (m + n) o (TRY o rtac conjI THEN' atac)];
- fun cong_tac map_cong = EVERY' [rtac (map_cong RS arg_cong),
+ fun cong_tac map_cong0 = EVERY' [rtac (map_cong0 RS arg_cong),
REPEAT_DETERM_N m o rtac refl,
REPEAT_DETERM_N n o (etac @{thm prop_restrict} THEN' atac)];
- fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong))) = EVERY' [rtac ballI, rtac CollectI,
+ fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong0))) = EVERY' [rtac ballI, rtac CollectI,
REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
REPEAT_DETERM_N m o rtac subset_UNIV,
REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
rtac trans, mor_tac morE in_mono,
- rtac trans, cong_tac map_cong,
+ rtac trans, cong_tac map_cong0,
rtac sym, mor_tac morE in_mono];
fun mk_unique_tac (k, least_min_alg) =
select_prem_tac n (etac @{thm prop_restrict}) k THEN' rtac least_min_alg THEN'
stac alg_def THEN'
- CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_congs)));
+ CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s)));
in
CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1
end;
@@ -514,9 +514,9 @@
CONJ_WRAP' mk_unique type_defs 1
end;
-fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_folds =
+fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_folds =
EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx,
- rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
+ rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
ctor_o_folds),
rtac sym, rtac id_apply] 1;
@@ -575,16 +575,16 @@
CONJ_WRAP' (K atac) ks] 1
end;
-fun mk_map_tac m n foldx map_comp_id map_cong =
+fun mk_map_tac m n foldx map_comp_id map_cong0 =
EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans, rtac o_apply,
- rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong RS arg_cong),
+ rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong0 RS arg_cong),
REPEAT_DETERM_N m o rtac refl,
REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
rtac sym, rtac o_apply] 1;
-fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_congs =
+fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_cong0s =
let
- val n = length map_congs;
+ val n = length map_cong0s;
fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm pointfreeE},
rtac sym, rtac trans, rtac o_apply, rtac trans, rtac (comp_id RS arg_cong),
rtac (cong RS arg_cong),
@@ -592,8 +592,8 @@
REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply]))];
in
EVERY' [rtac fold_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
- CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_congs,
- CONJ_WRAP' mk_mor (map_comp_ids ~~ map_congs)] 1
+ CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_cong0s,
+ CONJ_WRAP' mk_mor (map_comp_ids ~~ map_cong0s)] 1
end;
fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
@@ -647,7 +647,7 @@
(induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1
end;
-fun mk_mcong_tac induct_tac set_setsss map_congs ctor_maps {context = ctxt, prems = _} =
+fun mk_mcong_tac induct_tac set_setsss map_cong0s ctor_maps {context = ctxt, prems = _} =
let
fun use_asm thm = EVERY' [etac bspec, etac set_rev_mp, rtac thm];
@@ -655,14 +655,14 @@
CONJ_WRAP' (fn thm =>
EVERY' [rtac ballI, etac bspec, etac set_rev_mp, etac thm]) set_sets];
- fun mk_map_cong ctor_map map_cong set_setss =
+ fun mk_map_cong0 ctor_map map_cong0 set_setss =
EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
- rtac trans, rtac ctor_map, rtac trans, rtac (map_cong RS arg_cong),
+ rtac trans, rtac ctor_map, rtac trans, rtac (map_cong0 RS arg_cong),
EVERY' (map use_asm (map hd set_setss)),
EVERY' (map useIH (transpose (map tl set_setss))),
rtac sym, rtac ctor_map];
in
- (induct_tac THEN' EVERY' (map3 mk_map_cong ctor_maps map_congs set_setsss)) 1
+ (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
end;
fun mk_incl_min_alg_tac induct_tac set_setsss alg_sets alg_min_alg {context = ctxt, prems = _} =
@@ -775,7 +775,7 @@
EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
REPEAT_DETERM_N n o etac UnE]))))] 1);
-fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets ctor_inject
+fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject
ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss =
let
val m = length ctor_set_incls;
@@ -802,7 +802,7 @@
rtac conjI, rtac refl, rtac refl])
(in_Isrels ~~ (active_set_naturals ~~ ctor_set_set_inclss)),
CONJ_WRAP' (fn conv =>
- EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
+ EVERY' [rtac trans, rtac map_comp, 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,
@@ -827,7 +827,7 @@
(ctor_sets ~~ passive_set_naturals),
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_cong,
+ rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
EVERY' (map (fn in_Isrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Wed Apr 24 14:15:01 2013 +0200
@@ -27,8 +27,8 @@
thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
val mk_map_comp_id_tac: thm -> tactic
- val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
- val mk_map_congL_tac: int -> thm -> thm -> tactic
+ val mk_map_cong0_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_map_cong0L_tac: int -> thm -> thm -> tactic
end;
structure BNF_Tactics : BNF_TACTICS =
@@ -101,12 +101,12 @@
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_cong_tac m map_cong {context = ctxt, prems = _} =
- EVERY' [rtac mp, rtac map_cong,
+fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
+ EVERY' [rtac mp, rtac map_cong0,
CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
-fun mk_map_congL_tac passive map_cong map_id' =
- (rtac trans THEN' rtac map_cong THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
+fun mk_map_cong0L_tac passive map_cong0 map_id' =
+ (rtac trans THEN' rtac map_cong0 THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN
rtac map_id' 1;