src/HOL/BNF_Def.thy

 keywords
   "print_bnfs" :: diag and
   "bnf" :: thy_goal
 begin
 
-lemma Collect_splitD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
+lemma Collect_case_prodD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
   by auto
 
 inductive
    rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool" for R1 R2
 where

   using assms unfolding rel_set_def by simp
 
 lemma predicate2_transferD:
    "\<lbrakk>rel_fun R1 (rel_fun R2 (op =)) P Q; a \<in> A; b \<in> B; A \<subseteq> {(x, y). R1 x y}; B \<subseteq> {(x, y). R2 x y}\<rbrakk> \<Longrightarrow>
    P (fst a) (fst b) \<longleftrightarrow> Q (snd a) (snd b)"
-  unfolding rel_fun_def by (blast dest!: Collect_splitD)
+  unfolding rel_fun_def by (blast dest!: Collect_case_prodD)
 
 definition collect where
   "collect F x = (\<Union>f \<in> F. f x)"
 
 lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"

   unfolding Grp_def by auto
 
 lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
   unfolding Grp_def by auto
 
-lemma Collect_split_Grp_eqD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
+lemma Collect_case_prod_Grp_eqD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
   unfolding Grp_def comp_def by auto
 
-lemma Collect_split_Grp_inD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> fst z \<in> A"
+lemma Collect_case_prod_Grp_in: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> fst z \<in> A"
   unfolding Grp_def comp_def by auto
 
 definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
 
 lemma pick_middlep: