# HG changeset patch
# User haftmann
# Date 1440703188 -7200
# Node ID b57df8eecad6097a3e01e2ed8c06739b41ec2ab2
# Parent  162bd20dae23aad5479b4a83dd0764e0da48ec47
standardized some occurences of ancient "split" alias

diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/BNF_Composition.thy
--- a/src/HOL/BNF_Composition.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/BNF_Composition.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -82,7 +82,7 @@
   "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
   by simp
 
-lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
+lemma Grp_fst_snd: "(Grp (Collect (case_prod R)) fst)^--1 OO Grp (Collect (case_prod R)) snd = R"
   unfolding Grp_def fun_eq_iff relcompp.simps by auto
 
 lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/BNF_Def.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -15,7 +15,7 @@
   "bnf" :: thy_goal
 begin
 
-lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
+lemma Collect_splitD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
   by auto
 
 inductive
@@ -98,7 +98,7 @@
   unfolding convol_def by simp
 
 lemma convol_mem_GrpI:
-  "x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (split (Grp A g)))"
+  "x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (case_prod (Grp A g)))"
   unfolding convol_def Grp_def by auto
 
 definition csquare where
@@ -131,10 +131,10 @@
 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 (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
+lemma Collect_split_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 (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
+lemma Collect_split_Grp_inD: "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)"
@@ -149,7 +149,7 @@
 definition sndOp where
   "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))"
 
-lemma fstOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (split P)"
+lemma fstOp_in: "ac \<in> Collect (case_prod (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (case_prod P)"
   unfolding fstOp_def mem_Collect_eq
   by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1])
 
@@ -159,7 +159,7 @@
 lemma snd_sndOp: "snd bc = (snd \<circ> sndOp P Q) bc"
   unfolding comp_def sndOp_def by simp
 
-lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (split Q)"
+lemma sndOp_in: "ac \<in> Collect (case_prod (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (case_prod Q)"
   unfolding sndOp_def mem_Collect_eq
   by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2])
 
@@ -173,15 +173,15 @@
 lemma fst_snd_flip: "fst xy = (snd \<circ> (%(x, y). (y, x))) xy"
   by (simp split: prod.split)
 
-lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
+lemma flip_pred: "A \<subseteq> Collect (case_prod (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (case_prod R)"
   by auto
 
-lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
+lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
   by auto
 
 lemma Collect_split_mono_strong: 
-  "\<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)"
+  "\<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 (case_prod P)\<rbrakk> \<Longrightarrow>
+   A \<subseteq> Collect (case_prod Q)"
   by fastforce
 
 
@@ -216,7 +216,7 @@
 lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
   unfolding rel_fun_def vimage2p_def by auto
 
-lemma convol_image_vimage2p: "\<langle>f \<circ> fst, g \<circ> snd\<rangle> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
+lemma convol_image_vimage2p: "\<langle>f \<circ> fst, g \<circ> snd\<rangle> ` Collect (case_prod (vimage2p f g R)) \<subseteq> Collect (case_prod R)"
   unfolding vimage2p_def convol_def by auto
 
 lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/BNF_Greatest_Fixpoint.thy
--- a/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -82,13 +82,13 @@
 lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
   by blast
 
-lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
+lemma in_rel_Collect_split_eq: "in_rel (Collect (case_prod X)) = X"
   unfolding fun_eq_iff by auto
 
-lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
+lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
   by auto
 
-lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
+lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
   by force
 
 lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/Basic_BNFs.thy
--- a/src/HOL/Basic_BNFs.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Basic_BNFs.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -83,8 +83,8 @@
 next
   fix R S
   show "rel_sum R S =
-        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
-        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
+        (Grp {x. setl x \<subseteq> Collect (case_prod R) \<and> setr x \<subseteq> Collect (case_prod S)} (map_sum fst fst))\<inverse>\<inverse> OO
+        Grp {x. setl x \<subseteq> Collect (case_prod R) \<and> setr x \<subseteq> Collect (case_prod S)} (map_sum snd snd)"
   unfolding sum_set_defs Grp_def relcompp.simps conversep.simps fun_eq_iff
   by (fastforce elim: rel_sum.cases split: sum.splits)
 qed (auto simp: sum_set_defs)
@@ -153,8 +153,8 @@
 next
   fix R S
   show "rel_prod R S =
-        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
-        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
+        (Grp {x. {fst x} \<subseteq> Collect (case_prod R) \<and> {snd x} \<subseteq> Collect (case_prod S)} (map_prod fst fst))\<inverse>\<inverse> OO
+        Grp {x. {fst x} \<subseteq> Collect (case_prod R) \<and> {snd x} \<subseteq> Collect (case_prod S)} (map_prod snd snd)"
   unfolding prod_set_defs rel_prod_apply Grp_def relcompp.simps conversep.simps fun_eq_iff
   by auto
 qed
@@ -197,8 +197,8 @@
 next
   fix R
   show "rel_fun op = R =
-        (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
-         Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
+        (Grp {x. range x \<subseteq> Collect (case_prod R)} (op \<circ> fst))\<inverse>\<inverse> OO
+         Grp {x. range x \<subseteq> Collect (case_prod R)} (op \<circ> snd)"
   unfolding rel_fun_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
     comp_apply mem_Collect_eq split_beta bex_UNIV
   proof (safe, unfold fun_eq_iff[symmetric])
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Fun_Def.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -143,7 +143,7 @@
 
 lemma split_cong [fundef_cong]:
   "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
-    \<Longrightarrow> split f p = split g q"
+    \<Longrightarrow> case_prod f p = case_prod g q"
   by (auto simp: split_def)
 
 lemma comp_cong [fundef_cong]:
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Groups_Big.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -184,7 +184,7 @@
   using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
 
 lemma Sigma:
-  "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (split g) (SIGMA x:A. B x)"
+  "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (case_prod g) (SIGMA x:A. B x)"
 apply (subst Sigma_def)
 apply (subst UNION_disjoint, assumption, simp)
  apply blast
@@ -350,7 +350,7 @@
 qed
 
 lemma cartesian_product:
-   "F (\<lambda>x. F (g x) B) A = F (split g) (A <*> B)"
+   "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A <*> B)"
 apply (rule sym)
 apply (cases "finite A") 
  apply (cases "finite B") 
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/ABP/Abschannel.thy
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
 section {* The transmission channel *}
 
 theory Abschannel
-imports IOA Action Lemmas
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
 begin
 
 datatype 'a abs_action = S 'a | R 'a
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
 section {* The transmission channel -- finite version *}
 
 theory Abschannel_finite
-imports Abschannel IOA Action Lemmas
+imports Abschannel "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
 begin
 
 primrec reverse :: "'a list => 'a list"
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
 section {* The main correctness proof: System_fin implements System *}
 
 theory Correctness
-imports IOA Env Impl Impl_finite
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Env Impl Impl_finite
 begin
 
 ML_file "Check.ML"
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/ABP/Env.thy
--- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
 section {* The environment *}
 
 theory Env
-imports IOA Action
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
 begin
 
 type_synonym
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/ABP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
 section {* The implementation: receiver *}
 
 theory Receiver
-imports IOA Action Lemmas
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
 begin
 
 type_synonym
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/ABP/Sender.thy
--- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
 section {* The implementation: sender *}
 
 theory Sender
-imports IOA Action Lemmas
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
 begin
 
 type_synonym
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/NTP/Abschannel.thy
--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
 section {* The (faulty) transmission channel (both directions) *}
 
 theory Abschannel
-imports IOA Action
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
 begin
 
 datatype 'a abs_action = S 'a | R 'a
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/NTP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
 section {* The implementation: receiver *}
 
 theory Receiver
-imports IOA Action
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
 begin
 
 type_synonym
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/NTP/Sender.thy
--- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
 section {* The implementation: sender *}
 
 theory Sender
-imports IOA Action
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
 begin
 
 type_synonym
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/NTP/Spec.thy
--- a/src/HOL/HOLCF/IOA/NTP/Spec.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Spec.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
 section {* The specification of reliable transmission *}
 
 theory Spec
-imports IOA Action
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
 begin
 
 definition
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/Storage/Spec.thy
--- a/src/HOL/HOLCF/IOA/Storage/Spec.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
 section {* The specification of a memory *}
 
 theory Spec
-imports IOA Action
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
 begin
 
 definition
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -364,7 +364,7 @@
 (* main case *)
 apply clarify
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 (* UU case *)
 apply (simp add: nil_is_Conc)
 (* nil case *)
@@ -431,7 +431,7 @@
   temp_sat_def satisfies_def Init_def unlift_def)
 apply auto
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 done
 
@@ -441,7 +441,7 @@
 lemma TL_ex2seq_UU:
 "(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)"
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
@@ -450,7 +450,7 @@
 lemma TL_ex2seq_nil:
 "(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)"
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
@@ -474,7 +474,7 @@
 
 lemma TLex2seq: "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')"
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 apply auto
 done
@@ -482,7 +482,7 @@
 
 lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
@@ -517,7 +517,7 @@
   temp_sat_def satisfies_def Init_def unlift_def)
 apply auto
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 done
 
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -185,8 +185,7 @@
 apply (auto simp add: mk_traceConc)
 apply (frule reachable.reachable_n)
 apply assumption
