prefer "uncurry" as canonical name for case distinction on products in combinatorial view
authorhaftmann
Sun Sep 06 22:14:51 2015 +0200 (2015-09-06)
changeset 611254c68426800de
parent 61124 e70daf0d0fad
child 61126 e6b1236f9b3d
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
NEWS
src/HOL/Hoare/hoare_syntax.ML
src/HOL/Hoare/hoare_tac.ML
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Library/old_recdef.ML
src/HOL/Probability/Probability_Measure.thy
src/HOL/Product_Type.thy
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/set_comprehension_pointfree.ML
     1.1 --- a/NEWS	Sun Sep 06 22:14:51 2015 +0200
     1.2 +++ b/NEWS	Sun Sep 06 22:14:51 2015 +0200
     1.3 @@ -187,6 +187,10 @@
     1.4  constant and its defining fact become qualified, e.g. Option.is_none and
     1.5  Option.is_none_def. Occasional INCOMPATIBILITY in applications.
     1.6  
     1.7 +* Combinator to represent case distinction on products is named "uncurry",
     1.8 +with "split" and "prod_case" retained as input abbreviations.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * Some old and rarely used ASCII replacement syntax has been removed.
    1.12  INCOMPATIBILITY, standard syntax with symbols should be used instead.
    1.13  The subsequent commands help to reproduce the old forms, e.g. to
     2.1 --- a/src/HOL/Hoare/hoare_syntax.ML	Sun Sep 06 22:14:51 2015 +0200
     2.2 +++ b/src/HOL/Hoare/hoare_syntax.ML	Sun Sep 06 22:14:51 2015 +0200
     2.3 @@ -28,7 +28,7 @@
     2.4  
     2.5  fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
     2.6    | mk_abstuple (x :: xs) body =
     2.7 -      Syntax.const @{const_syntax case_prod} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
     2.8 +      Syntax.const @{const_syntax uncurry} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
     2.9  
    2.10  fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
    2.11    | mk_fbody x e (y :: xs) =
    2.12 @@ -82,21 +82,21 @@
    2.13  local
    2.14  
    2.15  fun dest_abstuple
    2.16 -      (Const (@{const_syntax case_prod}, _) $ Abs (v, _, body)) =
    2.17 +      (Const (@{const_syntax uncurry}, _) $ Abs (v, _, body)) =
    2.18          subst_bound (Syntax.free v, dest_abstuple body)
    2.19    | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
    2.20    | dest_abstuple tm = tm;
    2.21  
    2.22 -fun abs2list (Const (@{const_syntax case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
    2.23 +fun abs2list (Const (@{const_syntax uncurry}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
    2.24    | abs2list (Abs (x, T, _)) = [Free (x, T)]
    2.25    | abs2list _ = [];
    2.26  
    2.27 -fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (_, _, t)) = mk_ts t
    2.28 +fun mk_ts (Const (@{const_syntax uncurry}, _) $ Abs (_, _, t)) = mk_ts t
    2.29    | mk_ts (Abs (_, _, t)) = mk_ts t
    2.30    | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
    2.31    | mk_ts t = [t];
    2.32  
    2.33 -fun mk_vts (Const (@{const_syntax case_prod},_) $ Abs (x, _, t)) =
    2.34 +fun mk_vts (Const (@{const_syntax uncurry},_) $ Abs (x, _, t)) =
    2.35        (Syntax.free x :: abs2list t, mk_ts t)
    2.36    | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
    2.37    | mk_vts _ = raise Match;
    2.38 @@ -106,7 +106,7 @@
    2.39        if t = Bound i then find_ch vts (i - 1) xs
    2.40        else (true, (v, subst_bounds (xs, t)));
    2.41  
    2.42 -fun is_f (Const (@{const_syntax case_prod}, _) $ Abs _) = true
    2.43 +fun is_f (Const (@{const_syntax uncurry}, _) $ Abs _) = true
    2.44    | is_f (Abs _) = true
    2.45    | is_f _ = false;
    2.46  
     3.1 --- a/src/HOL/Hoare/hoare_tac.ML	Sun Sep 06 22:14:51 2015 +0200
     3.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Sun Sep 06 22:14:51 2015 +0200
     3.3 @@ -26,7 +26,7 @@
     3.4  local
     3.5  
     3.6  (** maps (%x1 ... xn. t) to [x1,...,xn] **)
     3.7 -fun abs2list (Const (@{const_name case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
     3.8 +fun abs2list (Const (@{const_name uncurry}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
     3.9    | abs2list (Abs (x, T, _)) = [Free (x, T)]
    3.10    | abs2list _ = [];
    3.11  
    3.12 @@ -47,7 +47,7 @@
    3.13              Abs (_, T, _) => T
    3.14            | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
    3.15        in
    3.16 -        Const (@{const_name case_prod},
    3.17 +        Const (@{const_name uncurry},
    3.18              (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
    3.19            absfree (x, T) z
    3.20        end;
     4.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Sun Sep 06 22:14:51 2015 +0200
     4.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Sun Sep 06 22:14:51 2015 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4  
     4.5  section \<open>Pairs\<close>
     4.6  
     4.7 -setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}]\<close>
     4.8 +setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name uncurry}]\<close>
     4.9  
    4.10  section \<open>Filters\<close>
    4.11  
     5.1 --- a/src/HOL/Library/old_recdef.ML	Sun Sep 06 22:14:51 2015 +0200
     5.2 +++ b/src/HOL/Library/old_recdef.ML	Sun Sep 06 22:14:51 2015 +0200
     5.3 @@ -551,7 +551,7 @@
     5.4  
     5.5  local
     5.6  fun mk_uncurry (xt, yt, zt) =
     5.7 -    Const(@{const_name case_prod}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
     5.8 +    Const(@{const_name uncurry}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
     5.9  fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
    5.10    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
    5.11  fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
    5.12 @@ -631,7 +631,7 @@
    5.13    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
    5.14  
    5.15  
    5.16 -local  fun ucheck t = (if #Name (dest_const t) = @{const_name case_prod} then t
    5.17 +local  fun ucheck t = (if #Name (dest_const t) = @{const_name uncurry} then t
    5.18                         else raise Match)
    5.19  in
    5.20  fun dest_pabs used tm =
     6.1 --- a/src/HOL/Probability/Probability_Measure.thy	Sun Sep 06 22:14:51 2015 +0200
     6.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Sun Sep 06 22:14:51 2015 +0200
     6.3 @@ -278,7 +278,7 @@
     6.4              in
     6.5                go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t
     6.6              end
     6.7 -        | go pattern elem (Const (@{const_syntax case_prod}, _) $ t) =
     6.8 +        | go pattern elem (Const (@{const_syntax uncurry}, _) $ t) =
     6.9              go 
    6.10                ((Syntax.const @{syntax_const "_pattern"}, 2) :: pattern)
    6.11                (Syntax.const @{const_syntax Pair} :: elem)
     7.1 --- a/src/HOL/Product_Type.thy	Sun Sep 06 22:14:51 2015 +0200
     7.2 +++ b/src/HOL/Product_Type.thy	Sun Sep 06 22:14:51 2015 +0200
     7.3 @@ -240,7 +240,7 @@
     7.4  lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
     7.5    by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
     7.6  
     7.7 -free_constructors case_prod for Pair fst snd
     7.8 +free_constructors uncurry for Pair fst snd
     7.9  proof -
    7.10    fix P :: bool and p :: "'a \<times> 'b"
    7.11    show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
    7.12 @@ -304,8 +304,8 @@
    7.13    "_pattern x y" \<rightleftharpoons> "CONST Pair x y"
    7.14    "_patterns x y" \<rightleftharpoons> "CONST Pair x y"
    7.15    "_tuple x (_tuple_args y z)" \<rightleftharpoons> "_tuple x (_tuple_arg (_tuple y z))"
    7.16 -  "\<lambda>(x, y, zs). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x (y, zs). b)"
    7.17 -  "\<lambda>(x, y). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x y. b)"
    7.18 +  "\<lambda>(x, y, zs). b" \<rightleftharpoons> "CONST uncurry (\<lambda>x (y, zs). b)"
    7.19 +  "\<lambda>(x, y). b" \<rightleftharpoons> "CONST uncurry (\<lambda>x y. b)"
    7.20    "_abs (CONST Pair x y) t" \<rightharpoonup> "\<lambda>(x, y). t"
    7.21    -- \<open>This rule accommodates tuples in @{text "case C \<dots> (x, y) \<dots> \<Rightarrow> \<dots>"}:
    7.22       The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic},
    7.23 @@ -317,7 +317,7 @@
    7.24      fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
    7.25        | split_guess_names_tr' T [Abs (x, xT, t)] =
    7.26            (case (head_of t) of
    7.27 -            Const (@{const_syntax case_prod}, _) => raise Match
    7.28 +            Const (@{const_syntax uncurry}, _) => raise Match
    7.29            | _ =>
    7.30              let 
    7.31                val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
    7.32 @@ -329,7 +329,7 @@
    7.33              end)
    7.34        | split_guess_names_tr' T [t] =
    7.35            (case head_of t of
    7.36 -            Const (@{const_syntax case_prod}, _) => raise Match
    7.37 +            Const (@{const_syntax uncurry}, _) => raise Match
    7.38            | _ =>
    7.39              let
    7.40                val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
    7.41 @@ -341,7 +341,7 @@
    7.42                  (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
    7.43              end)
    7.44        | split_guess_names_tr' _ _ = raise Match;
    7.45 -  in [(@{const_syntax case_prod}, K split_guess_names_tr')] end
    7.46 +  in [(@{const_syntax uncurry}, K split_guess_names_tr')] end
    7.47  \<close>
    7.48  
    7.49  
    7.50 @@ -379,7 +379,7 @@
    7.51    constant fst \<rightharpoonup> (Haskell) "fst"
    7.52  | constant snd \<rightharpoonup> (Haskell) "snd"
    7.53  
    7.54 -lemma case_prod_unfold [nitpick_unfold]: "case_prod = (%c p. c (fst p) (snd p))"
    7.55 +lemma case_prod_unfold [nitpick_unfold]: "uncurry = (%c p. c (fst p) (snd p))"
    7.56    by (simp add: fun_eq_iff split: prod.split)
    7.57  
    7.58  lemma fst_eqD: "fst (x, y) = a ==> x = a"
    7.59 @@ -396,13 +396,13 @@
    7.60  lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
    7.61    by (simp add: prod_eq_iff)
    7.62  
    7.63 -lemma split_conv [simp, code]: "case_prod f (a, b) = f a b"
    7.64 +lemma split_conv [simp, code]: "uncurry f (a, b) = f a b"
    7.65    by (fact prod.case)
    7.66  
    7.67 -lemma splitI: "f a b \<Longrightarrow> case_prod f (a, b)"
    7.68 +lemma splitI: "f a b \<Longrightarrow> uncurry f (a, b)"
    7.69    by (rule split_conv [THEN iffD2])
    7.70  
    7.71 -lemma splitD: "case_prod f (a, b) \<Longrightarrow> f a b"
    7.72 +lemma splitD: "uncurry f (a, b) \<Longrightarrow> f a b"
    7.73    by (rule split_conv [THEN iffD1])
    7.74  
    7.75  lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
    7.76 @@ -412,13 +412,13 @@
    7.77    -- \<open>Subsumes the old @{text split_Pair} when @{term f} is the identity function.\<close>
    7.78    by (simp add: fun_eq_iff split: prod.split)
    7.79  
    7.80 -lemma split_comp: "case_prod (f \<circ> g) x = f (g (fst x)) (snd x)"
    7.81 +lemma split_comp: "uncurry (f \<circ> g) x = f (g (fst x)) (snd x)"
    7.82    by (cases x) simp
    7.83  
    7.84 -lemma split_twice: "case_prod f (case_prod g p) = case_prod (\<lambda>x y. case_prod f (g x y)) p"
    7.85 +lemma split_twice: "uncurry f (uncurry g p) = uncurry (\<lambda>x y. uncurry f (g x y)) p"
    7.86    by (fact prod.case_distrib)
    7.87  
    7.88 -lemma The_split: "The (case_prod P) = (THE xy. P (fst xy) (snd xy))"
    7.89 +lemma The_split: "The (uncurry P) = (THE xy. P (fst xy) (snd xy))"
    7.90    by (simp add: case_prod_unfold)
    7.91  
    7.92  lemmas split_weak_cong = prod.case_cong_weak
    7.93 @@ -438,7 +438,7 @@
    7.94    from \<open>PROP P (fst x, snd x)\<close> show "PROP P x" by simp
    7.95  qed
    7.96  
    7.97 -lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
    7.98 +lemma uncurry_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
    7.99    by (cases x) simp
   7.100  
   7.101  text \<open>
   7.102 @@ -510,7 +510,7 @@
   7.103      | no_args k i (Bound m) = m < k orelse m > k + i
   7.104      | no_args _ _ _ = true;
   7.105    fun split_pat tp i (Abs  (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
   7.106 -    | split_pat tp i (Const (@{const_name case_prod}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
   7.107 +    | split_pat tp i (Const (@{const_name uncurry}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
   7.108      | split_pat tp i _ = NONE;
   7.109    fun metaeq ctxt lhs rhs = mk_meta_eq (Goal.prove ctxt [] []
   7.110          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
   7.111 @@ -528,12 +528,12 @@
   7.112          else (subst arg k i t $ subst arg k i u)
   7.113      | subst arg k i t = t;
   7.114  in
   7.115 -  fun beta_proc ctxt (s as Const (@{const_name case_prod}, _) $ Abs (_, _, t) $ arg) =
   7.116 +  fun beta_proc ctxt (s as Const (@{const_name uncurry}, _) $ Abs (_, _, t) $ arg) =
   7.117          (case split_pat beta_term_pat 1 t of
   7.118            SOME (i, f) => SOME (metaeq ctxt s (subst arg 0 i f))
   7.119          | NONE => NONE)
   7.120      | beta_proc _ _ = NONE;
   7.121 -  fun eta_proc ctxt (s as Const (@{const_name case_prod}, _) $ Abs (_, _, t)) =
   7.122 +  fun eta_proc ctxt (s as Const (@{const_name uncurry}, _) $ Abs (_, _, t)) =
   7.123          (case split_pat eta_term_pat 1 t of
   7.124            SOME (_, ft) => SOME (metaeq ctxt s (let val f $ _ = ft in f end))
   7.125          | NONE => NONE)
   7.126 @@ -563,31 +563,31 @@
   7.127  lemmas split_split_asm [no_atp] = prod.split_asm
   7.128  
   7.129  text \<open>
   7.130 -  \medskip @{const case_prod} used as a logical connective or set former.
   7.131 +  \medskip @{const uncurry} used as a logical connective or set former.
   7.132  
   7.133    \medskip These rules are for use with @{text blast}; could instead
   7.134    call @{text simp} using @{thm [source] prod.split} as rewrite.\<close>
   7.135  
   7.136 -lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case_prod c p"
   7.137 +lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> uncurry c p"
   7.138    apply (simp only: split_tupled_all)
   7.139    apply (simp (no_asm_simp))
   7.140    done
   7.141  
   7.142 -lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> case_prod c p x"
   7.143 +lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> uncurry c p x"
   7.144    apply (simp only: split_tupled_all)
   7.145    apply (simp (no_asm_simp))
   7.146    done
   7.147  
   7.148 -lemma splitE: "case_prod c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   7.149 +lemma splitE: "uncurry c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   7.150    by (induct p) auto
   7.151  
   7.152 -lemma splitE': "case_prod c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   7.153 +lemma splitE': "uncurry c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   7.154    by (induct p) auto
   7.155  
   7.156  lemma splitE2:
   7.157 -  "[| Q (case_prod P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
   7.158 +  "[| Q (uncurry P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
   7.159  proof -
   7.160 -  assume q: "Q (case_prod P z)"
   7.161 +  assume q: "Q (uncurry P z)"
   7.162    assume r: "!!x y. [|z = (x, y); Q (P x y)|] ==> R"
   7.163    show R
   7.164      apply (rule r surjective_pairing)+
   7.165 @@ -595,17 +595,17 @@
   7.166      done
   7.167  qed
   7.168  
   7.169 -lemma splitD': "case_prod R (a,b) c ==> R a b c"
   7.170 +lemma splitD': "uncurry R (a,b) c ==> R a b c"
   7.171    by simp
   7.172  
   7.173 -lemma mem_splitI: "z: c a b ==> z: case_prod c (a, b)"
   7.174 +lemma mem_splitI: "z: c a b ==> z: uncurry c (a, b)"
   7.175    by simp
   7.176  
   7.177 -lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: case_prod c p"
   7.178 +lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: uncurry c p"
   7.179  by (simp only: split_tupled_all, simp)
   7.180  
   7.181  lemma mem_splitE:
   7.182 -  assumes "z \<in> case_prod c p"
   7.183 +  assumes "z \<in> uncurry c p"
   7.184    obtains x y where "p = (x, y)" and "z \<in> c x y"
   7.185    using assms by (rule splitE2)
   7.186  
   7.187 @@ -614,7 +614,7 @@
   7.188  
   7.189  ML \<open>
   7.190  local (* filtering with exists_p_split is an essential optimization *)
   7.191 -  fun exists_p_split (Const (@{const_name case_prod},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
   7.192 +  fun exists_p_split (Const (@{const_name uncurry},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
   7.193      | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
   7.194      | exists_p_split (Abs (_, _, t)) = exists_p_split t
   7.195      | exists_p_split _ = false;
   7.196 @@ -633,10 +633,10 @@
   7.197  lemma split_eta_SetCompr [simp, no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   7.198    by (rule ext) fast
   7.199  
   7.200 -lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = case_prod P"
   7.201 +lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = uncurry P"
   7.202    by (rule ext) fast
   7.203  
   7.204 -lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & case_prod Q ab)"
   7.205 +lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & uncurry Q ab)"
   7.206    -- \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
   7.207    by (rule ext) blast
   7.208  
   7.209 @@ -646,7 +646,7 @@
   7.210  *)
   7.211  lemma split_comp_eq: 
   7.212    fixes f :: "'a => 'b => 'c" and g :: "'d => 'a"
   7.213 -  shows "(%u. f (g (fst u)) (snd u)) = (case_prod (%x. f (g x)))"
   7.214 +  shows "(%u. f (g (fst u)) (snd u)) = (uncurry (%x. f (g x)))"
   7.215    by (rule ext) auto
   7.216  
   7.217  lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
   7.218 @@ -676,22 +676,22 @@
   7.219  
   7.220  lemmas case_prodI = prod.case [THEN iffD2]
   7.221  
   7.222 -lemma case_prodI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case_prod c p"
   7.223 +lemma case_prodI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> uncurry c p"
   7.224    by (fact splitI2)
   7.225  
   7.226 -lemma case_prodI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> case_prod c p x"
   7.227 +lemma case_prodI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> uncurry c p x"
   7.228    by (fact splitI2')
   7.229  
   7.230 -lemma case_prodE: "case_prod c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   7.231 +lemma case_prodE: "uncurry c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   7.232    by (fact splitE)
   7.233  
   7.234 -lemma case_prodE': "case_prod c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   7.235 +lemma case_prodE': "uncurry c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   7.236    by (fact splitE')
   7.237  
   7.238  declare case_prodI [intro!]
   7.239  
   7.240  lemma case_prod_beta:
   7.241 -  "case_prod f p = f (fst p) (snd p)"
   7.242 +  "uncurry f p = f (fst p) (snd p)"
   7.243    by (fact split_beta)
   7.244  
   7.245  lemma prod_cases3 [cases type]:
   7.246 @@ -735,7 +735,7 @@
   7.247    by (cases x) blast
   7.248  
   7.249  definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
   7.250 -  "internal_split == case_prod"
   7.251 +  "internal_split == uncurry"
   7.252  
   7.253  lemma internal_split_conv: "internal_split c (a, b) = c a b"
   7.254    by (simp only: internal_split_def split_conv)
   7.255 @@ -762,10 +762,10 @@
   7.256  lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q"
   7.257    by (simp add: curry_def)
   7.258  
   7.259 -lemma curry_split [simp]: "curry (case_prod f) = f"
   7.260 +lemma curry_split [simp]: "curry (uncurry f) = f"
   7.261    by (simp add: curry_def case_prod_unfold)
   7.262  
   7.263 -lemma split_curry [simp]: "case_prod (curry f) = f"
   7.264 +lemma split_curry [simp]: "uncurry (curry f) = f"
   7.265    by (simp add: curry_def case_prod_unfold)
   7.266  
   7.267  lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)"
   7.268 @@ -778,12 +778,12 @@
   7.269  notation fcomp (infixl "\<circ>>" 60)
   7.270  
   7.271  definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60) where
   7.272 -  "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod g (f x))"
   7.273 +  "f \<circ>\<rightarrow> g = (\<lambda>x. uncurry g (f x))"
   7.274  
   7.275  lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
   7.276    by (simp add: fun_eq_iff scomp_def case_prod_unfold)
   7.277  
   7.278 -lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = case_prod g (f x)"
   7.279 +lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = uncurry g (f x)"
   7.280    by (simp add: scomp_unfold case_prod_unfold)
   7.281  
   7.282  lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
   7.283 @@ -1077,7 +1077,7 @@
   7.284    by (blast elim: equalityE)
   7.285  
   7.286  lemma SetCompr_Sigma_eq:
   7.287 -  "Collect (case_prod (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
   7.288 +  "Collect (uncurry (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
   7.289    by blast
   7.290  
   7.291  lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q"
   7.292 @@ -1314,8 +1314,11 @@
   7.293  
   7.294  subsection \<open>Legacy theorem bindings and duplicates\<close>
   7.295  
   7.296 +abbreviation (input) case_prod :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
   7.297 +  "case_prod \<equiv> uncurry"
   7.298 +
   7.299  abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
   7.300 -  "split \<equiv> case_prod"
   7.301 +  "split \<equiv> uncurry"
   7.302  
   7.303  lemmas PairE = prod.exhaust
   7.304  lemmas Pair_eq = prod.inject
     8.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Sun Sep 06 22:14:51 2015 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Sun Sep 06 22:14:51 2015 +0200
     8.3 @@ -66,7 +66,7 @@
     8.4    | unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u)
     8.5    | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
     8.6    | unfold_lets_splits t = t
     8.7 -and unfold_splits_lets ((t as Const (@{const_name case_prod}, _)) $ u) =
     8.8 +and unfold_splits_lets ((t as Const (@{const_name uncurry}, _)) $ u) =
     8.9      (case unfold_splits_lets u of
    8.10        u' as Abs (s1, T1, Abs (s2, T2, _)) =>
    8.11        let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in
     9.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sun Sep 06 22:14:51 2015 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sun Sep 06 22:14:51 2015 +0200
     9.3 @@ -294,7 +294,7 @@
     9.4            | (_, branches') =>
     9.5              Term.list_comb (If_const (typof (hd branches')) $ tap (check_no_call bound_Ts) obj,
     9.6                branches'))
     9.7 -        | (c as Const (@{const_name case_prod}, _), arg :: args) =>
     9.8 +        | (c as Const (@{const_name uncurry}, _), arg :: args) =>
     9.9            massage_rec bound_Ts
    9.10              (unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
    9.11          | (Const (c, _), args as _ :: _ :: _) =>
    9.12 @@ -398,12 +398,12 @@
    9.13                end
    9.14              | NONE =>
    9.15                (case t of
    9.16 -                Const (@{const_name case_prod}, _) $ t' =>
    9.17 +                Const (@{const_name uncurry}, _) $ t' =>
    9.18                  let
    9.19                    val U' = curried_type U;
    9.20                    val T' = curried_type T;
    9.21                  in
    9.22 -                  Const (@{const_name case_prod}, U' --> U) $ massage_any_call bound_Ts U' T' t'
    9.23 +                  Const (@{const_name uncurry}, U' --> U) $ massage_any_call bound_Ts U' T' t'
    9.24                  end
    9.25                | t1 $ t2 =>
    9.26                  (if has_call t2 then
    9.27 @@ -927,7 +927,7 @@
    9.28                let val (u, vs) = strip_comb t in
    9.29                  if is_Free u andalso has_call u then
    9.30                    Inr_const T U2 $ mk_tuple1_balanced bound_Ts vs
    9.31 -                else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
    9.32 +                else if try (fst o dest_Const) u = SOME @{const_name uncurry} then
    9.33                    map (rewrite bound_Ts) vs |> chop 1
    9.34                    |>> HOLogic.mk_split o the_single
    9.35                    |> Term.list_comb
    10.1 --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Sun Sep 06 22:14:51 2015 +0200
    10.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Sun Sep 06 22:14:51 2015 +0200
    10.3 @@ -164,7 +164,7 @@
    10.4          set_cases = @{thms fsts.cases[unfolded eq_fst_iff ex_neg_all_pos]
    10.5            snds.cases[unfolded eq_snd_iff ex_neg_all_pos]}},
    10.6       fp_co_induct_sugar =
    10.7 -       {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
    10.8 +       {co_rec = Const (@{const_name uncurry}, (ctr_Ts ---> C) --> fpT --> C),
    10.9          common_co_inducts = @{thms prod.induct},
   10.10          co_inducts = @{thms prod.induct},
   10.11          co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Sep 06 22:14:51 2015 +0200
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Sep 06 22:14:51 2015 +0200
    11.3 @@ -2287,7 +2287,7 @@
    11.4        HOLogic.Collect_const tuple_T $ list_comb (Const base_x, outer_bounds)
    11.5      val step_set =
    11.6        HOLogic.Collect_const prod_T
    11.7 -      $ (Const (@{const_name case_prod}, curried_T --> uncurried_T)
    11.8 +      $ (Const (@{const_name uncurry}, curried_T --> uncurried_T)
    11.9                  $ list_comb (Const step_x, outer_bounds))
   11.10      val image_set =
   11.11        image_const $ (rtrancl_const $ step_set) $ base_set
    12.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Sep 06 22:14:51 2015 +0200
    12.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Sep 06 22:14:51 2015 +0200
    12.3 @@ -1023,7 +1023,7 @@
    12.4  
    12.5  (* Definition of executable functions and their intro and elim rules *)
    12.6  
    12.7 -fun strip_split_abs (Const (@{const_name case_prod}, _) $ t) = strip_split_abs t
    12.8 +fun strip_split_abs (Const (@{const_name uncurry}, _) $ t) = strip_split_abs t
    12.9    | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
   12.10    | strip_split_abs t = t
   12.11  
    13.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Sep 06 22:14:51 2015 +0200
    13.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Sep 06 22:14:51 2015 +0200
    13.3 @@ -316,7 +316,7 @@
    13.4      fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
    13.5        liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    13.6      fun mk_split T = Sign.mk_const thy
    13.7 -      (@{const_name case_prod}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
    13.8 +      (@{const_name uncurry}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
    13.9      fun mk_scomp_split T t t' =
   13.10        mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
   13.11          (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
   13.12 @@ -362,7 +362,7 @@
   13.13      fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
   13.14        liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   13.15      fun mk_split T = Sign.mk_const thy
   13.16 -      (@{const_name case_prod}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
   13.17 +      (@{const_name uncurry}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
   13.18      fun mk_scomp_split T t t' =
   13.19        mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
   13.20          (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
    14.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Sun Sep 06 22:14:51 2015 +0200
    14.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sun Sep 06 22:14:51 2015 +0200
    14.3 @@ -634,12 +634,12 @@
    14.4            end
    14.5        end
    14.6  
    14.7 -  | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
    14.8 -     ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
    14.9 +  | (((t1 as Const (@{const_name uncurry}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
   14.10 +     ((t2 as Const (@{const_name uncurry}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
   14.11         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
   14.12  
   14.13 -  | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, s1)),
   14.14 -     ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , s2))) =>
   14.15 +  | (((t1 as Const (@{const_name uncurry}, _)) $ Abs (v1, ty, s1)),
   14.16 +     ((t2 as Const (@{const_name uncurry}, _)) $ Abs (v2, _ , s2))) =>
   14.17         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
   14.18  
   14.19    | (t1 $ t2, t1' $ t2') =>
    15.1 --- a/src/HOL/Tools/hologic.ML	Sun Sep 06 22:14:51 2015 +0200
    15.2 +++ b/src/HOL/Tools/hologic.ML	Sun Sep 06 22:14:51 2015 +0200
    15.3 @@ -349,12 +349,12 @@
    15.4    end;
    15.5  
    15.6  fun split_const (A, B, C) =
    15.7 -  Const ("Product_Type.prod.case_prod", (A --> B --> C) --> mk_prodT (A, B) --> C);
    15.8 +  Const ("Product_Type.prod.uncurry", (A --> B --> C) --> mk_prodT (A, B) --> C);
    15.9  
   15.10  fun mk_split t =
   15.11    (case Term.fastype_of t of
   15.12      T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
   15.13 -      Const ("Product_Type.prod.case_prod", T --> mk_prodT (A, B) --> C) $ t
   15.14 +      Const ("Product_Type.prod.uncurry", T --> mk_prodT (A, B) --> C) $ t
   15.15    | _ => raise TERM ("mk_split: bad body type", [t]));
   15.16  
   15.17  (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
   15.18 @@ -470,7 +470,7 @@
   15.19  val strip_psplits =
   15.20    let
   15.21      fun strip [] qs Ts t = (t, rev Ts, qs)
   15.22 -      | strip (p :: ps) qs Ts (Const ("Product_Type.prod.case_prod", _) $ t) =
   15.23 +      | strip (p :: ps) qs Ts (Const ("Product_Type.prod.uncurry", _) $ t) =
   15.24            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
   15.25        | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
   15.26        | strip (p :: ps) qs Ts t = strip ps qs
    16.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Sep 06 22:14:51 2015 +0200
    16.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Sep 06 22:14:51 2015 +0200
    16.3 @@ -92,7 +92,7 @@
    16.4  val strip_psplits =
    16.5    let
    16.6      fun strip [] qs vs t = (t, rev vs, qs)
    16.7 -      | strip (p :: ps) qs vs (Const (@{const_name Product_Type.prod.case_prod}, _) $ t) =
    16.8 +      | strip (p :: ps) qs vs (Const (@{const_name uncurry}, _) $ t) =
    16.9            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t
   16.10        | strip (_ :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t
   16.11        | strip (_ :: ps) qs vs t = strip ps qs
   16.12 @@ -305,7 +305,7 @@
   16.13  
   16.14  (* proof tactic *)
   16.15  
   16.16 -val case_prod_distrib = @{lemma "(case_prod g x) z = case_prod (% x y. (g x y) z) x" by (simp add: case_prod_beta)}
   16.17 +val case_prod_distrib = @{lemma "(uncurry g x) z = uncurry (\<lambda>x y. (g x y) z) x" by (simp add: case_prod_beta)}
   16.18  
   16.19  val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp}
   16.20  val vimageE' =