--- a/src/HOL/BNF/More_BNFs.thy Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Thu Aug 29 22:53:17 2013 +0200
@@ -227,7 +227,7 @@
apply transfer apply simp
done
-lemmas [simp] = fset.map_comp' fset.map_id' fset.set_map'
+lemmas [simp] = fset.map_comp fset.map_id fset.set_map'
lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
unfolding fset_rel_def set_rel_def by auto
--- a/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 22:53:17 2013 +0200
@@ -153,12 +153,12 @@
mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
(map map_id0_of_bnf inners);
- fun map_comp_tac _ =
- mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
- (map map_comp_of_bnf inners);
+ fun map_comp0_tac _ =
+ mk_comp_map_comp0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer)
+ (map map_comp0_of_bnf inners);
fun mk_single_set_map_tac i _ =
- mk_comp_set_map_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
+ mk_comp_set_map_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer)
(collect_set_map_of_bnf outer)
(map ((fn thms => nth thms i) o set_map_of_bnf) inners);
@@ -233,7 +233,7 @@
rtac thm 1
end;
- val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -301,8 +301,8 @@
(Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
- fun map_comp_tac {context = ctxt, prems = _} =
- unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+ fun map_comp0_tac {context = ctxt, prems = _} =
+ unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
rtac refl 1;
fun map_cong0_tac {context = ctxt, prems = _} =
mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
@@ -339,7 +339,7 @@
rtac thm 1
end;
- val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -391,8 +391,8 @@
val bd = mk_bd_of_bnf Ds As bnf;
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
- fun map_comp_tac {context = ctxt, prems = _} =
- unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+ fun map_comp0_tac {context = ctxt, prems = _} =
+ unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
rtac refl 1;
fun map_cong0_tac {context = ctxt, prems = _} =
rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
@@ -424,7 +424,7 @@
fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
- val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -475,7 +475,7 @@
val bd = mk_bd_of_bnf Ds As bnf;
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
- fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
+ fun map_comp0_tac _ = rtac (map_comp0_of_bnf bnf) 1;
fun map_cong0_tac {context = ctxt, prems = _} =
rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
val set_map_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf));
@@ -497,7 +497,7 @@
fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
- val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -630,7 +630,7 @@
(rtac (unfold_all thm) THEN'
SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
- val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
+ val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf))
(mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
(K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds)
(mk_tac (map_wpull_of_bnf bnf))
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 22:53:17 2013 +0200
@@ -11,7 +11,7 @@
val mk_comp_bd_card_order_tac: thm list -> thm -> tactic
val mk_comp_bd_cinfinite_tac: thm -> thm -> tactic
val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
- val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic
+ val mk_comp_map_comp0_tac: thm -> thm -> thm list -> tactic
val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic
val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
@@ -62,17 +62,17 @@
EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1;
-fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps =
+fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s =
EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
- rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
- map (fn thm => rtac (thm RS sym RS fun_cong)) map_comps) 1;
+ rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
+ map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1;
-fun mk_comp_set_map_tac Gmap_comp Gmap_cong0 Gset_map set_maps =
+fun mk_comp_set_map_tac Gmap_comp0 Gmap_cong0 Gset_map set_maps =
EVERY' ([rtac ext] @
replicate 3 (rtac trans_o_apply) @
[rtac (arg_cong_Union RS trans),
rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
- rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans),
+ rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans),
rtac Gmap_cong0] @
map (fn thm => rtac (thm RS fun_cong)) set_maps @
[rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
--- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 22:53:17 2013 +0200
@@ -50,13 +50,13 @@
val in_cong_of_bnf: bnf -> thm
val in_mono_of_bnf: bnf -> thm
val in_rel_of_bnf: bnf -> thm
- val map_comp'_of_bnf: bnf -> thm
+ val map_comp0_of_bnf: bnf -> thm
val map_comp_of_bnf: bnf -> thm
val map_cong0_of_bnf: bnf -> thm
val map_cong_of_bnf: bnf -> thm
val map_def_of_bnf: bnf -> thm
val map_id0_of_bnf: bnf -> thm
- val map_id'_of_bnf: bnf -> thm
+ val map_id_of_bnf: bnf -> thm
val map_transfer_of_bnf: bnf -> thm
val map_wppull_of_bnf: bnf -> thm
val map_wpull_of_bnf: bnf -> thm
@@ -114,7 +114,7 @@
type axioms = {
map_id0: thm,
- map_comp: thm,
+ map_comp0: thm,
map_cong0: thm,
set_map: thm list,
bd_card_order: thm,
@@ -125,7 +125,7 @@
};
fun mk_axioms' ((((((((id, comp), cong), nat), c_o), cinf), set_bd), wpull), rel) =
- {map_id0 = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
+ {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
bd_cinfinite = cinf, set_bd = set_bd, map_wpull = wpull, rel_OO_Grp = rel};
fun dest_cons [] = raise List.Empty
@@ -147,15 +147,15 @@
fun zip_axioms mid mcomp mcong snat bdco bdinf sbd wpull rel =
[mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [wpull, rel];
-fun dest_axioms {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun dest_axioms {map_id0, map_comp0, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
map_wpull, rel_OO_Grp} =
- zip_axioms map_id0 map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
+ zip_axioms map_id0 map_comp0 map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
rel_OO_Grp;
-fun map_axioms f {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun map_axioms f {map_id0, map_comp0, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
map_wpull, rel_OO_Grp} =
{map_id0 = f map_id0,
- map_comp = f map_comp,
+ map_comp0 = f map_comp0,
map_cong0 = f map_cong0,
set_map = map f set_map,
bd_card_order = f bd_card_order,
@@ -188,9 +188,9 @@
in_cong: thm lazy,
in_mono: thm lazy,
in_rel: thm lazy,
- map_comp': thm lazy,
+ map_comp: thm lazy,
map_cong: thm lazy,
- map_id': thm lazy,
+ map_id: thm lazy,
map_transfer: thm lazy,
map_wppull: thm lazy,
rel_eq: thm lazy,
@@ -205,7 +205,7 @@
};
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
- map_comp' map_cong map_id' map_transfer map_wppull rel_eq rel_flip set_map' rel_cong rel_mono
+ map_comp map_cong map_id map_transfer map_wppull rel_eq rel_flip set_map' rel_cong rel_mono
rel_mono_strong rel_Grp rel_conversep rel_OO = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
@@ -215,9 +215,9 @@
in_cong = in_cong,
in_mono = in_mono,
in_rel = in_rel,
- map_comp' = map_comp',
+ map_comp = map_comp,
map_cong = map_cong,
- map_id' = map_id',
+ map_id = map_id,
map_transfer = map_transfer,
map_wppull = map_wppull,
rel_eq = rel_eq,
@@ -239,9 +239,9 @@
in_cong,
in_mono,
in_rel,
- map_comp',
+ map_comp,
map_cong,
- map_id',
+ map_id,
map_transfer,
map_wppull,
rel_eq,
@@ -261,9 +261,9 @@
in_cong = Lazy.map f in_cong,
in_mono = Lazy.map f in_mono,
in_rel = Lazy.map f in_rel,
- map_comp' = Lazy.map f map_comp',
+ map_comp = Lazy.map f map_comp,
map_cong = Lazy.map f map_cong,
- map_id' = Lazy.map f map_id',
+ map_id = Lazy.map f map_id,
map_transfer = Lazy.map f map_transfer,
map_wppull = Lazy.map f map_wppull,
rel_eq = Lazy.map f rel_eq,
@@ -381,9 +381,9 @@
val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
val map_def_of_bnf = #map_def o #defs o rep_bnf;
val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf;
-val map_id'_of_bnf = Lazy.force o #map_id' o #facts o rep_bnf;
-val map_comp_of_bnf = #map_comp o #axioms o rep_bnf;
-val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
+val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf;
+val map_comp0_of_bnf = #map_comp0 o #axioms o rep_bnf;
+val map_comp_of_bnf = Lazy.force o #map_comp o #facts o rep_bnf;
val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
@@ -509,9 +509,9 @@
val in_monoN = "in_mono";
val in_relN = "in_rel";
val map_id0N = "map_id0";
-val map_id'N = "map_id'";
+val map_idN = "map_id";
+val map_comp0N = "map_comp0";
val map_compN = "map_comp";
-val map_comp'N = "map_comp'";
val map_cong0N = "map_cong0";
val map_congN = "map_cong";
val map_transferN = "map_transfer";
@@ -558,7 +558,7 @@
(in_bdN, [Lazy.force (#in_bd facts)]),
(in_monoN, [Lazy.force (#in_mono facts)]),
(in_relN, [Lazy.force (#in_rel facts)]),
- (map_compN, [#map_comp axioms]),
+ (map_comp0N, [#map_comp0 axioms]),
(map_id0N, [#map_id0 axioms]),
(map_transferN, [Lazy.force (#map_transfer facts)]),
(map_wpullN, [#map_wpull axioms]),
@@ -577,10 +577,10 @@
#> (if fact_policy <> Dont_Note then
let
val notes =
- [(map_comp'N, [Lazy.force (#map_comp' facts)], []),
+ [(map_compN, [Lazy.force (#map_comp facts)], []),
(map_cong0N, [#map_cong0 axioms], []),
(map_congN, [Lazy.force (#map_cong facts)], fundef_cong_attrs),
- (map_id'N, [Lazy.force (#map_id' facts)], []),
+ (map_idN, [Lazy.force (#map_id facts)], []),
(rel_eqN, [Lazy.force (#rel_eq facts)], []),
(rel_flipN, [Lazy.force (#rel_flip facts)], []),
(set_map'N, map Lazy.force (#set_map' facts), []),
@@ -850,7 +850,7 @@
mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA')
end;
- val map_comp_goal =
+ val map_comp0_goal =
let
val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs);
val comp_bnf_map_app = HOLogic.mk_comp
@@ -922,7 +922,7 @@
val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp));
- val goals = zip_axioms map_id0_goal map_comp_goal map_cong0_goal set_maps_goal
+ val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_maps_goal
card_order_bd_goal cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal;
fun mk_wit_goals (I, wit) =
@@ -1000,8 +1000,8 @@
val in_cong = Lazy.lazy mk_in_cong;
- val map_id' = Lazy.lazy (fn () => mk_map_id' (#map_id0 axioms));
- val map_comp' = Lazy.lazy (fn () => mk_map_comp' (#map_comp axioms));
+ val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms));
+ val map_comp = Lazy.lazy (fn () => mk_map_comp (#map_comp0 axioms));
fun mk_map_cong () =
let
@@ -1049,7 +1049,7 @@
in
Goal.prove_sorry lthy [] [] in_bd_goal
(mk_in_bd_tac live surj_imp_ordLeq_inst
- (Lazy.force map_comp') (Lazy.force map_id') (#map_cong0 axioms)
+ (Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms)
(map Lazy.force set_map') (#set_bd axioms) (#bd_card_order axioms)
bd_Card_order bd_Cinfinite bd_Cnotzero)
|> Thm.close_derivation
@@ -1087,7 +1087,7 @@
in
Goal.prove_sorry lthy [] [] goal
(fn _ => mk_map_wppull_tac (#map_id0 axioms) (#map_cong0 axioms)
- (#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_map'))
+ (#map_wpull axioms) (Lazy.force map_comp) (map Lazy.force set_map'))
|> Thm.close_derivation
end;
@@ -1102,8 +1102,8 @@
val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
in
Goal.prove_sorry lthy [] [] goal
- (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id')
- (Lazy.force map_comp') (map Lazy.force set_map'))
+ (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id)
+ (Lazy.force map_comp) (map Lazy.force set_map'))
|> Thm.close_derivation
end;
@@ -1155,7 +1155,7 @@
val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_leq lhs rhs));
val le_thm = Goal.prove_sorry lthy [] [] le_goal
(mk_rel_conversep_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
- (Lazy.force map_comp') (map Lazy.force set_map'))
+ (Lazy.force map_comp) (map Lazy.force set_map'))
|> Thm.close_derivation
val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
in
@@ -1176,7 +1176,7 @@
in
Goal.prove_sorry lthy [] [] goal
(mk_rel_OO_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
- (Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_map'))
+ (Lazy.force map_wppull) (Lazy.force map_comp) (map Lazy.force set_map'))
|> Thm.close_derivation
end;
@@ -1245,7 +1245,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl)
(mk_map_transfer_tac (Lazy.force rel_mono) (Lazy.force in_rel)
- (map Lazy.force set_map') (#map_cong0 axioms) (Lazy.force map_comp'))
+ (map Lazy.force set_map') (#map_cong0 axioms) (Lazy.force map_comp))
|> Thm.close_derivation
end;
@@ -1254,7 +1254,7 @@
val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
- in_mono in_rel map_comp' map_cong map_id' map_transfer map_wppull rel_eq rel_flip set_map'
+ in_mono in_rel map_comp map_cong map_id map_transfer map_wppull rel_eq rel_flip set_map'
rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
val wits = map2 mk_witness bnf_wits wit_thms;
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 22:53:17 2013 +0200
@@ -9,8 +9,8 @@
signature BNF_DEF_TACTICS =
sig
val mk_collect_set_map_tac: thm list -> tactic
- val mk_map_id': thm -> thm
- val mk_map_comp': thm -> thm
+ val mk_map_id: thm -> thm
+ val mk_map_comp: thm -> thm
val mk_map_cong_tac: Proof.context -> thm -> tactic
val mk_in_mono_tac: int -> tactic
val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
@@ -45,8 +45,8 @@
val ord_le_eq_trans = @{thm ord_le_eq_trans};
val conversep_shift = @{thm conversep_le_swap} RS iffD1;
-fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
-fun mk_map_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
+fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply};
+fun mk_map_comp comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
fun mk_map_cong_tac ctxt cong0 =
(hyp_subst_tac ctxt THEN' rtac cong0 THEN'
REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
@@ -66,7 +66,7 @@
rtac set_map) set_maps) THEN'
rtac @{thm image_empty}) 1;
-fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp set_maps =
+fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp0 set_maps =
if null set_maps then
EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id0, rtac map_id0] 1
else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
@@ -76,13 +76,13 @@
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
set_maps,
- CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
- rtac (map_comp RS trans RS sym), rtac map_cong0,
+ CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp0 RS trans), rtac (map_comp0 RS trans),
+ rtac (map_comp0 RS trans RS sym), rtac map_cong0,
REPEAT_DETERM_N (length set_maps) o EVERY' [rtac (o_apply RS trans),
rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
-fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id' map_comp set_maps
+fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp0 set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
@@ -95,7 +95,7 @@
EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I},
REPEAT_DETERM o
eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
- hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
+ hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac map_cong0,
REPEAT_DETERM_N n o EVERY' [rtac @{thm Collect_split_Grp_eqD}, etac @{thm set_mp}, atac],
rtac CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
@@ -105,7 +105,7 @@
hyp_subst_tac ctxt,
rtac @{thm relcomppI}, rtac @{thm conversepI},
EVERY' (map2 (fn convol => fn map_id0 =>
- EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id0]),
+ EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp0 RS sym, map_id0]),
REPEAT_DETERM_N n o rtac (convol RS fun_cong),
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac CollectI,
@@ -113,7 +113,7 @@
EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
rtac @{thm convol_mem_GrpI}, etac set_mp, atac])
set_maps])
- @{thms fst_convol snd_convol} [map_id', refl])] 1
+ @{thms fst_convol snd_convol} [map_id, refl])] 1
end;
fun mk_rel_eq_tac n rel_Grp rel_cong map_id0 =
@@ -135,7 +135,7 @@
rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1
end;
-fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
+fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp0 set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
@@ -151,7 +151,7 @@
hyp_subst_tac ctxt, rtac @{thm conversepI}, rtac @{thm relcomppI}, rtac @{thm conversepI},
EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac sym, rtac trans,
rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
- rtac (map_comp RS sym), rtac CollectI,
+ rtac (map_comp0 RS sym), rtac CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
end;
@@ -161,7 +161,7 @@
rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono,
REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
-fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp set_maps
+fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp0 set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
@@ -180,20 +180,20 @@
eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
hyp_subst_tac ctxt,
rtac @{thm relcomppI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI},
- rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
+ rtac trans, rtac map_comp0, rtac sym, rtac map_cong0,
REPEAT_DETERM_N n o rtac @{thm fst_fstOp},
in_tac @{thm fstOp_in},
- rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
+ rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac map_cong0,
REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply,
rtac ballE, rtac subst,
rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE,
etac set_mp, atac],
in_tac @{thm fstOp_in},
rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI},
- rtac trans, rtac map_comp, rtac map_cong0,
+ rtac trans, rtac map_comp0, rtac map_cong0,
REPEAT_DETERM_N n o rtac o_apply,
in_tac @{thm sndOp_in},
- rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
+ rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac sym, rtac map_cong0,
REPEAT_DETERM_N n o rtac @{thm snd_sndOp},
in_tac @{thm sndOp_in},
rtac @{thm predicate2I},
@@ -206,7 +206,7 @@
rtac @{thm relcomppI}, rtac @{thm conversepI},
EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans,
rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
- rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
+ rtac (map_comp0 RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
end;
fun mk_in_rel_tac rel_OO_Gr {context = ctxt, prems = _} =
@@ -226,7 +226,7 @@
EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
-fun mk_map_transfer_tac rel_mono in_rel set_map's map_cong0 map_comp'
+fun mk_map_transfer_tac rel_mono in_rel set_map's map_cong0 map_comp
{context = ctxt, prems = _} =
let
val n = length set_map's;
@@ -242,11 +242,11 @@
set_map's,
rtac conjI,
EVERY' (map (fn convol =>
- rtac (box_equals OF [map_cong0, map_comp' RS sym, map_comp' RS sym]) THEN'
+ rtac (box_equals OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN'
REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})])
end;
-fun mk_in_bd_tac live surj_imp_ordLeq_inst map_comp' map_id' map_cong0 set_map's set_bds
+fun mk_in_bd_tac live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_map's set_bds
bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero {context = ctxt, prems = _} =
if live = 0 then
rtac @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order]
@@ -294,7 +294,7 @@
rtac sym,
rtac (Drule.rotate_prems 1
((box_equals OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
- map_comp' RS sym, map_id']) RSN (2, trans))),
+ map_comp RS sym, map_id]) RSN (2, trans))),
REPEAT_DETERM_N (2 * live) o atac,
REPEAT_DETERM_N live o rtac (@{thm prod.cases} RS trans),
rtac refl,
@@ -305,7 +305,7 @@
set_map's,
rtac sym,
rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF sum_case_o_inj(1)]},
- map_comp' RS sym, map_id'])] 1
+ map_comp RS sym, map_id])] 1
end;
end;
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 22:53:17 2013 +0200
@@ -602,8 +602,8 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
- val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
- val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
+ val nesting_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
+ val nested_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -726,7 +726,7 @@
val goalss = map5 (map4 o mk_goal fss) fiters xctrss fss xsss fxsss;
val tacss =
- map2 (map o mk_iter_tac pre_map_defs (nested_map_ids'' @ nesting_map_ids'') iter_defs)
+ map2 (map o mk_iter_tac pre_map_defs (nested_map_id's @ nesting_map_id's) iter_defs)
ctor_iter_thms ctr_defss;
fun prove goal tac =
@@ -763,7 +763,7 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
- val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
+ val nesting_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -919,10 +919,10 @@
val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
val unfold_tacss =
- map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'')
+ map3 (map oo mk_coiter_tac unfold_defs nesting_map_id's)
(map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
val corec_tacss =
- map3 (map oo mk_coiter_tac corec_defs nesting_map_ids'')
+ map3 (map oo mk_coiter_tac corec_defs nesting_map_id's)
(map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
fun prove goal tac =
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Aug 29 22:53:17 2013 +0200
@@ -94,17 +94,17 @@
@{thms comp_def convol_def fst_conv id_def prod_case_Pair_iden snd_conv
split_conv unit_case_Unity} @ sum_prod_thms_map;
-fun mk_iter_tac pre_map_defs map_ids'' iter_defs ctor_iter ctr_def ctxt =
- unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_ids'' @
+fun mk_iter_tac pre_map_defs map_id's iter_defs ctor_iter ctr_def ctxt =
+ unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_id's @
iter_unfold_thms) THEN HEADGOAL (rtac refl);
val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
-fun mk_coiter_tac coiter_defs map_ids'' ctor_dtor_coiter pre_map_def ctr_def ctxt =
+fun mk_coiter_tac coiter_defs map_id's ctor_dtor_coiter pre_map_def ctr_def ctxt =
unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN
HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN'
asm_simp_tac (put_simpset ss_if_True_False ctxt)) THEN_MAYBE
- (unfold_thms_tac ctxt (pre_map_def :: map_ids'' @ coiter_unfold_thms) THEN
+ (unfold_thms_tac ctxt (pre_map_def :: map_id's @ coiter_unfold_thms) THEN
HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)));
fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt =
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 22:53:17 2013 +0200
@@ -214,12 +214,12 @@
val bd_Cinfinites = map bd_Cinfinite_of_bnf bnfs;
val bd_Cinfinite = hd bd_Cinfinites;
val in_monos = map in_mono_of_bnf bnfs;
+ val map_comp0s = map map_comp0_of_bnf bnfs;
+ val sym_map_comps = map mk_sym map_comp0s;
val map_comps = map map_comp_of_bnf bnfs;
- val sym_map_comps = map mk_sym map_comps;
- val map_comp's = map map_comp'_of_bnf bnfs;
val map_cong0s = map map_cong0_of_bnf bnfs;
val map_id0s = map map_id0_of_bnf bnfs;
- val map_id's = map map_id'_of_bnf bnfs;
+ val map_ids = map map_id_of_bnf bnfs;
val map_wpulls = map map_wpull_of_bnf bnfs;
val set_bdss = map set_bd_of_bnf bnfs;
val set_map'ss = map set_map'_of_bnf bnfs;
@@ -237,7 +237,7 @@
(*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) =
map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
- fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp =
+ fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 =
let
val lhs = Term.list_comb (mapBsCs, all_gs) $
(Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
@@ -246,15 +246,15 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
- (K (mk_map_comp_id_tac map_comp))
+ (K (mk_map_comp_id_tac map_comp0))
|> Thm.close_derivation
end;
- val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comp's;
+ val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
(*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_cong0L x mapAsAs sets map_cong0 map_id' =
+ fun mk_map_cong0L x mapAsAs sets map_cong0 map_id =
let
fun mk_prem set f z z' =
HOLogic.mk_Trueprop
@@ -264,11 +264,11 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
- (K (mk_map_cong0L_tac m map_cong0 map_id'))
+ (K (mk_map_cong0L_tac m map_cong0 map_id))
|> Thm.close_derivation
end;
- val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_id's;
+ val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
val in_mono'_thms = map (fn thm =>
(thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos;
@@ -438,7 +438,7 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
- (K (mk_mor_incl_tac mor_def map_id's))
+ (K (mk_mor_incl_tac mor_def map_ids))
|> Thm.close_derivation
end;
@@ -809,7 +809,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_rel_tac lthy m bis_def rel_OO_Grps map_comp's map_cong0s set_map'ss))
+ (K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comps map_cong0s set_map'ss))
|> Thm.close_derivation
end;
@@ -2098,7 +2098,7 @@
dtor_set_induct_thms, dtor_Jrel_thms, lthy) =
if m = 0 then
(timer, replicate n DEADID_bnf,
- map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_id's),
+ map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids),
replicate n [], [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, lthy)
else let
val fTs = map2 (curry op -->) passiveAs passiveBs;
@@ -2184,16 +2184,16 @@
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_cong0 =>
+ 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_cong0))
+ (K (mk_map_tac m n cT unfold map_comp map_cong0))
|> Thm.close_derivation)
- goals cTs dtor_unfold_thms map_comp's map_cong0s;
+ goals cTs dtor_unfold_thms map_comps map_cong0s;
in
map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
end;
- val map_comp_thms =
+ val map_comp0_thms =
let
val goal = fold_rev Logic.all (fs @ gs)
(HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -2202,7 +2202,7 @@
fs_maps gs_maps fgs_maps)))
in
split_conj_thm (Goal.prove_sorry lthy [] [] goal
- (K (mk_map_comp_tac m n map_thms map_comps map_cong0s dtor_unfold_unique_thm))
+ (K (mk_map_comp0_tac m n map_thms map_comp0s map_cong0s dtor_unfold_unique_thm))
|> Thm.close_derivation)
end;
@@ -2360,7 +2360,7 @@
val thm = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] goal
- (K (mk_mcong_tac lthy m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_map'ss
+ (K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_map_thms map_cong0s set_map'ss
set_hset_thmss set_hset_hset_thmsss)))
|> Thm.close_derivation
in
@@ -2420,11 +2420,11 @@
(Logic.mk_implies (wpull_prem, mor_pick));
in
(Goal.prove_sorry lthy [] [] fst_goal (mk_mor_thePull_fst_tac m mor_def map_wpull_thms
- map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
+ map_comps pickWP_assms_tacs) |> Thm.close_derivation,
Goal.prove_sorry lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms
- map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
+ map_comps pickWP_assms_tacs) |> Thm.close_derivation,
Goal.prove_sorry lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms
- map_comp's) |> Thm.close_derivation)
+ map_comps) |> Thm.close_derivation)
end;
val pick_col_thmss =
@@ -2459,7 +2459,7 @@
val map_id0_tacs =
map2 (K oo mk_map_id0_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms;
- val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms;
+ val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp0_thms;
val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
val set_nat_tacss =
map2 (map2 (K oo mk_set_map_tac)) hset_defss (transpose col_natural_thmss);
@@ -2476,7 +2476,7 @@
val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
- val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
+ val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss
bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs;
val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
@@ -2699,14 +2699,14 @@
(mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz')));
val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
in
- map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 =>
+ map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets
+ (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets
dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss))
|> Thm.close_derivation)
- ks goals in_rels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
+ ks goals in_rels map_comps map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
dtor_inject_thms dtor_ctor_thms set_map'ss dtor_set_incl_thmss
dtor_set_set_incl_thmsss
end;
@@ -2801,7 +2801,7 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map6 (mk_helper_coind_concl false)
activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds));
- val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comp's
+ val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comps
map_cong0s map_arg_cong_thms set_map'ss dtor_unfold_thms folded_dtor_map_thms;
fun mk_helper_coind_thms vars concl =
Goal.prove_sorry lthy [] []
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 22:53:17 2013 +0200
@@ -52,7 +52,7 @@
val mk_incl_lsbis_tac: int -> int -> thm -> tactic
val mk_length_Lev'_tac: thm -> tactic
val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
- val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
+ val mk_map_comp0_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
thm list list -> thm list list -> thm list list list -> tactic
val mk_map_id0_tac: thm list -> thm -> thm -> tactic
@@ -160,12 +160,12 @@
etac bspec THEN'
atac) 1;
-fun mk_mor_incl_tac mor_def map_id's =
+fun mk_mor_incl_tac mor_def map_ids =
(stac mor_def THEN'
rtac conjI THEN'
- CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_id's THEN'
+ CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_ids THEN'
CONJ_WRAP' (fn thm =>
- (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_id's) 1;
+ (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_ids) 1;
fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =
let
@@ -256,19 +256,19 @@
(rev ((1 upto n) ~~ (active_set_maps ~~ coalg_sets)))])
(rec_Sucs ~~ (morEs ~~ (map (chop m) set_mapss ~~ map (drop m) coalg_setss)))] 1;
-fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comps map_cong0s set_mapss =
+fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comp0s map_cong0s set_mapss =
let
val n = length rel_OO_Grps;
- val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ rel_OO_Grps);
+ val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_mapss ~~ rel_OO_Grps);
- fun mk_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) =
+ fun mk_if_tac ((((i, map_comp0), map_cong0), set_maps), rel_OO_Grp) =
EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
rtac (rel_OO_Grp RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
rtac @{thm relcomppI}, rtac @{thm conversepI},
EVERY' (map (fn thm =>
EVERY' [rtac @{thm GrpI},
- rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
+ rtac trans, rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac,
REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
CONJ_WRAP' (fn (i, thm) =>
@@ -281,17 +281,17 @@
(1 upto (m + n) ~~ set_maps)])
@{thms fst_diag_id snd_diag_id})];
- fun mk_only_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) =
+ fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_maps), rel_OO_Grp) =
EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
etac allE, etac allE, etac impE, atac,
dtac (rel_OO_Grp RS @{thm eq_refl} RS @{thm predicate2D}),
REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @
@{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}),
hyp_subst_tac ctxt,
- rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+ rtac bexI, rtac conjI, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
- atac, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+ atac, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
rtac trans, rtac map_cong0,
@@ -1008,9 +1008,9 @@
rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
end;
-fun mk_map_tac m n cT unfold map_comp' map_cong0 =
+fun mk_map_tac m n cT unfold map_comp map_cong0 =
EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
- rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong0,
+ 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;
@@ -1034,36 +1034,36 @@
EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps),
rtac unfold_dtor] 1;
-fun mk_map_comp_tac m n maps map_comps map_cong0s unfold_unique =
+fun mk_map_comp0_tac m n maps map_comp0s map_cong0s unfold_unique =
EVERY' [rtac unfold_unique,
- EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong0 =>
+ EVERY' (map3 (fn map_thm => fn map_comp0 => fn map_cong0 =>
EVERY' (map rtac
([@{thm o_assoc} RS trans,
- @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
+ @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans,
@{thm o_assoc} RS trans RS sym,
@{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans,
@{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans,
- @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
+ @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans,
ext, o_apply RS trans, o_apply RS trans RS sym, map_cong0] @
replicate m (@{thm id_o} RS fun_cong) @
replicate n (@{thm o_id} RS fun_cong))))
- maps map_comps map_cong0s)] 1;
+ maps map_comp0s map_cong0s)] 1;
-fun mk_mcong_tac ctxt m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
+fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_mapss set_hsetss
set_hset_hsetsss =
let
- val n = length map_comp's;
+ val n = length map_comps;
val ks = 1 upto n;
in
EVERY' ([rtac rev_mp,
coinduct_tac] @
- maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets),
+ maps (fn (((((map_comp_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets),
set_hset_hsetss) =>
[REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, rtac conjI,
- rtac conjI, rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
+ rtac conjI, 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_cong0,
+ 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),
@@ -1076,7 +1076,7 @@
CONJ_WRAP' (fn set_hset_hset =>
EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
(drop m set_maps ~~ set_hset_hsetss)])
- (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~
+ (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~
map_cong0s ~~ set_mapss ~~ set_hsetss ~~ set_hset_hsetsss) @
[rtac impI,
CONJ_WRAP' (fn k =>
@@ -1177,38 +1177,38 @@
(drop m set_maps)])
(map_wpulls ~~ (pickWP_assms_tacs ~~ set_mapss)) 1;
-fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs
+fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comp0s pickWP_assms_tacs
{context = ctxt, prems = _: thm list} =
let
- val n = length map_comps;
+ val n = length map_comp0s;
in
unfold_thms_tac ctxt [mor_def] THEN
EVERY' [rtac conjI,
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
- CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
+ CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp0)) =>
EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
hyp_subst_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
- rtac (map_comp RS trans),
+ rtac (map_comp0 RS trans),
SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
pickWP_assms_tac])
- (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1
+ (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comp0s))] 1
end;
val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)};
val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
-fun mk_mor_thePull_pick_tac mor_def unfolds map_comps {context = ctxt, prems = _} =
+fun mk_mor_thePull_pick_tac mor_def unfolds map_comp0s {context = ctxt, prems = _} =
unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
- CONJ_WRAP' (fn (unfold, map_comp) =>
+ CONJ_WRAP' (fn (unfold, map_comp0) =>
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
hyp_subst_tac ctxt,
- SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
+ SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp0 :: @{thms comp_def id_def})),
rtac refl])
- (unfolds ~~ map_comps) 1;
+ (unfolds ~~ map_comp0s) 1;
fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_mapss map_wpulls pickWP_assms_tacs
{context = ctxt, prems = _} =
@@ -1287,7 +1287,7 @@
ALLGOALS (TRY o
FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
-fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets dtor_inject
+fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject
dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss =
let
val m = length dtor_set_incls;
@@ -1309,7 +1309,7 @@
rtac conjI, rtac refl, rtac refl])
(in_Jrels ~~ (active_set_maps ~~ dtor_set_set_inclss)),
CONJ_WRAP' (fn conv =>
- EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+ EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
@@ -1339,7 +1339,7 @@
(dtor_sets ~~ passive_set_maps),
rtac conjI,
REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
- rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
+ rtac box_equals, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
dtac @{thm ssubst_mem[OF pair_collapse]},
@@ -1352,22 +1352,22 @@
EVERY' [rtac iffI, if_tac, only_if_tac] 1
end;
-fun mk_rel_coinduct_coind_tac m coinduct ks map_comps map_congs map_arg_congs set_mapss
+fun mk_rel_coinduct_coind_tac m coinduct ks map_comp0s map_congs map_arg_congs set_mapss
dtor_unfolds dtor_maps {context = ctxt, prems = _} =
let val n = length ks;
in
EVERY' [DETERM o rtac coinduct,
- EVERY' (map7 (fn i => fn map_comp => fn map_cong => fn map_arg_cong => fn set_maps =>
+ EVERY' (map7 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_maps =>
fn dtor_unfold => fn dtor_map =>
EVERY' [REPEAT_DETERM o eresolve_tac [exE, conjE],
select_prem_tac (length ks) (dtac @{thm spec2}) i, dtac mp, atac,
REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
rtac exI, rtac conjI, rtac conjI,
- rtac (map_comp RS trans), rtac (dtor_map RS trans RS sym),
- rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp, map_cong]),
+ rtac (map_comp0 RS trans), rtac (dtor_map RS trans RS sym),
+ rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp0, map_cong]),
REPEAT_DETERM_N m o rtac @{thm trans[OF fun_cong[OF o_id] sym[OF fun_cong[OF id_o]]]},
REPEAT_DETERM_N n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}),
- rtac (map_comp RS trans), rtac (map_cong RS trans),
+ rtac (map_comp0 RS trans), rtac (map_cong RS trans),
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_o]},
REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}),
etac (@{thm prod.cases} RS map_arg_cong RS trans),
@@ -1380,7 +1380,7 @@
hyp_subst_tac ctxt, rtac exI, rtac conjI, etac Collect_splitD_set_mp, atac,
rtac (o_apply RS trans), rtac (@{thm surjective_pairing} RS arg_cong)])
(drop m set_maps)])
- ks map_comps map_congs map_arg_congs set_mapss dtor_unfolds dtor_maps)] 1
+ ks map_comp0s map_congs map_arg_congs set_mapss dtor_unfolds dtor_maps)] 1
end;
val split_id_unfolds = @{thms prod.cases image_id id_apply};
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 22:53:17 2013 +0200
@@ -159,11 +159,11 @@
map (fn thm => ctrans OF [thm, bd0_Card_order RS @{thm ordLeq_csum1}]) set_bd0s)
set_bd0ss bd0_Card_orders;
val in_bds = map in_bd_of_bnf bnfs;
- val sym_map_comps = map (fn bnf => map_comp_of_bnf bnf RS sym) bnfs;
- val map_comp's = map map_comp'_of_bnf bnfs;
+ val sym_map_comps = map (fn bnf => map_comp0_of_bnf bnf RS sym) bnfs;
+ val map_comps = map map_comp_of_bnf bnfs;
val map_cong0s = map map_cong0_of_bnf bnfs;
val map_id0s = map map_id0_of_bnf bnfs;
- val map_id's = map map_id'_of_bnf bnfs;
+ val map_ids = map map_id_of_bnf bnfs;
val map_wpulls = map map_wpull_of_bnf bnfs;
val set_map'ss = map set_map'_of_bnf bnfs;
@@ -194,7 +194,7 @@
(*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) =
map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
- fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp =
+ fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 =
let
val lhs = Term.list_comb (mapBsCs, all_gs) $
(Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
@@ -203,15 +203,15 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
- (K (mk_map_comp_id_tac map_comp))
+ (K (mk_map_comp_id_tac map_comp0))
|> Thm.close_derivation
end;
- val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comp's;
+ val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
(*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_cong0L x mapAsAs sets map_cong0 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))));
@@ -220,11 +220,11 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
- (K (mk_map_cong0L_tac m map_cong0 map_id'))
+ (K (mk_map_cong0L_tac m map_cong0 map_id))
|> Thm.close_derivation
end;
- val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_id's;
+ val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
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;
@@ -389,7 +389,7 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
- (K (mk_mor_incl_tac mor_def map_id's))
+ (K (mk_mor_incl_tac mor_def map_ids))
|> Thm.close_derivation
end;
@@ -1405,7 +1405,7 @@
ctor_Irel_thms, lthy) =
if m = 0 then
(timer, replicate n DEADID_bnf,
- map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_id's),
+ map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids),
replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, lthy)
else let
val fTs = map2 (curry op -->) passiveAs passiveBs;
@@ -1692,8 +1692,8 @@
val timer = time (timer "helpers for BNF properties");
val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_map_unique_thms;
- val map_comp_tacs =
- map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks;
+ val map_comp0_tacs =
+ map2 (K oo mk_map_comp0_tac map_comps ctor_map_thms) ctor_map_unique_thms ks;
val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
val set_nat_tacss = map (map (K o mk_set_map_tac)) (transpose set_map_thmss);
val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
@@ -1703,7 +1703,7 @@
val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
- val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
+ val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss
bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs;
val ctor_witss =
@@ -1773,14 +1773,14 @@
(mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF));
val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
in
- map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 =>
+ map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets
+ (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets
ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss))
|> Thm.close_derivation)
- ks goals in_rels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
+ ks goals in_rels map_comps map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
ctor_inject_thms ctor_dtor_thms set_map'ss ctor_set_incl_thmss
ctor_set_set_incl_thmsss
end;
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 22:53:17 2013 +0200
@@ -39,7 +39,7 @@
val mk_least_min_alg_tac: thm -> thm -> tactic
val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list ->
thm list list -> thm list list list -> thm list -> tactic
- val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic
+ val mk_map_comp0_tac: thm list -> thm list -> thm -> int -> tactic
val mk_map_id0_tac: thm list -> thm -> tactic
val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic
@@ -115,12 +115,12 @@
etac bspec THEN'
atac) 1;
-fun mk_mor_incl_tac mor_def map_id's =
+fun mk_mor_incl_tac mor_def map_ids =
(stac mor_def THEN'
rtac conjI THEN'
- CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_id's THEN'
+ CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_ids THEN'
CONJ_WRAP' (fn thm =>
- (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_id's) 1;
+ (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_ids) 1;
fun mk_mor_comp_tac mor_def set_map's map_comp_ids =
let
@@ -710,18 +710,18 @@
EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id},
rtac (thm RS sym RS arg_cong)]) map_id0s)) 1;
-fun mk_map_comp_tac map_comps ctor_maps unique iplus1 =
+fun mk_map_comp0_tac map_comp0s ctor_maps unique iplus1 =
let
val i = iplus1 - 1;
val unique' = Thm.permute_prems 0 i unique;
- val map_comps' = drop i map_comps @ take i map_comps;
+ val map_comp0s' = drop i map_comp0s @ take i map_comp0s;
val ctor_maps' = drop i ctor_maps @ take i ctor_maps;
fun mk_comp comp simp =
EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac o_apply,
rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp,
rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply];
in
- (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comps' ctor_maps')) 1
+ (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1
end;
fun mk_set_map_tac set_nat =
@@ -746,7 +746,7 @@
EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
REPEAT_DETERM_N n o etac UnE]))))] 1);
-fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets ctor_inject
+fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject
ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss =
let
val m = length ctor_set_incls;
@@ -773,7 +773,7 @@
rtac conjI, rtac refl, rtac refl])
(in_Irels ~~ (active_set_maps ~~ ctor_set_set_inclss)),
CONJ_WRAP' (fn conv =>
- EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+ EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map,
@@ -802,7 +802,7 @@
(ctor_sets ~~ passive_set_maps),
rtac conjI,
REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
- rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+ rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
dtac @{thm ssubst_mem[OF pair_collapse]},
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 29 22:53:17 2013 +0200
@@ -106,16 +106,16 @@
split_conv}) THEN
rtac refl 1;
-fun mk_map_comp_id_tac map_comp =
- (rtac trans THEN' rtac map_comp THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
+fun mk_map_comp_id_tac map_comp0 =
+ (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
EVERY' [rtac mp, rtac map_cong0,
CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
-fun mk_map_cong0L_tac passive map_cong0 map_id' =
+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;
+ rtac map_id 1;
end;
--- a/src/HOL/Tools/Lifting/lifting_info.ML Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Thu Aug 29 22:53:17 2013 +0200
@@ -179,7 +179,7 @@
val (_, qtyp) = quot_thm_rty_qty quot_thm
val qty_full_name = (fst o dest_Type) qtyp
val symtab = get_quotients' ctxt
- fun compare_data (_, data) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
+ fun compare_data (_, data:quotient) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
in
if Symtab.member compare_data symtab (qty_full_name, quot_thm)
then Data.map (map_quotients (Symtab.delete qty_full_name)) ctxt