--- a/src/HOL/BNF/Tools/bnf_fp.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML Sun Sep 23 14:52:53 2012 +0200
@@ -31,6 +31,7 @@
val ctor_foldN: string
val ctor_fold_uniqueN: string
val ctor_foldsN: string
+ val ctor_mapN: string
val ctor_recN: string
val ctor_recsN: string
val ctor_relN: string
@@ -41,6 +42,7 @@
val disc_corecsN: string
val dtorN: string
val dtor_coinductN: string
+ val dtor_mapN: string
val dtor_relN: string
val dtor_corecN: string
val dtor_corecsN: string
@@ -61,7 +63,6 @@
val injectN: string
val isNodeN: string
val lsbisN: string
- val map_simpsN: string
val map_uniqueN: string
val min_algN: string
val morN: string
@@ -180,7 +181,8 @@
val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
val ctor_dtor_unfoldsN = ctorN ^ "_" ^ dtor_unfoldN ^ "s"
-val map_simpsN = mapN ^ "_" ^ simpsN
+val ctor_mapN = ctorN ^ "_" ^ mapN
+val dtor_mapN = dtorN ^ "_" ^ mapN
val map_uniqueN = mapN ^ uniqueN
val min_algN = "min_alg"
val morN = "mor"
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200
@@ -2366,7 +2366,7 @@
val p2id_Fmaps = map (mk_Fmap HOLogic.id_const p2s prodTs) (mk_mapsXB prodTs I);
val pid_Fmaps = map (mk_Fmap HOLogic.id_const ps prodTs) (mk_mapsXC prodTs I);
- val (map_simp_thms, map_thms) =
+ val (dtor_map_thms, map_thms) =
let
fun mk_goal fs_map map dtor dtor' = fold_rev Logic.all fs
(mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_map),
@@ -2482,7 +2482,7 @@
map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
- (mk_col_natural_tac cts rec_0s rec_Sucs map_simp_thms set_natural'ss))
+ (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_natural'ss))
|> Thm.close_derivation)
goals ctss hset_rec_0ss' hset_rec_Sucss';
in
@@ -2550,7 +2550,7 @@
val thm = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] goal
- (K (mk_mcong_tac m (rtac coinduct) map_comp's map_simp_thms map_congs set_natural'ss
+ (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_congs set_natural'ss
set_hset_thmss set_hset_hset_thmsss)))
|> Thm.close_derivation
in
@@ -2572,7 +2572,7 @@
(map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s));
val map_eq_thms = map2 (fn simp => fn diff => box_equals OF [diff RS iffD2, simp, simp])
- map_simp_thms dtor_inject_thms;
+ dtor_map_thms dtor_inject_thms;
val map_wpull_thms = map (fn thm => thm OF
(replicate m asm_rl @ replicate n @{thm wpull_thePull})) map_wpulls;
val pickWP_assms_tacs =
@@ -2893,7 +2893,7 @@
val Jsrel_defs = map srel_def_of_bnf Jbnfs;
val Jrel_defs = map rel_def_of_bnf Jbnfs;
- val folded_map_simp_thms = map fold_maps map_simp_thms;
+ val folded_dtor_map_thms = map fold_maps dtor_map_thms;
val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
@@ -2905,13 +2905,13 @@
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 =>
- fn map_simp => fn set_simps => fn dtor_inject => fn dtor_ctor =>
+ fn dtor_map => fn set_simps => fn dtor_inject => fn dtor_ctor =>
fn set_naturals => fn set_incls => fn set_set_inclss =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps
+ (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map set_simps
dtor_inject dtor_ctor set_naturals set_incls set_set_inclss))
|> Thm.close_derivation)
- ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
+ ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_set_simp_thmss'
dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
end;
@@ -2939,9 +2939,9 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
val Jbnf_notes =
- [(dtor_relN, map single dtor_Jrel_thms),
+ [(dtor_mapN, map single folded_dtor_map_thms),
+ (dtor_relN, map single dtor_Jrel_thms),
(dtor_srelN, map single dtor_Jsrel_thms),
- (map_simpsN, map single folded_map_simp_thms),
(set_inclN, set_incl_thmss),
(set_set_inclN, map flat set_set_incl_thmsss)] @
map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200
@@ -1220,7 +1220,7 @@
replicate n (@{thm o_id} RS fun_cong))))
maps map_comps map_congs)] 1;
-fun mk_mcong_tac m coinduct_tac map_comp's map_simps map_congs set_naturalss set_hsetss
+fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_congs set_naturalss set_hsetss
set_hset_hsetsss =
let
val n = length map_comp's;
@@ -1228,13 +1228,13 @@
in
EVERY' ([rtac rev_mp,
coinduct_tac] @
- maps (fn (((((map_comp'_trans, map_simps_trans), map_cong), set_naturals), set_hsets),
+ maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong), 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 map_simps_trans, rtac map_cong,
+ rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm id_apply}),
REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
- rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong,
+ rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
EVERY' (maps (fn set_hset =>
[rtac o_apply_trans_sym, rtac (@{thm id_apply} RS trans), etac CollectE,
REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
@@ -1247,7 +1247,7 @@
CONJ_WRAP' (fn set_hset_hset =>
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) map_simps ~~
+ (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) @
[rtac impI,
CONJ_WRAP' (fn k =>
@@ -1260,23 +1260,23 @@
unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
ALLGOALS (etac sym);
-fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss
+fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_naturalss
{context = ctxt, prems = _} =
let
- val n = length map_simps;
+ val n = length dtor_maps;
in
EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
REPEAT_DETERM o rtac allI,
- CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY'
+ CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY'
[SELECT_GOAL (unfold_thms_tac ctxt
- (rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
+ (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
rtac @{thm Un_cong}, rtac refl,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
(fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
- (rec_Sucs ~~ (map_simps ~~ set_naturalss))] 1
+ (rec_Sucs ~~ (dtor_maps ~~ set_naturalss))] 1
end;
fun mk_set_natural_tac hset_def col_natural =
@@ -1494,7 +1494,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 map_simp set_simps dtor_inject dtor_ctor
+fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map set_simps dtor_inject dtor_ctor
set_naturals set_incls set_set_inclss =
let
val m = length set_incls;
@@ -1519,7 +1519,7 @@
EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
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 map_simp, rtac (dtor_inject RS iffD2), atac])
+ rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
@{thms fst_conv snd_conv}];
val only_if_tac =
EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
@@ -1540,7 +1540,7 @@
(rev (active_set_naturals ~~ in_Jsrels))])
(set_simps ~~ passive_set_naturals),
rtac conjI,
- REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac map_simp,
+ 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]},
EVERY' (map (fn in_Jsrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200
@@ -1394,7 +1394,7 @@
val p1s_maps = map (mk_map XTs p1s Ts ctors (mk_passive_maps passiveXs passiveAs)) ks;
val p2s_maps = map (mk_map XTs p2s Ts' ctor's (mk_passive_maps passiveXs passiveBs)) ks;
- val map_simp_thms =
+ val ctor_map_thms =
let
fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs
(mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor),
@@ -1520,7 +1520,7 @@
(map4 (mk_set_natural f) fs_maps Izs sets sets')))
fs setss_by_range setss_by_range';
- fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_natural'ss map_simp_thms;
+ fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_natural'ss ctor_map_thms;
val thms =
map5 (fn goal => fn csets => fn set_simps => fn induct => fn i =>
singleton (Proof_Context.export names_lthy lthy)
@@ -1581,7 +1581,7 @@
val thm = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] goal
- (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs map_simp_thms))
+ (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs ctor_map_thms))
|> Thm.close_derivation;
in
split_conj_thm thm
@@ -1650,7 +1650,7 @@
val thm = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] goal
- (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls map_simp_thms
+ (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls ctor_map_thms
(transpose set_simp_thmss) Fset_set_thmsss ctor_inject_thms)))
|> Thm.close_derivation;
in
@@ -1661,7 +1661,7 @@
val map_id_tacs = map (K o mk_map_id_tac map_ids) map_unique_thms;
val map_comp_tacs =
- map2 (K oo mk_map_comp_tac map_comp's map_simp_thms) map_unique_thms ks;
+ map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) map_unique_thms ks;
val map_cong_tacs = map (mk_map_cong_tac m) map_cong_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));
@@ -1736,7 +1736,7 @@
val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
val set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
- val folded_map_simp_thms = map fold_maps map_simp_thms;
+ val folded_ctor_map_thms = map fold_maps ctor_map_thms;
val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
@@ -1748,13 +1748,13 @@
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 =>
- fn map_simp => fn set_simps => fn ctor_inject => fn ctor_dtor =>
+ fn ctor_map => fn set_simps => fn ctor_inject => fn ctor_dtor =>
fn set_naturals => fn set_incls => fn set_set_inclss =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps
+ (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map set_simps
ctor_inject ctor_dtor set_naturals set_incls set_set_inclss))
|> Thm.close_derivation)
- ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
+ ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_set_simp_thmss'
ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
end;
@@ -1781,9 +1781,9 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
val Ibnf_notes =
- [(ctor_relN, map single ctor_Irel_thms),
+ [(ctor_mapN, map single folded_ctor_map_thms),
+ (ctor_relN, map single ctor_Irel_thms),
(ctor_srelN, map single ctor_Isrel_thms),
- (map_simpsN, map single folded_map_simp_thms),
(set_inclN, set_incl_thmss),
(set_set_inclN, map flat set_set_incl_thmsss)] @
map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200
@@ -607,23 +607,23 @@
end;
fun mk_set_nat_tac m induct_tac set_natural'ss
- map_simps csets set_simps i {context = ctxt, prems = _} =
+ ctor_maps csets set_simps i {context = ctxt, prems = _} =
let
- val n = length map_simps;
+ val n = length ctor_maps;
fun useIH set_nat = EVERY' [rtac trans, rtac @{thm image_UN}, rtac trans, rtac @{thm UN_cong},
rtac refl, Goal.assume_rule_tac ctxt, rtac sym, rtac trans, rtac @{thm UN_cong},
rtac set_nat, rtac refl, rtac @{thm UN_simps(10)}];
- fun mk_set_nat cset map_simp set_simp set_nats =
+ fun mk_set_nat cset ctor_map set_simp set_nats =
EVERY' [rtac trans, rtac @{thm image_cong}, rtac set_simp, rtac refl,
- rtac sym, rtac (trans OF [map_simp RS HOL_arg_cong cset, set_simp RS trans]),
+ rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, set_simp RS trans]),
rtac sym, EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
rtac sym, rtac (nth set_nats (i - 1)),
REPEAT_DETERM_N (n - 1) o EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
EVERY' (map useIH (drop m set_nats))];
in
- (induct_tac THEN' EVERY' (map4 mk_set_nat csets map_simps set_simps set_natural'ss)) 1
+ (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps set_simps set_natural'ss)) 1
end;
fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss set_simps i {context = ctxt, prems = _} =
@@ -642,7 +642,7 @@
(induct_tac THEN' EVERY' (map2 mk_set_nat set_simps set_bdss)) 1
end;
-fun mk_mcong_tac induct_tac set_setsss map_congs map_simps {context = ctxt, prems = _} =
+fun mk_mcong_tac induct_tac set_setsss map_congs ctor_maps {context = ctxt, prems = _} =
let
fun use_asm thm = EVERY' [etac bspec, etac set_rev_mp, rtac thm];
@@ -650,14 +650,14 @@
CONJ_WRAP' (fn thm =>
EVERY' [rtac ballI, etac bspec, etac set_rev_mp, etac thm]) set_sets];
- fun mk_map_cong map_simp map_cong set_setss =
+ fun mk_map_cong ctor_map map_cong set_setss =
EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
- rtac trans, rtac map_simp, rtac trans, rtac (map_cong RS arg_cong),
+ rtac trans, rtac ctor_map, rtac trans, rtac (map_cong RS arg_cong),
EVERY' (map use_asm (map hd set_setss)),
EVERY' (map useIH (transpose (map tl set_setss))),
- rtac sym, rtac map_simp];
+ rtac sym, rtac ctor_map];
in
- (induct_tac THEN' EVERY' (map3 mk_map_cong map_simps map_congs set_setsss)) 1
+ (induct_tac THEN' EVERY' (map3 mk_map_cong ctor_maps map_congs set_setsss)) 1
end;
fun mk_incl_min_alg_tac induct_tac set_setsss alg_sets alg_min_alg {context = ctxt, prems = _} =
@@ -676,7 +676,7 @@
(induct_tac THEN' EVERY' (map2 mk_incl alg_sets set_setsss)) 1
end;
-fun mk_lfp_map_wpull_tac m induct_tac wpulls map_simps set_simpss set_setsss ctor_injects =
+fun mk_lfp_map_wpull_tac m induct_tac wpulls ctor_maps set_simpss set_setsss ctor_injects =
let
val n = length wpulls;
val ks = 1 upto n;
@@ -701,7 +701,7 @@
EVERY' [rtac @{thm UN_least}, rtac CollectE, etac set_rev_mp, atac,
REPEAT_DETERM o etac conjE, atac]];
- fun mk_wpull wpull map_simp set_simps set_setss ctor_inject =
+ fun mk_wpull wpull ctor_map set_simps set_setss ctor_inject =
EVERY' [rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac rev_mp, rtac wpull,
EVERY' (map (fn i => REPEAT_DETERM_N (i - 1) o etac thin_rl THEN' atac) ls),
@@ -712,12 +712,12 @@
CONJ_WRAP' (K (rtac subset_refl)) ks,
rtac conjI, rtac CollectI, EVERY' (map (use_pass_asm o hd) set_setss),
CONJ_WRAP' (K (rtac subset_refl)) ks,
- rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac map_simp,
- rtac trans, atac, rtac map_simp, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE],
- hyp_subst_tac, rtac bexI, rtac conjI, rtac map_simp, rtac map_simp, rtac CollectI,
+ rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac ctor_map,
+ rtac trans, atac, rtac ctor_map, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE],
+ hyp_subst_tac, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI,
CONJ_WRAP' mk_subset set_simps];
in
- (induct_tac THEN' EVERY' (map5 mk_wpull wpulls map_simps set_simpss set_setsss ctor_injects)) 1
+ (induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps set_simpss set_setsss ctor_injects)) 1
end;
(* BNF tactics *)
@@ -728,18 +728,18 @@
EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id},
rtac (thm RS sym RS arg_cong)]) map_ids)) 1;
-fun mk_map_comp_tac map_comps map_simps unique iplus1 =
+fun mk_map_comp_tac map_comps 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_simps' = drop i map_simps @ take i map_simps;
+ 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' map_simps')) 1
+ (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comps' ctor_maps')) 1
end;
fun mk_set_natural_tac set_nat =
@@ -770,7 +770,7 @@
EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
REPEAT_DETERM_N n o etac UnE]))))] 1);
-fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject
+fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map set_simps ctor_inject
ctor_dtor set_naturals set_incls set_set_inclss =
let
val m = length set_incls;
@@ -800,7 +800,7 @@
EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
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 map_simp,
+ rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map,
etac eq_arg_cong_ctor_dtor])
fst_snd_convs];
val only_if_tac =
@@ -821,7 +821,7 @@
(rev (active_set_naturals ~~ in_Isrels))])
(set_simps ~~ passive_set_naturals),
rtac conjI,
- REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac map_simp, rtac (ctor_inject RS iffD2),
+ 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,
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,