src/HOL/Library/Polynomial.thy
changeset 60679 ade12ef2773c
parent 60570 7ed2cde6806d
child 60685 cb21b7022b00
     1.1 --- a/src/HOL/Library/Polynomial.thy	Mon Jul 06 22:06:02 2015 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Jul 06 22:57:34 2015 +0200
     1.3 @@ -392,13 +392,12 @@
     1.4  definition
     1.5    [code]: "HOL.equal (p::'a poly) q \<longleftrightarrow> HOL.equal (coeffs p) (coeffs q)"
     1.6  
     1.7 -instance proof
     1.8 -qed (simp add: equal equal_poly_def coeffs_eq_iff)
     1.9 +instance
    1.10 +  by standard (simp add: equal equal_poly_def coeffs_eq_iff)
    1.11  
    1.12  end
    1.13  
    1.14 -lemma [code nbe]:
    1.15 -  "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
    1.16 +lemma [code nbe]: "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
    1.17    by (fact equal_refl)
    1.18  
    1.19  definition is_zero :: "'a::zero poly \<Rightarrow> bool"
    1.20 @@ -510,15 +509,16 @@
    1.21  lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
    1.22    is "\<lambda>p q n. coeff p n + coeff q n"
    1.23  proof -
    1.24 -  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
    1.25 +  fix q p :: "'a poly"
    1.26 +  show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
    1.27      using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
    1.28  qed
    1.29  
    1.30 -lemma coeff_add [simp]:
    1.31 -  "coeff (p + q) n = coeff p n + coeff q n"
    1.32 +lemma coeff_add [simp]: "coeff (p + q) n = coeff p n + coeff q n"
    1.33    by (simp add: plus_poly.rep_eq)
    1.34  
    1.35 -instance proof
    1.36 +instance
    1.37 +proof
    1.38    fix p q r :: "'a poly"
    1.39    show "(p + q) + r = p + (q + r)"
    1.40      by (simp add: poly_eq_iff add.assoc)
    1.41 @@ -536,15 +536,16 @@
    1.42  lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
    1.43    is "\<lambda>p q n. coeff p n - coeff q n"
    1.44  proof -
    1.45 -  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
    1.46 +  fix q p :: "'a poly"
    1.47 +  show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
    1.48      using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
    1.49  qed
    1.50  
    1.51 -lemma coeff_diff [simp]:
    1.52 -  "coeff (p - q) n = coeff p n - coeff q n"
    1.53 +lemma coeff_diff [simp]: "coeff (p - q) n = coeff p n - coeff q n"
    1.54    by (simp add: minus_poly.rep_eq)
    1.55  
    1.56 -instance proof
    1.57 +instance
    1.58 +proof
    1.59    fix p q r :: "'a poly"
    1.60    show "p + q - p = q"
    1.61      by (simp add: poly_eq_iff)
    1.62 @@ -560,14 +561,16 @@
    1.63  lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
    1.64    is "\<lambda>p n. - coeff p n"
    1.65  proof -
    1.66 -  fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
    1.67 +  fix p :: "'a poly"
    1.68 +  show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
    1.69      using MOST_coeff_eq_0 by simp
    1.70  qed
    1.71  
    1.72  lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
    1.73    by (simp add: uminus_poly.rep_eq)
    1.74  
    1.75 -instance proof
    1.76 +instance
    1.77 +proof
    1.78    fix p q :: "'a poly"
    1.79    show "- p + p = 0"
    1.80      by (simp add: poly_eq_iff)
    1.81 @@ -663,7 +666,8 @@
    1.82    { fix xs ys :: "'a list" and n
    1.83      have "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
    1.84      proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
    1.85 -      case (3 x xs y ys n) then show ?case by (cases n) (auto simp add: cCons_def)
    1.86 +      case (3 x xs y ys n)
    1.87 +      then show ?case by (cases n) (auto simp add: cCons_def)
    1.88      qed simp_all }
    1.89    note * = this
    1.90    { fix xs ys :: "'a list"
    1.91 @@ -825,7 +829,8 @@
    1.92    shows "(p + q) * r = p * r + q * r"
    1.93    by (induct r) (simp add: mult_poly_0, simp add: smult_distribs algebra_simps)
    1.94  
    1.95 -instance proof
    1.96 +instance
    1.97 +proof
    1.98    fix p q r :: "'a poly"
    1.99    show 0: "0 * p = 0"
   1.100      by (rule mult_poly_0_left)
   1.101 @@ -861,18 +866,17 @@
   1.102  done
   1.103  
   1.104  lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
   1.105 -  by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)
   1.106 +  by (induct m) (simp add: monom_0 smult_monom, simp add: monom_Suc)
   1.107  
   1.108  instantiation poly :: (comm_semiring_1) comm_semiring_1
   1.109  begin
   1.110  
   1.111 -definition one_poly_def:
   1.112 -  "1 = pCons 1 0"
   1.113 +definition one_poly_def: "1 = pCons 1 0"
   1.114  
   1.115 -instance proof
   1.116 -  fix p :: "'a poly" show "1 * p = p"
   1.117 +instance
   1.118 +proof
   1.119 +  show "1 * p = p" for p :: "'a poly"
   1.120      unfolding one_poly_def by simp
   1.121 -next
   1.122    show "0 \<noteq> (1::'a poly)"
   1.123      unfolding one_poly_def by simp
   1.124  qed
   1.125 @@ -1063,8 +1067,9 @@
   1.126  definition
   1.127    "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   1.128  
   1.129 -instance proof
   1.130 -  fix x y :: "'a poly"
   1.131 +instance
   1.132 +proof
   1.133 +  fix x y z :: "'a poly"
   1.134    show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
   1.135      unfolding less_eq_poly_def less_poly_def
   1.136      apply safe
   1.137 @@ -1072,50 +1077,34 @@
   1.138      apply (drule (1) pos_poly_add)
   1.139      apply simp
   1.140      done
   1.141 -next
   1.142 -  fix x :: "'a poly" show "x \<le> x"
   1.143 +  show "x \<le> x"
   1.144      unfolding less_eq_poly_def by simp
   1.145 -next
   1.146 -  fix x y z :: "'a poly"
   1.147 -  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
   1.148 +  show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
   1.149      unfolding less_eq_poly_def
   1.150      apply safe
   1.151      apply (drule (1) pos_poly_add)
   1.152      apply (simp add: algebra_simps)
   1.153      done
   1.154 -next
   1.155 -  fix x y :: "'a poly"
   1.156 -  assume "x \<le> y" and "y \<le> x" thus "x = y"
   1.157 +  show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
   1.158      unfolding less_eq_poly_def
   1.159      apply safe
   1.160      apply (drule (1) pos_poly_add)
   1.161      apply simp
   1.162      done
   1.163 -next
   1.164 -  fix x y z :: "'a poly"
   1.165 -  assume "x \<le> y" thus "z + x \<le> z + y"
   1.166 +  show "x \<le> y \<Longrightarrow> z + x \<le> z + y"
   1.167      unfolding less_eq_poly_def
   1.168      apply safe
   1.169      apply (simp add: algebra_simps)
   1.170      done
   1.171 -next
   1.172 -  fix x y :: "'a poly"
   1.173    show "x \<le> y \<or> y \<le> x"
   1.174      unfolding less_eq_poly_def
   1.175      using pos_poly_total [of "x - y"]
   1.176      by auto
   1.177 -next
   1.178 -  fix x y z :: "'a poly"
   1.179 -  assume "x < y" and "0 < z"
   1.180 -  thus "z * x < z * y"
   1.181 +  show "x < y \<Longrightarrow> 0 < z \<Longrightarrow> z * x < z * y"
   1.182      unfolding less_poly_def
   1.183      by (simp add: right_diff_distrib [symmetric] pos_poly_mult)
   1.184 -next
   1.185 -  fix x :: "'a poly"
   1.186    show "\<bar>x\<bar> = (if x < 0 then - x else x)"
   1.187      by (rule abs_poly_def)
   1.188 -next
   1.189 -  fix x :: "'a poly"
   1.190    show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   1.191      by (rule sgn_poly_def)
   1.192  qed
   1.193 @@ -1410,7 +1399,8 @@
   1.194      by (simp add: div_poly_eq mod_poly_eq)
   1.195  qed
   1.196  
   1.197 -instance proof
   1.198 +instance
   1.199 +proof
   1.200    fix x y :: "'a poly"
   1.201    show "x div y * y + x mod y = x"
   1.202      using pdivmod_rel [of x y]