--- a/src/HOL/BNF_Def.thy Wed Jan 29 15:05:53 2014 +0100
+++ b/src/HOL/BNF_Def.thy Wed Jan 29 16:35:05 2014 +0100
@@ -110,10 +110,11 @@
by auto
lemma Collect_split_mono_strong:
- "\<lbrakk>\<forall>a\<in>fst ` A. \<forall>b \<in> snd ` A. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (split P)\<rbrakk> \<Longrightarrow>
+ "\<lbrakk>X = fst ` A; Y = snd ` A; \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (split P)\<rbrakk> \<Longrightarrow>
A \<subseteq> Collect (split Q)"
by fastforce
+
lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
by metis
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Jan 29 15:05:53 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Jan 29 16:35:05 2014 +0100
@@ -189,9 +189,10 @@
unfold_tac ctxt [in_rel] THEN
REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN
hyp_subst_tac ctxt 1 THEN
- unfold_tac ctxt set_maps THEN
EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
- CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
+ CONJ_WRAP' (fn thm =>
+ (etac (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' atac))
+ set_maps] 1;
fun mk_map_transfer_tac rel_mono in_rel set_maps map_cong0 map_comp
{context = ctxt, prems = _} =