src/HOL/Library/Polynomial.thy
 changeset 55415 05f5fdb8d093 parent 54856 356b4c0a2061 child 55417 01fbfb60c33e
```     1.1 --- a/src/HOL/Library/Polynomial.thy	Wed Feb 12 08:35:57 2014 +0100
1.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Feb 12 08:35:57 2014 +0100
1.3 @@ -145,9 +145,9 @@
1.4    with that show thesis .
1.5  qed
1.6
1.7 -lemma almost_everywhere_zero_nat_case:
1.8 +lemma almost_everywhere_zero_case_nat:
1.9    assumes "almost_everywhere_zero f"
1.10 -  shows "almost_everywhere_zero (nat_case a f)"
1.11 +  shows "almost_everywhere_zero (case_nat a f)"
1.12    using assms
1.13    by (auto intro!: almost_everywhere_zeroI elim!: almost_everywhere_zeroE split: nat.split)
1.14      blast
1.15 @@ -258,8 +258,8 @@
1.16  subsection {* List-style constructor for polynomials *}
1.17
1.18  lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
1.19 -  is "\<lambda>a p. nat_case a (coeff p)"
1.20 -  using coeff_almost_everywhere_zero by (rule almost_everywhere_zero_nat_case)
1.21 +  is "\<lambda>a p. case_nat a (coeff p)"
1.22 +  using coeff_almost_everywhere_zero by (rule almost_everywhere_zero_case_nat)
1.23
1.24  lemmas coeff_pCons = pCons.rep_eq
1.25
1.26 @@ -405,8 +405,8 @@
1.27  proof -
1.28    { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
1.29      assume "\<forall>m\<in>set ms. m > 0"
1.30 -    then have "map (nat_case x f) ms = map f (map (\<lambda>n. n - 1) ms)"
1.31 -      by (induct ms) (auto, metis Suc_pred' nat_case_Suc) }
1.32 +    then have "map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
1.33 +      by (induct ms) (auto, metis Suc_pred' case_nat_Suc) }
1.34    note * = this
1.35    show ?thesis
1.36      by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)
1.37 @@ -452,7 +452,7 @@
1.38  lemma coeff_Poly_eq:
1.39    "coeff (Poly xs) n = nth_default 0 xs n"
1.40    apply (induct xs arbitrary: n) apply simp_all
1.41 -  by (metis nat_case_0 nat_case_Suc not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
1.42 +  by (metis case_nat_0 case_nat_Suc not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
1.43
1.44  lemma nth_default_coeffs_eq:
1.45    "nth_default 0 (coeffs p) = coeff p"
```