-apply (erule_tac x = "y" in allE)
-apply (simp add: move_subprop4 split add: split_if)
+apply (auto simp add: move_subprop4 split add: split_if) 
 done
 
 declare split_if [split]
@@ -232,7 +231,7 @@
 apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
 (* main case *)
 apply auto
-apply (rule_tac t = "f y" in lemma_2_1)
+apply (rule_tac t = "f x2" in lemma_2_1)
 
 (* Finite *)
 apply (erule move_subprop2)
@@ -246,7 +245,7 @@
 
 (* Induction hypothesis  *)
 (* reachable_n looping, therefore apply it manually *)
-apply (erule_tac x = "y" in allE)
+apply (erule_tac x = "x2" in allE)
 apply simp
 apply (frule reachable.reachable_n)
 apply assumption
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -1102,7 +1102,7 @@
   THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));
 
 fun pair_tac ctxt s =
-  Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), s)] [] @{thm PairE}
+  Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), s)] [] @{thm PairE}
   THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;
 
 (* induction on a sequence of pairs with pairsplitting and simplification *)
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -227,7 +227,7 @@
 apply (simp add: executions_def)
 apply (tactic {* pair_tac @{context} "ex" 1 *})
 apply auto
-apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI)
+apply (rule_tac x = " (x1,Cut (%a. fst a:ext A) x2) " in exI)
 apply (simp (no_asm_simp))
 
 (* Subgoal 1: Lemma:  propagation of execution through Cut *)
@@ -237,7 +237,7 @@
 (* Subgoal 2:  Lemma:  Filter P s = Filter P (Cut P s) *)
 
 apply (simp (no_asm) add: filter_act_def)
-apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) y) = Cut (%a. a:ext A) (Map fst$y) ")
+apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) x2) = Cut (%a. a:ext A) (Map fst$x2) ")
 
 apply (rule_tac [2] MapCut [unfolded o_def])
 apply (simp add: FilterCut [symmetric])
@@ -245,7 +245,7 @@
 (* Subgoal 3: Lemma: Cut idempotent  *)
 
 apply (simp (no_asm) add: LastActExtsch_def filter_act_def)
-apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) y) = Cut (%a. a:ext A) (Map fst$y) ")
+apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) x2) = Cut (%a. a:ext A) (Map fst$x2) ")
 apply (rule_tac [2] MapCut [unfolded o_def])
 apply (simp add: Cut_idemp)
 done
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -152,7 +152,7 @@
 
 lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
 apply (tactic {* pair_tac @{context} "exec" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 done
 
@@ -173,14 +173,14 @@
 (* TL = UU *)
 apply (rule conjI)
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 (* TL = nil *)
 apply (rule conjI)
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_tac @{context} "x2" 1 *})
 apply (simp add: unlift_def)
 apply fast
 apply (simp add: unlift_def)
@@ -193,7 +193,7 @@
 apply (simp add: unlift_def)
 
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -396,7 +396,7 @@
 lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)"
 apply (tactic {* pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1 *})
 apply (intro strip)
-apply (tactic {* Seq_case_simp_tac @{context} "xa" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 apply auto
 done
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -546,7 +546,7 @@
 lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
   by simp
 
-lemma Eps_split: "Eps (split P) = (SOME xy. P (fst xy) (snd xy))"
+lemma Eps_split: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
   by (simp add: split_def)
 
 lemma Eps_split_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/List.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -2664,7 +2664,7 @@
 by (simp add: list_all2_conv_all_nth)
 
 lemma list_all2I:
-  "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
+  "\<forall>x \<in> set (zip a b). case_prod P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
 by (simp add: list_all2_iff)
 
 lemma list_all2_nthD:
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Map.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -227,14 +227,14 @@
 
 lemma map_of_mapk_SomeI:
   "inj f \<Longrightarrow> map_of t k = Some x \<Longrightarrow>
-   map_of (map (split (\<lambda>k. Pair (f k))) t) (f k) = Some x"
+   map_of (map (case_prod (\<lambda>k. Pair (f k))) t) (f k) = Some x"
 by (induct t) (auto simp: inj_eq)
 
 lemma weak_map_of_SomeI: "(k, x) \<in> set l \<Longrightarrow> \<exists>x. map_of l k = Some x"
 by (induct l) auto
 
 lemma map_of_filter_in:
-  "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
+  "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (case_prod P) xs) k = Some z"
 by (induct xs) auto
 
 lemma map_of_map:
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -516,11 +516,10 @@
       finally show ?thesis .
     qed
     def C \<equiv> "(split BB) o prod_decode"
-    have C: "!!n. C n \<in> M"
-      apply (rule_tac p="prod_decode n" in PairE)
-      apply (simp add: C_def)
-      apply (metis BB subsetD rangeI)
-      done
+    from BB have "\<And>i j. BB i j \<in> M"
+      by (rule range_subsetD)
+    then have C: "\<And>n. C n \<in> M"
+      by (simp add: C_def split_def)
     have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
     proof (auto simp add: C_def)
       fix x i
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Product_Type.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -284,9 +284,6 @@
 
 subsubsection \<open>Tuple syntax\<close>
 
-abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
-  "split \<equiv> case_prod"
-
 text \<open>
   Patterns -- extends pre-defined type @{typ pttrn} used in
   abstractions.
@@ -310,6 +307,11 @@
   "%(x, y, zs). b" == "CONST case_prod (%x (y, zs). b)"
   "%(x, y). b" == "CONST case_prod (%x y. b)"
   "_abs (CONST Pair x y) t" => "%(x, y). t"
+
+
+
+
+
   -- \<open>The last rule accommodates tuples in `case C ... (x,y) ... => ...'
      The (x,y) is parsed as `Pair x y' because it is logic, not pttrn\<close>
 
@@ -435,13 +437,13 @@
 lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
   by (simp add: prod_eq_iff)
 
-lemma split_conv [simp, code]: "split f (a, b) = f a b"
+lemma split_conv [simp, code]: "case_prod f (a, b) = f a b"
   by (fact prod.case)
 
-lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
+lemma splitI: "f a b \<Longrightarrow> case_prod f (a, b)"
   by (rule split_conv [THEN iffD2])
 
-lemma splitD: "split f (a, b) \<Longrightarrow> f a b"
+lemma splitD: "case_prod f (a, b) \<Longrightarrow> f a b"
   by (rule split_conv [THEN iffD1])
 
 lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
@@ -451,13 +453,13 @@
   -- \<open>Subsumes the old @{text split_Pair} when @{term f} is the identity function.\<close>
   by (simp add: fun_eq_iff split: prod.split)
 
-lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
+lemma split_comp: "case_prod (f \<circ> g) x = f (g (fst x)) (snd x)"
   by (cases x) simp
 
-lemma split_twice: "split f (split g p) = split (\<lambda>x y. split f (g x y)) p"
-  by (cases p) simp
+lemma split_twice: "case_prod f (case_prod g p) = case_prod (\<lambda>x y. case_prod f (g x y)) p"
+  by (fact prod.case_distrib)
 
-lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
+lemma The_split: "The (case_prod P) = (THE xy. P (fst xy) (snd xy))"
   by (simp add: case_prod_unfold)
 
 lemmas split_weak_cong = prod.case_cong_weak
@@ -602,31 +604,31 @@
 lemmas split_split_asm [no_atp] = prod.split_asm
 
 text \<open>
-  \medskip @{term split} used as a logical connective or set former.
+  \medskip @{const case_prod} used as a logical connective or set former.
 
   \medskip These rules are for use with @{text blast}; could instead
   call @{text simp} using @{thm [source] prod.split} as rewrite.\<close>
 
-lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> split c p"
+lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case_prod c p"
   apply (simp only: split_tupled_all)
   apply (simp (no_asm_simp))
   done
 
-lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> split c p x"
+lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> case_prod c p x"
   apply (simp only: split_tupled_all)
   apply (simp (no_asm_simp))
   done
 
-lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
+lemma splitE: "case_prod c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   by (induct p) auto
 
-lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
+lemma splitE': "case_prod c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   by (induct p) auto
 
 lemma splitE2:
-  "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
+  "[| Q (case_prod P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
 proof -
-  assume q: "Q (split P z)"
+  assume q: "Q (case_prod P z)"
   assume r: "!!x y. [|z = (x, y); Q (P x y)|] ==> R"
   show R
     apply (rule r surjective_pairing)+
@@ -634,17 +636,17 @@
     done
 qed
 
-lemma splitD': "split R (a,b) c ==> R a b c"
+lemma splitD': "case_prod R (a,b) c ==> R a b c"
   by simp
 
-lemma mem_splitI: "z: c a b ==> z: split c (a, b)"
+lemma mem_splitI: "z: c a b ==> z: case_prod c (a, b)"
   by simp
 
-lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: split c p"
+lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: case_prod c p"
 by (simp only: split_tupled_all, simp)
 
 lemma mem_splitE:
-  assumes "z \<in> split c p"
+  assumes "z \<in> case_prod c p"
   obtains x y where "p = (x, y)" and "z \<in> c x y"
   using assms by (rule splitE2)
 
@@ -672,10 +674,10 @@
 lemma split_eta_SetCompr [simp, no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   by (rule ext) fast
 
-lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
+lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = case_prod P"
   by (rule ext) fast
 
-lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
+lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & case_prod Q ab)"
   -- \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
   by (rule ext) blast
 
@@ -685,7 +687,7 @@
 *)
 lemma split_comp_eq: 
   fixes f :: "'a => 'b => 'c" and g :: "'d => 'a"
-  shows "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
+  shows "(%u. f (g (fst u)) (snd u)) = (case_prod (%x. f (g x)))"
   by (rule ext) auto
 
 lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
@@ -773,12 +775,8 @@
     "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   by (cases x) blast
 
-lemma split_def:
-  "split = (\<lambda>c p. c (fst p) (snd p))"
-  by (fact case_prod_unfold)
-
 definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
-  "internal_split == split"
+  "internal_split == case_prod"
 
 lemma internal_split_conv: "internal_split c (a, b) = c a b"
   by (simp only: internal_split_def split_conv)
@@ -805,11 +803,11 @@
 lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q"
   by (simp add: curry_def)
 
-lemma curry_split [simp]: "curry (split f) = f"
-  by (simp add: curry_def split_def)
+lemma curry_split [simp]: "curry (case_prod f) = f"
+  by (simp add: curry_def case_prod_unfold)
 
-lemma split_curry [simp]: "split (curry f) = f"
-  by (simp add: curry_def split_def)
+lemma split_curry [simp]: "case_prod (curry f) = f"
+  by (simp add: curry_def case_prod_unfold)
 
 lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)"
 by(simp add: fun_eq_iff)
