--- a/src/HOL/BNF/More_BNFs.thy Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Thu Aug 29 22:39:46 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:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 22:39:46 2013 +0200
@@ -302,7 +302,7 @@
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
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
+ 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);
@@ -392,7 +392,7 @@
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
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
+ 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);
--- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 22:39:46 2013 +0200
@@ -50,8 +50,8 @@
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
@@ -188,7 +188,7 @@
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_transfer: 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,7 +215,7 @@
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_transfer = map_transfer,
@@ -239,7 +239,7 @@
in_cong,
in_mono,
in_rel,
- map_comp',
+ map_comp,
map_cong,
map_id,
map_transfer,
@@ -261,7 +261,7 @@
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_transfer = Lazy.map f map_transfer,
@@ -383,7 +383,7 @@
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_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_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;
@@ -511,7 +511,7 @@
val map_id0N = "map_id0";
val map_idN = "map_id";
val map_comp0N = "map_comp0";
-val map_comp'N = "map_comp'";
+val map_compN = "map_comp";
val map_cong0N = "map_cong0";
val map_congN = "map_cong";
val map_transferN = "map_transfer";
@@ -577,7 +577,7 @@
#> (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_idN, [Lazy.force (#map_id facts)], []),
@@ -1001,7 +1001,7 @@
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_comp0 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;
@@ -1103,7 +1103,7 @@
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'))
+ (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:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -10,7 +10,7 @@
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_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
@@ -46,7 +46,7 @@
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_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;
@@ -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_gfp.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 22:39:46 2013 +0200
@@ -216,7 +216,7 @@
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_comp's = map map_comp'_of_bnf 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_ids = map map_id_of_bnf bnfs;
@@ -250,7 +250,7 @@
|> 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*)
@@ -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;
@@ -2184,11 +2184,11 @@
val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's;
val cTs = map (SOME o certifyT lthy) FTs';
val maps =
- map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_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;
@@ -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 =
@@ -2706,7 +2706,7 @@
(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:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -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;
@@ -1049,21 +1049,21 @@
replicate n (@{thm o_id} RS fun_cong))))
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 =>
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 22:39:46 2013 +0200
@@ -160,7 +160,7 @@
set_bd0ss bd0_Card_orders;
val in_bds = map in_bd_of_bnf bnfs;
val sym_map_comps = map (fn bnf => map_comp0_of_bnf bnf RS sym) bnfs;
- val map_comp's = map map_comp'_of_bnf 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_ids = map map_id_of_bnf bnfs;
@@ -207,7 +207,7 @@
|> 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*)
@@ -1693,7 +1693,7 @@
val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_map_unique_thms;
val map_comp0_tacs =
- map2 (K oo mk_map_comp0_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks;
+ 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));
@@ -1780,7 +1780,7 @@
(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:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -714,14 +714,14 @@
let
val i = iplus1 - 1;
val unique' = Thm.permute_prems 0 i unique;
- val map_comps' = drop i map_comp0s @ take i map_comp0s;
+ 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 =