--- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 20:15:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 22:39:46 2013 +0200
@@ -56,7 +56,7 @@
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
@@ -190,7 +190,7 @@
in_rel: 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,
@@ -217,7 +217,7 @@
in_rel = in_rel,
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,
@@ -241,7 +241,7 @@
in_rel,
map_comp',
map_cong,
- map_id',
+ map_id,
map_transfer,
map_wppull,
rel_eq,
@@ -263,7 +263,7 @@
in_rel = Lazy.map f in_rel,
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,7 +381,7 @@
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_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_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
@@ -509,7 +509,7 @@
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_compN = "map_comp";
val map_comp'N = "map_comp'";
val map_cong0N = "map_cong0";
@@ -580,7 +580,7 @@
[(map_comp'N, [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), []),
@@ -1000,7 +1000,7 @@
val in_cong = Lazy.lazy mk_in_cong;
- val map_id' = Lazy.lazy (fn () => mk_map_id' (#map_id0 axioms));
+ val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms));
val map_comp' = Lazy.lazy (fn () => mk_map_comp' (#map_comp axioms));
fun mk_map_cong () =
@@ -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
@@ -1102,7 +1102,7 @@
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')
+ (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;
@@ -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 20:15:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -9,7 +9,7 @@
signature BNF_DEF_TACTICS =
sig
val mk_collect_set_map_tac: thm list -> tactic
- val mk_map_id': 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
@@ -45,7 +45,7 @@
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_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'
@@ -82,7 +82,7 @@
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_comp set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
@@ -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 =
@@ -246,7 +246,7 @@
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 20:15:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 22:39:46 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 20:15:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Aug 29 22:39:46 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 20:15:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 22:39:46 2013 +0200
@@ -219,7 +219,7 @@
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;
@@ -254,7 +254,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_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;
@@ -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;
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 20:15:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -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
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 20:15:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 22:39:46 2013 +0200
@@ -163,7 +163,7 @@
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_map'ss = map set_map'_of_bnf bnfs;
@@ -211,7 +211,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_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;
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 20:15:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -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
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 29 20:15:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -113,9 +113,9 @@
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;