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"