prod_case as canonical name for product type eliminator
authorhaftmann
Tue Oct 13 09:21:15 2015 +0200 (2015-10-13)
changeset 61424c3658c18b7bc
parent 61423 9b6a0fb85fa3
child 61425 fb95d06fb21f
prod_case as canonical name for product type eliminator
NEWS
src/Doc/Datatypes/Datatypes.thy
src/Doc/Isar_Ref/Generic.thy
src/Doc/Logics/document/HOL.tex
src/Doc/Main/Main_Doc.thy
src/Doc/Tutorial/Types/Pairs.thy
src/HOL/BNF_Def.thy
src/HOL/BNF_Greatest_Fixpoint.thy
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/DefiniteAssignmentCorrect.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/State.thy
src/HOL/Cardinals/Bounded_Set.thy
src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/HOLCF/Fix.thy
src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
src/HOL/HOLCF/Product_Cpo.thy
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/holcf_library.ML
src/HOL/HOLCF/ex/Domain_Proofs.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hoare/hoare_syntax.ML
src/HOL/Hoare/hoare_tac.ML
src/HOL/Induct/Com.thy
src/HOL/Library/Code_Real_Approx_By_Float.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Groups_Big_Fun.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Order.thy
src/HOL/Library/Permutations.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Stream.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Library/old_recdef.ML
src/HOL/MicroJava/Comp/AuxLemmas.thy
src/HOL/MicroJava/DFA/Listn.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nominal/nominal_induct.ML
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/ex/Measure_Not_CCC.thy
src/HOL/Probability/measurable.ML
src/HOL/Product_Type.thy
src/HOL/Relation.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/SMT_Examples/boogie.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/set_comprehension_pointfree.ML
src/HOL/Tools/split_rule.ML
src/HOL/Transitive_Closure.thy
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/Extend.thy
src/HOL/Wellfounded.thy
src/HOL/Word/Bool_List_Representation.thy
src/HOL/Word/Word.thy
src/HOL/ex/FinFunPred.thy
src/HOL/ex/Gauge_Integration.thy
src/HOL/ex/Normalization_by_Evaluation.thy
     1.1 --- a/NEWS	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/NEWS	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -229,6 +229,52 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Combinator to represent case distinction on products is named "case_prod",
     1.8 +uniformly, discontinuing any input aliasses.  Very popular theorem aliasses
     1.9 +have been retained.
    1.10 +Consolidated facts:
    1.11 +  PairE ~> prod.exhaust
    1.12 +  Pair_eq ~> prod.inject
    1.13 +  pair_collapse ~> prod.collapse
    1.14 +  Pair_fst_snd_eq ~> prod_eq_iff
    1.15 +  split_twice ~> prod.case_distrib
    1.16 +  split_weak_cong ~> prod.case_cong_weak
    1.17 +  split_split ~> prod.split
    1.18 +  split_split_asm ~> prod.split_asm
    1.19 +  splitI ~> case_prodI
    1.20 +  splitD ~> case_prodD
    1.21 +  splitI2 ~> case_prodI2
    1.22 +  splitI2' ~> case_prodI2'
    1.23 +  splitE ~> case_prodE
    1.24 +  splitE' ~> case_prodE'
    1.25 +  split_pair ~> case_prod_Pair
    1.26 +  split_eta ~> case_prod_eta
    1.27 +  split_comp ~> case_prod_comp
    1.28 +  mem_splitI ~> mem_case_prodI
    1.29 +  mem_splitI2 ~> mem_case_prodI2
    1.30 +  mem_splitE ~> mem_case_prodE
    1.31 +  The_split ~> The_case_prod
    1.32 +  cond_split_eta ~> cond_case_prod_eta
    1.33 +  Collect_split_in_rel_leE ~> Collect_case_prod_in_rel_leE
    1.34 +  Collect_split_in_rel_leI ~> Collect_case_prod_in_rel_leI
    1.35 +  in_rel_Collect_split_eq ~> in_rel_Collect_case_prod_eq
    1.36 +  Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD
    1.37 +  Collect_split_Grp_inD ~> Collect_case_prod_Grp_in
    1.38 +  Domain_Collect_split ~> Domain_Collect_case_prod
    1.39 +  Image_Collect_split ~> Image_Collect_case_prod
    1.40 +  Range_Collect_split ~> Range_Collect_case_prod
    1.41 +  Eps_split ~> Eps_case_prod
    1.42 +  Eps_split_eq ~> Eps_case_prod_eq
    1.43 +  split_rsp ~> case_prod_rsp
    1.44 +  curry_split ~> curry_case_prod
    1.45 +  split_curry ~> case_prod_curry
    1.46 +Changes in structure HOLogic:
    1.47 +  split_const ~> case_prod_const
    1.48 +  mk_split ~> mk_case_prod
    1.49 +  mk_psplits ~> mk_ptupleabs
    1.50 +  strip_psplits ~> strip_ptupleabs
    1.51 +INCOMPATIBILITY.
    1.52 +
    1.53  * Commands 'inductive' and 'inductive_set' work better when names for
    1.54  intro rules are omitted: the "cases" and "induct" rules no longer
    1.55  declare empty case_names, but no case_names at all. This allows to use
    1.56 @@ -247,14 +293,6 @@
    1.57  constant and its defining fact become qualified, e.g. Option.is_none and
    1.58  Option.is_none_def. Occasional INCOMPATIBILITY in applications.
    1.59  
    1.60 -* Combinator to represent case distinction on products is named "uncurry",
    1.61 -with "split" and "prod_case" retained as input abbreviations.
    1.62 -Hence, the "uncurry"-expressions are printed the following way:
    1.63 -a) fully applied "uncurry f p": explicit case-expression;
    1.64 -b) partially applied "uncurry f": explicit paired abstraction;
    1.65 -c) unapplied "uncurry": as it is.
    1.66 -INCOMPATIBILITY.
    1.67 -
    1.68  * Some old and rarely used ASCII replacement syntax has been removed.
    1.69  INCOMPATIBILITY, standard syntax with symbols should be used instead.
    1.70  The subsequent commands help to reproduce the old forms, e.g. to
     2.1 --- a/src/Doc/Datatypes/Datatypes.thy	Tue Oct 13 09:21:14 2015 +0200
     2.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Tue Oct 13 09:21:15 2015 +0200
     2.3 @@ -2775,12 +2775,12 @@
     2.4      next
     2.5        fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
     2.6        show "rel_fn R =
     2.7 -            (BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn fst))\<inverse>\<inverse> OO
     2.8 -             BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
     2.9 +            (BNF_Def.Grp {x. set_fn x \<subseteq> {(x, y). R x y}} (map_fn fst))\<inverse>\<inverse> OO
    2.10 +             BNF_Def.Grp {x. set_fn x \<subseteq> {(x, y). R x y}} (map_fn snd)"
    2.11          unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
    2.12          apply transfer
    2.13          unfolding rel_fun_def subset_iff image_iff
    2.14 -        by auto (force, metis pair_collapse)
    2.15 +        by auto (force, metis prod.collapse)
    2.16      qed
    2.17  
    2.18  text {* \blankline *}
     3.1 --- a/src/Doc/Isar_Ref/Generic.thy	Tue Oct 13 09:21:14 2015 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Tue Oct 13 09:21:15 2015 +0200
     3.3 @@ -1130,9 +1130,9 @@
     3.4    @{text [display] "?P (if ?Q ?x ?y) \<longleftrightarrow> (?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y)"}
     3.5  
     3.6    Another example is the elimination operator for Cartesian products
     3.7 -  (which happens to be called @{text split} in Isabelle/HOL:
     3.8 +  (which happens to be called @{const case_prod} in Isabelle/HOL:
     3.9  
    3.10 -  @{text [display] "?P (split ?f ?p) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?P (f a b))"}
    3.11 +  @{text [display] "?P (case_prod ?f ?p) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?P (f a b))"}
    3.12  
    3.13    For technical reasons, there is a distinction between case splitting
    3.14    in the conclusion and in the premises of a subgoal.  The former is
     4.1 --- a/src/Doc/Logics/document/HOL.tex	Tue Oct 13 09:21:14 2015 +0200
     4.2 +++ b/src/Doc/Logics/document/HOL.tex	Tue Oct 13 09:21:15 2015 +0200
     4.3 @@ -1013,22 +1013,22 @@
     4.4          $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
     4.5          & general sum of sets
     4.6  \end{constants}
     4.7 -%\tdx{fst_def}      fst p     == @a. ? b. p = (a,b)
     4.8 -%\tdx{snd_def}      snd p     == @b. ? a. p = (a,b)
     4.9 -%\tdx{split_def}    split c p == c (fst p) (snd p)
    4.10 +%\tdx{fst_def}      fst p         == @a. ? b. p = (a,b)
    4.11 +%\tdx{snd_def}      snd p         == @b. ? a. p = (a,b)
    4.12 +%\tdx{split_def}    case_prod c p == c (fst p) (snd p)
    4.13  \begin{ttbox}\makeatletter
    4.14  \tdx{Sigma_def}    Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}
    4.15  
    4.16 -\tdx{Pair_eq}      ((a,b) = (a',b')) = (a=a' & b=b')
    4.17 +\tdx{prod.inject}      ((a,b) = (a',b')) = (a=a' & b=b')
    4.18  \tdx{Pair_inject}  [| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R
    4.19 -\tdx{PairE}        [| !!x y. p = (x,y) ==> Q |] ==> Q
    4.20 +\tdx{prod.exhaust}        [| !!x y. p = (x,y) ==> Q |] ==> Q
    4.21  
    4.22  \tdx{fst_conv}     fst (a,b) = a
    4.23  \tdx{snd_conv}     snd (a,b) = b
    4.24  \tdx{surjective_pairing}  p = (fst p,snd p)
    4.25  
    4.26 -\tdx{split}        split c (a,b) = c a b
    4.27 -\tdx{split_split}  R(split c p) = (! x y. p = (x,y) --> R(c x y))
    4.28 +\tdx{split}        case_prod c (a,b) = c a b
    4.29 +\tdx{prod.split}  R(case_prod c p) = (! x y. p = (x,y) --> R(c x y))
    4.30  
    4.31  \tdx{SigmaI}    [| a:A;  b:B a |] ==> (a,b) : Sigma A B
    4.32  
    4.33 @@ -1059,8 +1059,8 @@
    4.34  \begin{eqnarray*}
    4.35  \hbox{\tt\%($x$,$y$,$z$).\ $t$} 
    4.36     & \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\
    4.37 -   & \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\
    4.38 -   & \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))}
    4.39 +   & \leadsto & \hbox{\tt case_prod(\%$x$.\%($y$,$z$).\ $t$)}\\
    4.40 +   & \leadsto & \hbox{\tt case_prod(\%$x$.\ case_prod(\%$y$ $z$.\ $t$))}
    4.41  \end{eqnarray*}
    4.42  The reverse translation is performed upon printing.
    4.43  \begin{warn}
     5.1 --- a/src/Doc/Main/Main_Doc.thy	Tue Oct 13 09:21:14 2015 +0200
     5.2 +++ b/src/Doc/Main/Main_Doc.thy	Tue Oct 13 09:21:15 2015 +0200
     5.3 @@ -218,7 +218,7 @@
     5.4  @{const Pair} & @{typeof Pair}\\
     5.5  @{const fst} & @{typeof fst}\\
     5.6  @{const snd} & @{typeof snd}\\
     5.7 -@{const split} & @{typeof split}\\
     5.8 +@{const case_prod} & @{typeof case_prod}\\
     5.9  @{const curry} & @{typeof curry}\\
    5.10  @{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\
    5.11  \end{supertabular}
    5.12 @@ -227,7 +227,7 @@
    5.13  
    5.14  \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
    5.15  @{term"Pair a b"} & @{term[source]"Pair a b"}\\
    5.16 -@{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\
    5.17 +@{term"case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
    5.18  @{term"A <*> B"} &  @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$)
    5.19  \end{tabular}
    5.20  
     6.1 --- a/src/Doc/Tutorial/Types/Pairs.thy	Tue Oct 13 09:21:14 2015 +0200
     6.2 +++ b/src/Doc/Tutorial/Types/Pairs.thy	Tue Oct 13 09:21:15 2015 +0200
     6.3 @@ -36,7 +36,7 @@
     6.4  instead of @{text"\<lambda>(x,y). x+y"}.  These terms are distinct even though they
     6.5  denote the same function.
     6.6  
     6.7 -Internally, @{term"%(x,y). t"} becomes @{text"split (\<lambda>x y. t)"}, where
     6.8 +Internally, @{term"%(x,y). t"} becomes @{text"case_prod (\<lambda>x y. t)"}, where
     6.9  \cdx{split} is the uncurrying function of type @{text"('a \<Rightarrow> 'b
    6.10  \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"} defined as
    6.11  \begin{center}
    6.12 @@ -71,13 +71,13 @@
    6.13  @{thm split_conv[no_vars]} and @{thm fst_conv[no_vars]}.  
    6.14  To reason about tuple patterns requires some way of
    6.15  converting a variable of product type into a pair.
    6.16 -In case of a subterm of the form @{term"split f p"} this is easy: the split
    6.17 -rule @{thm[source]split_split} replaces @{term p} by a pair:%
    6.18 +In case of a subterm of the form @{term"case_prod f p"} this is easy: the split
    6.19 +rule @{thm[source]prod.split} replaces @{term p} by a pair:%
    6.20  \index{*split (method)}
    6.21  *}
    6.22  
    6.23  lemma "(\<lambda>(x,y).y) p = snd p"
    6.24 -apply(split split_split)
    6.25 +apply(split prod.split)
    6.26  
    6.27  txt{*
    6.28  @{subgoals[display,indent=0]}
    6.29 @@ -87,7 +87,7 @@
    6.30  (*<*)
    6.31  by simp
    6.32  lemma "(\<lambda>(x,y).y) p = snd p"(*>*)
    6.33 -by(simp split: split_split)
    6.34 +by(simp split: prod.split)
    6.35  
    6.36  text{*
    6.37  Let us look at a second example:
    6.38 @@ -102,30 +102,30 @@
    6.39  can be split as above. The same is true for paired set comprehension:
    6.40  *}
    6.41  
    6.42 -(*<*)by(simp split: split_split)(*>*)
    6.43 +(*<*)by(simp split: prod.split)(*>*)
    6.44  lemma "p \<in> {(x,y). x=y} \<longrightarrow> fst p = snd p"
    6.45  apply simp
    6.46  
    6.47  txt{*
    6.48  @{subgoals[display,indent=0]}
    6.49 -Again, simplification produces a term suitable for @{thm[source]split_split}
    6.50 +Again, simplification produces a term suitable for @{thm[source]prod.split}
    6.51  as above. If you are worried about the strange form of the premise:
    6.52 -@{text"split (op =)"} is short for @{term"\<lambda>(x,y). x=y"}.
    6.53 +@{text"case_prod (op =)"} is short for @{term"\<lambda>(x,y). x=y"}.
    6.54  The same proof procedure works for
    6.55  *}
    6.56  
    6.57 -(*<*)by(simp split: split_split)(*>*)
    6.58 +(*<*)by(simp split: prod.split)(*>*)
    6.59  lemma "p \<in> {(x,y). x=y} \<Longrightarrow> fst p = snd p"
    6.60  
    6.61  txt{*\noindent
    6.62 -except that we now have to use @{thm[source]split_split_asm}, because
    6.63 +except that we now have to use @{thm[source]prod.split_asm}, because
    6.64  @{term split} occurs in the assumptions.
    6.65  
    6.66  However, splitting @{term split} is not always a solution, as no @{term split}
    6.67  may be present in the goal. Consider the following function:
    6.68  *}
    6.69  
    6.70 -(*<*)by(simp split: split_split_asm)(*>*)
    6.71 +(*<*)by(simp split: prod.split_asm)(*>*)
    6.72  primrec swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a" where "swap (x,y) = (y,x)"
    6.73  
    6.74  text{*\noindent
     7.1 --- a/src/HOL/BNF_Def.thy	Tue Oct 13 09:21:14 2015 +0200
     7.2 +++ b/src/HOL/BNF_Def.thy	Tue Oct 13 09:21:15 2015 +0200
     7.3 @@ -15,7 +15,7 @@
     7.4    "bnf" :: thy_goal
     7.5  begin
     7.6  
     7.7 -lemma Collect_splitD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
     7.8 +lemma Collect_case_prodD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
     7.9    by auto
    7.10  
    7.11  inductive
    7.12 @@ -61,7 +61,7 @@
    7.13  lemma predicate2_transferD:
    7.14     "\<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>
    7.15     P (fst a) (fst b) \<longleftrightarrow> Q (snd a) (snd b)"
    7.16 -  unfolding rel_fun_def by (blast dest!: Collect_splitD)
    7.17 +  unfolding rel_fun_def by (blast dest!: Collect_case_prodD)
    7.18  
    7.19  definition collect where
    7.20    "collect F x = (\<Union>f \<in> F. f x)"
    7.21 @@ -131,10 +131,10 @@
    7.22  lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
    7.23    unfolding Grp_def by auto
    7.24  
    7.25 -lemma Collect_split_Grp_eqD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
    7.26 +lemma Collect_case_prod_Grp_eqD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
    7.27    unfolding Grp_def comp_def by auto
    7.28  
    7.29 -lemma Collect_split_Grp_inD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> fst z \<in> A"
    7.30 +lemma Collect_case_prod_Grp_in: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> fst z \<in> A"
    7.31    unfolding Grp_def comp_def by auto
    7.32  
    7.33  definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
     8.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Tue Oct 13 09:21:14 2015 +0200
     8.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Tue Oct 13 09:21:15 2015 +0200
     8.3 @@ -82,13 +82,13 @@
     8.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})"
     8.5    by blast
     8.6  
     8.7 -lemma in_rel_Collect_split_eq: "in_rel (Collect (case_prod X)) = X"
     8.8 +lemma in_rel_Collect_case_prod_eq: "in_rel (Collect (case_prod X)) = X"
     8.9    unfolding fun_eq_iff by auto
    8.10  
    8.11 -lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
    8.12 +lemma Collect_case_prod_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
    8.13    by auto
    8.14  
    8.15 -lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
    8.16 +lemma Collect_case_prod_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
    8.17    by force
    8.18  
    8.19  lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
     9.1 --- a/src/HOL/Bali/AxCompl.thy	Tue Oct 13 09:21:14 2015 +0200
     9.2 +++ b/src/HOL/Bali/AxCompl.thy	Tue Oct 13 09:21:15 2015 +0200
     9.3 @@ -1446,7 +1446,7 @@
     9.4  
     9.5  lemma MGF_simult_Methd: "wf_prog G \<Longrightarrow> 
     9.6     G,({}::state triple set)|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) 
     9.7 -   ` Collect (split (is_methd G)) "
     9.8 +   ` Collect (case_prod (is_methd G)) "
     9.9  apply (frule finite_is_methd [OF wf_ws_prog])
    9.10  apply (rule MGF_simult_Methd_lemma)
    9.11  apply  assumption
    10.1 --- a/src/HOL/Bali/AxSem.thy	Tue Oct 13 09:21:14 2015 +0200
    10.2 +++ b/src/HOL/Bali/AxSem.thy	Tue Oct 13 09:21:15 2015 +0200
    10.3 @@ -969,7 +969,7 @@
    10.4  done
    10.5  
    10.6  lemma ax_methods_spec: 
    10.7 -"\<lbrakk>G,(A::'a triple set)|\<turnstile>split f ` ms; (C,sig) \<in> ms\<rbrakk>\<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)"
    10.8 +"\<lbrakk>G,(A::'a triple set)|\<turnstile>case_prod f ` ms; (C,sig) \<in> ms\<rbrakk>\<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)"
    10.9  apply (erule ax_derivs.weaken)
   10.10  apply (force del: image_eqI intro: rev_image_eqI)
   10.11  done
   10.12 @@ -977,7 +977,7 @@
   10.13  (* this version is used to avoid using the cut rule *)
   10.14  lemma ax_finite_pointwise_lemma [rule_format]: "\<lbrakk>F \<subseteq> ms; finite ms\<rbrakk> \<Longrightarrow>  
   10.15    ((\<forall>(C,sig)\<in>F. G,(A::'a triple set)\<turnstile>(f C sig::'a triple)) \<longrightarrow> (\<forall>(C,sig)\<in>ms. G,A\<turnstile>(g C sig::'a triple))) \<longrightarrow>  
   10.16 -      G,A|\<turnstile>split f ` F \<longrightarrow> G,A|\<turnstile>split g ` F"
   10.17 +      G,A|\<turnstile>case_prod f ` F \<longrightarrow> G,A|\<turnstile>case_prod g ` F"
   10.18  apply (frule (1) finite_subset)
   10.19  apply (erule rev_mp)
   10.20  apply (erule thin_rl)
    11.1 --- a/src/HOL/Bali/Basis.thy	Tue Oct 13 09:21:14 2015 +0200
    11.2 +++ b/src/HOL/Bali/Basis.thy	Tue Oct 13 09:21:15 2015 +0200
    11.3 @@ -16,7 +16,7 @@
    11.4  declare if_weak_cong [cong del] option.case_cong_weak [cong del]
    11.5  declare length_Suc_conv [iff]
    11.6  
    11.7 -lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
    11.8 +lemma Collect_split_eq: "{p. P (case_prod f p)} = {(a,b). P (f a b)}"
    11.9    by auto
   11.10  
   11.11  lemma subset_insertD: "A \<subseteq> insert x B \<Longrightarrow> A \<subseteq> B \<and> x \<notin> A \<or> (\<exists>B'. A = insert x B' \<and> B' \<subseteq> B)"
    12.1 --- a/src/HOL/Bali/DeclConcepts.thy	Tue Oct 13 09:21:14 2015 +0200
    12.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Tue Oct 13 09:21:15 2015 +0200
    12.3 @@ -2178,14 +2178,14 @@
    12.4  apply (subst fields_rec, assumption)
    12.5  apply clarify
    12.6  apply (simp only: map_of_append)
    12.7 -apply (case_tac "table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn") 
    12.8 +apply (case_tac "table_of (map (case_prod (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn") 
    12.9  apply   (force intro:rtrancl_into_rtrancl2 simp add: map_add_def)
   12.10  
   12.11  apply   (frule_tac fd="Ca" in fields_norec)
   12.12  apply     assumption
   12.13  apply     blast
   12.14  apply   (frule table_of_fieldsD)  
   12.15 -apply   (frule_tac n="table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c))"
   12.16 +apply   (frule_tac n="table_of (map (case_prod (\<lambda>fn. Pair (fn, Ca))) (cfields c))"
   12.17                and  m="table_of (if Ca = Object then [] else fields G (super c))"
   12.18           in map_add_find_right)
   12.19  apply   (case_tac "efn")
   12.20 @@ -2272,9 +2272,9 @@
   12.21  done
   12.22  
   12.23  lemma finite_is_methd: 
   12.24 - "ws_prog G \<Longrightarrow> finite (Collect (split (is_methd G)))"
   12.25 + "ws_prog G \<Longrightarrow> finite (Collect (case_prod (is_methd G)))"
   12.26  apply (unfold is_methd_def)
   12.27 -apply (subst SetCompr_Sigma_eq)
   12.28 +apply (subst Collect_case_prod_Sigma)
   12.29  apply (rule finite_is_class [THEN finite_SigmaI])
   12.30  apply (simp only: mem_Collect_eq)
   12.31  apply (fold dom_def)
    13.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Oct 13 09:21:14 2015 +0200
    13.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Oct 13 09:21:15 2015 +0200
    13.3 @@ -3962,7 +3962,7 @@
    13.4          moreover
    13.5          from upd normal_s2
    13.6          have "{vn} \<subseteq> dom (locals (store (assign upd v s2)))"
    13.7 -          by (auto simp add: assign_def Let_def lvar_def upd split: split_split)
    13.8 +          by (auto simp add: assign_def Let_def lvar_def upd split: prod.split)
    13.9          ultimately
   13.10          show "nrm A \<subseteq> \<dots>"
   13.11            by (rule Un_least [elim_format]) (simp add: nrm_A)
    14.1 --- a/src/HOL/Bali/Example.thy	Tue Oct 13 09:21:14 2015 +0200
    14.2 +++ b/src/HOL/Bali/Example.thy	Tue Oct 13 09:21:15 2015 +0200
    14.3 @@ -1247,7 +1247,7 @@
    14.4  abbreviation "s9' == (Some (Xcpt (Std IndOutBound)), s8)"
    14.5  
    14.6  
    14.7 -declare Pair_eq [simp del]
    14.8 +declare prod.inject [simp del]
    14.9  schematic_goal exec_test: 
   14.10  "\<lbrakk>the (new_Addr (heap  s1)) = a;  
   14.11    the (new_Addr (heap ?s2)) = b;  
   14.12 @@ -1377,6 +1377,6 @@
   14.13  apply  (simp (no_asm_simp))
   14.14  apply (auto simp add: in_bounds_def)
   14.15  done
   14.16 -declare Pair_eq [simp]
   14.17 +declare prod.inject [simp]
   14.18  
   14.19  end
    15.1 --- a/src/HOL/Bali/State.thy	Tue Oct 13 09:21:14 2015 +0200
    15.2 +++ b/src/HOL/Bali/State.thy	Tue Oct 13 09:21:15 2015 +0200
    15.3 @@ -143,7 +143,7 @@
    15.4  definition
    15.5    fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
    15.6    "fields_table G C P =
    15.7 -    map_option type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
    15.8 +    map_option type \<circ> table_of (filter (case_prod P) (DeclConcepts.fields G C))"
    15.9  
   15.10  lemma fields_table_SomeI: 
   15.11  "\<lbrakk>table_of (DeclConcepts.fields G C) n = Some f; P n f\<rbrakk> 
    16.1 --- a/src/HOL/Cardinals/Bounded_Set.thy	Tue Oct 13 09:21:14 2015 +0200
    16.2 +++ b/src/HOL/Cardinals/Bounded_Set.thy	Tue Oct 13 09:21:15 2015 +0200
    16.3 @@ -50,7 +50,7 @@
    16.4      BNF_Def.Grp {a. set_bset a \<subseteq> {(a, b). R a b}} (map_bset snd)) a b" (is "?L \<longleftrightarrow> ?R")
    16.5  proof
    16.6    assume ?L
    16.7 -  def R' \<equiv> "the_inv set_bset (Collect (split R) \<inter> (set_bset a \<times> set_bset b)) :: ('a \<times> 'b) set['k]"
    16.8 +  def R' \<equiv> "the_inv set_bset (Collect (case_prod R) \<inter> (set_bset a \<times> set_bset b)) :: ('a \<times> 'b) set['k]"
    16.9      (is "the_inv set_bset ?L'")
   16.10    have "|?L'| <o natLeq +c |UNIV :: 'k set|"
   16.11      unfolding csum_def Field_natLeq
    17.1 --- a/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Tue Oct 13 09:21:14 2015 +0200
    17.2 +++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Tue Oct 13 09:21:15 2015 +0200
    17.3 @@ -1012,7 +1012,7 @@
    17.4  proof-
    17.5    have "?L = (n, (id \<oplus> root) ` cont (pick n))"
    17.6    unfolding cont_H image_comp map_sum.comp id_comp comp_assoc[symmetric]
    17.7 -  unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
    17.8 +  unfolding prod.inject apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
    17.9    by (rule root_H_root[OF n])
   17.10    moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
   17.11    ultimately show ?thesis by simp
    18.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Oct 13 09:21:14 2015 +0200
    18.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Oct 13 09:21:15 2015 +0200
    18.3 @@ -1129,7 +1129,7 @@
    18.4    by pat_completeness auto
    18.5  termination rsplit0 by (relation "measure num_size") simp_all
    18.6  
    18.7 -lemma rsplit0: "Inum bs ((split (CN 0)) (rsplit0 t)) = Inum bs t \<and> numbound0 (snd (rsplit0 t))"
    18.8 +lemma rsplit0: "Inum bs ((case_prod (CN 0)) (rsplit0 t)) = Inum bs t \<and> numbound0 (snd (rsplit0 t))"
    18.9  proof (induct t rule: rsplit0.induct)
   18.10    case (2 a b)
   18.11    let ?sa = "rsplit0 a"
   18.12 @@ -1140,8 +1140,8 @@
   18.13    let ?tb = "snd ?sb"
   18.14    from 2 have nb: "numbound0 (snd(rsplit0 (Add a b)))"
   18.15      by (cases "rsplit0 a") (auto simp add: Let_def split_def)
   18.16 -  have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) =
   18.17 -    Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)"
   18.18 +  have "Inum bs ((case_prod (CN 0)) (rsplit0 (Add a b))) =
   18.19 +    Inum bs ((case_prod (CN 0)) ?sa)+Inum bs ((case_prod (CN 0)) ?sb)"
   18.20      by (simp add: Let_def split_def algebra_simps)
   18.21    also have "\<dots> = Inum bs a + Inum bs b"
   18.22      using 2 by (cases "rsplit0 a") auto
   18.23 @@ -1180,38 +1180,38 @@
   18.24    "neq c t = (if c = 0 then (NEq t) else if c > 0 then (NEq (CN 0 c t))
   18.25      else (NEq (CN 0 (-c) (Neg t))))"
   18.26  
   18.27 -lemma lt: "numnoabs t \<Longrightarrow> Ifm bs (split lt (rsplit0 t)) =
   18.28 -  Ifm bs (Lt t) \<and> isrlfm (split lt (rsplit0 t))"
   18.29 +lemma lt: "numnoabs t \<Longrightarrow> Ifm bs (case_prod lt (rsplit0 t)) =
   18.30 +  Ifm bs (Lt t) \<and> isrlfm (case_prod lt (rsplit0 t))"
   18.31    using rsplit0[where bs = "bs" and t="t"]
   18.32    by (auto simp add: lt_def split_def, cases "snd(rsplit0 t)", auto,
   18.33      rename_tac nat a b, case_tac "nat", auto)
   18.34  
   18.35 -lemma le: "numnoabs t \<Longrightarrow> Ifm bs (split le (rsplit0 t)) =
   18.36 -  Ifm bs (Le t) \<and> isrlfm (split le (rsplit0 t))"
   18.37 +lemma le: "numnoabs t \<Longrightarrow> Ifm bs (case_prod le (rsplit0 t)) =
   18.38 +  Ifm bs (Le t) \<and> isrlfm (case_prod le (rsplit0 t))"
   18.39    using rsplit0[where bs = "bs" and t="t"]
   18.40    by (auto simp add: le_def split_def, cases "snd(rsplit0 t)", auto,
   18.41      rename_tac nat a b, case_tac "nat", auto)
   18.42  
   18.43 -lemma gt: "numnoabs t \<Longrightarrow> Ifm bs (split gt (rsplit0 t)) =
   18.44 -  Ifm bs (Gt t) \<and> isrlfm (split gt (rsplit0 t))"
   18.45 +lemma gt: "numnoabs t \<Longrightarrow> Ifm bs (case_prod gt (rsplit0 t)) =
   18.46 +  Ifm bs (Gt t) \<and> isrlfm (case_prod gt (rsplit0 t))"
   18.47    using rsplit0[where bs = "bs" and t="t"]
   18.48    by (auto simp add: gt_def split_def, cases "snd(rsplit0 t)", auto,
   18.49      rename_tac nat a b, case_tac "nat", auto)
   18.50  
   18.51 -lemma ge: "numnoabs t \<Longrightarrow> Ifm bs (split ge (rsplit0 t)) =
   18.52 -  Ifm bs (Ge t) \<and> isrlfm (split ge (rsplit0 t))"
   18.53 +lemma ge: "numnoabs t \<Longrightarrow> Ifm bs (case_prod ge (rsplit0 t)) =
   18.54 +  Ifm bs (Ge t) \<and> isrlfm (case_prod ge (rsplit0 t))"
   18.55    using rsplit0[where bs = "bs" and t="t"]
   18.56    by (auto simp add: ge_def split_def, cases "snd(rsplit0 t)", auto,
   18.57      rename_tac nat a b, case_tac "nat", auto)
   18.58  
   18.59 -lemma eq: "numnoabs t \<Longrightarrow> Ifm bs (split eq (rsplit0 t)) =
   18.60 -  Ifm bs (Eq t) \<and> isrlfm (split eq (rsplit0 t))"
   18.61 +lemma eq: "numnoabs t \<Longrightarrow> Ifm bs (case_prod eq (rsplit0 t)) =
   18.62 +  Ifm bs (Eq t) \<and> isrlfm (case_prod eq (rsplit0 t))"
   18.63    using rsplit0[where bs = "bs" and t="t"]
   18.64    by (auto simp add: eq_def split_def, cases "snd(rsplit0 t)", auto,
   18.65      rename_tac nat a b, case_tac "nat", auto)
   18.66  
   18.67 -lemma neq: "numnoabs t \<Longrightarrow> Ifm bs (split neq (rsplit0 t)) =
   18.68 -  Ifm bs (NEq t) \<and> isrlfm (split neq (rsplit0 t))"
   18.69 +lemma neq: "numnoabs t \<Longrightarrow> Ifm bs (case_prod neq (rsplit0 t)) =
   18.70 +  Ifm bs (NEq t) \<and> isrlfm (case_prod neq (rsplit0 t))"
   18.71    using rsplit0[where bs = "bs" and t="t"]
   18.72    by (auto simp add: neq_def split_def, cases "snd(rsplit0 t)", auto,
   18.73      rename_tac nat a b, case_tac "nat", auto)
   18.74 @@ -1228,12 +1228,12 @@
   18.75    "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
   18.76    "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
   18.77    "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))"
   18.78 -  "rlfm (Lt a) = split lt (rsplit0 a)"
   18.79 -  "rlfm (Le a) = split le (rsplit0 a)"
   18.80 -  "rlfm (Gt a) = split gt (rsplit0 a)"
   18.81 -  "rlfm (Ge a) = split ge (rsplit0 a)"
   18.82 -  "rlfm (Eq a) = split eq (rsplit0 a)"
   18.83 -  "rlfm (NEq a) = split neq (rsplit0 a)"
   18.84 +  "rlfm (Lt a) = case_prod lt (rsplit0 a)"
   18.85 +  "rlfm (Le a) = case_prod le (rsplit0 a)"
   18.86 +  "rlfm (Gt a) = case_prod gt (rsplit0 a)"
   18.87 +  "rlfm (Ge a) = case_prod ge (rsplit0 a)"
   18.88 +  "rlfm (Eq a) = case_prod eq (rsplit0 a)"
   18.89 +  "rlfm (NEq a) = case_prod neq (rsplit0 a)"
   18.90    "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
   18.91    "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
   18.92    "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
   18.93 @@ -2430,7 +2430,7 @@
   18.94      using uset_cong[OF lq YU U_l Y_l] by (simp only: split_def fst_conv snd_conv simpfm)
   18.95    also have "\<dots> = (Ifm (x#bs) ?res)"
   18.96      using evaldjf_ex[where ps="?Y" and bs = "x#bs" and f="simpfm \<circ> (usubst ?q)",symmetric]
   18.97 -    by (simp add: split_def pair_collapse)
   18.98 +    by (simp add: split_def prod.collapse)
   18.99    finally have lheq: "?lhs = Ifm bs (decr ?res)"
  18.100      using decr[OF nbth] by blast
  18.101    then have lr: "?lhs = ?rhs"
    19.1 --- a/src/HOL/Decision_Procs/MIR.thy	Tue Oct 13 09:21:14 2015 +0200
    19.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Tue Oct 13 09:21:15 2015 +0200
    19.3 @@ -5072,7 +5072,7 @@
    19.4      by (simp only: split_def fst_conv snd_conv) 
    19.5    also have "\<dots> = (Ifm (x#bs) ?ep)" 
    19.6      using evaldjf_ex[where ps="?Y" and bs = "x#bs" and f="\<upsilon> ?q",symmetric]
    19.7 -    by (simp only: split_def pair_collapse)
    19.8 +    by (simp only: split_def prod.collapse)
    19.9    also have "\<dots> = (Ifm bs (decr ?ep))" using decr[OF ep_nb] by blast
   19.10    finally have lr: "?lhs = ?rhs" by (simp only: ferrack01_def Let_def)
   19.11    from decr_qf[OF ep_nb] have "qfree (ferrack01 p)" by (simp only: Let_def ferrack01_def)
    20.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Oct 13 09:21:14 2015 +0200
    20.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Oct 13 09:21:15 2015 +0200
    20.3 @@ -2608,7 +2608,7 @@
    20.4  section \<open>First implementation : Naive by encoding all case splits locally\<close>
    20.5  
    20.6  definition "msubsteq c t d s a r =
    20.7 -  evaldjf (split conj)
    20.8 +  evaldjf (case_prod conj)
    20.9    [(let cd = c *\<^sub>p d
   20.10      in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
   20.11     (conj (Eq (CP c)) (NEq (CP d)), Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
   20.12 @@ -2626,7 +2626,7 @@
   20.13        in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
   20.14       (conj (Eq (CP c)) (NEq (CP d)), Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
   20.15       (conj (NEq (CP c)) (Eq (CP d)), Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
   20.16 -     (conj (Eq (CP c)) (Eq (CP d)), Eq r)]. bound0 (split conj x)"
   20.17 +     (conj (Eq (CP c)) (Eq (CP d)), Eq r)]. bound0 (case_prod conj x)"
   20.18      using lp by (simp add: Let_def t s)
   20.19    from evaldjf_bound0[OF th] show ?thesis
   20.20      by (simp add: msubsteq_def)
   20.21 @@ -2715,7 +2715,7 @@
   20.22  
   20.23  
   20.24  definition "msubstneq c t d s a r =
   20.25 -  evaldjf (split conj)
   20.26 +  evaldjf (case_prod conj)
   20.27    [(let cd = c *\<^sub>p d
   20.28      in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
   20.29     (conj (Eq (CP c)) (NEq (CP d)), NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
   20.30 @@ -2733,7 +2733,7 @@
   20.31       in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
   20.32      (conj (Eq (CP c)) (NEq (CP d)), NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
   20.33      (conj (NEq (CP c)) (Eq (CP d)), NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
   20.34 -    (conj (Eq (CP c)) (Eq (CP d)), NEq r)]. bound0 (split conj x)"
   20.35 +    (conj (Eq (CP c)) (Eq (CP d)), NEq r)]. bound0 (case_prod conj x)"
   20.36      using lp by (simp add: Let_def t s)
   20.37    from evaldjf_bound0[OF th] show ?thesis
   20.38      by (simp add: msubstneq_def)
   20.39 @@ -2821,7 +2821,7 @@
   20.40  qed
   20.41  
   20.42  definition "msubstlt c t d s a r =
   20.43 -  evaldjf (split conj)
   20.44 +  evaldjf (case_prod conj)
   20.45    [(let cd = c *\<^sub>p d
   20.46      in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
   20.47     (let cd = c *\<^sub>p d
   20.48 @@ -2847,7 +2847,7 @@
   20.49     (conj (lt (CP c)) (Eq (CP d)), Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
   20.50     (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)), Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
   20.51     (conj (lt (CP d)) (Eq (CP c)), Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
   20.52 -   (conj (Eq (CP c)) (Eq (CP d)), Lt r)]. bound0 (split conj x)"
   20.53 +   (conj (Eq (CP c)) (Eq (CP d)), Lt r)]. bound0 (case_prod conj x)"
   20.54      using lp by (simp add: Let_def t s lt_nb)
   20.55    from evaldjf_bound0[OF th] show ?thesis
   20.56      by (simp add: msubstlt_def)
   20.57 @@ -3027,7 +3027,7 @@
   20.58  qed
   20.59  
   20.60  definition "msubstle c t d s a r =
   20.61 -  evaldjf (split conj)
   20.62 +  evaldjf (case_prod conj)
   20.63     [(let cd = c *\<^sub>p d
   20.64       in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
   20.65      (let cd = c *\<^sub>p d
   20.66 @@ -3053,7 +3053,7 @@
   20.67      (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
   20.68      (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
   20.69      (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
   20.70 -    (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (split conj x)"
   20.71 +    (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (case_prod conj x)"
   20.72      using lp by (simp add: Let_def t s lt_nb)
   20.73    from evaldjf_bound0[OF th] show ?thesis
   20.74      by (simp add: msubstle_def)
    21.1 --- a/src/HOL/HOLCF/Fix.thy	Tue Oct 13 09:21:14 2015 +0200
    21.2 +++ b/src/HOL/HOLCF/Fix.thy	Tue Oct 13 09:21:15 2015 +0200
    21.3 @@ -178,15 +178,15 @@
    21.4    assumes step: "\<And>x y. P x y \<Longrightarrow> P (F\<cdot>x) (G\<cdot>y)"
    21.5    shows "P (fix\<cdot>F) (fix\<cdot>G)"
    21.6  proof -
    21.7 -  from adm have adm': "adm (split P)"
    21.8 +  from adm have adm': "adm (case_prod P)"
    21.9      unfolding split_def .
   21.10    have "\<And>i. P (iterate i\<cdot>F\<cdot>\<bottom>) (iterate i\<cdot>G\<cdot>\<bottom>)"
   21.11      by (induct_tac i, simp add: base, simp add: step)
   21.12 -  hence "\<And>i. split P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
   21.13 +  hence "\<And>i. case_prod P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
   21.14      by simp
   21.15 -  hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
   21.16 +  hence "case_prod P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
   21.17      by - (rule admD [OF adm'], simp, assumption)
   21.18 -  hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
   21.19 +  hence "case_prod P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
   21.20      by (simp add: lub_Pair)
   21.21    hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
   21.22      by simp
    22.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Tue Oct 13 09:21:14 2015 +0200
    22.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Tue Oct 13 09:21:15 2015 +0200
    22.3 @@ -362,7 +362,7 @@
    22.4  fun Seq_Finite_induct_tac i = erule Seq_Finite_ind i
    22.5                                THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
    22.6  
    22.7 -fun pair_tac s = rule_tac p",s)] PairE
    22.8 +fun pair_tac s = rule_tac p",s)] prod.exhaust
    22.9                            THEN' hyp_subst_tac THEN' Simp_tac;
   22.10  *)
   22.11  (* induction on a sequence of pairs with pairsplitting and simplification *)
   22.12 @@ -1102,7 +1102,7 @@
   22.13    THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));
   22.14  
   22.15  fun pair_tac ctxt s =
   22.16 -  Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), s)] [] @{thm PairE}
   22.17 +  Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), s)] [] @{thm prod.exhaust}
   22.18    THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;
   22.19  
   22.20  (* induction on a sequence of pairs with pairsplitting and simplification *)
    23.1 --- a/src/HOL/HOLCF/Product_Cpo.thy	Tue Oct 13 09:21:14 2015 +0200
    23.2 +++ b/src/HOL/HOLCF/Product_Cpo.thy	Tue Oct 13 09:21:15 2015 +0200
    23.3 @@ -169,7 +169,7 @@
    23.4  lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
    23.5  by simp
    23.6  
    23.7 -lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
    23.8 +lemma split_strict [simp]: "case_prod f \<bottom> = f \<bottom> \<bottom>"
    23.9  unfolding split_def by simp
   23.10  
   23.11  subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
   23.12 @@ -235,7 +235,7 @@
   23.13    have "cont (\<lambda>(x, y). f (x, y))"
   23.14      by (intro cont2cont_case_prod f1 f2 cont2cont)
   23.15    thus "cont f"
   23.16 -    by (simp only: split_eta)
   23.17 +    by (simp only: case_prod_eta)
   23.18  qed
   23.19  
   23.20  lemma prod_cont_iff:
    24.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Oct 13 09:21:14 2015 +0200
    24.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Oct 13 09:21:15 2015 +0200
    24.3 @@ -688,7 +688,7 @@
    24.4          val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy
    24.5          val start_rules =
    24.6              @{thms lub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
    24.7 -            @ @{thms pair_collapse split_def}
    24.8 +            @ @{thms prod.collapse split_def}
    24.9              @ map_apply_thms @ map_ID_thms
   24.10          val rules0 =
   24.11              @{thms iterate_0 Pair_strict} @ take_0_thms
    25.1 --- a/src/HOL/HOLCF/Tools/holcf_library.ML	Tue Oct 13 09:21:14 2015 +0200
    25.2 +++ b/src/HOL/HOLCF/Tools/holcf_library.ML	Tue Oct 13 09:21:15 2015 +0200
    25.3 @@ -149,7 +149,7 @@
    25.4  fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
    25.5    | lambda_tuple (v::[]) rhs = Term.lambda v rhs
    25.6    | lambda_tuple (v::vs) rhs =
    25.7 -      HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs))
    25.8 +      HOLogic.mk_case_prod (Term.lambda v (lambda_tuple vs rhs))
    25.9  
   25.10  
   25.11  (*** Lifted cpo type ***)
    26.1 --- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Oct 13 09:21:14 2015 +0200
    26.2 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Oct 13 09:21:15 2015 +0200
    26.3 @@ -465,7 +465,7 @@
    26.4    "(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
    26.5      = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
    26.6  apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
    26.7 -apply (simp only: map_apply_thms pair_collapse)
    26.8 +apply (simp only: map_apply_thms prod.collapse)
    26.9  apply (simp only: fix_def2)
   26.10  apply (rule lub_eq)
   26.11  apply (rule nat.induct)
    27.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Oct 13 09:21:14 2015 +0200
    27.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Oct 13 09:21:15 2015 +0200
    27.3 @@ -546,10 +546,10 @@
    27.4  lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
    27.5    by simp
    27.6  
    27.7 -lemma Eps_split: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
    27.8 +lemma Eps_case_prod: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
    27.9    by (simp add: split_def)
   27.10  
   27.11 -lemma Eps_split_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
   27.12 +lemma Eps_case_prod_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
   27.13    by blast
   27.14  
   27.15  
    28.1 --- a/src/HOL/Hoare/hoare_syntax.ML	Tue Oct 13 09:21:14 2015 +0200
    28.2 +++ b/src/HOL/Hoare/hoare_syntax.ML	Tue Oct 13 09:21:15 2015 +0200
    28.3 @@ -28,7 +28,7 @@
    28.4  
    28.5  fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
    28.6    | mk_abstuple (x :: xs) body =
    28.7 -      Syntax.const @{const_syntax uncurry} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
    28.8 +      Syntax.const @{const_syntax case_prod} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
    28.9  
   28.10  fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
   28.11    | mk_fbody x e (y :: xs) =
   28.12 @@ -82,21 +82,21 @@
   28.13  local
   28.14  
   28.15  fun dest_abstuple
   28.16 -      (Const (@{const_syntax uncurry}, _) $ Abs (v, _, body)) =
   28.17 +      (Const (@{const_syntax case_prod}, _) $ Abs (v, _, body)) =
   28.18          subst_bound (Syntax.free v, dest_abstuple body)
   28.19    | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
   28.20    | dest_abstuple tm = tm;
   28.21  
   28.22 -fun abs2list (Const (@{const_syntax uncurry}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
   28.23 +fun abs2list (Const (@{const_syntax case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
   28.24    | abs2list (Abs (x, T, _)) = [Free (x, T)]
   28.25    | abs2list _ = [];
   28.26  
   28.27 -fun mk_ts (Const (@{const_syntax uncurry}, _) $ Abs (_, _, t)) = mk_ts t
   28.28 +fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (_, _, t)) = mk_ts t
   28.29    | mk_ts (Abs (_, _, t)) = mk_ts t
   28.30    | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
   28.31    | mk_ts t = [t];
   28.32  
   28.33 -fun mk_vts (Const (@{const_syntax uncurry},_) $ Abs (x, _, t)) =
   28.34 +fun mk_vts (Const (@{const_syntax case_prod},_) $ Abs (x, _, t)) =
   28.35        (Syntax.free x :: abs2list t, mk_ts t)
   28.36    | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
   28.37    | mk_vts _ = raise Match;
   28.38 @@ -106,7 +106,7 @@
   28.39        if t = Bound i then find_ch vts (i - 1) xs
   28.40        else (true, (v, subst_bounds (xs, t)));
   28.41  
   28.42 -fun is_f (Const (@{const_syntax uncurry}, _) $ Abs _) = true
   28.43 +fun is_f (Const (@{const_syntax case_prod}, _) $ Abs _) = true
   28.44    | is_f (Abs _) = true
   28.45    | is_f _ = false;
   28.46  
    29.1 --- a/src/HOL/Hoare/hoare_tac.ML	Tue Oct 13 09:21:14 2015 +0200
    29.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Tue Oct 13 09:21:15 2015 +0200
    29.3 @@ -26,7 +26,7 @@
    29.4  local
    29.5  
    29.6  (** maps (%x1 ... xn. t) to [x1,...,xn] **)
    29.7 -fun abs2list (Const (@{const_name uncurry}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
    29.8 +fun abs2list (Const (@{const_name case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
    29.9    | abs2list (Abs (x, T, _)) = [Free (x, T)]
   29.10    | abs2list _ = [];
   29.11  
   29.12 @@ -47,7 +47,7 @@
   29.13              Abs (_, T, _) => T
   29.14            | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
   29.15        in
   29.16 -        Const (@{const_name uncurry},
   29.17 +        Const (@{const_name case_prod},
   29.18              (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
   29.19            absfree (x, T) z
   29.20        end;
    30.1 --- a/src/HOL/Induct/Com.thy	Tue Oct 13 09:21:14 2015 +0200
    30.2 +++ b/src/HOL/Induct/Com.thy	Tue Oct 13 09:21:15 2015 +0200
    30.3 @@ -139,7 +139,7 @@
    30.4  text\<open>Make the induction rule look nicer -- though @{text eta_contract} makes the new
    30.5      version look worse than it is...\<close>
    30.6  
    30.7 -lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
    30.8 +lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (case_prod (%v. case_prod (case_prod P v)))"
    30.9    by auto
   30.10  
   30.11  text\<open>New induction rule.  Note the form of the VALOF induction hypothesis\<close>
    31.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Oct 13 09:21:14 2015 +0200
    31.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Oct 13 09:21:15 2015 +0200
    31.3 @@ -193,7 +193,7 @@
    31.4    constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
    31.5  
    31.6  lemma [code]:
    31.7 -  "Ratreal r = split Realfract (quotient_of r)"
    31.8 +  "Ratreal r = case_prod Realfract (quotient_of r)"
    31.9    by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
   31.10  
   31.11  lemma [code, code del]:
    32.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Tue Oct 13 09:21:14 2015 +0200
    32.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Tue Oct 13 09:21:15 2015 +0200
    32.3 @@ -564,7 +564,7 @@
    32.4     BNF_Def.Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R")
    32.5  proof
    32.6    assume ?L
    32.7 -  def R' \<equiv> "the_inv rcset (Collect (split R) \<inter> (rcset a \<times> rcset b))"
    32.8 +  def R' \<equiv> "the_inv rcset (Collect (case_prod R) \<inter> (rcset a \<times> rcset b))"
    32.9    (is "the_inv rcset ?L'")
   32.10    have L: "countable ?L'" by auto
   32.11    hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset)
   32.12 @@ -607,8 +607,8 @@
   32.13  next
   32.14    fix R
   32.15    show "rel_cset R =
   32.16 -        (BNF_Def.Grp {x. rcset x \<subseteq> Collect (split R)} (cimage fst))\<inverse>\<inverse> OO
   32.17 -         BNF_Def.Grp {x. rcset x \<subseteq> Collect (split R)} (cimage snd)"
   32.18 +        (BNF_Def.Grp {x. rcset x \<subseteq> Collect (case_prod R)} (cimage fst))\<inverse>\<inverse> OO
   32.19 +         BNF_Def.Grp {x. rcset x \<subseteq> Collect (case_prod R)} (cimage snd)"
   32.20    unfolding rel_cset_alt_def[abs_def] rel_cset_aux by simp
   32.21  qed(simp add: bot_cset.rep_eq)
   32.22  
    33.1 --- a/src/HOL/Library/FSet.thy	Tue Oct 13 09:21:14 2015 +0200
    33.2 +++ b/src/HOL/Library/FSet.thy	Tue Oct 13 09:21:15 2015 +0200
    33.3 @@ -939,7 +939,7 @@
    33.4    BNF_Def.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
    33.5  proof
    33.6    assume ?L
    33.7 -  def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
    33.8 +  def R' \<equiv> "the_inv fset (Collect (case_prod R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
    33.9    have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+
   33.10    hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
   33.11    show ?R unfolding Grp_def relcompp.simps conversep.simps
    34.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Tue Oct 13 09:21:14 2015 +0200
    34.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Tue Oct 13 09:21:15 2015 +0200
    34.3 @@ -183,7 +183,7 @@
    34.4    have bij: "bij (\<lambda>(a, b, c). ((a, b), c))"
    34.5      by (auto intro!: bijI injI simp add: image_def)
    34.6    have "{p. \<exists>c. g (fst p) (snd p) c \<noteq> 1} \<times> {c. \<exists>p. g (fst p) (snd p) c \<noteq> 1} \<subseteq> D"
    34.7 -    by auto (insert subset, auto)
    34.8 +    by auto (insert subset, blast)
    34.9    with fin have "G (\<lambda>p. G (g (fst p) (snd p))) = G (\<lambda>(p, c). g (fst p) (snd p) c)"
   34.10      by (rule cartesian_product)
   34.11    then have "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>((a, b), c). g a b c)"
    35.1 --- a/src/HOL/Library/Multiset.thy	Tue Oct 13 09:21:14 2015 +0200
    35.2 +++ b/src/HOL/Library/Multiset.thy	Tue Oct 13 09:21:15 2015 +0200
    35.3 @@ -2085,9 +2085,9 @@
    35.4  
    35.5  lemma [code]:
    35.6    "mset xs #\<union> mset ys =
    35.7 -    mset (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
    35.8 +    mset (case_prod append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
    35.9  proof -
   35.10 -  have "\<And>zs. mset (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
   35.11 +  have "\<And>zs. mset (case_prod append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
   35.12        (mset xs #\<union> mset ys) + mset zs"
   35.13      by (induct xs arbitrary: ys) (simp_all add: multiset_eq_iff)
   35.14    then show ?thesis by simp
    36.1 --- a/src/HOL/Library/Multiset_Order.thy	Tue Oct 13 09:21:14 2015 +0200
    36.2 +++ b/src/HOL/Library/Multiset_Order.thy	Tue Oct 13 09:21:15 2015 +0200
    36.3 @@ -230,7 +230,7 @@
    36.4  interpretation multiset_wellorder: wellorder
    36.5    "le_multiset :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
    36.6    "less_multiset :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
    36.7 -  by unfold_locales (blast intro: wf_less_multiset[unfolded wf_def, rule_format])
    36.8 +  by unfold_locales (blast intro: wf_less_multiset [unfolded wf_def, simplified, rule_format])
    36.9  
   36.10  lemma le_multiset_total:
   36.11    fixes M N :: "('a :: linorder) multiset"
    37.1 --- a/src/HOL/Library/Permutations.thy	Tue Oct 13 09:21:14 2015 +0200
    37.2 +++ b/src/HOL/Library/Permutations.thy	Tue Oct 13 09:21:15 2015 +0200
    37.3 @@ -196,7 +196,7 @@
    37.4        by (auto intro: card_ge_0_finite)
    37.5      then have pF'f: "finite ?pF'"
    37.6        using H0 \<open>finite F\<close>
    37.7 -      apply (simp only: Collect_split Collect_mem_eq)
    37.8 +      apply (simp only: Collect_case_prod Collect_mem_eq)
    37.9        apply (rule finite_cartesian_product)
   37.10        apply simp_all
   37.11        done
   37.12 @@ -246,7 +246,7 @@
   37.13      from pFs H0 have xFc: "card ?xF = fact n"
   37.14        unfolding xfgpF' card_image[OF ginj]
   37.15        using \<open>finite F\<close> \<open>finite ?pF\<close>
   37.16 -      apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
   37.17 +      apply (simp only: Collect_case_prod Collect_mem_eq card_cartesian_product)
   37.18        apply simp
   37.19        done
   37.20      from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF"
    38.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Oct 13 09:21:14 2015 +0200
    38.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Oct 13 09:21:15 2015 +0200
    38.3 @@ -22,7 +22,7 @@
    38.4  
    38.5  section \<open>Pairs\<close>
    38.6  
    38.7 -setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name uncurry}]\<close>
    38.8 +setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}]\<close>
    38.9  
   38.10  section \<open>Filters\<close>
   38.11  
    39.1 --- a/src/HOL/Library/Quotient_Product.thy	Tue Oct 13 09:21:14 2015 +0200
    39.2 +++ b/src/HOL/Library/Quotient_Product.thy	Tue Oct 13 09:21:15 2015 +0200
    39.3 @@ -76,14 +76,14 @@
    39.4    shows "(map_prod Rep1 Rep2 ---> Abs2) snd = snd"
    39.5    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2])
    39.6  
    39.7 -lemma split_rsp [quot_respect]:
    39.8 -  shows "((R1 ===> R2 ===> (op =)) ===> (rel_prod R1 R2) ===> (op =)) split split"
    39.9 +lemma case_prod_rsp [quot_respect]:
   39.10 +  shows "((R1 ===> R2 ===> (op =)) ===> (rel_prod R1 R2) ===> (op =)) case_prod case_prod"
   39.11    by (rule case_prod_transfer)
   39.12  
   39.13  lemma split_prs [quot_preserve]:
   39.14    assumes q1: "Quotient3 R1 Abs1 Rep1"
   39.15    and     q2: "Quotient3 R2 Abs2 Rep2"
   39.16 -  shows "(((Abs1 ---> Abs2 ---> id) ---> map_prod Rep1 Rep2 ---> id) split) = split"
   39.17 +  shows "(((Abs1 ---> Abs2 ---> id) ---> map_prod Rep1 Rep2 ---> id) case_prod) = case_prod"
   39.18    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
   39.19  
   39.20  lemma [quot_respect]:
   39.21 @@ -103,6 +103,6 @@
   39.22    (l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))"
   39.23    by simp
   39.24  
   39.25 -declare Pair_eq[quot_preserve]
   39.26 +declare prod.inject[quot_preserve]
   39.27  
   39.28  end
    40.1 --- a/src/HOL/Library/Stream.thy	Tue Oct 13 09:21:14 2015 +0200
    40.2 +++ b/src/HOL/Library/Stream.thy	Tue Oct 13 09:21:15 2015 +0200
    40.3 @@ -581,7 +581,7 @@
    40.4    by (subst smap2.ctr) simp
    40.5  
    40.6  lemma smap2_szip:
    40.7 -  "smap2 f s1 s2 = smap (split f) (szip s1 s2)"
    40.8 +  "smap2 f s1 s2 = smap (case_prod f) (szip s1 s2)"
    40.9    by (coinduction arbitrary: s1 s2) auto
   40.10  
   40.11  lemma smap_smap2[simp]:
   40.12 @@ -597,7 +597,7 @@
   40.13    by (induct n arbitrary: s1 s2) auto
   40.14  
   40.15  lemma stake_smap2[simp]:
   40.16 -  "stake n (smap2 f s1 s2) = map (split f) (zip (stake n s1) (stake n s2))"
   40.17 +  "stake n (smap2 f s1 s2) = map (case_prod f) (zip (stake n s1) (stake n s2))"
   40.18    by (induct n arbitrary: s1 s2) auto
   40.19  
   40.20  lemma sdrop_smap2[simp]:
    41.1 --- a/src/HOL/Library/While_Combinator.thy	Tue Oct 13 09:21:14 2015 +0200
    41.2 +++ b/src/HOL/Library/While_Combinator.thy	Tue Oct 13 09:21:15 2015 +0200
    41.3 @@ -349,7 +349,7 @@
    41.4      by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
    41.5    { assume "ws = []"
    41.6      hence ?thesis using I
    41.7 -      by (auto simp del:Image_Collect_split dest: Image_closed_trancl)
    41.8 +      by (auto simp del:Image_Collect_case_prod dest: Image_closed_trancl)
    41.9    } moreover
   41.10    { assume "ws \<noteq> []"
   41.11      hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
    42.1 --- a/src/HOL/Library/old_recdef.ML	Tue Oct 13 09:21:14 2015 +0200
    42.2 +++ b/src/HOL/Library/old_recdef.ML	Tue Oct 13 09:21:15 2015 +0200
    42.3 @@ -551,7 +551,7 @@
    42.4  
    42.5  local
    42.6  fun mk_uncurry (xt, yt, zt) =
    42.7 -    Const(@{const_name uncurry}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
    42.8 +    Const(@{const_name case_prod}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
    42.9  fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
   42.10    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
   42.11  fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
   42.12 @@ -631,7 +631,7 @@
   42.13    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
   42.14  
   42.15  
   42.16 -local  fun ucheck t = (if #Name (dest_const t) = @{const_name uncurry} then t
   42.17 +local  fun ucheck t = (if #Name (dest_const t) = @{const_name case_prod} then t
   42.18                         else raise Match)
   42.19  in
   42.20  fun dest_pabs used tm =
    43.1 --- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Tue Oct 13 09:21:14 2015 +0200
    43.2 +++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Tue Oct 13 09:21:15 2015 +0200
    43.3 @@ -48,7 +48,7 @@
    43.4  
    43.5  
    43.6  lemma split_compose: 
    43.7 -  "(split f) \<circ> (\<lambda> (a,b). ((fa a), (fb b))) = (\<lambda> (a,b). (f (fa a) (fb b)))"
    43.8 +  "(case_prod f) \<circ> (\<lambda> (a,b). ((fa a), (fb b))) = (\<lambda> (a,b). (f (fa a) (fb b)))"
    43.9    by (simp add: split_def o_def)
   43.10  
   43.11  lemma split_iter:
    44.1 --- a/src/HOL/MicroJava/DFA/Listn.thy	Tue Oct 13 09:21:14 2015 +0200
    44.2 +++ b/src/HOL/MicroJava/DFA/Listn.thy	Tue Oct 13 09:21:15 2015 +0200
    44.3 @@ -26,7 +26,7 @@
    44.4    where "x <[r] y == x <_(le r) y"
    44.5  
    44.6  definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
    44.7 -"map2 f == (%xs ys. map (split f) (zip xs ys))"
    44.8 +"map2 f == (%xs ys. map (case_prod f) (zip xs ys))"
    44.9  
   44.10  abbreviation
   44.11    plussublist_syntax :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
    45.1 --- a/src/HOL/MicroJava/J/Example.thy	Tue Oct 13 09:21:14 2015 +0200
    45.2 +++ b/src/HOL/MicroJava/J/Example.thy	Tue Oct 13 09:21:15 2015 +0200
    45.3 @@ -434,7 +434,7 @@
    45.4  apply     (simp (no_asm))
    45.5  apply     (rule e) -- "XcptE"
    45.6  apply    (simp (no_asm))
    45.7 -apply   (rule surjective_pairing [symmetric, THEN[2]trans], subst Pair_eq, force)
    45.8 +apply   (rule surjective_pairing [symmetric, THEN[2]trans], subst prod.inject, force)
    45.9  apply  (simp (no_asm))
   45.10  apply (simp (no_asm))
   45.11  apply (rule e) -- "XcptE"
    46.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Oct 13 09:21:14 2015 +0200
    46.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Oct 13 09:21:15 2015 +0200
    46.3 @@ -104,7 +104,7 @@
    46.4  lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;  
    46.5     list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;  
    46.6    length pTs' = length pns; distinct pns;  
    46.7 -  Ball (set lvars) (split (\<lambda>vn. is_type G))  
    46.8 +  Ball (set lvars) (case_prod (\<lambda>vn. is_type G))  
    46.9    |] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')"
   46.10  apply (unfold wf_mhead_def)
   46.11  apply( clarsimp)
    47.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Oct 13 09:21:14 2015 +0200
    47.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Oct 13 09:21:15 2015 +0200
    47.3 @@ -1593,7 +1593,7 @@
    47.4      obtain a b where ab: "snd x = cbox a b"
    47.5        using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
    47.6      have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
    47.7 -      by (metis pair_collapse \<open>x\<in>p\<close> \<open>snd x = snd y\<close> \<open>x \<noteq> y\<close>)+
    47.8 +      by (metis prod.collapse \<open>x\<in>p\<close> \<open>snd x = snd y\<close> \<open>x \<noteq> y\<close>)+
    47.9      with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
   47.10        by (intro assm(5)[of "fst x" _ "fst y"]) auto
   47.11      then have "content (cbox a b) = 0"
   47.12 @@ -3211,7 +3211,7 @@
   47.13          unfolding p(8)[symmetric] by auto
   47.14        fix x l
   47.15        assume xl: "(x, l) \<in> ?M1"
   47.16 -      then guess x' l' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note xl'=this
   47.17 +      then guess x' l' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note xl'=this
   47.18        show "x \<in> l" "l \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<le> c}"
   47.19          unfolding xl'
   47.20          using p(4-6)[OF xl'(3)] using xl'(4)
   47.21 @@ -3223,7 +3223,7 @@
   47.22        fix y r
   47.23        let ?goal = "interior l \<inter> interior r = {}"
   47.24        assume yr: "(y, r) \<in> ?M1"
   47.25 -      then guess y' r' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note yr'=this
   47.26 +      then guess y' r' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note yr'=this
   47.27        assume as: "(x, l) \<noteq> (y, r)"
   47.28        show "interior l \<inter> interior r = {}"
   47.29        proof (cases "l' = r' \<longrightarrow> x' = y'")
   47.30 @@ -3250,7 +3250,7 @@
   47.31          unfolding p(8)[symmetric] by auto
   47.32        fix x l
   47.33        assume xl: "(x, l) \<in> ?M2"
   47.34 -      then guess x' l' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note xl'=this
   47.35 +      then guess x' l' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note xl'=this
   47.36        show "x \<in> l" "l \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
   47.37          unfolding xl'
   47.38          using p(4-6)[OF xl'(3)] xl'(4) xk_ge_c[OF xl'(3-4)]
   47.39 @@ -3262,7 +3262,7 @@
   47.40        fix y r
   47.41        let ?goal = "interior l \<inter> interior r = {}"
   47.42        assume yr: "(y, r) \<in> ?M2"
   47.43 -      then guess y' r' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note yr'=this
   47.44 +      then guess y' r' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note yr'=this
   47.45        assume as: "(x, l) \<noteq> (y, r)"
   47.46        show "interior l \<inter> interior r = {}"
   47.47        proof (cases "l' = r' \<longrightarrow> x' = y'")
   47.48 @@ -10793,7 +10793,7 @@
   47.49            using p'(1)
   47.50            apply auto
   47.51            done
   47.52 -        also have "\<dots> = (\<Sum>x\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (split op \<inter> x) f))"
   47.53 +        also have "\<dots> = (\<Sum>x\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (case_prod op \<inter> x) f))"
   47.54            unfolding split_def ..
   47.55          also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
   47.56            unfolding *
   47.57 @@ -10898,7 +10898,7 @@
   47.58            apply (subst setsum.reindex_nontrivial)
   47.59            apply fact
   47.60            unfolding split_paired_all
   47.61 -          unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff Pair_eq
   47.62 +          unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff prod.inject
   47.63            apply (elim conjE)
   47.64          proof -
   47.65            fix x1 l1 k1 x2 l2 k2
   47.66 @@ -11116,9 +11116,8 @@
   47.67            by auto
   47.68          from henstock_lemma [OF f(1) \<open>e/2>0\<close>] obtain d2 where
   47.69            d2: "gauge d2" "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d2 fine p \<longrightarrow>
   47.70 -            (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
   47.71 -          by blast
   47.72 -        obtain p where
   47.73 +            (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" .
   47.74 +         obtain p where
   47.75            p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
   47.76            by (rule fine_division_exists [OF gauge_inter [OF d1(1) d2(1)], of a b])
   47.77              (auto simp add: fine_inter)
    48.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 13 09:21:14 2015 +0200
    48.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 13 09:21:15 2015 +0200
    48.3 @@ -6294,7 +6294,7 @@
    48.4  proof -
    48.5    from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
    48.6      unfolding bounded_def by auto
    48.7 -  have "bdd_above (split dist ` (s\<times>s))"
    48.8 +  have "bdd_above (case_prod dist ` (s\<times>s))"
    48.9    proof (intro bdd_aboveI, safe)
   48.10      fix a b
   48.11      assume "a \<in> s" "b \<in> s"
    49.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Oct 13 09:21:14 2015 +0200
    49.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Oct 13 09:21:15 2015 +0200
    49.3 @@ -16,23 +16,23 @@
    49.4  
    49.5  subsection {* Curry in a Hurry *}
    49.6  
    49.7 -lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
    49.8 +lemma "(\<lambda>f x y. (curry o case_prod) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
    49.9  nitpick [card = 1-12, expect = none]
   49.10  by auto
   49.11  
   49.12 -lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
   49.13 +lemma "(\<lambda>f p. (case_prod o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
   49.14  nitpick [card = 1-12, expect = none]
   49.15  by auto
   49.16  
   49.17 -lemma "split (curry f) = f"
   49.18 +lemma "case_prod (curry f) = f"
   49.19  nitpick [card = 1-12, expect = none]
   49.20  by auto
   49.21  
   49.22 -lemma "curry (split f) = f"
   49.23 +lemma "curry (case_prod f) = f"
   49.24  nitpick [card = 1-12, expect = none]
   49.25  by auto
   49.26  
   49.27 -lemma "split (\<lambda>x y. f (x, y)) = f"
   49.28 +lemma "case_prod (\<lambda>x y. f (x, y)) = f"
   49.29  nitpick [card = 1-12, expect = none]
   49.30  by auto
   49.31  
   49.32 @@ -139,7 +139,7 @@
   49.33  nitpick [card = 2, expect = none]
   49.34  by auto
   49.35  
   49.36 -lemma "f = split"
   49.37 +lemma "f = case_prod"
   49.38  nitpick [card = 2, expect = genuine]
   49.39  oops
   49.40  
    50.1 --- a/src/HOL/Nominal/nominal_induct.ML	Tue Oct 13 09:21:14 2015 +0200
    50.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Tue Oct 13 09:21:15 2015 +0200
    50.3 @@ -18,7 +18,7 @@
    50.4  fun tuple ts = HOLogic.unit |> fold (fn t => fn u => HOLogic.mk_prod (u, t)) ts;
    50.5  
    50.6  fun tuple_fun Ts (xi, T) =
    50.7 -  Library.funpow (length Ts) HOLogic.mk_split
    50.8 +  Library.funpow (length Ts) HOLogic.mk_case_prod
    50.9      (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T));
   50.10  
   50.11  fun split_all_tuples ctxt =
    51.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Tue Oct 13 09:21:14 2015 +0200
    51.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Tue Oct 13 09:21:15 2015 +0200
    51.3 @@ -324,7 +324,7 @@
    51.4    apply (case_tac "r' mod r = 0")
    51.5     prefer 2
    51.6     apply (frule_tac a = "r'" in pos_mod_sign, auto)
    51.7 -  apply (metis Pair_eq xzgcda.simps order_refl)
    51.8 +  apply (metis prod.inject xzgcda.simps order_refl)
    51.9    done
   51.10  
   51.11  lemma xzgcd_correct:
    52.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Oct 13 09:21:14 2015 +0200
    52.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Oct 13 09:21:15 2015 +0200
    52.3 @@ -338,7 +338,7 @@
    52.4    "jad = apsnd transpose o length_permutate o map sparsify"
    52.5  
    52.6  definition
    52.7 -  "jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
    52.8 +  "jad_mv v = inflate o case_prod zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
    52.9  
   52.10  lemma "matrix (M::int list list) rs cs \<Longrightarrow> False"
   52.11  quickcheck[tester = smart_exhaustive, size = 6]
    53.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Oct 13 09:21:14 2015 +0200
    53.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Oct 13 09:21:15 2015 +0200
    53.3 @@ -62,7 +62,7 @@
    53.4    by (intro measurable_measure_of) (auto dest: sets.sets_into_space)
    53.5  
    53.6  lemma measurable_split_replace[measurable (raw)]:
    53.7 -  "(\<lambda>x. f x (fst (g x)) (snd (g x))) \<in> measurable M N \<Longrightarrow> (\<lambda>x. split (f x) (g x)) \<in> measurable M N"
    53.8 +  "(\<lambda>x. f x (fst (g x)) (snd (g x))) \<in> measurable M N \<Longrightarrow> (\<lambda>x. case_prod (f x) (g x)) \<in> measurable M N"
    53.9    unfolding split_beta' .
   53.10  
   53.11  lemma measurable_Pair[measurable (raw)]:
   53.12 @@ -88,7 +88,7 @@
   53.13      measurable_def)
   53.14  
   53.15  lemma measurable_Pair_compose_split[measurable_dest]:
   53.16 -  assumes f: "split f \<in> measurable (M1 \<Otimes>\<^sub>M M2) N"
   53.17 +  assumes f: "case_prod f \<in> measurable (M1 \<Otimes>\<^sub>M M2) N"
   53.18    assumes g: "g \<in> measurable M M1" and h: "h \<in> measurable M M2"
   53.19    shows "(\<lambda>x. f (g x) (h x)) \<in> measurable M N"
   53.20    using measurable_compose[OF measurable_Pair f, OF g h] by simp
   53.21 @@ -571,8 +571,8 @@
   53.22    unfolding nn_integral_max_0 by auto
   53.23  
   53.24  lemma (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]:
   53.25 -  "split f \<in> borel_measurable (N \<Otimes>\<^sub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^sup>+ y. f x y \<partial>M) \<in> borel_measurable N"
   53.26 -  using borel_measurable_nn_integral_fst'[of "\<lambda>x. max 0 (split f x)" N]
   53.27 +  "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^sup>+ y. f x y \<partial>M) \<in> borel_measurable N"
   53.28 +  using borel_measurable_nn_integral_fst'[of "\<lambda>x. max 0 (case_prod f x)" N]
   53.29    by (simp add: nn_integral_max_0)
   53.30  
   53.31  lemma (in pair_sigma_finite) nn_integral_snd:
   53.32 @@ -595,7 +595,7 @@
   53.33    unfolding nn_integral_snd[OF assms] M2.nn_integral_fst[OF assms] ..
   53.34  
   53.35  lemma (in pair_sigma_finite) Fubini':
   53.36 -  assumes f: "split f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
   53.37 +  assumes f: "case_prod f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
   53.38    shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f x y \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f x y \<partial>M2) \<partial>M1)"
   53.39    using Fubini[OF f] by simp
   53.40  
    54.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Tue Oct 13 09:21:14 2015 +0200
    54.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Tue Oct 13 09:21:15 2015 +0200
    54.3 @@ -2453,7 +2453,7 @@
    54.4  
    54.5  lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
    54.6    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
    54.7 -  assumes [measurable]: "split f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
    54.8 +  assumes [measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
    54.9    shows "Measurable.pred N (\<lambda>x. integrable M (f x))"
   54.10  proof -
   54.11    have [simp]: "\<And>x. x \<in> space N \<Longrightarrow> integrable M (f x) \<longleftrightarrow> (\<integral>\<^sup>+y. norm (f x y) \<partial>M) < \<infinity>"
   54.12 @@ -2472,7 +2472,7 @@
   54.13  
   54.14  lemma (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
   54.15    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
   54.16 -  assumes f[measurable]: "split f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
   54.17 +  assumes f[measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
   54.18    shows "(\<lambda>x. \<integral>y. f x y \<partial>M) \<in> borel_measurable N"
   54.19  proof -
   54.20    from borel_measurable_implies_sequence_metric[OF f, of 0] guess s ..
   54.21 @@ -2738,7 +2738,7 @@
   54.22  
   54.23  lemma (in pair_sigma_finite)
   54.24    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
   54.25 -  assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
   54.26 +  assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
   54.27    shows AE_integrable_fst: "AE x in M1. integrable M2 (\<lambda>y. f x y)" (is "?AE")
   54.28      and integrable_fst: "integrable M1 (\<lambda>x. \<integral>y. f x y \<partial>M2)" (is "?INT")
   54.29      and integral_fst: "(\<integral>x. (\<integral>y. f x y \<partial>M2) \<partial>M1) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). f x y)" (is "?EQ")
   54.30 @@ -2746,10 +2746,10 @@
   54.31  
   54.32  lemma (in pair_sigma_finite)
   54.33    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
   54.34 -  assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
   54.35 +  assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
   54.36    shows AE_integrable_snd: "AE y in M2. integrable M1 (\<lambda>x. f x y)" (is "?AE")
   54.37      and integrable_snd: "integrable M2 (\<lambda>y. \<integral>x. f x y \<partial>M1)" (is "?INT")
   54.38 -    and integral_snd: "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (split f)" (is "?EQ")
   54.39 +    and integral_snd: "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (case_prod f)" (is "?EQ")
   54.40  proof -
   54.41    interpret Q: pair_sigma_finite M2 M1 ..
   54.42    have Q_int: "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x, y). f y x)"
   54.43 @@ -2757,12 +2757,12 @@
   54.44    show ?AE  using Q.AE_integrable_fst'[OF Q_int] by simp
   54.45    show ?INT using Q.integrable_fst'[OF Q_int] by simp
   54.46    show ?EQ using Q.integral_fst'[OF Q_int]
   54.47 -    using integral_product_swap[of "split f"] by simp
   54.48 +    using integral_product_swap[of "case_prod f"] by simp
   54.49  qed
   54.50  
   54.51  lemma (in pair_sigma_finite) Fubini_integral:
   54.52    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: {banach, second_countable_topology}"
   54.53 -  assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
   54.54 +  assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
   54.55    shows "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f x y \<partial>M2) \<partial>M1)"
   54.56    unfolding integral_snd[OF assms] integral_fst[OF assms] ..
   54.57  
    55.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Oct 13 09:21:14 2015 +0200
    55.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Oct 13 09:21:15 2015 +0200
    55.3 @@ -632,7 +632,7 @@
    55.4      finally show "a < x" .
    55.5    qed
    55.6    show "?set \<in> ?SIGMA" unfolding *
    55.7 -    by (auto del: Diff intro!: Diff i)
    55.8 +    by (auto intro!: Diff sigma_sets_Inter i)
    55.9  qed
   55.10  
   55.11  lemma borel_eq_halfspace_less:
    56.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Oct 13 09:21:14 2015 +0200
    56.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Oct 13 09:21:15 2015 +0200
    56.3 @@ -417,7 +417,7 @@
    56.4        and Ble: "\<And>n. (\<Sum>i. f (B n i)) \<le> ?O (A n) + e * (1/2)^(Suc n)"
    56.5        by auto blast
    56.6  
    56.7 -    def C \<equiv> "split B o prod_decode"
    56.8 +    def C \<equiv> "case_prod B o prod_decode"
    56.9      from B have B_in_M: "\<And>i j. B i j \<in> M"
   56.10        by (rule range_subsetD)
   56.11      then have C: "range C \<subseteq> M"
   56.12 @@ -800,24 +800,24 @@
   56.13            by blast
   56.14        qed
   56.15        from choice[OF this] guess f .. note f = this
   56.16 -      then have UN_f_eq: "(\<Union>i. split f (prod_decode i)) = (\<Union>i. A i)"
   56.17 +      then have UN_f_eq: "(\<Union>i. case_prod f (prod_decode i)) = (\<Union>i. A i)"
   56.18          unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff)
   56.19  
   56.20 -      have d: "disjoint_family (\<lambda>i. split f (prod_decode i))"
   56.21 +      have d: "disjoint_family (\<lambda>i. case_prod f (prod_decode i))"
   56.22          unfolding disjoint_family_on_def
   56.23        proof (intro ballI impI)
   56.24          fix m n :: nat assume "m \<noteq> n"
   56.25          then have neq: "prod_decode m \<noteq> prod_decode n"
   56.26            using inj_prod_decode[of UNIV] by (auto simp: inj_on_def)
   56.27 -        show "split f (prod_decode m) \<inter> split f (prod_decode n) = {}"
   56.28 +        show "case_prod f (prod_decode m) \<inter> case_prod f (prod_decode n) = {}"
   56.29          proof cases
   56.30            assume "fst (prod_decode m) = fst (prod_decode n)"
   56.31            then show ?thesis
   56.32              using neq f by (fastforce simp: disjoint_family_on_def)
   56.33          next
   56.34            assume neq: "fst (prod_decode m) \<noteq> fst (prod_decode n)"
   56.35 -          have "split f (prod_decode m) \<subseteq> A (fst (prod_decode m))"
   56.36 -            "split f (prod_decode n) \<subseteq> A (fst (prod_decode n))"
   56.37 +          have "case_prod f (prod_decode m) \<subseteq> A (fst (prod_decode m))"
   56.38 +            "case_prod f (prod_decode n) \<subseteq> A (fst (prod_decode n))"
   56.39              using f[THEN spec, of "fst (prod_decode m)"]
   56.40              using f[THEN spec, of "fst (prod_decode n)"]
   56.41              by (auto simp: set_eq_iff)
   56.42 @@ -825,12 +825,12 @@
   56.43              by (fastforce simp: disjoint_family_on_def subset_eq set_eq_iff)
   56.44          qed
   56.45        qed
   56.46 -      from f have "(\<Sum>n. \<mu>_r (A n)) = (\<Sum>n. \<mu>_r (split f (prod_decode n)))"
   56.47 +      from f have "(\<Sum>n. \<mu>_r (A n)) = (\<Sum>n. \<mu>_r (case_prod f (prod_decode n)))"
   56.48          by (intro suminf_ereal_2dimen[symmetric] positiveD2[OF pos] generated_ringI_Basic)
   56.49           (auto split: prod.split)
   56.50 -      also have "\<dots> = (\<Sum>n. \<mu> (split f (prod_decode n)))"
   56.51 +      also have "\<dots> = (\<Sum>n. \<mu> (case_prod f (prod_decode n)))"
   56.52          using f V(2) by (auto intro!: arg_cong[where f=suminf] split: prod.split)
   56.53 -      also have "\<dots> = \<mu> (\<Union>i. split f (prod_decode i))"
   56.54 +      also have "\<dots> = \<mu> (\<Union>i. case_prod f (prod_decode i))"
   56.55          using f `c \<in> C'` C'
   56.56          by (intro ca[unfolded countably_additive_def, rule_format])
   56.57             (auto split: prod.split simp: UN_f_eq d UN_eq)
    57.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Oct 13 09:21:14 2015 +0200
    57.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Oct 13 09:21:15 2015 +0200
    57.3 @@ -12,7 +12,7 @@
    57.4    by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
    57.5       (force intro: exI[of _ "restrict f I" for f])
    57.6  
    57.7 -lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
    57.8 +lemma case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
    57.9    by auto
   57.10  
   57.11  subsubsection {* More about Function restricted by @{const extensional}  *}
   57.12 @@ -1110,7 +1110,7 @@
   57.13  qed (simp add: space_PiM)
   57.14  
   57.15  lemma (in product_sigma_finite) product_nn_integral_pair:
   57.16 -  assumes [measurable]: "split f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
   57.17 +  assumes [measurable]: "case_prod f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
   57.18    assumes xy: "x \<noteq> y"
   57.19    shows "(\<integral>\<^sup>+\<sigma>. f (\<sigma> x) (\<sigma> y) \<partial>PiM {x, y} M) = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
   57.20  proof-
    58.1 --- a/src/HOL/Probability/Giry_Monad.thy	Tue Oct 13 09:21:14 2015 +0200
    58.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Tue Oct 13 09:21:15 2015 +0200
    58.3 @@ -559,12 +559,12 @@
    58.4    by (auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space)
    58.5  
    58.6  lemma measurable_distr2:
    58.7 -  assumes f[measurable]: "split f \<in> measurable (L \<Otimes>\<^sub>M M) N"
    58.8 +  assumes f[measurable]: "case_prod f \<in> measurable (L \<Otimes>\<^sub>M M) N"
    58.9    assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)"
   58.10    shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)"
   58.11  proof -
   58.12    have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)
   58.13 -    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (split f)) \<in> measurable L (subprob_algebra N)"
   58.14 +    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (case_prod f)) \<in> measurable L (subprob_algebra N)"
   58.15    proof (rule measurable_cong)
   58.16      fix x assume x: "x \<in> space L"
   58.17      have gx: "g x \<in> space (subprob_algebra M)"
   58.18 @@ -580,7 +580,7 @@
   58.19        using gx by (simp add: space_subprob_algebra)
   58.20      have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)"
   58.21        by (simp add: space_pair_measure)
   58.22 -    show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (split f)" (is "?l = ?r")
   58.23 +    show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (case_prod f)" (is "?l = ?r")
   58.24      proof (rule measure_eqI)
   58.25        show "sets ?l = sets ?r"
   58.26          by simp
   58.27 @@ -1150,7 +1150,7 @@
   58.28  
   58.29  lemma measurable_bind':
   58.30    assumes M1: "f \<in> measurable M (subprob_algebra N)" and
   58.31 -          M2: "split g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
   58.32 +          M2: "case_prod g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
   58.33    shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
   58.34  proof (subst measurable_cong)
   58.35    fix x assume x_in_M: "x \<in> space M"
   58.36 @@ -1445,7 +1445,7 @@
   58.37  lemma double_bind_assoc:
   58.38    assumes Mg: "g \<in> measurable N (subprob_algebra N')"
   58.39    assumes Mf: "f \<in> measurable M (subprob_algebra M')"
   58.40 -  assumes Mh: "split h \<in> measurable (M \<Otimes>\<^sub>M M') N"
   58.41 +  assumes Mh: "case_prod h \<in> measurable (M \<Otimes>\<^sub>M M') N"
   58.42    shows "do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)} = do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g"
   58.43  proof-
   58.44    have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g = 
    59.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 13 09:21:14 2015 +0200
    59.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 13 09:21:15 2015 +0200
    59.3 @@ -163,7 +163,7 @@
    59.4  
    59.5    show ?thesis
    59.6      by (intro measurable_compose_countable'[where f="\<lambda>a b. f (fst b, a)" and g=snd and I=A,
    59.7 -                                            unfolded pair_collapse] assms)
    59.8 +                                            unfolded prod.collapse] assms)
    59.9          measurable
   59.10  qed
   59.11  
   59.12 @@ -177,7 +177,7 @@
   59.13  
   59.14    show ?thesis
   59.15      by (intro measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A,
   59.16 -                                            unfolded pair_collapse] assms)
   59.17 +                                            unfolded prod.collapse] assms)
   59.18          measurable
   59.19  qed
   59.20  
    60.1 --- a/src/HOL/Probability/Probability_Measure.thy	Tue Oct 13 09:21:14 2015 +0200
    60.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Tue Oct 13 09:21:15 2015 +0200
    60.3 @@ -288,7 +288,7 @@
    60.4              in
    60.5                go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t
    60.6              end
    60.7 -        | go pattern elem (Const (@{const_syntax uncurry}, _) $ t) =
    60.8 +        | go pattern elem (Const (@{const_syntax case_prod}, _) $ t) =
    60.9              go 
   60.10                ((Syntax.const @{syntax_const "_pattern"}, 2) :: pattern)
   60.11                (Syntax.const @{const_syntax Pair} :: elem)
    61.1 --- a/src/HOL/Probability/ex/Measure_Not_CCC.thy	Tue Oct 13 09:21:14 2015 +0200
    61.2 +++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy	Tue Oct 13 09:21:15 2015 +0200
    61.3 @@ -116,7 +116,7 @@
    61.4  
    61.5  context
    61.6    fixes EXP :: "(real \<Rightarrow> bool) measure"
    61.7 -  assumes eq: "\<And>P. split P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP"
    61.8 +  assumes eq: "\<And>P. case_prod P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP"
    61.9  begin
   61.10  
   61.11  lemma space_EXP: "space EXP = measurable COCOUNT BOOL"
   61.12 @@ -164,7 +164,7 @@
   61.13  
   61.14  end
   61.15  
   61.16 -corollary "\<not> (\<exists>EXP. \<forall>P. split P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP)"
   61.17 +corollary "\<not> (\<exists>EXP. \<forall>P. case_prod P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP)"
   61.18    using ce by blast
   61.19  
   61.20  end
    62.1 --- a/src/HOL/Probability/measurable.ML	Tue Oct 13 09:21:14 2015 +0200
    62.2 +++ b/src/HOL/Probability/measurable.ML	Tue Oct 13 09:21:15 2015 +0200
    62.3 @@ -255,7 +255,7 @@
    62.4                (map (Option.map (Thm.ctyp_of ctxt)) Ts)
    62.5                (map (Option.map (Thm.cterm_of ctxt)) ts)
    62.6                @{thm measurable_compose_countable}
    62.7 -        in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end
    62.8 +        in r_tac "case_prod countable" (cnt_prefixes ctxt f |> map inst) i end
    62.9          handle TERM _ => no_tac) 1)
   62.10  
   62.11      val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
    63.1 --- a/src/HOL/Product_Type.thy	Tue Oct 13 09:21:14 2015 +0200
    63.2 +++ b/src/HOL/Product_Type.thy	Tue Oct 13 09:21:15 2015 +0200
    63.3 @@ -238,7 +238,7 @@
    63.4  lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
    63.5    by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
    63.6  
    63.7 -free_constructors uncurry for Pair fst snd
    63.8 +free_constructors case_prod for Pair fst snd
    63.9  proof -
   63.10    fix P :: bool and p :: "'a \<times> 'b"
   63.11    show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
   63.12 @@ -266,8 +266,7 @@
   63.13  
   63.14  setup \<open>Sign.mandatory_path "prod"\<close>
   63.15  
   63.16 -declare
   63.17 -  old.prod.inject[iff del]
   63.18 +declare old.prod.inject [iff del]
   63.19  
   63.20  lemmas induct = old.prod.induct
   63.21  lemmas inducts = old.prod.inducts
   63.22 @@ -278,6 +277,16 @@
   63.23  
   63.24  declare prod.case [nitpick_simp del]
   63.25  declare prod.case_cong_weak [cong del]
   63.26 +declare prod.case_eq_if [mono]
   63.27 +declare prod.split [no_atp]
   63.28 +declare prod.split_asm [no_atp]
   63.29 +
   63.30 +text \<open>
   63.31 +  @{thm [source] prod.split} could be declared as @{text "[split]"}
   63.32 +  done after the Splitter has been speeded up significantly;
   63.33 +  precompute the constants involved and don't do anything unless the
   63.34 +  current goal contains one of those constants.
   63.35 +\<close>
   63.36  
   63.37  
   63.38  subsubsection \<open>Tuple syntax\<close>
   63.39 @@ -302,22 +311,22 @@
   63.40    "_pattern x y" \<rightleftharpoons> "CONST Pair x y"
   63.41    "_patterns x y" \<rightleftharpoons> "CONST Pair x y"
   63.42    "_tuple x (_tuple_args y z)" \<rightleftharpoons> "_tuple x (_tuple_arg (_tuple y z))"
   63.43 -  "\<lambda>(x, y, zs). b" \<rightleftharpoons> "CONST uncurry (\<lambda>x (y, zs). b)"
   63.44 -  "\<lambda>(x, y). b" \<rightleftharpoons> "CONST uncurry (\<lambda>x y. b)"
   63.45 +  "\<lambda>(x, y, zs). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x (y, zs). b)"
   63.46 +  "\<lambda>(x, y). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x y. b)"
   63.47    "_abs (CONST Pair x y) t" \<rightharpoonup> "\<lambda>(x, y). t"
   63.48    -- \<open>This rule accommodates tuples in @{text "case C \<dots> (x, y) \<dots> \<Rightarrow> \<dots>"}:
   63.49       The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic},
   63.50       not @{text pttrn}.\<close>
   63.51  
   63.52 -text \<open>print @{term "uncurry f"} as @{term "\<lambda>(x, y). f x y"} and
   63.53 -  @{term "uncurry (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close>
   63.54 +text \<open>print @{term "case_prod f"} as @{term "\<lambda>(x, y). f x y"} and
   63.55 +  @{term "case_prod (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close>
   63.56  
   63.57  typed_print_translation \<open>
   63.58    let
   63.59 -    fun uncurry_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
   63.60 -      | uncurry_guess_names_tr' T [Abs (x, xT, t)] =
   63.61 +    fun case_prod_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
   63.62 +      | case_prod_guess_names_tr' T [Abs (x, xT, t)] =
   63.63            (case (head_of t) of
   63.64 -            Const (@{const_syntax uncurry}, _) => raise Match
   63.65 +            Const (@{const_syntax case_prod}, _) => raise Match
   63.66            | _ =>
   63.67              let 
   63.68                val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   63.69 @@ -327,9 +336,9 @@
   63.70                Syntax.const @{syntax_const "_abs"} $
   63.71                  (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   63.72              end)
   63.73 -      | uncurry_guess_names_tr' T [t] =
   63.74 +      | case_prod_guess_names_tr' T [t] =
   63.75            (case head_of t of
   63.76 -            Const (@{const_syntax uncurry}, _) => raise Match
   63.77 +            Const (@{const_syntax case_prod}, _) => raise Match
   63.78            | _ =>
   63.79              let
   63.80                val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   63.81 @@ -340,8 +349,8 @@
   63.82                Syntax.const @{syntax_const "_abs"} $
   63.83                  (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   63.84              end)
   63.85 -      | uncurry_guess_names_tr' _ _ = raise Match;
   63.86 -  in [(@{const_syntax uncurry}, K uncurry_guess_names_tr')] end
   63.87 +      | case_prod_guess_names_tr' _ _ = raise Match;
   63.88 +  in [(@{const_syntax case_prod}, K case_prod_guess_names_tr')] end
   63.89  \<close>
   63.90  
   63.91  
   63.92 @@ -362,32 +371,33 @@
   63.93      (Haskell) -
   63.94  | constant "HOL.equal :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" \<rightharpoonup>
   63.95      (Haskell) infix 4 "=="
   63.96 +| constant fst \<rightharpoonup> (Haskell) "fst"
   63.97 +| constant snd \<rightharpoonup> (Haskell) "snd"
   63.98  
   63.99  
  63.100  subsubsection \<open>Fundamental operations and properties\<close>
  63.101  
  63.102  lemma Pair_inject:
  63.103    assumes "(a, b) = (a', b')"
  63.104 -    and "a = a' ==> b = b' ==> R"
  63.105 +    and "a = a' \<Longrightarrow> b = b' \<Longrightarrow> R"
  63.106    shows R
  63.107    using assms by simp
  63.108  
  63.109  lemma surj_pair [simp]: "EX x y. p = (x, y)"
  63.110    by (cases p) simp
  63.111  
  63.112 -code_printing
  63.113 -  constant fst \<rightharpoonup> (Haskell) "fst"
  63.114 -| constant snd \<rightharpoonup> (Haskell) "snd"
  63.115 -
  63.116 -lemma case_prod_unfold [nitpick_unfold]: "uncurry = (%c p. c (fst p) (snd p))"
  63.117 -  by (simp add: fun_eq_iff split: prod.split)
  63.118 -
  63.119  lemma fst_eqD: "fst (x, y) = a ==> x = a"
  63.120    by simp
  63.121  
  63.122  lemma snd_eqD: "snd (x, y) = a ==> y = a"
  63.123    by simp
  63.124  
  63.125 +lemma case_prod_unfold [nitpick_unfold]: "case_prod = (\<lambda>c p. c (fst p) (snd p))"
  63.126 +  by (simp add: fun_eq_iff split: prod.split)
  63.127 +
  63.128 +lemma case_prod_conv [simp, code]: "(case (a, b) of (c, d) \<Rightarrow> f c d) = f a b"
  63.129 +  by (fact prod.case)
  63.130 +
  63.131  lemmas surjective_pairing = prod.collapse [symmetric]
  63.132  
  63.133  lemma prod_eq_iff: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
  63.134 @@ -396,36 +406,27 @@
  63.135  lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
  63.136    by (simp add: prod_eq_iff)
  63.137  
  63.138 -lemma split_conv [simp, code]: "(case (a, b) of (c, d) \<Rightarrow> f c d) = f a b"
  63.139 -  by (fact prod.case)
  63.140 +lemma case_prodI: "f a b \<Longrightarrow> case (a, b) of (c, d) \<Rightarrow> f c d"
  63.141 +  by (rule prod.case [THEN iffD2])
  63.142  
  63.143 -lemma splitI: "f a b \<Longrightarrow> case (a, b) of (c, d) \<Rightarrow> f c d"
  63.144 -  by (rule split_conv [THEN iffD2])
  63.145 +lemma case_prodD: "(case (a, b) of (c, d) \<Rightarrow> f c d) \<Longrightarrow> f a b"
  63.146 +  by (rule prod.case [THEN iffD1])
  63.147  
  63.148 -lemma splitD: "(case (a, b) of (c, d) \<Rightarrow> f c d) \<Longrightarrow> f a b"
  63.149 -  by (rule split_conv [THEN iffD1])
  63.150 -
  63.151 -lemma split_Pair [simp]: "uncurry Pair = id"
  63.152 +lemma case_prod_Pair [simp]: "case_prod Pair = id"
  63.153    by (simp add: fun_eq_iff split: prod.split)
  63.154  
  63.155 -lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
  63.156 +lemma case_prod_eta: "(\<lambda>(x, y). f (x, y)) = f"
  63.157    -- \<open>Subsumes the old @{text split_Pair} when @{term f} is the identity function.\<close>
  63.158    by (simp add: fun_eq_iff split: prod.split)
  63.159  
  63.160 -lemma split_comp: "(case x of (a, b) \<Rightarrow> (f \<circ> g) a b) = f (g (fst x)) (snd x)"
  63.161 +lemma case_prod_comp: "(case x of (a, b) \<Rightarrow> (f \<circ> g) a b) = f (g (fst x)) (snd x)"
  63.162    by (cases x) simp
  63.163  
  63.164 -lemma split_twice: "uncurry f (uncurry g p) = uncurry (\<lambda>x y. uncurry f (g x y)) p"
  63.165 -  by (fact prod.case_distrib)
  63.166 -
  63.167 -lemma The_split: "The (uncurry P) = (THE xy. P (fst xy) (snd xy))"
  63.168 +lemma The_case_prod: "The (case_prod P) = (THE xy. P (fst xy) (snd xy))"
  63.169    by (simp add: case_prod_unfold)
  63.170  
  63.171 -lemmas split_weak_cong = prod.case_cong_weak
  63.172 -  -- \<open>Prevents simplification of @{term c}: much faster\<close>
  63.173 -
  63.174 -lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
  63.175 -  by (simp add: split_eta)
  63.176 +lemma cond_case_prod_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
  63.177 +  by (simp add: case_prod_eta)
  63.178  
  63.179  lemma split_paired_all [no_atp]: "(!!x. PROP P x) == (!!a b. PROP P (a, b))"
  63.180  proof
  63.181 @@ -438,9 +439,6 @@
  63.182    from \<open>PROP P (fst x, snd x)\<close> show "PROP P x" by simp
  63.183  qed
  63.184  
  63.185 -lemma uncurry_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
  63.186 -  by (cases x) simp
  63.187 -
  63.188  text \<open>
  63.189    The rule @{thm [source] split_paired_all} does not work with the
  63.190    Simplifier because it also affects premises in congrence rules,
  63.191 @@ -487,20 +485,20 @@
  63.192  
  63.193  lemma split_paired_The [no_atp]: "(THE x. P x) = (THE (a, b). P (a, b))"
  63.194    -- \<open>Can't be added to simpset: loops!\<close>
  63.195 -  by (simp add: split_eta)
  63.196 +  by (simp add: case_prod_eta)
  63.197  
  63.198  text \<open>
  63.199 -  Simplification procedure for @{thm [source] cond_split_eta}.  Using
  63.200 -  @{thm [source] split_eta} as a rewrite rule is not general enough,
  63.201 -  and using @{thm [source] cond_split_eta} directly would render some
  63.202 +  Simplification procedure for @{thm [source] cond_case_prod_eta}.  Using
  63.203 +  @{thm [source] case_prod_eta} as a rewrite rule is not general enough,
  63.204 +  and using @{thm [source] cond_case_prod_eta} directly would render some
  63.205    existing proofs very inefficient; similarly for @{text
  63.206 -  split_beta}.
  63.207 +  prod.case_eq_if}.
  63.208  \<close>
  63.209  
  63.210  ML \<open>
  63.211  local
  63.212 -  val cond_split_eta_ss =
  63.213 -    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms cond_split_eta});
  63.214 +  val cond_case_prod_eta_ss =
  63.215 +    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms cond_case_prod_eta});
  63.216    fun Pair_pat k 0 (Bound m) = (m = k)
  63.217      | Pair_pat k i (Const (@{const_name Pair},  _) $ Bound m $ t) =
  63.218          i > 0 andalso m = k + i andalso Pair_pat k (i - 1) t
  63.219 @@ -510,11 +508,11 @@
  63.220      | no_args k i (Bound m) = m < k orelse m > k + i
  63.221      | no_args _ _ _ = true;
  63.222    fun split_pat tp i (Abs  (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
  63.223 -    | split_pat tp i (Const (@{const_name uncurry}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
  63.224 +    | split_pat tp i (Const (@{const_name case_prod}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
  63.225      | split_pat tp i _ = NONE;
  63.226    fun metaeq ctxt lhs rhs = mk_meta_eq (Goal.prove ctxt [] []
  63.227          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
  63.228 -        (K (simp_tac (put_simpset cond_split_eta_ss ctxt) 1)));
  63.229 +        (K (simp_tac (put_simpset cond_case_prod_eta_ss ctxt) 1)));
  63.230  
  63.231    fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k + 1) i t
  63.232      | beta_term_pat k i (t $ u) =
  63.233 @@ -528,103 +526,90 @@
  63.234          else (subst arg k i t $ subst arg k i u)
  63.235      | subst arg k i t = t;
  63.236  in
  63.237 -  fun beta_proc ctxt (s as Const (@{const_name uncurry}, _) $ Abs (_, _, t) $ arg) =
  63.238 +  fun beta_proc ctxt (s as Const (@{const_name case_prod}, _) $ Abs (_, _, t) $ arg) =
  63.239          (case split_pat beta_term_pat 1 t of
  63.240            SOME (i, f) => SOME (metaeq ctxt s (subst arg 0 i f))
  63.241          | NONE => NONE)
  63.242      | beta_proc _ _ = NONE;
  63.243 -  fun eta_proc ctxt (s as Const (@{const_name uncurry}, _) $ Abs (_, _, t)) =
  63.244 +  fun eta_proc ctxt (s as Const (@{const_name case_prod}, _) $ Abs (_, _, t)) =
  63.245          (case split_pat eta_term_pat 1 t of
  63.246            SOME (_, ft) => SOME (metaeq ctxt s (let val f $ _ = ft in f end))
  63.247          | NONE => NONE)
  63.248      | eta_proc _ _ = NONE;
  63.249  end;
  63.250  \<close>
  63.251 -simproc_setup split_beta ("split f z") =
  63.252 +simproc_setup case_prod_beta ("case_prod f z") =
  63.253    \<open>fn _ => fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct)\<close>
  63.254 -simproc_setup split_eta ("split f") =
  63.255 +simproc_setup case_prod_eta ("case_prod f") =
  63.256    \<open>fn _ => fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct)\<close>
  63.257  
  63.258 -lemmas split_beta [mono] = prod.case_eq_if
  63.259 -
  63.260 -lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
  63.261 +lemma case_prod_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
  63.262    by (auto simp: fun_eq_iff)
  63.263  
  63.264 -lemmas split_split [no_atp] = prod.split
  63.265 -  -- \<open>For use with @{text split} and the Simplifier.\<close>
  63.266 -
  63.267  text \<open>
  63.268 -  @{thm [source] split_split} could be declared as @{text "[split]"}
  63.269 -  done after the Splitter has been speeded up significantly;
  63.270 -  precompute the constants involved and don't do anything unless the
  63.271 -  current goal contains one of those constants.
  63.272 -\<close>
  63.273 -
  63.274 -lemmas split_split_asm [no_atp] = prod.split_asm
  63.275 -
  63.276 -text \<open>
  63.277 -  \medskip @{const uncurry} used as a logical connective or set former.
  63.278 +  \medskip @{const case_prod} used as a logical connective or set former.
  63.279  
  63.280    \medskip These rules are for use with @{text blast}; could instead
  63.281    call @{text simp} using @{thm [source] prod.split} as rewrite.\<close>
  63.282  
  63.283 -lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case p of (a, b) \<Rightarrow> c a b"
  63.284 -  apply (simp only: split_tupled_all)
  63.285 -  apply (simp (no_asm_simp))
  63.286 -  done
  63.287 +lemma case_prodI2:
  63.288 +  "\<And>p. (\<And>a b. p = (a, b) \<Longrightarrow> c a b) \<Longrightarrow> case p of (a, b) \<Rightarrow> c a b"
  63.289 +  by (simp add: split_tupled_all)
  63.290  
  63.291 -lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> (case p of (a, b) \<Rightarrow> c a b) x"
  63.292 -  apply (simp only: split_tupled_all)
  63.293 -  apply (simp (no_asm_simp))
  63.294 -  done
  63.295 +lemma case_prodI2':
  63.296 +  "\<And>p. (\<And>a b. (a, b) = p \<Longrightarrow> c a b x) \<Longrightarrow> (case p of (a, b) \<Rightarrow> c a b) x"
  63.297 +  by (simp add: split_tupled_all)
  63.298  
  63.299 -lemma splitE: "(case p of (a, b) \<Rightarrow> c a b) ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
  63.300 -  by (induct p) auto
  63.301 +lemma case_prodE [elim!]:
  63.302 +  "(case p of (a, b) \<Rightarrow> c a b) \<Longrightarrow> (\<And>x y. p = (x, y) \<Longrightarrow> c x y \<Longrightarrow> Q) \<Longrightarrow> Q"
  63.303 +  by (induct p) simp
  63.304  
  63.305 -lemma splitE': "(case p of (a, b) \<Rightarrow> c a b) z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
  63.306 -  by (induct p) auto
  63.307 +lemma case_prodE' [elim!]:
  63.308 +  "(case p of (a, b) \<Rightarrow> c a b) z \<Longrightarrow> (\<And>x y. p = (x, y) \<Longrightarrow> c x y z \<Longrightarrow> Q) \<Longrightarrow> Q"
  63.309 +  by (induct p) simp
  63.310  
  63.311 -lemma splitE2:
  63.312 -  "[| Q (case z of (a, b) \<Rightarrow> P a b);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
  63.313 -proof -
  63.314 -  assume q: "Q (uncurry P z)"
  63.315 -  assume r: "!!x y. [|z = (x, y); Q (P x y)|] ==> R"
  63.316 -  show R
  63.317 -    apply (rule r surjective_pairing)+
  63.318 -    apply (rule split_beta [THEN subst], rule q)
  63.319 -    done
  63.320 +lemma case_prodE2:
  63.321 +  assumes q: "Q (case z of (a, b) \<Rightarrow> P a b)"
  63.322 +    and r: "\<And>x y. z = (x, y) \<Longrightarrow> Q (P x y) \<Longrightarrow> R"
  63.323 +  shows R
  63.324 +proof (rule r)
  63.325 +  show "z = (fst z, snd z)" by simp
  63.326 +  then show "Q (P (fst z) (snd z))"
  63.327 +    using q by (simp add: case_prod_unfold)
  63.328  qed
  63.329  
  63.330 -lemma splitD':
  63.331 +lemma case_prodD':
  63.332    "(case (a, b) of (c, d) \<Rightarrow> R c d) c \<Longrightarrow> R a b c"
  63.333    by simp
  63.334  
  63.335 -lemma mem_splitI:
  63.336 +lemma mem_case_prodI:
  63.337    "z \<in> c a b \<Longrightarrow> z \<in> (case (a, b) of (d, e) \<Rightarrow> c d e)"
  63.338    by simp
  63.339  
  63.340 -lemma mem_splitI2:
  63.341 +lemma mem_case_prodI2 [intro!]:
  63.342    "\<And>p. (\<And>a b. p = (a, b) \<Longrightarrow> z \<in> c a b) \<Longrightarrow> z \<in> (case p of (a, b) \<Rightarrow> c a b)"
  63.343    by (simp only: split_tupled_all) simp
  63.344  
  63.345 -lemma mem_splitE:
  63.346 -  assumes "z \<in> uncurry c p"
  63.347 +declare mem_case_prodI [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
  63.348 +declare case_prodI2' [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
  63.349 +declare case_prodI2 [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
  63.350 +declare case_prodI [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
  63.351 +  
  63.352 +lemma mem_case_prodE [elim!]:
  63.353 +  assumes "z \<in> case_prod c p"
  63.354    obtains x y where "p = (x, y)" and "z \<in> c x y"
  63.355 -  using assms by (rule splitE2)
  63.356 -
  63.357 -declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
  63.358 -declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
  63.359 +  using assms by (rule case_prodE2)
  63.360  
  63.361  ML \<open>
  63.362  local (* filtering with exists_p_split is an essential optimization *)
  63.363 -  fun exists_p_split (Const (@{const_name uncurry},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
  63.364 +  fun exists_p_split (Const (@{const_name case_prod},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
  63.365      | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
  63.366      | exists_p_split (Abs (_, _, t)) = exists_p_split t
  63.367      | exists_p_split _ = false;
  63.368  in
  63.369  fun split_conv_tac ctxt = SUBGOAL (fn (t, i) =>
  63.370    if exists_p_split t
  63.371 -  then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_conv}) i
  63.372 +  then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms case_prod_conv}) i
  63.373    else no_tac);
  63.374  end;
  63.375  \<close>
  63.376 @@ -636,10 +621,10 @@
  63.377  lemma split_eta_SetCompr [simp, no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
  63.378    by (rule ext) fast
  63.379  
  63.380 -lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = uncurry P"
  63.381 +lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = case_prod P"
  63.382    by (rule ext) fast
  63.383  
  63.384 -lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & uncurry Q ab)"
  63.385 +lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & case_prod Q ab)"
  63.386    -- \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
  63.387    by (rule ext) blast
  63.388  
  63.389 @@ -649,7 +634,7 @@
  63.390  *)
  63.391  lemma split_comp_eq: 
  63.392    fixes f :: "'a => 'b => 'c" and g :: "'d => 'a"
  63.393 -  shows "(%u. f (g (fst u)) (snd u)) = (uncurry (%x. f (g x)))"
  63.394 +  shows "(%u. f (g (fst u)) (snd u)) = (case_prod (%x. f (g x)))"
  63.395    by (rule ext) auto
  63.396  
  63.397  lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
  63.398 @@ -673,29 +658,9 @@
  63.399  qed "The_split_eq";
  63.400  *)
  63.401  
  63.402 -text \<open>
  63.403 -  Setup of internal @{text split_rule}.
  63.404 -\<close>
  63.405 -
  63.406 -lemmas case_prodI = prod.case [THEN iffD2]
  63.407 -
  63.408 -lemma case_prodI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> uncurry c p"
  63.409 -  by (fact splitI2)
  63.410 -
  63.411 -lemma case_prodI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> uncurry c p x"
  63.412 -  by (fact splitI2')
  63.413 -
  63.414 -lemma case_prodE: "uncurry c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
  63.415 -  by (fact splitE)
  63.416 -
  63.417 -lemma case_prodE': "uncurry c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
  63.418 -  by (fact splitE')
  63.419 -
  63.420 -declare case_prodI [intro!]
  63.421 -
  63.422  lemma case_prod_beta:
  63.423 -  "uncurry f p = f (fst p) (snd p)"
  63.424 -  by (fact split_beta)
  63.425 +  "case_prod f p = f (fst p) (snd p)"
  63.426 +  by (fact prod.case_eq_if)
  63.427  
  63.428  lemma prod_cases3 [cases type]:
  63.429    obtains (fields) a b c where "y = (a, b, c)"
  63.430 @@ -737,20 +702,20 @@
  63.431      "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
  63.432    by (cases x) blast
  63.433  
  63.434 -definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
  63.435 -  "internal_split == uncurry"
  63.436 +definition internal_case_prod :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
  63.437 +  "internal_case_prod == case_prod"
  63.438  
  63.439 -lemma internal_split_conv: "internal_split c (a, b) = c a b"
  63.440 -  by (simp only: internal_split_def split_conv)
  63.441 +lemma internal_case_prod_conv: "internal_case_prod c (a, b) = c a b"
  63.442 +  by (simp only: internal_case_prod_def case_prod_conv)
  63.443  
  63.444  ML_file "Tools/split_rule.ML"
  63.445  
  63.446 -hide_const internal_split
  63.447 +hide_const internal_case_prod
  63.448  
  63.449  
  63.450  subsubsection \<open>Derived operations\<close>
  63.451  
  63.452 -definition curry    :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
  63.453 +definition curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
  63.454    "curry = (\<lambda>c x y. c (x, y))"
  63.455  
  63.456  lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
  63.457 @@ -765,10 +730,10 @@
  63.458  lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q"
  63.459    by (simp add: curry_def)
  63.460  
  63.461 -lemma curry_split [simp]: "curry (uncurry f) = f"
  63.462 +lemma curry_case_prod [simp]: "curry (case_prod f) = f"
  63.463    by (simp add: curry_def case_prod_unfold)
  63.464  
  63.465 -lemma split_curry [simp]: "uncurry (curry f) = f"
  63.466 +lemma case_prod_curry [simp]: "case_prod (curry f) = f"
  63.467    by (simp add: curry_def case_prod_unfold)
  63.468  
  63.469  lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)"
  63.470 @@ -781,12 +746,12 @@
  63.471  notation fcomp (infixl "\<circ>>" 60)
  63.472  
  63.473  definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60) where
  63.474 -  "f \<circ>\<rightarrow> g = (\<lambda>x. uncurry g (f x))"
  63.475 +  "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod g (f x))"
  63.476  
  63.477  lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
  63.478    by (simp add: fun_eq_iff scomp_def case_prod_unfold)
  63.479  
  63.480 -lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = uncurry g (f x)"
  63.481 +lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = case_prod g (f x)"
  63.482    by (simp add: scomp_unfold case_prod_unfold)
  63.483  
  63.484  lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
  63.485 @@ -1076,25 +1041,25 @@
  63.486  lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)"
  63.487    by (blast elim: equalityE)
  63.488  
  63.489 -lemma SetCompr_Sigma_eq:
  63.490 +lemma Collect_case_prod_Sigma:
  63.491    "{(x, y). P x \<and> Q x y} = (SIGMA x:Collect P. Collect (Q x))"
  63.492    by blast
  63.493  
  63.494 -lemma Collect_split [simp]:
  63.495 +lemma Collect_case_prod [simp]:
  63.496    "{(a, b). P a \<and> Q b} = Collect P \<times> Collect Q "
  63.497 -  by (fact SetCompr_Sigma_eq)
  63.498 +  by (fact Collect_case_prod_Sigma)
  63.499  
  63.500 -lemma Collect_splitD:
  63.501 -  "x \<in> Collect (uncurry A) \<Longrightarrow> A (fst x) (snd x)"
  63.502 +lemma Collect_case_prodD:
  63.503 +  "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
  63.504    by auto
  63.505  
  63.506 -lemma Collect_split_mono:
  63.507 -  "A \<le> B \<Longrightarrow> Collect (uncurry A) \<subseteq> Collect (uncurry B)"
  63.508 +lemma Collect_case_prod_mono:
  63.509 +  "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
  63.510    by auto (auto elim!: le_funE)
  63.511  
  63.512  lemma Collect_split_mono_strong: 
  63.513    "X = fst ` A \<Longrightarrow> Y = snd ` A \<Longrightarrow> \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b
  63.514 -    \<Longrightarrow> A \<subseteq> Collect (uncurry P) \<Longrightarrow> A \<subseteq> Collect (uncurry Q)"
  63.515 +    \<Longrightarrow> A \<subseteq> Collect (case_prod P) \<Longrightarrow> A \<subseteq> Collect (case_prod Q)"
  63.516    by fastforce
  63.517    
  63.518  lemma UN_Times_distrib:
  63.519 @@ -1318,7 +1283,7 @@
  63.520    fn _ => fn ctxt => fn ct =>
  63.521      (case Thm.term_of ct of
  63.522        S as Const (@{const_name Collect}, Type (@{type_name fun}, [_, T])) $ t =>
  63.523 -        let val (u, _, ps) = HOLogic.strip_psplits t in
  63.524 +        let val (u, _, ps) = HOLogic.strip_ptupleabs t in
  63.525            (case u of
  63.526              (c as Const (@{const_name Set.member}, _)) $ q $ S' =>
  63.527                (case try (HOLogic.strip_ptuple ps) q of
  63.528 @@ -1329,7 +1294,7 @@
  63.529                    then
  63.530                      let val simp =
  63.531                        full_simp_tac (put_simpset HOL_basic_ss ctxt
  63.532 -                        addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1
  63.533 +                        addsimps [@{thm split_paired_all}, @{thm case_prod_conv}]) 1
  63.534                      in
  63.535                        SOME (Goal.prove ctxt [] []
  63.536                          (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
  63.537 @@ -1350,20 +1315,13 @@
  63.538  
  63.539  subsection \<open>Legacy theorem bindings and duplicates\<close>
  63.540  
  63.541 -abbreviation (input) case_prod :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
  63.542 -  "case_prod \<equiv> uncurry"
  63.543 -
  63.544 -abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
  63.545 -  "split \<equiv> uncurry"
  63.546 -
  63.547 -lemmas PairE = prod.exhaust
  63.548 -lemmas Pair_eq = prod.inject
  63.549  lemmas fst_conv = prod.sel(1)
  63.550  lemmas snd_conv = prod.sel(2)
  63.551 -lemmas pair_collapse = prod.collapse
  63.552 -lemmas split = split_conv
  63.553 -lemmas Pair_fst_snd_eq = prod_eq_iff
  63.554  lemmas split_def = case_prod_unfold
  63.555 +lemmas split_beta' = case_prod_beta'
  63.556 +lemmas split_beta = prod.case_eq_if
  63.557 +lemmas split_conv = case_prod_conv
  63.558 +lemmas split = case_prod_conv
  63.559  
  63.560  hide_const (open) prod
  63.561  
    64.1 --- a/src/HOL/Relation.thy	Tue Oct 13 09:21:14 2015 +0200
    64.2 +++ b/src/HOL/Relation.thy	Tue Oct 13 09:21:15 2015 +0200
    64.3 @@ -951,10 +951,10 @@
    64.4  lemma Field_converse [simp]: "Field (r\<inverse>) = Field r"
    64.5    by (auto simp: Field_def)
    64.6  
    64.7 -lemma Domain_Collect_split [simp]: "Domain {(x, y). P x y} = {x. EX y. P x y}"
    64.8 +lemma Domain_Collect_case_prod [simp]: "Domain {(x, y). P x y} = {x. EX y. P x y}"
    64.9    by auto
   64.10  
   64.11 -lemma Range_Collect_split [simp]: "Range {(x, y). P x y} = {y. EX x. P x y}"
   64.12 +lemma Range_Collect_case_prod [simp]: "Range {(x, y). P x y} = {y. EX x. P x y}"
   64.13    by auto
   64.14  
   64.15  lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)"
   64.16 @@ -1058,7 +1058,7 @@
   64.17  lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"
   64.18    by blast
   64.19  
   64.20 -lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}"
   64.21 +lemma Image_Collect_case_prod [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}"
   64.22    by auto
   64.23  
   64.24  lemma Sigma_Image: "(SIGMA x:A. B x) `` X = (\<Union>x\<in>X \<inter> A. B x)"
    65.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Oct 13 09:21:14 2015 +0200
    65.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Oct 13 09:21:15 2015 +0200
    65.3 @@ -506,7 +506,7 @@
    65.4    "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
    65.5    "(fst (x, y) = snd (x, y)) = (x = y)"
    65.6    "(fst p = snd p) = (p = (snd p, fst p))"
    65.7 -  using fst_conv snd_conv pair_collapse
    65.8 +  using fst_conv snd_conv prod.collapse
    65.9    by smt+
   65.10  
   65.11  lemma
   65.12 @@ -525,7 +525,7 @@
   65.13  lemma
   65.14    "fst (hd [(a, b)]) = a"
   65.15    "snd (hd [(a, b)]) = b"
   65.16 -  using fst_conv snd_conv pair_collapse list.sel(1,3) list.simps
   65.17 +  using fst_conv snd_conv prod.collapse list.sel(1,3) list.simps
   65.18    by smt+
   65.19  
   65.20  
   65.21 @@ -627,7 +627,7 @@
   65.22    "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
   65.23    "(fst (x, y) = snd (x, y)) = (x = y)"
   65.24    "(fst p = snd p) = (p = (snd p, fst p))"
   65.25 -  using fst_conv snd_conv pair_collapse
   65.26 +  using fst_conv snd_conv prod.collapse
   65.27    using [[smt_oracle, z3_extensions]]
   65.28    by smt+
   65.29  
   65.30 @@ -648,7 +648,7 @@
   65.31  lemma
   65.32    "fst (hd [(a, b)]) = a"
   65.33    "snd (hd [(a, b)]) = b"
   65.34 -  using fst_conv snd_conv pair_collapse list.sel(1,3)
   65.35 +  using fst_conv snd_conv prod.collapse list.sel(1,3)
   65.36    using [[smt_oracle, z3_extensions]]
   65.37    by smt+
   65.38  
    66.1 --- a/src/HOL/SMT_Examples/boogie.ML	Tue Oct 13 09:21:14 2015 +0200
    66.2 +++ b/src/HOL/SMT_Examples/boogie.ML	Tue Oct 13 09:21:15 2015 +0200
    66.3 @@ -243,7 +243,7 @@
    66.4    end
    66.5  
    66.6  val boogie_rules =
    66.7 -  [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] @
    66.8 +  [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.collapse}] @
    66.9    [@{thm fun_upd_same}, @{thm fun_upd_apply}]
   66.10  
   66.11  fun boogie_tac ctxt axioms =
    67.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Oct 13 09:21:14 2015 +0200
    67.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Oct 13 09:21:15 2015 +0200
    67.3 @@ -943,7 +943,7 @@
    67.4      val CR = mk_bnf_T Ds RTs Calpha;
    67.5      val setRs =
    67.6        @{map 3} (fn R => fn T => fn U =>
    67.7 -          HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As Bs;
    67.8 +          HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_case_prod R) Rs As Bs;
    67.9  
   67.10      (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
   67.11        Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*)
   67.12 @@ -1301,7 +1301,7 @@
   67.13                  val ran_bnfT = mk_bnf_T ranTs Calpha;
   67.14                  val (revTs, Ts) = `rev (bd_bnfT :: funTs);
   67.15                  val cTs = map (SOME o Thm.ctyp_of lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
   67.16 -                val tinst = fold (fn T => fn t => HOLogic.mk_split (Term.absdummy T t)) (tl revTs)
   67.17 +                val tinst = fold (fn T => fn t => HOLogic.mk_case_prod (Term.absdummy T t)) (tl revTs)
   67.18                    (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
   67.19                      map Bound (live - 1 downto 0)) $ Bound live));
   67.20                  val cts = [NONE, SOME (Thm.cterm_of lthy tinst)];
    68.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Tue Oct 13 09:21:14 2015 +0200
    68.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Tue Oct 13 09:21:15 2015 +0200
    68.3 @@ -108,10 +108,10 @@
    68.4            eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
    68.5          hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
    68.6          REPEAT_DETERM_N n o
    68.7 -          EVERY' [rtac ctxt @{thm Collect_split_Grp_eqD}, etac ctxt @{thm set_mp}, assume_tac ctxt],
    68.8 +          EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD}, etac ctxt @{thm set_mp}, assume_tac ctxt],
    68.9          rtac ctxt CollectI,
   68.10          CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
   68.11 -          rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_split_Grp_inD},
   68.12 +          rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_case_prod_Grp_in},
   68.13            etac ctxt @{thm set_mp}, assume_tac ctxt])
   68.14          set_maps,
   68.15          rtac ctxt @{thm predicate2I}, REPEAT_DETERM o eresolve_tac ctxt [@{thm GrpE}, exE, conjE],
   68.16 @@ -165,8 +165,8 @@
   68.17          rtac ctxt (hd rel_OO_Grps RS sym RSN (2, ord_le_eq_trans));
   68.18    in
   68.19      EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm relcompp_mono}, rtac ctxt @{thm iffD2[OF conversep_mono]},
   68.20 -      rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_split_mono},
   68.21 -      rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_split_mono}] 1
   68.22 +      rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono},
   68.23 +      rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono}] 1
   68.24    end;
   68.25  
   68.26  fun mk_rel_conversep_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
    69.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Oct 13 09:21:14 2015 +0200
    69.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Oct 13 09:21:15 2015 +0200
    69.3 @@ -66,7 +66,7 @@
    69.4    | unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u)
    69.5    | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
    69.6    | unfold_lets_splits t = t
    69.7 -and unfold_splits_lets ((t as Const (@{const_name uncurry}, _)) $ u) =
    69.8 +and unfold_splits_lets ((t as Const (@{const_name case_prod}, _)) $ u) =
    69.9      (case unfold_splits_lets u of
   69.10        u' as Abs (s1, T1, Abs (s2, T2, _)) =>
   69.11        let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in
    70.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Oct 13 09:21:14 2015 +0200
    70.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Oct 13 09:21:15 2015 +0200
    70.3 @@ -958,7 +958,7 @@
    70.4          val (fTs1, fTs2) = apsnd tl (chop (i - 1) (map (fn T => T --> FT) bdFTs));
    70.5          val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2);
    70.6        in
    70.7 -        HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
    70.8 +        HOLogic.mk_case_prod (Term.absfree Kl' (Term.absfree lab'
    70.9            (mk_case_sumN fs $ (lab $ HOLogic.mk_list sum_sbdT []))))
   70.10        end;
   70.11  
   70.12 @@ -2280,7 +2280,7 @@
   70.13          ||>> mk_Frees' "z" zip_zTs;
   70.14  
   70.15        val Iphi_sets =
   70.16 -        map2 (fn phi => fn T => HOLogic.Collect_const T $ HOLogic.mk_split phi) allJphis zip_ranTs;
   70.17 +        map2 (fn phi => fn T => HOLogic.Collect_const T $ HOLogic.mk_case_prod phi) allJphis zip_ranTs;
   70.18        val in_phis = map2 (mk_in Iphi_sets) (mk_setss zip_ranTs) zipFTs;
   70.19        val fstABs = map fst_const passiveABs;
   70.20        val all_fsts = fstABs @ fstsTsTs';
   70.21 @@ -2295,7 +2295,7 @@
   70.22          Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveBs @ Ts') bnf, all_snds)) Dss bnfs;
   70.23        val Jmap_snds = map2 (fn map => fn T => if m = 0 then HOLogic.id_const T
   70.24          else Term.list_comb (map, sndABs)) (mk_Jmaps passiveABs passiveBs) Ts;
   70.25 -      val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_split zips)) ks;
   70.26 +      val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_case_prod zips)) ks;
   70.27        val zip_setss = mk_Jsetss passiveABs |> transpose;
   70.28  
   70.29        fun Jrel_coinduct_tac {context = ctxt, prems = CIHs} =
    71.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Oct 13 09:21:14 2015 +0200
    71.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Oct 13 09:21:15 2015 +0200
    71.3 @@ -298,7 +298,7 @@
    71.4            | (_, branches') =>
    71.5              Term.list_comb (If_const (typof (hd branches')) $ tap (check_no_call bound_Ts) obj,
    71.6                branches'))
    71.7 -        | (c as Const (@{const_name uncurry}, _), arg :: args) =>
    71.8 +        | (c as Const (@{const_name case_prod}, _), arg :: args) =>
    71.9            massage_rec bound_Ts
   71.10              (unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
   71.11          | (Const (c, _), args as _ :: _ :: _) =>
   71.12 @@ -402,12 +402,12 @@
   71.13                end
   71.14              | NONE =>
   71.15                (case t of
   71.16 -                Const (@{const_name uncurry}, _) $ t' =>
   71.17 +                Const (@{const_name case_prod}, _) $ t' =>
   71.18                  let
   71.19                    val U' = curried_type U;
   71.20                    val T' = curried_type T;
   71.21                  in
   71.22 -                  Const (@{const_name uncurry}, U' --> U) $ massage_any_call bound_Ts U' T' t'
   71.23 +                  Const (@{const_name case_prod}, U' --> U) $ massage_any_call bound_Ts U' T' t'
   71.24                  end
   71.25                | t1 $ t2 =>
   71.26                  (if has_call t2 then
   71.27 @@ -931,9 +931,9 @@
   71.28                let val (u, vs) = strip_comb t in
   71.29                  if is_Free u andalso has_call u then
   71.30                    Inr_const T U2 $ mk_tuple1_balanced bound_Ts vs
   71.31 -                else if try (fst o dest_Const) u = SOME @{const_name uncurry} then
   71.32 +                else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
   71.33                    map (rewrite bound_Ts) vs |> chop 1
   71.34 -                  |>> HOLogic.mk_split o the_single
   71.35 +                  |>> HOLogic.mk_case_prod o the_single
   71.36                    |> Term.list_comb
   71.37                  else
   71.38                    Term.list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs)
    72.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Tue Oct 13 09:21:14 2015 +0200
    72.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Tue Oct 13 09:21:15 2015 +0200
    72.3 @@ -108,7 +108,7 @@
    72.4  val snd_convol_fun_cong_sym = @{thm snd_convol[unfolded convol_def]} RS fun_cong RS sym;
    72.5  val sum_case_cong_weak = @{thm sum.case_cong_weak};
    72.6  val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
    72.7 -val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
    72.8 +val Collect_splitD_set_mp = @{thm Collect_case_prodD[OF set_mp]};
    72.9  val rev_bspec = Drule.rotate_prems 1 bspec;
   72.10  val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
   72.11  val converse_shift = @{thm converse_subset_swap} RS iffD1;
   72.12 @@ -239,7 +239,7 @@
   72.13              etac ctxt @{thm image_mono}, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
   72.14              rtac ctxt @{thm case_prodI}, rtac ctxt refl]
   72.15            else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
   72.16 -            rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt @{thm Collect_split_in_rel_leI}])
   72.17 +            rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt @{thm Collect_case_prod_in_rel_leI}])
   72.18          (1 upto (m + n) ~~ set_map0s)];
   72.19  
   72.20      fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
   72.21 @@ -247,7 +247,7 @@
   72.22          etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt,
   72.23          dtac ctxt (in_rel RS @{thm iffD1}),
   72.24          REPEAT_DETERM o eresolve_tac ctxt ([CollectE, conjE, exE] @
   72.25 -          @{thms CollectE Collect_split_in_rel_leE}),
   72.26 +          @{thms CollectE Collect_case_prod_in_rel_leE}),
   72.27          rtac ctxt bexI, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
   72.28          REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
   72.29          REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
   72.30 @@ -255,7 +255,7 @@
   72.31          REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
   72.32          REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
   72.33          rtac ctxt trans, rtac ctxt map_cong0,
   72.34 -        REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_splitD}, etac ctxt set_mp, assume_tac ctxt],
   72.35 +        REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_case_prodD}, etac ctxt set_mp, assume_tac ctxt],
   72.36          REPEAT_DETERM_N n o rtac ctxt refl,
   72.37          assume_tac ctxt, rtac ctxt CollectI,
   72.38          CONJ_WRAP' (fn (i, thm) =>
   72.39 @@ -772,8 +772,8 @@
   72.40      CONJ_WRAP' (fn rel_cong => EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
   72.41        REPEAT_DETERM o etac ctxt allE, rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
   72.42        REPEAT_DETERM_N m o rtac ctxt refl,
   72.43 -      REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm in_rel_Collect_split_eq[symmetric]},
   72.44 -      etac ctxt mp, etac ctxt CollectE, etac ctxt @{thm splitD}])
   72.45 +      REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm in_rel_Collect_case_prod_eq[symmetric]},
   72.46 +      etac ctxt mp, etac ctxt CollectE, etac ctxt @{thm case_prodD}])
   72.47      rel_congs,
   72.48      rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE,
   72.49      CONJ_WRAP' (K (EVERY' [rtac ctxt impI, rtac ctxt @{thm IdD}, etac ctxt set_mp,
   72.50 @@ -994,7 +994,7 @@
   72.51                  rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt @{thm box_equals[OF _ _ refl]},
   72.52                  rtac ctxt active_set_map0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt @{thm UN_least},
   72.53                  dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
   72.54 -                dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
   72.55 +                dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
   72.56                  REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
   72.57                    @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
   72.58                  hyp_subst_tac ctxt,
   72.59 @@ -1008,7 +1008,7 @@
   72.60            rtac ctxt @{thm box_equals}, rtac ctxt map_comp0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans,
   72.61            rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
   72.62            EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, assume_tac ctxt,
   72.63 -            dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
   72.64 +            dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
   72.65              REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
   72.66                @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
   72.67              hyp_subst_tac ctxt, dtac ctxt (in_Jrel RS iffD1),
    73.1 --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Oct 13 09:21:14 2015 +0200
    73.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Oct 13 09:21:15 2015 +0200
    73.3 @@ -164,7 +164,7 @@
    73.4          set_cases = @{thms fsts.cases[unfolded eq_fst_iff ex_neg_all_pos]
    73.5            snds.cases[unfolded eq_snd_iff ex_neg_all_pos]}},
    73.6       fp_co_induct_sugar =
    73.7 -       {co_rec = Const (@{const_name uncurry}, (ctr_Ts ---> C) --> fpT --> C),
    73.8 +       {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
    73.9          common_co_inducts = @{thms prod.induct},
   73.10          co_inducts = @{thms prod.induct},
   73.11          co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
    74.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Oct 13 09:21:14 2015 +0200
    74.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Oct 13 09:21:15 2015 +0200
    74.3 @@ -698,7 +698,7 @@
    74.4                (fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans,
    74.5                  rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least},
    74.6                  dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
    74.7 -                dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
    74.8 +                dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
    74.9                  REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
   74.10                    @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
   74.11                  hyp_subst_tac ctxt,
   74.12 @@ -712,7 +712,7 @@
   74.13            REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
   74.14            EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply,
   74.15              dtac ctxt set_rev_mp, assume_tac ctxt,
   74.16 -            dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
   74.17 +            dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
   74.18              REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
   74.19                @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
   74.20              hyp_subst_tac ctxt,
    75.1 --- a/src/HOL/Tools/Function/partial_function.ML	Tue Oct 13 09:21:14 2015 +0200
    75.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Tue Oct 13 09:21:15 2015 +0200
    75.3 @@ -146,11 +146,11 @@
    75.4  (* iterated versions. Nonstandard left-nested tuples arise naturally
    75.5  from "split o split o split"*)
    75.6  fun curry_n arity = funpow (arity - 1) mk_curry;
    75.7 -fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_split;
    75.8 +fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_case_prod;
    75.9  
   75.10  val curry_uncurry_ss =
   75.11    simpset_of (put_simpset HOL_basic_ss @{context}
   75.12 -    addsimps [@{thm Product_Type.curry_split}, @{thm Product_Type.split_curry}])
   75.13 +    addsimps [@{thm Product_Type.curry_case_prod}, @{thm Product_Type.case_prod_curry}])
   75.14  
   75.15  val split_conv_ss =
   75.16    simpset_of (put_simpset HOL_basic_ss @{context}
   75.17 @@ -177,7 +177,7 @@
   75.18         THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
   75.19      |> (fn thm => thm OF [mono_thm, f_def])
   75.20      |> Conv.fconv_rule (Conv.concl_conv ~1    (* simplify conclusion *)
   75.21 -         (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_split}]))
   75.22 +         (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}]))
   75.23      |> singleton (Variable.export ctxt' ctxt)
   75.24    end
   75.25  
    76.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 13 09:21:14 2015 +0200
    76.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 13 09:21:15 2015 +0200
    76.3 @@ -2210,7 +2210,7 @@
    76.4  fun n_ptuple_paths 0 = []
    76.5    | n_ptuple_paths 1 = []
    76.6    | n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1))
    76.7 -val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths
    76.8 +val ap_n_split = HOLogic.mk_ptupleabs o n_ptuple_paths
    76.9  
   76.10  val linear_pred_base_and_step_rhss =
   76.11    let
   76.12 @@ -2287,7 +2287,7 @@
   76.13        HOLogic.Collect_const tuple_T $ list_comb (Const base_x, outer_bounds)
   76.14      val step_set =
   76.15        HOLogic.Collect_const prod_T
   76.16 -      $ (Const (@{const_name uncurry}, curried_T --> uncurried_T)
   76.17 +      $ (Const (@{const_name case_prod}, curried_T --> uncurried_T)
   76.18                  $ list_comb (Const step_x, outer_bounds))
   76.19      val image_set =
   76.20        image_const $ (rtrancl_const $ step_set) $ base_set
    77.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Oct 13 09:21:14 2015 +0200
    77.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Oct 13 09:21:15 2015 +0200
    77.3 @@ -956,7 +956,7 @@
    77.4        (case t_compr of
    77.5          (Const (@{const_name Collect}, _) $ t) => t
    77.6        | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
    77.7 -    val (body, Ts, fp) = HOLogic.strip_psplits split
    77.8 +    val (body, Ts, fp) = HOLogic.strip_ptupleabs split
    77.9      val output_names = Name.variant_list (Term.add_free_names body [])
   77.10        (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
   77.11      val output_frees = rev (map2 (curry Free) output_names Ts)
    78.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Tue Oct 13 09:21:14 2015 +0200
    78.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Tue Oct 13 09:21:15 2015 +0200
    78.3 @@ -228,7 +228,7 @@
    78.4      val thy = Proof_Context.theory_of ctxt
    78.5      val nargs = length (binder_types (fastype_of pred))
    78.6      fun meta_eq_of th = th RS @{thm eq_reflection}
    78.7 -    val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]
    78.8 +    val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.inject}]
    78.9  
   78.10      fun instantiate i n ({context = ctxt2, prems, ...}: Subgoal.focus) =
   78.11        let
    79.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 13 09:21:14 2015 +0200
    79.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 13 09:21:15 2015 +0200
    79.3 @@ -884,9 +884,9 @@
    79.4      val intro'''' =
    79.5        Simplifier.full_simplify
    79.6          (put_simpset HOL_basic_ss ctxt
    79.7 -          addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
    79.8 +          addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.inject}])
    79.9        intro'''
   79.10 -    (* splitting conjunctions introduced by Pair_eq*)
   79.11 +    (* splitting conjunctions introduced by prod.inject*)
   79.12      val intro''''' = split_conjuncts_in_assms ctxt intro''''
   79.13    in
   79.14      intro'''''
    80.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 13 09:21:14 2015 +0200
    80.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 13 09:21:15 2015 +0200
    80.3 @@ -610,7 +610,7 @@
    80.4        | mk_tuple tTs = foldr1 mk_prod tTs
    80.5      fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t =
    80.6            absdummy T
    80.7 -            (HOLogic.split_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
    80.8 +            (HOLogic.case_prod_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
    80.9        | mk_split_abs T t = absdummy T t
   80.10      val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
   80.11      val (inargs, outargs) = split_mode mode args
   80.12 @@ -1023,7 +1023,7 @@
   80.13  
   80.14  (* Definition of executable functions and their intro and elim rules *)
   80.15  
   80.16 -fun strip_split_abs (Const (@{const_name uncurry}, _) $ t) = strip_split_abs t
   80.17 +fun strip_split_abs (Const (@{const_name case_prod}, _) $ t) = strip_split_abs t
   80.18    | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
   80.19    | strip_split_abs t = t
   80.20  
   80.21 @@ -1086,7 +1086,7 @@
   80.22      val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
   80.23      val simprules =
   80.24        [defthm, @{thm eval_pred},
   80.25 -        @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
   80.26 +        @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm prod.collapse}]
   80.27      val unfolddef_tac =
   80.28        Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simprules) 1
   80.29      val introthm = Goal.prove ctxt
   80.30 @@ -1748,7 +1748,7 @@
   80.31        (case t_compr of
   80.32          (Const (@{const_name Collect}, _) $ t) => t
   80.33        | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
   80.34 -    val (body, Ts, fp) = HOLogic.strip_psplits inner_t;
   80.35 +    val (body, Ts, fp) = HOLogic.strip_ptupleabs inner_t;
   80.36      val output_names = Name.variant_list (Term.add_free_names body [])
   80.37        (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
   80.38      val output_frees = map2 (curry Free) output_names (rev Ts)
    81.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Tue Oct 13 09:21:14 2015 +0200
    81.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Tue Oct 13 09:21:15 2015 +0200
    81.3 @@ -35,7 +35,7 @@
    81.4  
    81.5  val HOL_basic_ss' =
    81.6    simpset_of (put_simpset HOL_basic_ss @{context}
    81.7 -    addsimps @{thms simp_thms Pair_eq}
    81.8 +    addsimps @{thms simp_thms prod.inject}
    81.9      setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
   81.10      setSolver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI})))
   81.11  
   81.12 @@ -62,8 +62,8 @@
   81.13        (case f of
   81.14          Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
   81.15             [@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode,
   81.16 -           @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
   81.17 -           @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
   81.18 +           @{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv},
   81.19 +           @{thm snd_conv}, @{thm prod.collapse}, @{thm Product_Type.split_conv}]) 1
   81.20        | Free _ =>
   81.21          Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, ...} =>
   81.22            let
   81.23 @@ -232,8 +232,8 @@
   81.24                in
   81.25                  trace_tac ctxt options "before prove_neg_expr:"
   81.26                  THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
   81.27 -                  [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
   81.28 -                   @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
   81.29 +                  [@{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv},
   81.30 +                   @{thm snd_conv}, @{thm prod.collapse}, @{thm Product_Type.split_conv}]) 1
   81.31                  THEN (if (is_some name) then
   81.32                      trace_tac ctxt options "before applying not introduction rule"
   81.33                      THEN Subgoal.FOCUS_PREMS (fn {prems, ...} =>
   81.34 @@ -392,8 +392,8 @@
   81.35      val (in_ts, _) = split_mode mode ts;
   81.36      val split_simpset =
   81.37        put_simpset HOL_basic_ss' ctxt
   81.38 -      addsimps [@{thm split_eta}, @{thm split_beta},
   81.39 -        @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
   81.40 +      addsimps [@{thm case_prod_eta}, @{thm case_prod_beta},
   81.41 +        @{thm fst_conv}, @{thm snd_conv}, @{thm prod.collapse}]
   81.42      fun prove_prems2 out_ts [] =
   81.43        trace_tac ctxt options "before prove_match2 - last call:"
   81.44        THEN prove_match2 options ctxt out_ts
    82.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Oct 13 09:21:14 2015 +0200
    82.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Oct 13 09:21:15 2015 +0200
    82.3 @@ -152,7 +152,7 @@
    82.4  fun mk_full_equations functerms =
    82.5    let
    82.6      fun test_function T = Free ("f", termifyT T --> resultT)
    82.7 -    fun split_const T = HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, resultT)
    82.8 +    fun case_prod_const T = HOLogic.case_prod_const (T, @{typ "unit => Code_Evaluation.term"}, resultT)
    82.9      fun mk_call T =
   82.10        let
   82.11          val full_exhaustive =
   82.12 @@ -160,7 +160,7 @@
   82.13              full_exhaustiveT T)
   82.14        in                                   
   82.15          (T, fn t => full_exhaustive $
   82.16 -          (split_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
   82.17 +          (case_prod_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
   82.18        end
   82.19      fun mk_aux_call fTs (k, _) (tyco, Ts) =
   82.20        let
   82.21 @@ -168,7 +168,7 @@
   82.22          val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   82.23        in
   82.24          (T, fn t => nth functerms k $
   82.25 -          (split_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
   82.26 +          (case_prod_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
   82.27        end
   82.28      fun mk_consexpr simpleT (c, xs) =
   82.29        let
   82.30 @@ -387,11 +387,11 @@
   82.31      fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
   82.32        if Sign.of_sort thy (T, @{sort check_all}) then
   82.33          Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
   82.34 -          $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
   82.35 +          $ (HOLogic.case_prod_const (T, @{typ "unit => term"}, resultT)
   82.36              $ lambda free (lambda term_var t))
   82.37        else
   82.38          Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
   82.39 -          $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
   82.40 +          $ (HOLogic.case_prod_const (T, @{typ "unit => term"}, resultT)
   82.41              $ lambda free (lambda term_var t)) $ depth
   82.42      val none_t = Const (@{const_name "None"}, resultT)
   82.43      val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
    83.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Oct 13 09:21:14 2015 +0200
    83.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Oct 13 09:21:15 2015 +0200
    83.3 @@ -315,11 +315,11 @@
    83.4      fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
    83.5      fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
    83.6        liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    83.7 -    fun mk_split T = Sign.mk_const thy
    83.8 -      (@{const_name uncurry}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
    83.9 +    fun mk_case_prod T = Sign.mk_const thy
   83.10 +      (@{const_name case_prod}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
   83.11      fun mk_scomp_split T t t' =
   83.12        mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
   83.13 -        (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
   83.14 +        (mk_case_prod T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
   83.15      fun mk_bindclause (_, _, i, T) = mk_scomp_split T
   83.16        (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i);
   83.17    in
   83.18 @@ -361,11 +361,11 @@
   83.19      fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
   83.20      fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
   83.21        liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   83.22 -    fun mk_split T = Sign.mk_const thy
   83.23 -      (@{const_name uncurry}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
   83.24 +    fun mk_case_prod T = Sign.mk_const thy
   83.25 +      (@{const_name case_prod}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
   83.26      fun mk_scomp_split T t t' =
   83.27        mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
   83.28 -        (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
   83.29 +        (mk_case_prod T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
   83.30      fun mk_bindclause (_, _, i, T) = mk_scomp_split T
   83.31        (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i);
   83.32    in
    84.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Tue Oct 13 09:21:14 2015 +0200
    84.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Tue Oct 13 09:21:15 2015 +0200
    84.3 @@ -634,12 +634,12 @@
    84.4            end
    84.5        end
    84.6  
    84.7 -  | (((t1 as Const (@{const_name uncurry}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
    84.8 -     ((t2 as Const (@{const_name uncurry}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
    84.9 +  | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
   84.10 +     ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
   84.11         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
   84.12  
   84.13 -  | (((t1 as Const (@{const_name uncurry}, _)) $ Abs (v1, ty, s1)),
   84.14 -     ((t2 as Const (@{const_name uncurry}, _)) $ Abs (v2, _ , s2))) =>
   84.15 +  | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, s1)),
   84.16 +     ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , s2))) =>
   84.17         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
   84.18  
   84.19    | (t1 $ t2, t1' $ t2') =>
    85.1 --- a/src/HOL/Tools/hologic.ML	Tue Oct 13 09:21:14 2015 +0200
    85.2 +++ b/src/HOL/Tools/hologic.ML	Tue Oct 13 09:21:15 2015 +0200
    85.3 @@ -67,8 +67,8 @@
    85.4    val dest_prod: term -> term * term
    85.5    val mk_fst: term -> term
    85.6    val mk_snd: term -> term
    85.7 -  val split_const: typ * typ * typ -> term
    85.8 -  val mk_split: term -> term
    85.9 +  val case_prod_const: typ * typ * typ -> term
   85.10 +  val mk_case_prod: term -> term
   85.11    val flatten_tupleT: typ -> typ list
   85.12    val tupled_lambda: term -> term -> term
   85.13    val mk_tupleT: typ list -> typ
   85.14 @@ -81,8 +81,8 @@
   85.15    val mk_ptuple: int list list -> typ -> term list -> term
   85.16    val strip_ptuple: int list list -> term -> term list
   85.17    val flat_tuple_paths: term -> int list list
   85.18 -  val mk_psplits: int list list -> typ -> typ -> term -> term
   85.19 -  val strip_psplits: term -> term * typ list * int list list
   85.20 +  val mk_ptupleabs: int list list -> typ -> typ -> term -> term
   85.21 +  val strip_ptupleabs: term -> term * typ list * int list list
   85.22    val natT: typ
   85.23    val zero: term
   85.24    val is_zero: term -> bool
   85.25 @@ -348,14 +348,14 @@
   85.26      Const ("Product_Type.prod.snd", pT --> snd (dest_prodT pT)) $ p
   85.27    end;
   85.28  
   85.29 -fun split_const (A, B, C) =
   85.30 -  Const ("Product_Type.prod.uncurry", (A --> B --> C) --> mk_prodT (A, B) --> C);
   85.31 +fun case_prod_const (A, B, C) =
   85.32 +  Const ("Product_Type.prod.case_prod", (A --> B --> C) --> mk_prodT (A, B) --> C);
   85.33  
   85.34 -fun mk_split t =
   85.35 +fun mk_case_prod t =
   85.36    (case Term.fastype_of t of
   85.37      T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
   85.38 -      Const ("Product_Type.prod.uncurry", T --> mk_prodT (A, B) --> C) $ t
   85.39 -  | _ => raise TERM ("mk_split: bad body type", [t]));
   85.40 +      Const ("Product_Type.prod.case_prod", T --> mk_prodT (A, B) --> C) $ t
   85.41 +  | _ => raise TERM ("mk_case_prod: bad body type", [t]));
   85.42  
   85.43  (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
   85.44  fun flatten_tupleT (Type ("Product_Type.prod", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
   85.45 @@ -365,7 +365,7 @@
   85.46  fun tupled_lambda (x as Free _) b = lambda x b
   85.47    | tupled_lambda (x as Var _) b = lambda x b
   85.48    | tupled_lambda (Const ("Product_Type.Pair", _) $ u $ v) b =
   85.49 -      mk_split (tupled_lambda u (tupled_lambda v b))
   85.50 +      mk_case_prod (tupled_lambda u (tupled_lambda v b))
   85.51    | tupled_lambda (Const ("Product_Type.Unity", _)) b =
   85.52        Abs ("x", unitT, b)
   85.53    | tupled_lambda t _ = raise TERM ("tupled_lambda: bad tuple", [t]);
   85.54 @@ -450,27 +450,27 @@
   85.55        | factors p _ = []
   85.56    in factors [] end;
   85.57  
   85.58 -(*In mk_psplits ps S T u, term u expects separate arguments for the factors of S,
   85.59 +(*In mk_ptupleabs ps S T u, term u expects separate arguments for the factors of S,
   85.60    with result type T.  The call creates a new term expecting one argument
   85.61    of type S.*)
   85.62 -fun mk_psplits ps T T3 u =
   85.63 +fun mk_ptupleabs ps T T3 u =
   85.64    let
   85.65      fun ap ((p, T) :: pTs) =
   85.66            if member (op =) ps p then (case T of
   85.67                Type ("Product_Type.prod", [T1, T2]) =>
   85.68 -                split_const (T1, T2, map snd pTs ---> T3) $
   85.69 +                case_prod_const (T1, T2, map snd pTs ---> T3) $
   85.70                    ap ((1::p, T1) :: (2::p, T2) :: pTs)
   85.71 -            | _ => ptuple_err "mk_psplits")
   85.72 +            | _ => ptuple_err "mk_ptupleabs")
   85.73            else Abs ("x", T, ap pTs)
   85.74        | ap [] =
   85.75            let val k = length ps
   85.76            in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   85.77    in ap [([], T)] end;
   85.78  
   85.79 -val strip_psplits =
   85.80 +val strip_ptupleabs =
   85.81    let
   85.82      fun strip [] qs Ts t = (t, rev Ts, qs)
   85.83 -      | strip (p :: ps) qs Ts (Const ("Product_Type.prod.uncurry", _) $ t) =
   85.84 +      | strip (p :: ps) qs Ts (Const ("Product_Type.prod.case_prod", _) $ t) =
   85.85            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
   85.86        | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
   85.87        | strip (p :: ps) qs Ts t = strip ps qs
    86.1 --- a/src/HOL/Tools/inductive_set.ML	Tue Oct 13 09:21:14 2015 +0200
    86.2 +++ b/src/HOL/Tools/inductive_set.ML	Tue Oct 13 09:21:15 2015 +0200
    86.3 @@ -55,7 +55,7 @@
    86.4          fun mk_collect p T t =
    86.5            let val U = HOLogic.dest_setT T
    86.6            in HOLogic.Collect_const U $
    86.7 -            HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
    86.8 +            HOLogic.mk_ptupleabs (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
    86.9            end;
   86.10          fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member},
   86.11                Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
   86.12 @@ -66,7 +66,7 @@
   86.13            | decomp _ = NONE;
   86.14          val simp =
   86.15            full_simp_tac
   86.16 -            (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]) 1;
   86.17 +            (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm case_prod_conv}]) 1;
   86.18          fun mk_rew t = (case strip_abs_vars t of
   86.19              [] => NONE
   86.20            | xs => (case decomp (strip_abs_body t) of
   86.21 @@ -211,7 +211,7 @@
   86.22        (dest_Var x,
   86.23         Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
   86.24           (HOLogic.Collect_const U $
   86.25 -            HOLogic.mk_psplits ps U HOLogic.boolT
   86.26 +            HOLogic.mk_ptupleabs ps U HOLogic.boolT
   86.27                (list_comb (x', map Bound (length Ts - 1 downto 0))))))
   86.28      end) fs;
   86.29  
   86.30 @@ -232,11 +232,11 @@
   86.31            in
   86.32              thm' RS (infer_instantiate ctxt [(arg_cong_f,
   86.33                Thm.cterm_of ctxt (Abs ("P", Ts ---> HOLogic.boolT,
   86.34 -                HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
   86.35 +                HOLogic.Collect_const U $ HOLogic.mk_ptupleabs fs' U
   86.36                    HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
   86.37            end)
   86.38    in
   86.39 -    Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]
   86.40 +    Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm case_prod_conv}]
   86.41        addsimprocs [@{simproc Collect_mem}]) thm'' |>
   86.42          zero_var_indexes |> eta_contract_thm ctxt (equal p)
   86.43    end;
   86.44 @@ -344,7 +344,7 @@
   86.45      thm |>
   86.46      Thm.instantiate ([], insts) |>
   86.47      Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
   86.48 -      [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
   86.49 +      [to_pred_simproc (mem_Collect_eq :: @{thm case_prod_conv} :: to_pred_simps)]) |>
   86.50      eta_contract_thm ctxt (is_pred pred_arities) |>
   86.51      Rule_Cases.save thm
   86.52    end;
   86.53 @@ -415,7 +415,7 @@
   86.54            in
   86.55              (x, (x',
   86.56                (HOLogic.Collect_const T $
   86.57 -                 HOLogic.mk_psplits fs T HOLogic.boolT x',
   86.58 +                 HOLogic.mk_ptupleabs fs T HOLogic.boolT x',
   86.59                 fold_rev (Term.abs o pair "x") Ts
   86.60                   (HOLogic.mk_mem
   86.61                     (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)), x)))))
   86.62 @@ -442,12 +442,12 @@
   86.63        in
   86.64          ((c', (fs, U, Ts)),
   86.65           (list_comb (c, params2),
   86.66 -          HOLogic.Collect_const U $ HOLogic.mk_psplits fs U HOLogic.boolT
   86.67 +          HOLogic.Collect_const U $ HOLogic.mk_ptupleabs fs U HOLogic.boolT
   86.68              (list_comb (c', params1))))
   86.69        end) |> split_list |>> split_list;
   86.70      val eqns' = eqns @
   86.71        map (Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq)
   86.72 -        (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps);
   86.73 +        (mem_Collect_eq :: @{thm case_prod_conv} :: to_pred_simps);
   86.74  
   86.75      (* predicate version of the introduction rules *)
   86.76      val intros' =
   86.77 @@ -472,7 +472,7 @@
   86.78        |> fold_map Local_Theory.define
   86.79          (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
   86.80             fold_rev lambda params (HOLogic.Collect_const U $
   86.81 -             HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
   86.82 +             HOLogic.mk_ptupleabs fs U HOLogic.boolT (list_comb (p, params3))))))
   86.83             (cnames_syn ~~ cs_info ~~ preds));
   86.84  
   86.85      (* prove theorems for converting predicate to set notation *)
   86.86 @@ -487,7 +487,7 @@
   86.87                    list_comb (c, params))))))
   86.88              (K (REPEAT (resolve_tac lthy @{thms ext} 1) THEN
   86.89                simp_tac (put_simpset HOL_basic_ss lthy addsimps
   86.90 -                [def, mem_Collect_eq, @{thm split_conv}]) 1))
   86.91 +                [def, mem_Collect_eq, @{thm case_prod_conv}]) 1))
   86.92          in
   86.93            lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
   86.94              [Attrib.internal (K pred_set_conv_att)]),
   86.95 @@ -542,7 +542,7 @@
   86.96        "declare of monotonicity rule for set operators");
   86.97  
   86.98  
   86.99 -(* commands *)
  86.100 +(* commands *)                           
  86.101  
  86.102  val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
  86.103  
    87.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Oct 13 09:21:14 2015 +0200
    87.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Oct 13 09:21:15 2015 +0200
    87.3 @@ -85,14 +85,14 @@
    87.4  
    87.5  fun mk_split_abs vs (Bound i) t = let val (x, T) = nth vs i in Abs (x, T, t) end
    87.6    | mk_split_abs vs (Const (@{const_name Product_Type.Pair}, _) $ u $ v) t =
    87.7 -      HOLogic.mk_split (mk_split_abs vs u (mk_split_abs vs v t))
    87.8 +      HOLogic.mk_case_prod (mk_split_abs vs u (mk_split_abs vs v t))
    87.9    | mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]);
   87.10  
   87.11 -(* a variant of HOLogic.strip_psplits *)
   87.12 -val strip_psplits =
   87.13 +(* a variant of HOLogic.strip_ptupleabs *)
   87.14 +val strip_ptupleabs =
   87.15    let
   87.16      fun strip [] qs vs t = (t, rev vs, qs)
   87.17 -      | strip (p :: ps) qs vs (Const (@{const_name uncurry}, _) $ t) =
   87.18 +      | strip (p :: ps) qs vs (Const (@{const_name case_prod}, _) $ t) =
   87.19            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t
   87.20        | strip (_ :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t
   87.21        | strip (_ :: ps) qs vs t = strip ps qs
   87.22 @@ -129,11 +129,11 @@
   87.23    | is_collect_atom (Atom (_, Const (@{const_name "Groups.uminus_class.uminus"}, _) $ (Const(@{const_name Collect}, _) $ _))) = true
   87.24    | is_collect_atom _ = false
   87.25  
   87.26 -fun mk_split _ [(x, T)] t = (T, Abs (x, T, t))
   87.27 -  | mk_split rT ((x, T) :: vs) t =
   87.28 +fun mk_case_prod _ [(x, T)] t = (T, Abs (x, T, t))
   87.29 +  | mk_case_prod rT ((x, T) :: vs) t =
   87.30      let
   87.31 -      val (T', t') = mk_split rT vs t
   87.32 -      val t'' = HOLogic.split_const (T, T', rT) $ (Abs (x, T, t'))
   87.33 +      val (T', t') = mk_case_prod rT vs t
   87.34 +      val t'' = HOLogic.case_prod_const (T, T', rT) $ (Abs (x, T, t'))
   87.35      in (domain_type (fastype_of t''), t'') end
   87.36  
   87.37  fun mk_term vs t =
   87.38 @@ -151,7 +151,7 @@
   87.39    let
   87.40      val (tuple, (vs', t')) = mk_term vs t
   87.41      val T = HOLogic.mk_tupleT (map snd vs')
   87.42 -    val s = HOLogic.Collect_const T $ (snd (mk_split @{typ bool} vs' t'))
   87.43 +    val s = HOLogic.Collect_const T $ (snd (mk_case_prod @{typ bool} vs' t'))
   87.44    in
   87.45      (tuple, Atom (tuple, s))
   87.46    end
   87.47 @@ -166,7 +166,7 @@
   87.48          let
   87.49            val (tuple, (vs', x')) = mk_term vs x 
   87.50            val rT = HOLogic.dest_setT (fastype_of s)
   87.51 -          val s = mk_vimage (snd (mk_split rT vs' x')) s
   87.52 +          val s = mk_vimage (snd (mk_case_prod rT vs' x')) s
   87.53          in (tuple, Atom (tuple, s)) end)
   87.54    | mk_atom vs (Const (@{const_name "HOL.Not"}, _) $ t) = apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t)
   87.55    | mk_atom vs t = default_atom vs t
   87.56 @@ -219,7 +219,7 @@
   87.57      val bs = map (fn b => the (AList.lookup (op =) subst b)) pat'
   87.58      val rt = term_of_pattern Ts' (Pattern bs)
   87.59      val rT = type_of_pattern Ts' (Pattern bs)
   87.60 -    val (_, f) = mk_split rT vs' rt
   87.61 +    val (_, f) = mk_case_prod rT vs' rt
   87.62    in
   87.63      mk_image f t
   87.64    end;
   87.65 @@ -269,7 +269,7 @@
   87.66    end;
   87.67  
   87.68  fun is_reordering t =
   87.69 -  let val (t', _, _) = HOLogic.strip_psplits t
   87.70 +  let val (t', _, _) = HOLogic.strip_ptupleabs t
   87.71    in forall (fn Bound _ => true) (HOLogic.strip_tuple t') end
   87.72  
   87.73  fun mk_pointfree_expr t =
   87.74 @@ -305,7 +305,7 @@
   87.75  
   87.76  (* proof tactic *)
   87.77  
   87.78 -val case_prod_distrib = @{lemma "(uncurry g x) z = uncurry (\<lambda>x y. (g x y) z) x" by (simp add: case_prod_beta)}
   87.79 +val case_prod_beta = @{lemma "case_prod g x z = case_prod (\<lambda>x y. (g x y) z) x" by (simp add: case_prod_beta)}
   87.80  
   87.81  val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp}
   87.82  val vimageE' =
   87.83 @@ -327,7 +327,7 @@
   87.84        ORELSE' resolve_tac ctxt @{thms arg_cong2 [OF refl, where f = "op =", OF prod.case, THEN iffD2]}
   87.85        ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
   87.86          (HOLogic.Trueprop_conv
   87.87 -          (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_distrib)))))) ctxt)))
   87.88 +          (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_beta)))))) ctxt)))
   87.89  
   87.90  fun elim_image_tac ctxt =
   87.91    eresolve_tac ctxt @{thms imageE}
   87.92 @@ -421,7 +421,7 @@
   87.93      fun mk_term t =
   87.94        let
   87.95          val (T, t') = dest_Collect t
   87.96 -        val (t'', vs, fp) = case strip_psplits t' of
   87.97 +        val (t'', vs, fp) = case strip_ptupleabs t' of
   87.98              (_, [_], _) => raise TERM("mk_term", [t'])
   87.99            | (t'', vs, fp) => (t'', vs, fp)
  87.100          val Ts = map snd vs
    88.1 --- a/src/HOL/Tools/split_rule.ML	Tue Oct 13 09:21:14 2015 +0200
    88.2 +++ b/src/HOL/Tools/split_rule.ML	Tue Oct 13 09:21:15 2015 +0200
    88.3 @@ -16,13 +16,13 @@
    88.4  
    88.5  (** split rules **)
    88.6  
    88.7 -fun internal_split_const (Ta, Tb, Tc) =
    88.8 -  Const (@{const_name Product_Type.internal_split},
    88.9 +fun internal_case_prod_const (Ta, Tb, Tc) =
   88.10 +  Const (@{const_name Product_Type.internal_case_prod},
   88.11      [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
   88.12  
   88.13  fun eval_internal_split ctxt =
   88.14 -  hol_simplify ctxt @{thms internal_split_def} o
   88.15 -  hol_simplify ctxt @{thms internal_split_conv};
   88.16 +  hol_simplify ctxt @{thms internal_case_prod_def} o
   88.17 +  hol_simplify ctxt @{thms internal_case_prod_conv};
   88.18  
   88.19  fun remove_internal_split ctxt = eval_internal_split ctxt o split_all ctxt;
   88.20  
   88.21 @@ -31,7 +31,7 @@
   88.22    with result type T.  The call creates a new term expecting one argument
   88.23    of type S.*)
   88.24  fun ap_split (Type (@{type_name Product_Type.prod}, [T1, T2])) T3 u =
   88.25 -      internal_split_const (T1, T2, T3) $
   88.26 +      internal_case_prod_const (T1, T2, T3) $
   88.27        Abs ("v", T1,
   88.28            ap_split T2 T3
   88.29               ((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $
    89.1 --- a/src/HOL/Transitive_Closure.thy	Tue Oct 13 09:21:14 2015 +0200
    89.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Oct 13 09:21:15 2015 +0200
    89.3 @@ -898,7 +898,7 @@
    89.4  lemma rtranclp_imp_Sup_relpowp:
    89.5    assumes "(P^**) x y"
    89.6    shows "(\<Squnion>n. P ^^ n) x y"
    89.7 -  using assms and rtrancl_imp_UN_relpow [to_pred] by blast
    89.8 +  using assms and rtrancl_imp_UN_relpow [of "(x, y)", to_pred] by simp
    89.9  
   89.10  lemma relpow_imp_rtrancl:
   89.11    assumes "p \<in> R ^^ n"
   89.12 @@ -918,7 +918,7 @@
   89.13  lemma relpowp_imp_rtranclp:
   89.14    assumes "(P ^^ n) x y"
   89.15    shows "(P^**) x y"
   89.16 -  using assms and relpow_imp_rtrancl [to_pred] by blast
   89.17 +  using assms and relpow_imp_rtrancl [of "(x, y)", to_pred] by simp
   89.18  
   89.19  lemma rtrancl_is_UN_relpow:
   89.20    "R^* = (\<Union>n. R ^^ n)"
    90.1 --- a/src/HOL/UNITY/Comp.thy	Tue Oct 13 09:21:14 2015 +0200
    90.2 +++ b/src/HOL/UNITY/Comp.thy	Tue Oct 13 09:21:15 2015 +0200
    90.3 @@ -186,7 +186,7 @@
    90.4  apply simp
    90.5  apply (subgoal_tac "G \<in> preserves (funPair v w) ")
    90.6   prefer 2 apply simp
    90.7 -apply (drule_tac P1 = "split Q" for Q in preserves_subset_stable [THEN subsetD], 
    90.8 +apply (drule_tac P1 = "case_prod Q" for Q in preserves_subset_stable [THEN subsetD], 
    90.9         auto)
   90.10  done
   90.11  
    91.1 --- a/src/HOL/UNITY/Extend.thy	Tue Oct 13 09:21:14 2015 +0200
    91.2 +++ b/src/HOL/UNITY/Extend.thy	Tue Oct 13 09:21:15 2015 +0200
    91.3 @@ -127,7 +127,7 @@
    91.4       assumes surj_h: "surj h"
    91.5           and prem:   "!! x y. g (h(x,y)) = x"
    91.6       shows "fst (inv h z) = g z"
    91.7 -by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h)
    91.8 +by (metis UNIV_I f_inv_into_f prod.collapse prem surj_h)
    91.9  
   91.10  
   91.11  subsection{*Trivial properties of f, g, h*}
    92.1 --- a/src/HOL/Wellfounded.thy	Tue Oct 13 09:21:14 2015 +0200
    92.2 +++ b/src/HOL/Wellfounded.thy	Tue Oct 13 09:21:15 2015 +0200
    92.3 @@ -68,7 +68,7 @@
    92.4    assumes lin: "OFCLASS('a::ord, linorder_class)"
    92.5    shows "OFCLASS('a::ord, wellorder_class)"
    92.6  using lin by (rule wellorder_class.intro)
    92.7 -  (blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf])
    92.8 +  (rule class.wellorder_axioms.intro, rule wf_induct_rule [OF wf], simp)
    92.9  
   92.10  lemma (in wellorder) wf:
   92.11    "wf {(x, y). x < y}"
    93.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Tue Oct 13 09:21:14 2015 +0200
    93.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Oct 13 09:21:15 2015 +0200
    93.3 @@ -14,7 +14,7 @@
    93.4  
    93.5  definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
    93.6  where
    93.7 -  "map2 f as bs = map (split f) (zip as bs)"
    93.8 +  "map2 f as bs = map (case_prod f) (zip as bs)"
    93.9  
   93.10  lemma map2_Nil [simp, code]:
   93.11    "map2 f [] ys = []"
    94.1 --- a/src/HOL/Word/Word.thy	Tue Oct 13 09:21:14 2015 +0200
    94.2 +++ b/src/HOL/Word/Word.thy	Tue Oct 13 09:21:15 2015 +0200
    94.3 @@ -3836,7 +3836,7 @@
    94.4  lemma word_rsplit_empty_iff_size:
    94.5    "(word_rsplit w = []) = (size w = 0)" 
    94.6    unfolding word_rsplit_def bin_rsplit_def word_size
    94.7 -  by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
    94.8 +  by (simp add: bin_rsplit_aux_simp_alt Let_def split: prod.split)
    94.9  
   94.10  lemma test_bit_rsplit:
   94.11    "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a :: len word) \<Longrightarrow> 
    95.1 --- a/src/HOL/ex/FinFunPred.thy	Tue Oct 13 09:21:14 2015 +0200
    95.2 +++ b/src/HOL/ex/FinFunPred.thy	Tue Oct 13 09:21:15 2015 +0200
    95.3 @@ -78,7 +78,7 @@
    95.4  by(intro_classes)(simp add: sup_finfun_def inf_finfun_def expand_finfun_eq o_def sup_inf_distrib1)
    95.5  
    95.6  instantiation "finfun" :: (type, minus) minus begin
    95.7 -definition "f - g = split (op -) \<circ>$ ($f, g$)"
    95.8 +definition "f - g = case_prod (op -) \<circ>$ ($f, g$)"
    95.9  instance ..
   95.10  end
   95.11  
    96.1 --- a/src/HOL/ex/Gauge_Integration.thy	Tue Oct 13 09:21:14 2015 +0200
    96.2 +++ b/src/HOL/ex/Gauge_Integration.thy	Tue Oct 13 09:21:15 2015 +0200
    96.3 @@ -45,7 +45,7 @@
    96.4        \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
    96.5  
    96.6  lemmas fine_induct [induct set: fine] =
    96.7 -  fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv] for \<delta> a b D P
    96.8 +  fine.induct [of "\<delta>" "(a,b)" "D" "case_prod P", unfolded split_conv] for \<delta> a b D P
    96.9  
   96.10  lemma fine_single:
   96.11    "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
    97.1 --- a/src/HOL/ex/Normalization_by_Evaluation.thy	Tue Oct 13 09:21:14 2015 +0200
    97.2 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Tue Oct 13 09:21:15 2015 +0200
    97.3 @@ -54,7 +54,7 @@
    97.4  lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization
    97.5  
    97.6  lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization
    97.7 -lemma "split (%x y. x) (a, b) = a" by normalization
    97.8 +lemma "case_prod (%x y. x) (a, b) = a" by normalization
    97.9  lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization
   97.10  
   97.11  lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization