1.1 --- a/src/HOL/Library/Univ_Poly.thy Sun Aug 25 17:04:22 2013 +0200
1.2 +++ b/src/HOL/Library/Univ_Poly.thy Sun Aug 25 17:17:48 2013 +0200
1.3 @@ -97,7 +97,7 @@
1.4 lemma padd_Cons_Cons: "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)"
1.5 by auto
1.6
1.7 -lemma pminus_Nil[simp]: "-- [] = []"
1.8 +lemma pminus_Nil: "-- [] = []"
1.9 by (simp add: poly_minus_def)
1.10
1.11 lemma pmult_singleton: "[h1] *** p1 = h1 %* p1" by simp
1.12 @@ -114,7 +114,7 @@
1.13 proof(induct b arbitrary: a)
1.14 case Nil thus ?case by auto
1.15 next
1.16 - case (Cons b bs a) thus ?case by (cases a, simp_all add: add_commute)
1.17 + case (Cons b bs a) thus ?case by (cases a) (simp_all add: add_commute)
1.18 qed
1.19
1.20 lemma (in comm_semiring_0) padd_assoc: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
1.21 @@ -130,7 +130,7 @@
1.22
1.23 lemma (in ring_1) pmult_by_x[simp]: "[0, 1] *** t = ((0)#t)"
1.24 apply (induct "t", simp)
1.25 -apply (auto simp add: mult_zero_left poly_ident_mult padd_commut)
1.26 +apply (auto simp add: padd_commut)
1.27 apply (case_tac t, auto)
1.28 done
1.29
1.30 @@ -141,7 +141,7 @@
1.31 case Nil thus ?case by simp
1.32 next
1.33 case (Cons a as p2) thus ?case
1.34 - by (cases p2, simp_all add: add_ac distrib_left)
1.35 + by (cases p2) (simp_all add: add_ac distrib_left)
1.36 qed
1.37
1.38 lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x"
1.39 @@ -155,7 +155,7 @@
1.40
1.41 lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
1.42 apply (simp add: poly_minus_def)
1.43 -apply (auto simp add: poly_cmult minus_mult_left[symmetric])
1.44 +apply (auto simp add: poly_cmult)
1.45 done
1.46
1.47 lemma (in comm_semiring_0) poly_mult: "poly (p1 *** p2) x = poly p1 x * poly p2 x"
1.48 @@ -171,7 +171,7 @@
1.49
1.50 lemma (in comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
1.51 apply (induct "n")
1.52 -apply (auto simp add: poly_cmult poly_mult power_Suc)
1.53 +apply (auto simp add: poly_cmult poly_mult)
1.54 done
1.55
1.56 text{*More Polynomial Evaluation Lemmas*}
1.57 @@ -204,8 +204,7 @@
1.58 from Cons.hyps[rule_format, of x]
1.59 obtain q r where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast
1.60 have "h#x#xs = [a*r + h] +++ [-a, 1] *** (r#q)"
1.61 - using qr by(cases q, simp_all add: algebra_simps diff_minus[symmetric]
1.62 - minus_mult_left[symmetric] right_minus)
1.63 + using qr by (cases q) (simp_all add: algebra_simps)
1.64 hence "\<exists>q r. h#x#xs = [r] +++ [-a, 1] *** q" by blast}
1.65 thus ?case by blast
1.66 qed
1.67 @@ -218,9 +217,12 @@
1.68 proof-
1.69 {assume p: "p = []" hence ?thesis by simp}
1.70 moreover
1.71 - {fix x xs assume p: "p = x#xs"
1.72 - {fix q assume "p = [-a, 1] *** q" hence "poly p a = 0"
1.73 - by (simp add: poly_add poly_cmult minus_mult_left[symmetric])}
1.74 + {
1.75 + fix x xs assume p: "p = x#xs"
1.76 + {
1.77 + fix q assume "p = [-a, 1] *** q"
1.78 + hence "poly p a = 0" by (simp add: poly_add poly_cmult)
1.79 + }
1.80 moreover
1.81 {assume p0: "poly p a = 0"
1.82 from poly_linear_rem[of x xs a] obtain q r
1.83 @@ -388,20 +390,20 @@
1.84 by (simp add: poly_entire)
1.85
1.86 lemma fun_eq: " (f = g) = (\<forall>x. f x = g x)"
1.87 -by (auto intro!: ext)
1.88 +by auto
1.89
1.90 lemma (in comm_ring_1) poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)"
1.91 -by (auto simp add: algebra_simps poly_add poly_minus_def fun_eq poly_cmult minus_mult_left[symmetric])
1.92 +by (auto simp add: algebra_simps poly_add poly_minus_def fun_eq poly_cmult)
1.93
1.94 lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
1.95 -by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult distrib_left minus_mult_left[symmetric] minus_mult_right[symmetric])
1.96 +by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult distrib_left)
1.97
1.98 subclass (in idom_char_0) comm_ring_1 ..
1.99 lemma (in idom_char_0) poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"
1.100 proof-
1.101 have "poly (p *** q) = poly (p *** r) \<longleftrightarrow> poly (p *** q +++ -- (p *** r)) = poly []" by (simp only: poly_add_minus_zero_iff)
1.102 also have "\<dots> \<longleftrightarrow> poly p = poly [] | poly q = poly r"
1.103 - by (auto intro: ext simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff)
1.104 + by (auto intro: simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff)
1.105 finally show ?thesis .
1.106 qed
1.107
1.108 @@ -474,7 +476,7 @@
1.109 apply (simp add: distrib_right [symmetric])
1.110 apply clarsimp
1.111
1.112 -apply (auto simp add: right_minus poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
1.113 +apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
1.114 apply (rule_tac x = "pmult qa q" in exI)
1.115 apply (rule_tac [2] x = "pmult p qa" in exI)
1.116 apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
1.117 @@ -556,7 +558,7 @@
1.118 apply simp
1.119 apply (simp only: fun_eq)
1.120 apply (rule ccontr)
1.121 - apply (simp add: fun_eq poly_add poly_cmult minus_mult_left[symmetric])
1.122 + apply (simp add: fun_eq poly_add poly_cmult)
1.123 done
1.124 from Suc.hyps[OF qh] obtain m r where
1.125 mr: "q = mulexp m [-a,1] r" "poly r a \<noteq> 0" by blast
1.126 @@ -570,7 +572,7 @@
1.127
1.128
1.129 lemma (in comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
1.130 -by(induct n, auto simp add: poly_mult power_Suc mult_ac)
1.131 + by (induct n) (auto simp add: poly_mult mult_ac)
1.132
1.133 lemma (in comm_semiring_1) divides_left_mult:
1.134 assumes d:"(p***q) divides r" shows "p divides r \<and> q divides r"
1.135 @@ -588,7 +590,7 @@
1.136
1.137 lemma (in semiring_1)
1.138 zero_power_iff: "0 ^ n = (if n = 0 then 1 else 0)"
1.139 - by (induct n, simp_all add: power_Suc)
1.140 + by (induct n) simp_all
1.141
1.142 lemma (in idom_char_0) poly_order_exists:
1.143 assumes lp: "length p = d" and p0: "poly p \<noteq> poly []"
1.144 @@ -612,7 +614,7 @@
1.145 apply (induct_tac "n")
1.146 apply (simp del: pmult_Cons pexp_Suc)
1.147 apply (erule_tac Q = "?poly q a = zero" in contrapos_np)
1.148 -apply (simp add: poly_add poly_cmult minus_mult_left[symmetric])
1.149 +apply (simp add: poly_add poly_cmult)
1.150 apply (rule pexp_Suc [THEN ssubst])
1.151 apply (rule ccontr)
1.152 apply (simp add: poly_mult_left_cancel poly_mult_assoc del: pmult_Cons pexp_Suc)
1.153 @@ -664,12 +666,10 @@
1.154 by (blast intro: order_unique)
1.155
1.156 lemma (in ring_1) order_poly: "poly p = poly q ==> order a p = order a q"
1.157 -by (auto simp add: fun_eq divides_def poly_mult order_def)
1.158 + by (auto simp add: fun_eq divides_def poly_mult order_def)
1.159
1.160 lemma (in semiring_1) pexp_one[simp]: "p %^ (Suc 0) = p"
1.161 -apply (induct "p")
1.162 -apply (auto simp add: numeral_1_eq_1)
1.163 -done
1.164 + by (induct "p") auto
1.165
1.166 lemma (in comm_ring_1) lemma_order_root:
1.167 " 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
1.168 @@ -914,7 +914,8 @@
1.169
1.170 lemma (in semiring_0) poly_Nil_ext: "poly [] = (\<lambda>x. 0)" by (rule ext) simp
1.171
1.172 -lemma (in idom_char_0) linear_mul_degree: assumes p: "poly p \<noteq> poly []"
1.173 +lemma (in idom_char_0) linear_mul_degree:
1.174 + assumes p: "poly p \<noteq> poly []"
1.175 shows "degree ([a,1] *** p) = degree p + 1"
1.176 proof-
1.177 from p have pnz: "pnormalize p \<noteq> []"
1.178 @@ -927,7 +928,7 @@
1.179
1.180
1.181 have th: "degree ([a,1] *** pnormalize p) = degree (pnormalize p) + 1"
1.182 - by (auto simp add: poly_length_mult)
1.183 + by simp
1.184
1.185 have eqs: "poly ([a,1] *** pnormalize p) = poly ([a,1] *** p)"
1.186 by (rule ext) (simp add: poly_mult poly_add poly_cmult)