1.1 --- a/src/HOL/Library/Polynomial.thy Fri Nov 22 18:52:06 2013 +0100
1.2 +++ b/src/HOL/Library/Polynomial.thy Sat Nov 23 15:33:32 2013 +0100
1.3 @@ -7,7 +7,7 @@
1.4 header {* Polynomials as type over a ring structure *}
1.5
1.6 theory Polynomial
1.7 -imports Complex_Main GCD
1.8 +imports Complex_Main (* see (*1*)*) GCD
1.9 begin
1.10
1.11 subsection {* Auxiliary: operations for lists (later) representing coefficients *}
1.12 @@ -48,14 +48,14 @@
1.13 fixes xs :: "'a list"
1.14 obtains ys zs :: "'a list"
1.15 where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs"
1.16 -(*proof (rule that)
1.17 +proof (rule that)
1.18 show "strip_while P xs = strip_while P xs" ..
1.19 show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
1.20 have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
1.21 by (simp add: strip_while_def)
1.22 then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
1.23 by (simp only: rev_is_rev_conv)
1.24 -qed*) sorry
1.25 +qed
1.26
1.27
1.28 definition nth_default :: "'a => 'a list => nat => 'a"
1.29 @@ -86,7 +86,7 @@
1.30 then show ?thesis by (simp add: nth_default_def not_less nth_append)
1.31 qed
1.32
1.33 -
1.34 +(* ensures well-formed zero polynomial *)
1.35 definition cCons :: "'a::zero => 'a list => 'a list" (infixr "##" 65)
1.36 where
1.37 "x ## xs = (if xs = [] \<and> x = 0 then [] else x # xs)"
1.38 @@ -376,7 +376,7 @@
1.39
1.40 lemma Poly_eq_0:
1.41 "Poly as = 0 <-> (\<exists>n. as = replicate n 0)"
1.42 -(*by (induct as) (auto simp add: Cons_replicate_eq)*) sorry
1.43 + by (induct as) (auto simp add: Cons_replicate_eq)
1.44
1.45 definition coeffs :: "'a poly => 'a::zero list"
1.46 where
1.47 @@ -396,7 +396,9 @@
1.48
1.49 lemma coeffs_pCons_eq_cCons [simp]:
1.50 "coeffs (pCons a p) = a ## coeffs p"
1.51 -(*proof -
1.52 +(* fails with "imports Complex_Main"
1.53 + Complex_Main, however, is required for executable gcd (see (*1*))
1.54 + proof -
1.55 { fix ms :: "nat list" and f :: "nat => 'a" and x :: "'a"
1.56 assume "\<forall>m\<in>set ms. m > 0"
1.57 then have "map (nat_case x f) ms = map f (map (\<lambda>n. n - 1) ms)"
1.58 @@ -416,14 +418,14 @@
1.59
1.60 lemma coeffs_Poly [simp]:
1.61 "coeffs (Poly as) = strip_while (HOL.eq 0) as"
1.62 -(*proof (induct as)
1.63 +proof (induct as)
1.64 case Nil then show ?case by simp
1.65 next
1.66 case (Cons a as)
1.67 have "(\<forall>n. as \<noteq> replicate n 0) <-> (\<exists>a\<in>set as. a \<noteq> 0)"
1.68 using replicate_length_same [of as 0] by (auto dest: sym [of _ as])
1.69 with Cons show ?case by auto
1.70 -qed*) sorry
1.71 +qed
1.72
1.73 lemma last_coeffs_not_0:
1.74 "p \<noteq> 0 ==> last (coeffs p) \<noteq> 0"
1.75 @@ -468,7 +470,6 @@
1.76 lemma degree_eq_length_coeffs [code]:
1.77 "degree p = length (coeffs p) - 1"
1.78 by (simp add: coeffs_def)
1.79 -thm coeffs_def
1.80
1.81 lemma length_coeffs_degree:
1.82 "p \<noteq> 0 ==> length (coeffs p) = Suc (degree p)"
1.83 @@ -589,7 +590,7 @@
1.84
1.85 lemma fold_coeffs_monom [simp]:
1.86 "a \<noteq> 0 ==> fold_coeffs f (monom a n) = f 0 ^^ n o f a"
1.87 -(*by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff)*) sorry
1.88 + by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff)
1.89
1.90 lemma poly_monom:
1.91 fixes a x :: "'a::{comm_semiring_1}"
1.92 @@ -797,7 +798,7 @@
1.93 by (simp add: diff_minus)
1.94
1.95 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
1.96 -(*by (induct A rule: infinite_finite_induct) simp_all*) sorry
1.97 + by (induct A rule: infinite_finite_induct) simp_all
1.98
1.99
1.100 subsection {* Multiplication by a constant, polynomial multiplication and the unit polynomial *}
1.101 @@ -936,13 +937,13 @@
1.102
1.103 lemma coeff_mult:
1.104 "coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))"
1.105 -(*proof (induct p arbitrary: n)
1.106 +proof (induct p arbitrary: n)
1.107 case 0 show ?case by simp
1.108 next
1.109 case (pCons a p n) thus ?case
1.110 by (cases n, simp, simp add: setsum_atMost_Suc_shift
1.111 del: setsum_atMost_Suc)
1.112 -qed*) sorry
1.113 +qed
1.114
1.115 lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"
1.116 apply (rule degree_le)
1.117 @@ -1757,7 +1758,7 @@
1.118
1.119 value "gcd 6 (4::int)"
1.120 (*value "gcd [:1,2,3::int:] [:1,2,3::int:]"
1.121 -No type arity poly :: gcd*)
1.122 +No type arity poly :: gcd -- not yet defined for poly*)
1.123
1.124 instantiation poly :: (field) gcd
1.125 begin
1.126 @@ -1781,7 +1782,7 @@
1.127 (*value "gcd [:1,2,3::int:] [:1,2,3:]"
1.128 "Polynomial.zero_poly_inst.zero_poly" is not a constructor, on left hand side of equation, in theorem:
1.129 gcd_poly_inst.gcd_poly ?x zero_poly_inst.zero_poly \<equiv>
1.130 -smult (inverse (coeff ?x (degree ?x))) ?x*)
1.131 +smult (inverse (coeff ?x (degree ?x))) ?x -- gcd can not yet be evaluated*)
1.132
1.133 lemma
1.134 fixes x y :: "_ poly"
1.135 @@ -1862,7 +1863,7 @@
1.136 (*value "gcd [:1,2,3:] [:1,2,3::int:]"
1.137 "Polynomial.zero_poly_inst.zero_poly" is not a constructor, on left hand side of equation, in theorem:
1.138 gcd_poly_inst.gcd_poly ?x zero_poly_inst.zero_poly \<equiv>
1.139 -smult (inverse (coeff ?x (degree ?x))) ?x*)
1.140 +smult (inverse (coeff ?x (degree ?x))) ?x -- gcd can not yet be evaluated*)
1.141
1.142 interpretation gcd_poly!: abel_semigroup "gcd :: _ poly \<Rightarrow> _"
1.143 proof
1.144 @@ -1878,7 +1879,7 @@
1.145 (*value "gcd [:1,2,3:] [:1,2,3::int:]"
1.146 "Polynomial.zero_poly_inst.zero_poly" is not a constructor, on left hand side of equation, in theorem:
1.147 gcd_poly_inst.gcd_poly ?x zero_poly_inst.zero_poly \<equiv>
1.148 -smult (inverse (coeff ?x (degree ?x))) ?x*)
1.149 +smult (inverse (coeff ?x (degree ?x))) ?x -- gcd can not yet be evaluated*)
1.150
1.151 lemmas poly_gcd_assoc = gcd_poly.assoc
1.152 lemmas poly_gcd_commute = gcd_poly.commute
1.153 @@ -1903,7 +1904,7 @@
1.154 (*value "gcd [:1,2,3:] [:1,2,3::int:]"
1.155 "Polynomial.zero_poly_inst.zero_poly" is not a constructor, on left hand side of equation, in theorem:
1.156 gcd_poly_inst.gcd_poly ?x zero_poly_inst.zero_poly \<equiv>
1.157 -smult (inverse (coeff ?x (degree ?x))) ?x*)
1.158 +smult (inverse (coeff ?x (degree ?x))) ?x -- gcd can not yet be evaluated*)
1.159 term "Polynomial.zero_poly_inst.zero_poly" (*"zero_poly_inst.zero_poly" :: "'a poly"*)
1.160 term "zero_poly_inst.zero_poly"
1.161 term "zero_poly_inst" (* free! *)
1.162 @@ -1913,7 +1914,8 @@
1.163 "gcd x y = (if y = 0 then smult (inverse (coeff x (degree x))) x else gcd y (x mod (y :: _ poly)))"
1.164 by (simp add: gcd_poly.simps)
1.165
1.166 -value "gcd [:1,2,3:] [:1,2,3::int:]" (*"Poly [1 / 3, 2 / 3, 1]" :: "real poly"*)
1.167 +value "gcd [:1,2,3:] [:1,2,3::int:]" (*"Poly [1 / 3, 2 / 3, 1]" :: "real poly"
1.168 + -- now can be evaluated (*1*)*)
1.169
1.170 subsection {* Composition of polynomials *}
1.171
1.172 @@ -1946,4 +1948,3 @@
1.173
1.174 end
1.175
1.176 -