@@ -1120,11 +1118,11 @@
   by (blast elim: equalityE)
 
 lemma SetCompr_Sigma_eq:
-    "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
+  "Collect (case_prod (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
   by blast
 
 lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q"
-  by blast
+  by (fact SetCompr_Sigma_eq)
 
 lemma UN_Times_distrib:
   "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)"
@@ -1357,16 +1355,17 @@
 
 subsection \<open>Legacy theorem bindings and duplicates\<close>
 
-lemma PairE:
-  obtains x y where "p = (x, y)"
-  by (fact prod.exhaust)
+abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
+  "split \<equiv> case_prod"
 
+lemmas PairE = prod.exhaust
 lemmas Pair_eq = prod.inject
 lemmas fst_conv = prod.sel(1)
 lemmas snd_conv = prod.sel(2)
 lemmas pair_collapse = prod.collapse
 lemmas split = split_conv
 lemmas Pair_fst_snd_eq = prod_eq_iff
+lemmas split_def = case_prod_unfold
 
 hide_const (open) prod
 
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/String.thy
--- a/src/HOL/String.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/String.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -128,9 +128,9 @@
 ML_file "Tools/string_syntax.ML"
 
 lemma UNIV_char:
-  "UNIV = image (split Char) (UNIV \<times> UNIV)"
+  "UNIV = image (case_prod Char) (UNIV \<times> UNIV)"
 proof (rule UNIV_eq_I)
-  fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
+  fix x show "x \<in> image (case_prod Char) (UNIV \<times> UNIV)" by (cases x) auto
 qed
 
 lemma size_char [code, simp]:
@@ -218,7 +218,7 @@
   "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
 
 lemma enum_char_product_enum_nibble:
-  "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
+  "(Enum.enum :: char list) = map (case_prod Char) (List.product Enum.enum Enum.enum)"
   by (simp add: enum_char_def enum_nibble_def)
 
 instance proof
diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -169,8 +169,9 @@
 
 lemma rtrancl_Int_subset: "[| Id \<subseteq> s; (r^* \<inter> s) O r \<subseteq> s|] ==> r^* \<subseteq> s"
   apply (rule subsetI)
-  apply (rule_tac p="x" in PairE, clarify)
-  apply (erule rtrancl_induct, auto) 
+  apply auto
+  apply (erule rtrancl_induct)
+  apply auto
   done
 
 lemma converse_rtranclp_into_rtranclp:
@@ -409,10 +410,9 @@
 
 lemma trancl_Int_subset: "[| r \<subseteq> s; (r^+ \<inter> s) O r \<subseteq> s|] ==> r^+ \<subseteq> s"
   apply (rule subsetI)
-  apply (rule_tac p = x in PairE)
-  apply clarify
+  apply auto
   apply (erule trancl_induct)
-   apply auto
+  apply auto
   done
 
 lemma trancl_unfold: "r^+ = r Un r^+ O r"