renamed '{prod,sum,bool,unit}_case' to 'case_...'
authorblanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 55414eab03e9cee8a
parent 55413 a8e96847523c
child 55415 05f5fdb8d093
renamed '{prod,sum,bool,unit}_case' to 'case_...'
src/Doc/Logics/document/HOL.tex
src/HOL/BNF_Def.thy
src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy
src/HOL/BNF_FP_Base.thy
src/HOL/BNF_GFP.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/Eval.thy
src/HOL/Cardinals/Ordinal_Arithmetic.thy
src/HOL/Code_Numeral.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Divides.thy
src/HOL/Fun.thy
src/HOL/HOLCF/Library/Sum_Cpo.thy
src/HOL/HOLCF/Product_Cpo.thy
src/HOL/Hoare/hoare_syntax.ML
src/HOL/Hoare/hoare_tac.ML
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Import/HOL_Light_Maps.thy
src/HOL/Library/AList.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/RBT.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Lifting_Product.thy
src/HOL/Lifting_Sum.thy
src/HOL/Matrix_LP/ComputeHOL.thy
src/HOL/Nitpick.thy
src/HOL/Nominal/Examples/Class2.thy
src/HOL/Option.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Product_Type.thy
src/HOL/Relation.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/Function/sum_tree.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/set_comprehension_pointfree.ML
src/HOL/ex/Tree23.thy
     1.1 --- a/src/Doc/Logics/document/HOL.tex	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/Doc/Logics/document/HOL.tex	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -1115,7 +1115,7 @@
     1.4    \it symbol    & \it meta-type &           & \it description \\ 
     1.5    \cdx{Inl}     & $\alpha \To \alpha+\beta$    & & first injection\\
     1.6    \cdx{Inr}     & $\beta \To \alpha+\beta$     & & second injection\\
     1.7 -  \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
     1.8 +  \cdx{case_sum} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
     1.9          & & conditional
    1.10  \end{constants}
    1.11  \begin{ttbox}\makeatletter
    1.12 @@ -1126,11 +1126,11 @@
    1.13  
    1.14  \tdx{sumE}           [| !!x. P(Inl x);  !!y. P(Inr y) |] ==> P s
    1.15  
    1.16 -\tdx{sum_case_Inl}   sum_case f g (Inl x) = f x
    1.17 -\tdx{sum_case_Inr}   sum_case f g (Inr x) = g x
    1.18 +\tdx{case_sum_Inl}   case_sum f g (Inl x) = f x
    1.19 +\tdx{case_sum_Inr}   case_sum f g (Inr x) = g x
    1.20  
    1.21 -\tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
    1.22 -\tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
    1.23 +\tdx{surjective_sum} case_sum (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
    1.24 +\tdx{sum.split_case} R(case_sum f g s) = ((! x. s = Inl(x) --> R(f(x))) &
    1.25                                       (! y. s = Inr(y) --> R(g(y))))
    1.26  \end{ttbox}
    1.27  \caption{Type $\alpha+\beta$}\label{hol-sum}
     2.1 --- a/src/HOL/BNF_Def.thy	Wed Feb 12 08:35:56 2014 +0100
     2.2 +++ b/src/HOL/BNF_Def.thy	Wed Feb 12 08:35:57 2014 +0100
     2.3 @@ -118,9 +118,9 @@
     2.4  lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
     2.5  by metis
     2.6  
     2.7 -lemma sum_case_o_inj:
     2.8 -"sum_case f g \<circ> Inl = f"
     2.9 -"sum_case f g \<circ> Inr = g"
    2.10 +lemma case_sum_o_inj:
    2.11 +"case_sum f g \<circ> Inl = f"
    2.12 +"case_sum f g \<circ> Inr = g"
    2.13  by auto
    2.14  
    2.15  lemma card_order_csum_cone_cexp_def:
     3.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Wed Feb 12 08:35:56 2014 +0100
     3.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Wed Feb 12 08:35:57 2014 +0100
     3.3 @@ -27,8 +27,8 @@
     3.4  lemma sum_map_InrD: "(f \<oplus> g) z = Inr x \<Longrightarrow> \<exists>y. z = Inr y \<and> g y = x"
     3.5  by (cases z) auto
     3.6  
     3.7 -abbreviation sum_case_abbrev ("[[_,_]]" 800)
     3.8 -where "[[f,g]] \<equiv> Sum_Type.sum_case f g"
     3.9 +abbreviation case_sum_abbrev ("[[_,_]]" 800)
    3.10 +where "[[f,g]] \<equiv> Sum_Type.case_sum f g"
    3.11  
    3.12  lemma Inl_oplus_elim:
    3.13  assumes "Inl tr \<in> (id \<oplus> f) ` tns"
     4.1 --- a/src/HOL/BNF_FP_Base.thy	Wed Feb 12 08:35:56 2014 +0100
     4.2 +++ b/src/HOL/BNF_FP_Base.thy	Wed Feb 12 08:35:57 2014 +0100
     4.3 @@ -19,10 +19,10 @@
     4.4  lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
     4.5  by blast
     4.6  
     4.7 -lemma unit_case_Unity: "(case u of () \<Rightarrow> f) = f"
     4.8 +lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f"
     4.9  by (cases u) (hypsubst, rule unit.cases)
    4.10  
    4.11 -lemma prod_case_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
    4.12 +lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
    4.13  by simp
    4.14  
    4.15  lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
    4.16 @@ -53,9 +53,9 @@
    4.17  
    4.18  lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
    4.19  
    4.20 -lemma sum_case_step:
    4.21 -"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
    4.22 -"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
    4.23 +lemma case_sum_step:
    4.24 +"case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p"
    4.25 +"case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
    4.26  by auto
    4.27  
    4.28  lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    4.29 @@ -71,8 +71,8 @@
    4.30  lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    4.31  by (cases s) auto
    4.32  
    4.33 -lemma sum_case_if:
    4.34 -"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
    4.35 +lemma case_sum_if:
    4.36 +"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
    4.37  by simp
    4.38  
    4.39  lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
    4.40 @@ -122,14 +122,14 @@
    4.41  lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
    4.42    unfolding map_pair_o_convol id_comp comp_id ..
    4.43  
    4.44 -lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
    4.45 +lemma o_case_sum: "h o case_sum f g = case_sum (h o f) (h o g)"
    4.46    unfolding comp_def by (auto split: sum.splits)
    4.47  
    4.48 -lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
    4.49 +lemma case_sum_o_sum_map: "case_sum f g o sum_map h1 h2 = case_sum (f o h1) (g o h2)"
    4.50    unfolding comp_def by (auto split: sum.splits)
    4.51  
    4.52 -lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
    4.53 -  unfolding sum_case_o_sum_map id_comp comp_id ..
    4.54 +lemma case_sum_o_sum_map_id: "(case_sum id g o sum_map f id) x = case_sum (f o id) g x"
    4.55 +  unfolding case_sum_o_sum_map id_comp comp_id ..
    4.56  
    4.57  lemma fun_rel_def_butlast:
    4.58    "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
     5.1 --- a/src/HOL/BNF_GFP.thy	Wed Feb 12 08:35:56 2014 +0100
     5.2 +++ b/src/HOL/BNF_GFP.thy	Wed Feb 12 08:35:57 2014 +0100
     5.3 @@ -27,13 +27,13 @@
     5.4  lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
     5.5  by fast
     5.6  
     5.7 -lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
     5.8 +lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
     5.9  by (auto split: sum.splits)
    5.10  
    5.11 -lemma sum_case_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> sum_case g h = f"
    5.12 +lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
    5.13  apply rule
    5.14   apply (rule ext, force split: sum.split)
    5.15 -by (rule ext, metis sum_case_o_inj(2))
    5.16 +by (rule ext, metis case_sum_o_inj(2))
    5.17  
    5.18  lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
    5.19  by fast
     6.1 --- a/src/HOL/Bali/Basis.thy	Wed Feb 12 08:35:56 2014 +0100
     6.2 +++ b/src/HOL/Bali/Basis.thy	Wed Feb 12 08:35:57 2014 +0100
     6.3 @@ -147,7 +147,7 @@
     6.4  
     6.5  hide_const In0 In1
     6.6  
     6.7 -notation sum_case  (infixr "'(+')"80)
     6.8 +notation case_sum  (infixr "'(+')"80)
     6.9  
    6.10  primrec the_Inl :: "'a + 'b \<Rightarrow> 'a"
    6.11    where "the_Inl (Inl a) = a"
     7.1 --- a/src/HOL/Bali/Eval.thy	Wed Feb 12 08:35:56 2014 +0100
     7.2 +++ b/src/HOL/Bali/Eval.thy	Wed Feb 12 08:35:57 2014 +0100
     7.3 @@ -141,7 +141,7 @@
     7.4    where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
     7.5  
     7.6  definition undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals" where
     7.7 - "undefined3 = sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit))
     7.8 + "undefined3 = sum3_case (In1 \<circ> case_sum (\<lambda>x. undefined) (\<lambda>x. Unit))
     7.9                       (\<lambda>x. In2 undefined) (\<lambda>x. In3 undefined)"
    7.10  
    7.11  lemma [simp]: "undefined3 (In1l x) = In1 undefined"
     8.1 --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Wed Feb 12 08:35:56 2014 +0100
     8.2 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Wed Feb 12 08:35:57 2014 +0100
     8.3 @@ -365,9 +365,9 @@
     8.4  proof safe
     8.5    assume ?L
     8.6    from `?L` show ?R1 unfolding fin_support_def support_def
     8.7 -    by (fastforce simp: image_iff elim: finite_surj[of _ _ "sum_case id undefined"])
     8.8 +    by (fastforce simp: image_iff elim: finite_surj[of _ _ "case_sum id undefined"])
     8.9    from `?L` show ?R2 unfolding fin_support_def support_def
    8.10 -    by (fastforce simp: image_iff elim: finite_surj[of _ _ "sum_case undefined id"])
    8.11 +    by (fastforce simp: image_iff elim: finite_surj[of _ _ "case_sum undefined id"])
    8.12  next
    8.13    assume ?R1 ?R2
    8.14    thus ?L unfolding fin_support_def support_Un
    8.15 @@ -1506,15 +1506,15 @@
    8.16  qed
    8.17  
    8.18  lemma max_fun_diff_eq_Inl:
    8.19 -  assumes "wo_rel.max_fun_diff (s +o t) (sum_case f1 g1) (sum_case f2 g2) = Inl x"
    8.20 -    "sum_case f1 g1 \<noteq> sum_case f2 g2"
    8.21 -    "sum_case f1 g1 \<in> FinFunc r (s +o t)" "sum_case f2 g2 \<in> FinFunc r (s +o t)"
    8.22 +  assumes "wo_rel.max_fun_diff (s +o t) (case_sum f1 g1) (case_sum f2 g2) = Inl x"
    8.23 +    "case_sum f1 g1 \<noteq> case_sum f2 g2"
    8.24 +    "case_sum f1 g1 \<in> FinFunc r (s +o t)" "case_sum f2 g2 \<in> FinFunc r (s +o t)"
    8.25    shows "wo_rel.max_fun_diff s f1 f2 = x" (is ?P) "g1 = g2" (is ?Q)
    8.26  proof -
    8.27    interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
    8.28    interpret s!: wo_rel s by unfold_locales (rule s)
    8.29    interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
    8.30 -  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)"
    8.31 +  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)"
    8.32      using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
    8.33    hence "s.isMaxim {a \<in> Field s. f1 a \<noteq> f2 a} x"
    8.34      unfolding st.isMaxim_def s.isMaxim_def Field_osum by (auto simp: osum_def)
    8.35 @@ -1530,15 +1530,15 @@
    8.36  qed
    8.37  
    8.38  lemma max_fun_diff_eq_Inr:
    8.39 -  assumes "wo_rel.max_fun_diff (s +o t) (sum_case f1 g1) (sum_case f2 g2) = Inr x"
    8.40 -    "sum_case f1 g1 \<noteq> sum_case f2 g2"
    8.41 -    "sum_case f1 g1 \<in> FinFunc r (s +o t)" "sum_case f2 g2 \<in> FinFunc r (s +o t)"
    8.42 +  assumes "wo_rel.max_fun_diff (s +o t) (case_sum f1 g1) (case_sum f2 g2) = Inr x"
    8.43 +    "case_sum f1 g1 \<noteq> case_sum f2 g2"
    8.44 +    "case_sum f1 g1 \<in> FinFunc r (s +o t)" "case_sum f2 g2 \<in> FinFunc r (s +o t)"
    8.45    shows "wo_rel.max_fun_diff t g1 g2 = x" (is ?P) "g1 \<noteq> g2" (is ?Q)
    8.46  proof -
    8.47    interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
    8.48    interpret t!: wo_rel t by unfold_locales (rule t)
    8.49    interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
    8.50 -  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)"
    8.51 +  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)"
    8.52      using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
    8.53    hence "t.isMaxim {a \<in> Field t. g1 a \<noteq> g2 a} x"
    8.54      unfolding st.isMaxim_def t.isMaxim_def Field_osum by (auto simp: osum_def)
    8.55 @@ -1551,7 +1551,7 @@
    8.56    interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
    8.57    interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
    8.58    interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
    8.59 -  let ?f = "\<lambda>(f, g). sum_case f g"
    8.60 +  let ?f = "\<lambda>(f, g). case_sum f g"
    8.61    have "bij_betw ?f (Field ?L) (Field ?R)"
    8.62    unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI)
    8.63      show "inj_on ?f (FinFunc r s \<times> FinFunc r t)" unfolding inj_on_def
     9.1 --- a/src/HOL/Code_Numeral.thy	Wed Feb 12 08:35:56 2014 +0100
     9.2 +++ b/src/HOL/Code_Numeral.thy	Wed Feb 12 08:35:57 2014 +0100
     9.3 @@ -375,7 +375,7 @@
     9.4      by (auto simp add: sgn_if)
     9.5    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
     9.6    show ?thesis
     9.7 -    by (simp add: prod_eq_iff integer_eq_iff prod_case_beta aux1)
     9.8 +    by (simp add: prod_eq_iff integer_eq_iff case_prod_beta aux1)
     9.9        (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
    9.10  qed
    9.11  
    9.12 @@ -466,7 +466,7 @@
    9.13    }
    9.14    note aux = this
    9.15    show ?thesis
    9.16 -    by (auto simp add: num_of_integer_def nat_of_integer_def Let_def prod_case_beta
    9.17 +    by (auto simp add: num_of_integer_def nat_of_integer_def Let_def case_prod_beta
    9.18        not_le integer_eq_iff less_eq_integer_def
    9.19        nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib
    9.20         mult_2 [where 'a=nat] aux add_One)
    10.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Feb 12 08:35:56 2014 +0100
    10.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Feb 12 08:35:57 2014 +0100
    10.3 @@ -182,7 +182,7 @@
    10.4                else if x < 0 then - ub_sqrt prec (- x)
    10.5                              else 0)"
    10.6  by pat_completeness auto
    10.7 -termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto)
    10.8 +termination by (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 0 then 1 else 0))", auto)
    10.9  
   10.10  declare lb_sqrt.simps[simp del]
   10.11  declare ub_sqrt.simps[simp del]
   10.12 @@ -484,7 +484,7 @@
   10.13                                             else Float 1 1 * ub_horner y
   10.14                            else ub_pi prec * Float 1 -1 - lb_horner (float_divl prec 1 x)))"
   10.15  by pat_completeness auto
   10.16 -termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto)
   10.17 +termination by (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 0 then 1 else 0))", auto)
   10.18  
   10.19  declare ub_arctan_horner.simps[simp del]
   10.20  declare lb_arctan_horner.simps[simp del]
   10.21 @@ -1387,7 +1387,7 @@
   10.22               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))
   10.23                                else ub_exp_horner prec (get_odd (prec + 2)) 1 1 x)"
   10.24  by pat_completeness auto
   10.25 -termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if 0 < x then 1 else 0))", auto)
   10.26 +termination by (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if 0 < x then 1 else 0))", auto)
   10.27  
   10.28  lemma exp_m1_ge_quarter: "(1 / 4 :: real) \<le> exp (- 1)"
   10.29  proof -
   10.30 @@ -1709,7 +1709,7 @@
   10.31                                          Some (lb_ln2 prec * (Float (exponent x + l) 0) + horner (Float (mantissa x) (- l) - 1)))"
   10.32  by pat_completeness auto
   10.33  
   10.34 -termination proof (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 1 then 1 else 0))", auto)
   10.35 +termination proof (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 1 then 1 else 0))", auto)
   10.36    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"
   10.37    hence "0 < real x" "1 \<le> max prec (Suc 0)" "real x < 1" by auto
   10.38    from float_divl_pos_less1_bound[OF `0 < real x` `real x < 1` `1 \<le> max prec (Suc 0)`]
    11.1 --- a/src/HOL/Divides.thy	Wed Feb 12 08:35:56 2014 +0100
    11.2 +++ b/src/HOL/Divides.thy	Wed Feb 12 08:35:57 2014 +0100
    11.3 @@ -928,7 +928,7 @@
    11.4  
    11.5  lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
    11.6    let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
    11.7 -  by (simp add: prod_eq_iff prod_case_beta not_less le_div_geq le_mod_geq)
    11.8 +  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
    11.9  
   11.10  text {* Simproc for cancelling @{const div} and @{const mod} *}
   11.11  
    12.1 --- a/src/HOL/Fun.thy	Wed Feb 12 08:35:56 2014 +0100
    12.2 +++ b/src/HOL/Fun.thy	Wed Feb 12 08:35:57 2014 +0100
    12.3 @@ -662,10 +662,10 @@
    12.4    "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
    12.5    "f(x:=y)" == "CONST fun_upd f x y"
    12.6  
    12.7 -(* Hint: to define the sum of two functions (or maps), use sum_case.
    12.8 +(* Hint: to define the sum of two functions (or maps), use case_sum.
    12.9           A nice infix syntax could be defined (in Datatype.thy or below) by
   12.10  notation
   12.11 -  sum_case  (infixr "'(+')"80)
   12.12 +  case_sum  (infixr "'(+')"80)
   12.13  *)
   12.14  
   12.15  lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)"
    13.1 --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Wed Feb 12 08:35:56 2014 +0100
    13.2 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Wed Feb 12 08:35:57 2014 +0100
    13.3 @@ -145,39 +145,39 @@
    13.4  lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric]
    13.5  lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric]
    13.6  
    13.7 -lemma cont_sum_case1:
    13.8 +lemma cont_case_sum1:
    13.9    assumes f: "\<And>a. cont (\<lambda>x. f x a)"
   13.10    assumes g: "\<And>b. cont (\<lambda>x. g x b)"
   13.11    shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
   13.12  by (induct y, simp add: f, simp add: g)
   13.13  
   13.14 -lemma cont_sum_case2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (sum_case f g)"
   13.15 +lemma cont_case_sum2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (case_sum f g)"
   13.16  apply (rule contI)
   13.17  apply (erule sum_chain_cases)
   13.18  apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE)
   13.19  apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
   13.20  done
   13.21  
   13.22 -lemma cont2cont_sum_case:
   13.23 +lemma cont2cont_case_sum:
   13.24    assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
   13.25    assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
   13.26    assumes h: "cont (\<lambda>x. h x)"
   13.27    shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
   13.28  apply (rule cont_apply [OF h])
   13.29 -apply (rule cont_sum_case2 [OF f2 g2])
   13.30 -apply (rule cont_sum_case1 [OF f1 g1])
   13.31 +apply (rule cont_case_sum2 [OF f2 g2])
   13.32 +apply (rule cont_case_sum1 [OF f1 g1])
   13.33  done
   13.34  
   13.35 -lemma cont2cont_sum_case' [simp, cont2cont]:
   13.36 +lemma cont2cont_case_sum' [simp, cont2cont]:
   13.37    assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
   13.38    assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
   13.39    assumes h: "cont (\<lambda>x. h x)"
   13.40    shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
   13.41 -using assms by (simp add: cont2cont_sum_case prod_cont_iff)
   13.42 +using assms by (simp add: cont2cont_case_sum prod_cont_iff)
   13.43  
   13.44  text {* Continuity of map function. *}
   13.45  
   13.46 -lemma sum_map_eq: "sum_map f g = sum_case (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
   13.47 +lemma sum_map_eq: "sum_map f g = case_sum (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
   13.48  by (rule ext, case_tac x, simp_all)
   13.49  
   13.50  lemma cont2cont_sum_map [simp, cont2cont]:
    14.1 --- a/src/HOL/HOLCF/Product_Cpo.thy	Wed Feb 12 08:35:56 2014 +0100
    14.2 +++ b/src/HOL/HOLCF/Product_Cpo.thy	Wed Feb 12 08:35:57 2014 +0100
    14.3 @@ -213,7 +213,7 @@
    14.4  
    14.5  lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
    14.6  
    14.7 -lemma cont2cont_prod_case:
    14.8 +lemma cont2cont_case_prod:
    14.9    assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
   14.10    assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
   14.11    assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
   14.12 @@ -233,7 +233,7 @@
   14.13    shows "cont f"
   14.14  proof -
   14.15    have "cont (\<lambda>(x, y). f (x, y))"
   14.16 -    by (intro cont2cont_prod_case f1 f2 cont2cont)
   14.17 +    by (intro cont2cont_case_prod f1 f2 cont2cont)
   14.18    thus "cont f"
   14.19      by (simp only: split_eta)
   14.20  qed
   14.21 @@ -246,11 +246,11 @@
   14.22  apply (simp only: prod_contI)
   14.23  done
   14.24  
   14.25 -lemma cont2cont_prod_case' [simp, cont2cont]:
   14.26 +lemma cont2cont_case_prod' [simp, cont2cont]:
   14.27    assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
   14.28    assumes g: "cont (\<lambda>x. g x)"
   14.29 -  shows "cont (\<lambda>x. prod_case (f x) (g x))"
   14.30 -using assms by (simp add: cont2cont_prod_case prod_cont_iff)
   14.31 +  shows "cont (\<lambda>x. case_prod (f x) (g x))"
   14.32 +using assms by (simp add: cont2cont_case_prod prod_cont_iff)
   14.33  
   14.34  text {* The simple version (due to Joachim Breitner) is needed if
   14.35    either element type of the pair is not a cpo. *}
   14.36 @@ -262,10 +262,10 @@
   14.37  
   14.38  text {* Admissibility of predicates on product types. *}
   14.39  
   14.40 -lemma adm_prod_case [simp]:
   14.41 +lemma adm_case_prod [simp]:
   14.42    assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))"
   14.43    shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)"
   14.44 -unfolding prod_case_beta using assms .
   14.45 +unfolding case_prod_beta using assms .
   14.46  
   14.47  subsection {* Compactness and chain-finiteness *}
   14.48  
    15.1 --- a/src/HOL/Hoare/hoare_syntax.ML	Wed Feb 12 08:35:56 2014 +0100
    15.2 +++ b/src/HOL/Hoare/hoare_syntax.ML	Wed Feb 12 08:35:57 2014 +0100
    15.3 @@ -28,7 +28,7 @@
    15.4  
    15.5  fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
    15.6    | mk_abstuple (x :: xs) body =
    15.7 -      Syntax.const @{const_syntax prod_case} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
    15.8 +      Syntax.const @{const_syntax case_prod} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
    15.9  
   15.10  fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
   15.11    | mk_fbody x e (y :: xs) =
   15.12 @@ -82,21 +82,21 @@
   15.13  local
   15.14  
   15.15  fun dest_abstuple
   15.16 -      (Const (@{const_syntax prod_case}, _) $ Abs (v, _, body)) =
   15.17 +      (Const (@{const_syntax case_prod}, _) $ Abs (v, _, body)) =
   15.18          subst_bound (Syntax.free v, dest_abstuple body)
   15.19    | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
   15.20    | dest_abstuple tm = tm;
   15.21  
   15.22 -fun abs2list (Const (@{const_syntax prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
   15.23 +fun abs2list (Const (@{const_syntax case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
   15.24    | abs2list (Abs (x, T, t)) = [Free (x, T)]
   15.25    | abs2list _ = [];
   15.26  
   15.27 -fun mk_ts (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = mk_ts t
   15.28 +fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (x, _, t)) = mk_ts t
   15.29    | mk_ts (Abs (x, _, t)) = mk_ts t
   15.30    | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
   15.31    | mk_ts t = [t];
   15.32  
   15.33 -fun mk_vts (Const (@{const_syntax prod_case},_) $ Abs (x, _, t)) =
   15.34 +fun mk_vts (Const (@{const_syntax case_prod},_) $ Abs (x, _, t)) =
   15.35        (Syntax.free x :: abs2list t, mk_ts t)
   15.36    | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
   15.37    | mk_vts t = raise Match;
   15.38 @@ -106,7 +106,7 @@
   15.39        if t = Bound i then find_ch vts (i - 1) xs
   15.40        else (true, (v, subst_bounds (xs, t)));
   15.41  
   15.42 -fun is_f (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = true
   15.43 +fun is_f (Const (@{const_syntax case_prod}, _) $ Abs (x, _, t)) = true
   15.44    | is_f (Abs (x, _, t)) = true
   15.45    | is_f t = false;
   15.46  
    16.1 --- a/src/HOL/Hoare/hoare_tac.ML	Wed Feb 12 08:35:56 2014 +0100
    16.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Wed Feb 12 08:35:57 2014 +0100
    16.3 @@ -18,7 +18,7 @@
    16.4  local
    16.5  
    16.6  (** maps (%x1 ... xn. t) to [x1,...,xn] **)
    16.7 -fun abs2list (Const (@{const_name prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
    16.8 +fun abs2list (Const (@{const_name case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
    16.9    | abs2list (Abs (x, T, t)) = [Free (x, T)]
   16.10    | abs2list _ = [];
   16.11  
   16.12 @@ -39,7 +39,7 @@
   16.13              Abs (_, T, _) => T
   16.14            | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
   16.15        in
   16.16 -        Const (@{const_name prod_case},
   16.17 +        Const (@{const_name case_prod},
   16.18              (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
   16.19            absfree (x, T) z
   16.20        end;
    17.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Feb 12 08:35:56 2014 +0100
    17.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Feb 12 08:35:57 2014 +0100
    17.3 @@ -692,7 +692,7 @@
    17.4  
    17.5  
    17.6  
    17.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))"
    17.8 +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))"
    17.9  by (cases x) auto
   17.10  
   17.11  subsection {* Induction refinement by applying the abstraction function to our induct rule *}
    18.1 --- a/src/HOL/Import/HOL_Light_Maps.thy	Wed Feb 12 08:35:56 2014 +0100
    18.2 +++ b/src/HOL/Import/HOL_Light_Maps.thy	Wed Feb 12 08:35:57 2014 +0100
    18.3 @@ -210,7 +210,7 @@
    18.4  
    18.5  lemma sum_RECURSION:
    18.6    "\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>a :: 'B. fn (Inr a) = Inr' a)"
    18.7 -  by (intro allI, rule_tac x="sum_case Inl' Inr'" in exI) auto
    18.8 +  by (intro allI, rule_tac x="case_sum Inl' Inr'" in exI) auto
    18.9  
   18.10  lemma OUTL[import_const "OUTL" : "Sum_Type.projl"]:
   18.11    "Sum_Type.projl (Inl x) = x"
    19.1 --- a/src/HOL/Library/AList.thy	Wed Feb 12 08:35:56 2014 +0100
    19.2 +++ b/src/HOL/Library/AList.thy	Wed Feb 12 08:35:57 2014 +0100
    19.3 @@ -79,7 +79,7 @@
    19.4    by (simp add: update_conv')
    19.5  
    19.6  definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
    19.7 -  "updates ks vs = fold (prod_case update) (zip ks vs)"
    19.8 +  "updates ks vs = fold (case_prod update) (zip ks vs)"
    19.9  
   19.10  lemma updates_simps [simp]:
   19.11    "updates [] vs ps = ps"
   19.12 @@ -94,7 +94,7 @@
   19.13  
   19.14  lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
   19.15  proof -
   19.16 -  have "map_of \<circ> fold (prod_case update) (zip ks vs) =
   19.17 +  have "map_of \<circ> fold (case_prod update) (zip ks vs) =
   19.18      fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
   19.19      by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
   19.20    then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_conv_fold split_def)
   19.21 @@ -111,9 +111,9 @@
   19.22         (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
   19.23         (zip ks vs) (map fst al))"
   19.24      by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
   19.25 -  moreover have "map fst \<circ> fold (prod_case update) (zip ks vs) =
   19.26 +  moreover have "map fst \<circ> fold (case_prod update) (zip ks vs) =
   19.27      fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
   19.28 -    by (rule fold_commute) (simp add: update_keys split_def prod_case_beta comp_def)
   19.29 +    by (rule fold_commute) (simp add: update_keys split_def case_prod_beta comp_def)
   19.30    ultimately show ?thesis by (simp add: updates_def fun_eq_iff)
   19.31  qed
   19.32  
   19.33 @@ -339,9 +339,9 @@
   19.34  lemma clearjunk_updates:
   19.35    "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
   19.36  proof -
   19.37 -  have "clearjunk \<circ> fold (prod_case update) (zip ks vs) =
   19.38 -    fold (prod_case update) (zip ks vs) \<circ> clearjunk"
   19.39 -    by (rule fold_commute) (simp add: clearjunk_update prod_case_beta o_def)
   19.40 +  have "clearjunk \<circ> fold (case_prod update) (zip ks vs) =
   19.41 +    fold (case_prod update) (zip ks vs) \<circ> clearjunk"
   19.42 +    by (rule fold_commute) (simp add: clearjunk_update case_prod_beta o_def)
   19.43    then show ?thesis by (simp add: updates_def fun_eq_iff)
   19.44  qed
   19.45  
   19.46 @@ -444,9 +444,9 @@
   19.47  lemma merge_conv':
   19.48    "map_of (merge xs ys) = map_of xs ++ map_of ys"
   19.49  proof -
   19.50 -  have "map_of \<circ> fold (prod_case update) (rev ys) =
   19.51 +  have "map_of \<circ> fold (case_prod update) (rev ys) =
   19.52      fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
   19.53 -    by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
   19.54 +    by (rule fold_commute) (simp add: update_conv' case_prod_beta split_def fun_eq_iff)
   19.55    then show ?thesis
   19.56      by (simp add: merge_def map_add_map_of_foldr foldr_conv_fold fun_eq_iff)
   19.57  qed
    20.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Wed Feb 12 08:35:56 2014 +0100
    20.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Wed Feb 12 08:35:57 2014 +0100
    20.3 @@ -140,7 +140,7 @@
    20.4    have L: "countable ?L'" by auto
    20.5    hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset)
    20.6    thus ?R unfolding Grp_def relcompp.simps conversep.simps
    20.7 -  proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
    20.8 +  proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
    20.9      from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times)
   20.10    next
   20.11      from * `?L` show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times)
    21.1 --- a/src/HOL/Library/FSet.thy	Wed Feb 12 08:35:56 2014 +0100
    21.2 +++ b/src/HOL/Library/FSet.thy	Wed Feb 12 08:35:57 2014 +0100
    21.3 @@ -1017,7 +1017,7 @@
    21.4    have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+
    21.5    hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
    21.6    show ?R unfolding Grp_def relcompp.simps conversep.simps
    21.7 -  proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
    21.8 +  proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
    21.9      from * show "a = fimage fst R'" using conjunct1[OF `?L`]
   21.10        by (transfer, auto simp add: image_def Int_def split: prod.splits)
   21.11      from * show "b = fimage snd R'" using conjunct2[OF `?L`]
    22.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Feb 12 08:35:56 2014 +0100
    22.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Feb 12 08:35:57 2014 +0100
    22.3 @@ -22,7 +22,7 @@
    22.4  
    22.5  section {* Pairs *}
    22.6  
    22.7 -setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *}
    22.8 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}] *}
    22.9  
   22.10  section {* Bounded quantifiers *}
   22.11  
    23.1 --- a/src/HOL/Library/Quotient_Product.thy	Wed Feb 12 08:35:56 2014 +0100
    23.2 +++ b/src/HOL/Library/Quotient_Product.thy	Wed Feb 12 08:35:57 2014 +0100
    23.3 @@ -78,7 +78,7 @@
    23.4  
    23.5  lemma split_rsp [quot_respect]:
    23.6    shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
    23.7 -  by (rule prod_case_transfer)
    23.8 +  by (rule case_prod_transfer)
    23.9  
   23.10  lemma split_prs [quot_preserve]:
   23.11    assumes q1: "Quotient3 R1 Abs1 Rep1"
    24.1 --- a/src/HOL/Library/RBT.thy	Wed Feb 12 08:35:56 2014 +0100
    24.2 +++ b/src/HOL/Library/RBT.thy	Wed Feb 12 08:35:57 2014 +0100
    24.3 @@ -135,7 +135,7 @@
    24.4    by transfer (rule rbt_lookup_map)
    24.5  
    24.6  lemma fold_fold:
    24.7 -  "fold f t = List.fold (prod_case f) (entries t)"
    24.8 +  "fold f t = List.fold (case_prod f) (entries t)"
    24.9    by transfer (rule RBT_Impl.fold_def)
   24.10  
   24.11  lemma impl_of_empty:
   24.12 @@ -175,7 +175,7 @@
   24.13    by transfer (simp add: keys_entries)
   24.14  
   24.15  lemma fold_def_alt:
   24.16 -  "fold f t = List.fold (prod_case f) (entries t)"
   24.17 +  "fold f t = List.fold (case_prod f) (entries t)"
   24.18    by transfer (auto simp: RBT_Impl.fold_def)
   24.19  
   24.20  lemma distinct_entries: "distinct (List.map fst (entries t))"
    25.1 --- a/src/HOL/Library/RBT_Impl.thy	Wed Feb 12 08:35:56 2014 +0100
    25.2 +++ b/src/HOL/Library/RBT_Impl.thy	Wed Feb 12 08:35:57 2014 +0100
    25.3 @@ -1067,7 +1067,7 @@
    25.4  subsection {* Folding over entries *}
    25.5  
    25.6  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
    25.7 -  "fold f t = List.fold (prod_case f) (entries t)"
    25.8 +  "fold f t = List.fold (case_prod f) (entries t)"
    25.9  
   25.10  lemma fold_simps [simp]:
   25.11    "fold f Empty = id"
   25.12 @@ -1110,10 +1110,10 @@
   25.13  proof -
   25.14    obtain ys where "ys = rev xs" by simp
   25.15    have "\<And>t. is_rbt t \<Longrightarrow>
   25.16 -    rbt_lookup (List.fold (prod_case rbt_insert) ys t) = rbt_lookup t ++ map_of (rev ys)"
   25.17 -      by (induct ys) (simp_all add: rbt_bulkload_def rbt_lookup_rbt_insert prod_case_beta)
   25.18 +    rbt_lookup (List.fold (case_prod rbt_insert) ys t) = rbt_lookup t ++ map_of (rev ys)"
   25.19 +      by (induct ys) (simp_all add: rbt_bulkload_def rbt_lookup_rbt_insert case_prod_beta)
   25.20    from this Empty_is_rbt have
   25.21 -    "rbt_lookup (List.fold (prod_case rbt_insert) (rev xs) Empty) = rbt_lookup Empty ++ map_of xs"
   25.22 +    "rbt_lookup (List.fold (case_prod rbt_insert) (rev xs) Empty) = rbt_lookup Empty ++ map_of xs"
   25.23       by (simp add: `ys = rev xs`)
   25.24    then show ?thesis by (simp add: rbt_bulkload_def rbt_lookup_Empty foldr_conv_fold)
   25.25  qed
    26.1 --- a/src/HOL/Lifting_Product.thy	Wed Feb 12 08:35:56 2014 +0100
    26.2 +++ b/src/HOL/Lifting_Product.thy	Wed Feb 12 08:35:57 2014 +0100
    26.3 @@ -95,8 +95,8 @@
    26.4  lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd"
    26.5    unfolding fun_rel_def prod_rel_def by simp
    26.6  
    26.7 -lemma prod_case_transfer [transfer_rule]:
    26.8 -  "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case"
    26.9 +lemma case_prod_transfer [transfer_rule]:
   26.10 +  "((A ===> B ===> C) ===> prod_rel A B ===> C) case_prod case_prod"
   26.11    unfolding fun_rel_def prod_rel_def by simp
   26.12  
   26.13  lemma curry_transfer [transfer_rule]:
    27.1 --- a/src/HOL/Lifting_Sum.thy	Wed Feb 12 08:35:56 2014 +0100
    27.2 +++ b/src/HOL/Lifting_Sum.thy	Wed Feb 12 08:35:57 2014 +0100
    27.3 @@ -10,7 +10,7 @@
    27.4  
    27.5  subsection {* Relator and predicator properties *}
    27.6  
    27.7 -abbreviation (input) "sum_pred \<equiv> sum_case"
    27.8 +abbreviation (input) "sum_pred \<equiv> case_sum"
    27.9  
   27.10  lemmas sum_rel_eq[relator_eq] = sum.rel_eq
   27.11  lemmas sum_rel_mono[relator_mono] = sum.rel_mono
   27.12 @@ -80,8 +80,8 @@
   27.13  lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr"
   27.14    unfolding fun_rel_def by simp
   27.15  
   27.16 -lemma sum_case_transfer [transfer_rule]:
   27.17 -  "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case"
   27.18 +lemma case_sum_transfer [transfer_rule]:
   27.19 +  "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) case_sum case_sum"
   27.20    unfolding fun_rel_def sum_rel_def by (simp split: sum.split)
   27.21  
   27.22  end
    28.1 --- a/src/HOL/Matrix_LP/ComputeHOL.thy	Wed Feb 12 08:35:56 2014 +0100
    28.2 +++ b/src/HOL/Matrix_LP/ComputeHOL.thy	Wed Feb 12 08:35:57 2014 +0100
    28.3 @@ -50,9 +50,9 @@
    28.4  lemma compute_snd: "snd (x,y) = y" by simp
    28.5  lemma compute_pair_eq: "((a, b) = (c, d)) = (a = c \<and> b = d)" by auto
    28.6  
    28.7 -lemma prod_case_simp: "prod_case f (x,y) = f x y" by simp
    28.8 +lemma case_prod_simp: "case_prod f (x,y) = f x y" by simp
    28.9  
   28.10 -lemmas compute_pair = compute_fst compute_snd compute_pair_eq prod_case_simp
   28.11 +lemmas compute_pair = compute_fst compute_snd compute_pair_eq case_prod_simp
   28.12  
   28.13  (*** compute_option ***)
   28.14  
    29.1 --- a/src/HOL/Nitpick.thy	Wed Feb 12 08:35:56 2014 +0100
    29.2 +++ b/src/HOL/Nitpick.thy	Wed Feb 12 08:35:57 2014 +0100
    29.3 @@ -96,8 +96,8 @@
    29.4  apply (erule contrapos_np)
    29.5  by (rule someI)
    29.6  
    29.7 -lemma unit_case_unfold [nitpick_unfold]:
    29.8 -"unit_case x u \<equiv> x"
    29.9 +lemma case_unit_unfold [nitpick_unfold]:
   29.10 +"case_unit x u \<equiv> x"
   29.11  apply (subgoal_tac "u = ()")
   29.12   apply (simp only: unit.cases)
   29.13  by simp
   29.14 @@ -241,7 +241,7 @@
   29.15  hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
   29.16  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
   29.17      prod_def refl'_def wf'_def card'_def setsum'_def
   29.18 -    fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold
   29.19 +    fold_graph'_def The_psimp Eps_psimp case_unit_unfold nat_case_unfold
   29.20      list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
   29.21      zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
   29.22      plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
    30.1 --- a/src/HOL/Nominal/Examples/Class2.thy	Wed Feb 12 08:35:56 2014 +0100
    30.2 +++ b/src/HOL/Nominal/Examples/Class2.thy	Wed Feb 12 08:35:57 2014 +0100
    30.3 @@ -2881,7 +2881,7 @@
    30.4  done
    30.5  
    30.6  termination
    30.7 -apply(relation "measure (sum_case (size\<circ>fst) (size\<circ>fst))")
    30.8 +apply(relation "measure (case_sum (size\<circ>fst) (size\<circ>fst))")
    30.9  apply(simp_all)
   30.10  done
   30.11  
    31.1 --- a/src/HOL/Option.thy	Wed Feb 12 08:35:56 2014 +0100
    31.2 +++ b/src/HOL/Option.thy	Wed Feb 12 08:35:57 2014 +0100
    31.3 @@ -100,8 +100,8 @@
    31.4      "map f (map g opt) = map (f o g) opt"
    31.5    by (simp add: map_def split add: option.split)
    31.6  
    31.7 -lemma option_map_o_sum_case [simp]:
    31.8 -    "map f o sum_case g h = sum_case (map f o g) (map f o h)"
    31.9 +lemma option_map_o_case_sum [simp]:
   31.10 +    "map f o case_sum g h = case_sum (map f o g) (map f o h)"
   31.11    by (rule ext) (simp split: sum.split)
   31.12  
   31.13  lemma map_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map f x = map g y"
    32.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Feb 12 08:35:56 2014 +0100
    32.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Feb 12 08:35:57 2014 +0100
    32.3 @@ -465,7 +465,7 @@
    32.4    also have "\<dots> \<in> sets ?P"
    32.5      using A j
    32.6      by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
    32.7 -  finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
    32.8 +  finally show "{\<omega> \<in> space ?P. case_prod (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
    32.9  qed (auto simp: space_pair_measure space_PiM PiE_def)
   32.10  
   32.11  lemma measurable_component_update:
   32.12 @@ -1132,27 +1132,27 @@
   32.13  lemma pair_measure_eq_distr_PiM:
   32.14    fixes M1 :: "'a measure" and M2 :: "'a measure"
   32.15    assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
   32.16 -  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))"
   32.17 +  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))"
   32.18      (is "?P = ?D")
   32.19  proof (rule pair_measure_eqI[OF assms])
   32.20 -  interpret B: product_sigma_finite "bool_case M1 M2"
   32.21 +  interpret B: product_sigma_finite "case_bool M1 M2"
   32.22      unfolding product_sigma_finite_def using assms by (auto split: bool.split)
   32.23 -  let ?B = "Pi\<^sub>M UNIV (bool_case M1 M2)"
   32.24 +  let ?B = "Pi\<^sub>M UNIV (case_bool M1 M2)"
   32.25  
   32.26    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)"
   32.27      by auto
   32.28    fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
   32.29 -  have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))"
   32.30 +  have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (case_bool M1 M2 i) (case_bool A B i))"
   32.31      by (simp add: UNIV_bool ac_simps)
   32.32 -  also have "\<dots> = emeasure ?B (Pi\<^sub>E UNIV (bool_case A B))"
   32.33 +  also have "\<dots> = emeasure ?B (Pi\<^sub>E UNIV (case_bool A B))"
   32.34      using A B by (subst B.emeasure_PiM) (auto split: bool.split)
   32.35 -  also have "Pi\<^sub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
   32.36 +  also have "Pi\<^sub>E UNIV (case_bool A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
   32.37      using A[THEN sets.sets_into_space] B[THEN sets.sets_into_space]
   32.38      by (auto simp: PiE_iff all_bool_eq space_PiM split: bool.split)
   32.39    finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
   32.40      using A B
   32.41 -      measurable_component_singleton[of True UNIV "bool_case M1 M2"]
   32.42 -      measurable_component_singleton[of False UNIV "bool_case M1 M2"]
   32.43 +      measurable_component_singleton[of True UNIV "case_bool M1 M2"]
   32.44 +      measurable_component_singleton[of False UNIV "case_bool M1 M2"]
   32.45      by (subst emeasure_distr) (auto simp: measurable_pair_iff)
   32.46  qed simp
   32.47  
    33.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Feb 12 08:35:56 2014 +0100
    33.2 +++ b/src/HOL/Probability/Independent_Family.thy	Wed Feb 12 08:35:57 2014 +0100
    33.3 @@ -13,7 +13,7 @@
    33.4      (\<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))))"
    33.5  
    33.6  definition (in prob_space)
    33.7 -  "indep_set A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV"
    33.8 +  "indep_set A B \<longleftrightarrow> indep_sets (case_bool A B) UNIV"
    33.9  
   33.10  definition (in prob_space)
   33.11    indep_events_def_alt: "indep_events A I \<longleftrightarrow> indep_sets (\<lambda>i. {A i}) I"
   33.12 @@ -28,7 +28,7 @@
   33.13    done
   33.14  
   33.15  definition (in prob_space)
   33.16 -  "indep_event A B \<longleftrightarrow> indep_events (bool_case A B) UNIV"
   33.17 +  "indep_event A B \<longleftrightarrow> indep_events (case_bool A B) UNIV"
   33.18  
   33.19  lemma (in prob_space) indep_sets_cong:
   33.20    "I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i = G i) \<Longrightarrow> indep_sets F I \<longleftrightarrow> indep_sets G J"
   33.21 @@ -104,7 +104,7 @@
   33.22  lemma (in prob_space) indep_setD:
   33.23    assumes indep: "indep_set A B" and ev: "a \<in> A" "b \<in> B"
   33.24    shows "prob (a \<inter> b) = prob a * prob b"
   33.25 -  using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "bool_case a b"] ev
   33.26 +  using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "case_bool a b"] ev
   33.27    by (simp add: ac_simps UNIV_bool)
   33.28  
   33.29  lemma (in prob_space)
   33.30 @@ -312,7 +312,7 @@
   33.31      indep_sets (\<lambda>i. { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
   33.32  
   33.33  definition (in prob_space)
   33.34 -  "indep_var Ma A Mb B \<longleftrightarrow> indep_vars (bool_case Ma Mb) (bool_case A B) UNIV"
   33.35 +  "indep_var Ma A Mb B \<longleftrightarrow> indep_vars (case_bool Ma Mb) (case_bool A B) UNIV"
   33.36  
   33.37  lemma (in prob_space) indep_vars_def:
   33.38    "indep_vars M' X I \<longleftrightarrow>
   33.39 @@ -340,16 +340,16 @@
   33.40    "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)"
   33.41    unfolding indep_set_def
   33.42  proof (intro iffI ballI conjI)
   33.43 -  assume indep: "indep_sets (bool_case A B) UNIV"
   33.44 +  assume indep: "indep_sets (case_bool A B) UNIV"
   33.45    { fix a b assume "a \<in> A" "b \<in> B"
   33.46 -    with indep_setsD[OF indep, of UNIV "bool_case a b"]
   33.47 +    with indep_setsD[OF indep, of UNIV "case_bool a b"]
   33.48      show "prob (a \<inter> b) = prob a * prob b"
   33.49        unfolding UNIV_bool by (simp add: ac_simps) }
   33.50    from indep show "A \<subseteq> events" "B \<subseteq> events"
   33.51      unfolding indep_sets_def UNIV_bool by auto
   33.52  next
   33.53    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)"
   33.54 -  show "indep_sets (bool_case A B) UNIV"
   33.55 +  show "indep_sets (case_bool A B) UNIV"
   33.56    proof (rule indep_setsI)
   33.57      fix i show "(case i of True \<Rightarrow> A | False \<Rightarrow> B) \<subseteq> events"
   33.58        using * by (auto split: bool.split)
   33.59 @@ -369,7 +369,7 @@
   33.60  proof -
   33.61    have "indep_sets (\<lambda>i. sigma_sets (space M) (case i of True \<Rightarrow> A | False \<Rightarrow> B)) UNIV"
   33.62    proof (rule indep_sets_sigma)
   33.63 -    show "indep_sets (bool_case A B) UNIV"
   33.64 +    show "indep_sets (case_bool A B) UNIV"
   33.65        by (rule `indep_set A B`[unfolded indep_set_def])
   33.66      fix i show "Int_stable (case i of True \<Rightarrow> A | False \<Rightarrow> B)"
   33.67        using A B by (cases i) auto
   33.68 @@ -572,19 +572,19 @@
   33.69    qed
   33.70  
   33.71    { fix n
   33.72 -    have "indep_sets (\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) UNIV"
   33.73 +    have "indep_sets (\<lambda>b. sigma_sets (space M) (\<Union>m\<in>case_bool {..n} {Suc n..} b. A m)) UNIV"
   33.74      proof (rule indep_sets_collect_sigma)
   33.75        have *: "(\<Union>b. case b of True \<Rightarrow> {..n} | False \<Rightarrow> {Suc n..}) = UNIV" (is "?U = _")
   33.76          by (simp split: bool.split add: set_eq_iff) (metis not_less_eq_eq)
   33.77        with indep show "indep_sets A ?U" by simp
   33.78 -      show "disjoint_family (bool_case {..n} {Suc n..})"
   33.79 +      show "disjoint_family (case_bool {..n} {Suc n..})"
   33.80          unfolding disjoint_family_on_def by (auto split: bool.split)
   33.81        fix m
   33.82        show "Int_stable (A m)"
   33.83          unfolding Int_stable_def using A.Int by auto
   33.84      qed
   33.85 -    also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) =
   33.86 -      bool_case (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
   33.87 +    also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>case_bool {..n} {Suc n..} b. A m)) =
   33.88 +      case_bool (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
   33.89        by (auto intro!: ext split: bool.split)
   33.90      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))"
   33.91        unfolding indep_set_def by simp
   33.92 @@ -923,9 +923,9 @@
   33.93      prob (A -` Xa \<inter> space M) * prob (B -` Xb \<inter> space M)"
   33.94  proof -
   33.95    have "prob ((\<lambda>x. (A x, B x)) -` (Xa \<times> Xb) \<inter> space M) =
   33.96 -    prob (\<Inter>i\<in>UNIV. (bool_case A B i -` bool_case Xa Xb i \<inter> space M))"
   33.97 +    prob (\<Inter>i\<in>UNIV. (case_bool A B i -` case_bool Xa Xb i \<inter> space M))"
   33.98      by (auto intro!: arg_cong[where f=prob] simp: UNIV_bool)
   33.99 -  also have "\<dots> = (\<Prod>i\<in>UNIV. prob (bool_case A B i -` bool_case Xa Xb i \<inter> space M))"
  33.100 +  also have "\<dots> = (\<Prod>i\<in>UNIV. prob (case_bool A B i -` case_bool Xa Xb i \<inter> space M))"
  33.101      using indep unfolding indep_var_def
  33.102      by (rule indep_varsD) (auto split: bool.split intro: sets)
  33.103    also have "\<dots> = prob (A -` Xa \<inter> space M) * prob (B -` Xb \<inter> space M)"
  33.104 @@ -938,7 +938,7 @@
  33.105    shows indep_var_rv1: "random_variable S X"
  33.106      and indep_var_rv2: "random_variable T Y"
  33.107  proof -
  33.108 -  have "\<forall>i\<in>UNIV. random_variable (bool_case S T i) (bool_case X Y i)"
  33.109 +  have "\<forall>i\<in>UNIV. random_variable (case_bool S T i) (case_bool X Y i)"
  33.110      using assms unfolding indep_var_def indep_vars_def by auto
  33.111    then show "random_variable S X" "random_variable T Y"
  33.112      unfolding UNIV_bool by auto
    34.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Feb 12 08:35:56 2014 +0100
    34.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Feb 12 08:35:57 2014 +0100
    34.3 @@ -464,11 +464,11 @@
    34.4    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)"
    34.5      by (auto simp: space_pair_measure space_PiM PiE_iff split: split_comb_seq)
    34.6    fix j :: nat and A assume A: "A \<in> sets M"
    34.7 -  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} =
    34.8 +  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} =
    34.9      (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)
   34.10                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})"
   34.11      by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets.sets_into_space)
   34.12 -  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))"
   34.13 +  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))"
   34.14      unfolding * by (auto simp: A intro!: sets_Collect_single)
   34.15  qed
   34.16  
    35.1 --- a/src/HOL/Product_Type.thy	Wed Feb 12 08:35:56 2014 +0100
    35.2 +++ b/src/HOL/Product_Type.thy	Wed Feb 12 08:35:57 2014 +0100
    35.3 @@ -12,7 +12,7 @@
    35.4  
    35.5  subsection {* @{typ bool} is a datatype *}
    35.6  
    35.7 -wrap_free_constructors [True, False] bool_case [=]
    35.8 +wrap_free_constructors [True, False] case_bool [=]
    35.9  by auto
   35.10  
   35.11  -- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
   35.12 @@ -80,7 +80,7 @@
   35.13      else SOME (mk_meta_eq @{thm unit_eq})
   35.14  *}
   35.15  
   35.16 -wrap_free_constructors ["()"] unit_case
   35.17 +wrap_free_constructors ["()"] case_unit
   35.18  by auto
   35.19  
   35.20  -- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
   35.21 @@ -180,7 +180,7 @@
   35.22  lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
   35.23    by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
   35.24  
   35.25 -wrap_free_constructors [Pair] prod_case [] [[fst, snd]]
   35.26 +wrap_free_constructors [Pair] case_prod [] [[fst, snd]]
   35.27  proof -
   35.28    fix P :: bool and p :: "'a \<times> 'b"
   35.29    show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
   35.30 @@ -224,7 +224,7 @@
   35.31  subsubsection {* Tuple syntax *}
   35.32  
   35.33  abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
   35.34 -  "split \<equiv> prod_case"
   35.35 +  "split \<equiv> case_prod"
   35.36  
   35.37  text {*
   35.38    Patterns -- extends pre-defined type @{typ pttrn} used in
   35.39 @@ -246,8 +246,8 @@
   35.40    "_pattern x y" => "CONST Pair x y"
   35.41    "_patterns x y" => "CONST Pair x y"
   35.42    "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
   35.43 -  "%(x, y, zs). b" == "CONST prod_case (%x (y, zs). b)"
   35.44 -  "%(x, y). b" == "CONST prod_case (%x y. b)"
   35.45 +  "%(x, y, zs). b" == "CONST case_prod (%x (y, zs). b)"
   35.46 +  "%(x, y). b" == "CONST case_prod (%x y. b)"
   35.47    "_abs (CONST Pair x y) t" => "%(x, y). t"
   35.48    -- {* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
   35.49       The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *}
   35.50 @@ -265,7 +265,7 @@
   35.51              Syntax.const @{syntax_const "_abs"} $
   35.52                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   35.53            end
   35.54 -      | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
   35.55 +      | split_tr' [Abs (x, T, (s as Const (@{const_syntax case_prod}, _) $ t))] =
   35.56            (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
   35.57            let
   35.58              val Const (@{syntax_const "_abs"}, _) $
   35.59 @@ -276,7 +276,7 @@
   35.60                (Syntax.const @{syntax_const "_pattern"} $ x' $
   35.61                  (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
   35.62            end
   35.63 -      | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
   35.64 +      | split_tr' [Const (@{const_syntax case_prod}, _) $ t] =
   35.65            (* split (split (%x y z. t)) => %((x, y), z). t *)
   35.66            split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
   35.67        | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
   35.68 @@ -286,7 +286,7 @@
   35.69                (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
   35.70            end
   35.71        | split_tr' _ = raise Match;
   35.72 -  in [(@{const_syntax prod_case}, K split_tr')] end
   35.73 +  in [(@{const_syntax case_prod}, K split_tr')] end
   35.74  *}
   35.75  
   35.76  (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
   35.77 @@ -295,7 +295,7 @@
   35.78      fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
   35.79        | split_guess_names_tr' T [Abs (x, xT, t)] =
   35.80            (case (head_of t) of
   35.81 -            Const (@{const_syntax prod_case}, _) => raise Match
   35.82 +            Const (@{const_syntax case_prod}, _) => raise Match
   35.83            | _ =>
   35.84              let 
   35.85                val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   35.86 @@ -307,7 +307,7 @@
   35.87              end)
   35.88        | split_guess_names_tr' T [t] =
   35.89            (case head_of t of
   35.90 -            Const (@{const_syntax prod_case}, _) => raise Match
   35.91 +            Const (@{const_syntax case_prod}, _) => raise Match
   35.92            | _ =>
   35.93              let
   35.94                val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   35.95 @@ -319,10 +319,10 @@
   35.96                  (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   35.97              end)
   35.98        | split_guess_names_tr' _ _ = raise Match;
   35.99 -  in [(@{const_syntax prod_case}, K split_guess_names_tr')] end
  35.100 +  in [(@{const_syntax case_prod}, K split_guess_names_tr')] end
  35.101  *}
  35.102  
  35.103 -(* Force eta-contraction for terms of the form "Q A (%p. prod_case P p)"
  35.104 +(* Force eta-contraction for terms of the form "Q A (%p. case_prod P p)"
  35.105     where Q is some bounded quantifier or set operator.
  35.106     Reason: the above prints as "Q p : A. case p of (x,y) \<Rightarrow> P x y"
  35.107     whereas we want "Q (x,y):A. P x y".
  35.108 @@ -332,7 +332,7 @@
  35.109    let
  35.110      fun contract Q tr ctxt ts =
  35.111        (case ts of
  35.112 -        [A, Abs (_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)] =>
  35.113 +        [A, Abs (_, _, (s as Const (@{const_syntax case_prod},_) $ t) $ Bound 0)] =>
  35.114            if Term.is_dependent t then tr ctxt ts
  35.115            else Syntax.const Q $ A $ s
  35.116        | _ => tr ctxt ts);
  35.117 @@ -379,7 +379,7 @@
  35.118    constant fst \<rightharpoonup> (Haskell) "fst"
  35.119  | constant snd \<rightharpoonup> (Haskell) "snd"
  35.120  
  35.121 -lemma prod_case_unfold [nitpick_unfold]: "prod_case = (%c p. c (fst p) (snd p))"
  35.122 +lemma case_prod_unfold [nitpick_unfold]: "case_prod = (%c p. c (fst p) (snd p))"
  35.123    by (simp add: fun_eq_iff split: prod.split)
  35.124  
  35.125  lemma fst_eqD: "fst (x, y) = a ==> x = a"
  35.126 @@ -419,7 +419,7 @@
  35.127    by (cases p) simp
  35.128  
  35.129  lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
  35.130 -  by (simp add: prod_case_unfold)
  35.131 +  by (simp add: case_prod_unfold)
  35.132  
  35.133  lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
  35.134    -- {* Prevents simplification of @{term c}: much faster *}
  35.135 @@ -511,7 +511,7 @@
  35.136      | no_args k i (Bound m) = m < k orelse m > k + i
  35.137      | no_args _ _ _ = true;
  35.138    fun split_pat tp i (Abs  (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
  35.139 -    | split_pat tp i (Const (@{const_name prod_case}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
  35.140 +    | split_pat tp i (Const (@{const_name case_prod}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
  35.141      | split_pat tp i _ = NONE;
  35.142    fun metaeq ctxt lhs rhs = mk_meta_eq (Goal.prove ctxt [] []
  35.143          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
  35.144 @@ -529,12 +529,12 @@
  35.145          else (subst arg k i t $ subst arg k i u)
  35.146      | subst arg k i t = t;
  35.147  in
  35.148 -  fun beta_proc ctxt (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) =
  35.149 +  fun beta_proc ctxt (s as Const (@{const_name case_prod}, _) $ Abs (_, _, t) $ arg) =
  35.150          (case split_pat beta_term_pat 1 t of
  35.151            SOME (i, f) => SOME (metaeq ctxt s (subst arg 0 i f))
  35.152          | NONE => NONE)
  35.153      | beta_proc _ _ = NONE;
  35.154 -  fun eta_proc ctxt (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t)) =
  35.155 +  fun eta_proc ctxt (s as Const (@{const_name case_prod}, _) $ Abs (_, _, t)) =
  35.156          (case split_pat eta_term_pat 1 t of
  35.157            SOME (_, ft) => SOME (metaeq ctxt s (let val (f $ arg) = ft in f end))
  35.158          | NONE => NONE)
  35.159 @@ -611,14 +611,14 @@
  35.160    assumes major: "z \<in> split c p"
  35.161      and cases: "\<And>x y. p = (x, y) \<Longrightarrow> z \<in> c x y \<Longrightarrow> Q"
  35.162    shows Q
  35.163 -  by (rule major [unfolded prod_case_unfold] cases surjective_pairing)+
  35.164 +  by (rule major [unfolded case_prod_unfold] cases surjective_pairing)+
  35.165  
  35.166  declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
  35.167  declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
  35.168  
  35.169  ML {*
  35.170  local (* filtering with exists_p_split is an essential optimization *)
  35.171 -  fun exists_p_split (Const (@{const_name prod_case},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
  35.172 +  fun exists_p_split (Const (@{const_name case_prod},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
  35.173      | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
  35.174      | exists_p_split (Abs (_, _, t)) = exists_p_split t
  35.175      | exists_p_split _ = false;
  35.176 @@ -678,27 +678,27 @@
  35.177    Setup of internal @{text split_rule}.
  35.178  *}
  35.179  
  35.180 -lemmas prod_caseI = prod.cases [THEN iffD2]
  35.181 +lemmas case_prodI = prod.cases [THEN iffD2]
  35.182  
  35.183 -lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
  35.184 +lemma case_prodI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case_prod c p"
  35.185    by (fact splitI2)
  35.186  
  35.187 -lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x"
  35.188 +lemma case_prodI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> case_prod c p x"
  35.189    by (fact splitI2')
  35.190  
  35.191 -lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
  35.192 +lemma case_prodE: "case_prod c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
  35.193    by (fact splitE)
  35.194  
  35.195 -lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
  35.196 +lemma case_prodE': "case_prod c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
  35.197    by (fact splitE')
  35.198  
  35.199 -declare prod_caseI [intro!]
  35.200 +declare case_prodI [intro!]
  35.201  
  35.202 -lemma prod_case_beta:
  35.203 -  "prod_case f p = f (fst p) (snd p)"
  35.204 +lemma case_prod_beta:
  35.205 +  "case_prod f p = f (fst p) (snd p)"
  35.206    by (fact split_beta)
  35.207  
  35.208 -lemma prod_cases3 [cases type]:
  35.209 +lemma case_prods3 [cases type]:
  35.210    obtains (fields) a b c where "y = (a, b, c)"
  35.211    by (cases y, case_tac b) blast
  35.212  
  35.213 @@ -706,7 +706,7 @@
  35.214      "(!!a b c. P (a, b, c)) ==> P x"
  35.215    by (cases x) blast
  35.216  
  35.217 -lemma prod_cases4 [cases type]:
  35.218 +lemma case_prods4 [cases type]:
  35.219    obtains (fields) a b c d where "y = (a, b, c, d)"
  35.220    by (cases y, case_tac c) blast
  35.221  
  35.222 @@ -714,7 +714,7 @@
  35.223      "(!!a b c d. P (a, b, c, d)) ==> P x"
  35.224    by (cases x) blast
  35.225  
  35.226 -lemma prod_cases5 [cases type]:
  35.227 +lemma case_prods5 [cases type]:
  35.228    obtains (fields) a b c d e where "y = (a, b, c, d, e)"
  35.229    by (cases y, case_tac d) blast
  35.230  
  35.231 @@ -722,7 +722,7 @@
  35.232      "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
  35.233    by (cases x) blast
  35.234  
  35.235 -lemma prod_cases6 [cases type]:
  35.236 +lemma case_prods6 [cases type]:
  35.237    obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)"
  35.238    by (cases y, case_tac e) blast
  35.239  
  35.240 @@ -730,7 +730,7 @@
  35.241      "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
  35.242    by (cases x) blast
  35.243  
  35.244 -lemma prod_cases7 [cases type]:
  35.245 +lemma case_prods7 [cases type]:
  35.246    obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)"
  35.247    by (cases y, case_tac f) blast
  35.248  
  35.249 @@ -740,7 +740,7 @@
  35.250  
  35.251  lemma split_def:
  35.252    "split = (\<lambda>c p. c (fst p) (snd p))"
  35.253 -  by (fact prod_case_unfold)
  35.254 +  by (fact case_prod_unfold)
  35.255  
  35.256  definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
  35.257    "internal_split == split"
  35.258 @@ -787,13 +787,13 @@
  35.259  notation fcomp (infixl "\<circ>>" 60)
  35.260  
  35.261  definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60) where
  35.262 -  "f \<circ>\<rightarrow> g = (\<lambda>x. prod_case g (f x))"
  35.263 +  "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod g (f x))"
  35.264  
  35.265  lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
  35.266 -  by (simp add: fun_eq_iff scomp_def prod_case_unfold)
  35.267 +  by (simp add: fun_eq_iff scomp_def case_prod_unfold)
  35.268  
  35.269 -lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = prod_case g (f x)"
  35.270 -  by (simp add: scomp_unfold prod_case_unfold)
  35.271 +lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = case_prod g (f x)"
  35.272 +  by (simp add: scomp_unfold case_prod_unfold)
  35.273  
  35.274  lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
  35.275    by (simp add: fun_eq_iff)
    36.1 --- a/src/HOL/Relation.thy	Wed Feb 12 08:35:56 2014 +0100
    36.2 +++ b/src/HOL/Relation.thy	Wed Feb 12 08:35:57 2014 +0100
    36.3 @@ -54,7 +54,7 @@
    36.4  lemma lfp_induct2: -- {* Version of @{thm [source] lfp_induct} for binary relations *}
    36.5    "(a, b) \<in> lfp f \<Longrightarrow> mono f \<Longrightarrow>
    36.6      (\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b"
    36.7 -  using lfp_induct_set [of "(a, b)" f "prod_case P"] by auto
    36.8 +  using lfp_induct_set [of "(a, b)" f "case_prod P"] by auto
    36.9  
   36.10  
   36.11  subsubsection {* Conversions between set and predicate relations *}
   36.12 @@ -113,7 +113,7 @@
   36.13  lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
   36.14    by (simp add: fun_eq_iff)
   36.15  
   36.16 -lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (prod_case ` S) Collect)"
   36.17 +lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (case_prod ` S) Collect)"
   36.18    by (simp add: fun_eq_iff)
   36.19  
   36.20  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)"
   36.21 @@ -125,7 +125,7 @@
   36.22  lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)"
   36.23    by (simp add: fun_eq_iff)
   36.24  
   36.25 -lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (prod_case ` S) Collect)"
   36.26 +lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (case_prod ` S) Collect)"
   36.27    by (simp add: fun_eq_iff)
   36.28  
   36.29  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)"
    37.1 --- a/src/HOL/Sum_Type.thy	Wed Feb 12 08:35:56 2014 +0100
    37.2 +++ b/src/HOL/Sum_Type.thy	Wed Feb 12 08:35:57 2014 +0100
    37.3 @@ -85,7 +85,7 @@
    37.4    with assms show P by (auto simp add: sum_def Inl_def Inr_def)
    37.5  qed
    37.6  
    37.7 -wrap_free_constructors [Inl, Inr] sum_case [isl] [[projl], [projr]]
    37.8 +wrap_free_constructors [Inl, Inr] case_sum [isl] [[projl], [projr]]
    37.9  by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
   37.10  
   37.11  -- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
   37.12 @@ -146,29 +146,29 @@
   37.13  
   37.14  subsection {* Projections *}
   37.15  
   37.16 -lemma sum_case_KK [simp]: "sum_case (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)"
   37.17 +lemma case_sum_KK [simp]: "case_sum (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)"
   37.18    by (rule ext) (simp split: sum.split)
   37.19  
   37.20 -lemma surjective_sum: "sum_case (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f"
   37.21 +lemma surjective_sum: "case_sum (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f"
   37.22  proof
   37.23    fix s :: "'a + 'b"
   37.24    show "(case s of Inl (x\<Colon>'a) \<Rightarrow> f (Inl x) | Inr (y\<Colon>'b) \<Rightarrow> f (Inr y)) = f s"
   37.25      by (cases s) simp_all
   37.26  qed
   37.27  
   37.28 -lemma sum_case_inject:
   37.29 -  assumes a: "sum_case f1 f2 = sum_case g1 g2"
   37.30 +lemma case_sum_inject:
   37.31 +  assumes a: "case_sum f1 f2 = case_sum g1 g2"
   37.32    assumes r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
   37.33    shows P
   37.34  proof (rule r)
   37.35    show "f1 = g1" proof
   37.36      fix x :: 'a
   37.37 -    from a have "sum_case f1 f2 (Inl x) = sum_case g1 g2 (Inl x)" by simp
   37.38 +    from a have "case_sum f1 f2 (Inl x) = case_sum g1 g2 (Inl x)" by simp
   37.39      then show "f1 x = g1 x" by simp
   37.40    qed
   37.41    show "f2 = g2" proof
   37.42      fix y :: 'b
   37.43 -    from a have "sum_case f1 f2 (Inr y) = sum_case g1 g2 (Inr y)" by simp
   37.44 +    from a have "case_sum f1 f2 (Inr y) = case_sum g1 g2 (Inr y)" by simp
   37.45      then show "f2 y = g2 y" by simp
   37.46    qed
   37.47  qed
    38.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Wed Feb 12 08:35:56 2014 +0100
    38.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Wed Feb 12 08:35:57 2014 +0100
    38.3 @@ -265,7 +265,7 @@
    38.4            rtac (thm RS ord_eq_le_trans) THEN' etac @{thm subset_trans[OF image_mono Un_upper1]})
    38.5          set_maps,
    38.6          rtac sym,
    38.7 -        rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF sum_case_o_inj(1)]},
    38.8 +        rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]},
    38.9             map_comp RS sym, map_id])] 1
   38.10    end;
   38.11  
    39.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
    39.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:57 2014 +0100
    39.3 @@ -541,7 +541,7 @@
    39.4      fun generate_iter pre (_, _, fss, xssss) ctor_iter =
    39.5        (mk_binding pre,
    39.6         fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_iter,
    39.7 -         map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss)));
    39.8 +         map2 (mk_case_sumN_balanced oo map2 mk_uncurried2_fun) fss xssss)));
    39.9    in
   39.10      define_co_iters Least_FP fpT Cs (map3 generate_iter iterNs iter_args_typess' ctor_iters) lthy
   39.11    end;
   39.12 @@ -867,7 +867,7 @@
   39.13  
   39.14          fun tack z_name (c, u) f =
   39.15            let val z = Free (z_name, mk_sumT (fastype_of u, fastype_of c)) in
   39.16 -            Term.lambda z (mk_sum_case (Term.lambda u u, Term.lambda c (f $ c)) $ z)
   39.17 +            Term.lambda z (mk_case_sum (Term.lambda u u, Term.lambda c (f $ c)) $ z)
   39.18            end;
   39.19  
   39.20          fun build_coiter fcoiters maybe_mk_sumT maybe_tack cqf =
   39.21 @@ -902,7 +902,7 @@
   39.22          val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
   39.23          val corec_thmss =
   39.24            map2 (map2 prove) corec_goalss corec_tacss
   39.25 -          |> map (map (unfold_thms lthy @{thms sum_case_if}));
   39.26 +          |> map (map (unfold_thms lthy @{thms case_sum_if}));
   39.27        in
   39.28          (unfold_thmss, corec_thmss)
   39.29        end;
    40.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Feb 12 08:35:56 2014 +0100
    40.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Feb 12 08:35:57 2014 +0100
    40.3 @@ -84,8 +84,8 @@
    40.4    unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN HEADGOAL (rtac refl);
    40.5  
    40.6  val iter_unfold_thms =
    40.7 -  @{thms comp_def convol_def fst_conv id_def prod_case_Pair_iden snd_conv
    40.8 -      split_conv unit_case_Unity} @ sum_prod_thms_map;
    40.9 +  @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv
   40.10 +      case_unit_Unity} @ sum_prod_thms_map;
   40.11  
   40.12  fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter ctr_def ctxt =
   40.13    unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_idents @
    41.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Feb 12 08:35:56 2014 +0100
    41.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Feb 12 08:35:57 2014 +0100
    41.3 @@ -69,7 +69,7 @@
    41.4      val dest_co_algT = co_swap o dest_funT;
    41.5      val co_alg_argT = fp_case fp range_type domain_type;
    41.6      val co_alg_funT = fp_case fp domain_type range_type;
    41.7 -    val mk_co_product = curry (fp_case fp mk_convol mk_sum_case);
    41.8 +    val mk_co_product = curry (fp_case fp mk_convol mk_case_sum);
    41.9      val mk_map_co_product = fp_case fp mk_prod_map mk_sum_map;
   41.10      val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
   41.11      val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
   41.12 @@ -336,7 +336,7 @@
   41.13            o_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
   41.14          val rec_thms = fold_thms @ fp_case fp
   41.15            @{thms fst_convol map_pair_o_convol convol_o}
   41.16 -          @{thms sum_case_o_inj(1) sum_case_o_sum_map o_sum_case};
   41.17 +          @{thms case_sum_o_inj(1) case_sum_o_sum_map o_case_sum};
   41.18          val map_thms = no_refl (maps (fn bnf =>
   41.19            [map_comp0_of_bnf bnf RS sym, map_id0_of_bnf bnf]) fp_nesty_bnfs);
   41.20  
    42.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
    42.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 08:35:57 2014 +0100
    42.3 @@ -64,7 +64,7 @@
    42.4  
    42.5  fun unfold_lets_splits (Const (@{const_name Let}, _) $ arg1 $ arg2) =
    42.6      unfold_lets_splits (betapply (arg2, arg1))
    42.7 -  | unfold_lets_splits (t as Const (@{const_name prod_case}, _) $ u) =
    42.8 +  | unfold_lets_splits (t as Const (@{const_name case_prod}, _) $ u) =
    42.9      (case unfold_lets_splits u of
   42.10        u' as Abs (s1, T1, Abs (s2, T2, _)) =>
   42.11        let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in
    43.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Feb 12 08:35:56 2014 +0100
    43.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Feb 12 08:35:57 2014 +0100
    43.3 @@ -144,13 +144,13 @@
    43.4    val Inl_const: typ -> typ -> term
    43.5    val Inr_const: typ -> typ -> term
    43.6  
    43.7 +  val mk_case_sum: term * term -> term
    43.8 +  val mk_case_sumN: term list -> term
    43.9 +  val mk_case_sumN_balanced: term list -> term
   43.10    val mk_Inl: typ -> term -> term
   43.11    val mk_Inr: typ -> term -> term
   43.12    val mk_InN: typ list -> term -> int -> term
   43.13    val mk_InN_balanced: typ -> int -> term -> int -> term
   43.14 -  val mk_sum_case: term * term -> term
   43.15 -  val mk_sum_caseN: term list -> term
   43.16 -  val mk_sum_caseN_balanced: term list -> term
   43.17  
   43.18    val dest_sumT: typ -> typ * typ
   43.19    val dest_sumTN: int -> typ -> typ list
   43.20 @@ -166,8 +166,8 @@
   43.21    val mk_sumEN: int -> thm
   43.22    val mk_sumEN_balanced: int -> thm
   43.23    val mk_sumEN_tupled_balanced: int list -> thm
   43.24 -  val mk_sum_casesN: int -> int -> thm
   43.25 -  val mk_sum_casesN_balanced: int -> int -> thm
   43.26 +  val mk_sum_caseN: int -> int -> thm
   43.27 +  val mk_sum_caseN_balanced: int -> int -> thm
   43.28  
   43.29    val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
   43.30  
   43.31 @@ -409,17 +409,17 @@
   43.32      |> repair_types sum_T
   43.33    end;
   43.34  
   43.35 -fun mk_sum_case (f, g) =
   43.36 +fun mk_case_sum (f, g) =
   43.37    let
   43.38      val fT = fastype_of f;
   43.39      val gT = fastype_of g;
   43.40    in
   43.41 -    Const (@{const_name sum_case},
   43.42 +    Const (@{const_name case_sum},
   43.43        fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g
   43.44    end;
   43.45  
   43.46 -val mk_sum_caseN = Library.foldr1 mk_sum_case;
   43.47 -val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case;
   43.48 +val mk_case_sumN = Library.foldr1 mk_case_sum;
   43.49 +val mk_case_sumN_balanced = Balanced_Tree.make mk_case_sum;
   43.50  
   43.51  fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
   43.52  fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end;
   43.53 @@ -470,18 +470,18 @@
   43.54      else mk_sumEN_balanced' n (map mk_tupled_allIN ms)
   43.55    end;
   43.56  
   43.57 -fun mk_sum_casesN 1 1 = refl
   43.58 -  | mk_sum_casesN _ 1 = @{thm sum.cases(1)}
   43.59 -  | mk_sum_casesN 2 2 = @{thm sum.cases(2)}
   43.60 -  | mk_sum_casesN n k = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (k - 1)];
   43.61 +fun mk_sum_caseN 1 1 = refl
   43.62 +  | mk_sum_caseN _ 1 = @{thm sum.case(1)}
   43.63 +  | mk_sum_caseN 2 2 = @{thm sum.case(2)}
   43.64 +  | mk_sum_caseN n k = trans OF [@{thm case_sum_step(2)}, mk_sum_caseN (n - 1) (k - 1)];
   43.65  
   43.66  fun mk_sum_step base step thm =
   43.67    if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm];
   43.68  
   43.69 -fun mk_sum_casesN_balanced 1 1 = refl
   43.70 -  | mk_sum_casesN_balanced n k =
   43.71 -    Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)},
   43.72 -      right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k;
   43.73 +fun mk_sum_caseN_balanced 1 1 = refl
   43.74 +  | mk_sum_caseN_balanced n k =
   43.75 +    Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm case_sum_step(1)},
   43.76 +      right = mk_sum_step @{thm sum.cases(2)} @{thm case_sum_step(2)}, init = refl} n k;
   43.77  
   43.78  fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
   43.79    let
   43.80 @@ -532,11 +532,11 @@
   43.81      val rewrite_comp_comp = fp_case fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp};
   43.82      val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
   43.83      val map_cong_active_args1 = replicate n (if is_rec
   43.84 -      then fp_case fp @{thm convol_o} @{thm o_sum_case} RS fun_cong
   43.85 +      then fp_case fp @{thm convol_o} @{thm o_case_sum} RS fun_cong
   43.86        else refl);
   43.87      val map_cong_passive_args2 = replicate m (fp_case fp @{thm comp_id} @{thm id_comp} RS fun_cong);
   43.88      val map_cong_active_args2 = replicate n (if is_rec
   43.89 -      then fp_case fp @{thm map_pair_o_convol_id} @{thm sum_case_o_sum_map_id}
   43.90 +      then fp_case fp @{thm map_pair_o_convol_id} @{thm case_sum_o_sum_map_id}
   43.91        else fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
   43.92      fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
   43.93      val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
    44.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:56 2014 +0100
    44.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:57 2014 +0100
    44.3 @@ -493,16 +493,16 @@
    44.4          |> Thm.close_derivation
    44.5        end;
    44.6  
    44.7 -    val mor_sum_case_thm =
    44.8 +    val mor_case_sum_thm =
    44.9        let
   44.10          val maps = map3 (fn s => fn sum_s => fn mapx =>
   44.11 -          mk_sum_case (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s))
   44.12 +          mk_case_sum (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s))
   44.13            s's sum_ss map_Inls;
   44.14        in
   44.15          Goal.prove_sorry lthy [] []
   44.16            (fold_rev Logic.all (s's @ sum_ss) (HOLogic.mk_Trueprop
   44.17              (mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls)))
   44.18 -          (K (mk_mor_sum_case_tac ks mor_UNIV_thm))
   44.19 +          (K (mk_mor_case_sum_tac ks mor_UNIV_thm))
   44.20          |> Thm.close_derivation
   44.21        end;
   44.22  
   44.23 @@ -1133,7 +1133,7 @@
   44.24          val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2);
   44.25        in
   44.26          HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
   44.27 -          (mk_sum_caseN fs $ (lab $ HOLogic.mk_list sum_sbdT []))))
   44.28 +          (mk_case_sumN fs $ (lab $ HOLogic.mk_list sum_sbdT []))))
   44.29        end;
   44.30  
   44.31      val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
   44.32 @@ -1239,7 +1239,7 @@
   44.33              fun mk_case i' =
   44.34                Term.absfree k' (mk_nthN n rv_rec i' $ (mk_from_sbd s b i i' $ k));
   44.35            in
   44.36 -            Term.absfree b' (mk_sum_caseN (map mk_case ks) $ sumx)
   44.37 +            Term.absfree b' (mk_case_sumN (map mk_case ks) $ sumx)
   44.38            end;
   44.39  
   44.40          val Cons = Term.absfree sumx' (Term.absdummy sum_sbd_listT (Term.absfree rv_rec'
   44.41 @@ -1285,7 +1285,7 @@
   44.42  
   44.43          val Lab = Term.absfree kl' (mk_If
   44.44            (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z))
   44.45 -          (mk_sum_caseN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z))
   44.46 +          (mk_case_sumN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z))
   44.47            (mk_undefined sbdFT));
   44.48  
   44.49          val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
   44.50 @@ -1413,7 +1413,7 @@
   44.51  
   44.52          fun mk_conjunct i z B = HOLogic.mk_imp
   44.53            (HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), HOLogic.mk_mem (z, B)),
   44.54 -          mk_sum_caseN (map4 mk_case ss setssAs zs zs') $ (mk_rv ss kl i $ z));
   44.55 +          mk_case_sumN (map4 mk_case ss setssAs zs zs') $ (mk_rv ss kl i $ z));
   44.56  
   44.57          val goal = list_all_free (kl :: zs)
   44.58            (Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct ks zs Bs));
   44.59 @@ -1433,7 +1433,7 @@
   44.60            split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
   44.61              else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
   44.62                (2, @{thm sum.weak_case_cong} RS iffD1) RS
   44.63 -              (mk_sum_casesN n i' RS iffD1))) ks) ks
   44.64 +              (mk_case_sumN n i' RS iffD1))) ks) ks
   44.65        end;
   44.66  
   44.67      val set_Lev_thmsss =
   44.68 @@ -1828,7 +1828,7 @@
   44.69  
   44.70      val corec_Inl_sum_thms =
   44.71        let
   44.72 -        val mor = mor_comp_thm OF [mor_sum_case_thm, mor_unfold_thm];
   44.73 +        val mor = mor_comp_thm OF [mor_case_sum_thm, mor_unfold_thm];
   44.74        in
   44.75          map2 (fn unique => fn unfold_dtor =>
   44.76            trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms
   44.77 @@ -1839,7 +1839,7 @@
   44.78  
   44.79      val corec_strs =
   44.80        map3 (fn dtor => fn sum_s => fn mapx =>
   44.81 -        mk_sum_case
   44.82 +        mk_case_sum
   44.83            (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s))
   44.84        dtors corec_ss corec_maps;
   44.85  
   44.86 @@ -1863,14 +1863,14 @@
   44.87      val corec_defs = map (fn def =>
   44.88        mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) corec_def_frees;
   44.89  
   44.90 -    val sum_cases =
   44.91 -      map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
   44.92 +    val case_sums =
   44.93 +      map2 (fn T => fn i => mk_case_sum (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
   44.94      val dtor_corec_thms =
   44.95        let
   44.96          fun mk_goal i corec_s corec_map dtor z =
   44.97            let
   44.98              val lhs = dtor $ (mk_corec corec_ss i $ z);
   44.99 -            val rhs = Term.list_comb (corec_map, passive_ids @ sum_cases) $ (corec_s $ z);
  44.100 +            val rhs = Term.list_comb (corec_map, passive_ids @ case_sums) $ (corec_s $ z);
  44.101            in
  44.102              fold_rev Logic.all (z :: corec_ss) (mk_Trueprop_eq (lhs, rhs))
  44.103            end;
  44.104 @@ -1886,7 +1886,7 @@
  44.105  
  44.106      val corec_unique_mor_thm =
  44.107        let
  44.108 -        val id_fs = map2 (fn T => fn f => mk_sum_case (HOLogic.id_const T, f)) Ts unfold_fs;
  44.109 +        val id_fs = map2 (fn T => fn f => mk_case_sum (HOLogic.id_const T, f)) Ts unfold_fs;
  44.110          val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs corec_strs UNIVs dtors id_fs);
  44.111          fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i);
  44.112          val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  44.113 @@ -1907,9 +1907,9 @@
  44.114      val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
  44.115        `split_conj_thm (split_conj_prems n
  44.116          (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
  44.117 -        |> Local_Defs.unfold lthy (@{thms o_sum_case comp_id id_comp comp_assoc[symmetric]
  44.118 -           sum_case_o_inj(1)} @ map_id0s_o_id @ sym_map_comps)
  44.119 -        OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
  44.120 +        |> Local_Defs.unfold lthy (@{thms o_case_sum comp_id id_comp comp_assoc[symmetric]
  44.121 +           case_sum_o_inj(1)} @ map_id0s_o_id @ sym_map_comps)
  44.122 +        OF replicate n @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]});
  44.123  
  44.124      val timer = time (timer "corec definitions & thms");
  44.125  
    45.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
    45.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Feb 12 08:35:57 2014 +0100
    45.3 @@ -195,7 +195,7 @@
    45.4            let val branches' = map (massage_rec bound_Ts) branches in
    45.5              Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
    45.6            end
    45.7 -        | (c as Const (@{const_name prod_case}, _), arg :: args) =>
    45.8 +        | (c as Const (@{const_name case_prod}, _), arg :: args) =>
    45.9            massage_rec bound_Ts
   45.10              (unfold_lets_splits (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
   45.11          | (Const (c, _), args as _ :: _ :: _) =>
   45.12 @@ -295,12 +295,12 @@
   45.13                end
   45.14              | NONE =>
   45.15                (case t of
   45.16 -                Const (@{const_name prod_case}, _) $ t' =>
   45.17 +                Const (@{const_name case_prod}, _) $ t' =>
   45.18                  let
   45.19                    val U' = curried_type U;
   45.20                    val T' = curried_type T;
   45.21                  in
   45.22 -                  Const (@{const_name prod_case}, U' --> U) $ massage_call bound_Ts U' T' t'
   45.23 +                  Const (@{const_name case_prod}, U' --> U) $ massage_call bound_Ts U' T' t'
   45.24                  end
   45.25                | t1 $ t2 =>
   45.26                  (if has_call t2 then
   45.27 @@ -771,7 +771,7 @@
   45.28                let val (u, vs) = strip_comb t in
   45.29                  if is_Free u andalso has_call u then
   45.30                    Inr_const U T $ mk_tuple1 bound_Ts vs
   45.31 -                else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
   45.32 +                else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
   45.33                    map (rewrite bound_Ts) vs |> chop 1
   45.34                    |>> HOLogic.mk_split o the_single
   45.35                    |> Term.list_comb
    46.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Feb 12 08:35:56 2014 +0100
    46.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Feb 12 08:35:57 2014 +0100
    46.3 @@ -57,13 +57,13 @@
    46.4      thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
    46.5      thm list list list -> thm list list list -> thm list list -> thm list list -> thm list ->
    46.6      thm list -> thm list -> tactic
    46.7 +  val mk_mor_case_sum_tac: 'a list -> thm -> tactic
    46.8    val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
    46.9    val mk_mor_elim_tac: thm -> tactic
   46.10    val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
   46.11      thm list -> thm list list -> thm list list -> tactic
   46.12    val mk_mor_incl_tac: thm -> thm list -> tactic
   46.13    val mk_mor_str_tac: 'a list -> thm -> tactic
   46.14 -  val mk_mor_sum_case_tac: 'a list -> thm -> tactic
   46.15    val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
   46.16      thm list -> tactic
   46.17    val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
   46.18 @@ -170,8 +170,8 @@
   46.19  fun mk_mor_str_tac ks mor_UNIV =
   46.20    (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac refl)) ks) 1;
   46.21  
   46.22 -fun mk_mor_sum_case_tac ks mor_UNIV =
   46.23 -  (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm sum_case_o_inj(1)[symmetric]})) ks) 1;
   46.24 +fun mk_mor_case_sum_tac ks mor_UNIV =
   46.25 +  (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm case_sum_o_inj(1)[symmetric]})) ks) 1;
   46.26  
   46.27  fun mk_set_incl_hset_tac def rec_Suc =
   46.28    EVERY' (stac def ::
   46.29 @@ -376,7 +376,7 @@
   46.30      fun coalg_tac (i, ((passive_sets, active_sets), def)) =
   46.31        EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   46.32          hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
   46.33 -        rtac (mk_sum_casesN n i), rtac CollectI,
   46.34 +        rtac (mk_sum_caseN n i), rtac CollectI,
   46.35          EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
   46.36            etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
   46.37            passive_sets),
   46.38 @@ -504,7 +504,7 @@
   46.39        CONJ_WRAP' (fn rv_Cons =>
   46.40          CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac exI,
   46.41            rtac (@{thm append_Nil} RS arg_cong RS trans),
   46.42 -          rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans), rtac rv_Nil]))
   46.43 +          rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS arg_cong RS trans), rtac rv_Nil]))
   46.44          (ks ~~ rv_Nils))
   46.45        rv_Conss,
   46.46        REPEAT_DETERM o rtac allI, rtac (mk_sumEN n),
   46.47 @@ -513,7 +513,7 @@
   46.48            CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
   46.49              rtac (@{thm append_Cons} RS arg_cong RS trans),
   46.50              rtac (rv_Cons RS trans), etac (sum_weak_case_cong RS arg_cong RS trans),
   46.51 -            rtac (mk_sum_casesN n i RS arg_cong RS trans), atac])
   46.52 +            rtac (mk_sum_caseN n i RS arg_cong RS trans), atac])
   46.53            ks])
   46.54          rv_Conss)
   46.55        ks)] 1
   46.56 @@ -530,7 +530,7 @@
   46.57          EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
   46.58            dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
   46.59            rtac (rv_Nil RS arg_cong RS iffD2),
   46.60 -          rtac (mk_sum_casesN n i RS iffD2),
   46.61 +          rtac (mk_sum_caseN n i RS iffD2),
   46.62            CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
   46.63        (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
   46.64        REPEAT_DETERM o rtac allI,
   46.65 @@ -540,7 +540,7 @@
   46.66              (fn (i, (from_to_sbd, coalg_set)) =>
   46.67                EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
   46.68                rtac (rv_Cons RS arg_cong RS iffD2),
   46.69 -              rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
   46.70 +              rtac (mk_sum_caseN n i RS arg_cong RS trans RS iffD2),
   46.71                etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
   46.72                dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
   46.73                etac coalg_set, atac])
   46.74 @@ -583,7 +583,7 @@
   46.75                        rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnIN n i),
   46.76                        rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
   46.77                        rtac conjI, atac, dtac (sym RS trans RS sym),
   46.78 -                      rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS trans),
   46.79 +                      rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS trans),
   46.80                        etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
   46.81                        dtac (mk_conjunctN n i), dtac mp, atac,
   46.82                        dtac (mk_conjunctN n i'), dtac mp, atac,
   46.83 @@ -639,7 +639,7 @@
   46.84                      atac, atac, hyp_subst_tac ctxt] THEN'
   46.85                      CONJ_WRAP' (fn i'' =>
   46.86                        EVERY' [rtac impI, dtac (sym RS trans),
   46.87 -                        rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans),
   46.88 +                        rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS arg_cong RS trans),
   46.89                          etac (from_to_sbd RS arg_cong),
   46.90                          REPEAT_DETERM o etac allE,
   46.91                          dtac (mk_conjunctN n i), dtac mp, atac,
   46.92 @@ -684,7 +684,7 @@
   46.93                rtac exI, rtac conjI,
   46.94                (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
   46.95                else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
   46.96 -                etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
   46.97 +                etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)),
   46.98                EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
   46.99                  EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
  46.100                    rtac trans_fun_cong_image_id_id_apply,
  46.101 @@ -708,7 +708,7 @@
  46.102                rtac exI, rtac conjI,
  46.103                (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
  46.104                else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
  46.105 -                etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
  46.106 +                etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)),
  46.107                EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
  46.108                  EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
  46.109                    rtac trans_fun_cong_image_id_id_apply,
  46.110 @@ -735,7 +735,7 @@
  46.111            rtac length_Lev', rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI},
  46.112            CONVERSION (Conv.top_conv
  46.113              (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
  46.114 -          if n = 1 then rtac refl else rtac (mk_sum_casesN n i),
  46.115 +          if n = 1 then rtac refl else rtac (mk_sum_caseN n i),
  46.116            EVERY' (map2 (fn set_map0 => fn coalg_set =>
  46.117              EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
  46.118                rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])
  46.119 @@ -763,7 +763,7 @@
  46.120            (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
  46.121          if n = 1 then K all_tac
  46.122          else (rtac (sum_weak_case_cong RS trans) THEN'
  46.123 -          rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
  46.124 +          rtac (mk_sum_caseN n i) THEN' rtac (mk_sum_caseN n i RS trans)),
  46.125          rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
  46.126          EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
  46.127            DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
  46.128 @@ -800,7 +800,7 @@
  46.129              CONVERSION (Conv.top_conv
  46.130                (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
  46.131              if n = 1 then K all_tac
  46.132 -            else rtac sum_weak_case_cong THEN' rtac (mk_sum_casesN n i' RS trans),
  46.133 +            else rtac sum_weak_case_cong THEN' rtac (mk_sum_caseN n i' RS trans),
  46.134              SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,
  46.135              rtac refl])
  46.136          ks to_sbd_injs from_to_sbds)];
  46.137 @@ -927,11 +927,11 @@
  46.138    unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
  46.139      rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
  46.140      REPEAT_DETERM_N m o rtac refl,
  46.141 -    EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
  46.142 +    EVERY' (map (fn thm => rtac @{thm case_sum_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
  46.143  
  46.144  fun mk_corec_unique_mor_tac ctxt corec_defs corec_Inls unfold_unique_mor =
  46.145    unfold_thms_tac ctxt
  46.146 -    (corec_defs @ map (fn thm => thm RS @{thm sum_case_expand_Inr'}) corec_Inls) THEN
  46.147 +    (corec_defs @ map (fn thm => thm RS @{thm case_sum_expand_Inr'}) corec_Inls) THEN
  46.148    etac unfold_unique_mor 1;
  46.149  
  46.150  fun mk_dtor_coinduct_tac m raw_coind bis_rel rel_congs =
  46.151 @@ -946,7 +946,7 @@
  46.152      rel_congs,
  46.153      rtac impI, REPEAT_DETERM o etac conjE,
  46.154      CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
  46.155 -      rtac CollectI, etac @{thm prod_caseI}])) rel_congs] 1;
  46.156 +      rtac CollectI, etac @{thm case_prodI}])) rel_congs] 1;
  46.157  
  46.158  fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def =
  46.159    let
  46.160 @@ -1140,7 +1140,7 @@
  46.161          passive_set_map0s dtor_set_incls),
  46.162          CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) =>
  46.163            EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI,
  46.164 -            rtac @{thm prod_caseI}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  46.165 +            rtac @{thm case_prodI}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  46.166              CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
  46.167              rtac conjI, rtac refl, rtac refl])
  46.168          (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
  46.169 @@ -1164,7 +1164,7 @@
  46.170                  dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
  46.171                  dtac @{thm ssubst_mem[OF pair_collapse]},
  46.172                  REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
  46.173 -                  @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
  46.174 +                  @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
  46.175                  hyp_subst_tac ctxt,
  46.176                  dtac (in_Jrel RS iffD1),
  46.177                  dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
  46.178 @@ -1180,7 +1180,7 @@
  46.179            EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
  46.180              dtac @{thm ssubst_mem[OF pair_collapse]},
  46.181              REPEAT_DETERM o
  46.182 -              eresolve_tac (CollectE :: conjE :: @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
  46.183 +              eresolve_tac (CollectE :: conjE :: @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
  46.184              hyp_subst_tac ctxt, dtac (in_Jrel RS iffD1),
  46.185              dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jrels),
  46.186            atac]]
    47.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Feb 12 08:35:56 2014 +0100
    47.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Feb 12 08:35:57 2014 +0100
    47.3 @@ -724,7 +724,7 @@
    47.4          passive_set_map0s ctor_set_incls),
    47.5          CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) =>
    47.6            EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI,
    47.7 -            rtac @{thm prod_caseI}, rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
    47.8 +            rtac @{thm case_prodI}, rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
    47.9              CONJ_WRAP' (fn thm =>
   47.10                EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor]))
   47.11              ctor_set_set_incls,
   47.12 @@ -750,7 +750,7 @@
   47.13                  dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
   47.14                  dtac @{thm ssubst_mem[OF pair_collapse]},
   47.15                  REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
   47.16 -                  @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
   47.17 +                  @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
   47.18                  hyp_subst_tac ctxt,
   47.19                  dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
   47.20                  TRY o
   47.21 @@ -765,7 +765,7 @@
   47.22            EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
   47.23              dtac @{thm ssubst_mem[OF pair_collapse]},
   47.24              REPEAT_DETERM o
   47.25 -              eresolve_tac (CollectE :: conjE :: @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
   47.26 +              eresolve_tac (CollectE :: conjE :: @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
   47.27              hyp_subst_tac ctxt,
   47.28              dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac])
   47.29            in_Irels),
    48.1 --- a/src/HOL/Tools/Function/sum_tree.ML	Wed Feb 12 08:35:56 2014 +0100
    48.2 +++ b/src/HOL/Tools/Function/sum_tree.ML	Wed Feb 12 08:35:57 2014 +0100
    48.3 @@ -32,8 +32,7 @@
    48.4  (* Sum types *)
    48.5  fun mk_sumT LT RT = Type (@{type_name Sum_Type.sum}, [LT, RT])
    48.6  fun mk_sumcase TL TR T l r =
    48.7 -  Const (@{const_name sum.sum_case},
    48.8 -    (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
    48.9 +  Const (@{const_name sum.case_sum}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
   48.10  
   48.11  val App = curry op $
   48.12  
    49.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 12 08:35:56 2014 +0100
    49.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 12 08:35:57 2014 +0100
    49.3 @@ -2267,7 +2267,7 @@
    49.4        HOLogic.Collect_const tuple_T $ list_comb (Const base_x, outer_bounds)
    49.5      val step_set =
    49.6        HOLogic.Collect_const prod_T
    49.7 -      $ (Const (@{const_name prod_case}, curried_T --> uncurried_T)
    49.8 +      $ (Const (@{const_name case_prod}, curried_T --> uncurried_T)
    49.9                  $ list_comb (Const step_x, outer_bounds))
   49.10      val image_set =
   49.11        image_const $ (rtrancl_const $ step_set) $ base_set
    50.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 12 08:35:56 2014 +0100
    50.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 12 08:35:57 2014 +0100
    50.3 @@ -992,7 +992,7 @@
    50.4  
    50.5  (* Definition of executable functions and their intro and elim rules *)
    50.6  
    50.7 -fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
    50.8 +fun strip_split_abs (Const (@{const_name case_prod}, _) $ t) = strip_split_abs t
    50.9    | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
   50.10    | strip_split_abs t = t
   50.11  
    51.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Feb 12 08:35:56 2014 +0100
    51.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Feb 12 08:35:57 2014 +0100
    51.3 @@ -312,7 +312,7 @@
    51.4      fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
    51.5        liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    51.6      fun mk_split T = Sign.mk_const thy
    51.7 -      (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
    51.8 +      (@{const_name case_prod}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
    51.9      fun mk_scomp_split T t t' =
   51.10        mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
   51.11          (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
   51.12 @@ -358,7 +358,7 @@
   51.13      fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
   51.14        liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   51.15      fun mk_split T = Sign.mk_const thy
   51.16 -      (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
   51.17 +      (@{const_name case_prod}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
   51.18      fun mk_scomp_split T t t' =
   51.19        mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
   51.20          (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
    52.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Wed Feb 12 08:35:56 2014 +0100
    52.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Wed Feb 12 08:35:57 2014 +0100
    52.3 @@ -635,12 +635,12 @@
    52.4            end
    52.5        end
    52.6  
    52.7 -  | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
    52.8 -     ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
    52.9 +  | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
   52.10 +     ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
   52.11         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
   52.12  
   52.13 -  | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)),
   52.14 -     ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) =>
   52.15 +  | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, s1)),
   52.16 +     ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , s2))) =>
   52.17         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
   52.18  
   52.19    | (t1 $ t2, t1' $ t2') =>
    53.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Feb 12 08:35:56 2014 +0100
    53.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Feb 12 08:35:57 2014 +0100
    53.3 @@ -356,22 +356,22 @@
    53.4  (** rewrite bool case expressions as if expressions **)
    53.5  
    53.6  local
    53.7 -  fun is_bool_case (Const (@{const_name "bool.bool_case"}, _)) = true
    53.8 -    | is_bool_case _ = false
    53.9 +  fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true
   53.10 +    | is_case_bool _ = false
   53.11  
   53.12    val thm = mk_meta_eq @{lemma
   53.13 -    "bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp}
   53.14 +    "case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp}
   53.15  
   53.16    fun unfold_conv _ =
   53.17 -    SMT_Utils.if_true_conv (is_bool_case o Term.head_of)
   53.18 +    SMT_Utils.if_true_conv (is_case_bool o Term.head_of)
   53.19        (expand_head_conv (Conv.rewr_conv thm))
   53.20  in
   53.21  
   53.22 -fun rewrite_bool_case_conv ctxt =
   53.23 -  SMT_Utils.if_exists_conv is_bool_case (Conv.top_conv unfold_conv ctxt)
   53.24 +fun rewrite_case_bool_conv ctxt =
   53.25 +  SMT_Utils.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
   53.26  
   53.27 -val setup_bool_case =
   53.28 -  SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
   53.29 +val setup_case_bool =
   53.30 +  SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
   53.31  
   53.32  end
   53.33  
   53.34 @@ -558,7 +558,7 @@
   53.35  (** combined unfoldings and rewritings **)
   53.36  
   53.37  fun unfold_conv ctxt =
   53.38 -  rewrite_bool_case_conv ctxt then_conv
   53.39 +  rewrite_case_bool_conv ctxt then_conv
   53.40    unfold_abs_min_max_conv ctxt then_conv
   53.41    nat_as_int_conv ctxt then_conv
   53.42    Thm.beta_conversion true
   53.43 @@ -645,7 +645,7 @@
   53.44    setup_unfolded_quants #>
   53.45    setup_trigger #>
   53.46    setup_weight #>
   53.47 -  setup_bool_case #>
   53.48 +  setup_case_bool #>
   53.49    setup_abs_min_max #>
   53.50    setup_nat_as_int)
   53.51  
    54.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Wed Feb 12 08:35:56 2014 +0100
    54.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Wed Feb 12 08:35:57 2014 +0100
    54.3 @@ -196,7 +196,7 @@
    54.4  
    54.5  local
    54.6  fun mk_uncurry (xt, yt, zt) =
    54.7 -    Const(@{const_name prod_case}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
    54.8 +    Const(@{const_name case_prod}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
    54.9  fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
   54.10    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
   54.11  fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
   54.12 @@ -276,7 +276,7 @@
   54.13    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
   54.14  
   54.15  
   54.16 -local  fun ucheck t = (if #Name (dest_const t) = @{const_name prod_case} then t
   54.17 +local  fun ucheck t = (if #Name (dest_const t) = @{const_name case_prod} then t
   54.18                         else raise Match)
   54.19  in
   54.20  fun dest_pabs used tm =
    55.1 --- a/src/HOL/Tools/hologic.ML	Wed Feb 12 08:35:56 2014 +0100
    55.2 +++ b/src/HOL/Tools/hologic.ML	Wed Feb 12 08:35:57 2014 +0100
    55.3 @@ -357,12 +357,12 @@
    55.4    end;
    55.5  
    55.6  fun split_const (A, B, C) =
    55.7 -  Const ("Product_Type.prod.prod_case", (A --> B --> C) --> mk_prodT (A, B) --> C);
    55.8 +  Const ("Product_Type.prod.case_prod", (A --> B --> C) --> mk_prodT (A, B) --> C);
    55.9  
   55.10  fun mk_split t =
   55.11    (case Term.fastype_of t of
   55.12      T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
   55.13 -      Const ("Product_Type.prod.prod_case", T --> mk_prodT (A, B) --> C) $ t
   55.14 +      Const ("Product_Type.prod.case_prod", T --> mk_prodT (A, B) --> C) $ t
   55.15    | _ => raise TERM ("mk_split: bad body type", [t]));
   55.16  
   55.17  (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
   55.18 @@ -478,7 +478,7 @@
   55.19  val strip_psplits =
   55.20    let
   55.21      fun strip [] qs Ts t = (t, rev Ts, qs)
   55.22 -      | strip (p :: ps) qs Ts (Const ("Product_Type.prod.prod_case", _) $ t) =
   55.23 +      | strip (p :: ps) qs Ts (Const ("Product_Type.prod.case_prod", _) $ t) =
   55.24            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
   55.25        | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
   55.26        | strip (p :: ps) qs Ts t = strip ps qs
    56.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Feb 12 08:35:56 2014 +0100
    56.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Feb 12 08:35:57 2014 +0100
    56.3 @@ -84,7 +84,7 @@
    56.4    end;
    56.5  
    56.6  fun mk_split_abs vs (Bound i) t = let val (x, T) = nth vs i in Abs (x, T, t) end
    56.7 -  | mk_split_abs vs (Const ("Product_Type.Pair", _) $ u $ v) t =
    56.8 +  | mk_split_abs vs (Const (@{const_name Product_Type.Pair}, _) $ u $ v) t =
    56.9        HOLogic.mk_split (mk_split_abs vs u (mk_split_abs vs v t))
   56.10    | mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]);
   56.11  
   56.12 @@ -92,7 +92,7 @@
   56.13  val strip_psplits =
   56.14    let
   56.15      fun strip [] qs vs t = (t, rev vs, qs)
   56.16 -      | strip (p :: ps) qs vs (Const ("Product_Type.prod.prod_case", _) $ t) =
   56.17 +      | strip (p :: ps) qs vs (Const (@{const_name Product_Type.prod.case_prod}, _) $ t) =
   56.18            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t
   56.19        | strip (_ :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t
   56.20        | strip (_ :: ps) qs vs t = strip ps qs
   56.21 @@ -305,7 +305,7 @@
   56.22  
   56.23  (* proof tactic *)
   56.24  
   56.25 -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)}
   56.26 +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)}
   56.27  
   56.28  val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp}
   56.29  val vimageE' =
   56.30 @@ -326,7 +326,7 @@
   56.31          @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]}
   56.32        ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
   56.33          (HOLogic.Trueprop_conv
   56.34 -          (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq prod_case_distrib)))))) ctxt)))
   56.35 +          (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_distrib)))))) ctxt)))
   56.36  
   56.37  fun elim_image_tac ctxt = etac @{thm imageE}
   56.38    THEN' REPEAT_DETERM o CHANGED o
   56.39 @@ -521,4 +521,3 @@
   56.40    end;
   56.41  
   56.42  end;
   56.43 -
    57.1 --- a/src/HOL/ex/Tree23.thy	Wed Feb 12 08:35:56 2014 +0100
    57.2 +++ b/src/HOL/ex/Tree23.thy	Wed Feb 12 08:35:57 2014 +0100
    57.3 @@ -332,8 +332,8 @@
    57.4  lemmas dfull_case_intros =
    57.5    ord.exhaust [where y=y and P="dfull a (ord_case b c d y)"]
    57.6    option.exhaust [of y "dfull a (case_option b c y)"]
    57.7 -  prod.exhaust [where y=y and P="dfull a (prod_case b y)"]
    57.8 -  bool.exhaust [where y=y and P="dfull a (bool_case b c y)"]
    57.9 +  prod.exhaust [of y "dfull a (case_prod b y)"]
   57.10 +  bool.exhaust [of y "dfull a (case_bool b c y)"]
   57.11    tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))"]
   57.12    tree23.exhaust [where y=y and P="full a (tree23_case b c d y)"]
   57.13    for a b c d e y