--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 08 12:01:02 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 08 14:48:19 2013 +0200
@@ -2254,7 +2254,7 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (mk_dtor_map_unique_tac dtor_unfold_unique_thm map_comps)
+ (mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps)
|> Thm.close_derivation
end;
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 08 12:01:02 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 08 14:48:19 2013 +0200
@@ -1114,9 +1114,9 @@
rtac conjI, rtac refl, rtac refl]) ks]) 1
end
-fun mk_dtor_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
+fun mk_dtor_map_unique_tac unfold_unique sym_map_comps {context = ctxt, prems = _} =
rtac unfold_unique 1 THEN
- unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
+ unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN
ALLGOALS (etac sym);
fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_mapss
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 08 12:01:02 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 08 14:48:19 2013 +0200
@@ -1133,8 +1133,8 @@
`split_conj_thm unique_mor
end;
- val ctor_fold_unique_thms =
- split_conj_thm (mk_conjIN n RS
+ val (ctor_fold_unique_thms, ctor_fold_unique_thm) =
+ `split_conj_thm (mk_conjIN n RS
(mor_UNIV_thm RS iffD2 RS fold_unique_mor_thm))
val fold_ctor_thms =
@@ -1472,7 +1472,7 @@
(map2 (curry HOLogic.mk_eq) us fs_maps));
val unique = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_cong0s))
+ (mk_ctor_map_unique_tac ctor_fold_unique_thm sym_map_comps)
|> Thm.close_derivation;
in
`split_conj_thm unique
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 08 12:01:02 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 08 14:48:19 2013 +0200
@@ -42,7 +42,7 @@
val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic
val mk_map_id_tac: thm list -> thm -> tactic
val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
- val mk_ctor_map_unique_tac: int -> thm -> thm -> thm list -> thm list -> tactic
+ val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic
val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
@@ -584,19 +584,10 @@
REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
rtac sym, rtac o_apply] 1;
-fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_cong0s =
- let
- val n = length map_cong0s;
- fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm comp_eq_dest},
- rtac sym, rtac trans, rtac o_apply, rtac trans, rtac (comp_id RS arg_cong),
- rtac (cong RS arg_cong),
- REPEAT_DETERM_N m o rtac refl,
- REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply]))];
- in
- EVERY' [rtac fold_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
- CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_cong0s,
- CONJ_WRAP' mk_mor (map_comp_ids ~~ map_cong0s)] 1
- end;
+fun mk_ctor_map_unique_tac fold_unique sym_map_comps {context = ctxt, prems = _} =
+ rtac fold_unique 1 THEN
+ unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc[symmetric] id_o o_id}) THEN
+ ALLGOALS atac;
fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;