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)
```