tuned proofs -- fewer warnings;
authorwenzelm
Sun Aug 25 17:17:48 2013 +0200 (2013-08-25)
changeset 5319114ab2f821e1d
parent 53190 5d92649a310e
child 53192 04df1d236e1c
tuned proofs -- fewer warnings;
src/HOL/Library/Cardinality.thy
src/HOL/Library/Univ_Poly.thy
     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.9  by (simp add: poly_minus_def)
    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.25 -apply (auto simp add: mult_zero_left poly_ident_mult padd_commut)
    2.26 +apply (auto simp add: padd_commut)
    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.34 -    by (cases p2, simp_all  add: add_ac distrib_left)
    2.35 +    by (cases p2) (simp_all  add: add_ac distrib_left)
    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.42  apply (simp add: poly_minus_def)
    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.73 -        by (simp add: poly_add poly_cmult minus_mult_left[symmetric])}
    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.84  by (simp add: poly_entire)
    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.91 -by (auto simp add: algebra_simps poly_add poly_minus_def fun_eq poly_cmult minus_mult_left[symmetric])
    2.92 +by (auto simp add: algebra_simps poly_add poly_minus_def fun_eq poly_cmult)
    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.96 +by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult distrib_left)
    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.103 -    by (auto intro: ext simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff)
   2.104 +    by (auto intro: simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff)
   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.112 -apply (auto simp add: right_minus poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
   2.113 +apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
   2.114  apply (rule_tac x = "pmult qa q" in exI)
   2.115  apply (rule_tac [2] x = "pmult p qa" in exI)
   2.116  apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
   2.117 @@ -556,7 +558,7 @@
   2.118        apply simp
   2.119        apply (simp only: fun_eq)
   2.120        apply (rule ccontr)
   2.121 -      apply (simp add: fun_eq poly_add poly_cmult minus_mult_left[symmetric])
   2.122 +      apply (simp add: fun_eq poly_add poly_cmult)
   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.148 -apply (simp add: poly_add poly_cmult minus_mult_left[symmetric])
   2.149 +apply (simp add: poly_add poly_cmult)
   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)"
   2.186      by (rule ext) (simp add: poly_mult poly_add poly_cmult)