--- a/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 20 02:42:48 2012 +0200
@@ -263,13 +263,13 @@
val outer_rel_cong = rel_cong_of_bnf outer;
val rel_unfold_thm =
- trans OF [rel_def_of_bnf bnf',
+ trans OF [rel_O_Gr_of_bnf bnf',
trans OF [in_alt_thm RS @{thm subst_rel_def},
trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
[trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
rel_converse_of_bnf outer RS sym], outer_rel_Gr],
trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
- (map (fn bnf => rel_def_of_bnf bnf RS sym) inners)]]]];
+ (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]]];
val pred_unfold_thm = Collect_split_box_equals OF [rel_unfold_thm,
pred_def_of_bnf bnf' RS abs_pred_sym,
@@ -362,7 +362,7 @@
val rel_Gr = rel_Gr_of_bnf bnf RS sym;
val rel_unfold_thm =
- trans OF [rel_def_of_bnf bnf',
+ trans OF [rel_O_Gr_of_bnf bnf',
trans OF [in_alt_thm RS @{thm subst_rel_def},
trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
[trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]}, rel_converse_of_bnf bnf RS sym],
@@ -458,8 +458,8 @@
((((b, mapx), sets), Term.absdummy T bd), wits) lthy;
val rel_unfold_thm =
- trans OF [rel_def_of_bnf bnf',
- trans OF [in_alt_thm RS @{thm subst_rel_def}, rel_def_of_bnf bnf RS sym]];
+ trans OF [rel_O_Gr_of_bnf bnf',
+ trans OF [in_alt_thm RS @{thm subst_rel_def}, rel_O_Gr_of_bnf bnf RS sym]];
val pred_unfold_thm = Collect_split_box_equals OF [rel_unfold_thm,
pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
@@ -538,8 +538,8 @@
((((b, mapx), sets), Term.absdummy T bd), wits) lthy;
val rel_unfold_thm =
- trans OF [rel_def_of_bnf bnf',
- trans OF [in_alt_thm RS @{thm subst_rel_def}, rel_def_of_bnf bnf RS sym]];
+ trans OF [rel_O_Gr_of_bnf bnf',
+ trans OF [in_alt_thm RS @{thm subst_rel_def}, rel_O_Gr_of_bnf bnf RS sym]];
val pred_unfold_thm = Collect_split_box_equals OF [rel_unfold_thm,
pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
@@ -685,11 +685,11 @@
val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');
val unfold_defs' = unfold_defs o Local_Defs.unfold lthy' defs';
- val rel_def = unfold_defs' (rel_def_of_bnf bnf');
+ val rel_O_Gr = unfold_defs' (rel_O_Gr_of_bnf bnf');
val rel_unfold = Local_Defs.unfold lthy'
- (map unfold_defs (filter_refl (rel_unfolds_of unfold))) rel_def;
+ (map unfold_defs (filter_refl (rel_unfolds_of unfold))) rel_O_Gr;
- val unfold_defs'' = unfold_defs' o Local_Defs.unfold lthy' (filter_refl [rel_def_of_bnf bnf']);
+ val unfold_defs'' = unfold_defs' o Local_Defs.unfold lthy' (filter_refl [rel_O_Gr_of_bnf bnf']);
val pred_def = unfold_defs'' (pred_def_of_bnf bnf' RS abs_pred_sym_pred_abs);
val pred_unfold = Local_Defs.unfold lthy'
@@ -707,13 +707,13 @@
val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
-val ID_rel_def = rel_def_of_bnf ID_bnf;
-val ID_rel_def' = ID_rel_def RS sym;
-val ID_pred_def' = Local_Defs.unfold @{context} [ID_rel_def] (pred_def_of_bnf ID_bnf) RS sym;
+val ID_rel_O_Gr = rel_O_Gr_of_bnf ID_bnf;
+val ID_rel_O_Gr' = ID_rel_O_Gr RS sym;
+val ID_pred_def' = Local_Defs.unfold @{context} [ID_rel_O_Gr] (pred_def_of_bnf ID_bnf) RS sym;
fun bnf_of_typ _ _ _ (T as TFree _) (unfold, lthy) =
((ID_bnf, ([], [T])),
- (add_to_unfold_opt NONE NONE (SOME ID_rel_def') (SOME ID_pred_def') unfold, lthy))
+ (add_to_unfold_opt NONE NONE (SOME ID_rel_O_Gr') (SOME ID_pred_def') unfold, lthy))
| bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
| bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
let
@@ -732,9 +732,9 @@
val deads_lives =
pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
(deads, lives);
- val rel_def = rel_def_of_bnf bnf;
- val unfold' = add_to_unfold_opt NONE NONE (SOME (rel_def RS sym))
- (SOME (Local_Defs.unfold lthy [rel_def] (pred_def_of_bnf bnf) RS sym)) unfold;
+ val rel_O_Gr = rel_O_Gr_of_bnf bnf;
+ val unfold' = add_to_unfold_opt NONE NONE (SOME (rel_O_Gr RS sym))
+ (SOME (Local_Defs.unfold lthy [rel_O_Gr] (pred_def_of_bnf bnf) RS sym)) unfold;
in ((bnf, deads_lives), (unfold', lthy)) end
else
let
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:48 2012 +0200
@@ -59,12 +59,13 @@
val map_wppull_of_bnf: BNF -> thm
val map_wpull_of_bnf: BNF -> thm
val pred_def_of_bnf: BNF -> thm
+ val rel_def_of_bnf: BNF -> thm
val rel_Gr_of_bnf: BNF -> thm
val rel_Id_of_bnf: BNF -> thm
val rel_O_of_bnf: BNF -> thm
+ val rel_O_Gr_of_bnf: BNF -> thm
val rel_cong_of_bnf: BNF -> thm
val rel_converse_of_bnf: BNF -> thm
- val rel_def_of_bnf: BNF -> thm
val rel_mono_of_bnf: BNF -> thm
val set_bd_of_bnf: BNF -> thm list
val set_defs_of_bnf: BNF -> thm list
@@ -186,12 +187,13 @@
rel_Gr: thm lazy,
rel_converse: thm lazy,
rel_O: thm lazy,
+ rel_O_Gr: thm,
set_natural': thm lazy list
};
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero
collect_set_natural in_cong in_mono in_rel map_comp' map_id' map_wppull
- rel_cong rel_mono rel_Id rel_Gr rel_converse rel_O set_natural' = {
+ rel_cong rel_mono rel_Id rel_Gr rel_converse rel_O rel_O_Gr set_natural' = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
bd_Cnotzero = bd_Cnotzero,
@@ -208,6 +210,7 @@
rel_Gr = rel_Gr,
rel_converse = rel_converse,
rel_O = rel_O,
+ rel_O_Gr = rel_O_Gr,
set_natural' = set_natural'};
fun map_facts f {
@@ -227,6 +230,7 @@
rel_Gr,
rel_converse,
rel_O,
+ rel_O_Gr,
set_natural'} =
{bd_Card_order = f bd_Card_order,
bd_Cinfinite = f bd_Cinfinite,
@@ -244,6 +248,7 @@
rel_Gr = Lazy.map f rel_Gr,
rel_converse = Lazy.map f rel_converse,
rel_O = Lazy.map f rel_O,
+ rel_O_Gr = f rel_O_Gr,
set_natural' = map (Lazy.map f) set_natural'};
val morph_facts = map_facts o Morphism.thm;
@@ -364,6 +369,7 @@
val rel_Gr_of_bnf = Lazy.force o #rel_Gr o #facts o rep_bnf;
val rel_converse_of_bnf = Lazy.force o #rel_converse o #facts o rep_bnf;
val rel_O_of_bnf = Lazy.force o #rel_O o #facts o rep_bnf;
+val rel_O_Gr_of_bnf = #rel_O_Gr o #facts o rep_bnf;
val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
val set_natural_of_bnf = #set_natural o #axioms o rep_bnf;
@@ -494,6 +500,7 @@
val rel_converseN = "rel_converse";
val rel_monoN = "rel_mono"
val rel_ON = "rel_comp";
+val rel_O_GrN = "rel_comp_Gr";
val set_naturalN = "set_natural";
val set_natural'N = "set_natural'";
val set_bdN = "set_bd";
@@ -920,9 +927,11 @@
val relAsBs = mk_bnf_rel setRTs CA' CB';
val bnf_rel_def = Morphism.thm phi raw_rel_def;
- val rel_def_unabs =
+
+ val rel_O_Gr = Morphism.thm phi raw_rel_def; (*###*)
+ val rel_O_Gr_unabs =
if fact_policy <> Derive_Some_Facts then
- mk_unabs_def live (bnf_rel_def RS meta_eq_to_obj_eq)
+ mk_unabs_def live (rel_O_Gr RS meta_eq_to_obj_eq)
else
no_fact;
@@ -944,10 +953,10 @@
fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy QTs CA' CB' bnf_pred;
val pred = mk_bnf_pred QTs CA' CB';
- val bnf_pred_def = Morphism.thm phi raw_pred_def;
- val pred_def_unabs =
+ val bnf_pred_def0 = Morphism.thm phi raw_pred_def;
+ val bnf_pred_def =
if fact_policy <> Derive_Some_Facts then
- mk_unabs_def (live + 2) (bnf_pred_def RS meta_eq_to_obj_eq)
+ mk_unabs_def (live + 2) (bnf_pred_def0 RS meta_eq_to_obj_eq)
else
no_fact;
@@ -996,7 +1005,7 @@
val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
in
Skip_Proof.prove lthy [] [] goal
- (mk_rel_Gr_tac bnf_rel_def (#map_id axioms) (#map_cong axioms)
+ (mk_rel_Gr_tac rel_O_Gr (#map_id axioms) (#map_cong axioms)
(#map_wpull axioms) (Lazy.force in_cong) (Lazy.force map_id')
(Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
@@ -1015,7 +1024,7 @@
in
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
- (mk_rel_mono_tac bnf_rel_def (Lazy.force in_mono))
+ (mk_rel_mono_tac rel_O_Gr (Lazy.force in_mono))
|> Thm.close_derivation
end;
@@ -1051,7 +1060,7 @@
val rhs = mk_converse (Term.list_comb (relAsBs, Rs));
val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_subset lhs rhs));
val le_thm = Skip_Proof.prove lthy [] [] le_goal
- (mk_rel_converse_le_tac bnf_rel_def (Lazy.force rel_Id) (#map_cong axioms)
+ (mk_rel_converse_le_tac rel_O_Gr (Lazy.force rel_Id) (#map_cong axioms)
(Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
@@ -1071,7 +1080,7 @@
val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
in
Skip_Proof.prove lthy [] [] goal
- (mk_rel_O_tac bnf_rel_def (Lazy.force rel_Id) (#map_cong axioms)
+ (mk_rel_O_tac rel_O_Gr (Lazy.force rel_Id) (#map_cong axioms)
(Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
end;
@@ -1092,17 +1101,17 @@
val goal =
fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
in
- Skip_Proof.prove lthy [] [] goal (mk_in_rel_tac bnf_rel_def (length bnf_sets))
+ Skip_Proof.prove lthy [] [] goal (mk_in_rel_tac rel_O_Gr (length bnf_sets))
|> Thm.close_derivation
end;
val in_rel = mk_lazy mk_in_rel;
- val defs = mk_defs bnf_map_def bnf_set_defs rel_def_unabs pred_def_unabs;
+ val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_pred_def;
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural
in_cong in_mono in_rel map_comp' map_id' map_wppull
- rel_cong rel_mono rel_Id rel_Gr rel_converse rel_O set_natural';
+ rel_cong rel_mono rel_Id rel_Gr rel_converse rel_O rel_O_Gr_unabs set_natural';
val wits = map2 mk_witness bnf_wits wit_thms;
@@ -1152,6 +1161,7 @@
(rel_converseN, [Lazy.force (#rel_converse facts)]),
(rel_monoN, [Lazy.force (#rel_mono facts)]),
(rel_ON, [Lazy.force (#rel_O facts)]),
+ (rel_O_GrN, [#rel_O_Gr facts]),
(map_id'N, [Lazy.force (#map_id' facts)]),
(map_comp'N, [Lazy.force (#map_comp' facts)]),
(set_natural'N, map Lazy.force (#set_natural' facts))]
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Thu Sep 20 02:42:48 2012 +0200
@@ -65,14 +65,14 @@
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_Gr_tac rel_def map_id map_cong map_wpull in_cong map_id' map_comp set_naturals
+fun mk_rel_Gr_tac rel_O_Gr map_id map_cong map_wpull in_cong map_id' map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
in
if null set_naturals then
- Local_Defs.unfold_tac ctxt [rel_def] THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
- else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
+ Local_Defs.unfold_tac ctxt [rel_O_Gr] THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
+ else Local_Defs.unfold_tac ctxt [rel_O_Gr, @{thm Gr_def}] THEN
EVERY' [rtac equalityI, rtac subsetI,
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
@@ -112,20 +112,20 @@
rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI,
CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1);
-fun mk_rel_mono_tac rel_def in_mono {context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt [rel_def] THEN
+fun mk_rel_mono_tac rel_O_Gr in_mono {context = ctxt, prems = _} =
+ Local_Defs.unfold_tac ctxt [rel_O_Gr] THEN
EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
-fun mk_rel_converse_le_tac rel_def rel_Id map_cong map_comp set_naturals
+fun mk_rel_converse_le_tac rel_O_Gr rel_Id map_cong map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
in
if null set_naturals then
Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
- else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
+ else Local_Defs.unfold_tac ctxt [rel_O_Gr, @{thm Gr_def}] THEN
EVERY' [rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
@@ -143,7 +143,7 @@
EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
-fun mk_rel_O_tac rel_def rel_Id map_cong map_wppull map_comp set_naturals
+fun mk_rel_O_tac rel_O_Gr rel_Id map_cong map_wppull map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
@@ -152,7 +152,7 @@
rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
in
if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
- else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
+ else Local_Defs.unfold_tac ctxt [rel_O_Gr, @{thm Gr_def}] THEN
EVERY' [rtac equalityI, rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
@@ -193,11 +193,11 @@
rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
end;
-fun mk_in_rel_tac rel_def m {context = ctxt, prems = _} =
+fun mk_in_rel_tac rel_O_Gr m {context = ctxt, prems = _} =
let
val ls' = replicate (Int.max (1, m)) ();
in
- Local_Defs.unfold_tac ctxt (rel_def ::
+ Local_Defs.unfold_tac ctxt (rel_O_Gr ::
@{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 02:42:48 2012 +0200
@@ -223,11 +223,11 @@
val pred_defs = map pred_def_of_bnf bnfs;
val rel_congs = map rel_cong_of_bnf bnfs;
val rel_converses = map rel_converse_of_bnf bnfs;
- val rel_defs = map rel_def_of_bnf bnfs;
val rel_Grs = map rel_Gr_of_bnf bnfs;
val rel_Ids = map rel_Id_of_bnf bnfs;
val rel_monos = map rel_mono_of_bnf bnfs;
val rel_Os = map rel_O_of_bnf bnfs;
+ val rel_O_Grs = map rel_O_Gr_of_bnf bnfs;
val map_wpulls = map map_wpull_of_bnf bnfs;
val set_bdss = map set_bd_of_bnf bnfs;
val set_natural'ss = map set_natural'_of_bnf bnfs;
@@ -861,7 +861,7 @@
Skip_Proof.prove 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 m bis_def rel_defs map_comp's map_congs set_natural'ss))
+ (K (mk_bis_rel_tac m bis_def rel_O_Grs map_comp's map_congs set_natural'ss))
|> Thm.close_derivation
end;
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Thu Sep 20 02:42:48 2012 +0200
@@ -261,15 +261,15 @@
EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
atac, atac, rtac (hset_def RS sym)] 1
-fun mk_bis_rel_tac m bis_def rel_defs map_comps map_congs set_naturalss =
+fun mk_bis_rel_tac m bis_def rel_O_Grs map_comps map_congs set_naturalss =
let
- val n = length rel_defs;
- val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ rel_defs);
+ val n = length rel_O_Grs;
+ val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ rel_O_Grs);
- fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), rel_def) =
+ fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), rel_O_Gr) =
EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
- rtac (rel_def RS equalityD2 RS set_mp),
+ rtac (rel_O_Gr RS equalityD2 RS set_mp),
rtac @{thm relcompI}, rtac @{thm converseI},
EVERY' (map (fn thm =>
EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
@@ -285,10 +285,10 @@
REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
@{thms fst_diag_id snd_diag_id})];
- fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), rel_def) =
+ fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), rel_O_Gr) =
EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
etac allE, etac allE, etac impE, atac,
- dtac (rel_def RS equalityD1 RS set_mp),
+ dtac (rel_O_Gr RS equalityD1 RS set_mp),
REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
REPEAT_DETERM o dtac Pair_eq_subst_id,