1.1 --- a/src/HOL/Library/Polynomial.thy Sat Jul 20 08:07:39 2013 +0200
1.2 +++ b/src/HOL/Library/Polynomial.thy Sun Jul 21 15:08:31 2013 +0200
1.3 @@ -1,47 +1,202 @@
1.4 (* Title: HOL/Library/Polynomial.thy
1.5 Author: Brian Huffman
1.6 Author: Clemens Ballarin
1.7 + Author: Florian Haftmann
1.8 *)
1.9
1.10 -header {* Univariate Polynomials *}
1.11 +header {* Polynomials as type over a ring structure *}
1.12
1.13 theory Polynomial
1.14 -imports Main
1.15 +imports Main GCD
1.16 begin
1.17
1.18 +subsection {* Auxiliary: operations for lists (later) representing coefficients *}
1.19 +
1.20 +definition strip_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
1.21 +where
1.22 + "strip_while P = rev \<circ> dropWhile P \<circ> rev"
1.23 +
1.24 +lemma strip_while_Nil [simp]:
1.25 + "strip_while P [] = []"
1.26 + by (simp add: strip_while_def)
1.27 +
1.28 +lemma strip_while_append [simp]:
1.29 + "\<not> P x \<Longrightarrow> strip_while P (xs @ [x]) = xs @ [x]"
1.30 + by (simp add: strip_while_def)
1.31 +
1.32 +lemma strip_while_append_rec [simp]:
1.33 + "P x \<Longrightarrow> strip_while P (xs @ [x]) = strip_while P xs"
1.34 + by (simp add: strip_while_def)
1.35 +
1.36 +lemma strip_while_Cons [simp]:
1.37 + "\<not> P x \<Longrightarrow> strip_while P (x # xs) = x # strip_while P xs"
1.38 + by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
1.39 +
1.40 +lemma strip_while_eq_Nil [simp]:
1.41 + "strip_while P xs = [] \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
1.42 + by (simp add: strip_while_def)
1.43 +
1.44 +lemma strip_while_eq_Cons_rec:
1.45 + "strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))"
1.46 + by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
1.47 +
1.48 +lemma strip_while_not_last [simp]:
1.49 + "\<not> P (last xs) \<Longrightarrow> strip_while P xs = xs"
1.50 + by (cases xs rule: rev_cases) simp_all
1.51 +
1.52 +lemma split_strip_while_append:
1.53 + fixes xs :: "'a list"
1.54 + obtains ys zs :: "'a list"
1.55 + where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs"
1.56 +(* WN130721: takeWhile_eq_all_conv
1.57 +proof (rule that)
1.58 + show "strip_while P xs = strip_while P xs" ..
1.59 + show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
1.60 + have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
1.61 + by (simp add: strip_while_def)
1.62 + then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
1.63 + by (simp only: rev_is_rev_conv)
1.64 +qed
1.65 +*) sorry
1.66 +
1.67 +definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
1.68 +where
1.69 + "nth_default x xs n = (if n < length xs then xs ! n else x)"
1.70 +
1.71 +lemma nth_default_Nil [simp]:
1.72 + "nth_default y [] n = y"
1.73 + by (simp add: nth_default_def)
1.74 +
1.75 +lemma nth_default_Cons_0 [simp]:
1.76 + "nth_default y (x # xs) 0 = x"
1.77 + by (simp add: nth_default_def)
1.78 +
1.79 +lemma nth_default_Cons_Suc [simp]:
1.80 + "nth_default y (x # xs) (Suc n) = nth_default y xs n"
1.81 + by (simp add: nth_default_def)
1.82 +
1.83 +lemma nth_default_map_eq:
1.84 + "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
1.85 + by (simp add: nth_default_def)
1.86 +
1.87 +lemma nth_default_strip_while_eq [simp]:
1.88 + "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
1.89 +proof -
1.90 + from split_strip_while_append obtain ys zs
1.91 + where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
1.92 + then show ?thesis by (simp add: nth_default_def not_less nth_append)
1.93 +qed
1.94 +
1.95 +
1.96 +definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "##" 65)
1.97 +where
1.98 + "x ## xs = (if xs = [] \<and> x = 0 then [] else x # xs)"
1.99 +
1.100 +lemma cCons_0_Nil_eq [simp]:
1.101 + "0 ## [] = []"
1.102 + by (simp add: cCons_def)
1.103 +
1.104 +lemma cCons_Cons_eq [simp]:
1.105 + "x ## y # ys = x # y # ys"
1.106 + by (simp add: cCons_def)
1.107 +
1.108 +lemma cCons_append_Cons_eq [simp]:
1.109 + "x ## xs @ y # ys = x # xs @ y # ys"
1.110 + by (simp add: cCons_def)
1.111 +
1.112 +lemma cCons_not_0_eq [simp]:
1.113 + "x \<noteq> 0 \<Longrightarrow> x ## xs = x # xs"
1.114 + by (simp add: cCons_def)
1.115 +
1.116 +lemma strip_while_not_0_Cons_eq [simp]:
1.117 + "strip_while (\<lambda>x. x = 0) (x # xs) = x ## strip_while (\<lambda>x. x = 0) xs"
1.118 +proof (cases "x = 0")
1.119 + case False then show ?thesis by simp
1.120 +next
1.121 + case True show ?thesis
1.122 + proof (induct xs rule: rev_induct)
1.123 + case Nil with True show ?case by simp
1.124 + next
1.125 + case (snoc y ys) then show ?case
1.126 + by (cases "y = 0") (simp_all add: append_Cons [symmetric] del: append_Cons)
1.127 + qed
1.128 +qed
1.129 +
1.130 +lemma tl_cCons [simp]:
1.131 + "tl (x ## xs) = xs"
1.132 + by (simp add: cCons_def)
1.133 +
1.134 +
1.135 +subsection {* Almost everywhere zero functions *}
1.136 +
1.137 +definition almost_everywhere_zero :: "(nat \<Rightarrow> 'a::zero) \<Rightarrow> bool"
1.138 +where
1.139 + "almost_everywhere_zero f \<longleftrightarrow> (\<exists>n. \<forall>i>n. f i = 0)"
1.140 +
1.141 +lemma almost_everywhere_zeroI:
1.142 + "(\<And>i. i > n \<Longrightarrow> f i = 0) \<Longrightarrow> almost_everywhere_zero f"
1.143 + by (auto simp add: almost_everywhere_zero_def)
1.144 +
1.145 +lemma almost_everywhere_zeroE:
1.146 + assumes "almost_everywhere_zero f"
1.147 + obtains n where "\<And>i. i > n \<Longrightarrow> f i = 0"
1.148 +proof -
1.149 + from assms have "\<exists>n. \<forall>i>n. f i = 0" by (simp add: almost_everywhere_zero_def)
1.150 + then obtain n where "\<And>i. i > n \<Longrightarrow> f i = 0" by blast
1.151 + with that show thesis .
1.152 +qed
1.153 +
1.154 +lemma almost_everywhere_zero_nat_case:
1.155 + assumes "almost_everywhere_zero f"
1.156 + shows "almost_everywhere_zero (nat_case a f)"
1.157 + using assms
1.158 + by (auto intro!: almost_everywhere_zeroI elim!: almost_everywhere_zeroE split: nat.split)
1.159 + blast
1.160 +
1.161 +lemma almost_everywhere_zero_Suc:
1.162 + assumes "almost_everywhere_zero f"
1.163 + shows "almost_everywhere_zero (\<lambda>n. f (Suc n))"
1.164 +proof -
1.165 + from assms obtain n where "\<And>i. i > n \<Longrightarrow> f i = 0" by (erule almost_everywhere_zeroE)
1.166 + then have "\<And>i. i > n \<Longrightarrow> f (Suc i) = 0" by auto
1.167 + then show ?thesis by (rule almost_everywhere_zeroI)
1.168 +qed
1.169 +
1.170 +
1.171 subsection {* Definition of type @{text poly} *}
1.172
1.173 -definition "Poly = {f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
1.174 +typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. almost_everywhere_zero f}"
1.175 + morphisms coeff Abs_poly
1.176 + unfolding almost_everywhere_zero_def by auto
1.177
1.178 -typedef 'a poly = "Poly :: (nat => 'a::zero) set"
1.179 - morphisms coeff Abs_poly
1.180 - unfolding Poly_def by auto
1.181 +setup_lifting (no_code) type_definition_poly
1.182
1.183 -(* FIXME should be named poly_eq_iff *)
1.184 -lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
1.185 +lemma poly_eq_iff: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
1.186 by (simp add: coeff_inject [symmetric] fun_eq_iff)
1.187
1.188 -(* FIXME should be named poly_eqI *)
1.189 -lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
1.190 - by (simp add: expand_poly_eq)
1.191 +lemma poly_eqI: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
1.192 + by (simp add: poly_eq_iff)
1.193 +
1.194 +lemma coeff_almost_everywhere_zero:
1.195 + "almost_everywhere_zero (coeff p)"
1.196 + using coeff [of p] by simp
1.197
1.198
1.199 subsection {* Degree of a polynomial *}
1.200
1.201 -definition
1.202 - degree :: "'a::zero poly \<Rightarrow> nat" where
1.203 +definition degree :: "'a::zero poly \<Rightarrow> nat"
1.204 +where
1.205 "degree p = (LEAST n. \<forall>i>n. coeff p i = 0)"
1.206
1.207 -lemma coeff_eq_0: "degree p < n \<Longrightarrow> coeff p n = 0"
1.208 +lemma coeff_eq_0:
1.209 + assumes "degree p < n"
1.210 + shows "coeff p n = 0"
1.211 proof -
1.212 - have "coeff p \<in> Poly"
1.213 - by (rule coeff)
1.214 - hence "\<exists>n. \<forall>i>n. coeff p i = 0"
1.215 - unfolding Poly_def by simp
1.216 - hence "\<forall>i>degree p. coeff p i = 0"
1.217 + from coeff_almost_everywhere_zero
1.218 + have "\<exists>n. \<forall>i>n. coeff p i = 0" by (blast intro: almost_everywhere_zeroE)
1.219 + then have "\<forall>i>degree p. coeff p i = 0"
1.220 unfolding degree_def by (rule LeastI_ex)
1.221 - moreover assume "degree p < n"
1.222 - ultimately show ?thesis by simp
1.223 + with assms show ?thesis by simp
1.224 qed
1.225
1.226 lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p"
1.227 @@ -59,25 +214,28 @@
1.228 instantiation poly :: (zero) zero
1.229 begin
1.230
1.231 -definition
1.232 - zero_poly_def: "0 = Abs_poly (\<lambda>n. 0)"
1.233 +lift_definition zero_poly :: "'a poly"
1.234 + is "\<lambda>_. 0" by (rule almost_everywhere_zeroI) simp
1.235
1.236 instance ..
1.237 +
1.238 end
1.239
1.240 -lemma coeff_0 [simp]: "coeff 0 n = 0"
1.241 - unfolding zero_poly_def
1.242 - by (simp add: Abs_poly_inverse Poly_def)
1.243 +lemma coeff_0 [simp]:
1.244 + "coeff 0 n = 0"
1.245 + by transfer rule
1.246
1.247 -lemma degree_0 [simp]: "degree 0 = 0"
1.248 +lemma degree_0 [simp]:
1.249 + "degree 0 = 0"
1.250 by (rule order_antisym [OF degree_le le0]) simp
1.251
1.252 lemma leading_coeff_neq_0:
1.253 - assumes "p \<noteq> 0" shows "coeff p (degree p) \<noteq> 0"
1.254 + assumes "p \<noteq> 0"
1.255 + shows "coeff p (degree p) \<noteq> 0"
1.256 proof (cases "degree p")
1.257 case 0
1.258 from `p \<noteq> 0` have "\<exists>n. coeff p n \<noteq> 0"
1.259 - by (simp add: expand_poly_eq)
1.260 + by (simp add: poly_eq_iff)
1.261 then obtain n where "coeff p n \<noteq> 0" ..
1.262 hence "n \<le> degree p" by (rule le_degree)
1.263 with `coeff p n \<noteq> 0` and `degree p = 0`
1.264 @@ -93,68 +251,59 @@
1.265 with `coeff p i \<noteq> 0` show "coeff p (degree p) \<noteq> 0" by simp
1.266 qed
1.267
1.268 -lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
1.269 +lemma leading_coeff_0_iff [simp]:
1.270 + "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
1.271 by (cases "p = 0", simp, simp add: leading_coeff_neq_0)
1.272
1.273
1.274 subsection {* List-style constructor for polynomials *}
1.275
1.276 -definition
1.277 - pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
1.278 -where
1.279 - "pCons a p = Abs_poly (nat_case a (coeff p))"
1.280 +lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
1.281 + is "\<lambda>a p. nat_case a (coeff p)"
1.282 + using coeff_almost_everywhere_zero by (rule almost_everywhere_zero_nat_case)
1.283
1.284 -syntax
1.285 - "_poly" :: "args \<Rightarrow> 'a poly" ("[:(_):]")
1.286 +lemmas coeff_pCons = pCons.rep_eq
1.287
1.288 -translations
1.289 - "[:x, xs:]" == "CONST pCons x [:xs:]"
1.290 - "[:x:]" == "CONST pCons x 0"
1.291 - "[:x:]" <= "CONST pCons x (_constrain 0 t)"
1.292 +lemma coeff_pCons_0 [simp]:
1.293 + "coeff (pCons a p) 0 = a"
1.294 + by transfer simp
1.295
1.296 -lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly"
1.297 - unfolding Poly_def by (auto split: nat.split)
1.298 -
1.299 -lemma coeff_pCons:
1.300 - "coeff (pCons a p) = nat_case a (coeff p)"
1.301 - unfolding pCons_def
1.302 - by (simp add: Abs_poly_inverse Poly_nat_case coeff)
1.303 -
1.304 -lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a"
1.305 +lemma coeff_pCons_Suc [simp]:
1.306 + "coeff (pCons a p) (Suc n) = coeff p n"
1.307 by (simp add: coeff_pCons)
1.308
1.309 -lemma coeff_pCons_Suc [simp]: "coeff (pCons a p) (Suc n) = coeff p n"
1.310 - by (simp add: coeff_pCons)
1.311 -
1.312 -lemma degree_pCons_le: "degree (pCons a p) \<le> Suc (degree p)"
1.313 -by (rule degree_le, simp add: coeff_eq_0 coeff_pCons split: nat.split)
1.314 +lemma degree_pCons_le:
1.315 + "degree (pCons a p) \<le> Suc (degree p)"
1.316 + by (rule degree_le) (simp add: coeff_eq_0 coeff_pCons split: nat.split)
1.317
1.318 lemma degree_pCons_eq:
1.319 "p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)"
1.320 -apply (rule order_antisym [OF degree_pCons_le])
1.321 -apply (rule le_degree, simp)
1.322 -done
1.323 + apply (rule order_antisym [OF degree_pCons_le])
1.324 + apply (rule le_degree, simp)
1.325 + done
1.326
1.327 -lemma degree_pCons_0: "degree (pCons a 0) = 0"
1.328 -apply (rule order_antisym [OF _ le0])
1.329 -apply (rule degree_le, simp add: coeff_pCons split: nat.split)
1.330 -done
1.331 +lemma degree_pCons_0:
1.332 + "degree (pCons a 0) = 0"
1.333 + apply (rule order_antisym [OF _ le0])
1.334 + apply (rule degree_le, simp add: coeff_pCons split: nat.split)
1.335 + done
1.336
1.337 lemma degree_pCons_eq_if [simp]:
1.338 "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
1.339 -apply (cases "p = 0", simp_all)
1.340 -apply (rule order_antisym [OF _ le0])
1.341 -apply (rule degree_le, simp add: coeff_pCons split: nat.split)
1.342 -apply (rule order_antisym [OF degree_pCons_le])
1.343 -apply (rule le_degree, simp)
1.344 -done
1.345 + apply (cases "p = 0", simp_all)
1.346 + apply (rule order_antisym [OF _ le0])
1.347 + apply (rule degree_le, simp add: coeff_pCons split: nat.split)
1.348 + apply (rule order_antisym [OF degree_pCons_le])
1.349 + apply (rule le_degree, simp)
1.350 + done
1.351
1.352 -lemma pCons_0_0 [simp, code_post]: "pCons 0 0 = 0"
1.353 -by (rule poly_ext, simp add: coeff_pCons split: nat.split)
1.354 +lemma pCons_0_0 [simp]:
1.355 + "pCons 0 0 = 0"
1.356 + by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
1.357
1.358 lemma pCons_eq_iff [simp]:
1.359 "pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q"
1.360 -proof (safe)
1.361 +proof safe
1.362 assume "pCons a p = pCons b q"
1.363 then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp
1.364 then show "a = b" by simp
1.365 @@ -162,23 +311,19 @@
1.366 assume "pCons a p = pCons b q"
1.367 then have "\<forall>n. coeff (pCons a p) (Suc n) =
1.368 coeff (pCons b q) (Suc n)" by simp
1.369 - then show "p = q" by (simp add: expand_poly_eq)
1.370 + then show "p = q" by (simp add: poly_eq_iff)
1.371 qed
1.372
1.373 -lemma pCons_eq_0_iff [simp]: "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"
1.374 +lemma pCons_eq_0_iff [simp]:
1.375 + "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"
1.376 using pCons_eq_iff [of a p 0 0] by simp
1.377
1.378 -lemma Poly_Suc: "f \<in> Poly \<Longrightarrow> (\<lambda>n. f (Suc n)) \<in> Poly"
1.379 - unfolding Poly_def
1.380 - by (clarify, rule_tac x=n in exI, simp)
1.381 -
1.382 lemma pCons_cases [cases type: poly]:
1.383 obtains (pCons) a q where "p = pCons a q"
1.384 proof
1.385 show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"
1.386 - by (rule poly_ext)
1.387 - (simp add: Abs_poly_inverse Poly_Suc coeff coeff_pCons
1.388 - split: nat.split)
1.389 + by transfer
1.390 + (simp add: Abs_poly_inverse almost_everywhere_zero_Suc fun_eq_iff split: nat.split)
1.391 qed
1.392
1.393 lemma pCons_induct [case_names 0 pCons, induct type: poly]:
1.394 @@ -208,52 +353,233 @@
1.395 qed
1.396
1.397
1.398 -subsection {* Recursion combinator for polynomials *}
1.399 +subsection {* List-style syntax for polynomials *}
1.400
1.401 -function
1.402 - poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b"
1.403 +syntax
1.404 + "_poly" :: "args \<Rightarrow> 'a poly" ("[:(_):]")
1.405 +
1.406 +translations
1.407 + "[:x, xs:]" == "CONST pCons x [:xs:]"
1.408 + "[:x:]" == "CONST pCons x 0"
1.409 + "[:x:]" <= "CONST pCons x (_constrain 0 t)"
1.410 +
1.411 +
1.412 +subsection {* Representation of polynomials by lists of coefficients *}
1.413 +
1.414 +primrec Poly :: "'a::zero list \<Rightarrow> 'a poly"
1.415 where
1.416 - poly_rec_pCons_eq_if [simp del]:
1.417 - "poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)"
1.418 -by (case_tac x, rename_tac q, case_tac q, auto)
1.419 + "Poly [] = 0"
1.420 +| "Poly (a # as) = pCons a (Poly as)"
1.421
1.422 -termination poly_rec
1.423 -by (relation "measure (degree \<circ> snd \<circ> snd)", simp)
1.424 - (simp add: degree_pCons_eq)
1.425 +lemma Poly_replicate_0 [simp]:
1.426 + "Poly (replicate n 0) = 0"
1.427 + by (induct n) simp_all
1.428
1.429 -lemma poly_rec_0:
1.430 - "f 0 0 z = z \<Longrightarrow> poly_rec z f 0 = z"
1.431 - using poly_rec_pCons_eq_if [of z f 0 0] by simp
1.432 +lemma Poly_eq_0:
1.433 + "Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)"
1.434 +(* WN130721: unknown Cons_replicate_e
1.435 + by (induct as) (auto simp add: Cons_replicate_eq)
1.436 +*) sorry
1.437
1.438 -lemma poly_rec_pCons:
1.439 - "f 0 0 z = z \<Longrightarrow> poly_rec z f (pCons a p) = f a p (poly_rec z f p)"
1.440 - by (simp add: poly_rec_pCons_eq_if poly_rec_0)
1.441 +definition coeffs :: "'a poly \<Rightarrow> 'a::zero list"
1.442 +where
1.443 + "coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])"
1.444 +
1.445 +lemma coeffs_eq_Nil [simp]:
1.446 + "coeffs p = [] \<longleftrightarrow> p = 0"
1.447 + by (simp add: coeffs_def)
1.448 +
1.449 +lemma not_0_coeffs_not_Nil:
1.450 + "p \<noteq> 0 \<Longrightarrow> coeffs p \<noteq> []"
1.451 + by simp
1.452 +
1.453 +lemma coeffs_0_eq_Nil [simp]:
1.454 + "coeffs 0 = []"
1.455 + by simp
1.456 +
1.457 +lemma coeffs_pCons_eq_cCons [simp]:
1.458 + "coeffs (pCons a p) = a ## coeffs p"
1.459 +(* WN130721: unknown map_decr_upt
1.460 +proof -
1.461 + { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
1.462 + assume "\<forall>m\<in>set ms. m > 0"
1.463 + then have "map (nat_case x f) ms = map f (map (\<lambda>n. n - 1) ms)"
1.464 + by (induct ms) (auto, metis Suc_pred' nat_case_Suc) }
1.465 + note * = this
1.466 + show ?thesis
1.467 + by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)
1.468 +qed
1.469 +*) sorry
1.470 +
1.471 +lemma not_0_cCons_eq [simp]:
1.472 + "p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p"
1.473 + by (simp add: cCons_def)
1.474 +
1.475 +lemma Poly_coeffs [simp, code abstype]:
1.476 + "Poly (coeffs p) = p"
1.477 + by (induct p) (simp_all add: cCons_def)
1.478 +
1.479 +lemma coeffs_Poly [simp]:
1.480 + "coeffs (Poly as) = strip_while (HOL.eq 0) as"
1.481 +(* WN130721: unknown replicate_length_same
1.482 +proof (induct as)
1.483 + case Nil then show ?case by simp
1.484 +next
1.485 + case (Cons a as)
1.486 + have "(\<forall>n. as \<noteq> replicate n 0) \<longleftrightarrow> (\<exists>a\<in>set as. a \<noteq> 0)"
1.487 + using replicate_length_same [of as 0] by (auto dest: sym [of _ as])
1.488 + with Cons show ?case by auto
1.489 +qed
1.490 +*) sorry
1.491 +
1.492 +lemma last_coeffs_not_0:
1.493 + "p \<noteq> 0 \<Longrightarrow> last (coeffs p) \<noteq> 0"
1.494 + by (induct p) (auto simp add: cCons_def)
1.495 +
1.496 +lemma strip_while_coeffs [simp]:
1.497 + "strip_while (HOL.eq 0) (coeffs p) = coeffs p"
1.498 + by (cases "p = 0") (auto dest: last_coeffs_not_0 intro: strip_while_not_last)
1.499 +
1.500 +lemma coeffs_eq_iff:
1.501 + "p = q \<longleftrightarrow> coeffs p = coeffs q" (is "?P \<longleftrightarrow> ?Q")
1.502 +proof
1.503 + assume ?P then show ?Q by simp
1.504 +next
1.505 + assume ?Q
1.506 + then have "Poly (coeffs p) = Poly (coeffs q)" by simp
1.507 + then show ?P by simp
1.508 +qed
1.509 +
1.510 +lemma coeff_Poly_eq:
1.511 + "coeff (Poly xs) n = nth_default 0 xs n"
1.512 + apply (induct xs arbitrary: n) apply simp_all
1.513 + by (metis nat_case_0 nat_case_Suc not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
1.514 +
1.515 +lemma nth_default_coeffs_eq:
1.516 + "nth_default 0 (coeffs p) = coeff p"
1.517 + by (simp add: fun_eq_iff coeff_Poly_eq [symmetric])
1.518 +
1.519 +lemma [code]:
1.520 + "coeff p = nth_default 0 (coeffs p)"
1.521 + by (simp add: nth_default_coeffs_eq)
1.522 +
1.523 +lemma coeffs_eqI:
1.524 + assumes coeff: "\<And>n. coeff p n = nth_default 0 xs n"
1.525 + assumes zero: "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0"
1.526 + shows "coeffs p = xs"
1.527 +proof -
1.528 + from coeff have "p = Poly xs" by (simp add: poly_eq_iff coeff_Poly_eq)
1.529 + with zero show ?thesis by simp (cases xs, simp_all)
1.530 +qed
1.531 +
1.532 +lemma degree_eq_length_coeffs [code]:
1.533 + "degree p = length (coeffs p) - 1"
1.534 + by (simp add: coeffs_def)
1.535 +
1.536 +lemma length_coeffs_degree:
1.537 + "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = Suc (degree p)"
1.538 + by (induct p) (auto simp add: cCons_def)
1.539 +
1.540 +lemma [code abstract]:
1.541 + "coeffs 0 = []"
1.542 + by (fact coeffs_0_eq_Nil)
1.543 +
1.544 +lemma [code abstract]:
1.545 + "coeffs (pCons a p) = a ## coeffs p"
1.546 + by (fact coeffs_pCons_eq_cCons)
1.547 +
1.548 +instantiation poly :: ("{zero, equal}") equal
1.549 +begin
1.550 +
1.551 +definition
1.552 + [code]: "HOL.equal (p::'a poly) q \<longleftrightarrow> HOL.equal (coeffs p) (coeffs q)"
1.553 +
1.554 +instance proof
1.555 +qed (simp add: equal equal_poly_def coeffs_eq_iff)
1.556 +
1.557 +end
1.558 +
1.559 +lemma [code nbe]:
1.560 + "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
1.561 + by (fact equal_refl)
1.562 +
1.563 +definition is_zero :: "'a::zero poly \<Rightarrow> bool"
1.564 +where
1.565 + [code]: "is_zero p \<longleftrightarrow> List.null (coeffs p)"
1.566 +
1.567 +lemma is_zero_null [code_abbrev]:
1.568 + "is_zero p \<longleftrightarrow> p = 0"
1.569 + by (simp add: is_zero_def null_def)
1.570 +
1.571 +
1.572 +subsection {* Fold combinator for polynomials *}
1.573 +
1.574 +definition fold_coeffs :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b"
1.575 +where
1.576 + "fold_coeffs f p = foldr f (coeffs p)"
1.577 +
1.578 +lemma fold_coeffs_0_eq [simp]:
1.579 + "fold_coeffs f 0 = id"
1.580 + by (simp add: fold_coeffs_def)
1.581 +
1.582 +lemma fold_coeffs_pCons_eq [simp]:
1.583 + "f 0 = id \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
1.584 + by (simp add: fold_coeffs_def cCons_def fun_eq_iff)
1.585 +
1.586 +lemma fold_coeffs_pCons_0_0_eq [simp]:
1.587 + "fold_coeffs f (pCons 0 0) = id"
1.588 + by (simp add: fold_coeffs_def)
1.589 +
1.590 +lemma fold_coeffs_pCons_coeff_not_0_eq [simp]:
1.591 + "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
1.592 + by (simp add: fold_coeffs_def)
1.593 +
1.594 +lemma fold_coeffs_pCons_not_0_0_eq [simp]:
1.595 + "p \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
1.596 + by (simp add: fold_coeffs_def)
1.597 +
1.598 +
1.599 +subsection {* Canonical morphism on polynomials -- evaluation *}
1.600 +
1.601 +definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a"
1.602 +where
1.603 + "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" -- {* The Horner Schema *}
1.604 +
1.605 +lemma poly_0 [simp]:
1.606 + "poly 0 x = 0"
1.607 + by (simp add: poly_def)
1.608 +
1.609 +lemma poly_pCons [simp]:
1.610 + "poly (pCons a p) x = a + x * poly p x"
1.611 + by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)
1.612
1.613
1.614 subsection {* Monomials *}
1.615
1.616 -definition
1.617 - monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly" where
1.618 - "monom a m = Abs_poly (\<lambda>n. if m = n then a else 0)"
1.619 +lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly"
1.620 + is "\<lambda>a m n. if m = n then a else 0"
1.621 + by (auto intro!: almost_everywhere_zeroI)
1.622
1.623 -lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
1.624 - unfolding monom_def
1.625 - by (subst Abs_poly_inverse, auto simp add: Poly_def)
1.626 +lemma coeff_monom [simp]:
1.627 + "coeff (monom a m) n = (if m = n then a else 0)"
1.628 + by transfer rule
1.629
1.630 -lemma monom_0: "monom a 0 = pCons a 0"
1.631 - by (rule poly_ext, simp add: coeff_pCons split: nat.split)
1.632 +lemma monom_0:
1.633 + "monom a 0 = pCons a 0"
1.634 + by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
1.635
1.636 -lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)"
1.637 - by (rule poly_ext, simp add: coeff_pCons split: nat.split)
1.638 +lemma monom_Suc:
1.639 + "monom a (Suc n) = pCons 0 (monom a n)"
1.640 + by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
1.641
1.642 lemma monom_eq_0 [simp]: "monom 0 n = 0"
1.643 - by (rule poly_ext) simp
1.644 + by (rule poly_eqI) simp
1.645
1.646 lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0"
1.647 - by (simp add: expand_poly_eq)
1.648 + by (simp add: poly_eq_iff)
1.649
1.650 lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b"
1.651 - by (simp add: expand_poly_eq)
1.652 + by (simp add: poly_eq_iff)
1.653
1.654 lemma degree_monom_le: "degree (monom a n) \<le> n"
1.655 by (rule degree_le, simp)
1.656 @@ -263,37 +589,49 @@
1.657 apply (rule le_degree, simp)
1.658 done
1.659
1.660 +lemma coeffs_monom [code abstract]:
1.661 + "coeffs (monom a n) = (if a = 0 then [] else replicate n 0 @ [a])"
1.662 + by (induct n) (simp_all add: monom_0 monom_Suc)
1.663 +
1.664 +lemma fold_coeffs_monom [simp]:
1.665 + "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (monom a n) = f 0 ^^ n \<circ> f a"
1.666 +(* WN130721:
1.667 + by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff)
1.668 +*) sorry
1.669 +
1.670 +lemma poly_monom:
1.671 + fixes a x :: "'a::{comm_semiring_1}"
1.672 + shows "poly (monom a n) x = a * x ^ n"
1.673 + by (cases "a = 0", simp_all)
1.674 + (induct n, simp_all add: mult.left_commute poly_def)
1.675 +
1.676
1.677 subsection {* Addition and subtraction *}
1.678
1.679 instantiation poly :: (comm_monoid_add) comm_monoid_add
1.680 begin
1.681
1.682 -definition
1.683 - plus_poly_def:
1.684 - "p + q = Abs_poly (\<lambda>n. coeff p n + coeff q n)"
1.685 -
1.686 -lemma Poly_add:
1.687 - fixes f g :: "nat \<Rightarrow> 'a"
1.688 - shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n + g n) \<in> Poly"
1.689 - unfolding Poly_def
1.690 - apply (clarify, rename_tac m n)
1.691 - apply (rule_tac x="max m n" in exI, simp)
1.692 - done
1.693 +lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
1.694 + is "\<lambda>p q n. coeff p n + coeff q n"
1.695 +proof (rule almost_everywhere_zeroI)
1.696 + fix q p :: "'a poly" and i
1.697 + assume "max (degree q) (degree p) < i"
1.698 + then show "coeff p i + coeff q i = 0"
1.699 + by (simp add: coeff_eq_0)
1.700 +qed
1.701
1.702 lemma coeff_add [simp]:
1.703 "coeff (p + q) n = coeff p n + coeff q n"
1.704 - unfolding plus_poly_def
1.705 - by (simp add: Abs_poly_inverse coeff Poly_add)
1.706 + by (simp add: plus_poly.rep_eq)
1.707
1.708 instance proof
1.709 fix p q r :: "'a poly"
1.710 show "(p + q) + r = p + (q + r)"
1.711 - by (simp add: expand_poly_eq add_assoc)
1.712 + by (simp add: poly_eq_iff add_assoc)
1.713 show "p + q = q + p"
1.714 - by (simp add: expand_poly_eq add_commute)
1.715 + by (simp add: poly_eq_iff add_commute)
1.716 show "0 + p = p"
1.717 - by (simp add: expand_poly_eq)
1.718 + by (simp add: poly_eq_iff)
1.719 qed
1.720
1.721 end
1.722 @@ -302,60 +640,58 @@
1.723 proof
1.724 fix p q r :: "'a poly"
1.725 assume "p + q = p + r" thus "q = r"
1.726 - by (simp add: expand_poly_eq)
1.727 + by (simp add: poly_eq_iff)
1.728 qed
1.729
1.730 instantiation poly :: (ab_group_add) ab_group_add
1.731 begin
1.732
1.733 -definition
1.734 - uminus_poly_def:
1.735 - "- p = Abs_poly (\<lambda>n. - coeff p n)"
1.736 +lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
1.737 + is "\<lambda>p n. - coeff p n"
1.738 +proof (rule almost_everywhere_zeroI)
1.739 + fix p :: "'a poly" and i
1.740 + assume "degree p < i"
1.741 + then show "- coeff p i = 0"
1.742 + by (simp add: coeff_eq_0)
1.743 +qed
1.744
1.745 -definition
1.746 - minus_poly_def:
1.747 - "p - q = Abs_poly (\<lambda>n. coeff p n - coeff q n)"
1.748 -
1.749 -lemma Poly_minus:
1.750 - fixes f :: "nat \<Rightarrow> 'a"
1.751 - shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. - f n) \<in> Poly"
1.752 - unfolding Poly_def by simp
1.753 -
1.754 -lemma Poly_diff:
1.755 - fixes f g :: "nat \<Rightarrow> 'a"
1.756 - shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n - g n) \<in> Poly"
1.757 - unfolding diff_minus by (simp add: Poly_add Poly_minus)
1.758 +lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
1.759 + is "\<lambda>p q n. coeff p n - coeff q n"
1.760 +proof (rule almost_everywhere_zeroI)
1.761 + fix q p :: "'a poly" and i
1.762 + assume "max (degree q) (degree p) < i"
1.763 + then show "coeff p i - coeff q i = 0"
1.764 + by (simp add: coeff_eq_0)
1.765 +qed
1.766
1.767 lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
1.768 - unfolding uminus_poly_def
1.769 - by (simp add: Abs_poly_inverse coeff Poly_minus)
1.770 + by (simp add: uminus_poly.rep_eq)
1.771
1.772 lemma coeff_diff [simp]:
1.773 "coeff (p - q) n = coeff p n - coeff q n"
1.774 - unfolding minus_poly_def
1.775 - by (simp add: Abs_poly_inverse coeff Poly_diff)
1.776 + by (simp add: minus_poly.rep_eq)
1.777
1.778 instance proof
1.779 fix p q :: "'a poly"
1.780 show "- p + p = 0"
1.781 - by (simp add: expand_poly_eq)
1.782 + by (simp add: poly_eq_iff)
1.783 show "p - q = p + - q"
1.784 - by (simp add: expand_poly_eq diff_minus)
1.785 + by (simp add: poly_eq_iff diff_minus)
1.786 qed
1.787
1.788 end
1.789
1.790 lemma add_pCons [simp]:
1.791 "pCons a p + pCons b q = pCons (a + b) (p + q)"
1.792 - by (rule poly_ext, simp add: coeff_pCons split: nat.split)
1.793 + by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
1.794
1.795 lemma minus_pCons [simp]:
1.796 "- pCons a p = pCons (- a) (- p)"
1.797 - by (rule poly_ext, simp add: coeff_pCons split: nat.split)
1.798 + by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
1.799
1.800 lemma diff_pCons [simp]:
1.801 "pCons a p - pCons b q = pCons (a - b) (p - q)"
1.802 - by (rule poly_ext, simp add: coeff_pCons split: nat.split)
1.803 + by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
1.804
1.805 lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)"
1.806 by (rule degree_le, auto simp add: coeff_eq_0)
1.807 @@ -398,75 +734,135 @@
1.808 by (simp add: diff_minus degree_add_less)
1.809
1.810 lemma add_monom: "monom a n + monom b n = monom (a + b) n"
1.811 - by (rule poly_ext) simp
1.812 + by (rule poly_eqI) simp
1.813
1.814 lemma diff_monom: "monom a n - monom b n = monom (a - b) n"
1.815 - by (rule poly_ext) simp
1.816 + by (rule poly_eqI) simp
1.817
1.818 lemma minus_monom: "- monom a n = monom (-a) n"
1.819 - by (rule poly_ext) simp
1.820 + by (rule poly_eqI) simp
1.821
1.822 lemma coeff_setsum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)"
1.823 by (cases "finite A", induct set: finite, simp_all)
1.824
1.825 lemma monom_setsum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)"
1.826 - by (rule poly_ext) (simp add: coeff_setsum)
1.827 + by (rule poly_eqI) (simp add: coeff_setsum)
1.828
1.829 +fun plus_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list \<Rightarrow> 'a list"
1.830 +where
1.831 + "plus_coeffs xs [] = xs"
1.832 +| "plus_coeffs [] ys = ys"
1.833 +| "plus_coeffs (x # xs) (y # ys) = (x + y) ## plus_coeffs xs ys"
1.834
1.835 -subsection {* Multiplication by a constant *}
1.836 +lemma coeffs_plus_eq_plus_coeffs [code abstract]:
1.837 + "coeffs (p + q) = plus_coeffs (coeffs p) (coeffs q)"
1.838 +proof -
1.839 + { fix xs ys :: "'a list" and n
1.840 + have "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
1.841 + proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
1.842 + case (3 x xs y ys n) then show ?case by (cases n) (auto simp add: cCons_def)
1.843 + qed simp_all }
1.844 + note * = this
1.845 + { fix xs ys :: "'a list"
1.846 + assume "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0" and "ys \<noteq> [] \<Longrightarrow> last ys \<noteq> 0"
1.847 + moreover assume "plus_coeffs xs ys \<noteq> []"
1.848 + ultimately have "last (plus_coeffs xs ys) \<noteq> 0"
1.849 + proof (induct xs ys rule: plus_coeffs.induct)
1.850 + case (3 x xs y ys) then show ?case by (auto simp add: cCons_def) metis
1.851 + qed simp_all }
1.852 + note ** = this
1.853 + show ?thesis
1.854 + apply (rule coeffs_eqI)
1.855 + apply (simp add: * nth_default_coeffs_eq)
1.856 + apply (rule **)
1.857 + apply (auto dest: last_coeffs_not_0)
1.858 + done
1.859 +qed
1.860
1.861 -definition
1.862 - smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
1.863 - "smult a p = Abs_poly (\<lambda>n. a * coeff p n)"
1.864 +lemma coeffs_uminus [code abstract]:
1.865 + "coeffs (- p) = map (\<lambda>a. - a) (coeffs p)"
1.866 + by (rule coeffs_eqI)
1.867 + (simp_all add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq)
1.868
1.869 -lemma Poly_smult:
1.870 - fixes f :: "nat \<Rightarrow> 'a::comm_semiring_0"
1.871 - shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. a * f n) \<in> Poly"
1.872 - unfolding Poly_def
1.873 - by (clarify, rule_tac x=n in exI, simp)
1.874 +lemma [code]:
1.875 + fixes p q :: "'a::ab_group_add poly"
1.876 + shows "p - q = p + - q"
1.877 + by simp
1.878
1.879 -lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n"
1.880 - unfolding smult_def
1.881 - by (simp add: Abs_poly_inverse Poly_smult coeff)
1.882 +lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
1.883 + apply (induct p arbitrary: q, simp)
1.884 + apply (case_tac q, simp, simp add: algebra_simps)
1.885 + done
1.886 +
1.887 +lemma poly_minus [simp]:
1.888 + fixes x :: "'a::comm_ring"
1.889 + shows "poly (- p) x = - poly p x"
1.890 + by (induct p) simp_all
1.891 +
1.892 +lemma poly_diff [simp]:
1.893 + fixes x :: "'a::comm_ring"
1.894 + shows "poly (p - q) x = poly p x - poly q x"
1.895 + by (simp add: diff_minus)
1.896 +
1.897 +lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
1.898 +(* WN130721: unknown infinite_finite_induct
1.899 + by (induct A rule: infinite_finite_induct) simp_all
1.900 +*) sorry
1.901 +
1.902 +
1.903 +subsection {* Multiplication by a constant, polynomial multiplication and the unit polynomial *}
1.904 +
1.905 +lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
1.906 + is "\<lambda>a p n. a * coeff p n"
1.907 +proof (rule almost_everywhere_zeroI)
1.908 + fix a :: 'a and p :: "'a poly" and i
1.909 + assume "degree p < i"
1.910 + then show "a * coeff p i = 0"
1.911 + by (simp add: coeff_eq_0)
1.912 +qed
1.913 +
1.914 +lemma coeff_smult [simp]:
1.915 + "coeff (smult a p) n = a * coeff p n"
1.916 + by (simp add: smult.rep_eq)
1.917
1.918 lemma degree_smult_le: "degree (smult a p) \<le> degree p"
1.919 by (rule degree_le, simp add: coeff_eq_0)
1.920
1.921 lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
1.922 - by (rule poly_ext, simp add: mult_assoc)
1.923 + by (rule poly_eqI, simp add: mult_assoc)
1.924
1.925 lemma smult_0_right [simp]: "smult a 0 = 0"
1.926 - by (rule poly_ext, simp)
1.927 + by (rule poly_eqI, simp)
1.928
1.929 lemma smult_0_left [simp]: "smult 0 p = 0"
1.930 - by (rule poly_ext, simp)
1.931 + by (rule poly_eqI, simp)
1.932
1.933 lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"
1.934 - by (rule poly_ext, simp)
1.935 + by (rule poly_eqI, simp)
1.936
1.937 lemma smult_add_right:
1.938 "smult a (p + q) = smult a p + smult a q"
1.939 - by (rule poly_ext, simp add: algebra_simps)
1.940 + by (rule poly_eqI, simp add: algebra_simps)
1.941
1.942 lemma smult_add_left:
1.943 "smult (a + b) p = smult a p + smult b p"
1.944 - by (rule poly_ext, simp add: algebra_simps)
1.945 + by (rule poly_eqI, simp add: algebra_simps)
1.946
1.947 lemma smult_minus_right [simp]:
1.948 "smult (a::'a::comm_ring) (- p) = - smult a p"
1.949 - by (rule poly_ext, simp)
1.950 + by (rule poly_eqI, simp)
1.951
1.952 lemma smult_minus_left [simp]:
1.953 "smult (- a::'a::comm_ring) p = - smult a p"
1.954 - by (rule poly_ext, simp)
1.955 + by (rule poly_eqI, simp)
1.956
1.957 lemma smult_diff_right:
1.958 "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q"
1.959 - by (rule poly_ext, simp add: algebra_simps)
1.960 + by (rule poly_eqI, simp add: algebra_simps)
1.961
1.962 lemma smult_diff_left:
1.963 "smult (a - b::'a::comm_ring) p = smult a p - smult b p"
1.964 - by (rule poly_ext, simp add: algebra_simps)
1.965 + by (rule poly_eqI, simp add: algebra_simps)
1.966
1.967 lemmas smult_distribs =
1.968 smult_add_left smult_add_right
1.969 @@ -474,7 +870,7 @@
1.970
1.971 lemma smult_pCons [simp]:
1.972 "smult a (pCons b p) = pCons (a * b) (smult a p)"
1.973 - by (rule poly_ext, simp add: coeff_pCons split: nat.split)
1.974 + by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
1.975
1.976 lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
1.977 by (induct n, simp add: monom_0, simp add: monom_Suc)
1.978 @@ -487,65 +883,48 @@
1.979 lemma smult_eq_0_iff [simp]:
1.980 fixes a :: "'a::idom"
1.981 shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
1.982 - by (simp add: expand_poly_eq)
1.983 + by (simp add: poly_eq_iff)
1.984
1.985 -
1.986 -subsection {* Multiplication of polynomials *}
1.987 -
1.988 -(* TODO: move to Set_Interval.thy *)
1.989 -lemma setsum_atMost_Suc_shift:
1.990 - fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
1.991 - shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
1.992 -proof (induct n)
1.993 - case 0 show ?case by simp
1.994 -next
1.995 - case (Suc n) note IH = this
1.996 - have "(\<Sum>i\<le>Suc (Suc n). f i) = (\<Sum>i\<le>Suc n. f i) + f (Suc (Suc n))"
1.997 - by (rule setsum_atMost_Suc)
1.998 - also have "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
1.999 - by (rule IH)
1.1000 - also have "f 0 + (\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) =
1.1001 - f 0 + ((\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)))"
1.1002 - by (rule add_assoc)
1.1003 - also have "(\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = (\<Sum>i\<le>Suc n. f (Suc i))"
1.1004 - by (rule setsum_atMost_Suc [symmetric])
1.1005 - finally show ?case .
1.1006 -qed
1.1007 +lemma coeffs_smult [code abstract]:
1.1008 + fixes p :: "'a::idom poly"
1.1009 + shows "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
1.1010 + by (rule coeffs_eqI)
1.1011 + (auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq)
1.1012
1.1013 instantiation poly :: (comm_semiring_0) comm_semiring_0
1.1014 begin
1.1015
1.1016 definition
1.1017 - times_poly_def:
1.1018 - "p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p"
1.1019 + "p * q = fold_coeffs (\<lambda>a p. smult a q + pCons 0 p) p 0"
1.1020
1.1021 lemma mult_poly_0_left: "(0::'a poly) * q = 0"
1.1022 - unfolding times_poly_def by (simp add: poly_rec_0)
1.1023 + by (simp add: times_poly_def)
1.1024
1.1025 lemma mult_pCons_left [simp]:
1.1026 "pCons a p * q = smult a q + pCons 0 (p * q)"
1.1027 - unfolding times_poly_def by (simp add: poly_rec_pCons)
1.1028 + by (cases "p = 0 \<and> a = 0") (auto simp add: times_poly_def)
1.1029
1.1030 lemma mult_poly_0_right: "p * (0::'a poly) = 0"
1.1031 - by (induct p, simp add: mult_poly_0_left, simp)
1.1032 + by (induct p) (simp add: mult_poly_0_left, simp)
1.1033
1.1034 lemma mult_pCons_right [simp]:
1.1035 "p * pCons a q = smult a p + pCons 0 (p * q)"
1.1036 - by (induct p, simp add: mult_poly_0_left, simp add: algebra_simps)
1.1037 + by (induct p) (simp add: mult_poly_0_left, simp add: algebra_simps)
1.1038
1.1039 lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right
1.1040
1.1041 -lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)"
1.1042 - by (induct p, simp add: mult_poly_0, simp add: smult_add_right)
1.1043 +lemma mult_smult_left [simp]:
1.1044 + "smult a p * q = smult a (p * q)"
1.1045 + by (induct p) (simp add: mult_poly_0, simp add: smult_add_right)
1.1046
1.1047 -lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)"
1.1048 - by (induct q, simp add: mult_poly_0, simp add: smult_add_right)
1.1049 +lemma mult_smult_right [simp]:
1.1050 + "p * smult a q = smult a (p * q)"
1.1051 + by (induct q) (simp add: mult_poly_0, simp add: smult_add_right)
1.1052
1.1053 lemma mult_poly_add_left:
1.1054 fixes p q r :: "'a poly"
1.1055 shows "(p + q) * r = p * r + q * r"
1.1056 - by (induct r, simp add: mult_poly_0,
1.1057 - simp add: smult_distribs algebra_simps)
1.1058 + by (induct r) (simp add: mult_poly_0, simp add: smult_distribs algebra_simps)
1.1059
1.1060 instance proof
1.1061 fix p q r :: "'a poly"
1.1062 @@ -567,6 +946,7 @@
1.1063
1.1064 lemma coeff_mult:
1.1065 "coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))"
1.1066 +(* WN130721: unknown setsum_atMost_Suc_shift
1.1067 proof (induct p arbitrary: n)
1.1068 case 0 show ?case by simp
1.1069 next
1.1070 @@ -574,6 +954,7 @@
1.1071 by (cases n, simp, simp add: setsum_atMost_Suc_shift
1.1072 del: setsum_atMost_Suc)
1.1073 qed
1.1074 +*) sorry
1.1075
1.1076 lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"
1.1077 apply (rule degree_le)
1.1078 @@ -585,20 +966,15 @@
1.1079 lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
1.1080 by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)
1.1081
1.1082 -
1.1083 -subsection {* The unit polynomial and exponentiation *}
1.1084 -
1.1085 instantiation poly :: (comm_semiring_1) comm_semiring_1
1.1086 begin
1.1087
1.1088 -definition
1.1089 - one_poly_def:
1.1090 - "1 = pCons 1 0"
1.1091 +definition one_poly_def:
1.1092 + "1 = pCons 1 0"
1.1093
1.1094 instance proof
1.1095 fix p :: "'a poly" show "1 * p = p"
1.1096 - unfolding one_poly_def
1.1097 - by simp
1.1098 + unfolding one_poly_def by simp
1.1099 next
1.1100 show "0 \<noteq> (1::'a poly)"
1.1101 unfolding one_poly_def by simp
1.1102 @@ -608,6 +984,10 @@
1.1103
1.1104 instance poly :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
1.1105
1.1106 +instance poly :: (comm_ring) comm_ring ..
1.1107 +
1.1108 +instance poly :: (comm_ring_1) comm_ring_1 ..
1.1109 +
1.1110 lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"
1.1111 unfolding one_poly_def
1.1112 by (simp add: coeff_pCons split: nat.split)
1.1113 @@ -616,7 +996,33 @@
1.1114 unfolding one_poly_def
1.1115 by (rule degree_pCons_0)
1.1116
1.1117 -text {* Lemmas about divisibility *}
1.1118 +lemma coeffs_1_eq [simp, code abstract]:
1.1119 + "coeffs 1 = [1]"
1.1120 + by (simp add: one_poly_def)
1.1121 +
1.1122 +lemma degree_power_le:
1.1123 + "degree (p ^ n) \<le> degree p * n"
1.1124 + by (induct n) (auto intro: order_trans degree_mult_le)
1.1125 +
1.1126 +lemma poly_smult [simp]:
1.1127 + "poly (smult a p) x = a * poly p x"
1.1128 + by (induct p, simp, simp add: algebra_simps)
1.1129 +
1.1130 +lemma poly_mult [simp]:
1.1131 + "poly (p * q) x = poly p x * poly q x"
1.1132 + by (induct p, simp_all, simp add: algebra_simps)
1.1133 +
1.1134 +lemma poly_1 [simp]:
1.1135 + "poly 1 x = 1"
1.1136 + by (simp add: one_poly_def)
1.1137 +
1.1138 +lemma poly_power [simp]:
1.1139 + fixes p :: "'a::{comm_semiring_1} poly"
1.1140 + shows "poly (p ^ n) x = poly p x ^ n"
1.1141 + by (induct n) simp_all
1.1142 +
1.1143 +
1.1144 +subsection {* Lemmas about divisibility *}
1.1145
1.1146 lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"
1.1147 proof -
1.1148 @@ -655,13 +1061,6 @@
1.1149 shows "smult a p dvd q \<longleftrightarrow> (if a = 0 then q = 0 else p dvd q)"
1.1150 by (auto elim: smult_dvd smult_dvd_cancel)
1.1151
1.1152 -lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
1.1153 -by (induct n, simp, auto intro: order_trans degree_mult_le)
1.1154 -
1.1155 -instance poly :: (comm_ring) comm_ring ..
1.1156 -
1.1157 -instance poly :: (comm_ring_1) comm_ring_1 ..
1.1158 -
1.1159
1.1160 subsection {* Polynomials form an integral domain *}
1.1161
1.1162 @@ -680,7 +1079,7 @@
1.1163 also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
1.1164 using `p \<noteq> 0` and `q \<noteq> 0` by simp
1.1165 finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
1.1166 - thus "p * q \<noteq> 0" by (simp add: expand_poly_eq)
1.1167 + thus "p * q \<noteq> 0" by (simp add: poly_eq_iff)
1.1168 qed
1.1169
1.1170 lemma degree_mult_eq:
1.1171 @@ -698,8 +1097,7 @@
1.1172
1.1173 subsection {* Polynomials form an ordered integral domain *}
1.1174
1.1175 -definition
1.1176 - pos_poly :: "'a::linordered_idom poly \<Rightarrow> bool"
1.1177 +definition pos_poly :: "'a::linordered_idom poly \<Rightarrow> bool"
1.1178 where
1.1179 "pos_poly p \<longleftrightarrow> 0 < coeff p (degree p)"
1.1180
1.1181 @@ -725,6 +1123,20 @@
1.1182 lemma pos_poly_total: "p = 0 \<or> pos_poly p \<or> pos_poly (- p)"
1.1183 by (induct p) (auto simp add: pos_poly_pCons)
1.1184
1.1185 +lemma last_coeffs_eq_coeff_degree:
1.1186 + "p \<noteq> 0 \<Longrightarrow> last (coeffs p) = coeff p (degree p)"
1.1187 + by (simp add: coeffs_def)
1.1188 +
1.1189 +lemma pos_poly_coeffs [code]:
1.1190 + "pos_poly p \<longleftrightarrow> (let as = coeffs p in as \<noteq> [] \<and> last as > 0)" (is "?P \<longleftrightarrow> ?Q")
1.1191 +proof
1.1192 + assume ?Q then show ?P by (auto simp add: pos_poly_def last_coeffs_eq_coeff_degree)
1.1193 +next
1.1194 + assume ?P then have *: "0 < coeff p (degree p)" by (simp add: pos_poly_def)
1.1195 + then have "p \<noteq> 0" by auto
1.1196 + with * show ?Q by (simp add: last_coeffs_eq_coeff_degree)
1.1197 +qed
1.1198 +
1.1199 instantiation poly :: (linordered_idom) linordered_idom
1.1200 begin
1.1201
1.1202 @@ -802,10 +1214,145 @@
1.1203 text {* TODO: Simplification rules for comparisons *}
1.1204
1.1205
1.1206 +subsection {* Synthetic division and polynomial roots *}
1.1207 +
1.1208 +text {*
1.1209 + Synthetic division is simply division by the linear polynomial @{term "x - c"}.
1.1210 +*}
1.1211 +
1.1212 +definition synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
1.1213 +where
1.1214 + "synthetic_divmod p c = fold_coeffs (\<lambda>a (q, r). (pCons r q, a + c * r)) p (0, 0)"
1.1215 +
1.1216 +definition synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
1.1217 +where
1.1218 + "synthetic_div p c = fst (synthetic_divmod p c)"
1.1219 +
1.1220 +lemma synthetic_divmod_0 [simp]:
1.1221 + "synthetic_divmod 0 c = (0, 0)"
1.1222 + by (simp add: synthetic_divmod_def)
1.1223 +
1.1224 +lemma synthetic_divmod_pCons [simp]:
1.1225 + "synthetic_divmod (pCons a p) c = (\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)"
1.1226 + by (cases "p = 0 \<and> a = 0") (auto simp add: synthetic_divmod_def)
1.1227 +
1.1228 +lemma synthetic_div_0 [simp]:
1.1229 + "synthetic_div 0 c = 0"
1.1230 + unfolding synthetic_div_def by simp
1.1231 +
1.1232 +lemma synthetic_div_unique_lemma: "smult c p = pCons a p \<Longrightarrow> p = 0"
1.1233 +by (induct p arbitrary: a) simp_all
1.1234 +
1.1235 +lemma snd_synthetic_divmod:
1.1236 + "snd (synthetic_divmod p c) = poly p c"
1.1237 + by (induct p, simp, simp add: split_def)
1.1238 +
1.1239 +lemma synthetic_div_pCons [simp]:
1.1240 + "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)"
1.1241 + unfolding synthetic_div_def
1.1242 + by (simp add: split_def snd_synthetic_divmod)
1.1243 +
1.1244 +lemma synthetic_div_eq_0_iff:
1.1245 + "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
1.1246 + by (induct p, simp, case_tac p, simp)
1.1247 +
1.1248 +lemma degree_synthetic_div:
1.1249 + "degree (synthetic_div p c) = degree p - 1"
1.1250 + by (induct p, simp, simp add: synthetic_div_eq_0_iff)
1.1251 +
1.1252 +lemma synthetic_div_correct:
1.1253 + "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
1.1254 + by (induct p) simp_all
1.1255 +
1.1256 +lemma synthetic_div_unique:
1.1257 + "p + smult c q = pCons r q \<Longrightarrow> r = poly p c \<and> q = synthetic_div p c"
1.1258 +apply (induct p arbitrary: q r)
1.1259 +apply (simp, frule synthetic_div_unique_lemma, simp)
1.1260 +apply (case_tac q, force)
1.1261 +done
1.1262 +
1.1263 +lemma synthetic_div_correct':
1.1264 + fixes c :: "'a::comm_ring_1"
1.1265 + shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p"
1.1266 + using synthetic_div_correct [of p c]
1.1267 + by (simp add: algebra_simps)
1.1268 +
1.1269 +lemma poly_eq_0_iff_dvd:
1.1270 + fixes c :: "'a::idom"
1.1271 + shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p"
1.1272 +proof
1.1273 + assume "poly p c = 0"
1.1274 + with synthetic_div_correct' [of c p]
1.1275 + have "p = [:-c, 1:] * synthetic_div p c" by simp
1.1276 + then show "[:-c, 1:] dvd p" ..
1.1277 +next
1.1278 + assume "[:-c, 1:] dvd p"
1.1279 + then obtain k where "p = [:-c, 1:] * k" by (rule dvdE)
1.1280 + then show "poly p c = 0" by simp
1.1281 +qed
1.1282 +
1.1283 +lemma dvd_iff_poly_eq_0:
1.1284 + fixes c :: "'a::idom"
1.1285 + shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0"
1.1286 + by (simp add: poly_eq_0_iff_dvd)
1.1287 +
1.1288 +lemma poly_roots_finite:
1.1289 + fixes p :: "'a::idom poly"
1.1290 + shows "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}"
1.1291 +proof (induct n \<equiv> "degree p" arbitrary: p)
1.1292 + case (0 p)
1.1293 + then obtain a where "a \<noteq> 0" and "p = [:a:]"
1.1294 + by (cases p, simp split: if_splits)
1.1295 + then show "finite {x. poly p x = 0}" by simp
1.1296 +next
1.1297 + case (Suc n p)
1.1298 + show "finite {x. poly p x = 0}"
1.1299 + proof (cases "\<exists>x. poly p x = 0")
1.1300 + case False
1.1301 + then show "finite {x. poly p x = 0}" by simp
1.1302 + next
1.1303 + case True
1.1304 + then obtain a where "poly p a = 0" ..
1.1305 + then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd)
1.1306 + then obtain k where k: "p = [:-a, 1:] * k" ..
1.1307 + with `p \<noteq> 0` have "k \<noteq> 0" by auto
1.1308 + with k have "degree p = Suc (degree k)"
1.1309 + by (simp add: degree_mult_eq del: mult_pCons_left)
1.1310 + with `Suc n = degree p` have "n = degree k" by simp
1.1311 + then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps)
1.1312 + then have "finite (insert a {x. poly k x = 0})" by simp
1.1313 + then show "finite {x. poly p x = 0}"
1.1314 + by (simp add: k uminus_add_conv_diff Collect_disj_eq
1.1315 + del: mult_pCons_left)
1.1316 + qed
1.1317 +qed
1.1318 +
1.1319 +lemma poly_eq_poly_eq_iff:
1.1320 + fixes p q :: "'a::{idom,ring_char_0} poly"
1.1321 + shows "poly p = poly q \<longleftrightarrow> p = q" (is "?P \<longleftrightarrow> ?Q")
1.1322 +proof
1.1323 + assume ?Q then show ?P by simp
1.1324 +next
1.1325 + { fix p :: "'a::{idom,ring_char_0} poly"
1.1326 + have "poly p = poly 0 \<longleftrightarrow> p = 0"
1.1327 + apply (cases "p = 0", simp_all)
1.1328 + apply (drule poly_roots_finite)
1.1329 + apply (auto simp add: infinite_UNIV_char_0)
1.1330 + done
1.1331 + } note this [of "p - q"]
1.1332 + moreover assume ?P
1.1333 + ultimately show ?Q by auto
1.1334 +qed
1.1335 +
1.1336 +lemma poly_all_0_iff_0:
1.1337 + fixes p :: "'a::{ring_char_0, idom} poly"
1.1338 + shows "(\<forall>x. poly p x = 0) \<longleftrightarrow> p = 0"
1.1339 + by (auto simp add: poly_eq_poly_eq_iff [symmetric])
1.1340 +
1.1341 +
1.1342 subsection {* Long division of polynomials *}
1.1343
1.1344 -definition
1.1345 - pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
1.1346 +definition pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
1.1347 where
1.1348 "pdivmod_rel x y q r \<longleftrightarrow>
1.1349 x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
1.1350 @@ -1106,327 +1653,54 @@
1.1351 apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl])
1.1352 done
1.1353
1.1354 +definition pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
1.1355 +where
1.1356 + "pdivmod p q = (p div q, p mod q)"
1.1357
1.1358 -subsection {* GCD of polynomials *}
1.1359 +lemma div_poly_code [code]:
1.1360 + "p div q = fst (pdivmod p q)"
1.1361 + by (simp add: pdivmod_def)
1.1362
1.1363 -function
1.1364 - poly_gcd :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
1.1365 - "poly_gcd x 0 = smult (inverse (coeff x (degree x))) x"
1.1366 -| "y \<noteq> 0 \<Longrightarrow> poly_gcd x y = poly_gcd y (x mod y)"
1.1367 -by auto
1.1368 +lemma mod_poly_code [code]:
1.1369 + "p mod q = snd (pdivmod p q)"
1.1370 + by (simp add: pdivmod_def)
1.1371
1.1372 -termination poly_gcd
1.1373 -by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))")
1.1374 - (auto dest: degree_mod_less)
1.1375 +lemma pdivmod_0:
1.1376 + "pdivmod 0 q = (0, 0)"
1.1377 + by (simp add: pdivmod_def)
1.1378
1.1379 -declare poly_gcd.simps [simp del]
1.1380 -
1.1381 -lemma poly_gcd_dvd1 [iff]: "poly_gcd x y dvd x"
1.1382 - and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y"
1.1383 - apply (induct x y rule: poly_gcd.induct)
1.1384 - apply (simp_all add: poly_gcd.simps)
1.1385 - apply (fastforce simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
1.1386 - apply (blast dest: dvd_mod_imp_dvd)
1.1387 +lemma pdivmod_pCons:
1.1388 + "pdivmod (pCons a p) q =
1.1389 + (if q = 0 then (0, pCons a p) else
1.1390 + (let (s, r) = pdivmod p q;
1.1391 + b = coeff (pCons a r) (degree q) / coeff q (degree q)
1.1392 + in (pCons b s, pCons a r - smult b q)))"
1.1393 + apply (simp add: pdivmod_def Let_def, safe)
1.1394 + apply (rule div_poly_eq)
1.1395 + apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
1.1396 + apply (rule mod_poly_eq)
1.1397 + apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
1.1398 done
1.1399
1.1400 -lemma poly_gcd_greatest: "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd poly_gcd x y"
1.1401 - by (induct x y rule: poly_gcd.induct)
1.1402 - (simp_all add: poly_gcd.simps dvd_mod dvd_smult)
1.1403 -
1.1404 -lemma dvd_poly_gcd_iff [iff]:
1.1405 - "k dvd poly_gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
1.1406 - by (blast intro!: poly_gcd_greatest intro: dvd_trans)
1.1407 -
1.1408 -lemma poly_gcd_monic:
1.1409 - "coeff (poly_gcd x y) (degree (poly_gcd x y)) =
1.1410 - (if x = 0 \<and> y = 0 then 0 else 1)"
1.1411 - by (induct x y rule: poly_gcd.induct)
1.1412 - (simp_all add: poly_gcd.simps nonzero_imp_inverse_nonzero)
1.1413 -
1.1414 -lemma poly_gcd_zero_iff [simp]:
1.1415 - "poly_gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
1.1416 - by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff)
1.1417 -
1.1418 -lemma poly_gcd_0_0 [simp]: "poly_gcd 0 0 = 0"
1.1419 - by simp
1.1420 -
1.1421 -lemma poly_dvd_antisym:
1.1422 - fixes p q :: "'a::idom poly"
1.1423 - assumes coeff: "coeff p (degree p) = coeff q (degree q)"
1.1424 - assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
1.1425 -proof (cases "p = 0")
1.1426 - case True with coeff show "p = q" by simp
1.1427 -next
1.1428 - case False with coeff have "q \<noteq> 0" by auto
1.1429 - have degree: "degree p = degree q"
1.1430 - using `p dvd q` `q dvd p` `p \<noteq> 0` `q \<noteq> 0`
1.1431 - by (intro order_antisym dvd_imp_degree_le)
1.1432 -
1.1433 - from `p dvd q` obtain a where a: "q = p * a" ..
1.1434 - with `q \<noteq> 0` have "a \<noteq> 0" by auto
1.1435 - with degree a `p \<noteq> 0` have "degree a = 0"
1.1436 - by (simp add: degree_mult_eq)
1.1437 - with coeff a show "p = q"
1.1438 - by (cases a, auto split: if_splits)
1.1439 -qed
1.1440 -
1.1441 -lemma poly_gcd_unique:
1.1442 - assumes dvd1: "d dvd x" and dvd2: "d dvd y"
1.1443 - and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d"
1.1444 - and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)"
1.1445 - shows "poly_gcd x y = d"
1.1446 -proof -
1.1447 - have "coeff (poly_gcd x y) (degree (poly_gcd x y)) = coeff d (degree d)"
1.1448 - by (simp_all add: poly_gcd_monic monic)
1.1449 - moreover have "poly_gcd x y dvd d"
1.1450 - using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest)
1.1451 - moreover have "d dvd poly_gcd x y"
1.1452 - using dvd1 dvd2 by (rule poly_gcd_greatest)
1.1453 - ultimately show ?thesis
1.1454 - by (rule poly_dvd_antisym)
1.1455 -qed
1.1456 -
1.1457 -interpretation poly_gcd: abel_semigroup poly_gcd
1.1458 -proof
1.1459 - fix x y z :: "'a poly"
1.1460 - show "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
1.1461 - by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
1.1462 - show "poly_gcd x y = poly_gcd y x"
1.1463 - by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
1.1464 -qed
1.1465 -
1.1466 -lemmas poly_gcd_assoc = poly_gcd.assoc
1.1467 -lemmas poly_gcd_commute = poly_gcd.commute
1.1468 -lemmas poly_gcd_left_commute = poly_gcd.left_commute
1.1469 -
1.1470 -lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
1.1471 -
1.1472 -lemma poly_gcd_1_left [simp]: "poly_gcd 1 y = 1"
1.1473 -by (rule poly_gcd_unique) simp_all
1.1474 -
1.1475 -lemma poly_gcd_1_right [simp]: "poly_gcd x 1 = 1"
1.1476 -by (rule poly_gcd_unique) simp_all
1.1477 -
1.1478 -lemma poly_gcd_minus_left [simp]: "poly_gcd (- x) y = poly_gcd x y"
1.1479 -by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
1.1480 -
1.1481 -lemma poly_gcd_minus_right [simp]: "poly_gcd x (- y) = poly_gcd x y"
1.1482 -by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
1.1483 -
1.1484 -
1.1485 -subsection {* Evaluation of polynomials *}
1.1486 -
1.1487 -definition
1.1488 - poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a" where
1.1489 - "poly = poly_rec (\<lambda>x. 0) (\<lambda>a p f x. a + x * f x)"
1.1490 -
1.1491 -lemma poly_0 [simp]: "poly 0 x = 0"
1.1492 - unfolding poly_def by (simp add: poly_rec_0)
1.1493 -
1.1494 -lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x"
1.1495 - unfolding poly_def by (simp add: poly_rec_pCons)
1.1496 -
1.1497 -lemma poly_1 [simp]: "poly 1 x = 1"
1.1498 - unfolding one_poly_def by simp
1.1499 -
1.1500 -lemma poly_monom:
1.1501 - fixes a x :: "'a::{comm_semiring_1}"
1.1502 - shows "poly (monom a n) x = a * x ^ n"
1.1503 - by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)
1.1504 -
1.1505 -lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
1.1506 - apply (induct p arbitrary: q, simp)
1.1507 - apply (case_tac q, simp, simp add: algebra_simps)
1.1508 +lemma pdivmod_fold_coeffs [code]:
1.1509 + "pdivmod p q = (if q = 0 then (0, p)
1.1510 + else fold_coeffs (\<lambda>a (s, r).
1.1511 + let b = coeff (pCons a r) (degree q) / coeff q (degree q)
1.1512 + in (pCons b s, pCons a r - smult b q)
1.1513 + ) p (0, 0))"
1.1514 + apply (cases "q = 0")
1.1515 + apply (simp add: pdivmod_def)
1.1516 + apply (rule sym)
1.1517 + apply (induct p)
1.1518 + apply (simp_all add: pdivmod_0 pdivmod_pCons)
1.1519 + apply (case_tac "a = 0 \<and> p = 0")
1.1520 + apply (auto simp add: pdivmod_def)
1.1521 done
1.1522
1.1523 -lemma poly_minus [simp]:
1.1524 - fixes x :: "'a::comm_ring"
1.1525 - shows "poly (- p) x = - poly p x"
1.1526 - by (induct p, simp_all)
1.1527 -
1.1528 -lemma poly_diff [simp]:
1.1529 - fixes x :: "'a::comm_ring"
1.1530 - shows "poly (p - q) x = poly p x - poly q x"
1.1531 - by (simp add: diff_minus)
1.1532 -
1.1533 -lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
1.1534 - by (cases "finite A", induct set: finite, simp_all)
1.1535 -
1.1536 -lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x"
1.1537 - by (induct p, simp, simp add: algebra_simps)
1.1538 -
1.1539 -lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
1.1540 - by (induct p, simp_all, simp add: algebra_simps)
1.1541 -
1.1542 -lemma poly_power [simp]:
1.1543 - fixes p :: "'a::{comm_semiring_1} poly"
1.1544 - shows "poly (p ^ n) x = poly p x ^ n"
1.1545 - by (induct n, simp, simp add: power_Suc)
1.1546 -
1.1547 -
1.1548 -subsection {* Synthetic division *}
1.1549 -
1.1550 -text {*
1.1551 - Synthetic division is simply division by the
1.1552 - linear polynomial @{term "x - c"}.
1.1553 -*}
1.1554 -
1.1555 -definition
1.1556 - synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
1.1557 -where
1.1558 - "synthetic_divmod p c =
1.1559 - poly_rec (0, 0) (\<lambda>a p (q, r). (pCons r q, a + c * r)) p"
1.1560 -
1.1561 -definition
1.1562 - synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
1.1563 -where
1.1564 - "synthetic_div p c = fst (synthetic_divmod p c)"
1.1565 -
1.1566 -lemma synthetic_divmod_0 [simp]:
1.1567 - "synthetic_divmod 0 c = (0, 0)"
1.1568 - unfolding synthetic_divmod_def
1.1569 - by (simp add: poly_rec_0)
1.1570 -
1.1571 -lemma synthetic_divmod_pCons [simp]:
1.1572 - "synthetic_divmod (pCons a p) c =
1.1573 - (\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)"
1.1574 - unfolding synthetic_divmod_def
1.1575 - by (simp add: poly_rec_pCons)
1.1576 -
1.1577 -lemma snd_synthetic_divmod: "snd (synthetic_divmod p c) = poly p c"
1.1578 - by (induct p, simp, simp add: split_def)
1.1579 -
1.1580 -lemma synthetic_div_0 [simp]: "synthetic_div 0 c = 0"
1.1581 - unfolding synthetic_div_def by simp
1.1582 -
1.1583 -lemma synthetic_div_pCons [simp]:
1.1584 - "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)"
1.1585 - unfolding synthetic_div_def
1.1586 - by (simp add: split_def snd_synthetic_divmod)
1.1587 -
1.1588 -lemma synthetic_div_eq_0_iff:
1.1589 - "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
1.1590 - by (induct p, simp, case_tac p, simp)
1.1591 -
1.1592 -lemma degree_synthetic_div:
1.1593 - "degree (synthetic_div p c) = degree p - 1"
1.1594 - by (induct p, simp, simp add: synthetic_div_eq_0_iff)
1.1595 -
1.1596 -lemma synthetic_div_correct:
1.1597 - "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
1.1598 - by (induct p) simp_all
1.1599 -
1.1600 -lemma synthetic_div_unique_lemma: "smult c p = pCons a p \<Longrightarrow> p = 0"
1.1601 -by (induct p arbitrary: a) simp_all
1.1602 -
1.1603 -lemma synthetic_div_unique:
1.1604 - "p + smult c q = pCons r q \<Longrightarrow> r = poly p c \<and> q = synthetic_div p c"
1.1605 -apply (induct p arbitrary: q r)
1.1606 -apply (simp, frule synthetic_div_unique_lemma, simp)
1.1607 -apply (case_tac q, force)
1.1608 -done
1.1609 -
1.1610 -lemma synthetic_div_correct':
1.1611 - fixes c :: "'a::comm_ring_1"
1.1612 - shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p"
1.1613 - using synthetic_div_correct [of p c]
1.1614 - by (simp add: algebra_simps)
1.1615 -
1.1616 -lemma poly_eq_0_iff_dvd:
1.1617 - fixes c :: "'a::idom"
1.1618 - shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p"
1.1619 -proof
1.1620 - assume "poly p c = 0"
1.1621 - with synthetic_div_correct' [of c p]
1.1622 - have "p = [:-c, 1:] * synthetic_div p c" by simp
1.1623 - then show "[:-c, 1:] dvd p" ..
1.1624 -next
1.1625 - assume "[:-c, 1:] dvd p"
1.1626 - then obtain k where "p = [:-c, 1:] * k" by (rule dvdE)
1.1627 - then show "poly p c = 0" by simp
1.1628 -qed
1.1629 -
1.1630 -lemma dvd_iff_poly_eq_0:
1.1631 - fixes c :: "'a::idom"
1.1632 - shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0"
1.1633 - by (simp add: poly_eq_0_iff_dvd)
1.1634 -
1.1635 -lemma poly_roots_finite:
1.1636 - fixes p :: "'a::idom poly"
1.1637 - shows "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}"
1.1638 -proof (induct n \<equiv> "degree p" arbitrary: p)
1.1639 - case (0 p)
1.1640 - then obtain a where "a \<noteq> 0" and "p = [:a:]"
1.1641 - by (cases p, simp split: if_splits)
1.1642 - then show "finite {x. poly p x = 0}" by simp
1.1643 -next
1.1644 - case (Suc n p)
1.1645 - show "finite {x. poly p x = 0}"
1.1646 - proof (cases "\<exists>x. poly p x = 0")
1.1647 - case False
1.1648 - then show "finite {x. poly p x = 0}" by simp
1.1649 - next
1.1650 - case True
1.1651 - then obtain a where "poly p a = 0" ..
1.1652 - then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd)
1.1653 - then obtain k where k: "p = [:-a, 1:] * k" ..
1.1654 - with `p \<noteq> 0` have "k \<noteq> 0" by auto
1.1655 - with k have "degree p = Suc (degree k)"
1.1656 - by (simp add: degree_mult_eq del: mult_pCons_left)
1.1657 - with `Suc n = degree p` have "n = degree k" by simp
1.1658 - then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps)
1.1659 - then have "finite (insert a {x. poly k x = 0})" by simp
1.1660 - then show "finite {x. poly p x = 0}"
1.1661 - by (simp add: k uminus_add_conv_diff Collect_disj_eq
1.1662 - del: mult_pCons_left)
1.1663 - qed
1.1664 -qed
1.1665 -
1.1666 -lemma poly_zero:
1.1667 - fixes p :: "'a::{idom,ring_char_0} poly"
1.1668 - shows "poly p = poly 0 \<longleftrightarrow> p = 0"
1.1669 -apply (cases "p = 0", simp_all)
1.1670 -apply (drule poly_roots_finite)
1.1671 -apply (auto simp add: infinite_UNIV_char_0)
1.1672 -done
1.1673 -
1.1674 -lemma poly_eq_iff:
1.1675 - fixes p q :: "'a::{idom,ring_char_0} poly"
1.1676 - shows "poly p = poly q \<longleftrightarrow> p = q"
1.1677 - using poly_zero [of "p - q"]
1.1678 - by (simp add: fun_eq_iff)
1.1679 -
1.1680 -
1.1681 -subsection {* Composition of polynomials *}
1.1682 -
1.1683 -definition
1.1684 - pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
1.1685 -where
1.1686 - "pcompose p q = poly_rec 0 (\<lambda>a _ c. [:a:] + q * c) p"
1.1687 -
1.1688 -lemma pcompose_0 [simp]: "pcompose 0 q = 0"
1.1689 - unfolding pcompose_def by (simp add: poly_rec_0)
1.1690 -
1.1691 -lemma pcompose_pCons:
1.1692 - "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
1.1693 - unfolding pcompose_def by (simp add: poly_rec_pCons)
1.1694 -
1.1695 -lemma poly_pcompose: "poly (pcompose p q) x = poly p (poly q x)"
1.1696 - by (induct p) (simp_all add: pcompose_pCons)
1.1697 -
1.1698 -lemma degree_pcompose_le:
1.1699 - "degree (pcompose p q) \<le> degree p * degree q"
1.1700 -apply (induct p, simp)
1.1701 -apply (simp add: pcompose_pCons, clarify)
1.1702 -apply (rule degree_add_le, simp)
1.1703 -apply (rule order_trans [OF degree_mult_le], simp)
1.1704 -done
1.1705 -
1.1706
1.1707 subsection {* Order of polynomial roots *}
1.1708
1.1709 -definition
1.1710 - order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
1.1711 +definition order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
1.1712 where
1.1713 "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
1.1714
1.1715 @@ -1490,107 +1764,161 @@
1.1716 done
1.1717
1.1718
1.1719 -subsection {* Configuration of the code generator *}
1.1720 +subsection {* GCD of polynomials *}
1.1721
1.1722 -code_datatype "0::'a::zero poly" pCons
1.1723 -
1.1724 -quickcheck_generator poly constructors: "0::'a::zero poly", pCons
1.1725 -
1.1726 -instantiation poly :: ("{zero, equal}") equal
1.1727 +instantiation poly :: (field) gcd
1.1728 begin
1.1729
1.1730 -definition
1.1731 - "HOL.equal (p::'a poly) q \<longleftrightarrow> p = q"
1.1732 +function gcd_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
1.1733 +where
1.1734 + "gcd (x::'a poly) 0 = smult (inverse (coeff x (degree x))) x"
1.1735 +| "y \<noteq> 0 \<Longrightarrow> gcd (x::'a poly) y = gcd y (x mod y)"
1.1736 +by auto
1.1737
1.1738 -instance proof
1.1739 -qed (rule equal_poly_def)
1.1740 +termination "gcd :: _ poly \<Rightarrow> _"
1.1741 +by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))")
1.1742 + (auto dest: degree_mod_less)
1.1743 +
1.1744 +declare gcd_poly.simps [simp del]
1.1745 +
1.1746 +instance ..
1.1747
1.1748 end
1.1749
1.1750 -lemma eq_poly_code [code]:
1.1751 - "HOL.equal (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
1.1752 - "HOL.equal (0::_ poly) (pCons b q) \<longleftrightarrow> HOL.equal 0 b \<and> HOL.equal 0 q"
1.1753 - "HOL.equal (pCons a p) (0::_ poly) \<longleftrightarrow> HOL.equal a 0 \<and> HOL.equal p 0"
1.1754 - "HOL.equal (pCons a p) (pCons b q) \<longleftrightarrow> HOL.equal a b \<and> HOL.equal p q"
1.1755 - by (simp_all add: equal)
1.1756 +lemma
1.1757 + fixes x y :: "_ poly"
1.1758 + shows poly_gcd_dvd1 [iff]: "gcd x y dvd x"
1.1759 + and poly_gcd_dvd2 [iff]: "gcd x y dvd y"
1.1760 + apply (induct x y rule: gcd_poly.induct)
1.1761 + apply (simp_all add: gcd_poly.simps)
1.1762 + apply (fastforce simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
1.1763 + apply (blast dest: dvd_mod_imp_dvd)
1.1764 + done
1.1765
1.1766 -lemma [code nbe]:
1.1767 - "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
1.1768 - by (fact equal_refl)
1.1769 +lemma poly_gcd_greatest:
1.1770 + fixes k x y :: "_ poly"
1.1771 + shows "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd gcd x y"
1.1772 + by (induct x y rule: gcd_poly.induct)
1.1773 + (simp_all add: gcd_poly.simps dvd_mod dvd_smult)
1.1774
1.1775 -lemmas coeff_code [code] =
1.1776 - coeff_0 coeff_pCons_0 coeff_pCons_Suc
1.1777 +lemma dvd_poly_gcd_iff [iff]:
1.1778 + fixes k x y :: "_ poly"
1.1779 + shows "k dvd gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
1.1780 + by (blast intro!: poly_gcd_greatest intro: dvd_trans)
1.1781
1.1782 -lemmas degree_code [code] =
1.1783 - degree_0 degree_pCons_eq_if
1.1784 +lemma poly_gcd_monic:
1.1785 + fixes x y :: "_ poly"
1.1786 + shows "coeff (gcd x y) (degree (gcd x y)) =
1.1787 + (if x = 0 \<and> y = 0 then 0 else 1)"
1.1788 + by (induct x y rule: gcd_poly.induct)
1.1789 + (simp_all add: gcd_poly.simps nonzero_imp_inverse_nonzero)
1.1790
1.1791 -lemmas monom_poly_code [code] =
1.1792 - monom_0 monom_Suc
1.1793 +lemma poly_gcd_zero_iff [simp]:
1.1794 + fixes x y :: "_ poly"
1.1795 + shows "gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
1.1796 + by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff)
1.1797
1.1798 -lemma add_poly_code [code]:
1.1799 - "0 + q = (q :: _ poly)"
1.1800 - "p + 0 = (p :: _ poly)"
1.1801 - "pCons a p + pCons b q = pCons (a + b) (p + q)"
1.1802 -by simp_all
1.1803 +lemma poly_gcd_0_0 [simp]:
1.1804 + "gcd (0::_ poly) 0 = 0"
1.1805 + by simp
1.1806
1.1807 -lemma minus_poly_code [code]:
1.1808 - "- 0 = (0 :: _ poly)"
1.1809 - "- pCons a p = pCons (- a) (- p)"
1.1810 -by simp_all
1.1811 +lemma poly_dvd_antisym:
1.1812 + fixes p q :: "'a::idom poly"
1.1813 + assumes coeff: "coeff p (degree p) = coeff q (degree q)"
1.1814 + assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
1.1815 +proof (cases "p = 0")
1.1816 + case True with coeff show "p = q" by simp
1.1817 +next
1.1818 + case False with coeff have "q \<noteq> 0" by auto
1.1819 + have degree: "degree p = degree q"
1.1820 + using `p dvd q` `q dvd p` `p \<noteq> 0` `q \<noteq> 0`
1.1821 + by (intro order_antisym dvd_imp_degree_le)
1.1822
1.1823 -lemma diff_poly_code [code]:
1.1824 - "0 - q = (- q :: _ poly)"
1.1825 - "p - 0 = (p :: _ poly)"
1.1826 - "pCons a p - pCons b q = pCons (a - b) (p - q)"
1.1827 -by simp_all
1.1828 + from `p dvd q` obtain a where a: "q = p * a" ..
1.1829 + with `q \<noteq> 0` have "a \<noteq> 0" by auto
1.1830 + with degree a `p \<noteq> 0` have "degree a = 0"
1.1831 + by (simp add: degree_mult_eq)
1.1832 + with coeff a show "p = q"
1.1833 + by (cases a, auto split: if_splits)
1.1834 +qed
1.1835
1.1836 -lemmas smult_poly_code [code] =
1.1837 - smult_0_right smult_pCons
1.1838 +lemma poly_gcd_unique:
1.1839 + fixes d x y :: "_ poly"
1.1840 + assumes dvd1: "d dvd x" and dvd2: "d dvd y"
1.1841 + and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d"
1.1842 + and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)"
1.1843 + shows "gcd x y = d"
1.1844 +proof -
1.1845 + have "coeff (gcd x y) (degree (gcd x y)) = coeff d (degree d)"
1.1846 + by (simp_all add: poly_gcd_monic monic)
1.1847 + moreover have "gcd x y dvd d"
1.1848 + using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest)
1.1849 + moreover have "d dvd gcd x y"
1.1850 + using dvd1 dvd2 by (rule poly_gcd_greatest)
1.1851 + ultimately show ?thesis
1.1852 + by (rule poly_dvd_antisym)
1.1853 +qed
1.1854
1.1855 -lemma mult_poly_code [code]:
1.1856 - "0 * q = (0 :: _ poly)"
1.1857 - "pCons a p * q = smult a q + pCons 0 (p * q)"
1.1858 -by simp_all
1.1859 +interpretation gcd_poly!: abel_semigroup "gcd :: _ poly \<Rightarrow> _"
1.1860 +proof
1.1861 + fix x y z :: "'a poly"
1.1862 + show "gcd (gcd x y) z = gcd x (gcd y z)"
1.1863 + by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
1.1864 + show "gcd x y = gcd y x"
1.1865 + by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
1.1866 +qed
1.1867
1.1868 -lemmas poly_code [code] =
1.1869 - poly_0 poly_pCons
1.1870 +lemmas poly_gcd_assoc = gcd_poly.assoc
1.1871 +lemmas poly_gcd_commute = gcd_poly.commute
1.1872 +lemmas poly_gcd_left_commute = gcd_poly.left_commute
1.1873
1.1874 -lemmas synthetic_divmod_code [code] =
1.1875 - synthetic_divmod_0 synthetic_divmod_pCons
1.1876 +lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
1.1877
1.1878 -text {* code generator setup for div and mod *}
1.1879 +lemma poly_gcd_1_left [simp]: "gcd 1 y = (1 :: _ poly)"
1.1880 +by (rule poly_gcd_unique) simp_all
1.1881
1.1882 -definition
1.1883 - pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
1.1884 +lemma poly_gcd_1_right [simp]: "gcd x 1 = (1 :: _ poly)"
1.1885 +by (rule poly_gcd_unique) simp_all
1.1886 +
1.1887 +lemma poly_gcd_minus_left [simp]: "gcd (- x) y = gcd x (y :: _ poly)"
1.1888 +by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
1.1889 +
1.1890 +lemma poly_gcd_minus_right [simp]: "gcd x (- y) = gcd x (y :: _ poly)"
1.1891 +by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
1.1892 +
1.1893 +lemma poly_gcd_code [code]:
1.1894 + "gcd x y = (if y = 0 then smult (inverse (coeff x (degree x))) x else gcd y (x mod (y :: _ poly)))"
1.1895 + by (simp add: gcd_poly.simps)
1.1896 +
1.1897 +
1.1898 +subsection {* Composition of polynomials *}
1.1899 +
1.1900 +definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
1.1901 where
1.1902 - "pdivmod x y = (x div y, x mod y)"
1.1903 + "pcompose p q = fold_coeffs (\<lambda>a c. [:a:] + q * c) p 0"
1.1904
1.1905 -lemma div_poly_code [code]: "x div y = fst (pdivmod x y)"
1.1906 - unfolding pdivmod_def by simp
1.1907 +lemma pcompose_0 [simp]:
1.1908 + "pcompose 0 q = 0"
1.1909 + by (simp add: pcompose_def)
1.1910
1.1911 -lemma mod_poly_code [code]: "x mod y = snd (pdivmod x y)"
1.1912 - unfolding pdivmod_def by simp
1.1913 +lemma pcompose_pCons:
1.1914 + "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
1.1915 + by (cases "p = 0 \<and> a = 0") (auto simp add: pcompose_def)
1.1916
1.1917 -lemma pdivmod_0 [code]: "pdivmod 0 y = (0, 0)"
1.1918 - unfolding pdivmod_def by simp
1.1919 +lemma poly_pcompose:
1.1920 + "poly (pcompose p q) x = poly p (poly q x)"
1.1921 + by (induct p) (simp_all add: pcompose_pCons)
1.1922
1.1923 -lemma pdivmod_pCons [code]:
1.1924 - "pdivmod (pCons a x) y =
1.1925 - (if y = 0 then (0, pCons a x) else
1.1926 - (let (q, r) = pdivmod x y;
1.1927 - b = coeff (pCons a r) (degree y) / coeff y (degree y)
1.1928 - in (pCons b q, pCons a r - smult b y)))"
1.1929 -apply (simp add: pdivmod_def Let_def, safe)
1.1930 -apply (rule div_poly_eq)
1.1931 -apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
1.1932 -apply (rule mod_poly_eq)
1.1933 -apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
1.1934 +lemma degree_pcompose_le:
1.1935 + "degree (pcompose p q) \<le> degree p * degree q"
1.1936 +apply (induct p, simp)
1.1937 +apply (simp add: pcompose_pCons, clarify)
1.1938 +apply (rule degree_add_le, simp)
1.1939 +apply (rule order_trans [OF degree_mult_le], simp)
1.1940 done
1.1941
1.1942 -lemma poly_gcd_code [code]:
1.1943 - "poly_gcd x y =
1.1944 - (if y = 0 then smult (inverse (coeff x (degree x))) x
1.1945 - else poly_gcd y (x mod y))"
1.1946 - by (simp add: poly_gcd.simps)
1.1947 +
1.1948 +no_notation cCons (infixr "##" 65)
1.1949
1.1950 end
1.1951 +
2.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Sat Jul 20 08:07:39 2013 +0200
2.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Sun Jul 21 15:08:31 2013 +0200
2.3 @@ -168,7 +168,8 @@
2.4 function make_primes :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list" where
2.5 "make_primes last_p n ps =
2.6 (if n \<le> last ps then ps
2.7 - else make_primes (last_p + 2) n (if is_prime ps (last_p + 2) then ps @ [last_p + 2] else ps))"
2.8 + else make_primes (last_p + 2) n
2.9 + (if is_prime ps (last_p + 2) then ps @ [last_p + 2] else ps))"
2.10 by pat_completeness auto --"simp del: is_prime.simps <-- declare"
2.11 termination make_primes (*by lexicographic_order +PROOF primes? / size_change LOOPS*)
2.12 sorry -- {* FIXME proof needs semantic properties of primes themselves *}
2.13 @@ -274,7 +275,7 @@
2.14 (* degree *)
2.15 definition deg_up :: "unipoly \<Rightarrow> nat" where
2.16 "deg_up p = ((\<lambda>k. k - 1) o length o drop_tl_zeros) p"
2.17 - (* WRONG: (op - 1) o *)
2.18 + (* FH wrong: (op - 1) o *)
2.19
2.20 value "degree (Coeff [1::int, 2, 3])"
2.21 value "deg_up [1, 2, 3]"
2.22 @@ -324,7 +325,7 @@
2.23 THUS TYPE CONSTRAINED...
2.24 *)
2.25 definition swapf1 :: "(int \<Rightarrow> int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where "swapf1 f a b = f b a"
2.26 -definition div_ups :: "unipoly \<Rightarrow> int \<Rightarrow> unipoly" (infixl "%'/" (* %/ error FLORIAN 5*) 70) where
2.27 +definition div_ups :: "unipoly \<Rightarrow> int \<Rightarrow> unipoly" (infixl "%'/" 70) where
2.28 "p %/ m = map (swapf1 op div2 m) p"
2.29
2.30 value "[4, 3, 2, 5, 6] %/ 3 = [1, 1, 0, 1, 2]"
2.31 @@ -344,8 +345,8 @@
2.32 value "[8, 7, 6, 5, 4] %-% [2, 2, 3, 1, 1] = [6, 5, 3, 4, 3]"
2.33
2.34 function (sequential) dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "%|%" 70) where
2.35 -"[d] %|% [p] \<longleftrightarrow> (\<bar>d\<bar> \<le> \<bar>p\<bar>) \<and> (p mod d = 0)" |
2.36 -"ds %|% ps \<longleftrightarrow>
2.37 +"[d] %|% [p] \<longleftrightarrow> (\<bar>d\<bar> \<le> \<bar>p\<bar>) \<and> (p mod d = 0)" |
2.38 +"ds %|% ps \<longleftrightarrow> (*a hint by FH*)
2.39 (let
2.40 ds = drop_tl_zeros ds; ps = drop_tl_zeros ps;
2.41 d000 = (List.replicate (List.length ps - List.length ds) 0) @ ds;
2.42 @@ -359,7 +360,7 @@
2.43 centr_up_def normalise.simps mod_up_gcd.simps lcoeff_up.simps*)
2.44 termination (*dvd_up: by lexicographic_order LOOPS +PROOF primes? / size_change LOOPS*)
2.45 using [[linarith_split_limit = 999]]
2.46 -apply (relation "measure (\<lambda>(_, ps). length ps)")
2.47 +apply (relation "measure (\<lambda>(_, ps). length ps)") (*a hint by FH*)
2.48 apply auto
2.49 sorry
2.50
3.1 --- a/src/Tools/isac/calcelems.sml Sat Jul 20 08:07:39 2013 +0200
3.2 +++ b/src/Tools/isac/calcelems.sml Sun Jul 21 15:08:31 2013 +0200
3.3 @@ -634,8 +634,10 @@
3.4 *)
3.5 end;
3.6
3.7 -fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
3.8 - (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;
3.9 +fun term2str t =
3.10 + let
3.11 + val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory "Isac"));
3.12 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
3.13
3.14 fun terms2str ts = (strs2str o (map term2str )) ts;
3.15 (*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
4.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Jul 20 08:07:39 2013 +0200
4.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sun Jul 21 15:08:31 2013 +0200
4.3 @@ -660,6 +660,7 @@
4.4 of simplification occurs right here, in the next step.*}
4.5
4.6 ML {*
4.7 + trace_rewrite := false;
4.8 val SOME fract1 =
4.9 parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
4.10 (*
5.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Sat Jul 20 08:07:39 2013 +0200
5.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Sun Jul 21 15:08:31 2013 +0200
5.3 @@ -156,7 +156,7 @@
5.4 text {* The simplifiers are quite busy when finding the above results. you can
5.5 watch them at work by setting the switch 'trace_rewrite:*}
5.6 ML {*
5.7 -trace_rewrite := true;
5.8 +trace_rewrite := false;
5.9 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
5.10 val SOME (t, _) = rewrite_set_ thy true norm_Rational t2; term2str t;
5.11 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test.thy Sun Jul 21 15:08:31 2013 +0200
6.3 @@ -0,0 +1,80 @@
6.4 +(* Title: test/Tools/isac/ADDTESTS/file-depend
6.5 + Author: Walther Neuper 2009
6.6 +*)
6.7 +
6.8 +header {* Test file dependencies analogous to ISAC
6.9 +
6.10 +$ cd /usr/local/isabisac/test/Tools/isac/ADDTESTS/file-depend
6.11 +$ /usr/local/isabisac/bin/isabelle jedit Build_Test.thy &
6.12 +*}
6.13 +(*----------------------------------------------------------------------------
6.14 +theory Build_Test
6.15 +imports
6.16 + Complex_Main
6.17 + "1language/Foo_Language"
6.18 + "3knowledge/Foo_KnowALL"
6.19 +begin
6.20 +----------------------------------------------------------------------------*)
6.21 +
6.22 +theory BuildC_Test (*Duplicate theory name
6.23 + {..., Foo_Language, Foo_Know111, Foo_Know222, Foo_KnowALL, Build_Test}
6.24 + {..., Nitpick, Main, testdir1, testdirm, Build_Test}*)
6.25 +imports
6.26 + Complex_Main
6.27 + "~~/test/Tools/isac/ADDTESTS/file-depend/1language/Foo_Language"
6.28 + "~~/test/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_KnowALL"
6.29 +uses
6.30 + ("~~/test/Tools/isac/ADDTESTS/file-depend/0foolibrary.ML")
6.31 + ("~~/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML")
6.32 +begin
6.33 + use "~~/test/Tools/isac/ADDTESTS/file-depend/0foolibrary.ML"
6.34 + ML {* val Free ("b", _) = foolibrhs @{term "a = b"} *}
6.35 +(*use_thy "1language/Foo_Language" --- is done by import above*)
6.36 + ML {* val Const ("Foo_Language.fooprog", _) = @{term fooprog} *}
6.37 + use "~~/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML"
6.38 + ML {* val Free ("b", _) = foointerpret @{term "fooprog (a = b)"} *}
6.39 +
6.40 +text {* the different theories of knowledge are recognized, Const bar*: *}
6.41 +ML {*
6.42 +val trm = Syntax.read_term_global @{theory Foo_Know111}
6.43 + "fooprog (foo111 = bar111)";
6.44 +val Const ("Foo_Know111.bar111", _) = foointerpret trm;
6.45 +
6.46 +val trm = Syntax.read_term_global @{theory Foo_Know222}
6.47 + "fooprog (foo222 = bar222)";
6.48 +val Const ("Foo_Know222.bar222", _) = foointerpret trm;
6.49 +*}
6.50 +
6.51 +text {* the different theories of knowledge are recognized, Free bar*: *}
6.52 +ML {*
6.53 +val trm = Syntax.read_term_global @{theory Foo_Know111}
6.54 + "fooprog (foo222 = bar222)";
6.55 +(*Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $
6.56 + (Const ("HOL.eq", "'a => 'a => bool") $ Free ("foo222", "'a") $
6.57 + Free ("bar222", "'a"))
6.58 + : term*)
6.59 +
6.60 +val trm = Syntax.read_term_global @{theory Foo_Know222}
6.61 + "fooprog (foo111 = bar111)";
6.62 +(*val trm =
6.63 + Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $
6.64 + (Const ("HOL.eq", "'a => 'a => bool") $ Free ("foo111", "'a") $
6.65 + Free ("bar111", "'a"))
6.66 + : term*)
6.67 +*}
6.68 +
6.69 +text {* dir structure reflects ISAC, see Build_Isac.thy:
6.70 +/file-depend/0foolibrary.ML
6.71 +/file-depend/Build_Test.thy
6.72 +/file-depend/README
6.73 +
6.74 +/file-depend/1language/Foo_Language.thy
6.75 +
6.76 +/file-depend/2interpreter/2foointerpreter.ML
6.77 +
6.78 +/file-depend/3knowledge/Foo_Know111.thy
6.79 +/file-depend/3knowledge/Foo_Know222.thy
6.80 +/file-depend/3knowledge/Foo_KnowALL.thy
6.81 +*}
6.82 +
6.83 +end
6.84 \ No newline at end of file
7.1 --- a/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy Sat Jul 20 08:07:39 2013 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,78 +0,0 @@
7.4 -(* Title: test/Tools/isac/ADDTESTS/file-depend
7.5 - Author: Walther Neuper 2009
7.6 -*)
7.7 -
7.8 -header {* Test file dependencies analogous to ISAC
7.9 -
7.10 -$ cd /usr/local/isabisac/test/Tools/isac/ADDTESTS/file-depend
7.11 -$ /usr/local/isabisac/bin/isabelle jedit Build_Test.thy &
7.12 -*}
7.13 -(*----------------------------------------------------------------------------
7.14 -theory Build_Test
7.15 -imports
7.16 - Complex_Main
7.17 - "1language/Foo_Language"
7.18 - "3knowledge/Foo_KnowALL"
7.19 -begin
7.20 -----------------------------------------------------------------------------*)
7.21 -
7.22 -theory Build_Test
7.23 -imports
7.24 - Complex_Main
7.25 - "~~/test/Tools/isac/ADDTESTS/file-depend/1language/Foo_Language"
7.26 - "~~/test/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_KnowALL"
7.27 -uses
7.28 - ("~~/test/Tools/isac/ADDTESTS/file-depend/0foolibrary.ML")
7.29 - ("~~/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML")
7.30 -begin
7.31 - use "~~/test/Tools/isac/ADDTESTS/file-depend/0foolibrary.ML"
7.32 - ML {* val Free ("b", _) = foolibrhs @{term "a = b"} *}
7.33 -(*use_thy "1language/Foo_Language" --- is done by import above*)
7.34 - ML {* val Const ("Foo_Language.fooprog", _) = @{term fooprog} *}
7.35 - use "~~/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML"
7.36 - ML {* val Free ("b", _) = foointerpret @{term "fooprog (a = b)"} *}
7.37 -
7.38 -text {* the different theories of knowledge are recognized, Const bar*: *}
7.39 -ML {*
7.40 -val trm = Syntax.read_term_global @{theory Foo_Know111}
7.41 - "fooprog (foo111 = bar111)";
7.42 -val Const ("Foo_Know111.bar111", _) = foointerpret trm;
7.43 -
7.44 -val trm = Syntax.read_term_global @{theory Foo_Know222}
7.45 - "fooprog (foo222 = bar222)";
7.46 -val Const ("Foo_Know222.bar222", _) = foointerpret trm;
7.47 -*}
7.48 -
7.49 -text {* the different theories of knowledge are recognized, Free bar*: *}
7.50 -ML {*
7.51 -val trm = Syntax.read_term_global @{theory Foo_Know111}
7.52 - "fooprog (foo222 = bar222)";
7.53 -(*Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $
7.54 - (Const ("HOL.eq", "'a => 'a => bool") $ Free ("foo222", "'a") $
7.55 - Free ("bar222", "'a"))
7.56 - : term*)
7.57 -
7.58 -val trm = Syntax.read_term_global @{theory Foo_Know222}
7.59 - "fooprog (foo111 = bar111)";
7.60 -(*val trm =
7.61 - Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $
7.62 - (Const ("HOL.eq", "'a => 'a => bool") $ Free ("foo111", "'a") $
7.63 - Free ("bar111", "'a"))
7.64 - : term*)
7.65 -*}
7.66 -
7.67 -text {* dir structure reflects ISAC, see Build_Isac.thy:
7.68 -/file-depend/0foolibrary.ML
7.69 -/file-depend/Build_Test.thy
7.70 -/file-depend/README
7.71 -
7.72 -/file-depend/1language/Foo_Language.thy
7.73 -
7.74 -/file-depend/2interpreter/2foointerpreter.ML
7.75 -
7.76 -/file-depend/3knowledge/Foo_Know111.thy
7.77 -/file-depend/3knowledge/Foo_Know222.thy
7.78 -/file-depend/3knowledge/Foo_KnowALL.thy
7.79 -*}
7.80 -
7.81 -end
7.82 \ No newline at end of file
8.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Sat Jul 20 08:07:39 2013 +0200
8.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Sun Jul 21 15:08:31 2013 +0200
8.3 @@ -6,6 +6,7 @@
8.4 use"diffapp.sml";
8.5 *)
8.6
8.7 +trace_rewrite := false;
8.8 "Contents----------------------------------------------";
8.9 " Specify_Problem (match_itms_oris) ";
8.10 " test specify, fmz <> [] ";
9.1 --- a/test/Tools/isac/Knowledge/equation.sml Sat Jul 20 08:07:39 2013 +0200
9.2 +++ b/test/Tools/isac/Knowledge/equation.sml Sun Jul 21 15:08:31 2013 +0200
9.3 @@ -17,15 +17,18 @@
9.4 "----------- CAS input -------------------------------------------";
9.5 "----------- CAS input -------------------------------------------";
9.6 "----------- CAS input -------------------------------------------";
9.7 +trace_rewrite := false;
9.8 states:=[];
9.9 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
9.10 Iterator 1;
9.11 moveActiveRoot 1;
9.12 replaceFormula 1 "solve (x+1=2, x)";
9.13 +(*========== inhibit exn 130719 Isabelle2013 ===================================loops
9.14 autoCalculate 1 CompleteCalc;
9.15 val ((pt,p),_) = get_calc 1;
9.16 val Form res = (#1 o pt_extract) (pt, ([],Res));
9.17 show_pt pt;
9.18 if p = ([], Res) andalso term2str res = "[x = 1]" then ()
9.19 else error "equation.sml behav.changed for CAS solve (x+1=2, x))";
9.20 +============ inhibit exn 130719 Isabelle2013 =================================*)
9.21
10.1 --- a/test/Tools/isac/Knowledge/gcd_poly.sml Sat Jul 20 08:07:39 2013 +0200
10.2 +++ b/test/Tools/isac/Knowledge/gcd_poly.sml Sun Jul 21 15:08:31 2013 +0200
10.3 @@ -395,8 +395,7 @@
10.4
10.5 if try_new_prime_up a b d M P g p = [~1, 1, ~1] then () else error "try_new_prime_up changed";
10.6
10.7 -"----------- output from changeset cf55b1438731";
10.8 -(*
10.9 +(* ---- output from changeset cf55b1438731
10.10 try_new_prime_up: a = [~18, ~15, ~20, 12, 20, ~13, 2], b = [8, 28, 22, ~11, ~14, 1, 2],
10.11 d = 2, M = 10240, P = 12597, g = [~1, 1, ~1], p = 19
10.12 try_new_prime_up 1 -----> [~1, 1, ~1] *)
10.13 @@ -407,7 +406,7 @@
10.14 if try_new_prime_up a b d M P g p = [~1, 1, ~1]
10.15 then () else error "try_new_prime_up I [~18, ~15, ... changed";
10.16
10.17 -(* output from changeset cf55b1438731
10.18 +(* ---- output from changeset cf55b1438731
10.19 try_new_prime_up: a = [~18, ~15, ~20, 12, 20, ~13, 2], b = [8, 28, 22, ~11, ~14, 1, 2],
10.20 d = 2, M = 10240, P = 96577, g = [~4, ~2, 2], p = 23
10.21 try_new_prime_up 1 -----> [~4, ~2, 2] *)
11.1 --- a/test/Tools/isac/Test_Isac.thy Sat Jul 20 08:07:39 2013 +0200
11.2 +++ b/test/Tools/isac/Test_Isac.thy Sun Jul 21 15:08:31 2013 +0200
11.3 @@ -1,149 +1,79 @@
11.4 -(* Title: All tests on isac; observe outcommented
11.5 +(* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
11.6 Author: Walther Neuper 101001
11.7 (c) copyright due to lincense terms.
11.8
11.9 -$ cd /usr/local/isabisac/test/Tools/isac
11.10 -$ /usr/local/isabisac/bin/isabelle jedit -l Isac Test_Isac.thy &
11.11 + isac tests
11.12 + in ~~/test/Tools/isac are structured according
11.13 + to ~~/src/Tools/isac
11.14 + Additional tests are in
11.15 + ~~/test/Tools/isac/ADDTESTS
11.16 + ~~/test/Tools/isac/Minisubpbl
11.17 +
11.18 +$ cd /usr/local/isabisac/
11.19 +$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
11.20 *)
11.21
11.22 -theory Test_Isac imports "~~/src/Tools/isac/Build_Isac"
11.23 +theory Test_Isac imports Isac
11.24 "ADDTESTS/Ctxt"
11.25 "ADDTESTS/test-depend/Build_Test"
11.26 "ADDTESTS/All_Ctxt"
11.27 "ADDTESTS/course/phst11/T1_Basics"
11.28 "ADDTESTS/course/phst11/T2_Rewriting"
11.29 "ADDTESTS/course/phst11/T3_MathEngine"
11.30 - "ADDTESTS/file-depend/Build_Test"
11.31 + "ADDTESTS/file-depend/BuildC_Test"
11.32 "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
11.33 "../../Pure/Isar/Test_Parsers"
11.34 (*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
11.35 "../../Pure/Isar/Test_Parse_Term"
11.36
11.37 -uses
11.38 - ( "library.sml")
11.39 - ( "calcelems.sml")
11.40 - ("ProgLang/termC.sml")
11.41 - ("ProgLang/calculate.sml")
11.42 - ("ProgLang/rewrite.sml")
11.43 - (*"ProgLang/listC.sml"*)
11.44 - ("ProgLang/scrtools.sml")
11.45 - ("ProgLang/tools.sml")
11.46 -
11.47 - ("Minisubpbl/000-comments.sml")
11.48 - ("Minisubpbl/100-init-rootpbl.sml")
11.49 - ("Minisubpbl/150-add-given.sml")
11.50 - ("Minisubpbl/200-start-method.sml")
11.51 - ("Minisubpbl/300-init-subpbl.sml")
11.52 - ("Minisubpbl/400-start-meth-subpbl.sml")
11.53 - ("Minisubpbl/490-nxt-Check_Postcond.sml")
11.54 - ("Minisubpbl/500-met-sub-to-root.sml")
11.55 - ("Minisubpbl/530-error-Check_Elementwise.sml")
11.56 - ("Minisubpbl/600-postcond.sml")
11.57 -
11.58 - ("Interpret/mstools.sml")
11.59 - ("Interpret/ctree.sml")
11.60 - ("Interpret/ptyps.sml")
11.61 - ("Interpret/generate.sml")
11.62 - ("Interpret/calchead.sml")
11.63 - ("Interpret/appl.sml")
11.64 - ("Interpret/rewtools.sml")
11.65 - ("Interpret/script.sml")
11.66 - ("Interpret/solve.sml")
11.67 - ("Interpret/inform.sml")
11.68 - ("Interpret/mathengine.sml")
11.69 -
11.70 - ("xmlsrc/mathml.sml")
11.71 - ("xmlsrc/datatypes.sml")
11.72 - ("xmlsrc/pbl-met-hierarchy.sml")
11.73 - (*"xmlsrc/thy-hierarchy.sml"*)
11.74 - ("xmlsrc/interface-xml.sml")
11.75 -
11.76 - ("Frontend/messages.sml")
11.77 - ("Frontend/states.sml")
11.78 - ("Frontend/interface.sml")
11.79 - ("print_exn_G.sml")
11.80 -
11.81 - ("Knowledge/delete.sml")
11.82 - ("Knowledge/descript.sml")
11.83 - ("Knowledge/atools.sml")
11.84 - ("Knowledge/simplify.sml")
11.85 - ("Knowledge/poly.sml")
11.86 -(*THIS WAITS UNTIL Isabelle2013: ("Knowledge/gcd_poly.sml") ("Knowledge/gcd_poly_winkler.sml")
11.87 - IN THIS SEQUENCE: SEE Test_Some2.thy*)
11.88 - (*"Knowledge/rational.sml"*)
11.89 - ("Knowledge/equation.sml")
11.90 - ("Knowledge/root.sml")
11.91 - ("Knowledge/lineq.sml")
11.92 - (*"Knowledge/rooteq.sml"*)
11.93 - ("Knowledge/rateq.sml")
11.94 - ("Knowledge/rootrateq.sml")
11.95 - ("Knowledge/polyeq.sml")
11.96 - ("Knowledge/calculus.sml")
11.97 - ("Knowledge/trig.sml")
11.98 - (*"Knowledge/logexp.sml"*)
11.99 - ("Knowledge/diff.sml")
11.100 - ("Knowledge/integrate.sml")
11.101 - ("Knowledge/eqsystem.sml")
11.102 - ("Knowledge/test.sml")
11.103 - ("Knowledge/partial_fractions.sml")
11.104 - ("Knowledge/polyminus.sml")
11.105 - ("Knowledge/vect.sml")
11.106 - ("Knowledge/diffapp.sml")
11.107 - ("Knowledge/biegelinie.sml")
11.108 - ("Knowledge/algein.sml")
11.109 - ("Knowledge/diophanteq.sml")
11.110 - ("Knowledge/Inverse_Z_Transform/inverse_z_transform.sml")
11.111 - ("Knowledge/isac.sml")
11.112 - ("Knowledge/build_thydata.sml")
11.113 -
11.114 begin
11.115 section {* test ML Code of isac *}
11.116 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
11.117 - use "library.sml"
11.118 - use "calcelems.sml"
11.119 - use "ProgLang/termC.sml"
11.120 - use "ProgLang/calculate.sml"
11.121 - use "ProgLang/rewrite.sml"
11.122 -(*use "ProgLang/listC.sml" 2002*)
11.123 - use "ProgLang/scrtools.sml"
11.124 - use "ProgLang/tools.sml"
11.125 + ML_file "library.sml"
11.126 + ML_file "calcelems.sml"
11.127 + ML_file "ProgLang/termC.sml"
11.128 + ML_file "ProgLang/calculate.sml"
11.129 + ML_file "ProgLang/rewrite.sml"
11.130 +(*ML_file "ProgLang/listC.sml" 2002*)
11.131 + ML_file "ProgLang/scrtools.sml"
11.132 + ML_file "ProgLang/tools.sml"
11.133 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
11.134 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
11.135 - use "Minisubpbl/000-comments.sml"
11.136 - use "Minisubpbl/100-init-rootpbl.sml"
11.137 - use "Minisubpbl/150-add-given.sml"
11.138 - use "Minisubpbl/200-start-method.sml"
11.139 - use "Minisubpbl/300-init-subpbl.sml"
11.140 - use "Minisubpbl/400-start-meth-subpbl.sml"
11.141 - use "Minisubpbl/490-nxt-Check_Postcond.sml"
11.142 - use "Minisubpbl/500-met-sub-to-root.sml"
11.143 - use "Minisubpbl/530-error-Check_Elementwise.sml"
11.144 - use "Minisubpbl/600-postcond.sml"
11.145 + ML_file "Minisubpbl/000-comments.sml"
11.146 + ML_file "Minisubpbl/100-init-rootpbl.sml"
11.147 + ML_file "Minisubpbl/150-add-given.sml"
11.148 + ML_file "Minisubpbl/200-start-method.sml"
11.149 + ML_file "Minisubpbl/300-init-subpbl.sml"
11.150 + ML_file "Minisubpbl/400-start-meth-subpbl.sml"
11.151 + ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
11.152 + ML_file "Minisubpbl/500-met-sub-to-root.sml"
11.153 + ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
11.154 + ML_file "Minisubpbl/600-postcond.sml"
11.155 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
11.156 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
11.157 - use "Interpret/mstools.sml"
11.158 - use "Interpret/ctree.sml" (*!...!see(25)*)
11.159 - use "Interpret/ptyps.sml"
11.160 + ML_file "Interpret/mstools.sml"
11.161 + ML_file "Interpret/ctree.sml" (*!...!see(25)*)
11.162 + ML_file "Interpret/ptyps.sml"
11.163 ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
11.164 (*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
11.165 - use "Interpret/generate.sml"
11.166 + ML_file "Interpret/generate.sml"
11.167 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
11.168 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
11.169 - use "Interpret/calchead.sml"
11.170 - use "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
11.171 - use "Interpret/rewtools.sml" (*complete, isac's Context broken at 2009-2 --> 2011, thehier!*)
11.172 - use "Interpret/script.sml"
11.173 - use "Interpret/solve.sml"
11.174 - use "Interpret/inform.sml"
11.175 + ML_file "Interpret/calchead.sml"
11.176 + ML_file "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
11.177 + ML_file "Interpret/rewtools.sml" (*complete, isac's Context broken at 2009-2 --> 2011, thehier!*)
11.178 + ML_file "Interpret/script.sml"
11.179 + ML_file "Interpret/solve.sml"
11.180 + ML_file "Interpret/inform.sml"
11.181 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
11.182 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
11.183 - use "Interpret/mathengine.sml" (*!part.*)
11.184 + ML_file "Interpret/mathengine.sml" (*!part.*)
11.185 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
11.186 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
11.187 - use "xmlsrc/mathml.sml" (*part.*)
11.188 - use "xmlsrc/datatypes.sml" (*TODO/part.*)
11.189 - use "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
11.190 -(*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2/part | Isabelle2012-->13 !thehier! *)
11.191 + ML_file "xmlsrc/mathml.sml" (*part.*)
11.192 + ML_file "xmlsrc/datatypes.sml" (*TODO/part.*)
11.193 + ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
11.194 +(*ML_file "xmlsrc/thy-hierarchy.sml" TODO after 2009-2/part | Isabelle2012-->13 !thehier! *)
11.195 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
11.196 val it = "----------- ### thes2file ... Exception- Match raised -----------": string
11.197 :
11.198 @@ -153,52 +83,52 @@
11.199 exception Bind raised (line 359 of "~~/test/Tools/isac/xmlsrc/thy-hierarchy.sml")
11.200 ...CONCERNED WITH thehier
11.201 *)
11.202 - use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
11.203 + ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
11.204 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
11.205 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
11.206 - use "Frontend/messages.sml"
11.207 - use "Frontend/states.sml"
11.208 - use "Frontend/interface.sml"
11.209 + ML_file "Frontend/messages.sml"
11.210 + ML_file "Frontend/states.sml"
11.211 + ML_file "Frontend/interface.sml"
11.212 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
11.213 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
11.214 - use "print_exn_G.sml"
11.215 + ML_file "print_exn_G.sml"
11.216 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
11.217 ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*}
11.218 - use "Knowledge/delete.sml"
11.219 - use "Knowledge/descript.sml"
11.220 - use "Knowledge/atools.sml"
11.221 - use "Knowledge/simplify.sml"
11.222 - use "Knowledge/poly.sml"
11.223 + ML_file "Knowledge/delete.sml"
11.224 + ML_file "Knowledge/descript.sml"
11.225 + ML_file "Knowledge/atools.sml"
11.226 + ML_file "Knowledge/simplify.sml"
11.227 + ML_file "Knowledge/poly.sml"
11.228 (*THIS WAITS UNTIL Isabelle2013 IN THIS SEQUENCE (SEE Test_Some2.thy):0
11.229 - use "Knowledge/gcd_poly.sml" (*type error 'nth' etc*)
11.230 - use "Knowledge/gcd_poly_winkler.sml"*)
11.231 -(*use "Knowledge/rational.sml" WN120317.TODO postponed to joint work with dmeindl *)
11.232 - use "Knowledge/equation.sml"
11.233 - use "Knowledge/root.sml"
11.234 - use "Knowledge/lineq.sml"
11.235 -(*use "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
11.236 - use "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
11.237 - use "Knowledge/rootrat.sml"
11.238 - use "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
11.239 - use "Knowledge/partial_fractions.sml"
11.240 - use "Knowledge/polyeq.sml"
11.241 -(*use "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *)
11.242 - use "Knowledge/calculus.sml"
11.243 - use "Knowledge/trig.sml"
11.244 -(*use "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
11.245 - use "Knowledge/diff.sml"
11.246 - use "Knowledge/integrate.sml"
11.247 - use "Knowledge/eqsystem.sml"
11.248 - use "Knowledge/test.sml"
11.249 - use "Knowledge/polyminus.sml"
11.250 - use "Knowledge/vect.sml"
11.251 - use "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
11.252 - use "Knowledge/biegelinie.sml"
11.253 - use "Knowledge/algein.sml"
11.254 - use "Knowledge/diophanteq.sml"
11.255 - use "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
11.256 - use "Knowledge/isac.sml"
11.257 - use "Knowledge/build_thydata.sml"
11.258 + ML_file "Knowledge/gcd_poly.sml" (*type error 'nth' etc*)
11.259 + ML_file "Knowledge/gcd_poly_winkler.sml"*)
11.260 +(*ML_file "Knowledge/rational.sml" WN120317.TODO postponed to joint work with dmeindl *)
11.261 + ML_file "Knowledge/equation.sml"
11.262 + ML_file "Knowledge/root.sml"
11.263 + ML_file "Knowledge/lineq.sml"
11.264 +(*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
11.265 + ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
11.266 + ML_file "Knowledge/rootrat.sml"
11.267 + ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
11.268 + ML_file "Knowledge/partial_fractions.sml"
11.269 + ML_file "Knowledge/polyeq.sml"
11.270 +(*ML_file "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *)
11.271 + ML_file "Knowledge/calculus.sml"
11.272 + ML_file "Knowledge/trig.sml"
11.273 +(*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
11.274 + ML_file "Knowledge/diff.sml"
11.275 + ML_file "Knowledge/integrate.sml"
11.276 + ML_file "Knowledge/eqsystem.sml"
11.277 + ML_file "Knowledge/test.sml"
11.278 + ML_file "Knowledge/polyminus.sml"
11.279 + ML_file "Knowledge/vect.sml"
11.280 + ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
11.281 + ML_file "Knowledge/biegelinie.sml"
11.282 + ML_file "Knowledge/algein.sml"
11.283 + ML_file "Knowledge/diophanteq.sml"
11.284 + ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
11.285 + ML_file "Knowledge/isac.sml"
11.286 + ML_file "Knowledge/build_thydata.sml"
11.287 ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}
11.288 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
11.289 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
11.290 @@ -385,10 +315,9 @@
11.291 *}
11.292
11.293 end
11.294 -(*========== inhibit exn 110628 ================================================
11.295 -============ inhibit exn 110628 ==============================================*)
11.296 +(*========== inhibit exn 130719 Isabelle2013 ===================================
11.297 +============ inhibit exn 130719 Isabelle2013 =================================*)
11.298
11.299 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
11.300 -Pending source file dependencies: "Knowledge/algein.sml"
11.301 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
11.302
12.1 --- a/test/Tools/isac/Test_Some.thy Sat Jul 20 08:07:39 2013 +0200
12.2 +++ b/test/Tools/isac/Test_Some.thy Sun Jul 21 15:08:31 2013 +0200
12.3 @@ -1,19 +1,20 @@
12.4
12.5 -theory Test_Some imports Isac
12.6 - uses ("~~/test/Tools/isac/Interpret/inform.sml")
12.7 -begin
12.8 - use "~~/test/Tools/isac/Interpret/inform.sml"
12.9 -
12.10 +theory Test_Some imports Isac begin
12.11 + ML_file "ProgLang/calculate.sml"
12.12 +(*
12.13 declare [[show_types]]
12.14 declare [[show_sorts]]
12.15 find_theorems "?a <= ?a"
12.16
12.17 print_facts
12.18 print_statement ""
12.19 -print_theory
12.20 +print_theory
12.21 +*)
12.22
12.23 ML {*
12.24 *}
12.25 +ML {*
12.26 +*}
12.27 ML {* (*==================*)
12.28 *}
12.29 ML {*