# HG changeset patch
# User traytel
# Date 1378977829 -7200
# Node ID 92bcac4f9ac9b054b9146f86b7173a643de9e71b
# Parent  4b5f42cfa24456e0c4f5c82d4ed4aa3601e81c54
simplified derivation of in_rel

diff -r 4b5f42cfa244 -r 92bcac4f9ac9 src/HOL/BNF/BNF_Def.thy
--- a/src/HOL/BNF/BNF_Def.thy	Thu Sep 12 11:23:49 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy	Thu Sep 12 11:23:49 2013 +0200
@@ -89,6 +89,9 @@
 lemma eq_OOI: "R = op = \<Longrightarrow> R = R OO R"
   by auto
 
+lemma OO_Grp_alt: "(Grp A f)^--1 OO Grp A g = (\<lambda>x y. \<exists>z. z \<in> A \<and> f z = x \<and> g z = y)"
+  unfolding Grp_def by auto
+
 lemma Grp_UNIV_id: "f = id \<Longrightarrow> (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f"
 unfolding Grp_def by auto
 
diff -r 4b5f42cfa244 -r 92bcac4f9ac9 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Thu Sep 12 11:23:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Thu Sep 12 11:23:49 2013 +0200
@@ -770,7 +770,7 @@
     val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
 
     val pre_names_lthy = lthy;
-    val (((((((((((((((((((((((((fs, gs), hs), x), y), (z, z')), zs), ys), As),
+    val ((((((((((((((((((((((((fs, gs), hs), x), y), zs), ys), As),
       As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
       transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
       |> mk_Frees "f" (map2 (curry op -->) As' Bs')
@@ -778,7 +778,6 @@
       ||>> mk_Frees "h" (map2 (curry op -->) As' Ts)
       ||>> yield_singleton (mk_Frees "x") CA'
       ||>> yield_singleton (mk_Frees "y") CB'
-      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "z") CRs'
       ||>> mk_Frees "z" As'
       ||>> mk_Frees "y" Bs'
       ||>> mk_Frees "A" (map HOLogic.mk_setT As')
@@ -1093,7 +1092,8 @@
 
         val map_wppull = Lazy.lazy mk_map_wppull;
 
-        val rel_OO_Grps = no_refl [#rel_OO_Grp axioms];
+        val rel_OO_Grp = #rel_OO_Grp axioms;
+        val rel_OO_Grps = no_refl [rel_OO_Grp];
 
         fun mk_rel_Grp () =
           let
@@ -1182,23 +1182,7 @@
 
         val rel_OO = Lazy.lazy mk_rel_OO;
 
-        fun mk_in_rel () =
-          let
-            val bnf_in = mk_in setRs (map (mk_bnf_t RTs) bnf_sets) CRs';
-            val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
-            val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
-            val map_fst_eq = HOLogic.mk_eq (map1 $ z, x);
-            val map_snd_eq = HOLogic.mk_eq (map2 $ z, y);
-            val lhs = Term.list_comb (rel, Rs) $ x $ y;
-            val rhs =
-              HOLogic.mk_exists (fst z', snd z', HOLogic.mk_conj (HOLogic.mk_mem (z, bnf_in),
-                HOLogic.mk_conj (map_fst_eq, map_snd_eq)));
-            val goal =
-              fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
-          in
-            Goal.prove_sorry lthy [] [] goal (mk_in_rel_tac (the_single rel_OO_Grps))
-            |> Thm.close_derivation
-          end;
+        fun mk_in_rel () = trans OF [rel_OO_Grp, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD};
 
         val in_rel = Lazy.lazy mk_in_rel;
 
diff -r 4b5f42cfa244 -r 92bcac4f9ac9 src/HOL/BNF/Tools/bnf_def_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Sep 12 11:23:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Sep 12 11:23:49 2013 +0200
@@ -21,7 +21,6 @@
   val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic
   val mk_rel_OO_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
     {prems: thm list, context: Proof.context} -> tactic
-  val mk_in_rel_tac: thm -> {prems: 'a, context: Proof.context} -> tactic
   val mk_rel_conversep_tac: thm -> thm -> tactic
   val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
     {prems: thm list, context: Proof.context} -> tactic
@@ -209,13 +208,6 @@
           rtac (map_comp0 RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
   end;
 
-fun mk_in_rel_tac rel_OO_Gr {context = ctxt, prems = _} =
-  EVERY' [rtac (rel_OO_Gr RS fun_cong RS fun_cong RS trans), rtac iffI,
-    REPEAT_DETERM o eresolve_tac [@{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
-    hyp_subst_tac ctxt, rtac exI, rtac conjI, atac, rtac conjI, rtac refl, rtac refl,
-    REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI},
-    etac @{thm GrpI}, atac, etac @{thm GrpI}, atac] 1;
-
 fun mk_rel_mono_strong_tac in_rel set_map0s {context = ctxt, prems = _} =
   if null set_map0s then atac 1
   else