# HG changeset patch
# User blanchet
# Date 1348239743 -7200
# Node ID 82d99fe04018b369e46e5b0610aa5bb655455f32
# Parent  9f5bfef8bd8265cd3fa2024220e0349c97f636d4
clean up lemmas used for composition

diff -r 9f5bfef8bd82 -r 82d99fe04018 src/HOL/BNF/BNF_Comp.thy
--- a/src/HOL/BNF/BNF_Comp.thy	Fri Sep 21 16:53:38 2012 +0200
+++ b/src/HOL/BNF/BNF_Comp.thy	Fri Sep 21 17:02:23 2012 +0200
@@ -70,19 +70,7 @@
 lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R"
 unfolding Gr_def by auto
 
-lemma subst_rel_def: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
-by simp
-
-lemma abs_pred_def: "\<lbrakk>\<And>x y. (x, y) \<in> rel = pred x y\<rbrakk> \<Longrightarrow> rel = Collect (split pred)"
-by auto
-
-lemma Collect_split_cong: "Collect (split pred) = Collect (split pred') \<Longrightarrow> pred = pred'"
-by blast
-
-lemma pred_def_abs: "rel = Collect (split pred) \<Longrightarrow> pred = (\<lambda>x y. (x, y) \<in> rel)"
-by auto
-
-lemma mem_Id_eq_eq: "(\<lambda>x y. (x, y) \<in> Id) = (op =)"
+lemma O_Gr_cong: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
 by simp
 
 ML_file "Tools/bnf_comp_tactics.ML"
diff -r 9f5bfef8bd82 -r 82d99fe04018 src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri Sep 21 16:53:38 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri Sep 21 17:02:23 2012 +0200
@@ -236,7 +236,7 @@
         val outer_srel_Gr = srel_Gr_of_bnf outer RS sym;
         val outer_srel_cong = srel_cong_of_bnf outer;
         val thm =
-          (trans OF [in_alt_thm RS @{thm subst_rel_def},
+          (trans OF [in_alt_thm RS @{thm O_Gr_cong},
              trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
                [trans OF [outer_srel_Gr RS @{thm arg_cong[of _ _ converse]},
                  srel_converse_of_bnf outer RS sym], outer_srel_Gr],
@@ -345,7 +345,7 @@
       let
         val srel_Gr = srel_Gr_of_bnf bnf RS sym
         val thm =
-          (trans OF [in_alt_thm RS @{thm subst_rel_def},
+          (trans OF [in_alt_thm RS @{thm O_Gr_cong},
             trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
               [trans OF [srel_Gr RS @{thm arg_cong[of _ _ converse]},
                 srel_converse_of_bnf bnf RS sym], srel_Gr],
diff -r 9f5bfef8bd82 -r 82d99fe04018 src/HOL/BNF/Tools/bnf_comp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Fri Sep 21 16:53:38 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Fri Sep 21 17:02:23 2012 +0200
@@ -409,7 +409,7 @@
 
 fun mk_simple_srel_O_Gr_tac ctxt srel_def srel_O_Gr in_alt_thm =
   rtac (unfold_thms ctxt [srel_def]
-    (trans OF [srel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym])) 1;
+    (trans OF [srel_O_Gr, in_alt_thm RS @{thm O_Gr_cong} RS sym])) 1;
 
 fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));