--- a/src/HOL/BNF/BNF_Def.thy Thu Sep 12 11:05:19 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy Thu Sep 12 11:23:49 2013 +0200
@@ -110,10 +110,6 @@
lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
unfolding Grp_def o_def by auto
-lemma wpull_Grp:
-"wpull (Collect (split (Grp A f))) A (f ` A) f id fst snd"
-unfolding wpull_def Grp_def by auto
-
definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
lemma pick_middlep:
--- a/src/HOL/BNF/BNF_Util.thy Thu Sep 12 11:05:19 2013 +0200
+++ b/src/HOL/BNF/BNF_Util.thy Thu Sep 12 11:23:49 2013 +0200
@@ -47,16 +47,9 @@
lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
unfolding bij_def inj_on_def by auto blast
-lemma pair_mem_Collect_split:
-"(\<lambda>x y. (x, y) \<in> {(x, y). P x y}) = P"
-by simp
-
lemma Collect_pair_mem_eq: "{(x, y). (x, y) \<in> R} = R"
by simp
-lemma Collect_fst_snd_mem_eq: "{p. (fst p, snd p) \<in> A} = A"
-by simp
-
(* Operator: *)
definition "Gr A f = {(a, f a) | a. a \<in> A}"
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Thu Sep 12 11:05:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Thu Sep 12 11:23:49 2013 +0200
@@ -102,7 +102,7 @@
rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
@{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN
unfold_thms_tac ctxt (srel_def ::
- @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
+ @{thms pair_collapse Collect_mem_eq mem_Collect_eq prod.cases fst_conv snd_conv
split_conv}) THEN
rtac refl 1;