src/HOL/Library/Univ_Poly.thy
 changeset 31021 53642251a04f parent 30738 0842e906300c child 32456 341c83339aeb
```     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.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.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.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.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.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-
```