--- 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"
--- 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],
--- 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));