1.1 --- a/src/HOL/Library/Univ_Poly.thy Tue Apr 28 19:15:50 2009 +0200
1.2 +++ b/src/HOL/Library/Univ_Poly.thy Wed Apr 29 14:20:26 2009 +0200
1.3 @@ -167,22 +167,9 @@
1.4 simp_all add: poly_cmult poly_add left_distrib right_distrib mult_ac)
1.5 qed
1.6
1.7 -class recpower_semiring = semiring + recpower
1.8 -class recpower_semiring_1 = semiring_1 + recpower
1.9 -class recpower_semiring_0 = semiring_0 + recpower
1.10 -class recpower_ring = ring + recpower
1.11 -class recpower_ring_1 = ring_1 + recpower
1.12 -subclass (in recpower_ring_1) recpower_ring ..
1.13 -class recpower_comm_semiring_1 = recpower + comm_semiring_1
1.14 -class recpower_comm_ring_1 = recpower + comm_ring_1
1.15 -subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 ..
1.16 -class recpower_idom = recpower + idom
1.17 -subclass (in recpower_idom) recpower_comm_ring_1 ..
1.18 class idom_char_0 = idom + ring_char_0
1.19 -class recpower_idom_char_0 = recpower + idom_char_0
1.20 -subclass (in recpower_idom_char_0) recpower_idom ..
1.21
1.22 -lemma (in recpower_comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
1.23 +lemma (in comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
1.24 apply (induct "n")
1.25 apply (auto simp add: poly_cmult poly_mult power_Suc)
1.26 done
1.27 @@ -418,7 +405,7 @@
1.28 finally show ?thesis .
1.29 qed
1.30
1.31 -lemma (in recpower_idom) poly_exp_eq_zero[simp]:
1.32 +lemma (in idom) poly_exp_eq_zero[simp]:
1.33 "(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)"
1.34 apply (simp only: fun_eq add: all_simps [symmetric])
1.35 apply (rule arg_cong [where f = All])
1.36 @@ -437,7 +424,7 @@
1.37 apply simp
1.38 done
1.39
1.40 -lemma (in recpower_idom) poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])"
1.41 +lemma (in idom) poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])"
1.42 by auto
1.43
1.44 text{*A more constructive notion of polynomials being trivial*}
1.45 @@ -507,7 +494,7 @@
1.46 done
1.47
1.48
1.49 -lemma (in recpower_comm_semiring_1) poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
1.50 +lemma (in comm_semiring_1) poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
1.51 apply (auto simp add: le_iff_add)
1.52 apply (induct_tac k)
1.53 apply (rule_tac [2] poly_divides_trans)
1.54 @@ -516,7 +503,7 @@
1.55 apply (auto simp add: poly_mult fun_eq mult_ac)
1.56 done
1.57
1.58 -lemma (in recpower_comm_semiring_1) poly_exp_divides: "[| (p %^ n) divides q; m\<le>n |] ==> (p %^ m) divides q"
1.59 +lemma (in comm_semiring_1) poly_exp_divides: "[| (p %^ n) divides q; m\<le>n |] ==> (p %^ m) divides q"
1.60 by (blast intro: poly_divides_exp poly_divides_trans)
1.61
1.62 lemma (in comm_semiring_0) poly_divides_add:
1.63 @@ -583,7 +570,7 @@
1.64 qed
1.65
1.66
1.67 -lemma (in recpower_comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
1.68 +lemma (in comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
1.69 by(induct n, auto simp add: poly_mult power_Suc mult_ac)
1.70
1.71 lemma (in comm_semiring_1) divides_left_mult:
1.72 @@ -600,11 +587,11 @@
1.73
1.74 (* FIXME: Tidy up *)
1.75
1.76 -lemma (in recpower_semiring_1)
1.77 +lemma (in semiring_1)
1.78 zero_power_iff: "0 ^ n = (if n = 0 then 1 else 0)"
1.79 by (induct n, simp_all add: power_Suc)
1.80
1.81 -lemma (in recpower_idom_char_0) poly_order_exists:
1.82 +lemma (in idom_char_0) poly_order_exists:
1.83 assumes lp: "length p = d" and p0: "poly p \<noteq> poly []"
1.84 shows "\<exists>n. ([-a, 1] %^ n) divides p & ~(([-a, 1] %^ (Suc n)) divides p)"
1.85 proof-
1.86 @@ -637,7 +624,7 @@
1.87 lemma (in semiring_1) poly_one_divides[simp]: "[1] divides p"
1.88 by (simp add: divides_def, auto)
1.89
1.90 -lemma (in recpower_idom_char_0) poly_order: "poly p \<noteq> poly []
1.91 +lemma (in idom_char_0) poly_order: "poly p \<noteq> poly []
1.92 ==> EX! n. ([-a, 1] %^ n) divides p &
1.93 ~(([-a, 1] %^ (Suc n)) divides p)"
1.94 apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
1.95 @@ -652,7 +639,7 @@
1.96 lemma some1_equalityD: "[| n = (@n. P n); EX! n. P n |] ==> P n"
1.97 by (blast intro: someI2)
1.98
1.99 -lemma (in recpower_idom_char_0) order:
1.100 +lemma (in idom_char_0) order:
1.101 "(([-a, 1] %^ n) divides p &
1.102 ~(([-a, 1] %^ (Suc n)) divides p)) =
1.103 ((n = order a p) & ~(poly p = poly []))"
1.104 @@ -662,17 +649,17 @@
1.105 apply (blast intro!: poly_order [THEN [2] some1_equalityD])
1.106 done
1.107
1.108 -lemma (in recpower_idom_char_0) order2: "[| poly p \<noteq> poly [] |]
1.109 +lemma (in idom_char_0) order2: "[| poly p \<noteq> poly [] |]
1.110 ==> ([-a, 1] %^ (order a p)) divides p &
1.111 ~(([-a, 1] %^ (Suc(order a p))) divides p)"
1.112 by (simp add: order del: pexp_Suc)
1.113
1.114 -lemma (in recpower_idom_char_0) order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p;
1.115 +lemma (in idom_char_0) order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p;
1.116 ~(([-a, 1] %^ (Suc n)) divides p)
1.117 |] ==> (n = order a p)"
1.118 by (insert order [of a n p], auto)
1.119
1.120 -lemma (in recpower_idom_char_0) order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p &
1.121 +lemma (in idom_char_0) order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p &
1.122 ~(([-a, 1] %^ (Suc n)) divides p))
1.123 ==> (n = order a p)"
1.124 by (blast intro: order_unique)
1.125 @@ -692,7 +679,7 @@
1.126 apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
1.127 done
1.128
1.129 -lemma (in recpower_idom_char_0) order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \<noteq> 0)"
1.130 +lemma (in idom_char_0) order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \<noteq> 0)"
1.131 proof-
1.132 let ?poly = poly
1.133 show ?thesis
1.134 @@ -706,7 +693,7 @@
1.135 done
1.136 qed
1.137
1.138 -lemma (in recpower_idom_char_0) order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
1.139 +lemma (in idom_char_0) order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
1.140 proof-
1.141 let ?poly = poly
1.142 show ?thesis
1.143 @@ -718,7 +705,7 @@
1.144 done
1.145 qed
1.146
1.147 -lemma (in recpower_idom_char_0) order_decomp:
1.148 +lemma (in idom_char_0) order_decomp:
1.149 "poly p \<noteq> poly []
1.150 ==> \<exists>q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) &
1.151 ~([-a, 1] divides q)"
1.152 @@ -732,7 +719,7 @@
1.153
1.154 text{*Important composition properties of orders.*}
1.155 lemma order_mult: "poly (p *** q) \<noteq> poly []
1.156 - ==> order a (p *** q) = order a p + order (a::'a::{recpower_idom_char_0}) q"
1.157 + ==> order a (p *** q) = order a p + order (a::'a::{idom_char_0}) q"
1.158 apply (cut_tac a = a and p = "p *** q" and n = "order a p + order a q" in order)
1.159 apply (auto simp add: poly_entire simp del: pmult_Cons)
1.160 apply (drule_tac a = a in order2)+
1.161 @@ -753,7 +740,7 @@
1.162 apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
1.163 done
1.164
1.165 -lemma (in recpower_idom_char_0) order_mult:
1.166 +lemma (in idom_char_0) order_mult:
1.167 assumes pq0: "poly (p *** q) \<noteq> poly []"
1.168 shows "order a (p *** q) = order a p + order a q"
1.169 proof-
1.170 @@ -783,7 +770,7 @@
1.171 done
1.172 qed
1.173
1.174 -lemma (in recpower_idom_char_0) order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order a p \<noteq> 0)"
1.175 +lemma (in idom_char_0) order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order a p \<noteq> 0)"
1.176 by (rule order_root [THEN ssubst], auto)
1.177
1.178 lemma (in semiring_1) pmult_one[simp]: "[1] *** p = p" by auto
1.179 @@ -791,7 +778,7 @@
1.180 lemma (in semiring_0) poly_Nil_zero: "poly [] = poly [0]"
1.181 by (simp add: fun_eq)
1.182
1.183 -lemma (in recpower_idom_char_0) rsquarefree_decomp:
1.184 +lemma (in idom_char_0) rsquarefree_decomp:
1.185 "[| rsquarefree p; poly p a = 0 |]
1.186 ==> \<exists>q. (poly p = poly ([-a, 1] *** q)) & poly q a \<noteq> 0"
1.187 apply (simp add: rsquarefree_def, safe)
1.188 @@ -999,7 +986,7 @@
1.189 ultimately show ?case by blast
1.190 qed
1.191
1.192 -lemma (in recpower_idom_char_0) order_degree:
1.193 +lemma (in idom_char_0) order_degree:
1.194 assumes p0: "poly p \<noteq> poly []"
1.195 shows "order a p \<le> degree p"
1.196 proof-