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