src/HOL/Library/Polynomial.thy
changeset 58199 5fbe474b5da8
parent 57862 8f074e6e22fc
child 58513 0bf0cf1d3547
     1.1 --- a/src/HOL/Library/Polynomial.thy	Sun Sep 07 09:49:01 2014 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Sun Sep 07 09:49:05 2014 +0200
     1.3 @@ -7,86 +7,11 @@
     1.4  header {* Polynomials as type over a ring structure *}
     1.5  
     1.6  theory Polynomial
     1.7 -imports Main GCD
     1.8 +imports Main GCD "~~/src/HOL/Library/More_List"
     1.9  begin
    1.10  
    1.11  subsection {* Auxiliary: operations for lists (later) representing coefficients *}
    1.12  
    1.13 -definition strip_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.14 -where
    1.15 -  "strip_while P = rev \<circ> dropWhile P \<circ> rev"
    1.16 -
    1.17 -lemma strip_while_Nil [simp]:
    1.18 -  "strip_while P [] = []"
    1.19 -  by (simp add: strip_while_def)
    1.20 -
    1.21 -lemma strip_while_append [simp]:
    1.22 -  "\<not> P x \<Longrightarrow> strip_while P (xs @ [x]) = xs @ [x]"
    1.23 -  by (simp add: strip_while_def)
    1.24 -
    1.25 -lemma strip_while_append_rec [simp]:
    1.26 -  "P x \<Longrightarrow> strip_while P (xs @ [x]) = strip_while P xs"
    1.27 -  by (simp add: strip_while_def)
    1.28 -
    1.29 -lemma strip_while_Cons [simp]:
    1.30 -  "\<not> P x \<Longrightarrow> strip_while P (x # xs) = x # strip_while P xs"
    1.31 -  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
    1.32 -
    1.33 -lemma strip_while_eq_Nil [simp]:
    1.34 -  "strip_while P xs = [] \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
    1.35 -  by (simp add: strip_while_def)
    1.36 -
    1.37 -lemma strip_while_eq_Cons_rec:
    1.38 -  "strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))"
    1.39 -  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
    1.40 -
    1.41 -lemma strip_while_not_last [simp]:
    1.42 -  "\<not> P (last xs) \<Longrightarrow> strip_while P xs = xs"
    1.43 -  by (cases xs rule: rev_cases) simp_all
    1.44 -
    1.45 -lemma split_strip_while_append:
    1.46 -  fixes xs :: "'a list"
    1.47 -  obtains ys zs :: "'a list"
    1.48 -  where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs"
    1.49 -proof (rule that)
    1.50 -  show "strip_while P xs = strip_while P xs" ..
    1.51 -  show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
    1.52 -  have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
    1.53 -    by (simp add: strip_while_def)
    1.54 -  then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
    1.55 -    by (simp only: rev_is_rev_conv)
    1.56 -qed
    1.57 -
    1.58 -
    1.59 -definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
    1.60 -where
    1.61 -  "nth_default x xs n = (if n < length xs then xs ! n else x)"
    1.62 -
    1.63 -lemma nth_default_Nil [simp]:
    1.64 -  "nth_default y [] n = y"
    1.65 -  by (simp add: nth_default_def)
    1.66 -
    1.67 -lemma nth_default_Cons_0 [simp]:
    1.68 -  "nth_default y (x # xs) 0 = x"
    1.69 -  by (simp add: nth_default_def)
    1.70 -
    1.71 -lemma nth_default_Cons_Suc [simp]:
    1.72 -  "nth_default y (x # xs) (Suc n) = nth_default y xs n"
    1.73 -  by (simp add: nth_default_def)
    1.74 -
    1.75 -lemma nth_default_map_eq:
    1.76 -  "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
    1.77 -  by (simp add: nth_default_def)
    1.78 -
    1.79 -lemma nth_default_strip_while_eq [simp]:
    1.80 -  "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
    1.81 -proof -
    1.82 -  from split_strip_while_append obtain ys zs
    1.83 -    where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
    1.84 -  then show ?thesis by (simp add: nth_default_def not_less nth_append)
    1.85 -qed
    1.86 -
    1.87 -
    1.88  definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "##" 65)
    1.89  where
    1.90    "x ## xs = (if xs = [] \<and> x = 0 then [] else x # xs)"
    1.91 @@ -406,7 +331,8 @@
    1.92    { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
    1.93      assume "\<forall>m\<in>set ms. m > 0"
    1.94      then have "map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
    1.95 -      by (induct ms) (auto, metis Suc_pred' nat.case(2)) }
    1.96 +      by (induct ms) (auto split: nat.split)
    1.97 +  }
    1.98    note * = this
    1.99    show ?thesis
   1.100      by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)