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.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.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.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.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.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.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.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.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.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.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.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.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]
```