author wenzelm Sun Aug 25 17:17:48 2013 +0200 (2013-08-25) changeset 53191 14ab2f821e1d parent 53190 5d92649a310e child 53192 04df1d236e1c
tuned proofs -- fewer warnings;
 src/HOL/Library/Cardinality.thy file | annotate | diff | revisions src/HOL/Library/Univ_Poly.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Library/Cardinality.thy	Sun Aug 25 17:04:22 2013 +0200
1.2 +++ b/src/HOL/Library/Cardinality.thy	Sun Aug 25 17:17:48 2013 +0200
1.3 @@ -64,7 +64,7 @@
1.4  proof -
1.5    have "(None :: 'a option) \<notin> range Some" by clarsimp
1.6    thus ?thesis
1.7 -    by(simp add: UNIV_option_conv card_eq_0_iff finite_range_Some card_insert_disjoint card_image)
1.8 +    by (simp add: UNIV_option_conv card_eq_0_iff finite_range_Some card_image)
1.9  qed
1.10
1.11  lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)"
```
```     2.1 --- a/src/HOL/Library/Univ_Poly.thy	Sun Aug 25 17:04:22 2013 +0200
2.2 +++ b/src/HOL/Library/Univ_Poly.thy	Sun Aug 25 17:17:48 2013 +0200
2.3 @@ -97,7 +97,7 @@
2.4  lemma padd_Cons_Cons: "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)"
2.5  by auto
2.6
2.7 -lemma pminus_Nil[simp]: "-- [] = []"
2.8 +lemma pminus_Nil: "-- [] = []"
2.10
2.11  lemma pmult_singleton: "[h1] *** p1 = h1 %* p1" by simp
2.12 @@ -114,7 +114,7 @@
2.13  proof(induct b arbitrary: a)
2.14    case Nil thus ?case by auto
2.15  next
2.16 -  case (Cons b bs a) thus ?case by (cases a, simp_all add: add_commute)
2.17 +  case (Cons b bs a) thus ?case by (cases a) (simp_all add: add_commute)
2.18  qed
2.19
2.20  lemma (in comm_semiring_0) padd_assoc: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
2.21 @@ -130,7 +130,7 @@
2.22
2.23  lemma (in ring_1) pmult_by_x[simp]: "[0, 1] *** t = ((0)#t)"
2.24  apply (induct "t", simp)
2.27  apply (case_tac t, auto)
2.28  done
2.29
2.30 @@ -141,7 +141,7 @@
2.31    case Nil thus ?case by simp
2.32  next
2.33    case (Cons a as p2) thus ?case
2.36  qed
2.37
2.38  lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x"
2.39 @@ -155,7 +155,7 @@
2.40
2.41  lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
2.43 -apply (auto simp add: poly_cmult minus_mult_left[symmetric])
2.44 +apply (auto simp add: poly_cmult)
2.45  done
2.46
2.47  lemma (in comm_semiring_0) poly_mult: "poly (p1 *** p2) x = poly p1 x * poly p2 x"
2.48 @@ -171,7 +171,7 @@
2.49
2.50  lemma (in comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
2.51  apply (induct "n")
2.52 -apply (auto simp add: poly_cmult poly_mult power_Suc)
2.53 +apply (auto simp add: poly_cmult poly_mult)
2.54  done
2.55
2.56  text{*More Polynomial Evaluation Lemmas*}
2.57 @@ -204,8 +204,7 @@
2.58      from Cons.hyps[rule_format, of x]
2.59      obtain q r where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast
2.60      have "h#x#xs = [a*r + h] +++ [-a, 1] *** (r#q)"
2.61 -      using qr by(cases q, simp_all add: algebra_simps diff_minus[symmetric]
2.62 -        minus_mult_left[symmetric] right_minus)
2.63 +      using qr by (cases q) (simp_all add: algebra_simps)
2.64      hence "\<exists>q r. h#x#xs = [r] +++ [-a, 1] *** q" by blast}
2.65    thus ?case by blast
2.66  qed
2.67 @@ -218,9 +217,12 @@
2.68  proof-
2.69    {assume p: "p = []" hence ?thesis by simp}
2.70    moreover
2.71 -  {fix x xs assume p: "p = x#xs"
2.72 -    {fix q assume "p = [-a, 1] *** q" hence "poly p a = 0"
2.74 +  {
2.75 +    fix x xs assume p: "p = x#xs"
2.76 +    {
2.77 +      fix q assume "p = [-a, 1] *** q"
2.78 +      hence "poly p a = 0" by (simp add: poly_add poly_cmult)
2.79 +    }
2.80      moreover
2.81      {assume p0: "poly p a = 0"
2.82        from poly_linear_rem[of x xs a] obtain q r
2.83 @@ -388,20 +390,20 @@
2.85
2.86  lemma fun_eq: " (f = g) = (\<forall>x. f x = g x)"
2.87 -by (auto intro!: ext)
2.88 +by auto
2.89
2.90  lemma (in comm_ring_1) poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)"
2.93
2.94  lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
2.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])
2.97
2.98  subclass (in idom_char_0) comm_ring_1 ..
2.99  lemma (in idom_char_0) poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"
2.100  proof-
2.101    have "poly (p *** q) = poly (p *** r) \<longleftrightarrow> poly (p *** q +++ -- (p *** r)) = poly []" by (simp only: poly_add_minus_zero_iff)
2.102    also have "\<dots> \<longleftrightarrow> poly p = poly [] | poly q = poly r"
2.105    finally show ?thesis .
2.106  qed
2.107
2.108 @@ -474,7 +476,7 @@
2.109  apply (simp add: distrib_right [symmetric])
2.110  apply clarsimp
2.111
2.114  apply (rule_tac x = "pmult qa q" in exI)
2.115  apply (rule_tac [2] x = "pmult p qa" in exI)
2.117 @@ -556,7 +558,7 @@
2.118        apply simp
2.119        apply (simp only: fun_eq)
2.120        apply (rule ccontr)
2.123        done
2.124      from Suc.hyps[OF qh] obtain m r where
2.125        mr: "q = mulexp m [-a,1] r" "poly r a \<noteq> 0" by blast
2.126 @@ -570,7 +572,7 @@
2.127
2.128
2.129  lemma (in comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
2.130 -by(induct n, auto simp add: poly_mult power_Suc mult_ac)
2.131 +  by (induct n) (auto simp add: poly_mult mult_ac)
2.132
2.133  lemma (in comm_semiring_1) divides_left_mult:
2.134    assumes d:"(p***q) divides r" shows "p divides r \<and> q divides r"
2.135 @@ -588,7 +590,7 @@
2.136
2.137  lemma (in semiring_1)
2.138    zero_power_iff: "0 ^ n = (if n = 0 then 1 else 0)"
2.139 -  by (induct n, simp_all add: power_Suc)
2.140 +  by (induct n) simp_all
2.141
2.142  lemma (in idom_char_0) poly_order_exists:
2.143    assumes lp: "length p = d" and p0: "poly p \<noteq> poly []"
2.144 @@ -612,7 +614,7 @@
2.145  apply (induct_tac "n")
2.146  apply (simp del: pmult_Cons pexp_Suc)
2.147  apply (erule_tac Q = "?poly q a = zero" in contrapos_np)
2.150  apply (rule pexp_Suc [THEN ssubst])
2.151  apply (rule ccontr)
2.152  apply (simp add: poly_mult_left_cancel poly_mult_assoc del: pmult_Cons pexp_Suc)
2.153 @@ -664,12 +666,10 @@
2.154  by (blast intro: order_unique)
2.155
2.156  lemma (in ring_1) order_poly: "poly p = poly q ==> order a p = order a q"
2.157 -by (auto simp add: fun_eq divides_def poly_mult order_def)
2.158 +  by (auto simp add: fun_eq divides_def poly_mult order_def)
2.159
2.160  lemma (in semiring_1) pexp_one[simp]: "p %^ (Suc 0) = p"
2.161 -apply (induct "p")
2.162 -apply (auto simp add: numeral_1_eq_1)
2.163 -done
2.164 +  by (induct "p") auto
2.165
2.166  lemma (in comm_ring_1) lemma_order_root:
2.167       " 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
2.168 @@ -914,7 +914,8 @@
2.169
2.170  lemma (in semiring_0) poly_Nil_ext: "poly [] = (\<lambda>x. 0)" by (rule ext) simp
2.171
2.172 -lemma (in idom_char_0) linear_mul_degree: assumes p: "poly p \<noteq> poly []"
2.173 +lemma (in idom_char_0) linear_mul_degree:
2.174 +  assumes p: "poly p \<noteq> poly []"
2.175    shows "degree ([a,1] *** p) = degree p + 1"
2.176  proof-
2.177    from p have pnz: "pnormalize p \<noteq> []"
2.178 @@ -927,7 +928,7 @@
2.179
2.180
2.181    have th: "degree ([a,1] *** pnormalize p) = degree (pnormalize p) + 1"
2.182 -    by (auto simp add: poly_length_mult)
2.183 +    by simp
2.184
2.185    have eqs: "poly ([a,1] *** pnormalize p) = poly ([a,1] *** p)"