standardized some occurences of ancient "split" alias
authorhaftmann
Thu Aug 27 21:19:48 2015 +0200 (2015-08-27)
changeset 61032b57df8eecad6
parent 61031 162bd20dae23
child 61033 fd7fe96ca7b9
standardized some occurences of ancient "split" alias
src/HOL/BNF_Composition.thy
src/HOL/BNF_Def.thy
src/HOL/BNF_Greatest_Fixpoint.thy
src/HOL/Basic_BNFs.thy
src/HOL/Fun_Def.thy
src/HOL/Groups_Big.thy
src/HOL/HOLCF/IOA/ABP/Abschannel.thy
src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy
src/HOL/HOLCF/IOA/ABP/Correctness.thy
src/HOL/HOLCF/IOA/ABP/Env.thy
src/HOL/HOLCF/IOA/ABP/Receiver.thy
src/HOL/HOLCF/IOA/ABP/Sender.thy
src/HOL/HOLCF/IOA/NTP/Abschannel.thy
src/HOL/HOLCF/IOA/NTP/Receiver.thy
src/HOL/HOLCF/IOA/NTP/Sender.thy
src/HOL/HOLCF/IOA/NTP/Spec.thy
src/HOL/HOLCF/IOA/Storage/Spec.thy
src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy
src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy
src/HOL/HOLCF/IOA/meta_theory/TLS.thy
src/HOL/HOLCF/IOA/meta_theory/Traces.thy
src/HOL/Hilbert_Choice.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Product_Type.thy
src/HOL/String.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/BNF_Composition.thy	Thu Aug 27 13:07:45 2015 +0200
     1.2 +++ b/src/HOL/BNF_Composition.thy	Thu Aug 27 21:19:48 2015 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4    "\<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"
     1.5    by simp
     1.6  
     1.7 -lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
     1.8 +lemma Grp_fst_snd: "(Grp (Collect (case_prod R)) fst)^--1 OO Grp (Collect (case_prod R)) snd = R"
     1.9    unfolding Grp_def fun_eq_iff relcompp.simps by auto
    1.10  
    1.11  lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
     2.1 --- a/src/HOL/BNF_Def.thy	Thu Aug 27 13:07:45 2015 +0200
     2.2 +++ b/src/HOL/BNF_Def.thy	Thu Aug 27 21:19:48 2015 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4    "bnf" :: thy_goal
     2.5  begin
     2.6  
     2.7 -lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
     2.8 +lemma Collect_splitD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
     2.9    by auto
    2.10  
    2.11  inductive
    2.12 @@ -98,7 +98,7 @@
    2.13    unfolding convol_def by simp
    2.14  
    2.15  lemma convol_mem_GrpI:
    2.16 -  "x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (split (Grp A g)))"
    2.17 +  "x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (case_prod (Grp A g)))"
    2.18    unfolding convol_def Grp_def by auto
    2.19  
    2.20  definition csquare where
    2.21 @@ -131,10 +131,10 @@
    2.22  lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
    2.23    unfolding Grp_def by auto
    2.24  
    2.25 -lemma Collect_split_Grp_eqD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
    2.26 +lemma Collect_split_Grp_eqD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
    2.27    unfolding Grp_def comp_def by auto
    2.28  
    2.29 -lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
    2.30 +lemma Collect_split_Grp_inD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> fst z \<in> A"
    2.31    unfolding Grp_def comp_def by auto
    2.32  
    2.33  definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
    2.34 @@ -149,7 +149,7 @@
    2.35  definition sndOp where
    2.36    "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))"
    2.37  
    2.38 -lemma fstOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (split P)"
    2.39 +lemma fstOp_in: "ac \<in> Collect (case_prod (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (case_prod P)"
    2.40    unfolding fstOp_def mem_Collect_eq
    2.41    by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1])
    2.42  
    2.43 @@ -159,7 +159,7 @@
    2.44  lemma snd_sndOp: "snd bc = (snd \<circ> sndOp P Q) bc"
    2.45    unfolding comp_def sndOp_def by simp
    2.46  
    2.47 -lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (split Q)"
    2.48 +lemma sndOp_in: "ac \<in> Collect (case_prod (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (case_prod Q)"
    2.49    unfolding sndOp_def mem_Collect_eq
    2.50    by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2])
    2.51  
    2.52 @@ -173,15 +173,15 @@
    2.53  lemma fst_snd_flip: "fst xy = (snd \<circ> (%(x, y). (y, x))) xy"
    2.54    by (simp split: prod.split)
    2.55  
    2.56 -lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
    2.57 +lemma flip_pred: "A \<subseteq> Collect (case_prod (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (case_prod R)"
    2.58    by auto
    2.59  
    2.60 -lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
    2.61 +lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
    2.62    by auto
    2.63  
    2.64  lemma Collect_split_mono_strong: 
    2.65 -  "\<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>
    2.66 -   A \<subseteq> Collect (split Q)"
    2.67 +  "\<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>
    2.68 +   A \<subseteq> Collect (case_prod Q)"
    2.69    by fastforce
    2.70  
    2.71  
    2.72 @@ -216,7 +216,7 @@
    2.73  lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
    2.74    unfolding rel_fun_def vimage2p_def by auto
    2.75  
    2.76 -lemma convol_image_vimage2p: "\<langle>f \<circ> fst, g \<circ> snd\<rangle> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
    2.77 +lemma convol_image_vimage2p: "\<langle>f \<circ> fst, g \<circ> snd\<rangle> ` Collect (case_prod (vimage2p f g R)) \<subseteq> Collect (case_prod R)"
    2.78    unfolding vimage2p_def convol_def by auto
    2.79  
    2.80  lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
     3.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Aug 27 13:07:45 2015 +0200
     3.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Aug 27 21:19:48 2015 +0200
     3.3 @@ -82,13 +82,13 @@
     3.4  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})"
     3.5    by blast
     3.6  
     3.7 -lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
     3.8 +lemma in_rel_Collect_split_eq: "in_rel (Collect (case_prod X)) = X"
     3.9    unfolding fun_eq_iff by auto
    3.10  
    3.11 -lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
    3.12 +lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
    3.13    by auto
    3.14  
    3.15 -lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
    3.16 +lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
    3.17    by force
    3.18  
    3.19  lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
     4.1 --- a/src/HOL/Basic_BNFs.thy	Thu Aug 27 13:07:45 2015 +0200
     4.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Aug 27 21:19:48 2015 +0200
     4.3 @@ -83,8 +83,8 @@
     4.4  next
     4.5    fix R S
     4.6    show "rel_sum R S =
     4.7 -        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
     4.8 -        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
     4.9 +        (Grp {x. setl x \<subseteq> Collect (case_prod R) \<and> setr x \<subseteq> Collect (case_prod S)} (map_sum fst fst))\<inverse>\<inverse> OO
    4.10 +        Grp {x. setl x \<subseteq> Collect (case_prod R) \<and> setr x \<subseteq> Collect (case_prod S)} (map_sum snd snd)"
    4.11    unfolding sum_set_defs Grp_def relcompp.simps conversep.simps fun_eq_iff
    4.12    by (fastforce elim: rel_sum.cases split: sum.splits)
    4.13  qed (auto simp: sum_set_defs)
    4.14 @@ -153,8 +153,8 @@
    4.15  next
    4.16    fix R S
    4.17    show "rel_prod R S =
    4.18 -        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
    4.19 -        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
    4.20 +        (Grp {x. {fst x} \<subseteq> Collect (case_prod R) \<and> {snd x} \<subseteq> Collect (case_prod S)} (map_prod fst fst))\<inverse>\<inverse> OO
    4.21 +        Grp {x. {fst x} \<subseteq> Collect (case_prod R) \<and> {snd x} \<subseteq> Collect (case_prod S)} (map_prod snd snd)"
    4.22    unfolding prod_set_defs rel_prod_apply Grp_def relcompp.simps conversep.simps fun_eq_iff
    4.23    by auto
    4.24  qed
    4.25 @@ -197,8 +197,8 @@
    4.26  next
    4.27    fix R
    4.28    show "rel_fun op = R =
    4.29 -        (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
    4.30 -         Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
    4.31 +        (Grp {x. range x \<subseteq> Collect (case_prod R)} (op \<circ> fst))\<inverse>\<inverse> OO
    4.32 +         Grp {x. range x \<subseteq> Collect (case_prod R)} (op \<circ> snd)"
    4.33    unfolding rel_fun_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
    4.34      comp_apply mem_Collect_eq split_beta bex_UNIV
    4.35    proof (safe, unfold fun_eq_iff[symmetric])
     5.1 --- a/src/HOL/Fun_Def.thy	Thu Aug 27 13:07:45 2015 +0200
     5.2 +++ b/src/HOL/Fun_Def.thy	Thu Aug 27 21:19:48 2015 +0200
     5.3 @@ -143,7 +143,7 @@
     5.4  
     5.5  lemma split_cong [fundef_cong]:
     5.6    "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
     5.7 -    \<Longrightarrow> split f p = split g q"
     5.8 +    \<Longrightarrow> case_prod f p = case_prod g q"
     5.9    by (auto simp: split_def)
    5.10  
    5.11  lemma comp_cong [fundef_cong]:
     6.1 --- a/src/HOL/Groups_Big.thy	Thu Aug 27 13:07:45 2015 +0200
     6.2 +++ b/src/HOL/Groups_Big.thy	Thu Aug 27 21:19:48 2015 +0200
     6.3 @@ -184,7 +184,7 @@
     6.4    using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
     6.5  
     6.6  lemma Sigma:
     6.7 -  "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)"
     6.8 +  "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)"
     6.9  apply (subst Sigma_def)
    6.10  apply (subst UNION_disjoint, assumption, simp)
    6.11   apply blast
    6.12 @@ -350,7 +350,7 @@
    6.13  qed
    6.14  
    6.15  lemma cartesian_product:
    6.16 -   "F (\<lambda>x. F (g x) B) A = F (split g) (A <*> B)"
    6.17 +   "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A <*> B)"
    6.18  apply (rule sym)
    6.19  apply (cases "finite A") 
    6.20   apply (cases "finite B") 
     7.1 --- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Thu Aug 27 13:07:45 2015 +0200
     7.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Thu Aug 27 21:19:48 2015 +0200
     7.3 @@ -5,7 +5,7 @@
     7.4  section {* The transmission channel *}
     7.5  
     7.6  theory Abschannel
     7.7 -imports IOA Action Lemmas
     7.8 +imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
     7.9  begin
    7.10  
    7.11  datatype 'a abs_action = S 'a | R 'a
     8.1 --- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Thu Aug 27 13:07:45 2015 +0200
     8.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Thu Aug 27 21:19:48 2015 +0200
     8.3 @@ -5,7 +5,7 @@
     8.4  section {* The transmission channel -- finite version *}
     8.5  
     8.6  theory Abschannel_finite
     8.7 -imports Abschannel IOA Action Lemmas
     8.8 +imports Abschannel "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
     8.9  begin
    8.10  
    8.11  primrec reverse :: "'a list => 'a list"
     9.1 --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Thu Aug 27 13:07:45 2015 +0200
     9.2 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Thu Aug 27 21:19:48 2015 +0200
     9.3 @@ -5,7 +5,7 @@
     9.4  section {* The main correctness proof: System_fin implements System *}
     9.5  
     9.6  theory Correctness
     9.7 -imports IOA Env Impl Impl_finite
     9.8 +imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Env Impl Impl_finite
     9.9  begin
    9.10  
    9.11  ML_file "Check.ML"
    10.1 --- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Thu Aug 27 13:07:45 2015 +0200
    10.2 +++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Thu Aug 27 21:19:48 2015 +0200
    10.3 @@ -5,7 +5,7 @@
    10.4  section {* The environment *}
    10.5  
    10.6  theory Env
    10.7 -imports IOA Action
    10.8 +imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
    10.9  begin
   10.10  
   10.11  type_synonym
    11.1 --- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Thu Aug 27 13:07:45 2015 +0200
    11.2 +++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Thu Aug 27 21:19:48 2015 +0200
    11.3 @@ -5,7 +5,7 @@
    11.4  section {* The implementation: receiver *}
    11.5  
    11.6  theory Receiver
    11.7 -imports IOA Action Lemmas
    11.8 +imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
    11.9  begin
   11.10  
   11.11  type_synonym
    12.1 --- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Thu Aug 27 13:07:45 2015 +0200
    12.2 +++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Thu Aug 27 21:19:48 2015 +0200
    12.3 @@ -5,7 +5,7 @@
    12.4  section {* The implementation: sender *}
    12.5  
    12.6  theory Sender
    12.7 -imports IOA Action Lemmas
    12.8 +imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
    12.9  begin
   12.10  
   12.11  type_synonym
    13.1 --- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Thu Aug 27 13:07:45 2015 +0200
    13.2 +++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Thu Aug 27 21:19:48 2015 +0200
    13.3 @@ -5,7 +5,7 @@
    13.4  section {* The (faulty) transmission channel (both directions) *}
    13.5  
    13.6  theory Abschannel
    13.7 -imports IOA Action
    13.8 +imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
    13.9  begin
   13.10  
   13.11  datatype 'a abs_action = S 'a | R 'a
    14.1 --- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Thu Aug 27 13:07:45 2015 +0200
    14.2 +++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Thu Aug 27 21:19:48 2015 +0200
    14.3 @@ -5,7 +5,7 @@
    14.4  section {* The implementation: receiver *}
    14.5  
    14.6  theory Receiver
    14.7 -imports IOA Action
    14.8 +imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
    14.9  begin
   14.10  
   14.11  type_synonym
    15.1 --- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Thu Aug 27 13:07:45 2015 +0200
    15.2 +++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Thu Aug 27 21:19:48 2015 +0200
    15.3 @@ -5,7 +5,7 @@
    15.4  section {* The implementation: sender *}
    15.5  
    15.6  theory Sender
    15.7 -imports IOA Action
    15.8 +imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
    15.9  begin
   15.10  
   15.11  type_synonym
    16.1 --- a/src/HOL/HOLCF/IOA/NTP/Spec.thy	Thu Aug 27 13:07:45 2015 +0200
    16.2 +++ b/src/HOL/HOLCF/IOA/NTP/Spec.thy	Thu Aug 27 21:19:48 2015 +0200
    16.3 @@ -5,7 +5,7 @@
    16.4  section {* The specification of reliable transmission *}
    16.5  
    16.6  theory Spec
    16.7 -imports IOA Action
    16.8 +imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
    16.9  begin
   16.10  
   16.11  definition
    17.1 --- a/src/HOL/HOLCF/IOA/Storage/Spec.thy	Thu Aug 27 13:07:45 2015 +0200
    17.2 +++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy	Thu Aug 27 21:19:48 2015 +0200
    17.3 @@ -5,7 +5,7 @@
    17.4  section {* The specification of a memory *}
    17.5  
    17.6  theory Spec
    17.7 -imports IOA Action
    17.8 +imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
    17.9  begin
   17.10  
   17.11  definition
    18.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Aug 27 13:07:45 2015 +0200
    18.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Aug 27 21:19:48 2015 +0200
    18.3 @@ -364,7 +364,7 @@
    18.4  (* main case *)
    18.5  apply clarify
    18.6  apply (tactic {* pair_tac @{context} "ex" 1 *})
    18.7 -apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
    18.8 +apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
    18.9  (* UU case *)
   18.10  apply (simp add: nil_is_Conc)
   18.11  (* nil case *)
   18.12 @@ -431,7 +431,7 @@
   18.13    temp_sat_def satisfies_def Init_def unlift_def)
   18.14  apply auto
   18.15  apply (tactic {* pair_tac @{context} "ex" 1 *})
   18.16 -apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   18.17 +apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
   18.18  apply (tactic {* pair_tac @{context} "a" 1 *})
   18.19  done
   18.20  
   18.21 @@ -441,7 +441,7 @@
   18.22  lemma TL_ex2seq_UU:
   18.23  "(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)"
   18.24  apply (tactic {* pair_tac @{context} "ex" 1 *})
   18.25 -apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   18.26 +apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
   18.27  apply (tactic {* pair_tac @{context} "a" 1 *})
   18.28  apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   18.29  apply (tactic {* pair_tac @{context} "a" 1 *})
   18.30 @@ -450,7 +450,7 @@
   18.31  lemma TL_ex2seq_nil:
   18.32  "(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)"
   18.33  apply (tactic {* pair_tac @{context} "ex" 1 *})
   18.34 -apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   18.35 +apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
   18.36  apply (tactic {* pair_tac @{context} "a" 1 *})
   18.37  apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   18.38  apply (tactic {* pair_tac @{context} "a" 1 *})
   18.39 @@ -474,7 +474,7 @@
   18.40  
   18.41  lemma TLex2seq: "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')"
   18.42  apply (tactic {* pair_tac @{context} "ex" 1 *})
   18.43 -apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   18.44 +apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
   18.45  apply (tactic {* pair_tac @{context} "a" 1 *})
   18.46  apply auto
   18.47  done
   18.48 @@ -482,7 +482,7 @@
   18.49  
   18.50  lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"
   18.51  apply (tactic {* pair_tac @{context} "ex" 1 *})
   18.52 -apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   18.53 +apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
   18.54  apply (tactic {* pair_tac @{context} "a" 1 *})
   18.55  apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   18.56  apply (tactic {* pair_tac @{context} "a" 1 *})
   18.57 @@ -517,7 +517,7 @@
   18.58    temp_sat_def satisfies_def Init_def unlift_def)
   18.59  apply auto
   18.60  apply (tactic {* pair_tac @{context} "ex" 1 *})
   18.61 -apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   18.62 +apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
   18.63  apply (tactic {* pair_tac @{context} "a" 1 *})
   18.64  done
   18.65  
    19.1 --- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Aug 27 13:07:45 2015 +0200
    19.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Aug 27 21:19:48 2015 +0200
    19.3 @@ -185,8 +185,7 @@
    19.4  apply (auto simp add: mk_traceConc)
    19.5  apply (frule reachable.reachable_n)
    19.6  apply assumption
    19.7 -apply (erule_tac x = "y" in allE)
    19.8 -apply (simp add: move_subprop4 split add: split_if)
    19.9 +apply (auto simp add: move_subprop4 split add: split_if) 
   19.10  done
   19.11  
   19.12  declare split_if [split]
   19.13 @@ -232,7 +231,7 @@
   19.14  apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
   19.15  (* main case *)
   19.16  apply auto
   19.17 -apply (rule_tac t = "f y" in lemma_2_1)
   19.18 +apply (rule_tac t = "f x2" in lemma_2_1)
   19.19  
   19.20  (* Finite *)
   19.21  apply (erule move_subprop2)
   19.22 @@ -246,7 +245,7 @@
   19.23  
   19.24  (* Induction hypothesis  *)
   19.25  (* reachable_n looping, therefore apply it manually *)
   19.26 -apply (erule_tac x = "y" in allE)
   19.27 +apply (erule_tac x = "x2" in allE)
   19.28  apply simp
   19.29  apply (frule reachable.reachable_n)
   19.30  apply assumption
    20.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Thu Aug 27 13:07:45 2015 +0200
    20.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Thu Aug 27 21:19:48 2015 +0200
    20.3 @@ -1102,7 +1102,7 @@
    20.4    THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));
    20.5  
    20.6  fun pair_tac ctxt s =
    20.7 -  Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), s)] [] @{thm PairE}
    20.8 +  Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), s)] [] @{thm PairE}
    20.9    THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;
   20.10  
   20.11  (* induction on a sequence of pairs with pairsplitting and simplification *)
    21.1 --- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Thu Aug 27 13:07:45 2015 +0200
    21.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Thu Aug 27 21:19:48 2015 +0200
    21.3 @@ -227,7 +227,7 @@
    21.4  apply (simp add: executions_def)
    21.5  apply (tactic {* pair_tac @{context} "ex" 1 *})
    21.6  apply auto
    21.7 -apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI)
    21.8 +apply (rule_tac x = " (x1,Cut (%a. fst a:ext A) x2) " in exI)
    21.9  apply (simp (no_asm_simp))
   21.10  
   21.11  (* Subgoal 1: Lemma:  propagation of execution through Cut *)
   21.12 @@ -237,7 +237,7 @@
   21.13  (* Subgoal 2:  Lemma:  Filter P s = Filter P (Cut P s) *)
   21.14  
   21.15  apply (simp (no_asm) add: filter_act_def)
   21.16 -apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) y) = Cut (%a. a:ext A) (Map fst$y) ")
   21.17 +apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) x2) = Cut (%a. a:ext A) (Map fst$x2) ")
   21.18  
   21.19  apply (rule_tac [2] MapCut [unfolded o_def])
   21.20  apply (simp add: FilterCut [symmetric])
   21.21 @@ -245,7 +245,7 @@
   21.22  (* Subgoal 3: Lemma: Cut idempotent  *)
   21.23  
   21.24  apply (simp (no_asm) add: LastActExtsch_def filter_act_def)
   21.25 -apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) y) = Cut (%a. a:ext A) (Map fst$y) ")
   21.26 +apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) x2) = Cut (%a. a:ext A) (Map fst$x2) ")
   21.27  apply (rule_tac [2] MapCut [unfolded o_def])
   21.28  apply (simp add: Cut_idemp)
   21.29  done
    22.1 --- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Thu Aug 27 13:07:45 2015 +0200
    22.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Thu Aug 27 21:19:48 2015 +0200
    22.3 @@ -152,7 +152,7 @@
    22.4  
    22.5  lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
    22.6  apply (tactic {* pair_tac @{context} "exec" 1 *})
    22.7 -apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
    22.8 +apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
    22.9  apply (tactic {* pair_tac @{context} "a" 1 *})
   22.10  done
   22.11  
   22.12 @@ -173,14 +173,14 @@
   22.13  (* TL = UU *)
   22.14  apply (rule conjI)
   22.15  apply (tactic {* pair_tac @{context} "ex" 1 *})
   22.16 -apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   22.17 +apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
   22.18  apply (tactic {* pair_tac @{context} "a" 1 *})
   22.19  apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   22.20  apply (tactic {* pair_tac @{context} "a" 1 *})
   22.21  (* TL = nil *)
   22.22  apply (rule conjI)
   22.23  apply (tactic {* pair_tac @{context} "ex" 1 *})
   22.24 -apply (tactic {* Seq_case_tac @{context} "y" 1 *})
   22.25 +apply (tactic {* Seq_case_tac @{context} "x2" 1 *})
   22.26  apply (simp add: unlift_def)
   22.27  apply fast
   22.28  apply (simp add: unlift_def)
   22.29 @@ -193,7 +193,7 @@
   22.30  apply (simp add: unlift_def)
   22.31  
   22.32  apply (tactic {* pair_tac @{context} "ex" 1 *})
   22.33 -apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   22.34 +apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
   22.35  apply (tactic {* pair_tac @{context} "a" 1 *})
   22.36  apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   22.37  apply (tactic {* pair_tac @{context} "a" 1 *})
    23.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Thu Aug 27 13:07:45 2015 +0200
    23.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Thu Aug 27 21:19:48 2015 +0200
    23.3 @@ -396,7 +396,7 @@
    23.4  lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)"
    23.5  apply (tactic {* pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1 *})
    23.6  apply (intro strip)
    23.7 -apply (tactic {* Seq_case_simp_tac @{context} "xa" 1 *})
    23.8 +apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *})
    23.9  apply (tactic {* pair_tac @{context} "a" 1 *})
   23.10  apply auto
   23.11  done
    24.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Aug 27 13:07:45 2015 +0200
    24.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Aug 27 21:19:48 2015 +0200
    24.3 @@ -546,7 +546,7 @@
    24.4  lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
    24.5    by simp
    24.6  
    24.7 -lemma Eps_split: "Eps (split P) = (SOME xy. P (fst xy) (snd xy))"
    24.8 +lemma Eps_split: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
    24.9    by (simp add: split_def)
   24.10  
   24.11  lemma Eps_split_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
    25.1 --- a/src/HOL/List.thy	Thu Aug 27 13:07:45 2015 +0200
    25.2 +++ b/src/HOL/List.thy	Thu Aug 27 21:19:48 2015 +0200
    25.3 @@ -2664,7 +2664,7 @@
    25.4  by (simp add: list_all2_conv_all_nth)
    25.5  
    25.6  lemma list_all2I:
    25.7 -  "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
    25.8 +  "\<forall>x \<in> set (zip a b). case_prod P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
    25.9  by (simp add: list_all2_iff)
   25.10  
   25.11  lemma list_all2_nthD:
    26.1 --- a/src/HOL/Map.thy	Thu Aug 27 13:07:45 2015 +0200
    26.2 +++ b/src/HOL/Map.thy	Thu Aug 27 21:19:48 2015 +0200
    26.3 @@ -227,14 +227,14 @@
    26.4  
    26.5  lemma map_of_mapk_SomeI:
    26.6    "inj f \<Longrightarrow> map_of t k = Some x \<Longrightarrow>
    26.7 -   map_of (map (split (\<lambda>k. Pair (f k))) t) (f k) = Some x"
    26.8 +   map_of (map (case_prod (\<lambda>k. Pair (f k))) t) (f k) = Some x"
    26.9  by (induct t) (auto simp: inj_eq)
   26.10  
   26.11  lemma weak_map_of_SomeI: "(k, x) \<in> set l \<Longrightarrow> \<exists>x. map_of l k = Some x"
   26.12  by (induct l) auto
   26.13  
   26.14  lemma map_of_filter_in:
   26.15 -  "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
   26.16 +  "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (case_prod P) xs) k = Some z"
   26.17  by (induct xs) auto
   26.18  
   26.19  lemma map_of_map:
    27.1 --- a/src/HOL/Probability/Caratheodory.thy	Thu Aug 27 13:07:45 2015 +0200
    27.2 +++ b/src/HOL/Probability/Caratheodory.thy	Thu Aug 27 21:19:48 2015 +0200
    27.3 @@ -516,11 +516,10 @@
    27.4        finally show ?thesis .
    27.5      qed
    27.6      def C \<equiv> "(split BB) o prod_decode"
    27.7 -    have C: "!!n. C n \<in> M"
    27.8 -      apply (rule_tac p="prod_decode n" in PairE)
    27.9 -      apply (simp add: C_def)
   27.10 -      apply (metis BB subsetD rangeI)
   27.11 -      done
   27.12 +    from BB have "\<And>i j. BB i j \<in> M"
   27.13 +      by (rule range_subsetD)
   27.14 +    then have C: "\<And>n. C n \<in> M"
   27.15 +      by (simp add: C_def split_def)
   27.16      have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
   27.17      proof (auto simp add: C_def)
   27.18        fix x i
    28.1 --- a/src/HOL/Product_Type.thy	Thu Aug 27 13:07:45 2015 +0200
    28.2 +++ b/src/HOL/Product_Type.thy	Thu Aug 27 21:19:48 2015 +0200
    28.3 @@ -284,9 +284,6 @@
    28.4  
    28.5  subsubsection \<open>Tuple syntax\<close>
    28.6  
    28.7 -abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
    28.8 -  "split \<equiv> case_prod"
    28.9 -
   28.10  text \<open>
   28.11    Patterns -- extends pre-defined type @{typ pttrn} used in
   28.12    abstractions.
   28.13 @@ -310,6 +307,11 @@
   28.14    "%(x, y, zs). b" == "CONST case_prod (%x (y, zs). b)"
   28.15    "%(x, y). b" == "CONST case_prod (%x y. b)"
   28.16    "_abs (CONST Pair x y) t" => "%(x, y). t"
   28.17 +
   28.18 +
   28.19 +
   28.20 +
   28.21 +
   28.22    -- \<open>The last rule accommodates tuples in `case C ... (x,y) ... => ...'
   28.23       The (x,y) is parsed as `Pair x y' because it is logic, not pttrn\<close>
   28.24  
   28.25 @@ -435,13 +437,13 @@
   28.26  lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
   28.27    by (simp add: prod_eq_iff)
   28.28  
   28.29 -lemma split_conv [simp, code]: "split f (a, b) = f a b"
   28.30 +lemma split_conv [simp, code]: "case_prod f (a, b) = f a b"
   28.31    by (fact prod.case)
   28.32  
   28.33 -lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
   28.34 +lemma splitI: "f a b \<Longrightarrow> case_prod f (a, b)"
   28.35    by (rule split_conv [THEN iffD2])
   28.36  
   28.37 -lemma splitD: "split f (a, b) \<Longrightarrow> f a b"
   28.38 +lemma splitD: "case_prod f (a, b) \<Longrightarrow> f a b"
   28.39    by (rule split_conv [THEN iffD1])
   28.40  
   28.41  lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
   28.42 @@ -451,13 +453,13 @@
   28.43    -- \<open>Subsumes the old @{text split_Pair} when @{term f} is the identity function.\<close>
   28.44    by (simp add: fun_eq_iff split: prod.split)
   28.45  
   28.46 -lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
   28.47 +lemma split_comp: "case_prod (f \<circ> g) x = f (g (fst x)) (snd x)"
   28.48    by (cases x) simp
   28.49  
   28.50 -lemma split_twice: "split f (split g p) = split (\<lambda>x y. split f (g x y)) p"
   28.51 -  by (cases p) simp
   28.52 +lemma split_twice: "case_prod f (case_prod g p) = case_prod (\<lambda>x y. case_prod f (g x y)) p"
   28.53 +  by (fact prod.case_distrib)
   28.54  
   28.55 -lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
   28.56 +lemma The_split: "The (case_prod P) = (THE xy. P (fst xy) (snd xy))"
   28.57    by (simp add: case_prod_unfold)
   28.58  
   28.59  lemmas split_weak_cong = prod.case_cong_weak
   28.60 @@ -602,31 +604,31 @@
   28.61  lemmas split_split_asm [no_atp] = prod.split_asm
   28.62  
   28.63  text \<open>
   28.64 -  \medskip @{term split} used as a logical connective or set former.
   28.65 +  \medskip @{const case_prod} used as a logical connective or set former.
   28.66  
   28.67    \medskip These rules are for use with @{text blast}; could instead
   28.68    call @{text simp} using @{thm [source] prod.split} as rewrite.\<close>
   28.69  
   28.70 -lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> split c p"
   28.71 +lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case_prod c p"
   28.72    apply (simp only: split_tupled_all)
   28.73    apply (simp (no_asm_simp))
   28.74    done
   28.75  
   28.76 -lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> split c p x"
   28.77 +lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> case_prod c p x"
   28.78    apply (simp only: split_tupled_all)
   28.79    apply (simp (no_asm_simp))
   28.80    done
   28.81  
   28.82 -lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   28.83 +lemma splitE: "case_prod c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   28.84    by (induct p) auto
   28.85  
   28.86 -lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   28.87 +lemma splitE': "case_prod c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   28.88    by (induct p) auto
   28.89  
   28.90  lemma splitE2:
   28.91 -  "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
   28.92 +  "[| Q (case_prod P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
   28.93  proof -
   28.94 -  assume q: "Q (split P z)"
   28.95 +  assume q: "Q (case_prod P z)"
   28.96    assume r: "!!x y. [|z = (x, y); Q (P x y)|] ==> R"
   28.97    show R
   28.98      apply (rule r surjective_pairing)+
   28.99 @@ -634,17 +636,17 @@
  28.100      done
  28.101  qed
  28.102  
  28.103 -lemma splitD': "split R (a,b) c ==> R a b c"
  28.104 +lemma splitD': "case_prod R (a,b) c ==> R a b c"
  28.105    by simp
  28.106  
  28.107 -lemma mem_splitI: "z: c a b ==> z: split c (a, b)"
  28.108 +lemma mem_splitI: "z: c a b ==> z: case_prod c (a, b)"
  28.109    by simp
  28.110  
  28.111 -lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: split c p"
  28.112 +lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: case_prod c p"
  28.113  by (simp only: split_tupled_all, simp)
  28.114  
  28.115  lemma mem_splitE:
  28.116 -  assumes "z \<in> split c p"
  28.117 +  assumes "z \<in> case_prod c p"
  28.118    obtains x y where "p = (x, y)" and "z \<in> c x y"
  28.119    using assms by (rule splitE2)
  28.120  
  28.121 @@ -672,10 +674,10 @@
  28.122  lemma split_eta_SetCompr [simp, no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
  28.123    by (rule ext) fast
  28.124  
  28.125 -lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
  28.126 +lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = case_prod P"
  28.127    by (rule ext) fast
  28.128  
  28.129 -lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
  28.130 +lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & case_prod Q ab)"
  28.131    -- \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
  28.132    by (rule ext) blast
  28.133  
  28.134 @@ -685,7 +687,7 @@
  28.135  *)
  28.136  lemma split_comp_eq: 
  28.137    fixes f :: "'a => 'b => 'c" and g :: "'d => 'a"
  28.138 -  shows "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
  28.139 +  shows "(%u. f (g (fst u)) (snd u)) = (case_prod (%x. f (g x)))"
  28.140    by (rule ext) auto
  28.141  
  28.142  lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
  28.143 @@ -773,12 +775,8 @@
  28.144      "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
  28.145    by (cases x) blast
  28.146  
  28.147 -lemma split_def:
  28.148 -  "split = (\<lambda>c p. c (fst p) (snd p))"
  28.149 -  by (fact case_prod_unfold)
  28.150 -
  28.151  definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
  28.152 -  "internal_split == split"
  28.153 +  "internal_split == case_prod"
  28.154  
  28.155  lemma internal_split_conv: "internal_split c (a, b) = c a b"
  28.156    by (simp only: internal_split_def split_conv)
  28.157 @@ -805,11 +803,11 @@
  28.158  lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q"
  28.159    by (simp add: curry_def)
  28.160  
  28.161 -lemma curry_split [simp]: "curry (split f) = f"
  28.162 -  by (simp add: curry_def split_def)
  28.163 +lemma curry_split [simp]: "curry (case_prod f) = f"
  28.164 +  by (simp add: curry_def case_prod_unfold)
  28.165  
  28.166 -lemma split_curry [simp]: "split (curry f) = f"
  28.167 -  by (simp add: curry_def split_def)
  28.168 +lemma split_curry [simp]: "case_prod (curry f) = f"
  28.169 +  by (simp add: curry_def case_prod_unfold)
  28.170  
  28.171  lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)"
  28.172  by(simp add: fun_eq_iff)
  28.173 @@ -1120,11 +1118,11 @@
  28.174    by (blast elim: equalityE)
  28.175  
  28.176  lemma SetCompr_Sigma_eq:
  28.177 -    "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
  28.178 +  "Collect (case_prod (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
  28.179    by blast
  28.180  
  28.181  lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q"
  28.182 -  by blast
  28.183 +  by (fact SetCompr_Sigma_eq)
  28.184  
  28.185  lemma UN_Times_distrib:
  28.186    "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)"
  28.187 @@ -1357,16 +1355,17 @@
  28.188  
  28.189  subsection \<open>Legacy theorem bindings and duplicates\<close>
  28.190  
  28.191 -lemma PairE:
  28.192 -  obtains x y where "p = (x, y)"
  28.193 -  by (fact prod.exhaust)
  28.194 +abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
  28.195 +  "split \<equiv> case_prod"
  28.196  
  28.197 +lemmas PairE = prod.exhaust
  28.198  lemmas Pair_eq = prod.inject
  28.199  lemmas fst_conv = prod.sel(1)
  28.200  lemmas snd_conv = prod.sel(2)
  28.201  lemmas pair_collapse = prod.collapse
  28.202  lemmas split = split_conv
  28.203  lemmas Pair_fst_snd_eq = prod_eq_iff
  28.204 +lemmas split_def = case_prod_unfold
  28.205  
  28.206  hide_const (open) prod
  28.207  
    29.1 --- a/src/HOL/String.thy	Thu Aug 27 13:07:45 2015 +0200
    29.2 +++ b/src/HOL/String.thy	Thu Aug 27 21:19:48 2015 +0200
    29.3 @@ -128,9 +128,9 @@
    29.4  ML_file "Tools/string_syntax.ML"
    29.5  
    29.6  lemma UNIV_char:
    29.7 -  "UNIV = image (split Char) (UNIV \<times> UNIV)"
    29.8 +  "UNIV = image (case_prod Char) (UNIV \<times> UNIV)"
    29.9  proof (rule UNIV_eq_I)
   29.10 -  fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
   29.11 +  fix x show "x \<in> image (case_prod Char) (UNIV \<times> UNIV)" by (cases x) auto
   29.12  qed
   29.13  
   29.14  lemma size_char [code, simp]:
   29.15 @@ -218,7 +218,7 @@
   29.16    "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
   29.17  
   29.18  lemma enum_char_product_enum_nibble:
   29.19 -  "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
   29.20 +  "(Enum.enum :: char list) = map (case_prod Char) (List.product Enum.enum Enum.enum)"
   29.21    by (simp add: enum_char_def enum_nibble_def)
   29.22  
   29.23  instance proof
    30.1 --- a/src/HOL/Transitive_Closure.thy	Thu Aug 27 13:07:45 2015 +0200
    30.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Aug 27 21:19:48 2015 +0200
    30.3 @@ -169,8 +169,9 @@
    30.4  
    30.5  lemma rtrancl_Int_subset: "[| Id \<subseteq> s; (r^* \<inter> s) O r \<subseteq> s|] ==> r^* \<subseteq> s"
    30.6    apply (rule subsetI)
    30.7 -  apply (rule_tac p="x" in PairE, clarify)
    30.8 -  apply (erule rtrancl_induct, auto) 
    30.9 +  apply auto
   30.10 +  apply (erule rtrancl_induct)
   30.11 +  apply auto
   30.12    done
   30.13  
   30.14  lemma converse_rtranclp_into_rtranclp:
   30.15 @@ -409,10 +410,9 @@
   30.16  
   30.17  lemma trancl_Int_subset: "[| r \<subseteq> s; (r^+ \<inter> s) O r \<subseteq> s|] ==> r^+ \<subseteq> s"
   30.18    apply (rule subsetI)
   30.19 -  apply (rule_tac p = x in PairE)
   30.20 -  apply clarify
   30.21 +  apply auto
   30.22    apply (erule trancl_induct)
   30.23 -   apply auto
   30.24 +  apply auto
   30.25    done
   30.26  
   30.27  lemma trancl_unfold: "r^+ = r Un r^+ O r"