src/HOL/Product_Type.thy
changeset 61424 c3658c18b7bc
parent 61422 0dfcd0fb4172
child 61425 fb95d06fb21f
     1.1 --- a/src/HOL/Product_Type.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -238,7 +238,7 @@
     1.4  lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
     1.5    by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
     1.6  
     1.7 -free_constructors uncurry for Pair fst snd
     1.8 +free_constructors case_prod for Pair fst snd
     1.9  proof -
    1.10    fix P :: bool and p :: "'a \<times> 'b"
    1.11    show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
    1.12 @@ -266,8 +266,7 @@
    1.13  
    1.14  setup \<open>Sign.mandatory_path "prod"\<close>
    1.15  
    1.16 -declare
    1.17 -  old.prod.inject[iff del]
    1.18 +declare old.prod.inject [iff del]
    1.19  
    1.20  lemmas induct = old.prod.induct
    1.21  lemmas inducts = old.prod.inducts
    1.22 @@ -278,6 +277,16 @@
    1.23  
    1.24  declare prod.case [nitpick_simp del]
    1.25  declare prod.case_cong_weak [cong del]
    1.26 +declare prod.case_eq_if [mono]
    1.27 +declare prod.split [no_atp]
    1.28 +declare prod.split_asm [no_atp]
    1.29 +
    1.30 +text \<open>
    1.31 +  @{thm [source] prod.split} could be declared as @{text "[split]"}
    1.32 +  done after the Splitter has been speeded up significantly;
    1.33 +  precompute the constants involved and don't do anything unless the
    1.34 +  current goal contains one of those constants.
    1.35 +\<close>
    1.36  
    1.37  
    1.38  subsubsection \<open>Tuple syntax\<close>
    1.39 @@ -302,22 +311,22 @@
    1.40    "_pattern x y" \<rightleftharpoons> "CONST Pair x y"
    1.41    "_patterns x y" \<rightleftharpoons> "CONST Pair x y"
    1.42    "_tuple x (_tuple_args y z)" \<rightleftharpoons> "_tuple x (_tuple_arg (_tuple y z))"
    1.43 -  "\<lambda>(x, y, zs). b" \<rightleftharpoons> "CONST uncurry (\<lambda>x (y, zs). b)"
    1.44 -  "\<lambda>(x, y). b" \<rightleftharpoons> "CONST uncurry (\<lambda>x y. b)"
    1.45 +  "\<lambda>(x, y, zs). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x (y, zs). b)"
    1.46 +  "\<lambda>(x, y). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x y. b)"
    1.47    "_abs (CONST Pair x y) t" \<rightharpoonup> "\<lambda>(x, y). t"
    1.48    -- \<open>This rule accommodates tuples in @{text "case C \<dots> (x, y) \<dots> \<Rightarrow> \<dots>"}:
    1.49       The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic},
    1.50       not @{text pttrn}.\<close>
    1.51  
    1.52 -text \<open>print @{term "uncurry f"} as @{term "\<lambda>(x, y). f x y"} and
    1.53 -  @{term "uncurry (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close>
    1.54 +text \<open>print @{term "case_prod f"} as @{term "\<lambda>(x, y). f x y"} and
    1.55 +  @{term "case_prod (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close>
    1.56  
    1.57  typed_print_translation \<open>
    1.58    let
    1.59 -    fun uncurry_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
    1.60 -      | uncurry_guess_names_tr' T [Abs (x, xT, t)] =
    1.61 +    fun case_prod_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
    1.62 +      | case_prod_guess_names_tr' T [Abs (x, xT, t)] =
    1.63            (case (head_of t) of
    1.64 -            Const (@{const_syntax uncurry}, _) => raise Match
    1.65 +            Const (@{const_syntax case_prod}, _) => raise Match
    1.66            | _ =>
    1.67              let 
    1.68                val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
    1.69 @@ -327,9 +336,9 @@
    1.70                Syntax.const @{syntax_const "_abs"} $
    1.71                  (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
    1.72              end)
    1.73 -      | uncurry_guess_names_tr' T [t] =
    1.74 +      | case_prod_guess_names_tr' T [t] =
    1.75            (case head_of t of
    1.76 -            Const (@{const_syntax uncurry}, _) => raise Match
    1.77 +            Const (@{const_syntax case_prod}, _) => raise Match
    1.78            | _ =>
    1.79              let
    1.80                val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
    1.81 @@ -340,8 +349,8 @@
    1.82                Syntax.const @{syntax_const "_abs"} $
    1.83                  (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
    1.84              end)
    1.85 -      | uncurry_guess_names_tr' _ _ = raise Match;
    1.86 -  in [(@{const_syntax uncurry}, K uncurry_guess_names_tr')] end
    1.87 +      | case_prod_guess_names_tr' _ _ = raise Match;
    1.88 +  in [(@{const_syntax case_prod}, K case_prod_guess_names_tr')] end
    1.89  \<close>
    1.90  
    1.91  
    1.92 @@ -362,32 +371,33 @@
    1.93      (Haskell) -
    1.94  | constant "HOL.equal :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" \<rightharpoonup>
    1.95      (Haskell) infix 4 "=="
    1.96 +| constant fst \<rightharpoonup> (Haskell) "fst"
    1.97 +| constant snd \<rightharpoonup> (Haskell) "snd"
    1.98  
    1.99  
   1.100  subsubsection \<open>Fundamental operations and properties\<close>
   1.101  
   1.102  lemma Pair_inject:
   1.103    assumes "(a, b) = (a', b')"
   1.104 -    and "a = a' ==> b = b' ==> R"
   1.105 +    and "a = a' \<Longrightarrow> b = b' \<Longrightarrow> R"
   1.106    shows R
   1.107    using assms by simp
   1.108  
   1.109  lemma surj_pair [simp]: "EX x y. p = (x, y)"
   1.110    by (cases p) simp
   1.111  
   1.112 -code_printing
   1.113 -  constant fst \<rightharpoonup> (Haskell) "fst"
   1.114 -| constant snd \<rightharpoonup> (Haskell) "snd"
   1.115 -
   1.116 -lemma case_prod_unfold [nitpick_unfold]: "uncurry = (%c p. c (fst p) (snd p))"
   1.117 -  by (simp add: fun_eq_iff split: prod.split)
   1.118 -
   1.119  lemma fst_eqD: "fst (x, y) = a ==> x = a"
   1.120    by simp
   1.121  
   1.122  lemma snd_eqD: "snd (x, y) = a ==> y = a"
   1.123    by simp
   1.124  
   1.125 +lemma case_prod_unfold [nitpick_unfold]: "case_prod = (\<lambda>c p. c (fst p) (snd p))"
   1.126 +  by (simp add: fun_eq_iff split: prod.split)
   1.127 +
   1.128 +lemma case_prod_conv [simp, code]: "(case (a, b) of (c, d) \<Rightarrow> f c d) = f a b"
   1.129 +  by (fact prod.case)
   1.130 +
   1.131  lemmas surjective_pairing = prod.collapse [symmetric]
   1.132  
   1.133  lemma prod_eq_iff: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
   1.134 @@ -396,36 +406,27 @@
   1.135  lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
   1.136    by (simp add: prod_eq_iff)
   1.137  
   1.138 -lemma split_conv [simp, code]: "(case (a, b) of (c, d) \<Rightarrow> f c d) = f a b"
   1.139 -  by (fact prod.case)
   1.140 +lemma case_prodI: "f a b \<Longrightarrow> case (a, b) of (c, d) \<Rightarrow> f c d"
   1.141 +  by (rule prod.case [THEN iffD2])
   1.142  
   1.143 -lemma splitI: "f a b \<Longrightarrow> case (a, b) of (c, d) \<Rightarrow> f c d"
   1.144 -  by (rule split_conv [THEN iffD2])
   1.145 +lemma case_prodD: "(case (a, b) of (c, d) \<Rightarrow> f c d) \<Longrightarrow> f a b"
   1.146 +  by (rule prod.case [THEN iffD1])
   1.147  
   1.148 -lemma splitD: "(case (a, b) of (c, d) \<Rightarrow> f c d) \<Longrightarrow> f a b"
   1.149 -  by (rule split_conv [THEN iffD1])
   1.150 -
   1.151 -lemma split_Pair [simp]: "uncurry Pair = id"
   1.152 +lemma case_prod_Pair [simp]: "case_prod Pair = id"
   1.153    by (simp add: fun_eq_iff split: prod.split)
   1.154  
   1.155 -lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
   1.156 +lemma case_prod_eta: "(\<lambda>(x, y). f (x, y)) = f"
   1.157    -- \<open>Subsumes the old @{text split_Pair} when @{term f} is the identity function.\<close>
   1.158    by (simp add: fun_eq_iff split: prod.split)
   1.159  
   1.160 -lemma split_comp: "(case x of (a, b) \<Rightarrow> (f \<circ> g) a b) = f (g (fst x)) (snd x)"
   1.161 +lemma case_prod_comp: "(case x of (a, b) \<Rightarrow> (f \<circ> g) a b) = f (g (fst x)) (snd x)"
   1.162    by (cases x) simp
   1.163  
   1.164 -lemma split_twice: "uncurry f (uncurry g p) = uncurry (\<lambda>x y. uncurry f (g x y)) p"
   1.165 -  by (fact prod.case_distrib)
   1.166 -
   1.167 -lemma The_split: "The (uncurry P) = (THE xy. P (fst xy) (snd xy))"
   1.168 +lemma The_case_prod: "The (case_prod P) = (THE xy. P (fst xy) (snd xy))"
   1.169    by (simp add: case_prod_unfold)
   1.170  
   1.171 -lemmas split_weak_cong = prod.case_cong_weak
   1.172 -  -- \<open>Prevents simplification of @{term c}: much faster\<close>
   1.173 -
   1.174 -lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
   1.175 -  by (simp add: split_eta)
   1.176 +lemma cond_case_prod_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
   1.177 +  by (simp add: case_prod_eta)
   1.178  
   1.179  lemma split_paired_all [no_atp]: "(!!x. PROP P x) == (!!a b. PROP P (a, b))"
   1.180  proof
   1.181 @@ -438,9 +439,6 @@
   1.182    from \<open>PROP P (fst x, snd x)\<close> show "PROP P x" by simp
   1.183  qed
   1.184  
   1.185 -lemma uncurry_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
   1.186 -  by (cases x) simp
   1.187 -
   1.188  text \<open>
   1.189    The rule @{thm [source] split_paired_all} does not work with the
   1.190    Simplifier because it also affects premises in congrence rules,
   1.191 @@ -487,20 +485,20 @@
   1.192  
   1.193  lemma split_paired_The [no_atp]: "(THE x. P x) = (THE (a, b). P (a, b))"
   1.194    -- \<open>Can't be added to simpset: loops!\<close>
   1.195 -  by (simp add: split_eta)
   1.196 +  by (simp add: case_prod_eta)
   1.197  
   1.198  text \<open>
   1.199 -  Simplification procedure for @{thm [source] cond_split_eta}.  Using
   1.200 -  @{thm [source] split_eta} as a rewrite rule is not general enough,
   1.201 -  and using @{thm [source] cond_split_eta} directly would render some
   1.202 +  Simplification procedure for @{thm [source] cond_case_prod_eta}.  Using
   1.203 +  @{thm [source] case_prod_eta} as a rewrite rule is not general enough,
   1.204 +  and using @{thm [source] cond_case_prod_eta} directly would render some
   1.205    existing proofs very inefficient; similarly for @{text
   1.206 -  split_beta}.
   1.207 +  prod.case_eq_if}.
   1.208  \<close>
   1.209  
   1.210  ML \<open>
   1.211  local
   1.212 -  val cond_split_eta_ss =
   1.213 -    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms cond_split_eta});
   1.214 +  val cond_case_prod_eta_ss =
   1.215 +    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms cond_case_prod_eta});
   1.216    fun Pair_pat k 0 (Bound m) = (m = k)
   1.217      | Pair_pat k i (Const (@{const_name Pair},  _) $ Bound m $ t) =
   1.218          i > 0 andalso m = k + i andalso Pair_pat k (i - 1) t
   1.219 @@ -510,11 +508,11 @@
   1.220      | no_args k i (Bound m) = m < k orelse m > k + i
   1.221      | no_args _ _ _ = true;
   1.222    fun split_pat tp i (Abs  (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
   1.223 -    | split_pat tp i (Const (@{const_name uncurry}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
   1.224 +    | split_pat tp i (Const (@{const_name case_prod}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
   1.225      | split_pat tp i _ = NONE;
   1.226    fun metaeq ctxt lhs rhs = mk_meta_eq (Goal.prove ctxt [] []
   1.227          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
   1.228 -        (K (simp_tac (put_simpset cond_split_eta_ss ctxt) 1)));
   1.229 +        (K (simp_tac (put_simpset cond_case_prod_eta_ss ctxt) 1)));
   1.230  
   1.231    fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k + 1) i t
   1.232      | beta_term_pat k i (t $ u) =
   1.233 @@ -528,103 +526,90 @@
   1.234          else (subst arg k i t $ subst arg k i u)
   1.235      | subst arg k i t = t;
   1.236  in
   1.237 -  fun beta_proc ctxt (s as Const (@{const_name uncurry}, _) $ Abs (_, _, t) $ arg) =
   1.238 +  fun beta_proc ctxt (s as Const (@{const_name case_prod}, _) $ Abs (_, _, t) $ arg) =
   1.239          (case split_pat beta_term_pat 1 t of
   1.240            SOME (i, f) => SOME (metaeq ctxt s (subst arg 0 i f))
   1.241          | NONE => NONE)
   1.242      | beta_proc _ _ = NONE;
   1.243 -  fun eta_proc ctxt (s as Const (@{const_name uncurry}, _) $ Abs (_, _, t)) =
   1.244 +  fun eta_proc ctxt (s as Const (@{const_name case_prod}, _) $ Abs (_, _, t)) =
   1.245          (case split_pat eta_term_pat 1 t of
   1.246            SOME (_, ft) => SOME (metaeq ctxt s (let val f $ _ = ft in f end))
   1.247          | NONE => NONE)
   1.248      | eta_proc _ _ = NONE;
   1.249  end;
   1.250  \<close>
   1.251 -simproc_setup split_beta ("split f z") =
   1.252 +simproc_setup case_prod_beta ("case_prod f z") =
   1.253    \<open>fn _ => fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct)\<close>
   1.254 -simproc_setup split_eta ("split f") =
   1.255 +simproc_setup case_prod_eta ("case_prod f") =
   1.256    \<open>fn _ => fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct)\<close>
   1.257  
   1.258 -lemmas split_beta [mono] = prod.case_eq_if
   1.259 -
   1.260 -lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
   1.261 +lemma case_prod_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
   1.262    by (auto simp: fun_eq_iff)
   1.263  
   1.264 -lemmas split_split [no_atp] = prod.split
   1.265 -  -- \<open>For use with @{text split} and the Simplifier.\<close>
   1.266 -
   1.267  text \<open>
   1.268 -  @{thm [source] split_split} could be declared as @{text "[split]"}
   1.269 -  done after the Splitter has been speeded up significantly;
   1.270 -  precompute the constants involved and don't do anything unless the
   1.271 -  current goal contains one of those constants.
   1.272 -\<close>
   1.273 -
   1.274 -lemmas split_split_asm [no_atp] = prod.split_asm
   1.275 -
   1.276 -text \<open>
   1.277 -  \medskip @{const uncurry} used as a logical connective or set former.
   1.278 +  \medskip @{const case_prod} used as a logical connective or set former.
   1.279  
   1.280    \medskip These rules are for use with @{text blast}; could instead
   1.281    call @{text simp} using @{thm [source] prod.split} as rewrite.\<close>
   1.282  
   1.283 -lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case p of (a, b) \<Rightarrow> c a b"
   1.284 -  apply (simp only: split_tupled_all)
   1.285 -  apply (simp (no_asm_simp))
   1.286 -  done
   1.287 +lemma case_prodI2:
   1.288 +  "\<And>p. (\<And>a b. p = (a, b) \<Longrightarrow> c a b) \<Longrightarrow> case p of (a, b) \<Rightarrow> c a b"
   1.289 +  by (simp add: split_tupled_all)
   1.290  
   1.291 -lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> (case p of (a, b) \<Rightarrow> c a b) x"
   1.292 -  apply (simp only: split_tupled_all)
   1.293 -  apply (simp (no_asm_simp))
   1.294 -  done
   1.295 +lemma case_prodI2':
   1.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"
   1.297 +  by (simp add: split_tupled_all)
   1.298  
   1.299 -lemma splitE: "(case p of (a, b) \<Rightarrow> c a b) ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   1.300 -  by (induct p) auto
   1.301 +lemma case_prodE [elim!]:
   1.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"
   1.303 +  by (induct p) simp
   1.304  
   1.305 -lemma splitE': "(case p of (a, b) \<Rightarrow> c a b) z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   1.306 -  by (induct p) auto
   1.307 +lemma case_prodE' [elim!]:
   1.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"
   1.309 +  by (induct p) simp
   1.310  
   1.311 -lemma splitE2:
   1.312 -  "[| Q (case z of (a, b) \<Rightarrow> P a b);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
   1.313 -proof -
   1.314 -  assume q: "Q (uncurry P z)"
   1.315 -  assume r: "!!x y. [|z = (x, y); Q (P x y)|] ==> R"
   1.316 -  show R
   1.317 -    apply (rule r surjective_pairing)+
   1.318 -    apply (rule split_beta [THEN subst], rule q)
   1.319 -    done
   1.320 +lemma case_prodE2:
   1.321 +  assumes q: "Q (case z of (a, b) \<Rightarrow> P a b)"
   1.322 +    and r: "\<And>x y. z = (x, y) \<Longrightarrow> Q (P x y) \<Longrightarrow> R"
   1.323 +  shows R
   1.324 +proof (rule r)
   1.325 +  show "z = (fst z, snd z)" by simp
   1.326 +  then show "Q (P (fst z) (snd z))"
   1.327 +    using q by (simp add: case_prod_unfold)
   1.328  qed
   1.329  
   1.330 -lemma splitD':
   1.331 +lemma case_prodD':
   1.332    "(case (a, b) of (c, d) \<Rightarrow> R c d) c \<Longrightarrow> R a b c"
   1.333    by simp
   1.334  
   1.335 -lemma mem_splitI:
   1.336 +lemma mem_case_prodI:
   1.337    "z \<in> c a b \<Longrightarrow> z \<in> (case (a, b) of (d, e) \<Rightarrow> c d e)"
   1.338    by simp
   1.339  
   1.340 -lemma mem_splitI2:
   1.341 +lemma mem_case_prodI2 [intro!]:
   1.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)"
   1.343    by (simp only: split_tupled_all) simp
   1.344  
   1.345 -lemma mem_splitE:
   1.346 -  assumes "z \<in> uncurry c p"
   1.347 +declare mem_case_prodI [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
   1.348 +declare case_prodI2' [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
   1.349 +declare case_prodI2 [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
   1.350 +declare case_prodI [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
   1.351 +  
   1.352 +lemma mem_case_prodE [elim!]:
   1.353 +  assumes "z \<in> case_prod c p"
   1.354    obtains x y where "p = (x, y)" and "z \<in> c x y"
   1.355 -  using assms by (rule splitE2)
   1.356 -
   1.357 -declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
   1.358 -declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
   1.359 +  using assms by (rule case_prodE2)
   1.360  
   1.361  ML \<open>
   1.362  local (* filtering with exists_p_split is an essential optimization *)
   1.363 -  fun exists_p_split (Const (@{const_name uncurry},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
   1.364 +  fun exists_p_split (Const (@{const_name case_prod},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
   1.365      | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
   1.366      | exists_p_split (Abs (_, _, t)) = exists_p_split t
   1.367      | exists_p_split _ = false;
   1.368  in
   1.369  fun split_conv_tac ctxt = SUBGOAL (fn (t, i) =>
   1.370    if exists_p_split t
   1.371 -  then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_conv}) i
   1.372 +  then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms case_prod_conv}) i
   1.373    else no_tac);
   1.374  end;
   1.375  \<close>
   1.376 @@ -636,10 +621,10 @@
   1.377  lemma split_eta_SetCompr [simp, no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   1.378    by (rule ext) fast
   1.379  
   1.380 -lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = uncurry P"
   1.381 +lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = case_prod P"
   1.382    by (rule ext) fast
   1.383  
   1.384 -lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & uncurry Q ab)"
   1.385 +lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & case_prod Q ab)"
   1.386    -- \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
   1.387    by (rule ext) blast
   1.388  
   1.389 @@ -649,7 +634,7 @@
   1.390  *)
   1.391  lemma split_comp_eq: 
   1.392    fixes f :: "'a => 'b => 'c" and g :: "'d => 'a"
   1.393 -  shows "(%u. f (g (fst u)) (snd u)) = (uncurry (%x. f (g x)))"
   1.394 +  shows "(%u. f (g (fst u)) (snd u)) = (case_prod (%x. f (g x)))"
   1.395    by (rule ext) auto
   1.396  
   1.397  lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
   1.398 @@ -673,29 +658,9 @@
   1.399  qed "The_split_eq";
   1.400  *)
   1.401  
   1.402 -text \<open>
   1.403 -  Setup of internal @{text split_rule}.
   1.404 -\<close>
   1.405 -
   1.406 -lemmas case_prodI = prod.case [THEN iffD2]
   1.407 -
   1.408 -lemma case_prodI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> uncurry c p"
   1.409 -  by (fact splitI2)
   1.410 -
   1.411 -lemma case_prodI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> uncurry c p x"
   1.412 -  by (fact splitI2')
   1.413 -
   1.414 -lemma case_prodE: "uncurry c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   1.415 -  by (fact splitE)
   1.416 -
   1.417 -lemma case_prodE': "uncurry c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   1.418 -  by (fact splitE')
   1.419 -
   1.420 -declare case_prodI [intro!]
   1.421 -
   1.422  lemma case_prod_beta:
   1.423 -  "uncurry f p = f (fst p) (snd p)"
   1.424 -  by (fact split_beta)
   1.425 +  "case_prod f p = f (fst p) (snd p)"
   1.426 +  by (fact prod.case_eq_if)
   1.427  
   1.428  lemma prod_cases3 [cases type]:
   1.429    obtains (fields) a b c where "y = (a, b, c)"
   1.430 @@ -737,20 +702,20 @@
   1.431      "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   1.432    by (cases x) blast
   1.433  
   1.434 -definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
   1.435 -  "internal_split == uncurry"
   1.436 +definition internal_case_prod :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
   1.437 +  "internal_case_prod == case_prod"
   1.438  
   1.439 -lemma internal_split_conv: "internal_split c (a, b) = c a b"
   1.440 -  by (simp only: internal_split_def split_conv)
   1.441 +lemma internal_case_prod_conv: "internal_case_prod c (a, b) = c a b"
   1.442 +  by (simp only: internal_case_prod_def case_prod_conv)
   1.443  
   1.444  ML_file "Tools/split_rule.ML"
   1.445  
   1.446 -hide_const internal_split
   1.447 +hide_const internal_case_prod
   1.448  
   1.449  
   1.450  subsubsection \<open>Derived operations\<close>
   1.451  
   1.452 -definition curry    :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
   1.453 +definition curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
   1.454    "curry = (\<lambda>c x y. c (x, y))"
   1.455  
   1.456  lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
   1.457 @@ -765,10 +730,10 @@
   1.458  lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q"
   1.459    by (simp add: curry_def)
   1.460  
   1.461 -lemma curry_split [simp]: "curry (uncurry f) = f"
   1.462 +lemma curry_case_prod [simp]: "curry (case_prod f) = f"
   1.463    by (simp add: curry_def case_prod_unfold)
   1.464  
   1.465 -lemma split_curry [simp]: "uncurry (curry f) = f"
   1.466 +lemma case_prod_curry [simp]: "case_prod (curry f) = f"
   1.467    by (simp add: curry_def case_prod_unfold)
   1.468  
   1.469  lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)"
   1.470 @@ -781,12 +746,12 @@
   1.471  notation fcomp (infixl "\<circ>>" 60)
   1.472  
   1.473  definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60) where
   1.474 -  "f \<circ>\<rightarrow> g = (\<lambda>x. uncurry g (f x))"
   1.475 +  "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod g (f x))"
   1.476  
   1.477  lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
   1.478    by (simp add: fun_eq_iff scomp_def case_prod_unfold)
   1.479  
   1.480 -lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = uncurry g (f x)"
   1.481 +lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = case_prod g (f x)"
   1.482    by (simp add: scomp_unfold case_prod_unfold)
   1.483  
   1.484  lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
   1.485 @@ -1076,25 +1041,25 @@
   1.486  lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)"
   1.487    by (blast elim: equalityE)
   1.488  
   1.489 -lemma SetCompr_Sigma_eq:
   1.490 +lemma Collect_case_prod_Sigma:
   1.491    "{(x, y). P x \<and> Q x y} = (SIGMA x:Collect P. Collect (Q x))"
   1.492    by blast
   1.493  
   1.494 -lemma Collect_split [simp]:
   1.495 +lemma Collect_case_prod [simp]:
   1.496    "{(a, b). P a \<and> Q b} = Collect P \<times> Collect Q "
   1.497 -  by (fact SetCompr_Sigma_eq)
   1.498 +  by (fact Collect_case_prod_Sigma)
   1.499  
   1.500 -lemma Collect_splitD:
   1.501 -  "x \<in> Collect (uncurry A) \<Longrightarrow> A (fst x) (snd x)"
   1.502 +lemma Collect_case_prodD:
   1.503 +  "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
   1.504    by auto
   1.505  
   1.506 -lemma Collect_split_mono:
   1.507 -  "A \<le> B \<Longrightarrow> Collect (uncurry A) \<subseteq> Collect (uncurry B)"
   1.508 +lemma Collect_case_prod_mono:
   1.509 +  "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
   1.510    by auto (auto elim!: le_funE)
   1.511  
   1.512  lemma Collect_split_mono_strong: 
   1.513    "X = fst ` A \<Longrightarrow> Y = snd ` A \<Longrightarrow> \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b
   1.514 -    \<Longrightarrow> A \<subseteq> Collect (uncurry P) \<Longrightarrow> A \<subseteq> Collect (uncurry Q)"
   1.515 +    \<Longrightarrow> A \<subseteq> Collect (case_prod P) \<Longrightarrow> A \<subseteq> Collect (case_prod Q)"
   1.516    by fastforce
   1.517    
   1.518  lemma UN_Times_distrib:
   1.519 @@ -1318,7 +1283,7 @@
   1.520    fn _ => fn ctxt => fn ct =>
   1.521      (case Thm.term_of ct of
   1.522        S as Const (@{const_name Collect}, Type (@{type_name fun}, [_, T])) $ t =>
   1.523 -        let val (u, _, ps) = HOLogic.strip_psplits t in
   1.524 +        let val (u, _, ps) = HOLogic.strip_ptupleabs t in
   1.525            (case u of
   1.526              (c as Const (@{const_name Set.member}, _)) $ q $ S' =>
   1.527                (case try (HOLogic.strip_ptuple ps) q of
   1.528 @@ -1329,7 +1294,7 @@
   1.529                    then
   1.530                      let val simp =
   1.531                        full_simp_tac (put_simpset HOL_basic_ss ctxt
   1.532 -                        addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1
   1.533 +                        addsimps [@{thm split_paired_all}, @{thm case_prod_conv}]) 1
   1.534                      in
   1.535                        SOME (Goal.prove ctxt [] []
   1.536                          (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
   1.537 @@ -1350,20 +1315,13 @@
   1.538  
   1.539  subsection \<open>Legacy theorem bindings and duplicates\<close>
   1.540  
   1.541 -abbreviation (input) case_prod :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
   1.542 -  "case_prod \<equiv> uncurry"
   1.543 -
   1.544 -abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
   1.545 -  "split \<equiv> uncurry"
   1.546 -
   1.547 -lemmas PairE = prod.exhaust
   1.548 -lemmas Pair_eq = prod.inject
   1.549  lemmas fst_conv = prod.sel(1)
   1.550  lemmas snd_conv = prod.sel(2)
   1.551 -lemmas pair_collapse = prod.collapse
   1.552 -lemmas split = split_conv
   1.553 -lemmas Pair_fst_snd_eq = prod_eq_iff
   1.554  lemmas split_def = case_prod_unfold
   1.555 +lemmas split_beta' = case_prod_beta'
   1.556 +lemmas split_beta = prod.case_eq_if
   1.557 +lemmas split_conv = case_prod_conv
   1.558 +lemmas split = case_prod_conv
   1.559  
   1.560  hide_const (open) prod
   1.561