--- a/src/Doc/Logics/document/HOL.tex Wed Feb 12 08:35:56 2014 +0100
+++ b/src/Doc/Logics/document/HOL.tex Wed Feb 12 08:35:57 2014 +0100
@@ -1115,7 +1115,7 @@
\it symbol & \it meta-type & & \it description \\
\cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
\cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
- \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
+ \cdx{case_sum} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
& & conditional
\end{constants}
\begin{ttbox}\makeatletter
@@ -1126,11 +1126,11 @@
\tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s
-\tdx{sum_case_Inl} sum_case f g (Inl x) = f x
-\tdx{sum_case_Inr} sum_case f g (Inr x) = g x
+\tdx{case_sum_Inl} case_sum f g (Inl x) = f x
+\tdx{case_sum_Inr} case_sum f g (Inr x) = g x
-\tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
-\tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
+\tdx{surjective_sum} case_sum (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
+\tdx{sum.split_case} R(case_sum f g s) = ((! x. s = Inl(x) --> R(f(x))) &
(! y. s = Inr(y) --> R(g(y))))
\end{ttbox}
\caption{Type $\alpha+\beta$}\label{hol-sum}
--- a/src/HOL/BNF_Def.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/BNF_Def.thy Wed Feb 12 08:35:57 2014 +0100
@@ -118,9 +118,9 @@
lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
by metis
-lemma sum_case_o_inj:
-"sum_case f g \<circ> Inl = f"
-"sum_case f g \<circ> Inr = g"
+lemma case_sum_o_inj:
+"case_sum f g \<circ> Inl = f"
+"case_sum f g \<circ> Inr = g"
by auto
lemma card_order_csum_cone_cexp_def:
--- a/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy Wed Feb 12 08:35:57 2014 +0100
@@ -27,8 +27,8 @@
lemma sum_map_InrD: "(f \<oplus> g) z = Inr x \<Longrightarrow> \<exists>y. z = Inr y \<and> g y = x"
by (cases z) auto
-abbreviation sum_case_abbrev ("[[_,_]]" 800)
-where "[[f,g]] \<equiv> Sum_Type.sum_case f g"
+abbreviation case_sum_abbrev ("[[_,_]]" 800)
+where "[[f,g]] \<equiv> Sum_Type.case_sum f g"
lemma Inl_oplus_elim:
assumes "Inl tr \<in> (id \<oplus> f) ` tns"
--- a/src/HOL/BNF_FP_Base.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy Wed Feb 12 08:35:57 2014 +0100
@@ -19,10 +19,10 @@
lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
by blast
-lemma unit_case_Unity: "(case u of () \<Rightarrow> f) = f"
+lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f"
by (cases u) (hypsubst, rule unit.cases)
-lemma prod_case_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
+lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
by simp
lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
@@ -53,9 +53,9 @@
lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
-lemma sum_case_step:
-"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
-"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
+lemma case_sum_step:
+"case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p"
+"case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
by auto
lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
@@ -71,8 +71,8 @@
lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (cases s) auto
-lemma sum_case_if:
-"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
+lemma case_sum_if:
+"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
by simp
lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
@@ -122,14 +122,14 @@
lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
unfolding map_pair_o_convol id_comp comp_id ..
-lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
+lemma o_case_sum: "h o case_sum f g = case_sum (h o f) (h o g)"
unfolding comp_def by (auto split: sum.splits)
-lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
+lemma case_sum_o_sum_map: "case_sum f g o sum_map h1 h2 = case_sum (f o h1) (g o h2)"
unfolding comp_def by (auto split: sum.splits)
-lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
- unfolding sum_case_o_sum_map id_comp comp_id ..
+lemma case_sum_o_sum_map_id: "(case_sum id g o sum_map f id) x = case_sum (f o id) g x"
+ unfolding case_sum_o_sum_map id_comp comp_id ..
lemma fun_rel_def_butlast:
"(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
--- a/src/HOL/BNF_GFP.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/BNF_GFP.thy Wed Feb 12 08:35:57 2014 +0100
@@ -27,13 +27,13 @@
lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
by fast
-lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
+lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
by (auto split: sum.splits)
-lemma sum_case_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> sum_case g h = f"
+lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
apply rule
apply (rule ext, force split: sum.split)
-by (rule ext, metis sum_case_o_inj(2))
+by (rule ext, metis case_sum_o_inj(2))
lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
by fast
--- a/src/HOL/Bali/Basis.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Bali/Basis.thy Wed Feb 12 08:35:57 2014 +0100
@@ -147,7 +147,7 @@
hide_const In0 In1
-notation sum_case (infixr "'(+')"80)
+notation case_sum (infixr "'(+')"80)
primrec the_Inl :: "'a + 'b \<Rightarrow> 'a"
where "the_Inl (Inl a) = a"
--- a/src/HOL/Bali/Eval.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Bali/Eval.thy Wed Feb 12 08:35:57 2014 +0100
@@ -141,7 +141,7 @@
where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
definition undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals" where
- "undefined3 = sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit))
+ "undefined3 = sum3_case (In1 \<circ> case_sum (\<lambda>x. undefined) (\<lambda>x. Unit))
(\<lambda>x. In2 undefined) (\<lambda>x. In3 undefined)"
lemma [simp]: "undefined3 (In1l x) = In1 undefined"
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Wed Feb 12 08:35:57 2014 +0100
@@ -365,9 +365,9 @@
proof safe
assume ?L
from `?L` show ?R1 unfolding fin_support_def support_def
- by (fastforce simp: image_iff elim: finite_surj[of _ _ "sum_case id undefined"])
+ by (fastforce simp: image_iff elim: finite_surj[of _ _ "case_sum id undefined"])
from `?L` show ?R2 unfolding fin_support_def support_def
- by (fastforce simp: image_iff elim: finite_surj[of _ _ "sum_case undefined id"])
+ by (fastforce simp: image_iff elim: finite_surj[of _ _ "case_sum undefined id"])
next
assume ?R1 ?R2
thus ?L unfolding fin_support_def support_Un
@@ -1506,15 +1506,15 @@
qed
lemma max_fun_diff_eq_Inl:
- assumes "wo_rel.max_fun_diff (s +o t) (sum_case f1 g1) (sum_case f2 g2) = Inl x"
- "sum_case f1 g1 \<noteq> sum_case f2 g2"
- "sum_case f1 g1 \<in> FinFunc r (s +o t)" "sum_case f2 g2 \<in> FinFunc r (s +o t)"
+ assumes "wo_rel.max_fun_diff (s +o t) (case_sum f1 g1) (case_sum f2 g2) = Inl x"
+ "case_sum f1 g1 \<noteq> case_sum f2 g2"
+ "case_sum f1 g1 \<in> FinFunc r (s +o t)" "case_sum f2 g2 \<in> FinFunc r (s +o t)"
shows "wo_rel.max_fun_diff s f1 f2 = x" (is ?P) "g1 = g2" (is ?Q)
proof -
interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
interpret s!: wo_rel s by unfold_locales (rule s)
interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
- from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). sum_case f1 g1 a \<noteq> sum_case f2 g2 a} (Inl x)"
+ from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). case_sum f1 g1 a \<noteq> case_sum f2 g2 a} (Inl x)"
using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
hence "s.isMaxim {a \<in> Field s. f1 a \<noteq> f2 a} x"
unfolding st.isMaxim_def s.isMaxim_def Field_osum by (auto simp: osum_def)
@@ -1530,15 +1530,15 @@
qed
lemma max_fun_diff_eq_Inr:
- assumes "wo_rel.max_fun_diff (s +o t) (sum_case f1 g1) (sum_case f2 g2) = Inr x"
- "sum_case f1 g1 \<noteq> sum_case f2 g2"
- "sum_case f1 g1 \<in> FinFunc r (s +o t)" "sum_case f2 g2 \<in> FinFunc r (s +o t)"
+ assumes "wo_rel.max_fun_diff (s +o t) (case_sum f1 g1) (case_sum f2 g2) = Inr x"
+ "case_sum f1 g1 \<noteq> case_sum f2 g2"
+ "case_sum f1 g1 \<in> FinFunc r (s +o t)" "case_sum f2 g2 \<in> FinFunc r (s +o t)"
shows "wo_rel.max_fun_diff t g1 g2 = x" (is ?P) "g1 \<noteq> g2" (is ?Q)
proof -
interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
interpret t!: wo_rel t by unfold_locales (rule t)
interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
- from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). sum_case f1 g1 a \<noteq> sum_case f2 g2 a} (Inr x)"
+ from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). case_sum f1 g1 a \<noteq> case_sum f2 g2 a} (Inr x)"
using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
hence "t.isMaxim {a \<in> Field t. g1 a \<noteq> g2 a} x"
unfolding st.isMaxim_def t.isMaxim_def Field_osum by (auto simp: osum_def)
@@ -1551,7 +1551,7 @@
interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
- let ?f = "\<lambda>(f, g). sum_case f g"
+ let ?f = "\<lambda>(f, g). case_sum f g"
have "bij_betw ?f (Field ?L) (Field ?R)"
unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI)
show "inj_on ?f (FinFunc r s \<times> FinFunc r t)" unfolding inj_on_def
--- a/src/HOL/Code_Numeral.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Code_Numeral.thy Wed Feb 12 08:35:57 2014 +0100
@@ -375,7 +375,7 @@
by (auto simp add: sgn_if)
have aux2: "\<And>q::int. - int_of_integer k = int_of_integer l * q \<longleftrightarrow> int_of_integer k = int_of_integer l * - q" by auto
show ?thesis
- by (simp add: prod_eq_iff integer_eq_iff prod_case_beta aux1)
+ by (simp add: prod_eq_iff integer_eq_iff case_prod_beta aux1)
(auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
qed
@@ -466,7 +466,7 @@
}
note aux = this
show ?thesis
- by (auto simp add: num_of_integer_def nat_of_integer_def Let_def prod_case_beta
+ by (auto simp add: num_of_integer_def nat_of_integer_def Let_def case_prod_beta
not_le integer_eq_iff less_eq_integer_def
nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib
mult_2 [where 'a=nat] aux add_One)
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Feb 12 08:35:57 2014 +0100
@@ -182,7 +182,7 @@
else if x < 0 then - ub_sqrt prec (- x)
else 0)"
by pat_completeness auto
-termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto)
+termination by (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 0 then 1 else 0))", auto)
declare lb_sqrt.simps[simp del]
declare ub_sqrt.simps[simp del]
@@ -484,7 +484,7 @@
else Float 1 1 * ub_horner y
else ub_pi prec * Float 1 -1 - lb_horner (float_divl prec 1 x)))"
by pat_completeness auto
-termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto)
+termination by (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 0 then 1 else 0))", auto)
declare ub_arctan_horner.simps[simp del]
declare lb_arctan_horner.simps[simp del]
@@ -1387,7 +1387,7 @@
else if x < - 1 then ub_exp_horner prec (get_odd (prec + 2)) 1 1 (float_divr prec x (- floor_fl x)) ^ (nat (- int_floor_fl x))
else ub_exp_horner prec (get_odd (prec + 2)) 1 1 x)"
by pat_completeness auto
-termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if 0 < x then 1 else 0))", auto)
+termination by (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if 0 < x then 1 else 0))", auto)
lemma exp_m1_ge_quarter: "(1 / 4 :: real) \<le> exp (- 1)"
proof -
@@ -1709,7 +1709,7 @@
Some (lb_ln2 prec * (Float (exponent x + l) 0) + horner (Float (mantissa x) (- l) - 1)))"
by pat_completeness auto
-termination proof (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 1 then 1 else 0))", auto)
+termination proof (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 1 then 1 else 0))", auto)
fix prec and x :: float assume "\<not> real x \<le> 0" and "real x < 1" and "real (float_divl (max prec (Suc 0)) 1 x) < 1"
hence "0 < real x" "1 \<le> max prec (Suc 0)" "real x < 1" by auto
from float_divl_pos_less1_bound[OF `0 < real x` `real x < 1` `1 \<le> max prec (Suc 0)`]
--- a/src/HOL/Divides.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Divides.thy Wed Feb 12 08:35:57 2014 +0100
@@ -928,7 +928,7 @@
lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
- by (simp add: prod_eq_iff prod_case_beta not_less le_div_geq le_mod_geq)
+ by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
text {* Simproc for cancelling @{const div} and @{const mod} *}
--- a/src/HOL/Fun.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Fun.thy Wed Feb 12 08:35:57 2014 +0100
@@ -662,10 +662,10 @@
"_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
"f(x:=y)" == "CONST fun_upd f x y"
-(* Hint: to define the sum of two functions (or maps), use sum_case.
+(* Hint: to define the sum of two functions (or maps), use case_sum.
A nice infix syntax could be defined (in Datatype.thy or below) by
notation
- sum_case (infixr "'(+')"80)
+ case_sum (infixr "'(+')"80)
*)
lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)"
--- a/src/HOL/HOLCF/Library/Sum_Cpo.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy Wed Feb 12 08:35:57 2014 +0100
@@ -145,39 +145,39 @@
lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric]
lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric]
-lemma cont_sum_case1:
+lemma cont_case_sum1:
assumes f: "\<And>a. cont (\<lambda>x. f x a)"
assumes g: "\<And>b. cont (\<lambda>x. g x b)"
shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
by (induct y, simp add: f, simp add: g)
-lemma cont_sum_case2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (sum_case f g)"
+lemma cont_case_sum2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (case_sum f g)"
apply (rule contI)
apply (erule sum_chain_cases)
apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE)
apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
done
-lemma cont2cont_sum_case:
+lemma cont2cont_case_sum:
assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
assumes h: "cont (\<lambda>x. h x)"
shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
apply (rule cont_apply [OF h])
-apply (rule cont_sum_case2 [OF f2 g2])
-apply (rule cont_sum_case1 [OF f1 g1])
+apply (rule cont_case_sum2 [OF f2 g2])
+apply (rule cont_case_sum1 [OF f1 g1])
done
-lemma cont2cont_sum_case' [simp, cont2cont]:
+lemma cont2cont_case_sum' [simp, cont2cont]:
assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
assumes h: "cont (\<lambda>x. h x)"
shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
-using assms by (simp add: cont2cont_sum_case prod_cont_iff)
+using assms by (simp add: cont2cont_case_sum prod_cont_iff)
text {* Continuity of map function. *}
-lemma sum_map_eq: "sum_map f g = sum_case (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
+lemma sum_map_eq: "sum_map f g = case_sum (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
by (rule ext, case_tac x, simp_all)
lemma cont2cont_sum_map [simp, cont2cont]:
--- a/src/HOL/HOLCF/Product_Cpo.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/HOLCF/Product_Cpo.thy Wed Feb 12 08:35:57 2014 +0100
@@ -213,7 +213,7 @@
lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
-lemma cont2cont_prod_case:
+lemma cont2cont_case_prod:
assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
@@ -233,7 +233,7 @@
shows "cont f"
proof -
have "cont (\<lambda>(x, y). f (x, y))"
- by (intro cont2cont_prod_case f1 f2 cont2cont)
+ by (intro cont2cont_case_prod f1 f2 cont2cont)
thus "cont f"
by (simp only: split_eta)
qed
@@ -246,11 +246,11 @@
apply (simp only: prod_contI)
done
-lemma cont2cont_prod_case' [simp, cont2cont]:
+lemma cont2cont_case_prod' [simp, cont2cont]:
assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
assumes g: "cont (\<lambda>x. g x)"
- shows "cont (\<lambda>x. prod_case (f x) (g x))"
-using assms by (simp add: cont2cont_prod_case prod_cont_iff)
+ shows "cont (\<lambda>x. case_prod (f x) (g x))"
+using assms by (simp add: cont2cont_case_prod prod_cont_iff)
text {* The simple version (due to Joachim Breitner) is needed if
either element type of the pair is not a cpo. *}
@@ -262,10 +262,10 @@
text {* Admissibility of predicates on product types. *}
-lemma adm_prod_case [simp]:
+lemma adm_case_prod [simp]:
assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))"
shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)"
-unfolding prod_case_beta using assms .
+unfolding case_prod_beta using assms .
subsection {* Compactness and chain-finiteness *}
--- a/src/HOL/Hoare/hoare_syntax.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Hoare/hoare_syntax.ML Wed Feb 12 08:35:57 2014 +0100
@@ -28,7 +28,7 @@
fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
| mk_abstuple (x :: xs) body =
- Syntax.const @{const_syntax prod_case} $ 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 prod_case}, _) $ 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 prod_case}, _) $ 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, t)) = [Free (x, T)]
| abs2list _ = [];
-fun mk_ts (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = mk_ts t
+fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (x, _, t)) = mk_ts t
| mk_ts (Abs (x, _, 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 prod_case},_) $ 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 t = 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 prod_case}, _) $ Abs (x, _, t)) = true
+fun is_f (Const (@{const_syntax case_prod}, _) $ Abs (x, _, t)) = true
| is_f (Abs (x, _, t)) = true
| is_f t = false;
--- a/src/HOL/Hoare/hoare_tac.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML Wed Feb 12 08:35:57 2014 +0100
@@ -18,7 +18,7 @@
local
(** maps (%x1 ... xn. t) to [x1,...,xn] **)
-fun abs2list (Const (@{const_name prod_case}, _) $ 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, t)) = [Free (x, T)]
| abs2list _ = [];
@@ -39,7 +39,7 @@
Abs (_, T, _) => T
| Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
in
- Const (@{const_name prod_case},
+ Const (@{const_name case_prod},
(T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
absfree (x, T) z
end;
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Wed Feb 12 08:35:57 2014 +0100
@@ -692,7 +692,7 @@
-lemma sum_distrib: "sum_case fl fr (case x of Empty \<Rightarrow> y | Node v n \<Rightarrow> (z v n)) = (case x of Empty \<Rightarrow> sum_case fl fr y | Node v n \<Rightarrow> sum_case fl fr (z v n))"
+lemma sum_distrib: "case_sum fl fr (case x of Empty \<Rightarrow> y | Node v n \<Rightarrow> (z v n)) = (case x of Empty \<Rightarrow> case_sum fl fr y | Node v n \<Rightarrow> case_sum fl fr (z v n))"
by (cases x) auto
subsection {* Induction refinement by applying the abstraction function to our induct rule *}
--- a/src/HOL/Import/HOL_Light_Maps.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy Wed Feb 12 08:35:57 2014 +0100
@@ -210,7 +210,7 @@
lemma sum_RECURSION:
"\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>a :: 'B. fn (Inr a) = Inr' a)"
- by (intro allI, rule_tac x="sum_case Inl' Inr'" in exI) auto
+ by (intro allI, rule_tac x="case_sum Inl' Inr'" in exI) auto
lemma OUTL[import_const "OUTL" : "Sum_Type.projl"]:
"Sum_Type.projl (Inl x) = x"
--- a/src/HOL/Library/AList.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Library/AList.thy Wed Feb 12 08:35:57 2014 +0100
@@ -79,7 +79,7 @@
by (simp add: update_conv')
definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
- "updates ks vs = fold (prod_case update) (zip ks vs)"
+ "updates ks vs = fold (case_prod update) (zip ks vs)"
lemma updates_simps [simp]:
"updates [] vs ps = ps"
@@ -94,7 +94,7 @@
lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
proof -
- have "map_of \<circ> fold (prod_case update) (zip ks vs) =
+ have "map_of \<circ> fold (case_prod update) (zip ks vs) =
fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_conv_fold split_def)
@@ -111,9 +111,9 @@
(\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
(zip ks vs) (map fst al))"
by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
- moreover have "map fst \<circ> fold (prod_case update) (zip ks vs) =
+ moreover have "map fst \<circ> fold (case_prod update) (zip ks vs) =
fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
- by (rule fold_commute) (simp add: update_keys split_def prod_case_beta comp_def)
+ by (rule fold_commute) (simp add: update_keys split_def case_prod_beta comp_def)
ultimately show ?thesis by (simp add: updates_def fun_eq_iff)
qed
@@ -339,9 +339,9 @@
lemma clearjunk_updates:
"clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
proof -
- have "clearjunk \<circ> fold (prod_case update) (zip ks vs) =
- fold (prod_case update) (zip ks vs) \<circ> clearjunk"
- by (rule fold_commute) (simp add: clearjunk_update prod_case_beta o_def)
+ have "clearjunk \<circ> fold (case_prod update) (zip ks vs) =
+ fold (case_prod update) (zip ks vs) \<circ> clearjunk"
+ by (rule fold_commute) (simp add: clearjunk_update case_prod_beta o_def)
then show ?thesis by (simp add: updates_def fun_eq_iff)
qed
@@ -444,9 +444,9 @@
lemma merge_conv':
"map_of (merge xs ys) = map_of xs ++ map_of ys"
proof -
- have "map_of \<circ> fold (prod_case update) (rev ys) =
+ have "map_of \<circ> fold (case_prod update) (rev ys) =
fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
- by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
+ by (rule fold_commute) (simp add: update_conv' case_prod_beta split_def fun_eq_iff)
then show ?thesis
by (simp add: merge_def map_add_map_of_foldr foldr_conv_fold fun_eq_iff)
qed
--- a/src/HOL/Library/Countable_Set_Type.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Wed Feb 12 08:35:57 2014 +0100
@@ -140,7 +140,7 @@
have L: "countable ?L'" by auto
hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset)
thus ?R unfolding Grp_def relcompp.simps conversep.simps
- proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
+ proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times)
next
from * `?L` show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times)
--- a/src/HOL/Library/FSet.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Library/FSet.thy Wed Feb 12 08:35:57 2014 +0100
@@ -1017,7 +1017,7 @@
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
- proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
+ proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
from * show "a = fimage fst R'" using conjunct1[OF `?L`]
by (transfer, auto simp add: image_def Int_def split: prod.splits)
from * show "b = fimage snd R'" using conjunct2[OF `?L`]
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Feb 12 08:35:57 2014 +0100
@@ -22,7 +22,7 @@
section {* Pairs *}
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *}
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}] *}
section {* Bounded quantifiers *}
--- a/src/HOL/Library/Quotient_Product.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Library/Quotient_Product.thy Wed Feb 12 08:35:57 2014 +0100
@@ -78,7 +78,7 @@
lemma split_rsp [quot_respect]:
shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
- by (rule prod_case_transfer)
+ by (rule case_prod_transfer)
lemma split_prs [quot_preserve]:
assumes q1: "Quotient3 R1 Abs1 Rep1"
--- a/src/HOL/Library/RBT.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Library/RBT.thy Wed Feb 12 08:35:57 2014 +0100
@@ -135,7 +135,7 @@
by transfer (rule rbt_lookup_map)
lemma fold_fold:
- "fold f t = List.fold (prod_case f) (entries t)"
+ "fold f t = List.fold (case_prod f) (entries t)"
by transfer (rule RBT_Impl.fold_def)
lemma impl_of_empty:
@@ -175,7 +175,7 @@
by transfer (simp add: keys_entries)
lemma fold_def_alt:
- "fold f t = List.fold (prod_case f) (entries t)"
+ "fold f t = List.fold (case_prod f) (entries t)"
by transfer (auto simp: RBT_Impl.fold_def)
lemma distinct_entries: "distinct (List.map fst (entries t))"
--- a/src/HOL/Library/RBT_Impl.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Library/RBT_Impl.thy Wed Feb 12 08:35:57 2014 +0100
@@ -1067,7 +1067,7 @@
subsection {* Folding over entries *}
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
- "fold f t = List.fold (prod_case f) (entries t)"
+ "fold f t = List.fold (case_prod f) (entries t)"
lemma fold_simps [simp]:
"fold f Empty = id"
@@ -1110,10 +1110,10 @@
proof -
obtain ys where "ys = rev xs" by simp
have "\<And>t. is_rbt t \<Longrightarrow>
- rbt_lookup (List.fold (prod_case rbt_insert) ys t) = rbt_lookup t ++ map_of (rev ys)"
- by (induct ys) (simp_all add: rbt_bulkload_def rbt_lookup_rbt_insert prod_case_beta)
+ rbt_lookup (List.fold (case_prod rbt_insert) ys t) = rbt_lookup t ++ map_of (rev ys)"
+ by (induct ys) (simp_all add: rbt_bulkload_def rbt_lookup_rbt_insert case_prod_beta)
from this Empty_is_rbt have
- "rbt_lookup (List.fold (prod_case rbt_insert) (rev xs) Empty) = rbt_lookup Empty ++ map_of xs"
+ "rbt_lookup (List.fold (case_prod rbt_insert) (rev xs) Empty) = rbt_lookup Empty ++ map_of xs"
by (simp add: `ys = rev xs`)
then show ?thesis by (simp add: rbt_bulkload_def rbt_lookup_Empty foldr_conv_fold)
qed
--- a/src/HOL/Lifting_Product.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Lifting_Product.thy Wed Feb 12 08:35:57 2014 +0100
@@ -95,8 +95,8 @@
lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd"
unfolding fun_rel_def prod_rel_def by simp
-lemma prod_case_transfer [transfer_rule]:
- "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case"
+lemma case_prod_transfer [transfer_rule]:
+ "((A ===> B ===> C) ===> prod_rel A B ===> C) case_prod case_prod"
unfolding fun_rel_def prod_rel_def by simp
lemma curry_transfer [transfer_rule]:
--- a/src/HOL/Lifting_Sum.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Lifting_Sum.thy Wed Feb 12 08:35:57 2014 +0100
@@ -10,7 +10,7 @@
subsection {* Relator and predicator properties *}
-abbreviation (input) "sum_pred \<equiv> sum_case"
+abbreviation (input) "sum_pred \<equiv> case_sum"
lemmas sum_rel_eq[relator_eq] = sum.rel_eq
lemmas sum_rel_mono[relator_mono] = sum.rel_mono
@@ -80,8 +80,8 @@
lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr"
unfolding fun_rel_def by simp
-lemma sum_case_transfer [transfer_rule]:
- "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case"
+lemma case_sum_transfer [transfer_rule]:
+ "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) case_sum case_sum"
unfolding fun_rel_def sum_rel_def by (simp split: sum.split)
end
--- a/src/HOL/Matrix_LP/ComputeHOL.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Matrix_LP/ComputeHOL.thy Wed Feb 12 08:35:57 2014 +0100
@@ -50,9 +50,9 @@
lemma compute_snd: "snd (x,y) = y" by simp
lemma compute_pair_eq: "((a, b) = (c, d)) = (a = c \<and> b = d)" by auto
-lemma prod_case_simp: "prod_case f (x,y) = f x y" by simp
+lemma case_prod_simp: "case_prod f (x,y) = f x y" by simp
-lemmas compute_pair = compute_fst compute_snd compute_pair_eq prod_case_simp
+lemmas compute_pair = compute_fst compute_snd compute_pair_eq case_prod_simp
(*** compute_option ***)
--- a/src/HOL/Nitpick.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Nitpick.thy Wed Feb 12 08:35:57 2014 +0100
@@ -96,8 +96,8 @@
apply (erule contrapos_np)
by (rule someI)
-lemma unit_case_unfold [nitpick_unfold]:
-"unit_case x u \<equiv> x"
+lemma case_unit_unfold [nitpick_unfold]:
+"case_unit x u \<equiv> x"
apply (subgoal_tac "u = ()")
apply (simp only: unit.cases)
by simp
@@ -241,7 +241,7 @@
hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
prod_def refl'_def wf'_def card'_def setsum'_def
- fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold
+ fold_graph'_def The_psimp Eps_psimp case_unit_unfold nat_case_unfold
list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
--- a/src/HOL/Nominal/Examples/Class2.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Nominal/Examples/Class2.thy Wed Feb 12 08:35:57 2014 +0100
@@ -2881,7 +2881,7 @@
done
termination
-apply(relation "measure (sum_case (size\<circ>fst) (size\<circ>fst))")
+apply(relation "measure (case_sum (size\<circ>fst) (size\<circ>fst))")
apply(simp_all)
done
--- a/src/HOL/Option.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Option.thy Wed Feb 12 08:35:57 2014 +0100
@@ -100,8 +100,8 @@
"map f (map g opt) = map (f o g) opt"
by (simp add: map_def split add: option.split)
-lemma option_map_o_sum_case [simp]:
- "map f o sum_case g h = sum_case (map f o g) (map f o h)"
+lemma option_map_o_case_sum [simp]:
+ "map f o case_sum g h = case_sum (map f o g) (map f o h)"
by (rule ext) (simp split: sum.split)
lemma map_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map f x = map g y"
--- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Wed Feb 12 08:35:57 2014 +0100
@@ -465,7 +465,7 @@
also have "\<dots> \<in> sets ?P"
using A j
by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
- finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
+ finally show "{\<omega> \<in> space ?P. case_prod (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
qed (auto simp: space_pair_measure space_PiM PiE_def)
lemma measurable_component_update:
@@ -1132,27 +1132,27 @@
lemma pair_measure_eq_distr_PiM:
fixes M1 :: "'a measure" and M2 :: "'a measure"
assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
- shows "(M1 \<Otimes>\<^sub>M M2) = distr (Pi\<^sub>M UNIV (bool_case M1 M2)) (M1 \<Otimes>\<^sub>M M2) (\<lambda>x. (x True, x False))"
+ shows "(M1 \<Otimes>\<^sub>M M2) = distr (Pi\<^sub>M UNIV (case_bool M1 M2)) (M1 \<Otimes>\<^sub>M M2) (\<lambda>x. (x True, x False))"
(is "?P = ?D")
proof (rule pair_measure_eqI[OF assms])
- interpret B: product_sigma_finite "bool_case M1 M2"
+ interpret B: product_sigma_finite "case_bool M1 M2"
unfolding product_sigma_finite_def using assms by (auto split: bool.split)
- let ?B = "Pi\<^sub>M UNIV (bool_case M1 M2)"
+ let ?B = "Pi\<^sub>M UNIV (case_bool M1 M2)"
have [simp]: "fst \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x True)" "snd \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x False)"
by auto
fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
- have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))"
+ have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (case_bool M1 M2 i) (case_bool A B i))"
by (simp add: UNIV_bool ac_simps)
- also have "\<dots> = emeasure ?B (Pi\<^sub>E UNIV (bool_case A B))"
+ also have "\<dots> = emeasure ?B (Pi\<^sub>E UNIV (case_bool A B))"
using A B by (subst B.emeasure_PiM) (auto split: bool.split)
- also have "Pi\<^sub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
+ also have "Pi\<^sub>E UNIV (case_bool A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
using A[THEN sets.sets_into_space] B[THEN sets.sets_into_space]
by (auto simp: PiE_iff all_bool_eq space_PiM split: bool.split)
finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
using A B
- measurable_component_singleton[of True UNIV "bool_case M1 M2"]
- measurable_component_singleton[of False UNIV "bool_case M1 M2"]
+ measurable_component_singleton[of True UNIV "case_bool M1 M2"]
+ measurable_component_singleton[of False UNIV "case_bool M1 M2"]
by (subst emeasure_distr) (auto simp: measurable_pair_iff)
qed simp
--- a/src/HOL/Probability/Independent_Family.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Probability/Independent_Family.thy Wed Feb 12 08:35:57 2014 +0100
@@ -13,7 +13,7 @@
(\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> (\<forall>A\<in>Pi J F. prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))"
definition (in prob_space)
- "indep_set A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV"
+ "indep_set A B \<longleftrightarrow> indep_sets (case_bool A B) UNIV"
definition (in prob_space)
indep_events_def_alt: "indep_events A I \<longleftrightarrow> indep_sets (\<lambda>i. {A i}) I"
@@ -28,7 +28,7 @@
done
definition (in prob_space)
- "indep_event A B \<longleftrightarrow> indep_events (bool_case A B) UNIV"
+ "indep_event A B \<longleftrightarrow> indep_events (case_bool A B) UNIV"
lemma (in prob_space) indep_sets_cong:
"I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i = G i) \<Longrightarrow> indep_sets F I \<longleftrightarrow> indep_sets G J"
@@ -104,7 +104,7 @@
lemma (in prob_space) indep_setD:
assumes indep: "indep_set A B" and ev: "a \<in> A" "b \<in> B"
shows "prob (a \<inter> b) = prob a * prob b"
- using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "bool_case a b"] ev
+ using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "case_bool a b"] ev
by (simp add: ac_simps UNIV_bool)
lemma (in prob_space)
@@ -312,7 +312,7 @@
indep_sets (\<lambda>i. { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
definition (in prob_space)
- "indep_var Ma A Mb B \<longleftrightarrow> indep_vars (bool_case Ma Mb) (bool_case A B) UNIV"
+ "indep_var Ma A Mb B \<longleftrightarrow> indep_vars (case_bool Ma Mb) (case_bool A B) UNIV"
lemma (in prob_space) indep_vars_def:
"indep_vars M' X I \<longleftrightarrow>
@@ -340,16 +340,16 @@
"indep_set A B \<longleftrightarrow> A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)"
unfolding indep_set_def
proof (intro iffI ballI conjI)
- assume indep: "indep_sets (bool_case A B) UNIV"
+ assume indep: "indep_sets (case_bool A B) UNIV"
{ fix a b assume "a \<in> A" "b \<in> B"
- with indep_setsD[OF indep, of UNIV "bool_case a b"]
+ with indep_setsD[OF indep, of UNIV "case_bool a b"]
show "prob (a \<inter> b) = prob a * prob b"
unfolding UNIV_bool by (simp add: ac_simps) }
from indep show "A \<subseteq> events" "B \<subseteq> events"
unfolding indep_sets_def UNIV_bool by auto
next
assume *: "A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)"
- show "indep_sets (bool_case A B) UNIV"
+ show "indep_sets (case_bool A B) UNIV"
proof (rule indep_setsI)
fix i show "(case i of True \<Rightarrow> A | False \<Rightarrow> B) \<subseteq> events"
using * by (auto split: bool.split)
@@ -369,7 +369,7 @@
proof -
have "indep_sets (\<lambda>i. sigma_sets (space M) (case i of True \<Rightarrow> A | False \<Rightarrow> B)) UNIV"
proof (rule indep_sets_sigma)
- show "indep_sets (bool_case A B) UNIV"
+ show "indep_sets (case_bool A B) UNIV"
by (rule `indep_set A B`[unfolded indep_set_def])
fix i show "Int_stable (case i of True \<Rightarrow> A | False \<Rightarrow> B)"
using A B by (cases i) auto
@@ -572,19 +572,19 @@
qed
{ fix n
- have "indep_sets (\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) UNIV"
+ have "indep_sets (\<lambda>b. sigma_sets (space M) (\<Union>m\<in>case_bool {..n} {Suc n..} b. A m)) UNIV"
proof (rule indep_sets_collect_sigma)
have *: "(\<Union>b. case b of True \<Rightarrow> {..n} | False \<Rightarrow> {Suc n..}) = UNIV" (is "?U = _")
by (simp split: bool.split add: set_eq_iff) (metis not_less_eq_eq)
with indep show "indep_sets A ?U" by simp
- show "disjoint_family (bool_case {..n} {Suc n..})"
+ show "disjoint_family (case_bool {..n} {Suc n..})"
unfolding disjoint_family_on_def by (auto split: bool.split)
fix m
show "Int_stable (A m)"
unfolding Int_stable_def using A.Int by auto
qed
- also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) =
- bool_case (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
+ also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>case_bool {..n} {Suc n..} b. A m)) =
+ case_bool (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
by (auto intro!: ext split: bool.split)
finally have indep: "indep_set (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
unfolding indep_set_def by simp
@@ -923,9 +923,9 @@
prob (A -` Xa \<inter> space M) * prob (B -` Xb \<inter> space M)"
proof -
have "prob ((\<lambda>x. (A x, B x)) -` (Xa \<times> Xb) \<inter> space M) =
- prob (\<Inter>i\<in>UNIV. (bool_case A B i -` bool_case Xa Xb i \<inter> space M))"
+ prob (\<Inter>i\<in>UNIV. (case_bool A B i -` case_bool Xa Xb i \<inter> space M))"
by (auto intro!: arg_cong[where f=prob] simp: UNIV_bool)
- also have "\<dots> = (\<Prod>i\<in>UNIV. prob (bool_case A B i -` bool_case Xa Xb i \<inter> space M))"
+ also have "\<dots> = (\<Prod>i\<in>UNIV. prob (case_bool A B i -` case_bool Xa Xb i \<inter> space M))"
using indep unfolding indep_var_def
by (rule indep_varsD) (auto split: bool.split intro: sets)
also have "\<dots> = prob (A -` Xa \<inter> space M) * prob (B -` Xb \<inter> space M)"
@@ -938,7 +938,7 @@
shows indep_var_rv1: "random_variable S X"
and indep_var_rv2: "random_variable T Y"
proof -
- have "\<forall>i\<in>UNIV. random_variable (bool_case S T i) (bool_case X Y i)"
+ have "\<forall>i\<in>UNIV. random_variable (case_bool S T i) (case_bool X Y i)"
using assms unfolding indep_var_def indep_vars_def by auto
then show "random_variable S X" "random_variable T Y"
unfolding UNIV_bool by auto
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Feb 12 08:35:57 2014 +0100
@@ -464,11 +464,11 @@
show "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> space ((\<Pi>\<^sub>M i\<in>UNIV. M) \<Otimes>\<^sub>M (\<Pi>\<^sub>M i\<in>UNIV. M)) \<rightarrow> (UNIV \<rightarrow>\<^sub>E space M)"
by (auto simp: space_pair_measure space_PiM PiE_iff split: split_comb_seq)
fix j :: nat and A assume A: "A \<in> sets M"
- then have *: "{\<omega> \<in> space ((\<Pi>\<^sub>M i\<in>UNIV. M) \<Otimes>\<^sub>M (\<Pi>\<^sub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} =
+ then have *: "{\<omega> \<in> space ((\<Pi>\<^sub>M i\<in>UNIV. M) \<Otimes>\<^sub>M (\<Pi>\<^sub>M i\<in>UNIV. M)). case_prod (comb_seq i) \<omega> j \<in> A} =
(if j < i then {\<omega> \<in> space (\<Pi>\<^sub>M i\<in>UNIV. M). \<omega> j \<in> A} \<times> space (\<Pi>\<^sub>M i\<in>UNIV. M)
else space (\<Pi>\<^sub>M i\<in>UNIV. M) \<times> {\<omega> \<in> space (\<Pi>\<^sub>M i\<in>UNIV. M). \<omega> (j - i) \<in> A})"
by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets.sets_into_space)
- show "{\<omega> \<in> space ((\<Pi>\<^sub>M i\<in>UNIV. M) \<Otimes>\<^sub>M (\<Pi>\<^sub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} \<in> sets ((\<Pi>\<^sub>M i\<in>UNIV. M) \<Otimes>\<^sub>M (\<Pi>\<^sub>M i\<in>UNIV. M))"
+ show "{\<omega> \<in> space ((\<Pi>\<^sub>M i\<in>UNIV. M) \<Otimes>\<^sub>M (\<Pi>\<^sub>M i\<in>UNIV. M)). case_prod (comb_seq i) \<omega> j \<in> A} \<in> sets ((\<Pi>\<^sub>M i\<in>UNIV. M) \<Otimes>\<^sub>M (\<Pi>\<^sub>M i\<in>UNIV. M))"
unfolding * by (auto simp: A intro!: sets_Collect_single)
qed
--- a/src/HOL/Product_Type.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Product_Type.thy Wed Feb 12 08:35:57 2014 +0100
@@ -12,7 +12,7 @@
subsection {* @{typ bool} is a datatype *}
-wrap_free_constructors [True, False] bool_case [=]
+wrap_free_constructors [True, False] case_bool [=]
by auto
-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
@@ -80,7 +80,7 @@
else SOME (mk_meta_eq @{thm unit_eq})
*}
-wrap_free_constructors ["()"] unit_case
+wrap_free_constructors ["()"] case_unit
by auto
-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
@@ -180,7 +180,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)
-wrap_free_constructors [Pair] prod_case [] [[fst, snd]]
+wrap_free_constructors [Pair] case_prod [] [[fst, snd]]
proof -
fix P :: bool and p :: "'a \<times> 'b"
show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
@@ -224,7 +224,7 @@
subsubsection {* Tuple syntax *}
abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
- "split \<equiv> prod_case"
+ "split \<equiv> case_prod"
text {*
Patterns -- extends pre-defined type @{typ pttrn} used in
@@ -246,8 +246,8 @@
"_pattern x y" => "CONST Pair x y"
"_patterns x y" => "CONST Pair x y"
"_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
- "%(x, y, zs). b" == "CONST prod_case (%x (y, zs). b)"
- "%(x, y). b" == "CONST prod_case (%x y. b)"
+ "%(x, y, zs). b" == "CONST case_prod (%x (y, zs). b)"
+ "%(x, y). b" == "CONST case_prod (%x y. b)"
"_abs (CONST Pair x y) t" => "%(x, y). t"
-- {* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *}
@@ -265,7 +265,7 @@
Syntax.const @{syntax_const "_abs"} $
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
end
- | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
+ | split_tr' [Abs (x, T, (s as Const (@{const_syntax case_prod}, _) $ t))] =
(* split (%x. (split (%y z. t))) => %(x,y,z). t *)
let
val Const (@{syntax_const "_abs"}, _) $
@@ -276,7 +276,7 @@
(Syntax.const @{syntax_const "_pattern"} $ x' $
(Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
end
- | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
+ | split_tr' [Const (@{const_syntax case_prod}, _) $ t] =
(* split (split (%x y z. t)) => %((x, y), z). t *)
split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
| split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
@@ -286,7 +286,7 @@
(Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
end
| split_tr' _ = raise Match;
- in [(@{const_syntax prod_case}, K split_tr')] end
+ in [(@{const_syntax case_prod}, K split_tr')] end
*}
(* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *)
@@ -295,7 +295,7 @@
fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
| split_guess_names_tr' T [Abs (x, xT, t)] =
(case (head_of t) of
- Const (@{const_syntax prod_case}, _) => raise Match
+ Const (@{const_syntax case_prod}, _) => raise Match
| _ =>
let
val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
@@ -307,7 +307,7 @@
end)
| split_guess_names_tr' T [t] =
(case head_of t of
- Const (@{const_syntax prod_case}, _) => raise Match
+ Const (@{const_syntax case_prod}, _) => raise Match
| _ =>
let
val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
@@ -319,10 +319,10 @@
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
end)
| split_guess_names_tr' _ _ = raise Match;
- in [(@{const_syntax prod_case}, K split_guess_names_tr')] end
+ in [(@{const_syntax case_prod}, K split_guess_names_tr')] end
*}
-(* Force eta-contraction for terms of the form "Q A (%p. prod_case P p)"
+(* Force eta-contraction for terms of the form "Q A (%p. case_prod P p)"
where Q is some bounded quantifier or set operator.
Reason: the above prints as "Q p : A. case p of (x,y) \<Rightarrow> P x y"
whereas we want "Q (x,y):A. P x y".
@@ -332,7 +332,7 @@
let
fun contract Q tr ctxt ts =
(case ts of
- [A, Abs (_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)] =>
+ [A, Abs (_, _, (s as Const (@{const_syntax case_prod},_) $ t) $ Bound 0)] =>
if Term.is_dependent t then tr ctxt ts
else Syntax.const Q $ A $ s
| _ => tr ctxt ts);
@@ -379,7 +379,7 @@
constant fst \<rightharpoonup> (Haskell) "fst"
| constant snd \<rightharpoonup> (Haskell) "snd"
-lemma prod_case_unfold [nitpick_unfold]: "prod_case = (%c p. c (fst p) (snd p))"
+lemma case_prod_unfold [nitpick_unfold]: "case_prod = (%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"
@@ -419,7 +419,7 @@
by (cases p) simp
lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
- by (simp add: prod_case_unfold)
+ by (simp add: case_prod_unfold)
lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
-- {* Prevents simplification of @{term c}: much faster *}
@@ -511,7 +511,7 @@
| no_args k i (Bound m) = m < k orelse m > k + i
| no_args _ _ _ = true;
fun split_pat tp i (Abs (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
- | split_pat tp i (Const (@{const_name prod_case}, _) $ 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)))
@@ -529,12 +529,12 @@
else (subst arg k i t $ subst arg k i u)
| subst arg k i t = t;
in
- fun beta_proc ctxt (s as Const (@{const_name prod_case}, _) $ 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 prod_case}, _) $ 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 $ arg) = ft in f end))
| NONE => NONE)
@@ -611,14 +611,14 @@
assumes major: "z \<in> split c p"
and cases: "\<And>x y. p = (x, y) \<Longrightarrow> z \<in> c x y \<Longrightarrow> Q"
shows Q
- by (rule major [unfolded prod_case_unfold] cases surjective_pairing)+
+ by (rule major [unfolded case_prod_unfold] cases surjective_pairing)+
declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
ML {*
local (* filtering with exists_p_split is an essential optimization *)
- fun exists_p_split (Const (@{const_name prod_case},_) $ _ $ (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;
@@ -678,27 +678,27 @@
Setup of internal @{text split_rule}.
*}
-lemmas prod_caseI = prod.cases [THEN iffD2]
+lemmas case_prodI = prod.cases [THEN iffD2]
-lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
+lemma case_prodI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case_prod c p"
by (fact splitI2)
-lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x"
+lemma case_prodI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> case_prod c p x"
by (fact splitI2')
-lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
+lemma case_prodE: "case_prod c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
by (fact splitE)
-lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
+lemma case_prodE': "case_prod c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
by (fact splitE')
-declare prod_caseI [intro!]
+declare case_prodI [intro!]
-lemma prod_case_beta:
- "prod_case f p = f (fst p) (snd p)"
+lemma case_prod_beta:
+ "case_prod f p = f (fst p) (snd p)"
by (fact split_beta)
-lemma prod_cases3 [cases type]:
+lemma case_prods3 [cases type]:
obtains (fields) a b c where "y = (a, b, c)"
by (cases y, case_tac b) blast
@@ -706,7 +706,7 @@
"(!!a b c. P (a, b, c)) ==> P x"
by (cases x) blast
-lemma prod_cases4 [cases type]:
+lemma case_prods4 [cases type]:
obtains (fields) a b c d where "y = (a, b, c, d)"
by (cases y, case_tac c) blast
@@ -714,7 +714,7 @@
"(!!a b c d. P (a, b, c, d)) ==> P x"
by (cases x) blast
-lemma prod_cases5 [cases type]:
+lemma case_prods5 [cases type]:
obtains (fields) a b c d e where "y = (a, b, c, d, e)"
by (cases y, case_tac d) blast
@@ -722,7 +722,7 @@
"(!!a b c d e. P (a, b, c, d, e)) ==> P x"
by (cases x) blast
-lemma prod_cases6 [cases type]:
+lemma case_prods6 [cases type]:
obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)"
by (cases y, case_tac e) blast
@@ -730,7 +730,7 @@
"(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
by (cases x) blast
-lemma prod_cases7 [cases type]:
+lemma case_prods7 [cases type]:
obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)"
by (cases y, case_tac f) blast
@@ -740,7 +740,7 @@
lemma split_def:
"split = (\<lambda>c p. c (fst p) (snd p))"
- by (fact prod_case_unfold)
+ by (fact case_prod_unfold)
definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
"internal_split == split"
@@ -787,13 +787,13 @@
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. prod_case 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 prod_case_unfold)
+ by (simp add: fun_eq_iff scomp_def case_prod_unfold)
-lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = prod_case g (f x)"
- by (simp add: scomp_unfold prod_case_unfold)
+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"
by (simp add: fun_eq_iff)
--- a/src/HOL/Relation.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Relation.thy Wed Feb 12 08:35:57 2014 +0100
@@ -54,7 +54,7 @@
lemma lfp_induct2: -- {* Version of @{thm [source] lfp_induct} for binary relations *}
"(a, b) \<in> lfp f \<Longrightarrow> mono f \<Longrightarrow>
(\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b"
- using lfp_induct_set [of "(a, b)" f "prod_case P"] by auto
+ using lfp_induct_set [of "(a, b)" f "case_prod P"] by auto
subsubsection {* Conversions between set and predicate relations *}
@@ -113,7 +113,7 @@
lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
by (simp add: fun_eq_iff)
-lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (prod_case ` S) Collect)"
+lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (case_prod ` S) Collect)"
by (simp add: fun_eq_iff)
lemma INF_Int_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Inter>S)"
@@ -125,7 +125,7 @@
lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)"
by (simp add: fun_eq_iff)
-lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (prod_case ` S) Collect)"
+lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (case_prod ` S) Collect)"
by (simp add: fun_eq_iff)
lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
--- a/src/HOL/Sum_Type.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Sum_Type.thy Wed Feb 12 08:35:57 2014 +0100
@@ -85,7 +85,7 @@
with assms show P by (auto simp add: sum_def Inl_def Inr_def)
qed
-wrap_free_constructors [Inl, Inr] sum_case [isl] [[projl], [projr]]
+wrap_free_constructors [Inl, Inr] case_sum [isl] [[projl], [projr]]
by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
@@ -146,29 +146,29 @@
subsection {* Projections *}
-lemma sum_case_KK [simp]: "sum_case (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)"
+lemma case_sum_KK [simp]: "case_sum (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)"
by (rule ext) (simp split: sum.split)
-lemma surjective_sum: "sum_case (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f"
+lemma surjective_sum: "case_sum (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f"
proof
fix s :: "'a + 'b"
show "(case s of Inl (x\<Colon>'a) \<Rightarrow> f (Inl x) | Inr (y\<Colon>'b) \<Rightarrow> f (Inr y)) = f s"
by (cases s) simp_all
qed
-lemma sum_case_inject:
- assumes a: "sum_case f1 f2 = sum_case g1 g2"
+lemma case_sum_inject:
+ assumes a: "case_sum f1 f2 = case_sum g1 g2"
assumes r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
shows P
proof (rule r)
show "f1 = g1" proof
fix x :: 'a
- from a have "sum_case f1 f2 (Inl x) = sum_case g1 g2 (Inl x)" by simp
+ from a have "case_sum f1 f2 (Inl x) = case_sum g1 g2 (Inl x)" by simp
then show "f1 x = g1 x" by simp
qed
show "f2 = g2" proof
fix y :: 'b
- from a have "sum_case f1 f2 (Inr y) = sum_case g1 g2 (Inr y)" by simp
+ from a have "case_sum f1 f2 (Inr y) = case_sum g1 g2 (Inr y)" by simp
then show "f2 y = g2 y" by simp
qed
qed
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Feb 12 08:35:57 2014 +0100
@@ -265,7 +265,7 @@
rtac (thm RS ord_eq_le_trans) THEN' etac @{thm subset_trans[OF image_mono Un_upper1]})
set_maps,
rtac sym,
- rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF sum_case_o_inj(1)]},
+ rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]},
map_comp RS sym, map_id])] 1
end;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 12 08:35:57 2014 +0100
@@ -541,7 +541,7 @@
fun generate_iter pre (_, _, fss, xssss) ctor_iter =
(mk_binding pre,
fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_iter,
- map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss)));
+ map2 (mk_case_sumN_balanced oo map2 mk_uncurried2_fun) fss xssss)));
in
define_co_iters Least_FP fpT Cs (map3 generate_iter iterNs iter_args_typess' ctor_iters) lthy
end;
@@ -867,7 +867,7 @@
fun tack z_name (c, u) f =
let val z = Free (z_name, mk_sumT (fastype_of u, fastype_of c)) in
- Term.lambda z (mk_sum_case (Term.lambda u u, Term.lambda c (f $ c)) $ z)
+ Term.lambda z (mk_case_sum (Term.lambda u u, Term.lambda c (f $ c)) $ z)
end;
fun build_coiter fcoiters maybe_mk_sumT maybe_tack cqf =
@@ -902,7 +902,7 @@
val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
val corec_thmss =
map2 (map2 prove) corec_goalss corec_tacss
- |> map (map (unfold_thms lthy @{thms sum_case_if}));
+ |> map (map (unfold_thms lthy @{thms case_sum_if}));
in
(unfold_thmss, corec_thmss)
end;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Feb 12 08:35:57 2014 +0100
@@ -84,8 +84,8 @@
unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN HEADGOAL (rtac refl);
val iter_unfold_thms =
- @{thms comp_def convol_def fst_conv id_def prod_case_Pair_iden snd_conv
- split_conv unit_case_Unity} @ sum_prod_thms_map;
+ @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv
+ case_unit_Unity} @ sum_prod_thms_map;
fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter ctr_def ctxt =
unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_idents @
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Feb 12 08:35:57 2014 +0100
@@ -69,7 +69,7 @@
val dest_co_algT = co_swap o dest_funT;
val co_alg_argT = fp_case fp range_type domain_type;
val co_alg_funT = fp_case fp domain_type range_type;
- val mk_co_product = curry (fp_case fp mk_convol mk_sum_case);
+ val mk_co_product = curry (fp_case fp mk_convol mk_case_sum);
val mk_map_co_product = fp_case fp mk_prod_map mk_sum_map;
val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
@@ -336,7 +336,7 @@
o_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
val rec_thms = fold_thms @ fp_case fp
@{thms fst_convol map_pair_o_convol convol_o}
- @{thms sum_case_o_inj(1) sum_case_o_sum_map o_sum_case};
+ @{thms case_sum_o_inj(1) case_sum_o_sum_map o_case_sum};
val map_thms = no_refl (maps (fn bnf =>
[map_comp0_of_bnf bnf RS sym, map_id0_of_bnf bnf]) fp_nesty_bnfs);
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Feb 12 08:35:57 2014 +0100
@@ -64,7 +64,7 @@
fun unfold_lets_splits (Const (@{const_name Let}, _) $ arg1 $ arg2) =
unfold_lets_splits (betapply (arg2, arg1))
- | unfold_lets_splits (t as Const (@{const_name prod_case}, _) $ u) =
+ | unfold_lets_splits (t as Const (@{const_name case_prod}, _) $ u) =
(case unfold_lets_splits 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_fp_util.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Feb 12 08:35:57 2014 +0100
@@ -144,13 +144,13 @@
val Inl_const: typ -> typ -> term
val Inr_const: typ -> typ -> term
+ val mk_case_sum: term * term -> term
+ val mk_case_sumN: term list -> term
+ val mk_case_sumN_balanced: term list -> term
val mk_Inl: typ -> term -> term
val mk_Inr: typ -> term -> term
val mk_InN: typ list -> term -> int -> term
val mk_InN_balanced: typ -> int -> term -> int -> term
- val mk_sum_case: term * term -> term
- val mk_sum_caseN: term list -> term
- val mk_sum_caseN_balanced: term list -> term
val dest_sumT: typ -> typ * typ
val dest_sumTN: int -> typ -> typ list
@@ -166,8 +166,8 @@
val mk_sumEN: int -> thm
val mk_sumEN_balanced: int -> thm
val mk_sumEN_tupled_balanced: int list -> thm
- val mk_sum_casesN: int -> int -> thm
- val mk_sum_casesN_balanced: int -> int -> thm
+ val mk_sum_caseN: int -> int -> thm
+ val mk_sum_caseN_balanced: int -> int -> thm
val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
@@ -409,17 +409,17 @@
|> repair_types sum_T
end;
-fun mk_sum_case (f, g) =
+fun mk_case_sum (f, g) =
let
val fT = fastype_of f;
val gT = fastype_of g;
in
- Const (@{const_name sum_case},
+ Const (@{const_name case_sum},
fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g
end;
-val mk_sum_caseN = Library.foldr1 mk_sum_case;
-val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case;
+val mk_case_sumN = Library.foldr1 mk_case_sum;
+val mk_case_sumN_balanced = Balanced_Tree.make mk_case_sum;
fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end;
@@ -470,18 +470,18 @@
else mk_sumEN_balanced' n (map mk_tupled_allIN ms)
end;
-fun mk_sum_casesN 1 1 = refl
- | mk_sum_casesN _ 1 = @{thm sum.cases(1)}
- | mk_sum_casesN 2 2 = @{thm sum.cases(2)}
- | mk_sum_casesN n k = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (k - 1)];
+fun mk_sum_caseN 1 1 = refl
+ | mk_sum_caseN _ 1 = @{thm sum.case(1)}
+ | mk_sum_caseN 2 2 = @{thm sum.case(2)}
+ | mk_sum_caseN n k = trans OF [@{thm case_sum_step(2)}, mk_sum_caseN (n - 1) (k - 1)];
fun mk_sum_step base step thm =
if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm];
-fun mk_sum_casesN_balanced 1 1 = refl
- | mk_sum_casesN_balanced n k =
- Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)},
- right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k;
+fun mk_sum_caseN_balanced 1 1 = refl
+ | mk_sum_caseN_balanced n k =
+ Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm case_sum_step(1)},
+ right = mk_sum_step @{thm sum.cases(2)} @{thm case_sum_step(2)}, init = refl} n k;
fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
let
@@ -532,11 +532,11 @@
val rewrite_comp_comp = fp_case fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp};
val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
val map_cong_active_args1 = replicate n (if is_rec
- then fp_case fp @{thm convol_o} @{thm o_sum_case} RS fun_cong
+ then fp_case fp @{thm convol_o} @{thm o_case_sum} RS fun_cong
else refl);
val map_cong_passive_args2 = replicate m (fp_case fp @{thm comp_id} @{thm id_comp} RS fun_cong);
val map_cong_active_args2 = replicate n (if is_rec
- then fp_case fp @{thm map_pair_o_convol_id} @{thm sum_case_o_sum_map_id}
+ then fp_case fp @{thm map_pair_o_convol_id} @{thm case_sum_o_sum_map_id}
else fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 12 08:35:57 2014 +0100
@@ -493,16 +493,16 @@
|> Thm.close_derivation
end;
- val mor_sum_case_thm =
+ val mor_case_sum_thm =
let
val maps = map3 (fn s => fn sum_s => fn mapx =>
- mk_sum_case (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s))
+ mk_case_sum (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s))
s's sum_ss map_Inls;
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (s's @ sum_ss) (HOLogic.mk_Trueprop
(mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls)))
- (K (mk_mor_sum_case_tac ks mor_UNIV_thm))
+ (K (mk_mor_case_sum_tac ks mor_UNIV_thm))
|> Thm.close_derivation
end;
@@ -1133,7 +1133,7 @@
val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2);
in
HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
- (mk_sum_caseN fs $ (lab $ HOLogic.mk_list sum_sbdT []))))
+ (mk_case_sumN fs $ (lab $ HOLogic.mk_list sum_sbdT []))))
end;
val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
@@ -1239,7 +1239,7 @@
fun mk_case i' =
Term.absfree k' (mk_nthN n rv_rec i' $ (mk_from_sbd s b i i' $ k));
in
- Term.absfree b' (mk_sum_caseN (map mk_case ks) $ sumx)
+ Term.absfree b' (mk_case_sumN (map mk_case ks) $ sumx)
end;
val Cons = Term.absfree sumx' (Term.absdummy sum_sbd_listT (Term.absfree rv_rec'
@@ -1285,7 +1285,7 @@
val Lab = Term.absfree kl' (mk_If
(HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z))
- (mk_sum_caseN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z))
+ (mk_case_sumN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z))
(mk_undefined sbdFT));
val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
@@ -1413,7 +1413,7 @@
fun mk_conjunct i z B = HOLogic.mk_imp
(HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), HOLogic.mk_mem (z, B)),
- mk_sum_caseN (map4 mk_case ss setssAs zs zs') $ (mk_rv ss kl i $ z));
+ mk_case_sumN (map4 mk_case ss setssAs zs zs') $ (mk_rv ss kl i $ z));
val goal = list_all_free (kl :: zs)
(Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct ks zs Bs));
@@ -1433,7 +1433,7 @@
split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
(2, @{thm sum.weak_case_cong} RS iffD1) RS
- (mk_sum_casesN n i' RS iffD1))) ks) ks
+ (mk_case_sumN n i' RS iffD1))) ks) ks
end;
val set_Lev_thmsss =
@@ -1828,7 +1828,7 @@
val corec_Inl_sum_thms =
let
- val mor = mor_comp_thm OF [mor_sum_case_thm, mor_unfold_thm];
+ val mor = mor_comp_thm OF [mor_case_sum_thm, mor_unfold_thm];
in
map2 (fn unique => fn unfold_dtor =>
trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms
@@ -1839,7 +1839,7 @@
val corec_strs =
map3 (fn dtor => fn sum_s => fn mapx =>
- mk_sum_case
+ mk_case_sum
(HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s))
dtors corec_ss corec_maps;
@@ -1863,14 +1863,14 @@
val corec_defs = map (fn def =>
mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) corec_def_frees;
- val sum_cases =
- map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
+ val case_sums =
+ map2 (fn T => fn i => mk_case_sum (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
val dtor_corec_thms =
let
fun mk_goal i corec_s corec_map dtor z =
let
val lhs = dtor $ (mk_corec corec_ss i $ z);
- val rhs = Term.list_comb (corec_map, passive_ids @ sum_cases) $ (corec_s $ z);
+ val rhs = Term.list_comb (corec_map, passive_ids @ case_sums) $ (corec_s $ z);
in
fold_rev Logic.all (z :: corec_ss) (mk_Trueprop_eq (lhs, rhs))
end;
@@ -1886,7 +1886,7 @@
val corec_unique_mor_thm =
let
- val id_fs = map2 (fn T => fn f => mk_sum_case (HOLogic.id_const T, f)) Ts unfold_fs;
+ val id_fs = map2 (fn T => fn f => mk_case_sum (HOLogic.id_const T, f)) Ts unfold_fs;
val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs corec_strs UNIVs dtors id_fs);
fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i);
val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -1907,9 +1907,9 @@
val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
`split_conj_thm (split_conj_prems n
(mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
- |> Local_Defs.unfold lthy (@{thms o_sum_case comp_id id_comp comp_assoc[symmetric]
- sum_case_o_inj(1)} @ map_id0s_o_id @ sym_map_comps)
- OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
+ |> Local_Defs.unfold lthy (@{thms o_case_sum comp_id id_comp comp_assoc[symmetric]
+ case_sum_o_inj(1)} @ map_id0s_o_id @ sym_map_comps)
+ OF replicate n @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]});
val timer = time (timer "corec definitions & thms");
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Feb 12 08:35:57 2014 +0100
@@ -195,7 +195,7 @@
let val branches' = map (massage_rec bound_Ts) branches in
Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
end
- | (c as Const (@{const_name prod_case}, _), arg :: args) =>
+ | (c as Const (@{const_name case_prod}, _), arg :: args) =>
massage_rec bound_Ts
(unfold_lets_splits (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
| (Const (c, _), args as _ :: _ :: _) =>
@@ -295,12 +295,12 @@
end
| NONE =>
(case t of
- Const (@{const_name prod_case}, _) $ t' =>
+ Const (@{const_name case_prod}, _) $ t' =>
let
val U' = curried_type U;
val T' = curried_type T;
in
- Const (@{const_name prod_case}, U' --> U) $ massage_call bound_Ts U' T' t'
+ Const (@{const_name case_prod}, U' --> U) $ massage_call bound_Ts U' T' t'
end
| t1 $ t2 =>
(if has_call t2 then
@@ -771,7 +771,7 @@
let val (u, vs) = strip_comb t in
if is_Free u andalso has_call u then
Inr_const U T $ mk_tuple1 bound_Ts vs
- else if try (fst o dest_Const) u = SOME @{const_name prod_case} 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
|> Term.list_comb
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Wed Feb 12 08:35:57 2014 +0100
@@ -57,13 +57,13 @@
thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
thm list list list -> thm list list list -> thm list list -> thm list list -> thm list ->
thm list -> thm list -> tactic
+ val mk_mor_case_sum_tac: 'a list -> thm -> tactic
val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
val mk_mor_elim_tac: thm -> tactic
val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
thm list -> thm list list -> thm list list -> tactic
val mk_mor_incl_tac: thm -> thm list -> tactic
val mk_mor_str_tac: 'a list -> thm -> tactic
- val mk_mor_sum_case_tac: 'a list -> thm -> tactic
val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
thm list -> tactic
val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
@@ -170,8 +170,8 @@
fun mk_mor_str_tac ks mor_UNIV =
(stac mor_UNIV THEN' CONJ_WRAP' (K (rtac refl)) ks) 1;
-fun mk_mor_sum_case_tac ks mor_UNIV =
- (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm sum_case_o_inj(1)[symmetric]})) ks) 1;
+fun mk_mor_case_sum_tac ks mor_UNIV =
+ (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm case_sum_o_inj(1)[symmetric]})) ks) 1;
fun mk_set_incl_hset_tac def rec_Suc =
EVERY' (stac def ::
@@ -376,7 +376,7 @@
fun coalg_tac (i, ((passive_sets, active_sets), def)) =
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
- rtac (mk_sum_casesN n i), rtac CollectI,
+ rtac (mk_sum_caseN n i), rtac CollectI,
EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
passive_sets),
@@ -504,7 +504,7 @@
CONJ_WRAP' (fn rv_Cons =>
CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac exI,
rtac (@{thm append_Nil} RS arg_cong RS trans),
- rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans), rtac rv_Nil]))
+ rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS arg_cong RS trans), rtac rv_Nil]))
(ks ~~ rv_Nils))
rv_Conss,
REPEAT_DETERM o rtac allI, rtac (mk_sumEN n),
@@ -513,7 +513,7 @@
CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
rtac (@{thm append_Cons} RS arg_cong RS trans),
rtac (rv_Cons RS trans), etac (sum_weak_case_cong RS arg_cong RS trans),
- rtac (mk_sum_casesN n i RS arg_cong RS trans), atac])
+ rtac (mk_sum_caseN n i RS arg_cong RS trans), atac])
ks])
rv_Conss)
ks)] 1
@@ -530,7 +530,7 @@
EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
rtac (rv_Nil RS arg_cong RS iffD2),
- rtac (mk_sum_casesN n i RS iffD2),
+ rtac (mk_sum_caseN n i RS iffD2),
CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
(ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
REPEAT_DETERM o rtac allI,
@@ -540,7 +540,7 @@
(fn (i, (from_to_sbd, coalg_set)) =>
EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
rtac (rv_Cons RS arg_cong RS iffD2),
- rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
+ rtac (mk_sum_caseN n i RS arg_cong RS trans RS iffD2),
etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
etac coalg_set, atac])
@@ -583,7 +583,7 @@
rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnIN n i),
rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
rtac conjI, atac, dtac (sym RS trans RS sym),
- rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS trans),
+ rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS trans),
etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
dtac (mk_conjunctN n i), dtac mp, atac,
dtac (mk_conjunctN n i'), dtac mp, atac,
@@ -639,7 +639,7 @@
atac, atac, hyp_subst_tac ctxt] THEN'
CONJ_WRAP' (fn i'' =>
EVERY' [rtac impI, dtac (sym RS trans),
- rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans),
+ rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS arg_cong RS trans),
etac (from_to_sbd RS arg_cong),
REPEAT_DETERM o etac allE,
dtac (mk_conjunctN n i), dtac mp, atac,
@@ -684,7 +684,7 @@
rtac exI, rtac conjI,
(if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
- etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
+ etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)),
EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
rtac trans_fun_cong_image_id_id_apply,
@@ -708,7 +708,7 @@
rtac exI, rtac conjI,
(if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
- etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
+ etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)),
EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
rtac trans_fun_cong_image_id_id_apply,
@@ -735,7 +735,7 @@
rtac length_Lev', rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI},
CONVERSION (Conv.top_conv
(K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
- if n = 1 then rtac refl else rtac (mk_sum_casesN n i),
+ if n = 1 then rtac refl else rtac (mk_sum_caseN n i),
EVERY' (map2 (fn set_map0 => fn coalg_set =>
EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])
@@ -763,7 +763,7 @@
(K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
if n = 1 then K all_tac
else (rtac (sum_weak_case_cong RS trans) THEN'
- rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
+ rtac (mk_sum_caseN n i) THEN' rtac (mk_sum_caseN n i RS trans)),
rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
@@ -800,7 +800,7 @@
CONVERSION (Conv.top_conv
(K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
if n = 1 then K all_tac
- else rtac sum_weak_case_cong THEN' rtac (mk_sum_casesN n i' RS trans),
+ else rtac sum_weak_case_cong THEN' rtac (mk_sum_caseN n i' RS trans),
SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,
rtac refl])
ks to_sbd_injs from_to_sbds)];
@@ -927,11 +927,11 @@
unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
REPEAT_DETERM_N m o rtac refl,
- EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
+ EVERY' (map (fn thm => rtac @{thm case_sum_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
fun mk_corec_unique_mor_tac ctxt corec_defs corec_Inls unfold_unique_mor =
unfold_thms_tac ctxt
- (corec_defs @ map (fn thm => thm RS @{thm sum_case_expand_Inr'}) corec_Inls) THEN
+ (corec_defs @ map (fn thm => thm RS @{thm case_sum_expand_Inr'}) corec_Inls) THEN
etac unfold_unique_mor 1;
fun mk_dtor_coinduct_tac m raw_coind bis_rel rel_congs =
@@ -946,7 +946,7 @@
rel_congs,
rtac impI, REPEAT_DETERM o etac conjE,
CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
- rtac CollectI, etac @{thm prod_caseI}])) rel_congs] 1;
+ rtac CollectI, etac @{thm case_prodI}])) rel_congs] 1;
fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def =
let
@@ -1140,7 +1140,7 @@
passive_set_map0s dtor_set_incls),
CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) =>
EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI,
- rtac @{thm prod_caseI}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ rtac @{thm case_prodI}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
rtac conjI, rtac refl, rtac refl])
(in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
@@ -1164,7 +1164,7 @@
dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
dtac @{thm ssubst_mem[OF pair_collapse]},
REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
- @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
+ @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
hyp_subst_tac ctxt,
dtac (in_Jrel RS iffD1),
dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
@@ -1180,7 +1180,7 @@
EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
dtac @{thm ssubst_mem[OF pair_collapse]},
REPEAT_DETERM o
- eresolve_tac (CollectE :: conjE :: @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
+ eresolve_tac (CollectE :: conjE :: @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
hyp_subst_tac ctxt, dtac (in_Jrel RS iffD1),
dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jrels),
atac]]
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Wed Feb 12 08:35:57 2014 +0100
@@ -724,7 +724,7 @@
passive_set_map0s ctor_set_incls),
CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) =>
EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI,
- rtac @{thm prod_caseI}, rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ rtac @{thm case_prodI}, rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn thm =>
EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor]))
ctor_set_set_incls,
@@ -750,7 +750,7 @@
dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
dtac @{thm ssubst_mem[OF pair_collapse]},
REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
- @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
+ @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
hyp_subst_tac ctxt,
dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
TRY o
@@ -765,7 +765,7 @@
EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
dtac @{thm ssubst_mem[OF pair_collapse]},
REPEAT_DETERM o
- eresolve_tac (CollectE :: conjE :: @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
+ eresolve_tac (CollectE :: conjE :: @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
hyp_subst_tac ctxt,
dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac])
in_Irels),
--- a/src/HOL/Tools/Function/sum_tree.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Function/sum_tree.ML Wed Feb 12 08:35:57 2014 +0100
@@ -32,8 +32,7 @@
(* Sum types *)
fun mk_sumT LT RT = Type (@{type_name Sum_Type.sum}, [LT, RT])
fun mk_sumcase TL TR T l r =
- Const (@{const_name sum.sum_case},
- (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
+ Const (@{const_name sum.case_sum}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
val App = curry op $
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 12 08:35:57 2014 +0100
@@ -2267,7 +2267,7 @@
HOLogic.Collect_const tuple_T $ list_comb (Const base_x, outer_bounds)
val step_set =
HOLogic.Collect_const prod_T
- $ (Const (@{const_name prod_case}, 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/predicate_compile_core.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Feb 12 08:35:57 2014 +0100
@@ -992,7 +992,7 @@
(* Definition of executable functions and their intro and elim rules *)
-fun strip_split_abs (Const (@{const_name prod_case}, _) $ 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
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Wed Feb 12 08:35:57 2014 +0100
@@ -312,7 +312,7 @@
fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
fun mk_split T = Sign.mk_const thy
- (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
+ (@{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')));
@@ -358,7 +358,7 @@
fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
fun mk_split T = Sign.mk_const thy
- (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
+ (@{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')));
--- a/src/HOL/Tools/Quotient/quotient_term.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Wed Feb 12 08:35:57 2014 +0100
@@ -635,12 +635,12 @@
end
end
- | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
- ((t2 as Const (@{const_name prod_case}, _)) $ 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 prod_case}, _)) $ Abs (v1, ty, s1)),
- ((t2 as Const (@{const_name prod_case}, _)) $ 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/SMT/smt_normalize.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Feb 12 08:35:57 2014 +0100
@@ -356,22 +356,22 @@
(** rewrite bool case expressions as if expressions **)
local
- fun is_bool_case (Const (@{const_name "bool.bool_case"}, _)) = true
- | is_bool_case _ = false
+ fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true
+ | is_case_bool _ = false
val thm = mk_meta_eq @{lemma
- "bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp}
+ "case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp}
fun unfold_conv _ =
- SMT_Utils.if_true_conv (is_bool_case o Term.head_of)
+ SMT_Utils.if_true_conv (is_case_bool o Term.head_of)
(expand_head_conv (Conv.rewr_conv thm))
in
-fun rewrite_bool_case_conv ctxt =
- SMT_Utils.if_exists_conv is_bool_case (Conv.top_conv unfold_conv ctxt)
+fun rewrite_case_bool_conv ctxt =
+ SMT_Utils.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
-val setup_bool_case =
- SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
+val setup_case_bool =
+ SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
end
@@ -558,7 +558,7 @@
(** combined unfoldings and rewritings **)
fun unfold_conv ctxt =
- rewrite_bool_case_conv ctxt then_conv
+ rewrite_case_bool_conv ctxt then_conv
unfold_abs_min_max_conv ctxt then_conv
nat_as_int_conv ctxt then_conv
Thm.beta_conversion true
@@ -645,7 +645,7 @@
setup_unfolded_quants #>
setup_trigger #>
setup_weight #>
- setup_bool_case #>
+ setup_case_bool #>
setup_abs_min_max #>
setup_nat_as_int)
--- a/src/HOL/Tools/TFL/usyntax.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/TFL/usyntax.ML Wed Feb 12 08:35:57 2014 +0100
@@ -196,7 +196,7 @@
local
fun mk_uncurry (xt, yt, zt) =
- Const(@{const_name prod_case}, (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
@@ -276,7 +276,7 @@
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
-local fun ucheck t = (if #Name (dest_const t) = @{const_name prod_case} 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/Tools/hologic.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/hologic.ML Wed Feb 12 08:35:57 2014 +0100
@@ -357,12 +357,12 @@
end;
fun split_const (A, B, C) =
- Const ("Product_Type.prod.prod_case", (A --> B --> C) --> mk_prodT (A, B) --> C);
+ Const ("Product_Type.prod.case_prod", (A --> B --> C) --> mk_prodT (A, B) --> C);
fun mk_split t =
(case Term.fastype_of t of
T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
- Const ("Product_Type.prod.prod_case", T --> mk_prodT (A, B) --> C) $ t
+ Const ("Product_Type.prod.case_prod", T --> mk_prodT (A, B) --> C) $ t
| _ => raise TERM ("mk_split: bad body type", [t]));
(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
@@ -478,7 +478,7 @@
val strip_psplits =
let
fun strip [] qs Ts t = (t, rev Ts, qs)
- | strip (p :: ps) qs Ts (Const ("Product_Type.prod.prod_case", _) $ 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/set_comprehension_pointfree.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Wed Feb 12 08:35:57 2014 +0100
@@ -84,7 +84,7 @@
end;
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 ("Product_Type.Pair", _) $ u $ v) t =
+ | 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))
| mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]);
@@ -92,7 +92,7 @@
val strip_psplits =
let
fun strip [] qs vs t = (t, rev vs, qs)
- | strip (p :: ps) qs vs (Const ("Product_Type.prod.prod_case", _) $ t) =
+ | strip (p :: ps) qs vs (Const (@{const_name Product_Type.prod.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
@@ -305,7 +305,7 @@
(* proof tactic *)
-val prod_case_distrib = @{lemma "(prod_case g x) z = prod_case (% x y. (g x y) z) x" by (simp add: prod_case_beta)}
+val case_prod_distrib = @{lemma "(case_prod g x) z = case_prod (% x y. (g x y) z) x" by (simp add: case_prod_beta)}
val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp}
val vimageE' =
@@ -326,7 +326,7 @@
@{thm arg_cong2[OF refl, where f="op =", OF prod.cases, 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 prod_case_distrib)))))) ctxt)))
+ (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_distrib)))))) ctxt)))
fun elim_image_tac ctxt = etac @{thm imageE}
THEN' REPEAT_DETERM o CHANGED o
@@ -521,4 +521,3 @@
end;
end;
-
--- a/src/HOL/ex/Tree23.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/ex/Tree23.thy Wed Feb 12 08:35:57 2014 +0100
@@ -332,8 +332,8 @@
lemmas dfull_case_intros =
ord.exhaust [where y=y and P="dfull a (ord_case b c d y)"]
option.exhaust [of y "dfull a (case_option b c y)"]
- prod.exhaust [where y=y and P="dfull a (prod_case b y)"]
- bool.exhaust [where y=y and P="dfull a (bool_case b c y)"]
+ prod.exhaust [of y "dfull a (case_prod b y)"]
+ bool.exhaust [of y "dfull a (case_bool b c y)"]
tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))"]
tree23.exhaust [where y=y and P="full a (tree23_case b c d y)"]
for a b c d e y