author wenzelm Mon Jun 22 21:07:10 2015 +0200 (2015-06-22) changeset 60557 5854821993d2 parent 60556 e7003c8041e2 child 60558 4fcc6861e64f
tuned proofs;
```     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.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.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.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.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.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.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.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:
```