--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 22:56:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 23:01:04 2013 +0200
@@ -122,39 +122,39 @@
CONJ_WRAP' (fn thm =>
(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 =
+fun mk_mor_comp_tac mor_def set_maps map_comp_ids =
let
val fbetw_tac = EVERY' [rtac ballI, stac o_apply, etac bspec, etac bspec, atac];
- fun mor_tac (set_map', map_comp_id) =
+ fun mor_tac (set_map, map_comp_id) =
EVERY' [rtac ballI, stac o_apply, rtac trans,
rtac trans, dtac rev_bspec, atac, etac arg_cong,
REPEAT o eresolve_tac [CollectE, conjE], etac bspec, rtac CollectI] THEN'
CONJ_WRAP' (fn thm =>
FIRST' [rtac subset_UNIV,
(EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
- etac bspec, etac set_mp, atac])]) set_map' THEN'
+ etac bspec, etac set_mp, atac])]) set_map THEN'
rtac (map_comp_id RS arg_cong);
in
(dtac (mor_def RS subst) THEN' dtac (mor_def RS subst) THEN' stac mor_def THEN'
REPEAT o etac conjE THEN'
rtac conjI THEN'
- CONJ_WRAP' (K fbetw_tac) set_map's THEN'
- CONJ_WRAP' mor_tac (set_map's ~~ map_comp_ids)) 1
+ CONJ_WRAP' (K fbetw_tac) set_maps THEN'
+ CONJ_WRAP' mor_tac (set_maps ~~ map_comp_ids)) 1
end;
-fun mk_mor_inv_tac alg_def mor_def set_map's morEs map_comp_ids map_cong0Ls =
+fun mk_mor_inv_tac alg_def mor_def set_maps morEs map_comp_ids map_cong0Ls =
let
val fbetw_tac = EVERY' [rtac ballI, etac set_mp, etac imageI];
- fun Collect_tac set_map' =
+ fun Collect_tac set_map =
CONJ_WRAP' (fn thm =>
FIRST' [rtac subset_UNIV,
(EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
- etac @{thm image_mono}, atac])]) set_map';
- fun mor_tac (set_map', ((morE, map_comp_id), map_cong0L)) =
+ etac @{thm image_mono}, atac])]) set_map;
+ fun mor_tac (set_map, ((morE, map_comp_id), map_cong0L)) =
EVERY' [rtac ballI, ftac 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_map',
- rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map',
+ etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_map,
+ rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map,
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])];
@@ -164,8 +164,8 @@
dtac (alg_def RS iffD1) THEN'
REPEAT o etac conjE THEN'
rtac conjI THEN'
- CONJ_WRAP' (K fbetw_tac) set_map's THEN'
- CONJ_WRAP' mor_tac (set_map's ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1
+ CONJ_WRAP' (K fbetw_tac) set_maps THEN'
+ CONJ_WRAP' mor_tac (set_maps ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1
end;
fun mk_mor_str_tac ks mor_def =
@@ -211,7 +211,7 @@
(rtac iffI THEN' if_tac THEN' only_if_tac) 1
end;
-fun mk_copy_str_tac set_map's alg_def alg_sets =
+fun mk_copy_str_tac set_maps alg_def alg_sets =
let
val n = length alg_sets;
val bij_betw_inv_tac =
@@ -225,13 +225,13 @@
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp,
rtac equalityD1, etac @{thm bij_betw_imageE}, rtac imageI, etac thm,
REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)])
- (set_map's ~~ alg_sets);
+ (set_maps ~~ alg_sets);
in
(rtac rev_mp THEN' DETERM o bij_betw_inv_tac THEN' rtac impI THEN'
stac alg_def THEN' copy_str_tac) 1
end;
-fun mk_copy_alg_tac set_map's alg_sets mor_def iso_alt copy_str =
+fun mk_copy_alg_tac set_maps alg_sets mor_def iso_alt copy_str =
let
val n = length alg_sets;
val fbetw_tac = CONJ_WRAP' (K (etac @{thm bij_betwE})) alg_sets;
@@ -243,7 +243,7 @@
CONJ_WRAP' (fn (thms, thm) =>
EVERY' [rtac ballI, etac CollectE, etac @{thm inverE}, etac thm,
REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)])
- (set_map's ~~ alg_sets);
+ (set_maps ~~ alg_sets);
in
(rtac (iso_alt RS iffD2) THEN'
etac copy_str THEN' REPEAT_DETERM o atac THEN'
@@ -390,25 +390,25 @@
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
-fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select
- alg_sets set_map's str_init_defs =
+fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets
+ set_maps str_init_defs =
let
val n = length alg_sets;
val fbetw_tac =
CONJ_WRAP' (K (EVERY' [rtac ballI, etac rev_bspec, etac CollectE, atac])) alg_sets;
val mor_tac =
CONJ_WRAP' (fn thm => EVERY' [rtac ballI, rtac thm]) str_init_defs;
- fun alg_epi_tac ((alg_set, str_init_def), set_map') =
+ fun alg_epi_tac ((alg_set, str_init_def), set_map) =
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
rtac ballI, ftac (alg_select RS bspec), stac str_init_def, etac alg_set,
REPEAT_DETERM o FIRST' [rtac subset_UNIV,
- EVERY' [rtac ord_eq_le_trans, resolve_tac set_map', rtac subset_trans,
+ EVERY' [rtac ord_eq_le_trans, resolve_tac set_map, rtac subset_trans,
etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]]];
in
(rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm o_id}) THEN'
rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN'
stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' rtac mor_incl_min_alg THEN'
- stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_map's)) 1
+ stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)) 1
end;
fun mk_init_ex_mor_tac Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs
@@ -534,21 +534,21 @@
(rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN
etac fold_unique_mor 1;
-fun mk_ctor_induct_tac ctxt m set_map'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
+fun mk_ctor_induct_tac ctxt m set_mapss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
let
- val n = length set_map'ss;
+ val n = length set_mapss;
val ks = 1 upto n;
- fun mk_IH_tac Rep_inv Abs_inv set_map' =
+ fun mk_IH_tac Rep_inv Abs_inv set_map =
DETERM o EVERY' [dtac meta_mp, rtac (Rep_inv RS arg_cong RS subst), etac bspec,
- dtac set_rev_mp, rtac equalityD1, rtac set_map', etac imageE,
+ dtac set_rev_mp, rtac equalityD1, rtac set_map, etac imageE,
hyp_subst_tac ctxt, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac];
- fun mk_closed_tac (k, (morE, set_map's)) =
+ fun mk_closed_tac (k, (morE, set_maps)) =
EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI,
rtac (mor_Abs RS morE RS arg_cong RS ssubst), atac,
REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec},
- EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_map's)), atac];
+ EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac];
fun mk_induct_tac (Rep, Rep_inv) =
EVERY' [rtac (Rep_inv RS arg_cong RS subst), etac (Rep RSN (2, bspec))];
@@ -556,7 +556,7 @@
(rtac mp THEN' rtac impI THEN'
DETERM o CONJ_WRAP_GEN' (etac conjE THEN' rtac conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN'
rtac init_induct THEN'
- DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_map'ss))) 1
+ DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_mapss))) 1
end;
fun mk_ctor_induct2_tac cTs cts ctor_induct weak_ctor_inducts {context = ctxt, prems = _} =
@@ -592,19 +592,19 @@
fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;
-fun mk_ctor_set_tac set set_map' set_map's =
+fun mk_ctor_set_tac set set_map set_maps =
let
- val n = length set_map's;
+ val n = length set_maps;
fun mk_UN thm = rtac (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN'
rtac @{thm Union_image_eq};
in
EVERY' [rtac (set RS @{thm comp_eq_dest} RS trans), rtac Un_cong,
- rtac (trans OF [set_map', trans_fun_cong_image_id_id_apply]),
+ rtac (trans OF [set_map, trans_fun_cong_image_id_id_apply]),
REPEAT_DETERM_N (n - 1) o rtac Un_cong,
- EVERY' (map mk_UN set_map's)] 1
+ EVERY' (map mk_UN set_maps)] 1
end;
-fun mk_set_nat_tac m induct_tac set_map'ss
+fun mk_set_nat_tac m induct_tac set_mapss
ctor_maps csets ctor_sets i {context = ctxt, prems = _} =
let
val n = length ctor_maps;
@@ -621,7 +621,7 @@
REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
EVERY' (map useIH (drop m set_nats))];
in
- (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_map'ss)) 1
+ (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1
end;
fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i {context = ctxt, prems = _} =