# HG changeset patch # User blanchet # Date 1348101768 -7200 # Node ID e053519494d61c985bdfc37b2ffa6e7812114895 # Parent 7a28d22c33c68fd2fb929ec8817d4c419a429206 renamed "rel_def" to "rel_O_Gr" diff -r 7a28d22c33c6 -r e053519494d6 src/HOL/Codatatype/Tools/bnf_comp.ML --- 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 diff -r 7a28d22c33c6 -r e053519494d6 src/HOL/Codatatype/Tools/bnf_def.ML --- 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))] diff -r 7a28d22c33c6 -r e053519494d6 src/HOL/Codatatype/Tools/bnf_def_tactics.ML --- 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, diff -r 7a28d22c33c6 -r e053519494d6 src/HOL/Codatatype/Tools/bnf_gfp.ML --- 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; diff -r 7a28d22c33c6 -r e053519494d6 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML --- 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,