prefer "uncurry" as canonical name for case distinction on products in combinatorial view
--- a/NEWS Sun Sep 06 22:14:51 2015 +0200
+++ b/NEWS Sun Sep 06 22:14:51 2015 +0200
@@ -187,6 +187,10 @@
constant and its defining fact become qualified, e.g. Option.is_none and
Option.is_none_def. Occasional INCOMPATIBILITY in applications.
+* Combinator to represent case distinction on products is named "uncurry",
+with "split" and "prod_case" retained as input abbreviations.
+INCOMPATIBILITY.
+
* Some old and rarely used ASCII replacement syntax has been removed.
INCOMPATIBILITY, standard syntax with symbols should be used instead.
The subsequent commands help to reproduce the old forms, e.g. to
--- a/src/HOL/Hoare/hoare_syntax.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Hoare/hoare_syntax.ML Sun Sep 06 22:14:51 2015 +0200
@@ -28,7 +28,7 @@
fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
| mk_abstuple (x :: xs) body =
- Syntax.const @{const_syntax case_prod} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
+ Syntax.const @{const_syntax uncurry} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
| mk_fbody x e (y :: xs) =
@@ -82,21 +82,21 @@
local
fun dest_abstuple
- (Const (@{const_syntax case_prod}, _) $ Abs (v, _, body)) =
+ (Const (@{const_syntax uncurry}, _) $ Abs (v, _, body)) =
subst_bound (Syntax.free v, dest_abstuple body)
| dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
| dest_abstuple tm = tm;
-fun abs2list (Const (@{const_syntax case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+fun abs2list (Const (@{const_syntax uncurry}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
| abs2list (Abs (x, T, _)) = [Free (x, T)]
| abs2list _ = [];
-fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (_, _, t)) = mk_ts t
+fun mk_ts (Const (@{const_syntax uncurry}, _) $ Abs (_, _, t)) = mk_ts t
| mk_ts (Abs (_, _, t)) = mk_ts t
| mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
| mk_ts t = [t];
-fun mk_vts (Const (@{const_syntax case_prod},_) $ Abs (x, _, t)) =
+fun mk_vts (Const (@{const_syntax uncurry},_) $ Abs (x, _, t)) =
(Syntax.free x :: abs2list t, mk_ts t)
| mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
| mk_vts _ = raise Match;
@@ -106,7 +106,7 @@
if t = Bound i then find_ch vts (i - 1) xs
else (true, (v, subst_bounds (xs, t)));
-fun is_f (Const (@{const_syntax case_prod}, _) $ Abs _) = true
+fun is_f (Const (@{const_syntax uncurry}, _) $ Abs _) = true
| is_f (Abs _) = true
| is_f _ = false;
--- a/src/HOL/Hoare/hoare_tac.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Sun Sep 06 22:14:51 2015 +0200
@@ -26,7 +26,7 @@
local
(** maps (%x1 ... xn. t) to [x1,...,xn] **)
-fun abs2list (Const (@{const_name case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+fun abs2list (Const (@{const_name uncurry}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
| abs2list (Abs (x, T, _)) = [Free (x, T)]
| abs2list _ = [];
@@ -47,7 +47,7 @@
Abs (_, T, _) => T
| Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
in
- Const (@{const_name case_prod},
+ Const (@{const_name uncurry},
(T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
absfree (x, T) z
end;
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Sun Sep 06 22:14:51 2015 +0200
@@ -22,7 +22,7 @@
section \<open>Pairs\<close>
-setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}]\<close>
+setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name uncurry}]\<close>
section \<open>Filters\<close>
--- a/src/HOL/Library/old_recdef.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML Sun Sep 06 22:14:51 2015 +0200
@@ -551,7 +551,7 @@
local
fun mk_uncurry (xt, yt, zt) =
- Const(@{const_name case_prod}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
+ Const(@{const_name uncurry}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
@@ -631,7 +631,7 @@
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
-local fun ucheck t = (if #Name (dest_const t) = @{const_name case_prod} then t
+local fun ucheck t = (if #Name (dest_const t) = @{const_name uncurry} then t
else raise Match)
in
fun dest_pabs used tm =
--- a/src/HOL/Probability/Probability_Measure.thy Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Sun Sep 06 22:14:51 2015 +0200
@@ -278,7 +278,7 @@
in
go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t
end
- | go pattern elem (Const (@{const_syntax case_prod}, _) $ t) =
+ | go pattern elem (Const (@{const_syntax uncurry}, _) $ t) =
go
((Syntax.const @{syntax_const "_pattern"}, 2) :: pattern)
(Syntax.const @{const_syntax Pair} :: elem)
--- a/src/HOL/Product_Type.thy Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Product_Type.thy Sun Sep 06 22:14:51 2015 +0200
@@ -240,7 +240,7 @@
lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
-free_constructors case_prod for Pair fst snd
+free_constructors uncurry for Pair fst snd
proof -
fix P :: bool and p :: "'a \<times> 'b"
show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
@@ -304,8 +304,8 @@
"_pattern x y" \<rightleftharpoons> "CONST Pair x y"
"_patterns x y" \<rightleftharpoons> "CONST Pair x y"
"_tuple x (_tuple_args y z)" \<rightleftharpoons> "_tuple x (_tuple_arg (_tuple y z))"
- "\<lambda>(x, y, zs). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x (y, zs). b)"
- "\<lambda>(x, y). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x y. b)"
+ "\<lambda>(x, y, zs). b" \<rightleftharpoons> "CONST uncurry (\<lambda>x (y, zs). b)"
+ "\<lambda>(x, y). b" \<rightleftharpoons> "CONST uncurry (\<lambda>x y. b)"
"_abs (CONST Pair x y) t" \<rightharpoonup> "\<lambda>(x, y). t"
-- \<open>This rule accommodates tuples in @{text "case C \<dots> (x, y) \<dots> \<Rightarrow> \<dots>"}:
The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic},
@@ -317,7 +317,7 @@
fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
| split_guess_names_tr' T [Abs (x, xT, t)] =
(case (head_of t) of
- Const (@{const_syntax case_prod}, _) => raise Match
+ Const (@{const_syntax uncurry}, _) => raise Match
| _ =>
let
val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
@@ -329,7 +329,7 @@
end)
| split_guess_names_tr' T [t] =
(case head_of t of
- Const (@{const_syntax case_prod}, _) => raise Match
+ Const (@{const_syntax uncurry}, _) => raise Match
| _ =>
let
val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
@@ -341,7 +341,7 @@
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
end)
| split_guess_names_tr' _ _ = raise Match;
- in [(@{const_syntax case_prod}, K split_guess_names_tr')] end
+ in [(@{const_syntax uncurry}, K split_guess_names_tr')] end
\<close>
@@ -379,7 +379,7 @@
constant fst \<rightharpoonup> (Haskell) "fst"
| constant snd \<rightharpoonup> (Haskell) "snd"
-lemma case_prod_unfold [nitpick_unfold]: "case_prod = (%c p. c (fst p) (snd p))"
+lemma case_prod_unfold [nitpick_unfold]: "uncurry = (%c p. c (fst p) (snd p))"
by (simp add: fun_eq_iff split: prod.split)
lemma fst_eqD: "fst (x, y) = a ==> x = a"
@@ -396,13 +396,13 @@
lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
by (simp add: prod_eq_iff)
-lemma split_conv [simp, code]: "case_prod f (a, b) = f a b"
+lemma split_conv [simp, code]: "uncurry f (a, b) = f a b"
by (fact prod.case)
-lemma splitI: "f a b \<Longrightarrow> case_prod f (a, b)"
+lemma splitI: "f a b \<Longrightarrow> uncurry f (a, b)"
by (rule split_conv [THEN iffD2])
-lemma splitD: "case_prod f (a, b) \<Longrightarrow> f a b"
+lemma splitD: "uncurry f (a, b) \<Longrightarrow> f a b"
by (rule split_conv [THEN iffD1])
lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
@@ -412,13 +412,13 @@
-- \<open>Subsumes the old @{text split_Pair} when @{term f} is the identity function.\<close>
by (simp add: fun_eq_iff split: prod.split)
-lemma split_comp: "case_prod (f \<circ> g) x = f (g (fst x)) (snd x)"
+lemma split_comp: "uncurry (f \<circ> g) x = f (g (fst x)) (snd x)"
by (cases x) simp
-lemma split_twice: "case_prod f (case_prod g p) = case_prod (\<lambda>x y. case_prod f (g x y)) p"
+lemma split_twice: "uncurry f (uncurry g p) = uncurry (\<lambda>x y. uncurry f (g x y)) p"
by (fact prod.case_distrib)
-lemma The_split: "The (case_prod P) = (THE xy. P (fst xy) (snd xy))"
+lemma The_split: "The (uncurry P) = (THE xy. P (fst xy) (snd xy))"
by (simp add: case_prod_unfold)
lemmas split_weak_cong = prod.case_cong_weak
@@ -438,7 +438,7 @@
from \<open>PROP P (fst x, snd x)\<close> show "PROP P x" by simp
qed
-lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
+lemma uncurry_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
by (cases x) simp
text \<open>
@@ -510,7 +510,7 @@
| no_args k i (Bound m) = m < k orelse m > k + i
| no_args _ _ _ = true;
fun split_pat tp i (Abs (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
- | split_pat tp i (Const (@{const_name case_prod}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
+ | split_pat tp i (Const (@{const_name uncurry}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
| split_pat tp i _ = NONE;
fun metaeq ctxt lhs rhs = mk_meta_eq (Goal.prove ctxt [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
@@ -528,12 +528,12 @@
else (subst arg k i t $ subst arg k i u)
| subst arg k i t = t;
in
- fun beta_proc ctxt (s as Const (@{const_name case_prod}, _) $ Abs (_, _, t) $ arg) =
+ fun beta_proc ctxt (s as Const (@{const_name uncurry}, _) $ Abs (_, _, t) $ arg) =
(case split_pat beta_term_pat 1 t of
SOME (i, f) => SOME (metaeq ctxt s (subst arg 0 i f))
| NONE => NONE)
| beta_proc _ _ = NONE;
- fun eta_proc ctxt (s as Const (@{const_name case_prod}, _) $ Abs (_, _, t)) =
+ fun eta_proc ctxt (s as Const (@{const_name uncurry}, _) $ Abs (_, _, t)) =
(case split_pat eta_term_pat 1 t of
SOME (_, ft) => SOME (metaeq ctxt s (let val f $ _ = ft in f end))
| NONE => NONE)
@@ -563,31 +563,31 @@
lemmas split_split_asm [no_atp] = prod.split_asm
text \<open>
- \medskip @{const case_prod} used as a logical connective or set former.
+ \medskip @{const uncurry} used as a logical connective or set former.
\medskip These rules are for use with @{text blast}; could instead
call @{text simp} using @{thm [source] prod.split} as rewrite.\<close>
-lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case_prod c p"
+lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> uncurry c p"
apply (simp only: split_tupled_all)
apply (simp (no_asm_simp))
done
-lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> case_prod c p x"
+lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> uncurry c p x"
apply (simp only: split_tupled_all)
apply (simp (no_asm_simp))
done
-lemma splitE: "case_prod c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
+lemma splitE: "uncurry c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
by (induct p) auto
-lemma splitE': "case_prod c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
+lemma splitE': "uncurry c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
by (induct p) auto
lemma splitE2:
- "[| Q (case_prod P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
+ "[| Q (uncurry P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
proof -
- assume q: "Q (case_prod P z)"
+ assume q: "Q (uncurry P z)"
assume r: "!!x y. [|z = (x, y); Q (P x y)|] ==> R"
show R
apply (rule r surjective_pairing)+
@@ -595,17 +595,17 @@
done
qed
-lemma splitD': "case_prod R (a,b) c ==> R a b c"
+lemma splitD': "uncurry R (a,b) c ==> R a b c"
by simp
-lemma mem_splitI: "z: c a b ==> z: case_prod c (a, b)"
+lemma mem_splitI: "z: c a b ==> z: uncurry c (a, b)"
by simp
-lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: case_prod c p"
+lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: uncurry c p"
by (simp only: split_tupled_all, simp)
lemma mem_splitE:
- assumes "z \<in> case_prod c p"
+ assumes "z \<in> uncurry c p"
obtains x y where "p = (x, y)" and "z \<in> c x y"
using assms by (rule splitE2)
@@ -614,7 +614,7 @@
ML \<open>
local (* filtering with exists_p_split is an essential optimization *)
- fun exists_p_split (Const (@{const_name case_prod},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
+ fun exists_p_split (Const (@{const_name uncurry},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
| exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
| exists_p_split (Abs (_, _, t)) = exists_p_split t
| exists_p_split _ = false;
@@ -633,10 +633,10 @@
lemma split_eta_SetCompr [simp, no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
by (rule ext) fast
-lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = case_prod P"
+lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = uncurry P"
by (rule ext) fast
-lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & case_prod Q ab)"
+lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & uncurry Q ab)"
-- \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
by (rule ext) blast
@@ -646,7 +646,7 @@
*)
lemma split_comp_eq:
fixes f :: "'a => 'b => 'c" and g :: "'d => 'a"
- shows "(%u. f (g (fst u)) (snd u)) = (case_prod (%x. f (g x)))"
+ shows "(%u. f (g (fst u)) (snd u)) = (uncurry (%x. f (g x)))"
by (rule ext) auto
lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
@@ -676,22 +676,22 @@
lemmas case_prodI = prod.case [THEN iffD2]
-lemma case_prodI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case_prod c p"
+lemma case_prodI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> uncurry c p"
by (fact splitI2)
-lemma case_prodI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> case_prod c p x"
+lemma case_prodI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> uncurry c p x"
by (fact splitI2')
-lemma case_prodE: "case_prod c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
+lemma case_prodE: "uncurry c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
by (fact splitE)
-lemma case_prodE': "case_prod c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
+lemma case_prodE': "uncurry c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
by (fact splitE')
declare case_prodI [intro!]
lemma case_prod_beta:
- "case_prod f p = f (fst p) (snd p)"
+ "uncurry f p = f (fst p) (snd p)"
by (fact split_beta)
lemma prod_cases3 [cases type]:
@@ -735,7 +735,7 @@
by (cases x) blast
definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
- "internal_split == case_prod"
+ "internal_split == uncurry"
lemma internal_split_conv: "internal_split c (a, b) = c a b"
by (simp only: internal_split_def split_conv)
@@ -762,10 +762,10 @@
lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q"
by (simp add: curry_def)
-lemma curry_split [simp]: "curry (case_prod f) = f"
+lemma curry_split [simp]: "curry (uncurry f) = f"
by (simp add: curry_def case_prod_unfold)
-lemma split_curry [simp]: "case_prod (curry f) = f"
+lemma split_curry [simp]: "uncurry (curry f) = f"
by (simp add: curry_def case_prod_unfold)
lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)"
@@ -778,12 +778,12 @@
notation fcomp (infixl "\<circ>>" 60)
definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60) where
- "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod g (f x))"
+ "f \<circ>\<rightarrow> g = (\<lambda>x. uncurry g (f x))"
lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
by (simp add: fun_eq_iff scomp_def case_prod_unfold)
-lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = case_prod g (f x)"
+lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = uncurry g (f x)"
by (simp add: scomp_unfold case_prod_unfold)
lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
@@ -1077,7 +1077,7 @@
by (blast elim: equalityE)
lemma SetCompr_Sigma_eq:
- "Collect (case_prod (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
+ "Collect (uncurry (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
by blast
lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q"
@@ -1314,8 +1314,11 @@
subsection \<open>Legacy theorem bindings and duplicates\<close>
+abbreviation (input) case_prod :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
+ "case_prod \<equiv> uncurry"
+
abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
- "split \<equiv> case_prod"
+ "split \<equiv> uncurry"
lemmas PairE = prod.exhaust
lemmas Pair_eq = prod.inject
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Sun Sep 06 22:14:51 2015 +0200
@@ -66,7 +66,7 @@
| unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u)
| unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
| unfold_lets_splits t = t
-and unfold_splits_lets ((t as Const (@{const_name case_prod}, _)) $ u) =
+and unfold_splits_lets ((t as Const (@{const_name uncurry}, _)) $ u) =
(case unfold_splits_lets u of
u' as Abs (s1, T1, Abs (s2, T2, _)) =>
let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Sep 06 22:14:51 2015 +0200
@@ -294,7 +294,7 @@
| (_, branches') =>
Term.list_comb (If_const (typof (hd branches')) $ tap (check_no_call bound_Ts) obj,
branches'))
- | (c as Const (@{const_name case_prod}, _), arg :: args) =>
+ | (c as Const (@{const_name uncurry}, _), arg :: args) =>
massage_rec bound_Ts
(unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
| (Const (c, _), args as _ :: _ :: _) =>
@@ -398,12 +398,12 @@
end
| NONE =>
(case t of
- Const (@{const_name case_prod}, _) $ t' =>
+ Const (@{const_name uncurry}, _) $ t' =>
let
val U' = curried_type U;
val T' = curried_type T;
in
- Const (@{const_name case_prod}, U' --> U) $ massage_any_call bound_Ts U' T' t'
+ Const (@{const_name uncurry}, U' --> U) $ massage_any_call bound_Ts U' T' t'
end
| t1 $ t2 =>
(if has_call t2 then
@@ -927,7 +927,7 @@
let val (u, vs) = strip_comb t in
if is_Free u andalso has_call u then
Inr_const T U2 $ mk_tuple1_balanced bound_Ts vs
- else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
+ else if try (fst o dest_Const) u = SOME @{const_name uncurry} then
map (rewrite bound_Ts) vs |> chop 1
|>> HOLogic.mk_split o the_single
|> Term.list_comb
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Sun Sep 06 22:14:51 2015 +0200
@@ -164,7 +164,7 @@
set_cases = @{thms fsts.cases[unfolded eq_fst_iff ex_neg_all_pos]
snds.cases[unfolded eq_snd_iff ex_neg_all_pos]}},
fp_co_induct_sugar =
- {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
+ {co_rec = Const (@{const_name uncurry}, (ctr_Ts ---> C) --> fpT --> C),
common_co_inducts = @{thms prod.induct},
co_inducts = @{thms prod.induct},
co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Sep 06 22:14:51 2015 +0200
@@ -2287,7 +2287,7 @@
HOLogic.Collect_const tuple_T $ list_comb (Const base_x, outer_bounds)
val step_set =
HOLogic.Collect_const prod_T
- $ (Const (@{const_name case_prod}, curried_T --> uncurried_T)
+ $ (Const (@{const_name uncurry}, curried_T --> uncurried_T)
$ list_comb (Const step_x, outer_bounds))
val image_set =
image_const $ (rtrancl_const $ step_set) $ base_set
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Sep 06 22:14:51 2015 +0200
@@ -1023,7 +1023,7 @@
(* Definition of executable functions and their intro and elim rules *)
-fun strip_split_abs (Const (@{const_name case_prod}, _) $ t) = strip_split_abs t
+fun strip_split_abs (Const (@{const_name uncurry}, _) $ t) = strip_split_abs t
| strip_split_abs (Abs (_, _, t)) = strip_split_abs t
| strip_split_abs t = t
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sun Sep 06 22:14:51 2015 +0200
@@ -316,7 +316,7 @@
fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
fun mk_split T = Sign.mk_const thy
- (@{const_name case_prod}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
+ (@{const_name uncurry}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
fun mk_scomp_split T t t' =
mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
(mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
@@ -362,7 +362,7 @@
fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
fun mk_split T = Sign.mk_const thy
- (@{const_name case_prod}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
+ (@{const_name uncurry}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
fun mk_scomp_split T t t' =
mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
(mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
--- a/src/HOL/Tools/Quotient/quotient_term.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Sun Sep 06 22:14:51 2015 +0200
@@ -634,12 +634,12 @@
end
end
- | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
- ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
+ | (((t1 as Const (@{const_name uncurry}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
+ ((t2 as Const (@{const_name uncurry}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
- | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, s1)),
- ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , s2))) =>
+ | (((t1 as Const (@{const_name uncurry}, _)) $ Abs (v1, ty, s1)),
+ ((t2 as Const (@{const_name uncurry}, _)) $ Abs (v2, _ , s2))) =>
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
| (t1 $ t2, t1' $ t2') =>
--- a/src/HOL/Tools/hologic.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/hologic.ML Sun Sep 06 22:14:51 2015 +0200
@@ -349,12 +349,12 @@
end;
fun split_const (A, B, C) =
- Const ("Product_Type.prod.case_prod", (A --> B --> C) --> mk_prodT (A, B) --> C);
+ Const ("Product_Type.prod.uncurry", (A --> B --> C) --> mk_prodT (A, B) --> C);
fun mk_split t =
(case Term.fastype_of t of
T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
- Const ("Product_Type.prod.case_prod", T --> mk_prodT (A, B) --> C) $ t
+ Const ("Product_Type.prod.uncurry", T --> mk_prodT (A, B) --> C) $ t
| _ => raise TERM ("mk_split: bad body type", [t]));
(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
@@ -470,7 +470,7 @@
val strip_psplits =
let
fun strip [] qs Ts t = (t, rev Ts, qs)
- | strip (p :: ps) qs Ts (Const ("Product_Type.prod.case_prod", _) $ t) =
+ | strip (p :: ps) qs Ts (Const ("Product_Type.prod.uncurry", _) $ t) =
strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
| strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
| strip (p :: ps) qs Ts t = strip ps qs
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Sun Sep 06 22:14:51 2015 +0200
@@ -92,7 +92,7 @@
val strip_psplits =
let
fun strip [] qs vs t = (t, rev vs, qs)
- | strip (p :: ps) qs vs (Const (@{const_name Product_Type.prod.case_prod}, _) $ t) =
+ | strip (p :: ps) qs vs (Const (@{const_name uncurry}, _) $ t) =
strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t
| strip (_ :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t
| strip (_ :: ps) qs vs t = strip ps qs
@@ -305,7 +305,7 @@
(* proof tactic *)
-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)}
+val case_prod_distrib = @{lemma "(uncurry g x) z = uncurry (\<lambda>x y. (g x y) z) x" by (simp add: case_prod_beta)}
val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp}
val vimageE' =