--- a/NEWS Tue Oct 13 09:21:14 2015 +0200
+++ b/NEWS Tue Oct 13 09:21:15 2015 +0200
@@ -229,6 +229,52 @@
*** HOL ***
+* Combinator to represent case distinction on products is named "case_prod",
+uniformly, discontinuing any input aliasses. Very popular theorem aliasses
+have been retained.
+Consolidated facts:
+ PairE ~> prod.exhaust
+ Pair_eq ~> prod.inject
+ pair_collapse ~> prod.collapse
+ Pair_fst_snd_eq ~> prod_eq_iff
+ split_twice ~> prod.case_distrib
+ split_weak_cong ~> prod.case_cong_weak
+ split_split ~> prod.split
+ split_split_asm ~> prod.split_asm
+ splitI ~> case_prodI
+ splitD ~> case_prodD
+ splitI2 ~> case_prodI2
+ splitI2' ~> case_prodI2'
+ splitE ~> case_prodE
+ splitE' ~> case_prodE'
+ split_pair ~> case_prod_Pair
+ split_eta ~> case_prod_eta
+ split_comp ~> case_prod_comp
+ mem_splitI ~> mem_case_prodI
+ mem_splitI2 ~> mem_case_prodI2
+ mem_splitE ~> mem_case_prodE
+ The_split ~> The_case_prod
+ cond_split_eta ~> cond_case_prod_eta
+ Collect_split_in_rel_leE ~> Collect_case_prod_in_rel_leE
+ Collect_split_in_rel_leI ~> Collect_case_prod_in_rel_leI
+ in_rel_Collect_split_eq ~> in_rel_Collect_case_prod_eq
+ Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD
+ Collect_split_Grp_inD ~> Collect_case_prod_Grp_in
+ Domain_Collect_split ~> Domain_Collect_case_prod
+ Image_Collect_split ~> Image_Collect_case_prod
+ Range_Collect_split ~> Range_Collect_case_prod
+ Eps_split ~> Eps_case_prod
+ Eps_split_eq ~> Eps_case_prod_eq
+ split_rsp ~> case_prod_rsp
+ curry_split ~> curry_case_prod
+ split_curry ~> case_prod_curry
+Changes in structure HOLogic:
+ split_const ~> case_prod_const
+ mk_split ~> mk_case_prod
+ mk_psplits ~> mk_ptupleabs
+ strip_psplits ~> strip_ptupleabs
+INCOMPATIBILITY.
+
* Commands 'inductive' and 'inductive_set' work better when names for
intro rules are omitted: the "cases" and "induct" rules no longer
declare empty case_names, but no case_names at all. This allows to use
@@ -247,14 +293,6 @@
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.
-Hence, the "uncurry"-expressions are printed the following way:
-a) fully applied "uncurry f p": explicit case-expression;
-b) partially applied "uncurry f": explicit paired abstraction;
-c) unapplied "uncurry": as it is.
-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/Doc/Datatypes/Datatypes.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Oct 13 09:21:15 2015 +0200
@@ -2775,12 +2775,12 @@
next
fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
show "rel_fn R =
- (BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn fst))\<inverse>\<inverse> OO
- BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
+ (BNF_Def.Grp {x. set_fn x \<subseteq> {(x, y). R x y}} (map_fn fst))\<inverse>\<inverse> OO
+ BNF_Def.Grp {x. set_fn x \<subseteq> {(x, y). R x y}} (map_fn snd)"
unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
apply transfer
unfolding rel_fun_def subset_iff image_iff
- by auto (force, metis pair_collapse)
+ by auto (force, metis prod.collapse)
qed
text {* \blankline *}
--- a/src/Doc/Isar_Ref/Generic.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Tue Oct 13 09:21:15 2015 +0200
@@ -1130,9 +1130,9 @@
@{text [display] "?P (if ?Q ?x ?y) \<longleftrightarrow> (?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y)"}
Another example is the elimination operator for Cartesian products
- (which happens to be called @{text split} in Isabelle/HOL:
+ (which happens to be called @{const case_prod} in Isabelle/HOL:
- @{text [display] "?P (split ?f ?p) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?P (f a b))"}
+ @{text [display] "?P (case_prod ?f ?p) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?P (f a b))"}
For technical reasons, there is a distinction between case splitting
in the conclusion and in the premises of a subgoal. The former is
--- a/src/Doc/Logics/document/HOL.tex Tue Oct 13 09:21:14 2015 +0200
+++ b/src/Doc/Logics/document/HOL.tex Tue Oct 13 09:21:15 2015 +0200
@@ -1013,22 +1013,22 @@
$[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
& general sum of sets
\end{constants}
-%\tdx{fst_def} fst p == @a. ? b. p = (a,b)
-%\tdx{snd_def} snd p == @b. ? a. p = (a,b)
-%\tdx{split_def} split c p == c (fst p) (snd p)
+%\tdx{fst_def} fst p == @a. ? b. p = (a,b)
+%\tdx{snd_def} snd p == @b. ? a. p = (a,b)
+%\tdx{split_def} case_prod c p == c (fst p) (snd p)
\begin{ttbox}\makeatletter
\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}
-\tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b')
+\tdx{prod.inject} ((a,b) = (a',b')) = (a=a' & b=b')
\tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R
-\tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q
+\tdx{prod.exhaust} [| !!x y. p = (x,y) ==> Q |] ==> Q
\tdx{fst_conv} fst (a,b) = a
\tdx{snd_conv} snd (a,b) = b
\tdx{surjective_pairing} p = (fst p,snd p)
-\tdx{split} split c (a,b) = c a b
-\tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
+\tdx{split} case_prod c (a,b) = c a b
+\tdx{prod.split} R(case_prod c p) = (! x y. p = (x,y) --> R(c x y))
\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B
@@ -1059,8 +1059,8 @@
\begin{eqnarray*}
\hbox{\tt\%($x$,$y$,$z$).\ $t$}
& \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\
- & \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\
- & \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))}
+ & \leadsto & \hbox{\tt case_prod(\%$x$.\%($y$,$z$).\ $t$)}\\
+ & \leadsto & \hbox{\tt case_prod(\%$x$.\ case_prod(\%$y$ $z$.\ $t$))}
\end{eqnarray*}
The reverse translation is performed upon printing.
\begin{warn}
--- a/src/Doc/Main/Main_Doc.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/Doc/Main/Main_Doc.thy Tue Oct 13 09:21:15 2015 +0200
@@ -218,7 +218,7 @@
@{const Pair} & @{typeof Pair}\\
@{const fst} & @{typeof fst}\\
@{const snd} & @{typeof snd}\\
-@{const split} & @{typeof split}\\
+@{const case_prod} & @{typeof case_prod}\\
@{const curry} & @{typeof curry}\\
@{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\
\end{supertabular}
@@ -227,7 +227,7 @@
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
@{term"Pair a b"} & @{term[source]"Pair a b"}\\
-@{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\
+@{term"case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
@{term"A <*> B"} & @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$)
\end{tabular}
--- a/src/Doc/Tutorial/Types/Pairs.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/Doc/Tutorial/Types/Pairs.thy Tue Oct 13 09:21:15 2015 +0200
@@ -36,7 +36,7 @@
instead of @{text"\<lambda>(x,y). x+y"}. These terms are distinct even though they
denote the same function.
-Internally, @{term"%(x,y). t"} becomes @{text"split (\<lambda>x y. t)"}, where
+Internally, @{term"%(x,y). t"} becomes @{text"case_prod (\<lambda>x y. t)"}, where
\cdx{split} is the uncurrying function of type @{text"('a \<Rightarrow> 'b
\<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"} defined as
\begin{center}
@@ -71,13 +71,13 @@
@{thm split_conv[no_vars]} and @{thm fst_conv[no_vars]}.
To reason about tuple patterns requires some way of
converting a variable of product type into a pair.
-In case of a subterm of the form @{term"split f p"} this is easy: the split
-rule @{thm[source]split_split} replaces @{term p} by a pair:%
+In case of a subterm of the form @{term"case_prod f p"} this is easy: the split
+rule @{thm[source]prod.split} replaces @{term p} by a pair:%
\index{*split (method)}
*}
lemma "(\<lambda>(x,y).y) p = snd p"
-apply(split split_split)
+apply(split prod.split)
txt{*
@{subgoals[display,indent=0]}
@@ -87,7 +87,7 @@
(*<*)
by simp
lemma "(\<lambda>(x,y).y) p = snd p"(*>*)
-by(simp split: split_split)
+by(simp split: prod.split)
text{*
Let us look at a second example:
@@ -102,30 +102,30 @@
can be split as above. The same is true for paired set comprehension:
*}
-(*<*)by(simp split: split_split)(*>*)
+(*<*)by(simp split: prod.split)(*>*)
lemma "p \<in> {(x,y). x=y} \<longrightarrow> fst p = snd p"
apply simp
txt{*
@{subgoals[display,indent=0]}
-Again, simplification produces a term suitable for @{thm[source]split_split}
+Again, simplification produces a term suitable for @{thm[source]prod.split}
as above. If you are worried about the strange form of the premise:
-@{text"split (op =)"} is short for @{term"\<lambda>(x,y). x=y"}.
+@{text"case_prod (op =)"} is short for @{term"\<lambda>(x,y). x=y"}.
The same proof procedure works for
*}
-(*<*)by(simp split: split_split)(*>*)
+(*<*)by(simp split: prod.split)(*>*)
lemma "p \<in> {(x,y). x=y} \<Longrightarrow> fst p = snd p"
txt{*\noindent
-except that we now have to use @{thm[source]split_split_asm}, because
+except that we now have to use @{thm[source]prod.split_asm}, because
@{term split} occurs in the assumptions.
However, splitting @{term split} is not always a solution, as no @{term split}
may be present in the goal. Consider the following function:
*}
-(*<*)by(simp split: split_split_asm)(*>*)
+(*<*)by(simp split: prod.split_asm)(*>*)
primrec swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a" where "swap (x,y) = (y,x)"
text{*\noindent
--- a/src/HOL/BNF_Def.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/BNF_Def.thy Tue Oct 13 09:21:15 2015 +0200
@@ -15,7 +15,7 @@
"bnf" :: thy_goal
begin
-lemma Collect_splitD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
+lemma Collect_case_prodD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
by auto
inductive
@@ -61,7 +61,7 @@
lemma predicate2_transferD:
"\<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>
P (fst a) (fst b) \<longleftrightarrow> Q (snd a) (snd b)"
- unfolding rel_fun_def by (blast dest!: Collect_splitD)
+ unfolding rel_fun_def by (blast dest!: Collect_case_prodD)
definition collect where
"collect F x = (\<Union>f \<in> F. f x)"
@@ -131,10 +131,10 @@
lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
unfolding Grp_def by auto
-lemma Collect_split_Grp_eqD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
+lemma Collect_case_prod_Grp_eqD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
unfolding Grp_def comp_def by auto
-lemma Collect_split_Grp_inD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> fst z \<in> A"
+lemma Collect_case_prod_Grp_in: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> fst z \<in> A"
unfolding Grp_def comp_def by auto
definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
--- a/src/HOL/BNF_Greatest_Fixpoint.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy Tue Oct 13 09:21:15 2015 +0200
@@ -82,13 +82,13 @@
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})"
by blast
-lemma in_rel_Collect_split_eq: "in_rel (Collect (case_prod X)) = X"
+lemma in_rel_Collect_case_prod_eq: "in_rel (Collect (case_prod X)) = X"
unfolding fun_eq_iff by auto
-lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
+lemma Collect_case_prod_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
by auto
-lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
+lemma Collect_case_prod_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
by force
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
--- a/src/HOL/Bali/AxCompl.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Bali/AxCompl.thy Tue Oct 13 09:21:15 2015 +0200
@@ -1446,7 +1446,7 @@
lemma MGF_simult_Methd: "wf_prog G \<Longrightarrow>
G,({}::state triple set)|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>})
- ` Collect (split (is_methd G)) "
+ ` Collect (case_prod (is_methd G)) "
apply (frule finite_is_methd [OF wf_ws_prog])
apply (rule MGF_simult_Methd_lemma)
apply assumption
--- a/src/HOL/Bali/AxSem.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Bali/AxSem.thy Tue Oct 13 09:21:15 2015 +0200
@@ -969,7 +969,7 @@
done
lemma ax_methods_spec:
-"\<lbrakk>G,(A::'a triple set)|\<turnstile>split f ` ms; (C,sig) \<in> ms\<rbrakk>\<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)"
+"\<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)"
apply (erule ax_derivs.weaken)
apply (force del: image_eqI intro: rev_image_eqI)
done
@@ -977,7 +977,7 @@
(* this version is used to avoid using the cut rule *)
lemma ax_finite_pointwise_lemma [rule_format]: "\<lbrakk>F \<subseteq> ms; finite ms\<rbrakk> \<Longrightarrow>
((\<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>
- G,A|\<turnstile>split f ` F \<longrightarrow> G,A|\<turnstile>split g ` F"
+ G,A|\<turnstile>case_prod f ` F \<longrightarrow> G,A|\<turnstile>case_prod g ` F"
apply (frule (1) finite_subset)
apply (erule rev_mp)
apply (erule thin_rl)
--- a/src/HOL/Bali/Basis.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Bali/Basis.thy Tue Oct 13 09:21:15 2015 +0200
@@ -16,7 +16,7 @@
declare if_weak_cong [cong del] option.case_cong_weak [cong del]
declare length_Suc_conv [iff]
-lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
+lemma Collect_split_eq: "{p. P (case_prod f p)} = {(a,b). P (f a b)}"
by auto
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)"
--- a/src/HOL/Bali/DeclConcepts.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy Tue Oct 13 09:21:15 2015 +0200
@@ -2178,14 +2178,14 @@
apply (subst fields_rec, assumption)
apply clarify
apply (simp only: map_of_append)
-apply (case_tac "table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn")
+apply (case_tac "table_of (map (case_prod (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn")
apply (force intro:rtrancl_into_rtrancl2 simp add: map_add_def)
apply (frule_tac fd="Ca" in fields_norec)
apply assumption
apply blast
apply (frule table_of_fieldsD)
-apply (frule_tac n="table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c))"
+apply (frule_tac n="table_of (map (case_prod (\<lambda>fn. Pair (fn, Ca))) (cfields c))"
and m="table_of (if Ca = Object then [] else fields G (super c))"
in map_add_find_right)
apply (case_tac "efn")
@@ -2272,9 +2272,9 @@
done
lemma finite_is_methd:
- "ws_prog G \<Longrightarrow> finite (Collect (split (is_methd G)))"
+ "ws_prog G \<Longrightarrow> finite (Collect (case_prod (is_methd G)))"
apply (unfold is_methd_def)
-apply (subst SetCompr_Sigma_eq)
+apply (subst Collect_case_prod_Sigma)
apply (rule finite_is_class [THEN finite_SigmaI])
apply (simp only: mem_Collect_eq)
apply (fold dom_def)
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Tue Oct 13 09:21:15 2015 +0200
@@ -3962,7 +3962,7 @@
moreover
from upd normal_s2
have "{vn} \<subseteq> dom (locals (store (assign upd v s2)))"
- by (auto simp add: assign_def Let_def lvar_def upd split: split_split)
+ by (auto simp add: assign_def Let_def lvar_def upd split: prod.split)
ultimately
show "nrm A \<subseteq> \<dots>"
by (rule Un_least [elim_format]) (simp add: nrm_A)
--- a/src/HOL/Bali/Example.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Bali/Example.thy Tue Oct 13 09:21:15 2015 +0200
@@ -1247,7 +1247,7 @@
abbreviation "s9' == (Some (Xcpt (Std IndOutBound)), s8)"
-declare Pair_eq [simp del]
+declare prod.inject [simp del]
schematic_goal exec_test:
"\<lbrakk>the (new_Addr (heap s1)) = a;
the (new_Addr (heap ?s2)) = b;
@@ -1377,6 +1377,6 @@
apply (simp (no_asm_simp))
apply (auto simp add: in_bounds_def)
done
-declare Pair_eq [simp]
+declare prod.inject [simp]
end
--- a/src/HOL/Bali/State.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Bali/State.thy Tue Oct 13 09:21:15 2015 +0200
@@ -143,7 +143,7 @@
definition
fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool) \<Rightarrow> (fspec, ty) table" where
"fields_table G C P =
- map_option type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
+ map_option type \<circ> table_of (filter (case_prod P) (DeclConcepts.fields G C))"
lemma fields_table_SomeI:
"\<lbrakk>table_of (DeclConcepts.fields G C) n = Some f; P n f\<rbrakk>
--- a/src/HOL/Cardinals/Bounded_Set.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Cardinals/Bounded_Set.thy Tue Oct 13 09:21:15 2015 +0200
@@ -50,7 +50,7 @@
BNF_Def.Grp {a. set_bset a \<subseteq> {(a, b). R a b}} (map_bset snd)) a b" (is "?L \<longleftrightarrow> ?R")
proof
assume ?L
- def R' \<equiv> "the_inv set_bset (Collect (split R) \<inter> (set_bset a \<times> set_bset b)) :: ('a \<times> 'b) set['k]"
+ def R' \<equiv> "the_inv set_bset (Collect (case_prod R) \<inter> (set_bset a \<times> set_bset b)) :: ('a \<times> 'b) set['k]"
(is "the_inv set_bset ?L'")
have "|?L'| <o natLeq +c |UNIV :: 'k set|"
unfolding csum_def Field_natLeq
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy Tue Oct 13 09:21:15 2015 +0200
@@ -1012,7 +1012,7 @@
proof-
have "?L = (n, (id \<oplus> root) ` cont (pick n))"
unfolding cont_H image_comp map_sum.comp id_comp comp_assoc[symmetric]
- unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
+ unfolding prod.inject apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
by (rule root_H_root[OF n])
moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
ultimately show ?thesis by simp
--- a/src/HOL/Decision_Procs/Ferrack.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Tue Oct 13 09:21:15 2015 +0200
@@ -1129,7 +1129,7 @@
by pat_completeness auto
termination rsplit0 by (relation "measure num_size") simp_all
-lemma rsplit0: "Inum bs ((split (CN 0)) (rsplit0 t)) = Inum bs t \<and> numbound0 (snd (rsplit0 t))"
+lemma rsplit0: "Inum bs ((case_prod (CN 0)) (rsplit0 t)) = Inum bs t \<and> numbound0 (snd (rsplit0 t))"
proof (induct t rule: rsplit0.induct)
case (2 a b)
let ?sa = "rsplit0 a"
@@ -1140,8 +1140,8 @@
let ?tb = "snd ?sb"
from 2 have nb: "numbound0 (snd(rsplit0 (Add a b)))"
by (cases "rsplit0 a") (auto simp add: Let_def split_def)
- have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) =
- Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)"
+ have "Inum bs ((case_prod (CN 0)) (rsplit0 (Add a b))) =
+ Inum bs ((case_prod (CN 0)) ?sa)+Inum bs ((case_prod (CN 0)) ?sb)"
by (simp add: Let_def split_def algebra_simps)
also have "\<dots> = Inum bs a + Inum bs b"
using 2 by (cases "rsplit0 a") auto
@@ -1180,38 +1180,38 @@
"neq c t = (if c = 0 then (NEq t) else if c > 0 then (NEq (CN 0 c t))
else (NEq (CN 0 (-c) (Neg t))))"
-lemma lt: "numnoabs t \<Longrightarrow> Ifm bs (split lt (rsplit0 t)) =
- Ifm bs (Lt t) \<and> isrlfm (split lt (rsplit0 t))"
+lemma lt: "numnoabs t \<Longrightarrow> Ifm bs (case_prod lt (rsplit0 t)) =
+ Ifm bs (Lt t) \<and> isrlfm (case_prod lt (rsplit0 t))"
using rsplit0[where bs = "bs" and t="t"]
by (auto simp add: lt_def split_def, cases "snd(rsplit0 t)", auto,
rename_tac nat a b, case_tac "nat", auto)
-lemma le: "numnoabs t \<Longrightarrow> Ifm bs (split le (rsplit0 t)) =
- Ifm bs (Le t) \<and> isrlfm (split le (rsplit0 t))"
+lemma le: "numnoabs t \<Longrightarrow> Ifm bs (case_prod le (rsplit0 t)) =
+ Ifm bs (Le t) \<and> isrlfm (case_prod le (rsplit0 t))"
using rsplit0[where bs = "bs" and t="t"]
by (auto simp add: le_def split_def, cases "snd(rsplit0 t)", auto,
rename_tac nat a b, case_tac "nat", auto)
-lemma gt: "numnoabs t \<Longrightarrow> Ifm bs (split gt (rsplit0 t)) =
- Ifm bs (Gt t) \<and> isrlfm (split gt (rsplit0 t))"
+lemma gt: "numnoabs t \<Longrightarrow> Ifm bs (case_prod gt (rsplit0 t)) =
+ Ifm bs (Gt t) \<and> isrlfm (case_prod gt (rsplit0 t))"
using rsplit0[where bs = "bs" and t="t"]
by (auto simp add: gt_def split_def, cases "snd(rsplit0 t)", auto,
rename_tac nat a b, case_tac "nat", auto)
-lemma ge: "numnoabs t \<Longrightarrow> Ifm bs (split ge (rsplit0 t)) =
- Ifm bs (Ge t) \<and> isrlfm (split ge (rsplit0 t))"
+lemma ge: "numnoabs t \<Longrightarrow> Ifm bs (case_prod ge (rsplit0 t)) =
+ Ifm bs (Ge t) \<and> isrlfm (case_prod ge (rsplit0 t))"
using rsplit0[where bs = "bs" and t="t"]
by (auto simp add: ge_def split_def, cases "snd(rsplit0 t)", auto,
rename_tac nat a b, case_tac "nat", auto)
-lemma eq: "numnoabs t \<Longrightarrow> Ifm bs (split eq (rsplit0 t)) =
- Ifm bs (Eq t) \<and> isrlfm (split eq (rsplit0 t))"
+lemma eq: "numnoabs t \<Longrightarrow> Ifm bs (case_prod eq (rsplit0 t)) =
+ Ifm bs (Eq t) \<and> isrlfm (case_prod eq (rsplit0 t))"
using rsplit0[where bs = "bs" and t="t"]
by (auto simp add: eq_def split_def, cases "snd(rsplit0 t)", auto,
rename_tac nat a b, case_tac "nat", auto)
-lemma neq: "numnoabs t \<Longrightarrow> Ifm bs (split neq (rsplit0 t)) =
- Ifm bs (NEq t) \<and> isrlfm (split neq (rsplit0 t))"
+lemma neq: "numnoabs t \<Longrightarrow> Ifm bs (case_prod neq (rsplit0 t)) =
+ Ifm bs (NEq t) \<and> isrlfm (case_prod neq (rsplit0 t))"
using rsplit0[where bs = "bs" and t="t"]
by (auto simp add: neq_def split_def, cases "snd(rsplit0 t)", auto,
rename_tac nat a b, case_tac "nat", auto)
@@ -1228,12 +1228,12 @@
"rlfm (Or p q) = disj (rlfm p) (rlfm q)"
"rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
"rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))"
- "rlfm (Lt a) = split lt (rsplit0 a)"
- "rlfm (Le a) = split le (rsplit0 a)"
- "rlfm (Gt a) = split gt (rsplit0 a)"
- "rlfm (Ge a) = split ge (rsplit0 a)"
- "rlfm (Eq a) = split eq (rsplit0 a)"
- "rlfm (NEq a) = split neq (rsplit0 a)"
+ "rlfm (Lt a) = case_prod lt (rsplit0 a)"
+ "rlfm (Le a) = case_prod le (rsplit0 a)"
+ "rlfm (Gt a) = case_prod gt (rsplit0 a)"
+ "rlfm (Ge a) = case_prod ge (rsplit0 a)"
+ "rlfm (Eq a) = case_prod eq (rsplit0 a)"
+ "rlfm (NEq a) = case_prod neq (rsplit0 a)"
"rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
"rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
"rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
@@ -2430,7 +2430,7 @@
using uset_cong[OF lq YU U_l Y_l] by (simp only: split_def fst_conv snd_conv simpfm)
also have "\<dots> = (Ifm (x#bs) ?res)"
using evaldjf_ex[where ps="?Y" and bs = "x#bs" and f="simpfm \<circ> (usubst ?q)",symmetric]
- by (simp add: split_def pair_collapse)
+ by (simp add: split_def prod.collapse)
finally have lheq: "?lhs = Ifm bs (decr ?res)"
using decr[OF nbth] by blast
then have lr: "?lhs = ?rhs"
--- a/src/HOL/Decision_Procs/MIR.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Tue Oct 13 09:21:15 2015 +0200
@@ -5072,7 +5072,7 @@
by (simp only: split_def fst_conv snd_conv)
also have "\<dots> = (Ifm (x#bs) ?ep)"
using evaldjf_ex[where ps="?Y" and bs = "x#bs" and f="\<upsilon> ?q",symmetric]
- by (simp only: split_def pair_collapse)
+ by (simp only: split_def prod.collapse)
also have "\<dots> = (Ifm bs (decr ?ep))" using decr[OF ep_nb] by blast
finally have lr: "?lhs = ?rhs" by (simp only: ferrack01_def Let_def)
from decr_qf[OF ep_nb] have "qfree (ferrack01 p)" by (simp only: Let_def ferrack01_def)
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Oct 13 09:21:15 2015 +0200
@@ -2608,7 +2608,7 @@
section \<open>First implementation : Naive by encoding all case splits locally\<close>
definition "msubsteq c t d s a r =
- evaldjf (split conj)
+ evaldjf (case_prod conj)
[(let cd = c *\<^sub>p d
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)))),
(conj (Eq (CP c)) (NEq (CP d)), Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
@@ -2626,7 +2626,7 @@
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)))),
(conj (Eq (CP c)) (NEq (CP d)), Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
(conj (NEq (CP c)) (Eq (CP d)), Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
- (conj (Eq (CP c)) (Eq (CP d)), Eq r)]. bound0 (split conj x)"
+ (conj (Eq (CP c)) (Eq (CP d)), Eq r)]. bound0 (case_prod conj x)"
using lp by (simp add: Let_def t s)
from evaldjf_bound0[OF th] show ?thesis
by (simp add: msubsteq_def)
@@ -2715,7 +2715,7 @@
definition "msubstneq c t d s a r =
- evaldjf (split conj)
+ evaldjf (case_prod conj)
[(let cd = c *\<^sub>p d
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)))),
(conj (Eq (CP c)) (NEq (CP d)), NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
@@ -2733,7 +2733,7 @@
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)))),
(conj (Eq (CP c)) (NEq (CP d)), NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
(conj (NEq (CP c)) (Eq (CP d)), NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
- (conj (Eq (CP c)) (Eq (CP d)), NEq r)]. bound0 (split conj x)"
+ (conj (Eq (CP c)) (Eq (CP d)), NEq r)]. bound0 (case_prod conj x)"
using lp by (simp add: Let_def t s)
from evaldjf_bound0[OF th] show ?thesis
by (simp add: msubstneq_def)
@@ -2821,7 +2821,7 @@
qed
definition "msubstlt c t d s a r =
- evaldjf (split conj)
+ evaldjf (case_prod conj)
[(let cd = c *\<^sub>p d
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)))),
(let cd = c *\<^sub>p d
@@ -2847,7 +2847,7 @@
(conj (lt (CP c)) (Eq (CP d)), Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
(conj (lt (CP (~\<^sub>p d))) (Eq (CP c)), Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
(conj (lt (CP d)) (Eq (CP c)), Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
- (conj (Eq (CP c)) (Eq (CP d)), Lt r)]. bound0 (split conj x)"
+ (conj (Eq (CP c)) (Eq (CP d)), Lt r)]. bound0 (case_prod conj x)"
using lp by (simp add: Let_def t s lt_nb)
from evaldjf_bound0[OF th] show ?thesis
by (simp add: msubstlt_def)
@@ -3027,7 +3027,7 @@
qed
definition "msubstle c t d s a r =
- evaldjf (split conj)
+ evaldjf (case_prod conj)
[(let cd = c *\<^sub>p d
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)))),
(let cd = c *\<^sub>p d
@@ -3053,7 +3053,7 @@
(conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
(conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
(conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
- (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (split conj x)"
+ (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (case_prod conj x)"
using lp by (simp add: Let_def t s lt_nb)
from evaldjf_bound0[OF th] show ?thesis
by (simp add: msubstle_def)
--- a/src/HOL/HOLCF/Fix.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/HOLCF/Fix.thy Tue Oct 13 09:21:15 2015 +0200
@@ -178,15 +178,15 @@
assumes step: "\<And>x y. P x y \<Longrightarrow> P (F\<cdot>x) (G\<cdot>y)"
shows "P (fix\<cdot>F) (fix\<cdot>G)"
proof -
- from adm have adm': "adm (split P)"
+ from adm have adm': "adm (case_prod P)"
unfolding split_def .
have "\<And>i. P (iterate i\<cdot>F\<cdot>\<bottom>) (iterate i\<cdot>G\<cdot>\<bottom>)"
by (induct_tac i, simp add: base, simp add: step)
- hence "\<And>i. split P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
+ hence "\<And>i. case_prod P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
by simp
- hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
+ hence "case_prod P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
by - (rule admD [OF adm'], simp, assumption)
- hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
+ hence "case_prod P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
by (simp add: lub_Pair)
hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
by simp
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Tue Oct 13 09:21:15 2015 +0200
@@ -362,7 +362,7 @@
fun Seq_Finite_induct_tac i = erule Seq_Finite_ind i
THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
-fun pair_tac s = rule_tac p",s)] PairE
+fun pair_tac s = rule_tac p",s)] prod.exhaust
THEN' hyp_subst_tac THEN' Simp_tac;
*)
(* induction on a sequence of pairs with pairsplitting and simplification *)
@@ -1102,7 +1102,7 @@
THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));
fun pair_tac ctxt s =
- Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), s)] [] @{thm PairE}
+ Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), s)] [] @{thm prod.exhaust}
THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;
(* induction on a sequence of pairs with pairsplitting and simplification *)
--- a/src/HOL/HOLCF/Product_Cpo.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/HOLCF/Product_Cpo.thy Tue Oct 13 09:21:15 2015 +0200
@@ -169,7 +169,7 @@
lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
by simp
-lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
+lemma split_strict [simp]: "case_prod f \<bottom> = f \<bottom> \<bottom>"
unfolding split_def by simp
subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
@@ -235,7 +235,7 @@
have "cont (\<lambda>(x, y). f (x, y))"
by (intro cont2cont_case_prod f1 f2 cont2cont)
thus "cont f"
- by (simp only: split_eta)
+ by (simp only: case_prod_eta)
qed
lemma prod_cont_iff:
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Oct 13 09:21:15 2015 +0200
@@ -688,7 +688,7 @@
val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy
val start_rules =
@{thms lub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
- @ @{thms pair_collapse split_def}
+ @ @{thms prod.collapse split_def}
@ map_apply_thms @ map_ID_thms
val rules0 =
@{thms iterate_0 Pair_strict} @ take_0_thms
--- a/src/HOL/HOLCF/Tools/holcf_library.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML Tue Oct 13 09:21:15 2015 +0200
@@ -149,7 +149,7 @@
fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
| lambda_tuple (v::[]) rhs = Term.lambda v rhs
| lambda_tuple (v::vs) rhs =
- HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs))
+ HOLogic.mk_case_prod (Term.lambda v (lambda_tuple vs rhs))
(*** Lifted cpo type ***)
--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy Tue Oct 13 09:21:15 2015 +0200
@@ -465,7 +465,7 @@
"(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
= (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
-apply (simp only: map_apply_thms pair_collapse)
+apply (simp only: map_apply_thms prod.collapse)
apply (simp only: fix_def2)
apply (rule lub_eq)
apply (rule nat.induct)
--- a/src/HOL/Hilbert_Choice.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Hilbert_Choice.thy Tue Oct 13 09:21:15 2015 +0200
@@ -546,10 +546,10 @@
lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
by simp
-lemma Eps_split: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
+lemma Eps_case_prod: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
by (simp add: split_def)
-lemma Eps_split_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
+lemma Eps_case_prod_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
by blast
--- a/src/HOL/Hoare/hoare_syntax.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Hoare/hoare_syntax.ML Tue Oct 13 09:21:15 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 uncurry} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
+ Syntax.const @{const_syntax case_prod} $ 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 uncurry}, _) $ Abs (v, _, body)) =
+ (Const (@{const_syntax case_prod}, _) $ 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 uncurry}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+fun abs2list (Const (@{const_syntax case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
| abs2list (Abs (x, T, _)) = [Free (x, T)]
| abs2list _ = [];
-fun mk_ts (Const (@{const_syntax uncurry}, _) $ Abs (_, _, t)) = mk_ts t
+fun mk_ts (Const (@{const_syntax case_prod}, _) $ 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 uncurry},_) $ Abs (x, _, t)) =
+fun mk_vts (Const (@{const_syntax case_prod},_) $ 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 uncurry}, _) $ Abs _) = true
+fun is_f (Const (@{const_syntax case_prod}, _) $ Abs _) = true
| is_f (Abs _) = true
| is_f _ = false;
--- a/src/HOL/Hoare/hoare_tac.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Tue Oct 13 09:21:15 2015 +0200
@@ -26,7 +26,7 @@
local
(** maps (%x1 ... xn. t) to [x1,...,xn] **)
-fun abs2list (Const (@{const_name uncurry}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+fun abs2list (Const (@{const_name case_prod}, _) $ 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 uncurry},
+ Const (@{const_name case_prod},
(T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
absfree (x, T) z
end;
--- a/src/HOL/Induct/Com.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Induct/Com.thy Tue Oct 13 09:21:15 2015 +0200
@@ -139,7 +139,7 @@
text\<open>Make the induction rule look nicer -- though @{text eta_contract} makes the new
version look worse than it is...\<close>
-lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
+lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (case_prod (%v. case_prod (case_prod P v)))"
by auto
text\<open>New induction rule. Note the form of the VALOF induction hypothesis\<close>
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Tue Oct 13 09:21:15 2015 +0200
@@ -193,7 +193,7 @@
constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
lemma [code]:
- "Ratreal r = split Realfract (quotient_of r)"
+ "Ratreal r = case_prod Realfract (quotient_of r)"
by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
lemma [code, code del]:
--- a/src/HOL/Library/Countable_Set_Type.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy Tue Oct 13 09:21:15 2015 +0200
@@ -564,7 +564,7 @@
BNF_Def.Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R")
proof
assume ?L
- def R' \<equiv> "the_inv rcset (Collect (split R) \<inter> (rcset a \<times> rcset b))"
+ def R' \<equiv> "the_inv rcset (Collect (case_prod R) \<inter> (rcset a \<times> rcset b))"
(is "the_inv rcset ?L'")
have L: "countable ?L'" by auto
hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset)
@@ -607,8 +607,8 @@
next
fix R
show "rel_cset R =
- (BNF_Def.Grp {x. rcset x \<subseteq> Collect (split R)} (cimage fst))\<inverse>\<inverse> OO
- BNF_Def.Grp {x. rcset x \<subseteq> Collect (split R)} (cimage snd)"
+ (BNF_Def.Grp {x. rcset x \<subseteq> Collect (case_prod R)} (cimage fst))\<inverse>\<inverse> OO
+ BNF_Def.Grp {x. rcset x \<subseteq> Collect (case_prod R)} (cimage snd)"
unfolding rel_cset_alt_def[abs_def] rel_cset_aux by simp
qed(simp add: bot_cset.rep_eq)
--- a/src/HOL/Library/FSet.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/FSet.thy Tue Oct 13 09:21:15 2015 +0200
@@ -939,7 +939,7 @@
BNF_Def.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
proof
assume ?L
- def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
+ def R' \<equiv> "the_inv fset (Collect (case_prod R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+
hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
show ?R unfolding Grp_def relcompp.simps conversep.simps
--- a/src/HOL/Library/Groups_Big_Fun.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Tue Oct 13 09:21:15 2015 +0200
@@ -183,7 +183,7 @@
have bij: "bij (\<lambda>(a, b, c). ((a, b), c))"
by (auto intro!: bijI injI simp add: image_def)
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"
- by auto (insert subset, auto)
+ by auto (insert subset, blast)
with fin have "G (\<lambda>p. G (g (fst p) (snd p))) = G (\<lambda>(p, c). g (fst p) (snd p) c)"
by (rule cartesian_product)
then have "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>((a, b), c). g a b c)"
--- a/src/HOL/Library/Multiset.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Oct 13 09:21:15 2015 +0200
@@ -2085,9 +2085,9 @@
lemma [code]:
"mset xs #\<union> mset ys =
- mset (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
+ mset (case_prod append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
proof -
- have "\<And>zs. mset (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
+ have "\<And>zs. mset (case_prod append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
(mset xs #\<union> mset ys) + mset zs"
by (induct xs arbitrary: ys) (simp_all add: multiset_eq_iff)
then show ?thesis by simp
--- a/src/HOL/Library/Multiset_Order.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Tue Oct 13 09:21:15 2015 +0200
@@ -230,7 +230,7 @@
interpretation multiset_wellorder: wellorder
"le_multiset :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
"less_multiset :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
- by unfold_locales (blast intro: wf_less_multiset[unfolded wf_def, rule_format])
+ by unfold_locales (blast intro: wf_less_multiset [unfolded wf_def, simplified, rule_format])
lemma le_multiset_total:
fixes M N :: "('a :: linorder) multiset"
--- a/src/HOL/Library/Permutations.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/Permutations.thy Tue Oct 13 09:21:15 2015 +0200
@@ -196,7 +196,7 @@
by (auto intro: card_ge_0_finite)
then have pF'f: "finite ?pF'"
using H0 \<open>finite F\<close>
- apply (simp only: Collect_split Collect_mem_eq)
+ apply (simp only: Collect_case_prod Collect_mem_eq)
apply (rule finite_cartesian_product)
apply simp_all
done
@@ -246,7 +246,7 @@
from pFs H0 have xFc: "card ?xF = fact n"
unfolding xfgpF' card_image[OF ginj]
using \<open>finite F\<close> \<open>finite ?pF\<close>
- apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
+ apply (simp only: Collect_case_prod Collect_mem_eq card_cartesian_product)
apply simp
done
from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF"
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Oct 13 09:21:15 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 uncurry}]\<close>
+setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}]\<close>
section \<open>Filters\<close>
--- a/src/HOL/Library/Quotient_Product.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/Quotient_Product.thy Tue Oct 13 09:21:15 2015 +0200
@@ -76,14 +76,14 @@
shows "(map_prod Rep1 Rep2 ---> Abs2) snd = snd"
by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2])
-lemma split_rsp [quot_respect]:
- shows "((R1 ===> R2 ===> (op =)) ===> (rel_prod R1 R2) ===> (op =)) split split"
+lemma case_prod_rsp [quot_respect]:
+ shows "((R1 ===> R2 ===> (op =)) ===> (rel_prod R1 R2) ===> (op =)) case_prod case_prod"
by (rule case_prod_transfer)
lemma split_prs [quot_preserve]:
assumes q1: "Quotient3 R1 Abs1 Rep1"
and q2: "Quotient3 R2 Abs2 Rep2"
- shows "(((Abs1 ---> Abs2 ---> id) ---> map_prod Rep1 Rep2 ---> id) split) = split"
+ shows "(((Abs1 ---> Abs2 ---> id) ---> map_prod Rep1 Rep2 ---> id) case_prod) = case_prod"
by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
lemma [quot_respect]:
@@ -103,6 +103,6 @@
(l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))"
by simp
-declare Pair_eq[quot_preserve]
+declare prod.inject[quot_preserve]
end
--- a/src/HOL/Library/Stream.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/Stream.thy Tue Oct 13 09:21:15 2015 +0200
@@ -581,7 +581,7 @@
by (subst smap2.ctr) simp
lemma smap2_szip:
- "smap2 f s1 s2 = smap (split f) (szip s1 s2)"
+ "smap2 f s1 s2 = smap (case_prod f) (szip s1 s2)"
by (coinduction arbitrary: s1 s2) auto
lemma smap_smap2[simp]:
@@ -597,7 +597,7 @@
by (induct n arbitrary: s1 s2) auto
lemma stake_smap2[simp]:
- "stake n (smap2 f s1 s2) = map (split f) (zip (stake n s1) (stake n s2))"
+ "stake n (smap2 f s1 s2) = map (case_prod f) (zip (stake n s1) (stake n s2))"
by (induct n arbitrary: s1 s2) auto
lemma sdrop_smap2[simp]:
--- a/src/HOL/Library/While_Combinator.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/While_Combinator.thy Tue Oct 13 09:21:15 2015 +0200
@@ -349,7 +349,7 @@
by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
{ assume "ws = []"
hence ?thesis using I
- by (auto simp del:Image_Collect_split dest: Image_closed_trancl)
+ by (auto simp del:Image_Collect_case_prod dest: Image_closed_trancl)
} moreover
{ assume "ws \<noteq> []"
hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
--- a/src/HOL/Library/old_recdef.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML Tue Oct 13 09:21:15 2015 +0200
@@ -551,7 +551,7 @@
local
fun mk_uncurry (xt, yt, zt) =
- Const(@{const_name uncurry}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
+ Const(@{const_name case_prod}, (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 uncurry} then t
+local fun ucheck t = (if #Name (dest_const t) = @{const_name case_prod} then t
else raise Match)
in
fun dest_pabs used tm =
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Tue Oct 13 09:21:15 2015 +0200
@@ -48,7 +48,7 @@
lemma split_compose:
- "(split f) \<circ> (\<lambda> (a,b). ((fa a), (fb b))) = (\<lambda> (a,b). (f (fa a) (fb b)))"
+ "(case_prod f) \<circ> (\<lambda> (a,b). ((fa a), (fb b))) = (\<lambda> (a,b). (f (fa a) (fb b)))"
by (simp add: split_def o_def)
lemma split_iter:
--- a/src/HOL/MicroJava/DFA/Listn.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Listn.thy Tue Oct 13 09:21:15 2015 +0200
@@ -26,7 +26,7 @@
where "x <[r] y == x <_(le r) y"
definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
-"map2 f == (%xs ys. map (split f) (zip xs ys))"
+"map2 f == (%xs ys. map (case_prod f) (zip xs ys))"
abbreviation
plussublist_syntax :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
--- a/src/HOL/MicroJava/J/Example.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Tue Oct 13 09:21:15 2015 +0200
@@ -434,7 +434,7 @@
apply (simp (no_asm))
apply (rule e) -- "XcptE"
apply (simp (no_asm))
-apply (rule surjective_pairing [symmetric, THEN[2]trans], subst Pair_eq, force)
+apply (rule surjective_pairing [symmetric, THEN[2]trans], subst prod.inject, force)
apply (simp (no_asm))
apply (simp (no_asm))
apply (rule e) -- "XcptE"
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Tue Oct 13 09:21:15 2015 +0200
@@ -104,7 +104,7 @@
lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;
list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;
length pTs' = length pns; distinct pns;
- Ball (set lvars) (split (\<lambda>vn. is_type G))
+ Ball (set lvars) (case_prod (\<lambda>vn. is_type G))
|] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')"
apply (unfold wf_mhead_def)
apply( clarsimp)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Oct 13 09:21:15 2015 +0200
@@ -1593,7 +1593,7 @@
obtain a b where ab: "snd x = cbox a b"
using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
- by (metis pair_collapse \<open>x\<in>p\<close> \<open>snd x = snd y\<close> \<open>x \<noteq> y\<close>)+
+ by (metis prod.collapse \<open>x\<in>p\<close> \<open>snd x = snd y\<close> \<open>x \<noteq> y\<close>)+
with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
by (intro assm(5)[of "fst x" _ "fst y"]) auto
then have "content (cbox a b) = 0"
@@ -3211,7 +3211,7 @@
unfolding p(8)[symmetric] by auto
fix x l
assume xl: "(x, l) \<in> ?M1"
- then guess x' l' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note xl'=this
+ then guess x' l' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note xl'=this
show "x \<in> l" "l \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<le> c}"
unfolding xl'
using p(4-6)[OF xl'(3)] using xl'(4)
@@ -3223,7 +3223,7 @@
fix y r
let ?goal = "interior l \<inter> interior r = {}"
assume yr: "(y, r) \<in> ?M1"
- then guess y' r' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note yr'=this
+ then guess y' r' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note yr'=this
assume as: "(x, l) \<noteq> (y, r)"
show "interior l \<inter> interior r = {}"
proof (cases "l' = r' \<longrightarrow> x' = y'")
@@ -3250,7 +3250,7 @@
unfolding p(8)[symmetric] by auto
fix x l
assume xl: "(x, l) \<in> ?M2"
- then guess x' l' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note xl'=this
+ then guess x' l' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note xl'=this
show "x \<in> l" "l \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
unfolding xl'
using p(4-6)[OF xl'(3)] xl'(4) xk_ge_c[OF xl'(3-4)]
@@ -3262,7 +3262,7 @@
fix y r
let ?goal = "interior l \<inter> interior r = {}"
assume yr: "(y, r) \<in> ?M2"
- then guess y' r' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note yr'=this
+ then guess y' r' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note yr'=this
assume as: "(x, l) \<noteq> (y, r)"
show "interior l \<inter> interior r = {}"
proof (cases "l' = r' \<longrightarrow> x' = y'")
@@ -10793,7 +10793,7 @@
using p'(1)
apply auto
done
- 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))"
+ 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))"
unfolding split_def ..
also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
unfolding *
@@ -10898,7 +10898,7 @@
apply (subst setsum.reindex_nontrivial)
apply fact
unfolding split_paired_all
- unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff Pair_eq
+ unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff prod.inject
apply (elim conjE)
proof -
fix x1 l1 k1 x2 l2 k2
@@ -11116,9 +11116,8 @@
by auto
from henstock_lemma [OF f(1) \<open>e/2>0\<close>] obtain d2 where
d2: "gauge d2" "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d2 fine p \<longrightarrow>
- (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
- by blast
- obtain p where
+ (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" .
+ obtain p where
p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
by (rule fine_division_exists [OF gauge_inter [OF d1(1) d2(1)], of a b])
(auto simp add: fine_inter)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Oct 13 09:21:15 2015 +0200
@@ -6294,7 +6294,7 @@
proof -
from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
unfolding bounded_def by auto
- have "bdd_above (split dist ` (s\<times>s))"
+ have "bdd_above (case_prod dist ` (s\<times>s))"
proof (intro bdd_aboveI, safe)
fix a b
assume "a \<in> s" "b \<in> s"
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Oct 13 09:21:15 2015 +0200
@@ -16,23 +16,23 @@
subsection {* Curry in a Hurry *}
-lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
+lemma "(\<lambda>f x y. (curry o case_prod) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
nitpick [card = 1-12, expect = none]
by auto
-lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
+lemma "(\<lambda>f p. (case_prod o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
nitpick [card = 1-12, expect = none]
by auto
-lemma "split (curry f) = f"
+lemma "case_prod (curry f) = f"
nitpick [card = 1-12, expect = none]
by auto
-lemma "curry (split f) = f"
+lemma "curry (case_prod f) = f"
nitpick [card = 1-12, expect = none]
by auto
-lemma "split (\<lambda>x y. f (x, y)) = f"
+lemma "case_prod (\<lambda>x y. f (x, y)) = f"
nitpick [card = 1-12, expect = none]
by auto
@@ -139,7 +139,7 @@
nitpick [card = 2, expect = none]
by auto
-lemma "f = split"
+lemma "f = case_prod"
nitpick [card = 2, expect = genuine]
oops
--- a/src/HOL/Nominal/nominal_induct.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Tue Oct 13 09:21:15 2015 +0200
@@ -18,7 +18,7 @@
fun tuple ts = HOLogic.unit |> fold (fn t => fn u => HOLogic.mk_prod (u, t)) ts;
fun tuple_fun Ts (xi, T) =
- Library.funpow (length Ts) HOLogic.mk_split
+ Library.funpow (length Ts) HOLogic.mk_case_prod
(Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T));
fun split_all_tuples ctxt =
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Tue Oct 13 09:21:15 2015 +0200
@@ -324,7 +324,7 @@
apply (case_tac "r' mod r = 0")
prefer 2
apply (frule_tac a = "r'" in pos_mod_sign, auto)
- apply (metis Pair_eq xzgcda.simps order_refl)
+ apply (metis prod.inject xzgcda.simps order_refl)
done
lemma xzgcd_correct:
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Tue Oct 13 09:21:15 2015 +0200
@@ -338,7 +338,7 @@
"jad = apsnd transpose o length_permutate o map sparsify"
definition
- "jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
+ "jad_mv v = inflate o case_prod zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
lemma "matrix (M::int list list) rs cs \<Longrightarrow> False"
quickcheck[tester = smart_exhaustive, size = 6]
--- a/src/HOL/Probability/Binary_Product_Measure.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Oct 13 09:21:15 2015 +0200
@@ -62,7 +62,7 @@
by (intro measurable_measure_of) (auto dest: sets.sets_into_space)
lemma measurable_split_replace[measurable (raw)]:
- "(\<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"
+ "(\<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"
unfolding split_beta' .
lemma measurable_Pair[measurable (raw)]:
@@ -88,7 +88,7 @@
measurable_def)
lemma measurable_Pair_compose_split[measurable_dest]:
- assumes f: "split f \<in> measurable (M1 \<Otimes>\<^sub>M M2) N"
+ assumes f: "case_prod f \<in> measurable (M1 \<Otimes>\<^sub>M M2) N"
assumes g: "g \<in> measurable M M1" and h: "h \<in> measurable M M2"
shows "(\<lambda>x. f (g x) (h x)) \<in> measurable M N"
using measurable_compose[OF measurable_Pair f, OF g h] by simp
@@ -571,8 +571,8 @@
unfolding nn_integral_max_0 by auto
lemma (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]:
- "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"
- using borel_measurable_nn_integral_fst'[of "\<lambda>x. max 0 (split f x)" N]
+ "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"
+ using borel_measurable_nn_integral_fst'[of "\<lambda>x. max 0 (case_prod f x)" N]
by (simp add: nn_integral_max_0)
lemma (in pair_sigma_finite) nn_integral_snd:
@@ -595,7 +595,7 @@
unfolding nn_integral_snd[OF assms] M2.nn_integral_fst[OF assms] ..
lemma (in pair_sigma_finite) Fubini':
- assumes f: "split f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
+ assumes f: "case_prod f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
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)"
using Fubini[OF f] by simp
--- a/src/HOL/Probability/Bochner_Integration.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy Tue Oct 13 09:21:15 2015 +0200
@@ -2453,7 +2453,7 @@
lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
- assumes [measurable]: "split f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
+ assumes [measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
shows "Measurable.pred N (\<lambda>x. integrable M (f x))"
proof -
have [simp]: "\<And>x. x \<in> space N \<Longrightarrow> integrable M (f x) \<longleftrightarrow> (\<integral>\<^sup>+y. norm (f x y) \<partial>M) < \<infinity>"
@@ -2472,7 +2472,7 @@
lemma (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
- assumes f[measurable]: "split f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
+ assumes f[measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
shows "(\<lambda>x. \<integral>y. f x y \<partial>M) \<in> borel_measurable N"
proof -
from borel_measurable_implies_sequence_metric[OF f, of 0] guess s ..
@@ -2738,7 +2738,7 @@
lemma (in pair_sigma_finite)
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
- assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
+ assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
shows AE_integrable_fst: "AE x in M1. integrable M2 (\<lambda>y. f x y)" (is "?AE")
and integrable_fst: "integrable M1 (\<lambda>x. \<integral>y. f x y \<partial>M2)" (is "?INT")
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")
@@ -2746,10 +2746,10 @@
lemma (in pair_sigma_finite)
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
- assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
+ assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
shows AE_integrable_snd: "AE y in M2. integrable M1 (\<lambda>x. f x y)" (is "?AE")
and integrable_snd: "integrable M2 (\<lambda>y. \<integral>x. f x y \<partial>M1)" (is "?INT")
- 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")
+ 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")
proof -
interpret Q: pair_sigma_finite M2 M1 ..
have Q_int: "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x, y). f y x)"
@@ -2757,12 +2757,12 @@
show ?AE using Q.AE_integrable_fst'[OF Q_int] by simp
show ?INT using Q.integrable_fst'[OF Q_int] by simp
show ?EQ using Q.integral_fst'[OF Q_int]
- using integral_product_swap[of "split f"] by simp
+ using integral_product_swap[of "case_prod f"] by simp
qed
lemma (in pair_sigma_finite) Fubini_integral:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: {banach, second_countable_topology}"
- assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
+ assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
shows "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f x y \<partial>M2) \<partial>M1)"
unfolding integral_snd[OF assms] integral_fst[OF assms] ..
--- a/src/HOL/Probability/Borel_Space.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Tue Oct 13 09:21:15 2015 +0200
@@ -632,7 +632,7 @@
finally show "a < x" .
qed
show "?set \<in> ?SIGMA" unfolding *
- by (auto del: Diff intro!: Diff i)
+ by (auto intro!: Diff sigma_sets_Inter i)
qed
lemma borel_eq_halfspace_less:
--- a/src/HOL/Probability/Caratheodory.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Tue Oct 13 09:21:15 2015 +0200
@@ -417,7 +417,7 @@
and Ble: "\<And>n. (\<Sum>i. f (B n i)) \<le> ?O (A n) + e * (1/2)^(Suc n)"
by auto blast
- def C \<equiv> "split B o prod_decode"
+ def C \<equiv> "case_prod B o prod_decode"
from B have B_in_M: "\<And>i j. B i j \<in> M"
by (rule range_subsetD)
then have C: "range C \<subseteq> M"
@@ -800,24 +800,24 @@
by blast
qed
from choice[OF this] guess f .. note f = this
- then have UN_f_eq: "(\<Union>i. split f (prod_decode i)) = (\<Union>i. A i)"
+ then have UN_f_eq: "(\<Union>i. case_prod f (prod_decode i)) = (\<Union>i. A i)"
unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff)
- have d: "disjoint_family (\<lambda>i. split f (prod_decode i))"
+ have d: "disjoint_family (\<lambda>i. case_prod f (prod_decode i))"
unfolding disjoint_family_on_def
proof (intro ballI impI)
fix m n :: nat assume "m \<noteq> n"
then have neq: "prod_decode m \<noteq> prod_decode n"
using inj_prod_decode[of UNIV] by (auto simp: inj_on_def)
- show "split f (prod_decode m) \<inter> split f (prod_decode n) = {}"
+ show "case_prod f (prod_decode m) \<inter> case_prod f (prod_decode n) = {}"
proof cases
assume "fst (prod_decode m) = fst (prod_decode n)"
then show ?thesis
using neq f by (fastforce simp: disjoint_family_on_def)
next
assume neq: "fst (prod_decode m) \<noteq> fst (prod_decode n)"
- have "split f (prod_decode m) \<subseteq> A (fst (prod_decode m))"
- "split f (prod_decode n) \<subseteq> A (fst (prod_decode n))"
+ have "case_prod f (prod_decode m) \<subseteq> A (fst (prod_decode m))"
+ "case_prod f (prod_decode n) \<subseteq> A (fst (prod_decode n))"
using f[THEN spec, of "fst (prod_decode m)"]
using f[THEN spec, of "fst (prod_decode n)"]
by (auto simp: set_eq_iff)
@@ -825,12 +825,12 @@
by (fastforce simp: disjoint_family_on_def subset_eq set_eq_iff)
qed
qed
- from f have "(\<Sum>n. \<mu>_r (A n)) = (\<Sum>n. \<mu>_r (split f (prod_decode n)))"
+ from f have "(\<Sum>n. \<mu>_r (A n)) = (\<Sum>n. \<mu>_r (case_prod f (prod_decode n)))"
by (intro suminf_ereal_2dimen[symmetric] positiveD2[OF pos] generated_ringI_Basic)
(auto split: prod.split)
- also have "\<dots> = (\<Sum>n. \<mu> (split f (prod_decode n)))"
+ also have "\<dots> = (\<Sum>n. \<mu> (case_prod f (prod_decode n)))"
using f V(2) by (auto intro!: arg_cong[where f=suminf] split: prod.split)
- also have "\<dots> = \<mu> (\<Union>i. split f (prod_decode i))"
+ also have "\<dots> = \<mu> (\<Union>i. case_prod f (prod_decode i))"
using f `c \<in> C'` C'
by (intro ca[unfolded countably_additive_def, rule_format])
(auto split: prod.split simp: UN_f_eq d UN_eq)
--- a/src/HOL/Probability/Finite_Product_Measure.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Oct 13 09:21:15 2015 +0200
@@ -12,7 +12,7 @@
by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
(force intro: exI[of _ "restrict f I" for f])
-lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
+lemma case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
by auto
subsubsection {* More about Function restricted by @{const extensional} *}
@@ -1110,7 +1110,7 @@
qed (simp add: space_PiM)
lemma (in product_sigma_finite) product_nn_integral_pair:
- assumes [measurable]: "split f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
+ assumes [measurable]: "case_prod f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
assumes xy: "x \<noteq> y"
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))"
proof-
--- a/src/HOL/Probability/Giry_Monad.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy Tue Oct 13 09:21:15 2015 +0200
@@ -559,12 +559,12 @@
by (auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space)
lemma measurable_distr2:
- assumes f[measurable]: "split f \<in> measurable (L \<Otimes>\<^sub>M M) N"
+ assumes f[measurable]: "case_prod f \<in> measurable (L \<Otimes>\<^sub>M M) N"
assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)"
shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)"
proof -
have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)
- \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (split f)) \<in> measurable L (subprob_algebra N)"
+ \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (case_prod f)) \<in> measurable L (subprob_algebra N)"
proof (rule measurable_cong)
fix x assume x: "x \<in> space L"
have gx: "g x \<in> space (subprob_algebra M)"
@@ -580,7 +580,7 @@
using gx by (simp add: space_subprob_algebra)
have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)"
by (simp add: space_pair_measure)
- show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (split f)" (is "?l = ?r")
+ show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (case_prod f)" (is "?l = ?r")
proof (rule measure_eqI)
show "sets ?l = sets ?r"
by simp
@@ -1150,7 +1150,7 @@
lemma measurable_bind':
assumes M1: "f \<in> measurable M (subprob_algebra N)" and
- M2: "split g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
+ M2: "case_prod g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
proof (subst measurable_cong)
fix x assume x_in_M: "x \<in> space M"
@@ -1445,7 +1445,7 @@
lemma double_bind_assoc:
assumes Mg: "g \<in> measurable N (subprob_algebra N')"
assumes Mf: "f \<in> measurable M (subprob_algebra M')"
- assumes Mh: "split h \<in> measurable (M \<Otimes>\<^sub>M M') N"
+ assumes Mh: "case_prod h \<in> measurable (M \<Otimes>\<^sub>M M') N"
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"
proof-
have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g =
--- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Oct 13 09:21:15 2015 +0200
@@ -163,7 +163,7 @@
show ?thesis
by (intro measurable_compose_countable'[where f="\<lambda>a b. f (fst b, a)" and g=snd and I=A,
- unfolded pair_collapse] assms)
+ unfolded prod.collapse] assms)
measurable
qed
@@ -177,7 +177,7 @@
show ?thesis
by (intro measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A,
- unfolded pair_collapse] assms)
+ unfolded prod.collapse] assms)
measurable
qed
--- a/src/HOL/Probability/Probability_Measure.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Tue Oct 13 09:21:15 2015 +0200
@@ -288,7 +288,7 @@
in
go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t
end
- | go pattern elem (Const (@{const_syntax uncurry}, _) $ t) =
+ | go pattern elem (Const (@{const_syntax case_prod}, _) $ t) =
go
((Syntax.const @{syntax_const "_pattern"}, 2) :: pattern)
(Syntax.const @{const_syntax Pair} :: elem)
--- a/src/HOL/Probability/ex/Measure_Not_CCC.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy Tue Oct 13 09:21:15 2015 +0200
@@ -116,7 +116,7 @@
context
fixes EXP :: "(real \<Rightarrow> bool) measure"
- assumes eq: "\<And>P. split P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP"
+ assumes eq: "\<And>P. case_prod P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP"
begin
lemma space_EXP: "space EXP = measurable COCOUNT BOOL"
@@ -164,7 +164,7 @@
end
-corollary "\<not> (\<exists>EXP. \<forall>P. split P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP)"
+corollary "\<not> (\<exists>EXP. \<forall>P. case_prod P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP)"
using ce by blast
end
--- a/src/HOL/Probability/measurable.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/measurable.ML Tue Oct 13 09:21:15 2015 +0200
@@ -255,7 +255,7 @@
(map (Option.map (Thm.ctyp_of ctxt)) Ts)
(map (Option.map (Thm.cterm_of ctxt)) ts)
@{thm measurable_compose_countable}
- in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end
+ in r_tac "case_prod countable" (cnt_prefixes ctxt f |> map inst) i end
handle TERM _ => no_tac) 1)
val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
--- a/src/HOL/Product_Type.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Product_Type.thy Tue Oct 13 09:21:15 2015 +0200
@@ -238,7 +238,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 uncurry for Pair fst snd
+free_constructors case_prod 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"
@@ -266,8 +266,7 @@
setup \<open>Sign.mandatory_path "prod"\<close>
-declare
- old.prod.inject[iff del]
+declare old.prod.inject [iff del]
lemmas induct = old.prod.induct
lemmas inducts = old.prod.inducts
@@ -278,6 +277,16 @@
declare prod.case [nitpick_simp del]
declare prod.case_cong_weak [cong del]
+declare prod.case_eq_if [mono]
+declare prod.split [no_atp]
+declare prod.split_asm [no_atp]
+
+text \<open>
+ @{thm [source] prod.split} could be declared as @{text "[split]"}
+ done after the Splitter has been speeded up significantly;
+ precompute the constants involved and don't do anything unless the
+ current goal contains one of those constants.
+\<close>
subsubsection \<open>Tuple syntax\<close>
@@ -302,22 +311,22 @@
"_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 uncurry (\<lambda>x (y, zs). b)"
- "\<lambda>(x, y). b" \<rightleftharpoons> "CONST uncurry (\<lambda>x y. b)"
+ "\<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)"
"_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},
not @{text pttrn}.\<close>
-text \<open>print @{term "uncurry f"} as @{term "\<lambda>(x, y). f x y"} and
- @{term "uncurry (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close>
+text \<open>print @{term "case_prod f"} as @{term "\<lambda>(x, y). f x y"} and
+ @{term "case_prod (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close>
typed_print_translation \<open>
let
- fun uncurry_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
- | uncurry_guess_names_tr' T [Abs (x, xT, t)] =
+ fun case_prod_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
+ | case_prod_guess_names_tr' T [Abs (x, xT, t)] =
(case (head_of t) of
- Const (@{const_syntax uncurry}, _) => raise Match
+ Const (@{const_syntax case_prod}, _) => raise Match
| _ =>
let
val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
@@ -327,9 +336,9 @@
Syntax.const @{syntax_const "_abs"} $
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
end)
- | uncurry_guess_names_tr' T [t] =
+ | case_prod_guess_names_tr' T [t] =
(case head_of t of
- Const (@{const_syntax uncurry}, _) => raise Match
+ Const (@{const_syntax case_prod}, _) => raise Match
| _ =>
let
val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
@@ -340,8 +349,8 @@
Syntax.const @{syntax_const "_abs"} $
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
end)
- | uncurry_guess_names_tr' _ _ = raise Match;
- in [(@{const_syntax uncurry}, K uncurry_guess_names_tr')] end
+ | case_prod_guess_names_tr' _ _ = raise Match;
+ in [(@{const_syntax case_prod}, K case_prod_guess_names_tr')] end
\<close>
@@ -362,32 +371,33 @@
(Haskell) -
| constant "HOL.equal :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" \<rightharpoonup>
(Haskell) infix 4 "=="
+| constant fst \<rightharpoonup> (Haskell) "fst"
+| constant snd \<rightharpoonup> (Haskell) "snd"
subsubsection \<open>Fundamental operations and properties\<close>
lemma Pair_inject:
assumes "(a, b) = (a', b')"
- and "a = a' ==> b = b' ==> R"
+ and "a = a' \<Longrightarrow> b = b' \<Longrightarrow> R"
shows R
using assms by simp
lemma surj_pair [simp]: "EX x y. p = (x, y)"
by (cases p) simp
-code_printing
- constant fst \<rightharpoonup> (Haskell) "fst"
-| constant snd \<rightharpoonup> (Haskell) "snd"
-
-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"
by simp
lemma snd_eqD: "snd (x, y) = a ==> y = a"
by simp
+lemma case_prod_unfold [nitpick_unfold]: "case_prod = (\<lambda>c p. c (fst p) (snd p))"
+ by (simp add: fun_eq_iff split: prod.split)
+
+lemma case_prod_conv [simp, code]: "(case (a, b) of (c, d) \<Rightarrow> f c d) = f a b"
+ by (fact prod.case)
+
lemmas surjective_pairing = prod.collapse [symmetric]
lemma prod_eq_iff: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
@@ -396,36 +406,27 @@
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 (a, b) of (c, d) \<Rightarrow> f c d) = f a b"
- by (fact prod.case)
+lemma case_prodI: "f a b \<Longrightarrow> case (a, b) of (c, d) \<Rightarrow> f c d"
+ by (rule prod.case [THEN iffD2])
-lemma splitI: "f a b \<Longrightarrow> case (a, b) of (c, d) \<Rightarrow> f c d"
- by (rule split_conv [THEN iffD2])
+lemma case_prodD: "(case (a, b) of (c, d) \<Rightarrow> f c d) \<Longrightarrow> f a b"
+ by (rule prod.case [THEN iffD1])
-lemma splitD: "(case (a, b) of (c, d) \<Rightarrow> f c d) \<Longrightarrow> f a b"
- by (rule split_conv [THEN iffD1])
-
-lemma split_Pair [simp]: "uncurry Pair = id"
+lemma case_prod_Pair [simp]: "case_prod Pair = id"
by (simp add: fun_eq_iff split: prod.split)
-lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
+lemma case_prod_eta: "(\<lambda>(x, y). f (x, y)) = f"
-- \<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 x of (a, b) \<Rightarrow> (f \<circ> g) a b) = f (g (fst x)) (snd x)"
+lemma case_prod_comp: "(case x of (a, b) \<Rightarrow> (f \<circ> g) a b) = f (g (fst x)) (snd x)"
by (cases x) simp
-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 (uncurry P) = (THE xy. P (fst xy) (snd xy))"
+lemma The_case_prod: "The (case_prod P) = (THE xy. P (fst xy) (snd xy))"
by (simp add: case_prod_unfold)
-lemmas split_weak_cong = prod.case_cong_weak
- -- \<open>Prevents simplification of @{term c}: much faster\<close>
-
-lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
- by (simp add: split_eta)
+lemma cond_case_prod_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
+ by (simp add: case_prod_eta)
lemma split_paired_all [no_atp]: "(!!x. PROP P x) == (!!a b. PROP P (a, b))"
proof
@@ -438,9 +439,6 @@
from \<open>PROP P (fst x, snd x)\<close> show "PROP P x" by simp
qed
-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>
The rule @{thm [source] split_paired_all} does not work with the
Simplifier because it also affects premises in congrence rules,
@@ -487,20 +485,20 @@
lemma split_paired_The [no_atp]: "(THE x. P x) = (THE (a, b). P (a, b))"
-- \<open>Can't be added to simpset: loops!\<close>
- by (simp add: split_eta)
+ by (simp add: case_prod_eta)
text \<open>
- Simplification procedure for @{thm [source] cond_split_eta}. Using
- @{thm [source] split_eta} as a rewrite rule is not general enough,
- and using @{thm [source] cond_split_eta} directly would render some
+ Simplification procedure for @{thm [source] cond_case_prod_eta}. Using
+ @{thm [source] case_prod_eta} as a rewrite rule is not general enough,
+ and using @{thm [source] cond_case_prod_eta} directly would render some
existing proofs very inefficient; similarly for @{text
- split_beta}.
+ prod.case_eq_if}.
\<close>
ML \<open>
local
- val cond_split_eta_ss =
- simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms cond_split_eta});
+ val cond_case_prod_eta_ss =
+ simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms cond_case_prod_eta});
fun Pair_pat k 0 (Bound m) = (m = k)
| Pair_pat k i (Const (@{const_name Pair}, _) $ Bound m $ t) =
i > 0 andalso m = k + i andalso Pair_pat k (i - 1) t
@@ -510,11 +508,11 @@
| 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 uncurry}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
+ | split_pat tp i (Const (@{const_name case_prod}, _) $ 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)))
- (K (simp_tac (put_simpset cond_split_eta_ss ctxt) 1)));
+ (K (simp_tac (put_simpset cond_case_prod_eta_ss ctxt) 1)));
fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k + 1) i t
| beta_term_pat k i (t $ u) =
@@ -528,103 +526,90 @@
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 uncurry}, _) $ Abs (_, _, t) $ arg) =
+ fun beta_proc ctxt (s as Const (@{const_name case_prod}, _) $ 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 uncurry}, _) $ Abs (_, _, t)) =
+ fun eta_proc ctxt (s as Const (@{const_name case_prod}, _) $ 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)
| eta_proc _ _ = NONE;
end;
\<close>
-simproc_setup split_beta ("split f z") =
+simproc_setup case_prod_beta ("case_prod f z") =
\<open>fn _ => fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct)\<close>
-simproc_setup split_eta ("split f") =
+simproc_setup case_prod_eta ("case_prod f") =
\<open>fn _ => fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct)\<close>
-lemmas split_beta [mono] = prod.case_eq_if
-
-lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
+lemma case_prod_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
by (auto simp: fun_eq_iff)
-lemmas split_split [no_atp] = prod.split
- -- \<open>For use with @{text split} and the Simplifier.\<close>
-
text \<open>
- @{thm [source] split_split} could be declared as @{text "[split]"}
- done after the Splitter has been speeded up significantly;
- precompute the constants involved and don't do anything unless the
- current goal contains one of those constants.
-\<close>
-
-lemmas split_split_asm [no_atp] = prod.split_asm
-
-text \<open>
- \medskip @{const uncurry} used as a logical connective or set former.
+ \medskip @{const case_prod} 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 p of (a, b) \<Rightarrow> c a b"
- apply (simp only: split_tupled_all)
- apply (simp (no_asm_simp))
- done
+lemma case_prodI2:
+ "\<And>p. (\<And>a b. p = (a, b) \<Longrightarrow> c a b) \<Longrightarrow> case p of (a, b) \<Rightarrow> c a b"
+ by (simp add: split_tupled_all)
-lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> (case p of (a, b) \<Rightarrow> c a b) x"
- apply (simp only: split_tupled_all)
- apply (simp (no_asm_simp))
- done
+lemma case_prodI2':
+ "\<And>p. (\<And>a b. (a, b) = p \<Longrightarrow> c a b x) \<Longrightarrow> (case p of (a, b) \<Rightarrow> c a b) x"
+ by (simp add: split_tupled_all)
-lemma splitE: "(case p of (a, b) \<Rightarrow> c a b) ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
- by (induct p) auto
+lemma case_prodE [elim!]:
+ "(case p of (a, b) \<Rightarrow> c a b) \<Longrightarrow> (\<And>x y. p = (x, y) \<Longrightarrow> c x y \<Longrightarrow> Q) \<Longrightarrow> Q"
+ by (induct p) simp
-lemma splitE': "(case p of (a, b) \<Rightarrow> c a b) z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
- by (induct p) auto
+lemma case_prodE' [elim!]:
+ "(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"
+ by (induct p) simp
-lemma splitE2:
- "[| Q (case z of (a, b) \<Rightarrow> P a b); !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
-proof -
- 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)+
- apply (rule split_beta [THEN subst], rule q)
- done
+lemma case_prodE2:
+ assumes q: "Q (case z of (a, b) \<Rightarrow> P a b)"
+ and r: "\<And>x y. z = (x, y) \<Longrightarrow> Q (P x y) \<Longrightarrow> R"
+ shows R
+proof (rule r)
+ show "z = (fst z, snd z)" by simp
+ then show "Q (P (fst z) (snd z))"
+ using q by (simp add: case_prod_unfold)
qed
-lemma splitD':
+lemma case_prodD':
"(case (a, b) of (c, d) \<Rightarrow> R c d) c \<Longrightarrow> R a b c"
by simp
-lemma mem_splitI:
+lemma mem_case_prodI:
"z \<in> c a b \<Longrightarrow> z \<in> (case (a, b) of (d, e) \<Rightarrow> c d e)"
by simp
-lemma mem_splitI2:
+lemma mem_case_prodI2 [intro!]:
"\<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)"
by (simp only: split_tupled_all) simp
-lemma mem_splitE:
- assumes "z \<in> uncurry c p"
+declare mem_case_prodI [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
+declare case_prodI2' [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
+declare case_prodI2 [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
+declare case_prodI [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
+
+lemma mem_case_prodE [elim!]:
+ assumes "z \<in> case_prod c p"
obtains x y where "p = (x, y)" and "z \<in> c x y"
- using assms by (rule splitE2)
-
-declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
-declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
+ using assms by (rule case_prodE2)
ML \<open>
local (* filtering with exists_p_split is an essential optimization *)
- fun exists_p_split (Const (@{const_name uncurry},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
+ fun exists_p_split (Const (@{const_name case_prod},_) $ _ $ (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;
in
fun split_conv_tac ctxt = SUBGOAL (fn (t, i) =>
if exists_p_split t
- then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_conv}) i
+ then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms case_prod_conv}) i
else no_tac);
end;
\<close>
@@ -636,10 +621,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) = uncurry P"
+lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = case_prod P"
by (rule ext) fast
-lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & uncurry Q ab)"
+lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & case_prod Q ab)"
-- \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
by (rule ext) blast
@@ -649,7 +634,7 @@
*)
lemma split_comp_eq:
fixes f :: "'a => 'b => 'c" and g :: "'d => 'a"
- shows "(%u. f (g (fst u)) (snd u)) = (uncurry (%x. f (g x)))"
+ shows "(%u. f (g (fst u)) (snd u)) = (case_prod (%x. f (g x)))"
by (rule ext) auto
lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
@@ -673,29 +658,9 @@
qed "The_split_eq";
*)
-text \<open>
- Setup of internal @{text split_rule}.
-\<close>
-
-lemmas case_prodI = prod.case [THEN iffD2]
-
-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 |] ==> uncurry c p x"
- by (fact splitI2')
-
-lemma case_prodE: "uncurry c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
- by (fact splitE)
-
-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:
- "uncurry f p = f (fst p) (snd p)"
- by (fact split_beta)
+ "case_prod f p = f (fst p) (snd p)"
+ by (fact prod.case_eq_if)
lemma prod_cases3 [cases type]:
obtains (fields) a b c where "y = (a, b, c)"
@@ -737,20 +702,20 @@
"(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
by (cases x) blast
-definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
- "internal_split == uncurry"
+definition internal_case_prod :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
+ "internal_case_prod == case_prod"
-lemma internal_split_conv: "internal_split c (a, b) = c a b"
- by (simp only: internal_split_def split_conv)
+lemma internal_case_prod_conv: "internal_case_prod c (a, b) = c a b"
+ by (simp only: internal_case_prod_def case_prod_conv)
ML_file "Tools/split_rule.ML"
-hide_const internal_split
+hide_const internal_case_prod
subsubsection \<open>Derived operations\<close>
-definition curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
+definition curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
"curry = (\<lambda>c x y. c (x, y))"
lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
@@ -765,10 +730,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 (uncurry f) = f"
+lemma curry_case_prod [simp]: "curry (case_prod f) = f"
by (simp add: curry_def case_prod_unfold)
-lemma split_curry [simp]: "uncurry (curry f) = f"
+lemma case_prod_curry [simp]: "case_prod (curry f) = f"
by (simp add: curry_def case_prod_unfold)
lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)"
@@ -781,12 +746,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. uncurry g (f x))"
+ "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod 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 = uncurry g (f x)"
+lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = case_prod g (f x)"
by (simp add: scomp_unfold case_prod_unfold)
lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
@@ -1076,25 +1041,25 @@
lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)"
by (blast elim: equalityE)
-lemma SetCompr_Sigma_eq:
+lemma Collect_case_prod_Sigma:
"{(x, y). P x \<and> Q x y} = (SIGMA x:Collect P. Collect (Q x))"
by blast
-lemma Collect_split [simp]:
+lemma Collect_case_prod [simp]:
"{(a, b). P a \<and> Q b} = Collect P \<times> Collect Q "
- by (fact SetCompr_Sigma_eq)
+ by (fact Collect_case_prod_Sigma)
-lemma Collect_splitD:
- "x \<in> Collect (uncurry A) \<Longrightarrow> A (fst x) (snd x)"
+lemma Collect_case_prodD:
+ "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
by auto
-lemma Collect_split_mono:
- "A \<le> B \<Longrightarrow> Collect (uncurry A) \<subseteq> Collect (uncurry B)"
+lemma Collect_case_prod_mono:
+ "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
by auto (auto elim!: le_funE)
lemma Collect_split_mono_strong:
"X = fst ` A \<Longrightarrow> Y = snd ` A \<Longrightarrow> \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b
- \<Longrightarrow> A \<subseteq> Collect (uncurry P) \<Longrightarrow> A \<subseteq> Collect (uncurry Q)"
+ \<Longrightarrow> A \<subseteq> Collect (case_prod P) \<Longrightarrow> A \<subseteq> Collect (case_prod Q)"
by fastforce
lemma UN_Times_distrib:
@@ -1318,7 +1283,7 @@
fn _ => fn ctxt => fn ct =>
(case Thm.term_of ct of
S as Const (@{const_name Collect}, Type (@{type_name fun}, [_, T])) $ t =>
- let val (u, _, ps) = HOLogic.strip_psplits t in
+ let val (u, _, ps) = HOLogic.strip_ptupleabs t in
(case u of
(c as Const (@{const_name Set.member}, _)) $ q $ S' =>
(case try (HOLogic.strip_ptuple ps) q of
@@ -1329,7 +1294,7 @@
then
let val simp =
full_simp_tac (put_simpset HOL_basic_ss ctxt
- addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1
+ addsimps [@{thm split_paired_all}, @{thm case_prod_conv}]) 1
in
SOME (Goal.prove ctxt [] []
(Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
@@ -1350,20 +1315,13 @@
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> uncurry"
-
-lemmas PairE = prod.exhaust
-lemmas Pair_eq = prod.inject
lemmas fst_conv = prod.sel(1)
lemmas snd_conv = prod.sel(2)
-lemmas pair_collapse = prod.collapse
-lemmas split = split_conv
-lemmas Pair_fst_snd_eq = prod_eq_iff
lemmas split_def = case_prod_unfold
+lemmas split_beta' = case_prod_beta'
+lemmas split_beta = prod.case_eq_if
+lemmas split_conv = case_prod_conv
+lemmas split = case_prod_conv
hide_const (open) prod
--- a/src/HOL/Relation.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Relation.thy Tue Oct 13 09:21:15 2015 +0200
@@ -951,10 +951,10 @@
lemma Field_converse [simp]: "Field (r\<inverse>) = Field r"
by (auto simp: Field_def)
-lemma Domain_Collect_split [simp]: "Domain {(x, y). P x y} = {x. EX y. P x y}"
+lemma Domain_Collect_case_prod [simp]: "Domain {(x, y). P x y} = {x. EX y. P x y}"
by auto
-lemma Range_Collect_split [simp]: "Range {(x, y). P x y} = {y. EX x. P x y}"
+lemma Range_Collect_case_prod [simp]: "Range {(x, y). P x y} = {y. EX x. P x y}"
by auto
lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)"
@@ -1058,7 +1058,7 @@
lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"
by blast
-lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}"
+lemma Image_Collect_case_prod [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}"
by auto
lemma Sigma_Image: "(SIGMA x:A. B x) `` X = (\<Union>x\<in>X \<inter> A. B x)"
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Tue Oct 13 09:21:15 2015 +0200
@@ -506,7 +506,7 @@
"p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
"(fst (x, y) = snd (x, y)) = (x = y)"
"(fst p = snd p) = (p = (snd p, fst p))"
- using fst_conv snd_conv pair_collapse
+ using fst_conv snd_conv prod.collapse
by smt+
lemma
@@ -525,7 +525,7 @@
lemma
"fst (hd [(a, b)]) = a"
"snd (hd [(a, b)]) = b"
- using fst_conv snd_conv pair_collapse list.sel(1,3) list.simps
+ using fst_conv snd_conv prod.collapse list.sel(1,3) list.simps
by smt+
@@ -627,7 +627,7 @@
"p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
"(fst (x, y) = snd (x, y)) = (x = y)"
"(fst p = snd p) = (p = (snd p, fst p))"
- using fst_conv snd_conv pair_collapse
+ using fst_conv snd_conv prod.collapse
using [[smt_oracle, z3_extensions]]
by smt+
@@ -648,7 +648,7 @@
lemma
"fst (hd [(a, b)]) = a"
"snd (hd [(a, b)]) = b"
- using fst_conv snd_conv pair_collapse list.sel(1,3)
+ using fst_conv snd_conv prod.collapse list.sel(1,3)
using [[smt_oracle, z3_extensions]]
by smt+
--- a/src/HOL/SMT_Examples/boogie.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/SMT_Examples/boogie.ML Tue Oct 13 09:21:15 2015 +0200
@@ -243,7 +243,7 @@
end
val boogie_rules =
- [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] @
+ [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.collapse}] @
[@{thm fun_upd_same}, @{thm fun_upd_apply}]
fun boogie_tac ctxt axioms =
--- a/src/HOL/Tools/BNF/bnf_def.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Oct 13 09:21:15 2015 +0200
@@ -943,7 +943,7 @@
val CR = mk_bnf_T Ds RTs Calpha;
val setRs =
@{map 3} (fn R => fn T => fn U =>
- HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As Bs;
+ HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_case_prod R) Rs As Bs;
(*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*)
@@ -1301,7 +1301,7 @@
val ran_bnfT = mk_bnf_T ranTs Calpha;
val (revTs, Ts) = `rev (bd_bnfT :: funTs);
val cTs = map (SOME o Thm.ctyp_of lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
- val tinst = fold (fn T => fn t => HOLogic.mk_split (Term.absdummy T t)) (tl revTs)
+ val tinst = fold (fn T => fn t => HOLogic.mk_case_prod (Term.absdummy T t)) (tl revTs)
(Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
map Bound (live - 1 downto 0)) $ Bound live));
val cts = [NONE, SOME (Thm.cterm_of lthy tinst)];
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Tue Oct 13 09:21:15 2015 +0200
@@ -108,10 +108,10 @@
eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
REPEAT_DETERM_N n o
- EVERY' [rtac ctxt @{thm Collect_split_Grp_eqD}, etac ctxt @{thm set_mp}, assume_tac ctxt],
+ EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD}, etac ctxt @{thm set_mp}, assume_tac ctxt],
rtac ctxt CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
- rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_split_Grp_inD},
+ rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_case_prod_Grp_in},
etac ctxt @{thm set_mp}, assume_tac ctxt])
set_maps,
rtac ctxt @{thm predicate2I}, REPEAT_DETERM o eresolve_tac ctxt [@{thm GrpE}, exE, conjE],
@@ -165,8 +165,8 @@
rtac ctxt (hd rel_OO_Grps RS sym RSN (2, ord_le_eq_trans));
in
EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm relcompp_mono}, rtac ctxt @{thm iffD2[OF conversep_mono]},
- rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_split_mono},
- rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_split_mono}] 1
+ rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono},
+ rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono}] 1
end;
fun mk_rel_conversep_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 13 09:21:15 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 uncurry}, _)) $ u) =
+and unfold_splits_lets ((t as Const (@{const_name case_prod}, _)) $ 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.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Oct 13 09:21:15 2015 +0200
@@ -958,7 +958,7 @@
val (fTs1, fTs2) = apsnd tl (chop (i - 1) (map (fn T => T --> FT) bdFTs));
val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2);
in
- HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
+ HOLogic.mk_case_prod (Term.absfree Kl' (Term.absfree lab'
(mk_case_sumN fs $ (lab $ HOLogic.mk_list sum_sbdT []))))
end;
@@ -2280,7 +2280,7 @@
||>> mk_Frees' "z" zip_zTs;
val Iphi_sets =
- map2 (fn phi => fn T => HOLogic.Collect_const T $ HOLogic.mk_split phi) allJphis zip_ranTs;
+ map2 (fn phi => fn T => HOLogic.Collect_const T $ HOLogic.mk_case_prod phi) allJphis zip_ranTs;
val in_phis = map2 (mk_in Iphi_sets) (mk_setss zip_ranTs) zipFTs;
val fstABs = map fst_const passiveABs;
val all_fsts = fstABs @ fstsTsTs';
@@ -2295,7 +2295,7 @@
Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveBs @ Ts') bnf, all_snds)) Dss bnfs;
val Jmap_snds = map2 (fn map => fn T => if m = 0 then HOLogic.id_const T
else Term.list_comb (map, sndABs)) (mk_Jmaps passiveABs passiveBs) Ts;
- val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_split zips)) ks;
+ val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_case_prod zips)) ks;
val zip_setss = mk_Jsetss passiveABs |> transpose;
fun Jrel_coinduct_tac {context = ctxt, prems = CIHs} =
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Oct 13 09:21:15 2015 +0200
@@ -298,7 +298,7 @@
| (_, branches') =>
Term.list_comb (If_const (typof (hd branches')) $ tap (check_no_call bound_Ts) obj,
branches'))
- | (c as Const (@{const_name uncurry}, _), arg :: args) =>
+ | (c as Const (@{const_name case_prod}, _), arg :: args) =>
massage_rec bound_Ts
(unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
| (Const (c, _), args as _ :: _ :: _) =>
@@ -402,12 +402,12 @@
end
| NONE =>
(case t of
- Const (@{const_name uncurry}, _) $ t' =>
+ Const (@{const_name case_prod}, _) $ t' =>
let
val U' = curried_type U;
val T' = curried_type T;
in
- Const (@{const_name uncurry}, U' --> U) $ massage_any_call bound_Ts U' T' t'
+ Const (@{const_name case_prod}, U' --> U) $ massage_any_call bound_Ts U' T' t'
end
| t1 $ t2 =>
(if has_call t2 then
@@ -931,9 +931,9 @@
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 uncurry} then
+ else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
map (rewrite bound_Ts) vs |> chop 1
- |>> HOLogic.mk_split o the_single
+ |>> HOLogic.mk_case_prod o the_single
|> Term.list_comb
else
Term.list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs)
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Tue Oct 13 09:21:15 2015 +0200
@@ -108,7 +108,7 @@
val snd_convol_fun_cong_sym = @{thm snd_convol[unfolded convol_def]} RS fun_cong RS sym;
val sum_case_cong_weak = @{thm sum.case_cong_weak};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
-val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
+val Collect_splitD_set_mp = @{thm Collect_case_prodD[OF set_mp]};
val rev_bspec = Drule.rotate_prems 1 bspec;
val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
val converse_shift = @{thm converse_subset_swap} RS iffD1;
@@ -239,7 +239,7 @@
etac ctxt @{thm image_mono}, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
rtac ctxt @{thm case_prodI}, rtac ctxt refl]
else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
- rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt @{thm Collect_split_in_rel_leI}])
+ rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt @{thm Collect_case_prod_in_rel_leI}])
(1 upto (m + n) ~~ set_map0s)];
fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
@@ -247,7 +247,7 @@
etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt,
dtac ctxt (in_rel RS @{thm iffD1}),
REPEAT_DETERM o eresolve_tac ctxt ([CollectE, conjE, exE] @
- @{thms CollectE Collect_split_in_rel_leE}),
+ @{thms CollectE Collect_case_prod_in_rel_leE}),
rtac ctxt bexI, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
@@ -255,7 +255,7 @@
REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
rtac ctxt trans, rtac ctxt map_cong0,
- REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_splitD}, etac ctxt set_mp, assume_tac ctxt],
+ REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_case_prodD}, etac ctxt set_mp, assume_tac ctxt],
REPEAT_DETERM_N n o rtac ctxt refl,
assume_tac ctxt, rtac ctxt CollectI,
CONJ_WRAP' (fn (i, thm) =>
@@ -772,8 +772,8 @@
CONJ_WRAP' (fn rel_cong => EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
REPEAT_DETERM o etac ctxt allE, rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
REPEAT_DETERM_N m o rtac ctxt refl,
- REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm in_rel_Collect_split_eq[symmetric]},
- etac ctxt mp, etac ctxt CollectE, etac ctxt @{thm splitD}])
+ REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm in_rel_Collect_case_prod_eq[symmetric]},
+ etac ctxt mp, etac ctxt CollectE, etac ctxt @{thm case_prodD}])
rel_congs,
rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE,
CONJ_WRAP' (K (EVERY' [rtac ctxt impI, rtac ctxt @{thm IdD}, etac ctxt set_mp,
@@ -994,7 +994,7 @@
rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt @{thm box_equals[OF _ _ refl]},
rtac ctxt active_set_map0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt @{thm UN_least},
dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
- dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
+ dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
@{thms case_prodE iffD1[OF prod.inject, elim_format]}),
hyp_subst_tac ctxt,
@@ -1008,7 +1008,7 @@
rtac ctxt @{thm box_equals}, rtac ctxt map_comp0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans,
rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, assume_tac ctxt,
- dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
+ dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
@{thms case_prodE iffD1[OF prod.inject, elim_format]}),
hyp_subst_tac ctxt, dtac ctxt (in_Jrel RS iffD1),
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 13 09:21:15 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 uncurry}, (ctr_Ts ---> C) --> fpT --> C),
+ {co_rec = Const (@{const_name case_prod}, (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/BNF/bnf_lfp_tactics.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Oct 13 09:21:15 2015 +0200
@@ -698,7 +698,7 @@
(fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans,
rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least},
dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
- dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
+ dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
@{thms case_prodE iffD1[OF prod.inject, elim_format]}),
hyp_subst_tac ctxt,
@@ -712,7 +712,7 @@
REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply,
dtac ctxt set_rev_mp, assume_tac ctxt,
- dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
+ dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
@{thms case_prodE iffD1[OF prod.inject, elim_format]}),
hyp_subst_tac ctxt,
--- a/src/HOL/Tools/Function/partial_function.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Tue Oct 13 09:21:15 2015 +0200
@@ -146,11 +146,11 @@
(* iterated versions. Nonstandard left-nested tuples arise naturally
from "split o split o split"*)
fun curry_n arity = funpow (arity - 1) mk_curry;
-fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_split;
+fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_case_prod;
val curry_uncurry_ss =
simpset_of (put_simpset HOL_basic_ss @{context}
- addsimps [@{thm Product_Type.curry_split}, @{thm Product_Type.split_curry}])
+ addsimps [@{thm Product_Type.curry_case_prod}, @{thm Product_Type.case_prod_curry}])
val split_conv_ss =
simpset_of (put_simpset HOL_basic_ss @{context}
@@ -177,7 +177,7 @@
THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
|> (fn thm => thm OF [mono_thm, f_def])
|> Conv.fconv_rule (Conv.concl_conv ~1 (* simplify conclusion *)
- (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_split}]))
+ (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}]))
|> singleton (Variable.export ctxt' ctxt)
end
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Oct 13 09:21:15 2015 +0200
@@ -2210,7 +2210,7 @@
fun n_ptuple_paths 0 = []
| n_ptuple_paths 1 = []
| n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1))
-val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths
+val ap_n_split = HOLogic.mk_ptupleabs o n_ptuple_paths
val linear_pred_base_and_step_rhss =
let
@@ -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 uncurry}, curried_T --> uncurried_T)
+ $ (Const (@{const_name case_prod}, 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/code_prolog.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Oct 13 09:21:15 2015 +0200
@@ -956,7 +956,7 @@
(case t_compr of
(Const (@{const_name Collect}, _) $ t) => t
| _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
- val (body, Ts, fp) = HOLogic.strip_psplits split
+ val (body, Ts, fp) = HOLogic.strip_ptupleabs split
val output_names = Name.variant_list (Term.add_free_names body [])
(map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
val output_frees = rev (map2 (curry Free) output_names Ts)
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Oct 13 09:21:15 2015 +0200
@@ -228,7 +228,7 @@
val thy = Proof_Context.theory_of ctxt
val nargs = length (binder_types (fastype_of pred))
fun meta_eq_of th = th RS @{thm eq_reflection}
- val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]
+ val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.inject}]
fun instantiate i n ({context = ctxt2, prems, ...}: Subgoal.focus) =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Oct 13 09:21:15 2015 +0200
@@ -884,9 +884,9 @@
val intro'''' =
Simplifier.full_simplify
(put_simpset HOL_basic_ss ctxt
- addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
+ addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.inject}])
intro'''
- (* splitting conjunctions introduced by Pair_eq*)
+ (* splitting conjunctions introduced by prod.inject*)
val intro''''' = split_conjuncts_in_assms ctxt intro''''
in
intro'''''
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 13 09:21:15 2015 +0200
@@ -610,7 +610,7 @@
| mk_tuple tTs = foldr1 mk_prod tTs
fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t =
absdummy T
- (HOLogic.split_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
+ (HOLogic.case_prod_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
| mk_split_abs T t = absdummy T t
val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
val (inargs, outargs) = split_mode mode args
@@ -1023,7 +1023,7 @@
(* Definition of executable functions and their intro and elim rules *)
-fun strip_split_abs (Const (@{const_name uncurry}, _) $ t) = strip_split_abs t
+fun strip_split_abs (Const (@{const_name case_prod}, _) $ t) = strip_split_abs t
| strip_split_abs (Abs (_, _, t)) = strip_split_abs t
| strip_split_abs t = t
@@ -1086,7 +1086,7 @@
val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
val simprules =
[defthm, @{thm eval_pred},
- @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
+ @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm prod.collapse}]
val unfolddef_tac =
Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simprules) 1
val introthm = Goal.prove ctxt
@@ -1748,7 +1748,7 @@
(case t_compr of
(Const (@{const_name Collect}, _) $ t) => t
| _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
- val (body, Ts, fp) = HOLogic.strip_psplits inner_t;
+ val (body, Ts, fp) = HOLogic.strip_ptupleabs inner_t;
val output_names = Name.variant_list (Term.add_free_names body [])
(map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
val output_frees = map2 (curry Free) output_names (rev Ts)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Tue Oct 13 09:21:15 2015 +0200
@@ -35,7 +35,7 @@
val HOL_basic_ss' =
simpset_of (put_simpset HOL_basic_ss @{context}
- addsimps @{thms simp_thms Pair_eq}
+ addsimps @{thms simp_thms prod.inject}
setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
setSolver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI})))
@@ -62,8 +62,8 @@
(case f of
Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
[@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode,
- @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
- @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
+ @{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv},
+ @{thm snd_conv}, @{thm prod.collapse}, @{thm Product_Type.split_conv}]) 1
| Free _ =>
Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, ...} =>
let
@@ -232,8 +232,8 @@
in
trace_tac ctxt options "before prove_neg_expr:"
THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
- [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
- @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
+ [@{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv},
+ @{thm snd_conv}, @{thm prod.collapse}, @{thm Product_Type.split_conv}]) 1
THEN (if (is_some name) then
trace_tac ctxt options "before applying not introduction rule"
THEN Subgoal.FOCUS_PREMS (fn {prems, ...} =>
@@ -392,8 +392,8 @@
val (in_ts, _) = split_mode mode ts;
val split_simpset =
put_simpset HOL_basic_ss' ctxt
- addsimps [@{thm split_eta}, @{thm split_beta},
- @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
+ addsimps [@{thm case_prod_eta}, @{thm case_prod_beta},
+ @{thm fst_conv}, @{thm snd_conv}, @{thm prod.collapse}]
fun prove_prems2 out_ts [] =
trace_tac ctxt options "before prove_match2 - last call:"
THEN prove_match2 options ctxt out_ts
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Oct 13 09:21:15 2015 +0200
@@ -152,7 +152,7 @@
fun mk_full_equations functerms =
let
fun test_function T = Free ("f", termifyT T --> resultT)
- fun split_const T = HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, resultT)
+ fun case_prod_const T = HOLogic.case_prod_const (T, @{typ "unit => Code_Evaluation.term"}, resultT)
fun mk_call T =
let
val full_exhaustive =
@@ -160,7 +160,7 @@
full_exhaustiveT T)
in
(T, fn t => full_exhaustive $
- (split_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
+ (case_prod_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
end
fun mk_aux_call fTs (k, _) (tyco, Ts) =
let
@@ -168,7 +168,7 @@
val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
in
(T, fn t => nth functerms k $
- (split_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
+ (case_prod_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
end
fun mk_consexpr simpleT (c, xs) =
let
@@ -387,11 +387,11 @@
fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
if Sign.of_sort thy (T, @{sort check_all}) then
Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
- $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
+ $ (HOLogic.case_prod_const (T, @{typ "unit => term"}, resultT)
$ lambda free (lambda term_var t))
else
Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
- $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
+ $ (HOLogic.case_prod_const (T, @{typ "unit => term"}, resultT)
$ lambda free (lambda term_var t)) $ depth
val none_t = Const (@{const_name "None"}, resultT)
val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Tue Oct 13 09:21:15 2015 +0200
@@ -315,11 +315,11 @@
fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
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 uncurry}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
+ fun mk_case_prod T = Sign.mk_const thy
+ (@{const_name case_prod}, [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')));
+ (mk_case_prod T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
fun mk_bindclause (_, _, i, T) = mk_scomp_split T
(Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i);
in
@@ -361,11 +361,11 @@
fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
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 uncurry}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
+ fun mk_case_prod T = Sign.mk_const thy
+ (@{const_name case_prod}, [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')));
+ (mk_case_prod T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
fun mk_bindclause (_, _, i, T) = mk_scomp_split T
(Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i);
in
--- a/src/HOL/Tools/Quotient/quotient_term.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Tue Oct 13 09:21:15 2015 +0200
@@ -634,12 +634,12 @@
end
end
- | (((t1 as Const (@{const_name uncurry}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
- ((t2 as Const (@{const_name uncurry}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
+ | (((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)))) =>
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
- | (((t1 as Const (@{const_name uncurry}, _)) $ Abs (v1, ty, s1)),
- ((t2 as Const (@{const_name uncurry}, _)) $ Abs (v2, _ , s2))) =>
+ | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, s1)),
+ ((t2 as Const (@{const_name case_prod}, _)) $ 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 Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/hologic.ML Tue Oct 13 09:21:15 2015 +0200
@@ -67,8 +67,8 @@
val dest_prod: term -> term * term
val mk_fst: term -> term
val mk_snd: term -> term
- val split_const: typ * typ * typ -> term
- val mk_split: term -> term
+ val case_prod_const: typ * typ * typ -> term
+ val mk_case_prod: term -> term
val flatten_tupleT: typ -> typ list
val tupled_lambda: term -> term -> term
val mk_tupleT: typ list -> typ
@@ -81,8 +81,8 @@
val mk_ptuple: int list list -> typ -> term list -> term
val strip_ptuple: int list list -> term -> term list
val flat_tuple_paths: term -> int list list
- val mk_psplits: int list list -> typ -> typ -> term -> term
- val strip_psplits: term -> term * typ list * int list list
+ val mk_ptupleabs: int list list -> typ -> typ -> term -> term
+ val strip_ptupleabs: term -> term * typ list * int list list
val natT: typ
val zero: term
val is_zero: term -> bool
@@ -348,14 +348,14 @@
Const ("Product_Type.prod.snd", pT --> snd (dest_prodT pT)) $ p
end;
-fun split_const (A, B, C) =
- Const ("Product_Type.prod.uncurry", (A --> B --> C) --> mk_prodT (A, B) --> C);
+fun case_prod_const (A, B, C) =
+ Const ("Product_Type.prod.case_prod", (A --> B --> C) --> mk_prodT (A, B) --> C);
-fun mk_split t =
+fun mk_case_prod t =
(case Term.fastype_of t of
T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
- Const ("Product_Type.prod.uncurry", T --> mk_prodT (A, B) --> C) $ t
- | _ => raise TERM ("mk_split: bad body type", [t]));
+ Const ("Product_Type.prod.case_prod", T --> mk_prodT (A, B) --> C) $ t
+ | _ => raise TERM ("mk_case_prod: bad body type", [t]));
(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
fun flatten_tupleT (Type ("Product_Type.prod", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
@@ -365,7 +365,7 @@
fun tupled_lambda (x as Free _) b = lambda x b
| tupled_lambda (x as Var _) b = lambda x b
| tupled_lambda (Const ("Product_Type.Pair", _) $ u $ v) b =
- mk_split (tupled_lambda u (tupled_lambda v b))
+ mk_case_prod (tupled_lambda u (tupled_lambda v b))
| tupled_lambda (Const ("Product_Type.Unity", _)) b =
Abs ("x", unitT, b)
| tupled_lambda t _ = raise TERM ("tupled_lambda: bad tuple", [t]);
@@ -450,27 +450,27 @@
| factors p _ = []
in factors [] end;
-(*In mk_psplits ps S T u, term u expects separate arguments for the factors of S,
+(*In mk_ptupleabs ps S T u, term u expects separate arguments for the factors of S,
with result type T. The call creates a new term expecting one argument
of type S.*)
-fun mk_psplits ps T T3 u =
+fun mk_ptupleabs ps T T3 u =
let
fun ap ((p, T) :: pTs) =
if member (op =) ps p then (case T of
Type ("Product_Type.prod", [T1, T2]) =>
- split_const (T1, T2, map snd pTs ---> T3) $
+ case_prod_const (T1, T2, map snd pTs ---> T3) $
ap ((1::p, T1) :: (2::p, T2) :: pTs)
- | _ => ptuple_err "mk_psplits")
+ | _ => ptuple_err "mk_ptupleabs")
else Abs ("x", T, ap pTs)
| ap [] =
let val k = length ps
in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
in ap [([], T)] end;
-val strip_psplits =
+val strip_ptupleabs =
let
fun strip [] qs Ts t = (t, rev Ts, qs)
- | strip (p :: ps) qs Ts (Const ("Product_Type.prod.uncurry", _) $ t) =
+ | strip (p :: ps) qs Ts (Const ("Product_Type.prod.case_prod", _) $ 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/inductive_set.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML Tue Oct 13 09:21:15 2015 +0200
@@ -55,7 +55,7 @@
fun mk_collect p T t =
let val U = HOLogic.dest_setT T
in HOLogic.Collect_const U $
- HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
+ HOLogic.mk_ptupleabs (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
end;
fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member},
Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
@@ -66,7 +66,7 @@
| decomp _ = NONE;
val simp =
full_simp_tac
- (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]) 1;
+ (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm case_prod_conv}]) 1;
fun mk_rew t = (case strip_abs_vars t of
[] => NONE
| xs => (case decomp (strip_abs_body t) of
@@ -211,7 +211,7 @@
(dest_Var x,
Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
(HOLogic.Collect_const U $
- HOLogic.mk_psplits ps U HOLogic.boolT
+ HOLogic.mk_ptupleabs ps U HOLogic.boolT
(list_comb (x', map Bound (length Ts - 1 downto 0))))))
end) fs;
@@ -232,11 +232,11 @@
in
thm' RS (infer_instantiate ctxt [(arg_cong_f,
Thm.cterm_of ctxt (Abs ("P", Ts ---> HOLogic.boolT,
- HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
+ HOLogic.Collect_const U $ HOLogic.mk_ptupleabs fs' U
HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
end)
in
- Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]
+ Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm case_prod_conv}]
addsimprocs [@{simproc Collect_mem}]) thm'' |>
zero_var_indexes |> eta_contract_thm ctxt (equal p)
end;
@@ -344,7 +344,7 @@
thm |>
Thm.instantiate ([], insts) |>
Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
- [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
+ [to_pred_simproc (mem_Collect_eq :: @{thm case_prod_conv} :: to_pred_simps)]) |>
eta_contract_thm ctxt (is_pred pred_arities) |>
Rule_Cases.save thm
end;
@@ -415,7 +415,7 @@
in
(x, (x',
(HOLogic.Collect_const T $
- HOLogic.mk_psplits fs T HOLogic.boolT x',
+ HOLogic.mk_ptupleabs fs T HOLogic.boolT x',
fold_rev (Term.abs o pair "x") Ts
(HOLogic.mk_mem
(HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)), x)))))
@@ -442,12 +442,12 @@
in
((c', (fs, U, Ts)),
(list_comb (c, params2),
- HOLogic.Collect_const U $ HOLogic.mk_psplits fs U HOLogic.boolT
+ HOLogic.Collect_const U $ HOLogic.mk_ptupleabs fs U HOLogic.boolT
(list_comb (c', params1))))
end) |> split_list |>> split_list;
val eqns' = eqns @
map (Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq)
- (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps);
+ (mem_Collect_eq :: @{thm case_prod_conv} :: to_pred_simps);
(* predicate version of the introduction rules *)
val intros' =
@@ -472,7 +472,7 @@
|> fold_map Local_Theory.define
(map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
fold_rev lambda params (HOLogic.Collect_const U $
- HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
+ HOLogic.mk_ptupleabs fs U HOLogic.boolT (list_comb (p, params3))))))
(cnames_syn ~~ cs_info ~~ preds));
(* prove theorems for converting predicate to set notation *)
@@ -487,7 +487,7 @@
list_comb (c, params))))))
(K (REPEAT (resolve_tac lthy @{thms ext} 1) THEN
simp_tac (put_simpset HOL_basic_ss lthy addsimps
- [def, mem_Collect_eq, @{thm split_conv}]) 1))
+ [def, mem_Collect_eq, @{thm case_prod_conv}]) 1))
in
lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
[Attrib.internal (K pred_set_conv_att)]),
@@ -542,7 +542,7 @@
"declare of monotonicity rule for set operators");
-(* commands *)
+(* commands *)
val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Tue Oct 13 09:21:15 2015 +0200
@@ -85,14 +85,14 @@
fun mk_split_abs vs (Bound i) t = let val (x, T) = nth vs i in Abs (x, T, t) end
| mk_split_abs vs (Const (@{const_name Product_Type.Pair}, _) $ u $ v) t =
- HOLogic.mk_split (mk_split_abs vs u (mk_split_abs vs v t))
+ HOLogic.mk_case_prod (mk_split_abs vs u (mk_split_abs vs v t))
| mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]);
-(* a variant of HOLogic.strip_psplits *)
-val strip_psplits =
+(* a variant of HOLogic.strip_ptupleabs *)
+val strip_ptupleabs =
let
fun strip [] qs vs t = (t, rev vs, qs)
- | strip (p :: ps) qs vs (Const (@{const_name uncurry}, _) $ t) =
+ | strip (p :: ps) qs vs (Const (@{const_name case_prod}, _) $ 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
@@ -129,11 +129,11 @@
| is_collect_atom (Atom (_, Const (@{const_name "Groups.uminus_class.uminus"}, _) $ (Const(@{const_name Collect}, _) $ _))) = true
| is_collect_atom _ = false
-fun mk_split _ [(x, T)] t = (T, Abs (x, T, t))
- | mk_split rT ((x, T) :: vs) t =
+fun mk_case_prod _ [(x, T)] t = (T, Abs (x, T, t))
+ | mk_case_prod rT ((x, T) :: vs) t =
let
- val (T', t') = mk_split rT vs t
- val t'' = HOLogic.split_const (T, T', rT) $ (Abs (x, T, t'))
+ val (T', t') = mk_case_prod rT vs t
+ val t'' = HOLogic.case_prod_const (T, T', rT) $ (Abs (x, T, t'))
in (domain_type (fastype_of t''), t'') end
fun mk_term vs t =
@@ -151,7 +151,7 @@
let
val (tuple, (vs', t')) = mk_term vs t
val T = HOLogic.mk_tupleT (map snd vs')
- val s = HOLogic.Collect_const T $ (snd (mk_split @{typ bool} vs' t'))
+ val s = HOLogic.Collect_const T $ (snd (mk_case_prod @{typ bool} vs' t'))
in
(tuple, Atom (tuple, s))
end
@@ -166,7 +166,7 @@
let
val (tuple, (vs', x')) = mk_term vs x
val rT = HOLogic.dest_setT (fastype_of s)
- val s = mk_vimage (snd (mk_split rT vs' x')) s
+ val s = mk_vimage (snd (mk_case_prod rT vs' x')) s
in (tuple, Atom (tuple, s)) end)
| mk_atom vs (Const (@{const_name "HOL.Not"}, _) $ t) = apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t)
| mk_atom vs t = default_atom vs t
@@ -219,7 +219,7 @@
val bs = map (fn b => the (AList.lookup (op =) subst b)) pat'
val rt = term_of_pattern Ts' (Pattern bs)
val rT = type_of_pattern Ts' (Pattern bs)
- val (_, f) = mk_split rT vs' rt
+ val (_, f) = mk_case_prod rT vs' rt
in
mk_image f t
end;
@@ -269,7 +269,7 @@
end;
fun is_reordering t =
- let val (t', _, _) = HOLogic.strip_psplits t
+ let val (t', _, _) = HOLogic.strip_ptupleabs t
in forall (fn Bound _ => true) (HOLogic.strip_tuple t') end
fun mk_pointfree_expr t =
@@ -305,7 +305,7 @@
(* proof tactic *)
-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 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)}
val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp}
val vimageE' =
@@ -327,7 +327,7 @@
ORELSE' resolve_tac ctxt @{thms arg_cong2 [OF refl, where f = "op =", OF prod.case, THEN iffD2]}
ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
(HOLogic.Trueprop_conv
- (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_distrib)))))) ctxt)))
+ (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_beta)))))) ctxt)))
fun elim_image_tac ctxt =
eresolve_tac ctxt @{thms imageE}
@@ -421,7 +421,7 @@
fun mk_term t =
let
val (T, t') = dest_Collect t
- val (t'', vs, fp) = case strip_psplits t' of
+ val (t'', vs, fp) = case strip_ptupleabs t' of
(_, [_], _) => raise TERM("mk_term", [t'])
| (t'', vs, fp) => (t'', vs, fp)
val Ts = map snd vs
--- a/src/HOL/Tools/split_rule.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/split_rule.ML Tue Oct 13 09:21:15 2015 +0200
@@ -16,13 +16,13 @@
(** split rules **)
-fun internal_split_const (Ta, Tb, Tc) =
- Const (@{const_name Product_Type.internal_split},
+fun internal_case_prod_const (Ta, Tb, Tc) =
+ Const (@{const_name Product_Type.internal_case_prod},
[[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
fun eval_internal_split ctxt =
- hol_simplify ctxt @{thms internal_split_def} o
- hol_simplify ctxt @{thms internal_split_conv};
+ hol_simplify ctxt @{thms internal_case_prod_def} o
+ hol_simplify ctxt @{thms internal_case_prod_conv};
fun remove_internal_split ctxt = eval_internal_split ctxt o split_all ctxt;
@@ -31,7 +31,7 @@
with result type T. The call creates a new term expecting one argument
of type S.*)
fun ap_split (Type (@{type_name Product_Type.prod}, [T1, T2])) T3 u =
- internal_split_const (T1, T2, T3) $
+ internal_case_prod_const (T1, T2, T3) $
Abs ("v", T1,
ap_split T2 T3
((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $
--- a/src/HOL/Transitive_Closure.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Transitive_Closure.thy Tue Oct 13 09:21:15 2015 +0200
@@ -898,7 +898,7 @@
lemma rtranclp_imp_Sup_relpowp:
assumes "(P^**) x y"
shows "(\<Squnion>n. P ^^ n) x y"
- using assms and rtrancl_imp_UN_relpow [to_pred] by blast
+ using assms and rtrancl_imp_UN_relpow [of "(x, y)", to_pred] by simp
lemma relpow_imp_rtrancl:
assumes "p \<in> R ^^ n"
@@ -918,7 +918,7 @@
lemma relpowp_imp_rtranclp:
assumes "(P ^^ n) x y"
shows "(P^**) x y"
- using assms and relpow_imp_rtrancl [to_pred] by blast
+ using assms and relpow_imp_rtrancl [of "(x, y)", to_pred] by simp
lemma rtrancl_is_UN_relpow:
"R^* = (\<Union>n. R ^^ n)"
--- a/src/HOL/UNITY/Comp.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/UNITY/Comp.thy Tue Oct 13 09:21:15 2015 +0200
@@ -186,7 +186,7 @@
apply simp
apply (subgoal_tac "G \<in> preserves (funPair v w) ")
prefer 2 apply simp
-apply (drule_tac P1 = "split Q" for Q in preserves_subset_stable [THEN subsetD],
+apply (drule_tac P1 = "case_prod Q" for Q in preserves_subset_stable [THEN subsetD],
auto)
done
--- a/src/HOL/UNITY/Extend.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/UNITY/Extend.thy Tue Oct 13 09:21:15 2015 +0200
@@ -127,7 +127,7 @@
assumes surj_h: "surj h"
and prem: "!! x y. g (h(x,y)) = x"
shows "fst (inv h z) = g z"
-by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h)
+by (metis UNIV_I f_inv_into_f prod.collapse prem surj_h)
subsection{*Trivial properties of f, g, h*}
--- a/src/HOL/Wellfounded.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Wellfounded.thy Tue Oct 13 09:21:15 2015 +0200
@@ -68,7 +68,7 @@
assumes lin: "OFCLASS('a::ord, linorder_class)"
shows "OFCLASS('a::ord, wellorder_class)"
using lin by (rule wellorder_class.intro)
- (blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf])
+ (rule class.wellorder_axioms.intro, rule wf_induct_rule [OF wf], simp)
lemma (in wellorder) wf:
"wf {(x, y). x < y}"
--- a/src/HOL/Word/Bool_List_Representation.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy Tue Oct 13 09:21:15 2015 +0200
@@ -14,7 +14,7 @@
definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
where
- "map2 f as bs = map (split f) (zip as bs)"
+ "map2 f as bs = map (case_prod f) (zip as bs)"
lemma map2_Nil [simp, code]:
"map2 f [] ys = []"
--- a/src/HOL/Word/Word.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Word/Word.thy Tue Oct 13 09:21:15 2015 +0200
@@ -3836,7 +3836,7 @@
lemma word_rsplit_empty_iff_size:
"(word_rsplit w = []) = (size w = 0)"
unfolding word_rsplit_def bin_rsplit_def word_size
- by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
+ by (simp add: bin_rsplit_aux_simp_alt Let_def split: prod.split)
lemma test_bit_rsplit:
"sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a :: len word) \<Longrightarrow>
--- a/src/HOL/ex/FinFunPred.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/ex/FinFunPred.thy Tue Oct 13 09:21:15 2015 +0200
@@ -78,7 +78,7 @@
by(intro_classes)(simp add: sup_finfun_def inf_finfun_def expand_finfun_eq o_def sup_inf_distrib1)
instantiation "finfun" :: (type, minus) minus begin
-definition "f - g = split (op -) \<circ>$ ($f, g$)"
+definition "f - g = case_prod (op -) \<circ>$ ($f, g$)"
instance ..
end
--- a/src/HOL/ex/Gauge_Integration.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy Tue Oct 13 09:21:15 2015 +0200
@@ -45,7 +45,7 @@
\<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
lemmas fine_induct [induct set: fine] =
- fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv] for \<delta> a b D P
+ fine.induct [of "\<delta>" "(a,b)" "D" "case_prod P", unfolded split_conv] for \<delta> a b D P
lemma fine_single:
"\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
--- a/src/HOL/ex/Normalization_by_Evaluation.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy Tue Oct 13 09:21:15 2015 +0200
@@ -54,7 +54,7 @@
lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization
lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization
-lemma "split (%x y. x) (a, b) = a" by normalization
+lemma "case_prod (%x y. x) (a, b) = a" by normalization
lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization
lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization