tuned proofs;
authorwenzelm
Mon Jun 22 21:07:10 2015 +0200 (2015-06-22)
changeset 605575854821993d2
parent 60556 e7003c8041e2
child 60558 4fcc6861e64f
tuned proofs;
src/HOL/Library/Fundamental_Theorem_Algebra.thy
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jun 22 20:38:38 2015 +0200
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jun 22 21:07:10 2015 +0200
     1.3 @@ -132,9 +132,9 @@
     1.4      by (cases z) auto
     1.5    from md z have xy: "x\<^sup>2 + y\<^sup>2 = 1"
     1.6      by (simp add: cmod_def)
     1.7 -  {
     1.8 -    assume C: "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
     1.9 -    from C z xy have "2 * x \<le> 1" "2 * x \<ge> -1" "2 * y \<le> 1" "2 * y \<ge> -1"
    1.10 +  have False if "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
    1.11 +  proof -
    1.12 +    from that z xy have "2 * x \<le> 1" "2 * x \<ge> -1" "2 * y \<le> 1" "2 * y \<ge> -1"
    1.13        by (simp_all add: cmod_def power2_eq_square algebra_simps)
    1.14      then have "abs (2 * x) \<le> 1" "abs (2 * y) \<le> 1"
    1.15        by simp_all
    1.16 @@ -142,8 +142,9 @@
    1.17        by - (rule power_mono, simp, simp)+
    1.18      then have th0: "4 * x\<^sup>2 \<le> 1" "4 * y\<^sup>2 \<le> 1"
    1.19        by (simp_all add: power_mult_distrib)
    1.20 -    from add_mono[OF th0] xy have False by simp
    1.21 -  }
    1.22 +    from add_mono[OF th0] xy show ?thesis
    1.23 +      by simp
    1.24 +  qed
    1.25    then show ?thesis
    1.26      unfolding linorder_not_le[symmetric] by blast
    1.27  qed
    1.28 @@ -283,27 +284,24 @@
    1.29    let ?w = "Complex x y"
    1.30    from f(1) g(1) have hs: "subseq ?h"
    1.31      unfolding subseq_def by auto
    1.32 -  {
    1.33 -    fix e :: real
    1.34 -    assume ep: "e > 0"
    1.35 -    then have e2: "e/2 > 0"
    1.36 +  have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" if "e > 0" for e
    1.37 +  proof -
    1.38 +    from that have e2: "e/2 > 0"
    1.39        by simp
    1.40      from x[rule_format, OF e2] y[rule_format, OF e2]
    1.41      obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2"
    1.42        and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2"
    1.43        by blast
    1.44 -    {
    1.45 -      fix n
    1.46 -      assume nN12: "n \<ge> N1 + N2"
    1.47 -      then have nN1: "g n \<ge> N1" and nN2: "n \<ge> N2"
    1.48 +    have "cmod (s (?h n) - ?w) < e" if "n \<ge> N1 + N2" for n
    1.49 +    proof -
    1.50 +      from that have nN1: "g n \<ge> N1" and nN2: "n \<ge> N2"
    1.51          using seq_suble[OF g(1), of n] by arith+
    1.52        from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
    1.53 -      have "cmod (s (?h n) - ?w) < e"
    1.54 +      show ?thesis
    1.55          using metric_bound_lemma[of "s (f (g n))" ?w] by simp
    1.56 -    }
    1.57 -    then have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e"
    1.58 -      by blast
    1.59 -  }
    1.60 +    qed
    1.61 +    then show ?thesis by blast
    1.62 +  qed
    1.63    with hs show ?thesis by blast
    1.64  qed
    1.65  
    1.66 @@ -374,34 +372,27 @@
    1.67        by simp
    1.68      then have mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"
    1.69        by blast
    1.70 -    {
    1.71 -      fix x z
    1.72 -      assume H: "cmod z \<le> r" "cmod (poly p z) = - x" "\<not> x < 1"
    1.73 -      then have "- x < 0 "
    1.74 +    have False if "cmod z \<le> r" "cmod (poly p z) = - x" "\<not> x < 1" for x z
    1.75 +    proof -
    1.76 +      from that have "- x < 0 "
    1.77          by arith
    1.78 -      with H(2) norm_ge_zero[of "poly p z"] have False
    1.79 +      with that(2) norm_ge_zero[of "poly p z"] show ?thesis
    1.80          by simp
    1.81 -    }
    1.82 +    qed
    1.83      then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z"
    1.84        by blast
    1.85      from real_sup_exists[OF mth1 mth2] obtain s where
    1.86 -      s: "\<forall>y. (\<exists>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<and> y < x) \<longleftrightarrow> y < s" by blast
    1.87 +      s: "\<forall>y. (\<exists>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<and> y < x) \<longleftrightarrow> y < s"
    1.88 +      by blast
    1.89      let ?m = "- s"
    1.90 -    {
    1.91 -      fix y
    1.92 -      from s[rule_format, of "-y"]
    1.93 -      have "(\<exists>z x. cmod z \<le> r \<and> - (- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y"
    1.94 -        unfolding minus_less_iff[of y ] equation_minus_iff by blast
    1.95 -    }
    1.96 -    note s1 = this[unfolded minus_minus]
    1.97 +    have s1[unfolded minus_minus]:
    1.98 +      "(\<exists>z x. cmod z \<le> r \<and> - (- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y" for y
    1.99 +      using s[rule_format, of "-y"]
   1.100 +      unfolding minus_less_iff[of y] equation_minus_iff by blast
   1.101      from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m"
   1.102        by auto
   1.103 -    {
   1.104 -      fix n :: nat
   1.105 -      from s1[rule_format, of "?m + 1/real (Suc n)"]
   1.106 -      have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)"
   1.107 -        by simp
   1.108 -    }
   1.109 +    have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" for n
   1.110 +      using s1[rule_format, of "?m + 1/real (Suc n)"] by simp
   1.111      then have th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
   1.112      from choice[OF th] obtain g where
   1.113          g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m + 1 /real(Suc n)"
   1.114 @@ -420,14 +411,8 @@
   1.115          from poly_cont[OF e2, of z p] obtain d where
   1.116              d: "d > 0" "\<forall>w. 0<cmod (w - z)\<and> cmod(w - z) < d \<longrightarrow> cmod(poly p w - poly p z) < ?e/2"
   1.117            by blast
   1.118 -        {
   1.119 -          fix w
   1.120 -          assume w: "cmod (w - z) < d"
   1.121 -          have "cmod(poly p w - poly p z) < ?e / 2"
   1.122 -            using d(2)[rule_format, of w] w e by (cases "w = z") simp_all
   1.123 -        }
   1.124 -        note th1 = this
   1.125 -
   1.126 +        have th1: "cmod(poly p w - poly p z) < ?e / 2" if w: "cmod (w - z) < d" for w
   1.127 +          using d(2)[rule_format, of w] w e by (cases "w = z") simp_all
   1.128          from fz(2) d(1) obtain N1 where N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d"
   1.129            by blast
   1.130          from reals_Archimedean2[of "2/?e"] obtain N2 :: nat where N2: "2/?e < real N2"
   1.131 @@ -499,14 +484,13 @@
   1.132      with pCons.hyps obtain r where r: "\<forall>z. r \<le> norm z \<longrightarrow> d + norm a \<le> norm (poly (pCons c cs) z)"
   1.133        by blast
   1.134      let ?r = "1 + \<bar>r\<bar>"
   1.135 -    {
   1.136 -      fix z :: 'a
   1.137 -      assume h: "1 + \<bar>r\<bar> \<le> norm z"
   1.138 +    have "d \<le> norm (poly (pCons a (pCons c cs)) z)" if "1 + \<bar>r\<bar> \<le> norm z" for z
   1.139 +    proof -
   1.140        have r0: "r \<le> norm z"
   1.141 -        using h by arith
   1.142 +        using that by arith
   1.143        from r[rule_format, OF r0] have th0: "d + norm a \<le> 1 * norm(poly (pCons c cs) z)"
   1.144          by arith
   1.145 -      from h have z1: "norm z \<ge> 1"
   1.146 +      from that have z1: "norm z \<ge> 1"
   1.147          by arith
   1.148        from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
   1.149        have th1: "d \<le> norm(z * poly (pCons c cs) z) - norm a"
   1.150 @@ -514,9 +498,9 @@
   1.151        from norm_diff_ineq[of "z * poly (pCons c cs) z" a]
   1.152        have th2: "norm (z * poly (pCons c cs) z) - norm a \<le> norm (poly (pCons a (pCons c cs)) z)"
   1.153          by (simp add: algebra_simps)
   1.154 -      from th1 th2 have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
   1.155 +      from th1 th2 show ?thesis
   1.156          by arith
   1.157 -    }
   1.158 +    qed
   1.159      then show ?thesis by blast
   1.160    next
   1.161      case True
   1.162 @@ -596,7 +580,8 @@
   1.163      from pCons.hyps pCons.prems True show ?thesis
   1.164        apply auto
   1.165        apply (rule_tac x="k+1" in exI)
   1.166 -      apply (rule_tac x="a" in exI, clarsimp)
   1.167 +      apply (rule_tac x="a" in exI)
   1.168 +      apply clarsimp
   1.169        apply (rule_tac x="q" in exI)
   1.170        apply auto
   1.171        done
   1.172 @@ -622,15 +607,15 @@
   1.173      by (simp add: constant_def)
   1.174  next
   1.175    case (pCons c cs)
   1.176 -  {
   1.177 +  have "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)"
   1.178 +  proof
   1.179      assume "\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
   1.180      then have "poly (pCons c cs) x = poly (pCons c cs) y" for x y
   1.181        by (cases "x = 0") auto
   1.182 -    with pCons.prems have False
   1.183 +    with pCons.prems show False
   1.184        by (auto simp add: constant_def)
   1.185 -  }
   1.186 -  then have th: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)" ..
   1.187 -  from poly_decompose_lemma[OF th]
   1.188 +  qed
   1.189 +  from poly_decompose_lemma[OF this]
   1.190    show ?case
   1.191      apply clarsimp
   1.192      apply (rule_tac x="k+1" in exI)
   1.193 @@ -699,16 +684,16 @@
   1.194        by (simp add: poly_eq_iff)
   1.195      have False if h: "\<And>x y. poly ?r x = poly ?r y"
   1.196      proof -
   1.197 -      {
   1.198 -        fix x y
   1.199 +      have "poly q x = poly q y" for x y
   1.200 +      proof -
   1.201          from qr[rule_format, of x] have "poly q x = poly ?r x * ?a0"
   1.202            by auto
   1.203          also have "\<dots> = poly ?r y * ?a0"
   1.204            using h by simp
   1.205          also have "\<dots> = poly q y"
   1.206            using qr[rule_format, of y] by simp
   1.207 -        finally have "poly q x = poly q y" .
   1.208 -      }
   1.209 +        finally show ?thesis .
   1.210 +      qed
   1.211        with qnc show ?thesis
   1.212          unfolding constant_def by blast
   1.213      qed
   1.214 @@ -833,7 +818,8 @@
   1.215      then show ?thesis by auto
   1.216    next
   1.217      case False
   1.218 -    {
   1.219 +    have "\<not> constant (poly (pCons c cs))"
   1.220 +    proof
   1.221        assume nc: "constant (poly (pCons c cs))"
   1.222        from nc[unfolded constant_def, rule_format, of 0]
   1.223        have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto
   1.224 @@ -874,10 +860,11 @@
   1.225              by blast
   1.226          qed
   1.227        qed
   1.228 -    }
   1.229 -    then have nc: "\<not> constant (poly (pCons c cs))"
   1.230 -      using pCons.prems False by blast
   1.231 -    from fundamental_theorem_of_algebra[OF nc] show ?thesis .
   1.232 +      then show False
   1.233 +        using pCons.prems False by blast
   1.234 +    qed
   1.235 +    then show ?thesis
   1.236 +      by (rule fundamental_theorem_of_algebra)
   1.237    qed
   1.238  qed
   1.239  
   1.240 @@ -901,11 +888,11 @@
   1.241      and dpn: "degree p = n"
   1.242      and n0: "n \<noteq> 0"
   1.243    from dpn n0 have pne: "p \<noteq> 0" by auto
   1.244 -  let ?ths = "p dvd (q ^ n)"
   1.245 -  {
   1.246 -    fix a
   1.247 -    assume a: "poly p a = 0"
   1.248 -    have ?ths if oa: "order a p \<noteq> 0"
   1.249 +  show "p dvd (q ^ n)"
   1.250 +  proof (cases "\<exists>a. poly p a = 0")
   1.251 +    case True
   1.252 +    then obtain a where a: "poly p a = 0" ..
   1.253 +    have ?thesis if oa: "order a p \<noteq> 0"
   1.254      proof -
   1.255        let ?op = "order a p"
   1.256        from pne have ap: "([:- a, 1:] ^ ?op) dvd p" "\<not> [:- a, 1:] ^ (Suc ?op) dvd p"
   1.257 @@ -945,73 +932,69 @@
   1.258          next
   1.259            case False
   1.260            with sne dpn s oa have dsn: "degree s < n"
   1.261 -              apply auto
   1.262 -              apply (erule ssubst)
   1.263 -              apply (simp add: degree_mult_eq degree_linear_power)
   1.264 -              done
   1.265 -            {
   1.266 -              fix x assume h: "poly s x = 0"
   1.267 -              {
   1.268 -                assume xa: "x = a"
   1.269 -                from h[unfolded xa poly_eq_0_iff_dvd] obtain u where u: "s = [:- a, 1:] * u"
   1.270 -                  by (rule dvdE)
   1.271 -                have "p = [:- a, 1:] ^ (Suc ?op) * u"
   1.272 -                  apply (subst s)
   1.273 -                  apply (subst u)
   1.274 -                  apply (simp only: power_Suc ac_simps)
   1.275 -                  done
   1.276 -                with ap(2)[unfolded dvd_def] have False
   1.277 -                  by blast
   1.278 -              }
   1.279 -              note xa = this
   1.280 -              from h have "poly p x = 0"
   1.281 -                by (subst s) simp
   1.282 -              with pq0 have "poly q x = 0"
   1.283 +            apply auto
   1.284 +            apply (erule ssubst)
   1.285 +            apply (simp add: degree_mult_eq degree_linear_power)
   1.286 +            done
   1.287 +          have "poly r x = 0" if h: "poly s x = 0" for x
   1.288 +          proof -
   1.289 +            have xa: "x \<noteq> a"
   1.290 +            proof
   1.291 +              assume "x = a"
   1.292 +              from h[unfolded this poly_eq_0_iff_dvd] obtain u where u: "s = [:- a, 1:] * u"
   1.293 +                by (rule dvdE)
   1.294 +              have "p = [:- a, 1:] ^ (Suc ?op) * u"
   1.295 +                apply (subst s)
   1.296 +                apply (subst u)
   1.297 +                apply (simp only: power_Suc ac_simps)
   1.298 +                done
   1.299 +              with ap(2)[unfolded dvd_def] show False
   1.300                  by blast
   1.301 -              with r xa have "poly r x = 0"
   1.302 -                by auto
   1.303 -            }
   1.304 -            note impth = this
   1.305 -            from IH[rule_format, OF dsn, of s r] impth False
   1.306 -            have "s dvd (r ^ (degree s))"
   1.307 +            qed
   1.308 +            from h have "poly p x = 0"
   1.309 +              by (subst s) simp
   1.310 +            with pq0 have "poly q x = 0"
   1.311                by blast
   1.312 -            then obtain u where u: "r ^ (degree s) = s * u" ..
   1.313 -            then have u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
   1.314 -              by (simp only: poly_mult[symmetric] poly_power[symmetric])
   1.315 -            let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
   1.316 -            from oop[of a] dsn have "q ^ n = p * ?w"
   1.317 -              apply -
   1.318 -              apply (subst s)
   1.319 -              apply (subst r)
   1.320 -              apply (simp only: power_mult_distrib)
   1.321 -              apply (subst mult.assoc [where b=s])
   1.322 -              apply (subst mult.assoc [where a=u])
   1.323 -              apply (subst mult.assoc [where b=u, symmetric])
   1.324 -              apply (subst u [symmetric])
   1.325 -              apply (simp add: ac_simps power_add [symmetric])
   1.326 -              done
   1.327 -            then show ?thesis
   1.328 -              unfolding dvd_def by blast
   1.329 +            with r xa show ?thesis
   1.330 +              by auto
   1.331 +          qed
   1.332 +          with IH[rule_format, OF dsn, of s r] False have "s dvd (r ^ (degree s))"
   1.333 +            by blast
   1.334 +          then obtain u where u: "r ^ (degree s) = s * u" ..
   1.335 +          then have u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
   1.336 +            by (simp only: poly_mult[symmetric] poly_power[symmetric])
   1.337 +          let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
   1.338 +          from oop[of a] dsn have "q ^ n = p * ?w"
   1.339 +            apply -
   1.340 +            apply (subst s)
   1.341 +            apply (subst r)
   1.342 +            apply (simp only: power_mult_distrib)
   1.343 +            apply (subst mult.assoc [where b=s])
   1.344 +            apply (subst mult.assoc [where a=u])
   1.345 +            apply (subst mult.assoc [where b=u, symmetric])
   1.346 +            apply (subst u [symmetric])
   1.347 +            apply (simp add: ac_simps power_add [symmetric])
   1.348 +            done
   1.349 +          then show ?thesis
   1.350 +            unfolding dvd_def by blast
   1.351          qed
   1.352        qed
   1.353      qed
   1.354 -    then have ?ths using a order_root pne by blast
   1.355 -  }
   1.356 -  moreover
   1.357 -  {
   1.358 -    assume exa: "\<not> (\<exists>a. poly p a = 0)"
   1.359 -    from fundamental_theorem_of_algebra_alt[of p] exa
   1.360 +    then show ?thesis
   1.361 +      using a order_root pne by blast
   1.362 +  next
   1.363 +    case False
   1.364 +    with fundamental_theorem_of_algebra_alt[of p]
   1.365      obtain c where ccs: "c \<noteq> 0" "p = pCons c 0"
   1.366        by blast
   1.367 -    then have pp: "\<And>x. poly p x = c"
   1.368 +    then have pp: "poly p x = c" for x
   1.369        by simp
   1.370      let ?w = "[:1/c:] * (q ^ n)"
   1.371      from ccs have "(q ^ n) = (p * ?w)"
   1.372        by simp
   1.373 -    then have ?ths
   1.374 +    then show ?thesis
   1.375        unfolding dvd_def by blast
   1.376 -  }
   1.377 -  ultimately show ?ths by blast
   1.378 +  qed
   1.379  qed
   1.380  
   1.381  lemma nullstellensatz_univariate:
   1.382 @@ -1044,43 +1027,43 @@
   1.383        by blast
   1.384    next
   1.385      case 3
   1.386 -    {
   1.387 -      assume "p dvd (q ^ (Suc n))"
   1.388 -      then obtain u where u: "q ^ (Suc n) = p * u" ..
   1.389 -      fix x
   1.390 -      assume h: "poly p x = 0" "poly q x \<noteq> 0"
   1.391 -      then have "poly (q ^ (Suc n)) x \<noteq> 0"
   1.392 +    have False if dvd: "p dvd (q ^ (Suc n))" and h: "poly p x = 0" "poly q x \<noteq> 0" for x
   1.393 +    proof -
   1.394 +      from dvd obtain u where u: "q ^ (Suc n) = p * u" ..
   1.395 +      from h have "poly (q ^ (Suc n)) x \<noteq> 0"
   1.396          by simp
   1.397 -      then have False using u h(1)
   1.398 +      with u h(1) show ?thesis
   1.399          by (simp only: poly_mult) simp
   1.400 -    }
   1.401 +    qed
   1.402      with 3 nullstellensatz_lemma[of p q "degree p"]
   1.403      show ?thesis by auto
   1.404    qed
   1.405  qed
   1.406  
   1.407  text \<open>Useful lemma\<close>
   1.408 -
   1.409  lemma constant_degree:
   1.410    fixes p :: "'a::{idom,ring_char_0} poly"
   1.411    shows "constant (poly p) \<longleftrightarrow> degree p = 0" (is "?lhs = ?rhs")
   1.412  proof
   1.413 -  assume l: ?lhs
   1.414 -  from l[unfolded constant_def, rule_format, of _ "0"]
   1.415 -  have th: "poly p = poly [:poly p 0:]"
   1.416 -    by auto
   1.417 -  then have "p = [:poly p 0:]"
   1.418 -    by (simp add: poly_eq_poly_eq_iff)
   1.419 -  then have "degree p = degree [:poly p 0:]"
   1.420 -    by simp
   1.421 -  then show ?rhs
   1.422 -    by simp
   1.423 -next
   1.424 -  assume r: ?rhs
   1.425 -  then obtain k where "p = [:k:]"
   1.426 -    by (cases p) (simp split: if_splits)
   1.427 -  then show ?lhs
   1.428 -    unfolding constant_def by auto
   1.429 +  show ?rhs if ?lhs
   1.430 +  proof -
   1.431 +    from that[unfolded constant_def, rule_format, of _ "0"]
   1.432 +    have th: "poly p = poly [:poly p 0:]"
   1.433 +      by auto
   1.434 +    then have "p = [:poly p 0:]"
   1.435 +      by (simp add: poly_eq_poly_eq_iff)
   1.436 +    then have "degree p = degree [:poly p 0:]"
   1.437 +      by simp
   1.438 +    then show ?thesis
   1.439 +      by simp
   1.440 +  qed
   1.441 +  show ?lhs if ?rhs
   1.442 +  proof -
   1.443 +    from that obtain k where "p = [:k:]"
   1.444 +      by (cases p) (simp split: if_splits)
   1.445 +    then show ?thesis
   1.446 +      unfolding constant_def by auto
   1.447 +  qed
   1.448  qed
   1.449  
   1.450  lemma divides_degree:
   1.451 @@ -1129,7 +1112,7 @@
   1.452      and lq: "p \<noteq> 0"
   1.453    shows "p dvd q \<longleftrightarrow> q = 0" (is "?lhs \<longleftrightarrow> ?rhs")
   1.454  proof
   1.455 -  assume r: ?rhs
   1.456 +  assume ?rhs
   1.457    then have "q = p * 0" by simp
   1.458    then show ?lhs ..
   1.459  next
   1.460 @@ -1154,19 +1137,21 @@
   1.461    shows "p dvd q \<longleftrightarrow> p dvd r" (is "?lhs \<longleftrightarrow> ?rhs")
   1.462  proof
   1.463    from pp' obtain t where t: "p' = p * t" ..
   1.464 -  {
   1.465 -    assume l: ?lhs
   1.466 -    then obtain u where u: "q = p * u" ..
   1.467 +  show ?rhs if ?lhs
   1.468 +  proof -
   1.469 +    from that obtain u where u: "q = p * u" ..
   1.470      have "r = p * (smult a u - t)"
   1.471        using u qrp' [symmetric] t by (simp add: algebra_simps)
   1.472 -    then show ?rhs ..
   1.473 -  next
   1.474 -    assume r: ?rhs
   1.475 -    then obtain u where u: "r = p * u" ..
   1.476 +    then show ?thesis ..
   1.477 +  qed
   1.478 +  show ?lhs if ?rhs
   1.479 +  proof -
   1.480 +    from that obtain u where u: "r = p * u" ..
   1.481      from u [symmetric] t qrp' [symmetric] a0
   1.482 -    have "q = p * smult (1/a) (u + t)" by (simp add: algebra_simps)
   1.483 -    then show ?lhs ..
   1.484 -  }
   1.485 +    have "q = p * smult (1/a) (u + t)"
   1.486 +      by (simp add: algebra_simps)
   1.487 +    then show ?thesis ..
   1.488 +  qed
   1.489  qed
   1.490  
   1.491  lemma basic_cqe_conv1: